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. --- kernel/declareops.ml | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index cdea468ad..883896652 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -49,6 +49,11 @@ let instantiate cb c = Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c else c +let instantiate_constraints cb cst = + if cb.const_polymorphic then + Univ.subst_instance_constraints (Univ.UContext.instance cb.const_universes) cst + else cst + let body_of_constant otab cb = match cb.const_body with | Undef _ -> None | Def c -> Some (instantiate cb (force_constr c)) @@ -61,13 +66,15 @@ let type_of_constant cb = if t' == t then x else RegularArity t' | TemplateArity _ as x -> x -let constraints_of_constant otab cb = Univ.Constraint.union - (Univ.UContext.constraints cb.const_universes) - (match cb.const_body with - | Undef _ -> Univ.empty_constraint - | Def c -> Univ.empty_constraint - | OpaqueDef o -> - Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) +let constraints_of_constant otab cb = + let cst = Univ.Constraint.union + (Univ.UContext.constraints cb.const_universes) + (match cb.const_body with + | Undef _ -> Univ.empty_constraint + | Def c -> Univ.empty_constraint + | OpaqueDef o -> + Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) + in instantiate_constraints cb cst let universes_of_constant otab cb = match cb.const_body with -- cgit v1.2.3