Adding support for untyped conversion-checking

.gitignore

@@ -17,4 +17,7 @@ Makefile.coq.conf
 
 _opam
 
-*.dot
+*.dot
+docs/dependency_graph.png
+
+docs/dependency_graph.pre

Makefile

@@ -2,6 +2,8 @@
 
 all: partial-fun logrel
 
+autosubst:
+	autosubst -f -s ucoq -v ge813 -p ./theories/AutoSubst/Ast_preamble -no-static -o ./theories/AutoSubst/Ast.v ./theories/AutoSubst/Ast.sig
 partial-fun:
 	@+$(MAKE) -C coq-partialfun all
 
@@ -21,4 +23,4 @@ force _CoqProject Makefile: ;
 %: Makefile.coq force
 	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: all clean force partial-fun logrel
+.PHONY: all clean force partial-fun logrel autosubst

README.md

@@ -22,13 +22,12 @@ Browsing the development
 
 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).
 
-Syntax (re)generation
-============
+Syntax regeneration
+====================
 
-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
-re-generating the syntax.
+For simplicity, we include the syntax file (`Ast.v`) generated using [autosubst-ocaml](https://github.com/uds-psl/autosubst-ocaml).
 
-**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.
+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`.
 
 Getting started with using the development
 =================

_CoqProject

@@ -3,23 +3,32 @@
 -Q theories LogRel
 
 theories/Utils.v
-theories/BasicAst.v
+theories/Syntax/BasicAst.v
 
 theories/AutoSubst/core.v
 theories/AutoSubst/unscoped.v
 theories/AutoSubst/Ast.v
 theories/AutoSubst/Extra.v
-theories/Context.v
-theories/Notations.v
 
-theories/NormalForms.v
-theories/Weakening.v
-theories/UntypedReduction.v
-theories/UntypedValues.v
-theories/GenericTyping.v
+theories/Syntax/Context.v
+theories/Syntax/Notations.v
+theories/Syntax/TermNotations.v
+theories/Syntax/NormalForms.v
+theories/Syntax/Weakening.v
+theories/Syntax/UntypedReduction.v
+theories/Syntax/Sections.v
+theories/Syntax/All.v
 
+theories/GenericTyping.v
 theories/DeclarativeTyping.v
-theories/DeclarativeInstance.v
+
+theories/TypingProperties/PropertiesDefinition.v
+theories/TypingProperties/DeclarativeProperties.v
+theories/TypingProperties/SubstConsequences.v
+theories/TypingProperties/TypeConstructorsInj.v
+theories/TypingProperties/NeutralConvProperties.v
+theories/TypingProperties/NormalisationConsequences.v
+theories/TypingProperties/LogRelConsequences.v
 
 theories/LogicalRelation.v
 theories/LogicalRelation/Induction.v
@@ -39,44 +48,41 @@ theories/LogicalRelation/Application.v
 theories/LogicalRelation/SimpleArr.v
 theories/LogicalRelation/Id.v
 
-theories/Validity.v
-theories/Substitution/Irrelevance.v
-theories/Substitution/Properties.v
-theories/Substitution/Escape.v
-theories/Substitution/Conversion.v
-theories/Substitution/Reflexivity.v
-theories/Substitution/Reduction.v
-theories/Substitution/SingleSubst.v
-theories/Substitution/Introductions/Application.v
-theories/Substitution/Introductions/Universe.v
-theories/Substitution/Introductions/Poly.v
-theories/Substitution/Introductions/Pi.v
-theories/Substitution/Introductions/Lambda.v
-theories/Substitution/Introductions/SimpleArr.v
-theories/Substitution/Introductions/Var.v
-theories/Substitution/Introductions/Nat.v
-theories/Substitution/Introductions/Empty.v
-theories/Substitution/Introductions/Sigma.v
-theories/Substitution/Introductions/Id.v
+theories/Validity/Validity.v
+theories/Validity/Irrelevance.v
+theories/Validity/Properties.v
+theories/Validity/Escape.v
+theories/Validity/Conversion.v
+theories/Validity/Reflexivity.v
+theories/Validity/Reduction.v
+theories/Validity/SingleSubst.v
+theories/Validity/Introductions/Application.v
+theories/Validity/Introductions/Universe.v
+theories/Validity/Introductions/Poly.v
+theories/Validity/Introductions/Pi.v
+theories/Validity/Introductions/Lambda.v
+theories/Validity/Introductions/SimpleArr.v
+theories/Validity/Introductions/Var.v
+theories/Validity/Introductions/Nat.v
+theories/Validity/Introductions/Empty.v
+theories/Validity/Introductions/Sigma.v
+theories/Validity/Introductions/Id.v
 theories/Fundamental.v
 
 theories/AlgorithmicTyping.v
-theories/DeclarativeSubst.v
-theories/TypeConstructorsInj.v
-theories/Normalisation.v
-theories/Consequences.v
-
-theories/BundledAlgorithmicTyping.v
-theories/AlgorithmicConvProperties.v
-theories/AlgorithmicTypingProperties.v
-theories/TypeUniqueness.v
+theories/Algorithmic/UntypedAlgorithmicConversion.v
+theories/Algorithmic/BundledAlgorithmicTyping.v
+theories/Algorithmic/AlgorithmicConvProperties.v
+theories/Algorithmic/AlgorithmicTypingProperties.v
 
 theories/Decidability/Functions.v
+theories/Decidability/UntypedFunctions.v
 theories/Decidability/Soundness.v
+theories/Decidability/NegativeSoundness.v
 theories/Decidability/Completeness.v
 theories/Decidability/Termination.v
+theories/Decidability/UntypedSoundness.v
+theories/Decidability/UntypedCompleteness.v
 theories/Decidability.v
 
-theories/TermNotations.v
-theories/Decidability/Execution.v
-theories/Positivity.v
+theories/Decidability/Execution.v

generate_deps.pl

@@ -1,23 +1,33 @@
 print "digraph logrel_deps {\n";
-print "  node [shape = ellipse,style=filled];\n";
+# See here for color schemes: https://graphviz.org/doc/info/colors.html
+print "  node [shape = ellipse,style=filled,colorscheme = paired12];\n";
 print "  subgraph cluster_autosubst { label=\"AutoSubst\" \n}";
+print "  subgraph cluster_syntax { label=\"Syntax\" \n}";
 print "  subgraph cluster_logrel { label=\"LogicalRelation\" \n}";
 print "  subgraph cluster_subst { label=\"Validity\" \n}";
+print "  subgraph cluster_typing { label=\"Typing Properties\" \n}";
+print "  subgraph cluster_algo { label=\"Algorithmic\" \n}";
 print "  subgraph cluster_dec { label=\"Decidability\" \n}";
 while (<>) {
   if (m/.*?theories\/([^\s]*)\.vo.*:(.*)/) {
     $dests = $2 ;
     ($path,$src) = ($1 =~ s/\//\./rg =~ m/(.*\.)?([^.]*)$/);
     if ($path =~ m/AutoSubst\./) {
-      print "subgraph cluster_autosubst { \"$path$src\"[label=\"$src\",fillcolor=firebrick]}"
+      print "subgraph cluster_autosubst { \"$path$src\"[label=\"$src\",fillcolor=1]}"
+    }elsif ($path =~ m/Syntax\./) {
+      print "subgraph cluster_syntax { \"$path$src\"[label=\"$src\",fillcolor=2,fontcolor=white]}"
     }elsif ($path =~ m/LogicalRelation\./) {
-      print "subgraph cluster_logrel { \"$path$src\"[label=\"$src\",fillcolor=forestgreen]}"
-    }elsif ($path =~ m/Substitution\./) {
-      print "subgraph cluster_subst { \"$path$src\"[label=\"$src\",fillcolor=goldenrod1]}"
+      print "subgraph cluster_logrel { \"$path$src\"[label=\"$src\",fillcolor=3]}"
+    }elsif ($path =~ m/Validity\./) {
+      print "subgraph cluster_subst { \"$path$src\"[label=\"$src\",fillcolor=4,fontcolor=white]}"
+    }elsif ($path =~ m/TypingProperties\./) {
+      print "subgraph cluster_typing { \"$path$src\"[label=\"$src\",fillcolor=5]}"
+    }elsif ($path =~ m/Algorithmic\./) {
+      print "subgraph cluster_algo { \"$path$src\"[label=\"$src\",fillcolor=9]}"
     }elsif ($path =~ m/Decidability\./) {
-      print "subgraph cluster_dec { \"$path$src\"[label=\"$src\",fillcolor=deeppink3]}"
+      print "subgraph cluster_dec { \"$path$src\"[label=\"$src\",fillcolor=10,fontcolor=white]}"
     }else {
-      print "\"$path$src\"[label=\"$src\",fillcolor=dodgerblue1]"
+      print "\"$path$src\"[label=\"$src\",fillcolor=6,fontcolor=white]"
     }
     for my $dest (split(" ", $dests)) {
       $dest =~ s/\//\./g ;

opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "8.19.dev"
+version: "8.20.dev"
 maintainer: "Meven.Bertrand@univ-nantes.fr"
 dev-repo: "git+https://github.com/CoqHott/logrel-coq.git"
 bug-reports: "https://github.com/CoqHott/logrel-coq/issues"
@@ -8,11 +8,15 @@ authors: ["Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
           "Kenji Maillard <kenji.maillard@inria.fr>"
           "Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>"
 ]
+homepage: "https://github.com/CoqHott/logrel-coq"
+synopsis:"A formalisation of meta-theory for a dependent type system, in Coq"
 license: "MIT"
 depends: [
   "coq" { >= "8.20" & < "8.21~" }
   "coq-smpl"
   "coq-equations" { >= "1.3" }
+  "coq-autosubst-ocaml" {>= "1.1"}
+  "coq-metacoq-template" {>= "1.3.1"}
 ]
 build: [
   [make]