Skip to content

Commit f7f1b44

Browse files
ppedrotppedrot
authored
Merge pull request #64 from CoqHott/untyped-algo
Adding support for untyped conversion-checking
2 parents 168786b + e3b6139 commit f7f1b44

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

91 files changed

+10792
-4699
lines changed

‎.gitignore‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,4 +17,7 @@ Makefile.coq.conf
1717

1818
_opam
1919

20-
*.dot
20+
*.dot
21+
docs/dependency_graph.png
22+
23+
docs/dependency_graph.pre

‎Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22

33
all: partial-fun logrel
44

5+
autosubst:
6+
autosubst -f -s ucoq -v ge813 -p ./theories/AutoSubst/Ast_preamble -no-static -o ./theories/AutoSubst/Ast.v ./theories/AutoSubst/Ast.sig
57
partial-fun:
68
@+$(MAKE) -C coq-partialfun all
79

@@ -21,4 +23,4 @@ force _CoqProject Makefile: ;
2123
%: Makefile.coq force
2224
@+$(MAKE) -f Makefile.coq $@
2325

24-
.PHONY: all clean force partial-fun logrel
26+
.PHONY: all clean force partial-fun logrel autosubst

‎README.md‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,12 @@ Browsing the development
2222

2323
The development, rendered using `coqdoc`, can be [browsed online](https://coqhott.github.io/logrel-coq/). A dependency graph for the project is available [here](https://coqhott.github.io/logrel-coq/dependency_graph.png).
2424

25-
Syntax (re)generation
26-
============
25+
Syntax regeneration
26+
====================
2727

28-
The syntax boilerplate has been generated using AutoSubst OCaml from the root folder, with the options `-s ucoq -v ge813 -no-static -p ./theories/AutoSubst/Ast_preamble` (see the [AutoSubst OCaml documentation](https://github.com/uds-psl/autosubst-ocaml) for installation instructions). Currently, this package works only with older version of Coq (8.14), so we cannot add a recipe to the MakeFile for automatically
29-
re-generating the syntax.
28+
For simplicity, we include the syntax file (`Ast.v`) generated using [autosubst-ocaml](https://github.com/uds-psl/autosubst-ocaml).
3029

31-
**If you wish to regenerate the syntax** by hand, you need to install AutoSubst from source using Coq 8.14, and use it with the previous options.
30+
It can be re-generated using the `make autosubst` recipe, once `autosubst-ocaml` has been installed. Note that we include modified versions of the `core` and `unscoped` files, which fix their dependency inclusion. Thus, when the recipe offers to overwrite these, one should choose __not to__, and only let AutoSubst overwrite `Ast.v`.
3231

3332
Getting started with using the development
3433
=================

‎_CoqProject‎

Lines changed: 46 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -3,23 +3,32 @@
33
-Q theories LogRel
44

55
theories/Utils.v
6-
theories/BasicAst.v
6+
theories/Syntax/BasicAst.v
77

88
theories/AutoSubst/core.v
99
theories/AutoSubst/unscoped.v
1010
theories/AutoSubst/Ast.v
1111
theories/AutoSubst/Extra.v
12-
theories/Context.v
13-
theories/Notations.v
1412

15-
theories/NormalForms.v
16-
theories/Weakening.v
17-
theories/UntypedReduction.v
18-
theories/UntypedValues.v
19-
theories/GenericTyping.v
13+
theories/Syntax/Context.v
14+
theories/Syntax/Notations.v
15+
theories/Syntax/TermNotations.v
16+
theories/Syntax/NormalForms.v
17+
theories/Syntax/Weakening.v
18+
theories/Syntax/UntypedReduction.v
19+
theories/Syntax/Sections.v
20+
theories/Syntax/All.v
2021

22+
theories/GenericTyping.v
2123
theories/DeclarativeTyping.v
22-
theories/DeclarativeInstance.v
24+
25+
theories/TypingProperties/PropertiesDefinition.v
26+
theories/TypingProperties/DeclarativeProperties.v
27+
theories/TypingProperties/SubstConsequences.v
28+
theories/TypingProperties/TypeConstructorsInj.v
29+
theories/TypingProperties/NeutralConvProperties.v
30+
theories/TypingProperties/NormalisationConsequences.v
31+
theories/TypingProperties/LogRelConsequences.v
2332

2433
theories/LogicalRelation.v
2534
theories/LogicalRelation/Induction.v
@@ -39,44 +48,41 @@ theories/LogicalRelation/Application.v
3948
theories/LogicalRelation/SimpleArr.v
4049
theories/LogicalRelation/Id.v
4150

42-
theories/Validity.v
43-
theories/Substitution/Irrelevance.v
44-
theories/Substitution/Properties.v
45-
theories/Substitution/Escape.v
46-
theories/Substitution/Conversion.v
47-
theories/Substitution/Reflexivity.v
48-
theories/Substitution/Reduction.v
49-
theories/Substitution/SingleSubst.v
50-
theories/Substitution/Introductions/Application.v
51-
theories/Substitution/Introductions/Universe.v
52-
theories/Substitution/Introductions/Poly.v
53-
theories/Substitution/Introductions/Pi.v
54-
theories/Substitution/Introductions/Lambda.v
55-
theories/Substitution/Introductions/SimpleArr.v
56-
theories/Substitution/Introductions/Var.v
57-
theories/Substitution/Introductions/Nat.v
58-
theories/Substitution/Introductions/Empty.v
59-
theories/Substitution/Introductions/Sigma.v
60-
theories/Substitution/Introductions/Id.v
51+
theories/Validity/Validity.v
52+
theories/Validity/Irrelevance.v
53+
theories/Validity/Properties.v
54+
theories/Validity/Escape.v
55+
theories/Validity/Conversion.v
56+
theories/Validity/Reflexivity.v
57+
theories/Validity/Reduction.v
58+
theories/Validity/SingleSubst.v
59+
theories/Validity/Introductions/Application.v
60+
theories/Validity/Introductions/Universe.v
61+
theories/Validity/Introductions/Poly.v
62+
theories/Validity/Introductions/Pi.v
63+
theories/Validity/Introductions/Lambda.v
64+
theories/Validity/Introductions/SimpleArr.v
65+
theories/Validity/Introductions/Var.v
66+
theories/Validity/Introductions/Nat.v
67+
theories/Validity/Introductions/Empty.v
68+
theories/Validity/Introductions/Sigma.v
69+
theories/Validity/Introductions/Id.v
6170
theories/Fundamental.v
6271

6372
theories/AlgorithmicTyping.v
64-
theories/DeclarativeSubst.v
65-
theories/TypeConstructorsInj.v
66-
theories/Normalisation.v
67-
theories/Consequences.v
68-
69-
theories/BundledAlgorithmicTyping.v
70-
theories/AlgorithmicConvProperties.v
71-
theories/AlgorithmicTypingProperties.v
72-
theories/TypeUniqueness.v
73+
theories/Algorithmic/UntypedAlgorithmicConversion.v
74+
theories/Algorithmic/BundledAlgorithmicTyping.v
75+
theories/Algorithmic/AlgorithmicConvProperties.v
76+
theories/Algorithmic/AlgorithmicTypingProperties.v
7377

7478
theories/Decidability/Functions.v
79+
theories/Decidability/UntypedFunctions.v
7580
theories/Decidability/Soundness.v
81+
theories/Decidability/NegativeSoundness.v
7682
theories/Decidability/Completeness.v
7783
theories/Decidability/Termination.v
84+
theories/Decidability/UntypedSoundness.v
85+
theories/Decidability/UntypedCompleteness.v
7886
theories/Decidability.v
7987

80-
theories/TermNotations.v
81-
theories/Decidability/Execution.v
82-
theories/Positivity.v
88+
theories/Decidability/Execution.v

‎coq-partialfun‎

‎generate_deps.pl‎

Lines changed: 17 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,33 @@
11
print "digraph logrel_deps {\n";
2-
print " node [shape = ellipse,style=filled];\n";
2+
# See here for color schemes: https://graphviz.org/doc/info/colors.html
3+
print " node [shape = ellipse,style=filled,colorscheme = paired12];\n";
34
print " subgraph cluster_autosubst { label=\"AutoSubst\" \n}";
5+
print " subgraph cluster_syntax { label=\"Syntax\" \n}";
46
print " subgraph cluster_logrel { label=\"LogicalRelation\" \n}";
57
print " subgraph cluster_subst { label=\"Validity\" \n}";
8+
print " subgraph cluster_typing { label=\"Typing Properties\" \n}";
9+
print " subgraph cluster_algo { label=\"Algorithmic\" \n}";
610
print " subgraph cluster_dec { label=\"Decidability\" \n}";
711
while (<>) {
812
if (m/.*?theories\/([^\s]*)\.vo.*:(.*)/) {
913
$dests = $2 ;
1014
($path,$src) = ($1 =~ s/\//\./rg =~ m/(.*\.)?([^.]*)$/);
1115
if ($path =~ m/AutoSubst\./) {
12-
print "subgraph cluster_autosubst { \"$path$src\"[label=\"$src\",fillcolor=firebrick]}"
16+
print "subgraph cluster_autosubst { \"$path$src\"[label=\"$src\",fillcolor=1]}"
17+
}elsif ($path =~ m/Syntax\./) {
18+
print "subgraph cluster_syntax { \"$path$src\"[label=\"$src\",fillcolor=2,fontcolor=white]}"
1319
}elsif ($path =~ m/LogicalRelation\./) {
14-
print "subgraph cluster_logrel { \"$path$src\"[label=\"$src\",fillcolor=forestgreen]}"
15-
}elsif ($path =~ m/Substitution\./) {
16-
print "subgraph cluster_subst { \"$path$src\"[label=\"$src\",fillcolor=goldenrod1]}"
20+
print "subgraph cluster_logrel { \"$path$src\"[label=\"$src\",fillcolor=3]}"
21+
}elsif ($path =~ m/Validity\./) {
22+
print "subgraph cluster_subst { \"$path$src\"[label=\"$src\",fillcolor=4,fontcolor=white]}"
23+
}elsif ($path =~ m/TypingProperties\./) {
24+
print "subgraph cluster_typing { \"$path$src\"[label=\"$src\",fillcolor=5]}"
25+
}elsif ($path =~ m/Algorithmic\./) {
26+
print "subgraph cluster_algo { \"$path$src\"[label=\"$src\",fillcolor=9]}"
1727
}elsif ($path =~ m/Decidability\./) {
18-
print "subgraph cluster_dec { \"$path$src\"[label=\"$src\",fillcolor=deeppink3]}"
28+
print "subgraph cluster_dec { \"$path$src\"[label=\"$src\",fillcolor=10,fontcolor=white]}"
1929
}else {
20-
print "\"$path$src\"[label=\"$src\",fillcolor=dodgerblue1]"
30+
print "\"$path$src\"[label=\"$src\",fillcolor=6,fontcolor=white]"
2131
}
2232
for my $dest (split(" ", $dests)) {
2333
$dest =~ s/\//\./g ;

‎opam‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
opam-version: "2.0"
2-
version: "8.19.dev"
2+
version: "8.20.dev"
33
maintainer: "Meven.Bertrand@univ-nantes.fr"
44
dev-repo: "git+https://github.com/CoqHott/logrel-coq.git"
55
bug-reports: "https://github.com/CoqHott/logrel-coq/issues"
@@ -8,6 +8,8 @@ authors: ["Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
88
"Kenji Maillard <kenji.maillard@inria.fr>"
99
"Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>"
1010
]
11+
homepage: "https://github.com/CoqHott/logrel-coq"
12+
synopsis:"A formalisation of meta-theory for a dependent type system, in Coq"
1113
license: "MIT"
1214
depends: [
1315
"coq" { >= "8.20" & < "8.21~" }

0 commit comments

Comments
 (0)