diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 18 | ||||
| -rw-r--r-- | engine/evarutil.mli | 17 | ||||
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 7 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 22 | ||||
| -rw-r--r-- | engine/proofview.mli | 15 | ||||
| -rw-r--r-- | engine/uState.ml | 47 | ||||
| -rw-r--r-- | engine/uState.mli | 8 | ||||
| -rw-r--r-- | engine/univMinim.ml | 10 | ||||
| -rw-r--r-- | engine/univMinim.mli | 2 | ||||
| -rw-r--r-- | engine/univops.mli | 2 |
12 files changed, 89 insertions, 63 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index ea71be8e43..c946125d3f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -861,12 +861,12 @@ let compare_constructor_instances evd u u' = in Evd.add_universe_constraints evd soft -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [u] up to existential variable instantiation and equalisable - universes. The term [t] is interpreted in [sigma1] while [u] is - interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extension of those in [sigma1]. *) -let eq_constr_univs_test sigma1 sigma2 t u = +(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of + [t] and [u] up to existential variable instantiation and + equalisable universes. The term [t] is interpreted in [evd] while + [u] is interpreted in [extended_evd]. The universe constraints in + [extended_evd] are assumed to be an extension of those in [evd]. *) +let eq_constr_univs_test ~evd ~extended_evd t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in let t = EConstr.Unsafe.to_constr t @@ -877,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u = in let ans = UnivProblem.eq_constr_univs_infer_with - (fun t -> kind_of_term_upto sigma1 t) - (fun u -> kind_of_term_upto sigma2 u) - (universes sigma2) fold t u sigma2 + (fun t -> kind_of_term_upto evd t) + (fun u -> kind_of_term_upto extended_evd u) + (universes extended_evd) fold t u extended_evd in match ans with None -> false | Some _ -> true diff --git a/engine/evarutil.mli b/engine/evarutil.mli index e9d579af32..7877b94582 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -204,12 +204,17 @@ val finalize : ?abort_on_undefined_evars:bool -> evar_map -> val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [u] up to existential variable instantiation and equalisable - universes. The term [t] is interpreted in [sigma1] while [u] is - interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extension of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool +(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of + [t] and [u] up to existential variable instantiation and + equalisable universes. The term [t] is interpreted in [evd] while + [u] is interpreted in [extended_evd]. The universe constraints in + [extended_evd] are assumed to be an extension of those in [evd]. *) +val eq_constr_univs_test : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + constr -> + constr -> + bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns [Inl sigma'] where [sigma'] is [sigma] augmented with universe diff --git a/engine/evd.ml b/engine/evd.ml index b621a3fe2f..6a721a1a8a 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -702,7 +702,7 @@ let empty = { } let from_env e = - { empty with universes = UState.make (Environ.universes e) } + { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) } let from_ctx ctx = { empty with universes = ctx } diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 7c06bb59f1..3c383b2e00 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system @@ -38,7 +38,6 @@ exception Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!") | Exception e -> CErrors.print e | TacticFailure e -> CErrors.print e | _ -> raise CErrors.Unhandled @@ -99,7 +98,7 @@ struct let print_char = fun c -> (); fun () -> print_char c let timeout = fun n t -> (); fun () -> - Control.timeout n t () (Exception Timeout) + Control.timeout n t () (Exception Tac_Timeout) let make f = (); fun () -> try f () @@ -108,7 +107,7 @@ struct Util.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) - let print_debug s = make (fun _ -> Feedback.msg_info s) + let print_debug s = make (fun _ -> Feedback.msg_debug s) let print_info s = make (fun _ -> Feedback.msg_info s) let print_warning s = make (fun _ -> Feedback.msg_warning s) let print_notice s = make (fun _ -> Feedback.msg_notice s) diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 90c920439a..75920455ce 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system diff --git a/engine/proofview.ml b/engine/proofview.ml index 8b5bd4cd80..1f076470c1 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -849,7 +849,8 @@ let give_up = module Progress = struct - let eq_constr = Evarutil.eq_constr_univs_test + let eq_constr evd extended_evd = + Evarutil.eq_constr_univs_test ~evd ~extended_evd (** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = @@ -879,10 +880,10 @@ module Progress = struct eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body (** Equality function on goals *) - let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - eq_evar_info evars1 evars2 evi1 evi2 + let goal_equal ~evd ~extended_evd evar extended_evar = + let evi = Evd.find evd evar in + let extended_evi = Evd.find extended_evd extended_evar in + eq_evar_info evd extended_evd evi extended_evi end @@ -899,17 +900,17 @@ let tclPROGRESS t = let test = quick_test || Util.List.for_all2eq begin fun i f -> - Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f) + Progress.goal_equal ~evd:initial.solution + ~extended_evd:final.solution (drop_state i) (drop_state f) end initial.comb final.comb in if not test then tclUNIT res else - tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress.")) -exception Timeout let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") | _ -> raise CErrors.Unhandled end @@ -934,7 +935,8 @@ let tclTIMEOUT n t = end begin let open Logic_monad.NonLogical in function (e, info) -> match e with - | Logic_monad.Timeout -> return (Util.Inr (Timeout, info)) + | Logic_monad.Tac_Timeout -> + return (Util.Inr (Logic_monad.Tac_Timeout, info)) | Logic_monad.TacticFailure e -> return (Util.Inr (e, info)) | e -> Logic_monad.NonLogical.raise ~info e diff --git a/engine/proofview.mli b/engine/proofview.mli index f90f02f3e1..764a4a0058 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -398,14 +398,23 @@ val give_up : unit tactic val tclPROGRESS : 'a tactic -> 'a tactic module Progress : sig - val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool +(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether + the [evar_info] from [evd] corresponding to [evar] is equal to that + from [extended_evd] corresponding to [extended_evar], up to + existential variable instantiation and equalisable universes. The + universe constraints in [extended_evd] are assumed to be an + extension of the universe constraints in [evd]. *) + val goal_equal : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + Evar.t -> + Evar.t -> + bool end (** Checks for interrupts *) val tclCHECKINTERRUPT : unit tactic -exception Timeout - (** [tclTIMEOUT n t] can have only one success. In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic diff --git a/engine/uState.ml b/engine/uState.ml index 5ed016e0d0..cb40e6eadd 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -34,6 +34,7 @@ type t = (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) + uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) uctx_weak_constraints : UPairSet.t } @@ -47,6 +48,7 @@ let empty = uctx_univ_variables = LMap.empty; uctx_univ_algebraic = LSet.empty; uctx_universes = initial_sprop_cumulative; + uctx_universes_lbound = Univ.Level.set; uctx_initial_universes = initial_sprop_cumulative; uctx_weak_constraints = UPairSet.empty; } @@ -54,10 +56,12 @@ let elaboration_sprop_cumul = Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration" ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true -let make u = +let make ~lbound u = let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in - { empty with - uctx_universes = u; uctx_initial_universes = u} + { empty with + uctx_universes = u; + uctx_universes_lbound = lbound; + uctx_initial_universes = u} let is_empty ctx = ContextSet.is_empty ctx.uctx_local && @@ -83,7 +87,7 @@ let union ctx ctx' = let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in let declarenew g = - LSet.fold (fun u g -> UGraph.add_universe u false g) newus g + LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g in let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); @@ -99,6 +103,7 @@ let union ctx ctx' = else let cstrsr = ContextSet.constraints ctx'.uctx_local in UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); + uctx_universes_lbound = ctx.uctx_universes_lbound; uctx_weak_constraints = weak} let context_set ctx = ctx.uctx_local @@ -431,18 +436,19 @@ let check_univ_decl ~poly uctx decl = (ContextSet.constraints uctx.uctx_local); ctx -let restrict_universe_context (univs, csts) keep = +let restrict_universe_context ~lbound (univs, csts) keep = let removed = LSet.diff univs keep in if LSet.is_empty removed then univs, csts else let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in let g = UGraph.initial_universes in - let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in + let g = LSet.fold (fun v g -> if Level.is_small v then g else + UGraph.add_universe v ~lbound ~strict:false g) allunivs g in let g = UGraph.merge_constraints csts g in let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in let csts = Constraint.filter (fun (l,d,r) -> - not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in + not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = @@ -450,7 +456,7 @@ let restrict ctx vars = let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars) (fst ctx.uctx_names) vars in - let uctx' = restrict_universe_context ctx.uctx_local vars in + let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in { ctx with uctx_local = uctx' } let demote_seff_univs universes uctx = @@ -497,7 +503,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' = else ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> - try UGraph.add_universe u false g + try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g with UGraph.AlreadyDeclared when sideff -> g) levels g in @@ -544,16 +550,17 @@ let new_univ_variable ?loc rigid name | None -> add_uctx_loc u loc uctx.uctx_names in let initial = - UGraph.add_universe u false uctx.uctx_initial_universes + UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = UGraph.add_universe u false uctx.uctx_universes; + uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false + u uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u -let make_with_initial_binders e us = - let uctx = make e in +let make_with_initial_binders ~lbound e us = + let uctx = make ~lbound e in List.fold_left (fun uctx { CAst.loc; v = id } -> fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) @@ -561,10 +568,10 @@ let make_with_initial_binders e us = let add_global_univ uctx u = let initial = - UGraph.add_universe u true uctx.uctx_initial_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes in let univs = - UGraph.add_universe u true uctx.uctx_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes in { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local; uctx_initial_universes = initial; @@ -679,8 +686,9 @@ let refresh_undefined_univ_variables uctx = uctx.uctx_univ_variables LMap.empty in let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in - let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g) - (ContextSet.levels ctx') g in + let lbound = uctx.uctx_universes_lbound in + let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) + (ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; @@ -688,14 +696,16 @@ let refresh_undefined_univ_variables uctx = uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; + uctx_universes_lbound = lbound; uctx_initial_universes = initial; uctx_weak_constraints = weak; } in uctx', subst let minimize uctx = let open UnivMinim in + let lbound = uctx.uctx_universes_lbound in let ((vars',algs'), us') = - normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables + normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints in if ContextSet.equal us' uctx.uctx_local then uctx @@ -709,6 +719,7 @@ let minimize uctx = uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; + uctx_universes_lbound = lbound; uctx_initial_universes = uctx.uctx_initial_universes; uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } diff --git a/engine/uState.mli b/engine/uState.mli index 9689f2e961..52e48c4eeb 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -25,9 +25,9 @@ type t val empty : t -val make : UGraph.t -> t +val make : lbound:Univ.Level.t -> UGraph.t -> t -val make_with_initial_binders : UGraph.t -> lident list -> t +val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t val is_empty : t -> bool @@ -88,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t (** {5 Unification} *) -(** [restrict_universe_context (univs,csts) keep] restricts [univs] to +(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to the universes in [keep]. The constraints [csts] are adjusted so that transitive constraints between remaining universes (those in [keep] and those not in [univs]) are preserved. *) -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t (** [restrict uctx ctx] restricts the local universes of [uctx] to [ctx] extended by local named universes and side effect universes diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 1b7c33b9c1..30fdd28997 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -269,11 +269,11 @@ module UPairs = OrderedType.UnorderedPair(Univ.Level) module UPairSet = Set.Make (UPairs) (* TODO check is_small/sprop *) -let normalize_context_set g ctx us algs weak = +let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts + Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles @@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak = let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = LSet.fold (fun v g -> UGraph.add_universe v false g) + let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) ctx UGraph.initial_universes in let add_soft u g = if not (Level.is_small u || LSet.mem u ctx) - then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g + then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g else g in let g = Constraint.fold @@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak = (* We ignore the trivial Prop/Set <= i constraints. *) let noneqs = Constraint.filter - (fun (l,d,r) -> not ((d == Le && Level.is_small l) || + (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 21f6efe86a..72b432e62f 100644 --- a/engine/univMinim.mli +++ b/engine/univMinim.mli @@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val normalize_context_set : UGraph.t -> ContextSet.t -> +val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> diff --git a/engine/univops.mli b/engine/univops.mli index 6cc7868a38..1f1edbed16 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -15,5 +15,5 @@ open Univ val universes_of_constr : constr -> LSet.t [@@ocaml.deprecated "Use [Vars.universes_of_constr]"] -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t [@@ocaml.deprecated "Use [UState.restrict_universe_context]"] |