From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sun, 21 May 2017 14:46:30 +0200 Subject: Squashed commit of the following: Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints. --- dev/include | 1 + dev/top_printers.ml | 1 + 2 files changed, 2 insertions(+) (limited to 'dev') diff --git a/dev/include b/dev/include index 0f43f00729..4835b360db 100644 --- a/dev/include +++ b/dev/include @@ -41,6 +41,7 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; +#install_printer (* univ info *) ppuniverse_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6ae5125f6d..e902da0b19 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -215,6 +215,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx +let ppuniverse_info c = pp (Univ.pr_universe_info_ind Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- dev/base_include | 2 +- dev/include | 2 +- dev/top_printers.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'dev') diff --git a/dev/base_include b/dev/base_include index f9af0696b1..98cf67256f 100644 --- a/dev/base_include +++ b/dev/base_include @@ -196,7 +196,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; +(*let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;*) let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/dev/include b/dev/include index 4835b360db..1d87456de7 100644 --- a/dev/include +++ b/dev/include @@ -41,7 +41,7 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* univ info *) ppuniverse_info;; +#install_printer (* univ info *) ppcumulativity_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e902da0b19..abf6db1b7f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -215,7 +215,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverse_info c = pp (Univ.pr_universe_info_ind Univ.Level.pr c) +let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) -- cgit v1.2.3 From a4969591f391d857a9efd038338e1a80fc68950b Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 14 Jun 2017 16:32:47 +0200 Subject: A short cleanup --- dev/base_include | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/base_include b/dev/base_include index 98cf67256f..f9af0696b1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -196,7 +196,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -(*let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;*) +let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of -- cgit v1.2.3 From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 15 Jun 2017 16:50:05 +0200 Subject: Fix a bug in cumulativity --- dev/base_include | 2 -- dev/include | 3 ++- dev/top_printers.ml | 1 - dev/vm_printers.ml | 1 - 4 files changed, 2 insertions(+), 5 deletions(-) (limited to 'dev') diff --git a/dev/base_include b/dev/base_include index f9af0696b1..8ee1cceb23 100644 --- a/dev/base_include +++ b/dev/base_include @@ -58,8 +58,6 @@ (* Open main files *) -open API -open Grammar_API open Names open Term open Vars diff --git a/dev/include b/dev/include index 1d87456de7..31ae5da71a 100644 --- a/dev/include +++ b/dev/include @@ -41,7 +41,8 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* univ info *) ppcumulativity_info;; +#install_printer (* cumulativity info *) ppcumulativity_info;; +#install_printer (* abstract cumulativity info *) ppabstract_cumulativity_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index abf6db1b7f..ff575e432c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -8,7 +8,6 @@ (* Printers for the ocaml toplevel. *) -open API open Util open Pp open Names diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index be6b914b6b..afa94a63e0 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,4 +1,3 @@ -open API open Format open Term open Names -- cgit v1.2.3