From fe99efdbe409e47f20776c62a76d4de7f0188afc Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 11 Apr 2017 12:46:23 +0200 Subject: Update various comments to use "template polymorphism" Also remove obvious comments. --- engine/universes.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/universes.mli b/engine/universes.mli index 932de941a6..83ca1ea606 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -223,7 +223,7 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds -(** {6 Support for old-style sort-polymorphism } *) +(** {6 Support for template polymorphism } *) val solve_constraints_system : universe option array -> universe array -> universe array -> universe array -- cgit v1.2.3 From adc2035410a339cfa88dae527b631f5131adaa54 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 7 Mar 2017 18:13:07 +0100 Subject: Fix an optimization failure in tclPROGRESS. Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails. --- engine/proofview.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'engine') diff --git a/engine/proofview.ml b/engine/proofview.ml index f054038e9c..99bd4bc4ff 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -858,14 +858,12 @@ let tclPROGRESS t = let quick_test = initial.solution == final.solution && initial.comb == final.comb in - let exhaustive_test = + let test = + quick_test || Util.List.for_all2eq begin fun i f -> Progress.goal_equal initial.solution i final.solution f end initial.comb final.comb in - let test = - quick_test || exhaustive_test - in if not test then tclUNIT res else -- cgit v1.2.3 From bc6de5aa4e00dfc19c4866de4876f6213546fa5c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 24 Mar 2017 11:31:50 +0100 Subject: Code cleaning in unification algorithm for universes. This patch is only moving code around and expliciting statically the invariants of the functions, so it should be 1:1 equivalent to the other one. Amongst other goodies, the unification function is not recursive anymore, which ensures that it will terminate. --- engine/uState.ml | 125 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 64 insertions(+), 61 deletions(-) (limited to 'engine') diff --git a/engine/uState.ml b/engine/uState.ml index c66af02bb9..353d8976db 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -131,84 +131,87 @@ let instantiate_variable l b v = exception UniversesDiffer let process_universe_constraints ctx cstrs = + let open Univ in let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let normalize = Universes.normalize_universe_opt_subst vars in - let rec unify_universes fo l d r local = + let is_local l = Univ.LMap.mem l !vars in + let varinfo x = + match Univ.Universe.level x with + | None -> Inl x + | Some l -> Inr l + in + let equalize_variables fo l l' r r' local = + (** Assumes l = [l',0] and r = [r',0] *) + let () = + if is_local l' then + instantiate_variable l' r vars + else if is_local r' then + instantiate_variable r' l vars + else if not (UGraph.check_eq univs l r) then + (* Two rigid/global levels, none of them being local, + one of them being Prop/Set, disallow *) + if Univ.Level.is_small l' || Univ.Level.is_small r' then + raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + else if fo then + raise UniversesDiffer + in + Univ.enforce_eq_level l' r' local + in + let equalize_universes l r local = match varinfo l, varinfo r with + | Inr l', Inr r' -> equalize_variables false l l' r r' local + | Inr l, Inl r | Inl r, Inr l -> + let alg = Univ.LSet.mem l ctx.uctx_univ_algebraic in + let inst = Univ.univ_level_rem l r r in + if alg then (instantiate_variable l inst vars; local) + else + let lu = Univ.Universe.make l in + if Univ.univ_level_mem l r then + Univ.enforce_leq inst lu local + else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) + | Inl _, Inl _ (* both are algebraic *) -> + if UGraph.check_eq univs l r then local + else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + in + let unify_universes (l, d, r) local = let l = normalize l and r = normalize r in if Univ.Universe.equal l r then local else - let varinfo x = - match Univ.Universe.level x with - | None -> Inl x - | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l ctx.uctx_univ_algebraic) - in - if d == Universes.ULe then + match d with + | Universes.ULe -> if UGraph.check_leq univs l r then (** Keep Prop/Set <= var around if var might be instantiated by prop or set later. *) - if Univ.Universe.is_level l then - match Univ.Universe.level r with - | Some r -> - Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local - | _ -> local - else local + match Univ.Universe.level l, Univ.Universe.level r with + | Some l, Some r -> + Univ.Constraint.add (l, Univ.Le, r) local + | _ -> local else - match Univ.Universe.level r with + begin match Univ.Universe.level r with | None -> error ("Algebraic universe on the right") - | Some rl -> - if Univ.Level.is_small rl then + | Some r' -> + if Univ.Level.is_small r' then let levels = Univ.Universe.levels l in - Univ.LSet.fold (fun l local -> - if Univ.Level.is_small l || Univ.LMap.mem l !vars then - unify_universes fo (Univ.Universe.make l) Universes.UEq r local - else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None))) - levels local + let fold l' local = + let l = Univ.Universe.make l' in + if Univ.Level.is_small l' || is_local l' then + equalize_variables false l l' r r' local + else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None)) + in + Univ.LSet.fold fold levels local else Univ.enforce_leq l r local - else if d == Universes.ULub then - match varinfo l, varinfo r with - | (Inr (l, true, _), Inr (r, _, _)) - | (Inr (r, _, _), Inr (l, true, _)) -> - instantiate_variable l (Univ.Universe.make r) vars; - Univ.enforce_eq_level l r local - | Inr (_, _, _), Inr (_, _, _) -> - unify_universes true l Universes.UEq r local + end + | Universes.ULub -> + begin match Universe.level l, Universe.level r with + | Some l', Some r' -> + equalize_variables true l l' r r' local | _, _ -> assert false - else (* d = Universes.UEq *) - match varinfo l, varinfo r with - | Inr (l', lloc, _), Inr (r', rloc, _) -> - let () = - if lloc then - instantiate_variable l' r vars - else if rloc then - instantiate_variable r' l vars - else if not (UGraph.check_eq univs l r) then - (* Two rigid/global levels, none of them being local, - one of them being Prop/Set, disallow *) - if Univ.Level.is_small l' || Univ.Level.is_small r' then - raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) - else - if fo then - raise UniversesDiffer - in - Univ.enforce_eq_level l' r' local - | Inr (l, loc, alg), Inl r - | Inl r, Inr (l, loc, alg) -> - let inst = Univ.univ_level_rem l r r in - if alg then (instantiate_variable l inst vars; local) - else - let lu = Univ.Universe.make l in - if Univ.univ_level_mem l r then - Univ.enforce_leq inst lu local - else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) - | _, _ (* One of the two is algebraic or global *) -> - if UGraph.check_eq univs l r then local - else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + end + | Universes.UEq -> equalize_universes l r local in let local = - Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) - cstrs Univ.Constraint.empty + Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty in !vars, local -- cgit v1.2.3 From 051f2c1be929a46a0713b47b072bb5be0a7558d0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 24 Mar 2017 15:50:21 +0100 Subject: Fast path when checking equality of universe levels in UState. We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes. --- engine/uState.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/uState.ml b/engine/uState.ml index 353d8976db..e27d0536d6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -148,7 +148,7 @@ let process_universe_constraints ctx cstrs = instantiate_variable l' r vars else if is_local r' then instantiate_variable r' l vars - else if not (UGraph.check_eq univs l r) then + else if not (UGraph.check_eq_level univs l' r') then (* Two rigid/global levels, none of them being local, one of them being Prop/Set, disallow *) if Univ.Level.is_small l' || Univ.Level.is_small r' then -- cgit v1.2.3 From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- engine/termops.ml | 24 ------------------------ 1 file changed, 24 deletions(-) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index 64f4c6dc5e..29dcddbb02 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -612,30 +612,6 @@ let adjust_app_array_size f1 l1 f2 l2 = let extras,restl1 = Array.chop (len1-len2) l1 in (mkApp (f1,extras), restl1, f2, l2) -(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate - subterms of [c]; it carries an extra data [l] (typically a name - list) which is processed by [g na] (which typically cons [na] to - [l]) at each binder traversal (with name [na]); it is not recursive - and the order with which subterms are processed is not specified *) - -let map_constr_with_named_binders g f l c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (c,k,t) -> mkCast (f l c, k, f l t) - | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c) - | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) - | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) - | App (c,al) -> mkApp (f l c, Array.map (f l) al) - | Proj (p,c) -> mkProj (p, f l c) - | Evar (e,al) -> mkEvar (e, Array.map (f l) al) - | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl) - | Fix (ln,(lna,tl,bl)) -> - let l' = Array.fold_left (fun l na -> g na l) l lna in - mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - | CoFix(ln,(lna,tl,bl)) -> - let l' = Array.fold_left (fun l na -> g na l) l lna in - mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - (* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to -- cgit v1.2.3 From 528c237b658dbba896a1fe0041990cc7fec9c4c8 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:07:32 +0200 Subject: Add [_] prefix to unused values which maybe should be kept --- engine/universes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/universes.ml b/engine/universes.ml index ad5ff827bd..ab561784c3 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -732,7 +732,7 @@ let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cs type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t -let pr_constraints_map cmap = +let _pr_constraints_map (cmap:constraints_map) = LMap.fold (fun l cstrs acc -> Level.pr l ++ str " => " ++ prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ -- cgit v1.2.3 From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:11:47 +0200 Subject: Remove unused [open] statements --- engine/eConstr.ml | 1 - engine/eConstr.mli | 1 - engine/evarutil.ml | 1 - engine/evd.ml | 4 ---- engine/proofview.mli | 1 - engine/termops.ml | 1 - engine/universes.ml | 1 - 7 files changed, 10 deletions(-) (limited to 'engine') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index bb9075e74a..54d3ce6cf7 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open CSig open CErrors open Util open Names diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 3a9469e55a..693b592fd4 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -9,7 +9,6 @@ open CSig open Names open Constr -open Context open Environ type t diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 1624dc93e4..fba4661074 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -10,7 +10,6 @@ open CErrors open Util open Names open Term -open Vars open Termops open Namegen open Pre_env diff --git a/engine/evd.ml b/engine/evd.ml index 5419a10a8e..6b1e1a855f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -14,8 +14,6 @@ open Nameops open Term open Vars open Environ -open Globnames -open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -360,8 +358,6 @@ module EvMap = Evar.Map module EvNames : sig -open Misctypes - type t val empty : t diff --git a/engine/proofview.mli b/engine/proofview.mli index a3b0304b17..da8a8fecdd 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -13,7 +13,6 @@ state and returning a value of type ['a]. *) open Util -open Term open EConstr (** Main state of tactics *) diff --git a/engine/termops.ml b/engine/termops.ml index 29dcddbb02..19e62f8e62 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1427,7 +1427,6 @@ let dependency_closure env sigma sign hyps = List.rev lh let global_app_of_constr sigma c = - let open Univ in let open Globnames in match EConstr.kind sigma c with | Const (c, u) -> (ConstRef c, u), None diff --git a/engine/universes.ml b/engine/universes.ml index ab561784c3..1900112dde 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -13,7 +13,6 @@ open Term open Environ open Univ open Globnames -open Decl_kinds let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) -- cgit v1.2.3 From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 25 Apr 2017 14:31:15 +0200 Subject: Fix 4.04 warnings --- engine/evd.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 6b1e1a855f..db048bbd6e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -15,7 +15,7 @@ open Term open Vars open Environ -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) module NamedDecl = Context.Named.Declaration (** Generic filters *) -- cgit v1.2.3 From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 1 May 2017 17:48:57 +0200 Subject: More consistent writing of de Bruijn. --- engine/evarutil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 1624dc93e4..22f93faa6f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -462,7 +462,7 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami ev (* This assumes an evar with identity instance and generalizes it over only - the De Bruijn part of the context *) + the de Bruijn part of the context *) let generalize_evar_over_rels sigma (ev,args) = let open EConstr in let evi = Evd.find sigma ev in -- cgit v1.2.3