From f52826877059858fb3fcd4314c629ed63d90a042 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Sep 2015 19:50:41 +0200 Subject: Hardening the API of evarmaps. The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap. --- engine/evd.ml | 45 +++++++++++++++++++++------------------------ engine/evd.mli | 18 ++++++++++-------- 2 files changed, 31 insertions(+), 32 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index fc4f5e040e..1af8565bdb 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -632,14 +632,30 @@ let reassign_name_defined evk evk' (evtoid,idtoev) = (EvMap.add evk' id (EvMap.remove evk evtoid), Idmap.add id evk' (Idmap.remove id idtoev)) -let add d e i = match i.evar_body with +let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with | Evar_empty -> - let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in + let evar_names = add_name_undefined naming e i d.evar_names in { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } | Evar_defined _ -> let evar_names = remove_name_possibly_already_defined e d.evar_names in { d with defn_evars = EvMap.add e i d.defn_evars; evar_names } +let add d e i = add_with_name d e i + +(** New evars *) + +let evar_counter_summary_name = "evar counter" + +(* Generator of existential names *) +let new_untyped_evar = + let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in + fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr + +let new_evar evd ?naming evi = + let evk = new_untyped_evar () in + let evd = add_with_name evd ?naming evk evi in + (evd, evk) + let remove d e = let undf_evars = EvMap.remove e d.undf_evars in let defn_evars = EvMap.remove e d.defn_evars in @@ -831,27 +847,8 @@ let define evk body evd = let evar_names = remove_name_defined evk evd.evar_names in { evd with defn_evars; undf_evars; last_mods; evar_names } -let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) - ?(filter=Filter.identity) ?candidates ?(store=Store.empty) - ?(naming=Misctypes.IntroAnonymous) evd = - let () = match Filter.repr filter with - | None -> () - | Some filter -> - assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps))) - in - let evar_info = { - evar_hyps = hyps; - evar_concl = ty; - evar_body = Evar_empty; - evar_filter = filter; - evar_source = src; - evar_candidates = candidates; - evar_extra = store; } - in - let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in - { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names } - -let restrict evk evk' filter ?candidates evd = +let restrict evk filter ?candidates evd = + let evk' = new_untyped_evar () in let evar_info = EvMap.find evk evd.undf_evars in let evar_info' = { evar_info with evar_filter = filter; @@ -863,7 +860,7 @@ let restrict evk evk' filter ?candidates evd = let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; - defn_evars; evar_names } + defn_evars; evar_names }, evk' let downcast evk ccl evd = let evar_info = EvMap.find evk evd.undf_evars in diff --git a/engine/evd.mli b/engine/evd.mli index 94d9d5f662..e240ebc310 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -143,6 +143,10 @@ val has_undefined : evar_map -> bool (** [has_undefined sigma] is [true] if and only if there are uninstantiated evars in [sigma]. *) +val new_evar : evar_map -> + ?naming:Misctypes.intro_pattern_naming_expr -> evar_info -> evar_map * evar +(** Creates a fresh evar mapping to the given information. *) + val add : evar_map -> evar -> evar_info -> evar_map (** [add sigma ev info] adds [ev] with evar info [info] in sigma. Precondition: ev must not preexist in [sigma]. *) @@ -230,14 +234,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> (** {6 Misc} *) -val evar_declare : - named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t -> - ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> evar_map -> evar_map -(** Convenience function. Just a wrapper around {!add}. *) - -val restrict : evar -> evar -> Filter.t -> ?candidates:constr list -> - evar_map -> evar_map +val restrict : evar -> Filter.t -> ?candidates:constr list -> + evar_map -> evar_map * evar (** Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates *) @@ -614,3 +612,7 @@ val create_evar_defs : evar_map -> evar_map (** Create an [evar_map] with empty meta map: *) val create_goal_evar_defs : evar_map -> evar_map + +(** {5 Summary names} *) + +val evar_counter_summary_name : string -- cgit v1.2.3 From ca14b0bb67c9db000736333a056fc147c6f5199c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Sep 2015 14:16:54 +0200 Subject: Removing uselessly duplicated function in Evd. --- engine/evd.ml | 4 ---- engine/evd.mli | 2 -- 2 files changed, 6 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 1af8565bdb..ae382cab45 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -766,10 +766,6 @@ let cmap f evd = (* spiwack: deprecated *) let create_evar_defs sigma = { sigma with conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } -(* spiwack: tentatively deprecated *) -let create_goal_evar_defs sigma = { sigma with - (* conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } *) - metas=Metamap.empty } let empty = { defn_evars = EvMap.empty; diff --git a/engine/evd.mli b/engine/evd.mli index e240ebc310..0902191818 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -611,8 +611,6 @@ val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds val create_evar_defs : evar_map -> evar_map (** Create an [evar_map] with empty meta map: *) -val create_goal_evar_defs : evar_map -> evar_map - (** {5 Summary names} *) val evar_counter_summary_name : string -- cgit v1.2.3 From 9cadb903b7c3a3be8014152b293cd5ade3a7c8b7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Sep 2015 16:36:10 +0200 Subject: Removing subst_defined_metas_evars from Evd. --- engine/evd.ml | 12 ------------ engine/evd.mli | 1 - 2 files changed, 13 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index ae382cab45..9c53006c13 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1504,18 +1504,6 @@ let retract_coercible_metas evd = let metas = Metamap.smartmapi map evd.metas in !mc, set_metas evd metas -let subst_defined_metas_evars (bl,el) c = - let rec substrec c = match kind_of_term c with - | Meta i -> - let select (j,_,_) = Int.equal i j in - substrec (pi2 (List.find select bl)) - | Evar (evk,args) -> - let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in - (try substrec (pi3 (List.find select el)) - with Not_found -> map_constr substrec c) - | _ -> map_constr substrec c - in try Some (substrec c) with Not_found -> None - let evar_source_of_meta mv evd = match meta_name evd mv with | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar) diff --git a/engine/evd.mli b/engine/evd.mli index 0902191818..cfe4adc09d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -457,7 +457,6 @@ val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map type metabinding = metavariable * constr * instance_status val retract_coercible_metas : evar_map -> metabinding list * evar_map -val subst_defined_metas_evars : metabinding list * ('a * existential * constr) list -> constr -> constr option (** {5 FIXME: Nothing to do here} *) -- cgit v1.2.3 From a3d7630d74b720b771e880dcf0fcad05de553a6e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Sep 2015 16:39:36 +0200 Subject: Removing meta_with_name from Evd. --- engine/evd.ml | 33 --------------------------------- engine/evd.mli | 1 - 2 files changed, 34 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 9c53006c13..12a04fcc22 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1451,39 +1451,6 @@ let meta_reassign mv (v, pb) evd = let meta_name evd mv = try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous -let explain_no_such_bound_variable evd id = - let mvl = - List.rev (Metamap.fold (fun n clb l -> - let na = fst (clb_name clb) in - if na != Anonymous then out_name na :: l else l) - evd.metas []) in - errorlabstrm "Evd.meta_with_name" - (str"No such bound variable " ++ pr_id id ++ - (if mvl == [] then str " (no bound variables at all in the expression)." - else - (str" (possible name" ++ - str (if List.length mvl == 1 then " is: " else "s are: ") ++ - pr_enum pr_id mvl ++ str")."))) - -let meta_with_name evd id = - let na = Name id in - let (mvl,mvnodef) = - Metamap.fold - (fun n clb (l1,l2 as l) -> - let (na',def) = clb_name clb in - if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) - else l) - evd.metas ([],[]) in - match mvnodef, mvl with - | _,[] -> - explain_no_such_bound_variable evd id - | ([n],_|_,[n]) -> - n - | _ -> - errorlabstrm "Evd.meta_with_name" - (str "Binder name \"" ++ pr_id id ++ - strbrk "\" occurs more than once in clause.") - let clear_metas evd = {evd with metas = Metamap.empty} let meta_merge evd1 evd2 = diff --git a/engine/evd.mli b/engine/evd.mli index cfe4adc09d..bc81bd8189 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -440,7 +440,6 @@ val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_ val meta_type : evar_map -> metavariable -> types val meta_ftype : evar_map -> metavariable -> types freelisted val meta_name : evar_map -> metavariable -> Name.t -val meta_with_name : evar_map -> Id.t -> metavariable val meta_declare : metavariable -> types -> ?name:Name.t -> evar_map -> evar_map val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map -- cgit v1.2.3 From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- engine/evd.ml | 44 ++++++++++++++++++++++---------------------- engine/evd.mli | 4 ++-- 2 files changed, 24 insertions(+), 24 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index cd0b52ecaa..3f4bfe7afe 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -283,8 +283,8 @@ type evar_universe_context = (** The subset of unification variables that can be instantiated with algebraic universes as they appear in types and universe instances only. *) - uctx_universes : Univ.universes; (** The current graph extended with the local constraints *) - uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *) + uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) + uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) } let empty_evar_universe_context = @@ -292,8 +292,8 @@ let empty_evar_universe_context = uctx_local = Univ.ContextSet.empty; uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; - uctx_universes = Univ.initial_universes; - uctx_initial_universes = Univ.initial_universes } + uctx_universes = UGraph.initial_universes; + uctx_initial_universes = UGraph.initial_universes } let evar_universe_context_from e = let u = universes e in @@ -314,7 +314,7 @@ let union_evar_universe_context ctx ctx' = (Univ.ContextSet.levels ctx.uctx_local) in let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in let declarenew g = - Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g + Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g in let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); @@ -328,7 +328,7 @@ let union_evar_universe_context ctx ctx' = if local == ctx.uctx_local then ctx.uctx_universes else let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) } + UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *) (* let union_evar_universe_context = *) @@ -374,7 +374,7 @@ let process_universe_constraints univs vars alg cstrs = | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg) in if d == Universes.ULe then - if Univ.check_leq univs l r then + 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 @@ -413,7 +413,7 @@ let process_universe_constraints univs vars alg cstrs = instantiate_variable l' r vars else if rloc then instantiate_variable r' l vars - else if not (Univ.check_eq univs l r) then + 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 @@ -433,7 +433,7 @@ let process_universe_constraints univs vars alg cstrs = Univ.enforce_leq inst lu local else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) | _, _ (* One of the two is algebraic or global *) -> - if Univ.check_eq univs l r then local + if UGraph.check_eq univs l r then local else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) in let local = @@ -459,7 +459,7 @@ let add_constraints_context ctx cstrs = in { ctx with uctx_local = (univs, Univ.Constraint.union local local'); uctx_univ_variables = vars; - uctx_universes = Univ.merge_constraints local' ctx.uctx_universes } + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) @@ -473,7 +473,7 @@ let add_universe_constraints_context ctx cstrs = in { ctx with uctx_local = (univs, Univ.Constraint.union local local'); uctx_univ_variables = vars; - uctx_universes = Univ.merge_constraints local' ctx.uctx_universes } + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *) (* let add_universe_constraints_context = *) @@ -1012,13 +1012,13 @@ let merge_uctx sideff rigid uctx ctx' = in let declare g = LSet.fold (fun u g -> - try Univ.add_universe u false g - with Univ.AlreadyDeclared when sideff -> g) + try UGraph.add_universe u false g + with UGraph.AlreadyDeclared when sideff -> g) levels g in let initial = declare uctx.uctx_initial_universes in let univs = declare uctx.uctx_universes in - let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in + let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } let merge_context_set rigid evd ctx' = @@ -1079,11 +1079,11 @@ let uctx_new_univ_variable rigid name predicative | None -> uctx.uctx_names in let initial = - Univ.add_universe u false uctx.uctx_initial_universes + UGraph.add_universe u false uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u false uctx.uctx_universes; + uctx_universes = UGraph.add_universe u false uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u @@ -1102,10 +1102,10 @@ let new_sort_variable ?name ?(predicative=true) rigid d = let add_global_univ d u = let uctx = d.universes in let initial = - Univ.add_universe u true uctx.uctx_initial_universes + UGraph.add_universe u true uctx.uctx_initial_universes in let univs = - Univ.add_universe u true uctx.uctx_universes + UGraph.add_universe u true uctx.uctx_universes in { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; uctx_initial_universes = initial; @@ -1245,10 +1245,10 @@ let set_leq_sort env evd s1 s2 = else evd let check_eq evd s s' = - Univ.check_eq evd.universes.uctx_universes s s' + UGraph.check_eq evd.universes.uctx_universes s s' let check_leq evd s s' = - Univ.check_leq evd.universes.uctx_universes s s' + UGraph.check_leq evd.universes.uctx_universes s s' let subst_univs_context_with_def def usubst (ctx, cst) = (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) @@ -1301,10 +1301,10 @@ let refresh_undefined_univ_variables uctx = (Option.map (Univ.subst_univs_level_universe subst) v) acc) uctx.uctx_univ_variables Univ.LMap.empty in - let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) + let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) (Univ.ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in - let univs = declare Univ.initial_universes in + let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; uctx_local = ctx'; uctx_univ_variables = vars; uctx_univ_algebraic = alg; diff --git a/engine/evd.mli b/engine/evd.mli index db60f5ff43..22d0174973 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -489,7 +489,7 @@ val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map val universe_of_name : evar_map -> string -> Univ.universe_level val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map -val universes : evar_map -> Univ.universes +val universes : evar_map -> UGraph.t val add_constraints_context : evar_universe_context -> Univ.constraints -> evar_universe_context @@ -532,7 +532,7 @@ val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst -val universes : evar_map -> Univ.universes +val universes : evar_map -> UGraph.t val merge_universe_context : evar_map -> evar_universe_context -> evar_map -- cgit v1.2.3 From 68863acca9abf4490c651df889721ef7f6a4d375 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 17 Oct 2015 15:32:03 +0200 Subject: Dedicated file for universe unification context manipulation. This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar. --- engine/engine.mllib | 1 + engine/evd.ml | 528 ++++++---------------------------------------------- engine/evd.mli | 4 +- engine/uState.ml | 484 +++++++++++++++++++++++++++++++++++++++++++++++ engine/uState.mli | 83 +++++++++ 5 files changed, 623 insertions(+), 477 deletions(-) create mode 100644 engine/uState.ml create mode 100644 engine/uState.mli (limited to 'engine') diff --git a/engine/engine.mllib b/engine/engine.mllib index dc7ff2a642..befeaa1476 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,5 +1,6 @@ Logic_monad Termops Namegen +UState Evd Proofview_monad diff --git a/engine/evd.ml b/engine/evd.ml index 79e73bda57..cfe9a3da40 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -259,221 +259,20 @@ let instantiate_evar_array info c args = | [] -> c | _ -> replace_vars inst c -module StringOrd = struct type t = string let compare = String.compare end -module UNameMap = struct - - include Map.Make(StringOrd) - - let union s t = - if s == t then s - else - merge (fun k l r -> - match l, r with - | Some _, _ -> l - | _, _ -> r) s t -end - -(* 2nd part used to check consistency on the fly. *) -type evar_universe_context = - { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; - uctx_local : Univ.universe_context_set; (** The local context of variables *) - uctx_univ_variables : Universes.universe_opt_subst; - (** The local universes that are unification variables *) - uctx_univ_algebraic : Univ.universe_set; - (** The subset of unification variables that - can be instantiated with algebraic universes as they appear in types - and universe instances only. *) - uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) - uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) - } - -let empty_evar_universe_context = - { uctx_names = UNameMap.empty, Univ.LMap.empty; - uctx_local = Univ.ContextSet.empty; - uctx_univ_variables = Univ.LMap.empty; - uctx_univ_algebraic = Univ.LSet.empty; - uctx_universes = UGraph.initial_universes; - uctx_initial_universes = UGraph.initial_universes } - -let evar_universe_context_from e = - let u = universes e in - {empty_evar_universe_context with - uctx_universes = u; uctx_initial_universes = u} - -let is_empty_evar_universe_context ctx = - Univ.ContextSet.is_empty ctx.uctx_local && - Univ.LMap.is_empty ctx.uctx_univ_variables - -let union_evar_universe_context ctx ctx' = - if ctx == ctx' then ctx - else if is_empty_evar_universe_context ctx' then ctx - else - let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in - let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in - let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) - (Univ.ContextSet.levels ctx.uctx_local) in - let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in - let declarenew g = - Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g - in - let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in - { uctx_names = (names, names_rev); - uctx_local = local; - uctx_univ_variables = - Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; - uctx_univ_algebraic = - Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; - uctx_initial_universes = declarenew ctx.uctx_initial_universes; - uctx_universes = - if local == ctx.uctx_local then ctx.uctx_universes - else - let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } - -(* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *) -(* let union_evar_universe_context = *) -(* Profile.profile2 union_evar_universe_context_key union_evar_universe_context;; *) - +type evar_universe_context = UState.t type 'a in_evar_universe_context = 'a * evar_universe_context -let evar_universe_context_set diff ctx = - let initctx = ctx.uctx_local in - let cstrs = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty - in - Univ.ContextSet.add_constraints cstrs initctx - -let evar_universe_context_constraints ctx = snd ctx.uctx_local -let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local - -let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx } -let evar_universe_context_subst ctx = ctx.uctx_univ_variables - -let instantiate_variable l b v = - v := Univ.LMap.add l (Some b) !v - -exception UniversesDiffer - -let process_universe_constraints univs vars alg cstrs = - let vars = ref vars in - let normalize = Universes.normalize_universe_opt_subst vars in - let rec unify_universes fo 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 alg) - in - if d == Universes.ULe then - 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 - else - match Univ.Universe.level r with - | None -> error ("Algebraic universe on the right") - | Some rl -> - if Univ.Level.is_small rl 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 - 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 - | _, _ -> 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)) - in - let local = - Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) - cstrs Univ.Constraint.empty - in - !vars, local - -let add_constraints_context ctx cstrs = - let univs, local = ctx.uctx_local in - let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> - let l = Univ.Universe.make l and r = Univ.Universe.make r in - let cstr' = - if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r) - else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r) - in Universes.Constraints.add cstr' acc) - cstrs Universes.Constraints.empty - in - let vars, local' = - process_universe_constraints ctx.uctx_universes - ctx.uctx_univ_variables ctx.uctx_univ_algebraic - cstrs' - in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } - -(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) -(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) - -let add_universe_constraints_context ctx cstrs = - let univs, local = ctx.uctx_local in - let vars, local' = - process_universe_constraints ctx.uctx_universes - ctx.uctx_univ_variables ctx.uctx_univ_algebraic - cstrs - in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } +let empty_evar_universe_context = UState.empty +let evar_universe_context_from = UState.from +let is_empty_evar_universe_context = UState.is_empty +let union_evar_universe_context = UState.union +let evar_universe_context_set = UState.context_set +let evar_universe_context_constraints = UState.constraints +let evar_context_universe_context = UState.context +let evar_universe_context_of = UState.of_context_set +let evar_universe_context_subst = UState.subst +let add_constraints_context = UState.add_constraints +let add_universe_constraints_context = UState.add_universe_constraints (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *) (* let add_universe_constraints_context = *) @@ -937,7 +736,7 @@ let evars_of_filtered_evar_info evi = (**********************************************************) (* Sort variables *) -type rigid = +type rigid = UState.rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) @@ -947,146 +746,32 @@ let univ_flexible_alg = UnivFlexible true let evar_universe_context d = d.universes -let universe_context_set d = d.universes.uctx_local - -let pr_uctx_level uctx = - let map, map_rev = uctx.uctx_names in - fun l -> - try str(Univ.LMap.find l map_rev) - with Not_found -> - Universes.pr_with_global_universes l - -let universe_context ?names evd = - match names with - | None -> Univ.ContextSet.to_context evd.universes.uctx_local - | Some pl -> - let levels = Univ.ContextSet.levels evd.universes.uctx_local in - let newinst, left = - List.fold_right - (fun (loc,id) (newinst, acc) -> - let l = - try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names) - with Not_found -> - user_err_loc (loc, "universe_context", - str"Universe " ++ pr_id id ++ str" is not bound anymore.") - in (l :: newinst, Univ.LSet.remove l acc)) - pl ([], levels) - in - if not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - errorlabstrm "universe_context" - (str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level evd.universes) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") - else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst), - Univ.ContextSet.constraints evd.universes.uctx_local) +let universe_context_set d = UState.context_set Univ.UContext.empty d.universes + +let pr_uctx_level = UState.pr_uctx_level +let universe_context ?names evd = UState.universe_context ?names evd.universes let restrict_universe_context evd vars = - let uctx = evd.universes in - let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in - { evd with universes = { uctx with uctx_local = uctx' } } - + { evd with universes = UState.restrict evd.universes vars } + let universe_subst evd = - evd.universes.uctx_univ_variables - -let merge_uctx sideff rigid uctx ctx' = - let open Univ in - let levels = ContextSet.levels ctx' in - let uctx = if sideff then uctx else - match rigid with - | UnivRigid -> uctx - | UnivFlexible b -> - let fold u accu = - if LMap.mem u accu then accu - else LMap.add u None accu - in - let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in - if b then - { uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } - else { uctx with uctx_univ_variables = uvars' } - in - let uctx_local = - if sideff then uctx.uctx_local - else ContextSet.append ctx' uctx.uctx_local - in - let declare g = - LSet.fold (fun u g -> - try UGraph.add_universe u false g - with UGraph.AlreadyDeclared when sideff -> g) - levels g - in - let initial = declare uctx.uctx_initial_universes in - let univs = declare uctx.uctx_universes in - let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in - { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } + UState.subst evd.universes let merge_context_set ?(sideff=false) rigid evd ctx' = - {evd with universes = merge_uctx sideff rigid evd.universes ctx'} + {evd with universes = UState.merge sideff rigid evd.universes ctx'} -let merge_uctx_subst uctx s = - { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } - let merge_universe_subst evd subst = - {evd with universes = merge_uctx_subst evd.universes subst } + {evd with universes = UState.merge_subst evd.universes subst } let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) -let emit_universe_side_effects eff u = - Declareops.fold_side_effects - (fun acc eff -> - match eff with - | Declarations.SEscheme (l,s) -> - List.fold_left - (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx - in if cb.Declarations.const_polymorphic then acc - else - merge_uctx true univ_rigid acc - (Univ.ContextSet.of_context cb.Declarations.const_universes)) - acc l - | Declarations.SEsubproof _ -> acc) - u eff - -let add_uctx_names s l (names, names_rev) = - (UNameMap.add s l names, Univ.LMap.add l s names_rev) - -let uctx_new_univ_variable rigid name predicative - ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level (Global.current_dirpath ()) in - let ctx' = Univ.ContextSet.add_universe u ctx in - let uctx', pred = - match rigid with - | UnivRigid -> uctx, true - | UnivFlexible b -> - let uvars' = Univ.LMap.add u None uvars in - if b then {uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = Univ.LSet.add u avars}, false - else {uctx with uctx_univ_variables = uvars'}, false - in - let names = - match name with - | Some n -> add_uctx_names n u uctx.uctx_names - | None -> uctx.uctx_names - in - let initial = - UGraph.add_universe u false 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_initial_universes = initial} - in uctx', u - let new_univ_level_variable ?name ?(predicative=true) rigid evd = - let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in + let uctx', u = UState.new_univ_variable rigid name evd.universes in ({evd with universes = uctx'}, u) let new_univ_variable ?name ?(predicative=true) rigid evd = - let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in + let uctx', u = UState.new_univ_variable rigid name evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) let new_sort_variable ?name ?(predicative=true) rigid d = @@ -1094,42 +779,12 @@ let new_sort_variable ?name ?(predicative=true) rigid d = (d', Type u) let add_global_univ d u = - let uctx = d.universes in - let initial = - UGraph.add_universe u true uctx.uctx_initial_universes - in - let univs = - UGraph.add_universe u true uctx.uctx_universes - in - { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; - uctx_initial_universes = initial; - uctx_universes = univs } } - + { d with universes = UState.add_global_univ d.universes u } + let make_flexible_variable evd b u = - let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in - let uvars' = Univ.LMap.add u None uvars in - let avars' = - if b then - let uu = Univ.Universe.make u in - let substu_not_alg u' v = - Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v - in - if not (Univ.LMap.exists substu_not_alg uvars) - then Univ.LSet.add u avars else avars - else avars - in - {evd with universes = {ctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = avars'}} - -let make_evar_universe_context e l = - let uctx = evar_universe_context_from e in - match l with - | None -> uctx - | Some us -> - List.fold_left - (fun uctx (loc,id) -> - fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx)) - uctx us + { evd with universes = UState.make_flexible_variable evd.universes b u } + +let make_evar_universe_context = UState.make (****************************************) (* Operations on constants *) @@ -1152,20 +807,11 @@ let fresh_global ?(rigid=univ_flexible) ?names env evd gr = let whd_sort_variable evd t = t -let is_sort_variable evd s = - match s with - | Type u -> - (match Univ.universe_level u with - | Some l as x -> - let uctx = evd.universes in - if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x - else None - | None -> None) - | _ -> None +let is_sort_variable evd s = UState.is_sort_variable evd.universes s let is_flexible_level evd l = let uctx = evd.universes in - Univ.LMap.mem l uctx.uctx_univ_variables + Univ.LMap.mem l (UState.subst uctx) let is_eq_sort s1 s2 = if Sorts.equal s1 s2 then None @@ -1176,12 +822,12 @@ let is_eq_sort s1 s2 = else Some (u1, u2) let normalize_universe evd = - let vars = ref evd.universes.uctx_univ_variables in + let vars = ref (UState.subst evd.universes) in let normalize = Universes.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = - let vars = ref evd.universes.uctx_univ_variables in + let vars = ref (UState.subst evd.universes) in let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l @@ -1239,96 +885,28 @@ let set_leq_sort env evd s1 s2 = else evd let check_eq evd s s' = - UGraph.check_eq evd.universes.uctx_universes s s' + UGraph.check_eq (UState.ugraph evd.universes) s s' let check_leq evd s s' = - UGraph.check_leq evd.universes.uctx_universes s s' - -let subst_univs_context_with_def def usubst (ctx, cst) = - (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) + UGraph.check_leq (UState.ugraph evd.universes) s s' -let normalize_evar_universe_context_variables uctx = - let normalized_variables, undef, def, subst = - Universes.normalize_univ_variables uctx.uctx_univ_variables - in - let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in - let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in - subst, { uctx with uctx_local = ctx_local'; - uctx_univ_variables = normalized_variables; - uctx_universes = univs } +let normalize_evar_universe_context_variables = UState.normalize_variables (* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *) (* let normalize_evar_universe_context_variables = *) (* Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *) -let abstract_undefined_variables uctx = - let vars' = - Univ.LMap.fold (fun u v acc -> - if v == None then Univ.LSet.remove u acc - else acc) - uctx.uctx_univ_variables uctx.uctx_univ_algebraic - in { uctx with uctx_local = Univ.ContextSet.empty; - uctx_univ_algebraic = vars' } - -let fix_undefined_variables ({ universes = uctx } as evm) = - let algs', vars' = - Univ.LMap.fold (fun u v (algs, vars as acc) -> - if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) - else acc) - uctx.uctx_univ_variables - (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) - in - {evm with universes = - { uctx with uctx_univ_variables = vars'; - uctx_univ_algebraic = algs' } } +let abstract_undefined_variables = UState.abstract_undefined_variables - -let refresh_undefined_univ_variables uctx = - let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in - let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) - uctx.uctx_univ_algebraic Univ.LSet.empty - in - let vars = - Univ.LMap.fold - (fun u v acc -> - Univ.LMap.add (Univ.subst_univs_level_level subst u) - (Option.map (Univ.subst_univs_level_universe subst) v) acc) - uctx.uctx_univ_variables Univ.LMap.empty - in - let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) - (Univ.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; - uctx_local = ctx'; - uctx_univ_variables = vars; uctx_univ_algebraic = alg; - uctx_universes = univs; - uctx_initial_universes = initial } in - uctx', subst +let fix_undefined_variables evd = + { evd with universes = UState.fix_undefined_variables evd.universes } let refresh_undefined_universes evd = - let uctx', subst = refresh_undefined_univ_variables evd.universes in + let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in evd', subst -let normalize_evar_universe_context uctx = - let rec fixpoint uctx = - let ((vars',algs'), us') = - Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables - uctx.uctx_univ_algebraic - in - if Univ.ContextSet.equal us' uctx.uctx_local then uctx - else - let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in - let uctx' = - { uctx_names = uctx.uctx_names; - uctx_local = us'; - uctx_univ_variables = vars'; - uctx_univ_algebraic = algs'; - uctx_universes = universes; - uctx_initial_universes = uctx.uctx_initial_universes } - in fixpoint uctx' - in fixpoint uctx +let normalize_evar_universe_context = UState.normalize let nf_univ_variables evd = let subst, uctx' = normalize_evar_universe_context_variables evd.universes in @@ -1346,14 +924,12 @@ let nf_constraints = Profile.profile1 nfconstrkey nf_constraints else nf_constraints -let universe_of_name evd s = - UNameMap.find s (fst evd.universes.uctx_names) +let universe_of_name evd s = UState.universe_of_name evd.universes s let add_universe_name evd s l = - let names' = add_uctx_names s l evd.universes.uctx_names in - {evd with universes = {evd.universes with uctx_names = names'}} + { evd with universes = UState.add_universe_name evd.universes s l } -let universes evd = evd.universes.uctx_universes +let universes evd = UState.ugraph evd.universes (* Conversion w.r.t. an evar map and its local universes. *) @@ -1362,10 +938,10 @@ let conversion_gen env evd pb t u = | Reduction.CONV -> Reduction.trans_conv_universes full_transparent_state ~evars:(existential_opt_value evd) env - evd.universes.uctx_universes t u + (UState.ugraph evd.universes) t u | Reduction.CUMUL -> Reduction.trans_conv_leq_universes full_transparent_state ~evars:(existential_opt_value evd) env - evd.universes.uctx_universes t u + (UState.ugraph evd.universes) t u (* let conversion_gen_key = Profile.declare_profile "conversion_gen" *) (* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *) @@ -1377,8 +953,10 @@ let test_conversion env d pb t u = try conversion_gen env d pb t u; true with _ -> false +exception UniversesDiffer = UState.UniversesDiffer + let eq_constr_univs evd t u = - let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in + let b, c = Universes.eq_constr_univs_infer (UState.ugraph evd.universes) t u in if b then try let evd' = add_universe_constraints evd c in evd', b with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false @@ -1393,7 +971,7 @@ let e_eq_constr_univs evdref t u = let emit_side_effects eff evd = { evd with effects = Declareops.union_side_effects eff evd.effects; - universes = emit_universe_side_effects eff evd.universes } + universes = UState.emit_side_effects eff evd.universes } let drop_side_effects evd = { evd with effects = Declareops.no_seff; } @@ -1760,11 +1338,11 @@ let pr_evar_universe_context ctx = if is_empty_evar_universe_context ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++ + h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set Univ.UContext.empty ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ - h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++ + h 0 (Univ.LSet.pr prl (UState.variables ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl()) + h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl()) let print_env_short env = let pr_body n = function diff --git a/engine/evd.mli b/engine/evd.mli index d659b8826e..796f503746 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -119,7 +119,7 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info (** {6 Unification state} **) -type evar_universe_context +type evar_universe_context = UState.t (** The universe context associated to an evar map *) type evar_map @@ -464,7 +464,7 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map (** Rigid or flexible universe variables *) -type rigid = +type rigid = UState.rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) diff --git a/engine/uState.ml b/engine/uState.ml new file mode 100644 index 0000000000..2eb0519b78 --- /dev/null +++ b/engine/uState.ml @@ -0,0 +1,484 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + match l, r with + | Some _, _ -> l + | _, _ -> r) s t +end + +(* 2nd part used to check consistency on the fly. *) +type t = + { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; + uctx_local : Univ.universe_context_set; (** The local context of variables *) + uctx_univ_variables : Universes.universe_opt_subst; + (** The local universes that are unification variables *) + uctx_univ_algebraic : Univ.universe_set; + (** The subset of unification variables that + can be instantiated with algebraic universes as they appear in types + and universe instances only. *) + uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) + uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) + } + +let empty = + { uctx_names = UNameMap.empty, Univ.LMap.empty; + uctx_local = Univ.ContextSet.empty; + uctx_univ_variables = Univ.LMap.empty; + uctx_univ_algebraic = Univ.LSet.empty; + uctx_universes = UGraph.initial_universes; + uctx_initial_universes = UGraph.initial_universes } + +let from e = + let u = Environ.universes e in + { empty with + uctx_universes = u; uctx_initial_universes = u} + +let is_empty ctx = + Univ.ContextSet.is_empty ctx.uctx_local && + Univ.LMap.is_empty ctx.uctx_univ_variables + +let union ctx ctx' = + if ctx == ctx' then ctx + else if is_empty ctx' then ctx + else + let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in + let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in + let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) + (Univ.ContextSet.levels ctx.uctx_local) in + let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in + let declarenew g = + Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g + in + let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in + { uctx_names = (names, names_rev); + uctx_local = local; + uctx_univ_variables = + Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; + uctx_univ_algebraic = + Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; + uctx_initial_universes = declarenew ctx.uctx_initial_universes; + uctx_universes = + if local == ctx.uctx_local then ctx.uctx_universes + else + let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in + UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } + +let context_set diff ctx = + let initctx = ctx.uctx_local in + let cstrs = + Univ.LSet.fold + (fun l cstrs -> + try + match Univ.LMap.find l ctx.uctx_univ_variables with + | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs + | None -> cstrs + with Not_found | Option.IsNone -> cstrs) + (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty + in + Univ.ContextSet.add_constraints cstrs initctx + +let constraints ctx = snd ctx.uctx_local + +let context ctx = Univ.ContextSet.to_context ctx.uctx_local + +let of_context_set ctx = { empty with uctx_local = ctx } + +let subst ctx = ctx.uctx_univ_variables + +let ugraph ctx = ctx.uctx_universes + +let variables ctx = ctx.uctx_univ_algebraic + +let instantiate_variable l b v = + v := Univ.LMap.add l (Some b) !v + +exception UniversesDiffer + +let process_universe_constraints univs vars alg cstrs = + let vars = ref vars in + let normalize = Universes.normalize_universe_opt_subst vars in + let rec unify_universes fo 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 alg) + in + if d == Universes.ULe then + 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 + else + match Univ.Universe.level r with + | None -> error ("Algebraic universe on the right") + | Some rl -> + if Univ.Level.is_small rl 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 + 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 + | _, _ -> 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)) + in + let local = + Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) + cstrs Univ.Constraint.empty + in + !vars, local + +let add_constraints ctx cstrs = + let univs, local = ctx.uctx_local in + let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> + let l = Univ.Universe.make l and r = Univ.Universe.make r in + let cstr' = + if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r) + else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r) + in Universes.Constraints.add cstr' acc) + cstrs Universes.Constraints.empty + in + let vars, local' = + process_universe_constraints ctx.uctx_universes + ctx.uctx_univ_variables ctx.uctx_univ_algebraic + cstrs' + in + { ctx with uctx_local = (univs, Univ.Constraint.union local local'); + uctx_univ_variables = vars; + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } + +(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) +(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) + +let add_universe_constraints ctx cstrs = + let univs, local = ctx.uctx_local in + let vars, local' = + process_universe_constraints ctx.uctx_universes + ctx.uctx_univ_variables ctx.uctx_univ_algebraic + cstrs + in + { ctx with uctx_local = (univs, Univ.Constraint.union local local'); + uctx_univ_variables = vars; + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } + +let pr_uctx_level uctx = + let map, map_rev = uctx.uctx_names in + fun l -> + try str(Univ.LMap.find l map_rev) + with Not_found -> + Universes.pr_with_global_universes l + +let universe_context ?names ctx = + match names with + | None -> Univ.ContextSet.to_context ctx.uctx_local + | Some pl -> + let levels = Univ.ContextSet.levels ctx.uctx_local in + let newinst, left = + List.fold_right + (fun (loc,id) (newinst, acc) -> + let l = + try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) + with Not_found -> + user_err_loc (loc, "universe_context", + str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + in (l :: newinst, Univ.LSet.remove l acc)) + pl ([], levels) + in + if not (Univ.LSet.is_empty left) then + let n = Univ.LSet.cardinal left in + errorlabstrm "universe_context" + (str(CString.plural n "Universe") ++ spc () ++ + Univ.LSet.pr (pr_uctx_level ctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") + else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst), + Univ.ContextSet.constraints ctx.uctx_local) + +let restrict ctx vars = + let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in + { ctx with uctx_local = uctx' } + +type rigid = + | UnivRigid + | UnivFlexible of bool (** Is substitution by an algebraic ok? *) + +let univ_rigid = UnivRigid +let univ_flexible = UnivFlexible false +let univ_flexible_alg = UnivFlexible true + +let merge sideff rigid uctx ctx' = + let open Univ in + let levels = ContextSet.levels ctx' in + let uctx = if sideff then uctx else + match rigid with + | UnivRigid -> uctx + | UnivFlexible b -> + let fold u accu = + if LMap.mem u accu then accu + else LMap.add u None accu + in + let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in + if b then + { uctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } + else { uctx with uctx_univ_variables = uvars' } + in + let uctx_local = + if sideff then uctx.uctx_local + else ContextSet.append ctx' uctx.uctx_local + in + let declare g = + LSet.fold (fun u g -> + try UGraph.add_universe u false g + with UGraph.AlreadyDeclared when sideff -> g) + levels g + in + let initial = declare uctx.uctx_initial_universes in + let univs = declare uctx.uctx_universes in + let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in + { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } + +let merge_subst uctx s = + { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } + +let emit_side_effects eff u = + Declareops.fold_side_effects + (fun acc eff -> + match eff with + | Declarations.SEscheme (l,s) -> + List.fold_left + (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (s, ctx) -> merge true univ_rigid acc ctx + in if cb.Declarations.const_polymorphic then acc + else + merge true univ_rigid acc + (Univ.ContextSet.of_context cb.Declarations.const_universes)) + acc l + | Declarations.SEsubproof _ -> acc) + u eff + +let add_uctx_names s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l s names_rev) + +let new_univ_variable rigid name + ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = + let u = Universes.new_univ_level (Global.current_dirpath ()) in + let ctx' = Univ.ContextSet.add_universe u ctx in + let uctx', pred = + match rigid with + | UnivRigid -> uctx, true + | UnivFlexible b -> + let uvars' = Univ.LMap.add u None uvars in + if b then {uctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = Univ.LSet.add u avars}, false + else {uctx with uctx_univ_variables = uvars'}, false + in + let names = + match name with + | Some n -> add_uctx_names n u uctx.uctx_names + | None -> uctx.uctx_names + in + let initial = + UGraph.add_universe u false 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_initial_universes = initial} + in uctx', u + +let add_global_univ uctx u = + let initial = + UGraph.add_universe u true uctx.uctx_initial_universes + in + let univs = + UGraph.add_universe u true uctx.uctx_universes + in + { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; + uctx_initial_universes = initial; + uctx_universes = univs } + +let make_flexible_variable ctx b u = + let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in + let uvars' = Univ.LMap.add u None uvars in + let avars' = + if b then + let uu = Univ.Universe.make u in + let substu_not_alg u' v = + Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v + in + if not (Univ.LMap.exists substu_not_alg uvars) + then Univ.LSet.add u avars else avars + else avars + in + {ctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = avars'} + +let make e l = + let uctx = from e in + match l with + | None -> uctx + | Some us -> + List.fold_left + (fun uctx (loc,id) -> + fst (new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) + uctx us + +let is_sort_variable uctx s = + match s with + | Sorts.Type u -> + (match Univ.universe_level u with + | Some l as x -> + if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x + else None + | None -> None) + | _ -> None + +let subst_univs_context_with_def def usubst (ctx, cst) = + (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) + +let normalize_variables uctx = + let normalized_variables, undef, def, subst = + Universes.normalize_univ_variables uctx.uctx_univ_variables + in + let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in + let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in + subst, { uctx with uctx_local = ctx_local'; + uctx_univ_variables = normalized_variables; + uctx_universes = univs } + +let abstract_undefined_variables uctx = + let vars' = + Univ.LMap.fold (fun u v acc -> + if v == None then Univ.LSet.remove u acc + else acc) + uctx.uctx_univ_variables uctx.uctx_univ_algebraic + in { uctx with uctx_local = Univ.ContextSet.empty; + uctx_univ_algebraic = vars' } + +let fix_undefined_variables uctx = + let algs', vars' = + Univ.LMap.fold (fun u v (algs, vars as acc) -> + if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) + else acc) + uctx.uctx_univ_variables + (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) + in + { uctx with uctx_univ_variables = vars'; + uctx_univ_algebraic = algs' } + +let refresh_undefined_univ_variables uctx = + let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in + let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) + uctx.uctx_univ_algebraic Univ.LSet.empty + in + let vars = + Univ.LMap.fold + (fun u v acc -> + Univ.LMap.add (Univ.subst_univs_level_level subst u) + (Option.map (Univ.subst_univs_level_universe subst) v) acc) + uctx.uctx_univ_variables Univ.LMap.empty + in + let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) + (Univ.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; + uctx_local = ctx'; + uctx_univ_variables = vars; uctx_univ_algebraic = alg; + uctx_universes = univs; + uctx_initial_universes = initial } in + uctx', subst + +let normalize uctx = + let rec fixpoint uctx = + let ((vars',algs'), us') = + Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables + uctx.uctx_univ_algebraic + in + if Univ.ContextSet.equal us' uctx.uctx_local then uctx + else + let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in + let uctx' = + { uctx_names = uctx.uctx_names; + uctx_local = us'; + uctx_univ_variables = vars'; + uctx_univ_algebraic = algs'; + uctx_universes = universes; + uctx_initial_universes = uctx.uctx_initial_universes } + in fixpoint uctx' + in fixpoint uctx + +let universe_of_name uctx s = + UNameMap.find s (fst uctx.uctx_names) + +let add_universe_name uctx s l = + let names' = add_uctx_names s l uctx.uctx_names in + { uctx with uctx_names = names' } diff --git a/engine/uState.mli b/engine/uState.mli new file mode 100644 index 0000000000..c3b28d0a6a --- /dev/null +++ b/engine/uState.mli @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t + +val make : Environ.env -> Id.t Loc.located list option -> t + +val is_empty : t -> bool + +val union : t -> t -> t + +val of_context_set : Univ.universe_context_set -> t + +(** {5 Projections} *) + +val context_set : Univ.universe_context -> t -> Univ.universe_context_set +val constraints : t -> Univ.constraints +val context : t -> Univ.universe_context +val subst : t -> Universes.universe_opt_subst +val ugraph : t -> UGraph.t +val variables : t -> Univ.LSet.t + +(** {5 Constraints handling} *) + +val add_constraints : t -> Univ.constraints -> t +val add_universe_constraints : t -> Universes.universe_constraints -> t + +(** {5 TODO: Document me} *) + +val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context + +val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds + +val restrict : t -> Univ.universe_set -> t + +type rigid = + | UnivRigid + | UnivFlexible of bool (** Is substitution by an algebraic ok? *) + +val univ_rigid : rigid +val univ_flexible : rigid +val univ_flexible_alg : rigid + +val merge : bool -> rigid -> t -> Univ.universe_context_set -> t +val merge_subst : t -> Universes.universe_opt_subst -> t +val emit_side_effects : Declareops.side_effects -> t -> t + +val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t +val add_global_univ : t -> Univ.Level.t -> t +val make_flexible_variable : t -> bool -> Univ.Level.t -> t + +val is_sort_variable : t -> Sorts.t -> Univ.Level.t option + +val normalize_variables : t -> Univ.universe_subst * t + +val abstract_undefined_variables : t -> t + +val fix_undefined_variables : t -> t + +val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst + +val normalize : t -> t + +val universe_of_name : t -> string -> Univ.Level.t + +val add_universe_name : t -> string -> Univ.Level.t -> t -- cgit v1.2.3 From d558bf5289e87899a850dda410a3a3c4de1ce979 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 17 Oct 2015 18:55:42 +0200 Subject: Clarifying and documenting the UState API. --- engine/evd.ml | 22 +++++++++++++++------- engine/evd.mli | 4 +++- engine/uState.ml | 41 ++++++++++++++--------------------------- engine/uState.mli | 54 ++++++++++++++++++++++++++++++++++++++++++------------ 4 files changed, 74 insertions(+), 47 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index cfe9a3da40..52bfc2d1d1 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -263,7 +263,6 @@ type evar_universe_context = UState.t type 'a in_evar_universe_context = 'a * evar_universe_context let empty_evar_universe_context = UState.empty -let evar_universe_context_from = UState.from let is_empty_evar_universe_context = UState.is_empty let union_evar_universe_context = UState.union let evar_universe_context_set = UState.context_set @@ -273,6 +272,7 @@ let evar_universe_context_of = UState.of_context_set let evar_universe_context_subst = UState.subst let add_constraints_context = UState.add_constraints let add_universe_constraints_context = UState.add_universe_constraints +let constrain_variables = UState.constrain_variables (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *) (* let add_universe_constraints_context = *) @@ -587,7 +587,7 @@ let empty = { } let from_env e = - { empty with universes = evar_universe_context_from e } + { empty with universes = UState.make (Environ.universes e) } let from_ctx ctx = { empty with universes = ctx } @@ -746,7 +746,7 @@ let univ_flexible_alg = UnivFlexible true let evar_universe_context d = d.universes -let universe_context_set d = UState.context_set Univ.UContext.empty d.universes +let universe_context_set d = UState.context_set d.universes let pr_uctx_level = UState.pr_uctx_level let universe_context ?names evd = UState.universe_context ?names evd.universes @@ -784,8 +784,16 @@ let add_global_univ d u = let make_flexible_variable evd b u = { evd with universes = UState.make_flexible_variable evd.universes b u } -let make_evar_universe_context = UState.make - +let make_evar_universe_context e l = + let uctx = UState.make (Environ.universes e) in + match l with + | None -> uctx + | Some us -> + List.fold_left + (fun uctx (loc,id) -> + fst (UState.new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) + uctx us + (****************************************) (* Operations on constants *) (****************************************) @@ -1338,9 +1346,9 @@ let pr_evar_universe_context ctx = if is_empty_evar_universe_context ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set Univ.UContext.empty ctx)) ++ fnl () ++ + h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ - h 0 (Univ.LSet.pr prl (UState.variables ctx)) ++ fnl() ++ + h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl()) diff --git a/engine/evd.mli b/engine/evd.mli index 796f503746..dc498ed42e 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -474,7 +474,7 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * evar_universe_context -val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set +val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set val evar_universe_context_constraints : evar_universe_context -> Univ.constraints val evar_context_universe_context : evar_universe_context -> Univ.universe_context val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context @@ -482,6 +482,8 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst +val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints + val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 2eb0519b78..227c4ad52b 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -47,8 +47,7 @@ let empty = uctx_universes = UGraph.initial_universes; uctx_initial_universes = UGraph.initial_universes } -let from e = - let u = Environ.universes e in +let make u = { empty with uctx_universes = u; uctx_initial_universes = u} @@ -82,20 +81,8 @@ let union ctx ctx' = let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } -let context_set diff ctx = - let initctx = ctx.uctx_local in - let cstrs = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty - in - Univ.ContextSet.add_constraints cstrs initctx - +let context_set ctx = ctx.uctx_local + let constraints ctx = snd ctx.uctx_local let context ctx = Univ.ContextSet.to_context ctx.uctx_local @@ -106,7 +93,17 @@ let subst ctx = ctx.uctx_univ_variables let ugraph ctx = ctx.uctx_universes -let variables ctx = ctx.uctx_univ_algebraic +let algebraics ctx = ctx.uctx_univ_algebraic + +let constrain_variables diff ctx = + Univ.LSet.fold + (fun l cstrs -> + try + match Univ.LMap.find l ctx.uctx_univ_variables with + | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs + | None -> cstrs + with Not_found | Option.IsNone -> cstrs) + diff Univ.Constraint.empty let instantiate_variable l b v = v := Univ.LMap.add l (Some b) !v @@ -381,16 +378,6 @@ let make_flexible_variable ctx b u = {ctx with uctx_univ_variables = uvars'; uctx_univ_algebraic = avars'} -let make e l = - let uctx = from e in - match l with - | None -> uctx - | Some us -> - List.fold_left - (fun uctx (loc,id) -> - fst (new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) - uctx us - let is_sort_variable uctx s = match s with | Sorts.Type u -> diff --git a/engine/uState.mli b/engine/uState.mli index c3b28d0a6a..56e0fe14e5 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -13,14 +13,14 @@ open Names exception UniversesDiffer type t +(** Type of universe unification states. They allow the incremental building of + universe constraints during an interactive proof. *) (** {5 Constructors} *) val empty : t -val from : Environ.env -> t - -val make : Environ.env -> Id.t Loc.located list option -> t +val make : UGraph.t -> t val is_empty : t -> bool @@ -30,23 +30,47 @@ val of_context_set : Univ.universe_context_set -> t (** {5 Projections} *) -val context_set : Univ.universe_context -> t -> Univ.universe_context_set -val constraints : t -> Univ.constraints -val context : t -> Univ.universe_context +val context_set : t -> Univ.universe_context_set +(** The local context of the state, i.e. a set of bound variables together + with their associated constraints. *) + val subst : t -> Universes.universe_opt_subst +(** The local universes that are unification variables *) + val ugraph : t -> UGraph.t -val variables : t -> Univ.LSet.t +(** The current graph extended with the local constraints *) + +val algebraics : t -> Univ.LSet.t +(** The subset of unification variables that can be instantiated with algebraic + universes as they appear in types and universe instances only. *) + +val constraints : t -> Univ.constraints +(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *) + +val context : t -> Univ.universe_context +(** Shorthand for {!context_set} with {!Context_set.to_context}. *) (** {5 Constraints handling} *) val add_constraints : t -> Univ.constraints -> t +(** + @raise UniversesDiffer +*) + val add_universe_constraints : t -> Universes.universe_constraints -> t +(** + @raise UniversesDiffer +*) -(** {5 TODO: Document me} *) +(** {5 Names} *) -val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context +val add_universe_name : t -> string -> Univ.Level.t -> t +(** Associate a human-readable name to a local variable. *) -val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds +val universe_of_name : t -> string -> Univ.Level.t +(** Retrieve the universe associated to the name. *) + +(** {5 Unification} *) val restrict : t -> Univ.universe_set -> t @@ -70,6 +94,8 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t +val constrain_variables : Univ.LSet.t -> t -> Univ.constraints + val abstract_undefined_variables : t -> t val fix_undefined_variables : t -> t @@ -78,6 +104,10 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -val universe_of_name : t -> string -> Univ.Level.t +(** {5 TODO: Document me} *) -val add_universe_name : t -> string -> Univ.Level.t -> t +val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context + +(** {5 Pretty-printing} *) + +val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds -- cgit v1.2.3 From 7cfb1c359faf13cd55bd92cba21fb00ca8d2d0d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Sep 2015 19:08:11 +0200 Subject: Adding a notion of monotonous evarmap. --- engine/engine.mllib | 1 + engine/sigma.ml | 83 +++++++++++++++++++++++++++++++++++++++++++ engine/sigma.mli | 100 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 184 insertions(+) create mode 100644 engine/sigma.ml create mode 100644 engine/sigma.mli (limited to 'engine') diff --git a/engine/engine.mllib b/engine/engine.mllib index befeaa1476..7197a25838 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -3,4 +3,5 @@ Termops Namegen UState Evd +Sigma Proofview_monad diff --git a/engine/sigma.ml b/engine/sigma.ml new file mode 100644 index 0000000000..e6189e29ce --- /dev/null +++ b/engine/sigma.ml @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ) = fun _ _ -> () + +type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma + +type 'a evar = Evar.t + +let lift_evar evk () = evk + +let to_evar_map evd = evd +let to_evar evk = evk + +(** API *) + +type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh + +let new_evar sigma ?naming info = + let (sigma, evk) = Evd.new_evar sigma ?naming info in + Fresh (evk, sigma, ()) + +let define evk c sigma = + Sigma ((), Evd.define evk c sigma, ()) + +(** Run *) + +type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma } + +let run sigma f : 'a * Evd.evar_map = + let Sigma (x, sigma, ()) = f.run sigma in + (x, sigma) + +(** Monotonic references *) + +type evdref = Evd.evar_map ref + +let apply evdref f = + let Sigma (x, sigma, ()) = f.run !evdref in + evdref := sigma; + x + +let purify f = + let f (sigma : Evd.evar_map) = + let evdref = ref sigma in + let ans = f evdref in + Sigma (ans, !evdref, ()) + in + { run = f } + +(** Unsafe primitives *) + +module Unsafe = +struct + +let le = () +let of_evar_map sigma = sigma +let of_evar evk = evk +let of_ref ref = ref +let of_pair (x, sigma) = Sigma (x, sigma, ()) + +end + +module Notations = +struct + type ('a, 'r) sigma_ = ('a, 'r) sigma = + Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_ + + let (+>) = fun _ _ -> () + + type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma } +end diff --git a/engine/sigma.mli b/engine/sigma.mli new file mode 100644 index 0000000000..f4c47e08c6 --- /dev/null +++ b/engine/sigma.mli @@ -0,0 +1,100 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ('b, 'c) le -> ('a, 'c) le +(** Transitivity of anteriority *) + +val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le +(** Alias for {!cons} *) + +(** {5 Monotonous evarmaps} *) + +type 'r t +(** Stage-indexed evarmaps. *) + +type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma +(** Return values at a later stage *) + +type 'r evar +(** Stage-indexed evars *) + +(** {5 Postponing} *) + +val lift_evar : 'r evar -> ('r, 's) le -> 's evar +(** Any evar existing at stage ['r] is also valid at any later stage. *) + +(** {5 Downcasting} *) + +val to_evar_map : 'r t -> Evd.evar_map +val to_evar : 'r evar -> Evar.t + +(** {5 Monotonous API} *) + +type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh + +val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr -> + Evd.evar_info -> 'r fresh + +val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma + +(** FILLME *) + +(** {5 Run} *) + +type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma } + +val run : Evd.evar_map -> 'a run -> 'a * Evd.evar_map + +(** {5 Imperative monotonic functions} *) + +type evdref +(** Monotonic references over evarmaps *) + +val apply : evdref -> 'a run -> 'a +(** Apply a monotonic function on a reference. *) + +val purify : (evdref -> 'a) -> 'a run +(** Converse of {!apply}. *) + +(** {5 Unsafe primitives} *) + +module Unsafe : +sig + val le : ('a, 'b) le + val of_evar_map : Evd.evar_map -> 'r t + val of_evar : Evd.evar -> 'r evar + val of_ref : Evd.evar_map ref -> evdref + val of_pair : ('a * Evd.evar_map) -> ('a, 'r) sigma +end + +(** {5 Notations} *) + +module Notations : +sig + type ('a, 'r) sigma_ = ('a, 'r) sigma = + Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_ + + type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma } + + val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le + (** Alias for {!cons} *) +end -- cgit v1.2.3 From 94502de7ecf7db3830b2e419f43627fa2c8c1c87 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Oct 2015 18:47:50 +0200 Subject: Removing some unsafe uses of monotonicity. --- engine/sigma.ml | 10 ++++++++++ engine/sigma.mli | 16 ++++++++++++++++ 2 files changed, 26 insertions(+) (limited to 'engine') diff --git a/engine/sigma.ml b/engine/sigma.ml index e6189e29ce..e3e83b6024 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -23,6 +23,8 @@ let lift_evar evk () = evk let to_evar_map evd = evd let to_evar evk = evk +let here x s = Sigma (x, s, ()) + (** API *) type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh @@ -34,6 +36,14 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) +let fresh_constructor_instance env sigma pc = + let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in + Sigma (c, sigma, ()) + +let fresh_global ?rigid ?names env sigma r = + let (sigma, c) = Evd.fresh_global ?rigid ?names env sigma r in + Sigma (c, sigma, ()) + (** Run *) type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma } diff --git a/engine/sigma.mli b/engine/sigma.mli index f4c47e08c6..6ac56bb3e2 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names +open Constr + (** Monotonous state enforced by typing. This module allows to constrain uses of evarmaps in a monotonous fashion, @@ -37,6 +40,11 @@ type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma type 'r evar (** Stage-indexed evars *) +(** {5 Constructors} *) + +val here : 'a -> 'r t -> ('a, 'r) sigma +(** [here x s] is a shorthand for [Sigma (x, s, refl)] *) + (** {5 Postponing} *) val lift_evar : 'r evar -> ('r, 's) le -> 's evar @@ -56,6 +64,14 @@ val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr -> val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma +(** Polymorphic universes *) + +val fresh_constructor_instance : Environ.env -> 'r t -> constructor -> + (pconstructor, 'r) sigma + +val fresh_global : ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> + 'r t -> Globnames.global_reference -> (constr, 'r) sigma + (** FILLME *) (** {5 Run} *) -- cgit v1.2.3 From f02f64a21863ce03f2da4ff04cd003051f96801f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 29 Oct 2015 18:18:43 +0100 Subject: Removing some goal unsafeness in inductive schemes. --- engine/sigma.ml | 12 ++++++++++++ engine/sigma.mli | 6 ++++++ 2 files changed, 18 insertions(+) (limited to 'engine') diff --git a/engine/sigma.ml b/engine/sigma.ml index e3e83b6024..e886b0d1e7 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,6 +36,18 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) +let fresh_sort_in_family ?rigid env sigma s = + let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in + Sigma (s, sigma, ()) + +let fresh_constant_instance env sigma cst = + let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in + Sigma (cst, sigma, ()) + +let fresh_inductive_instance env sigma ind = + let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in + Sigma (ind, sigma, ()) + let fresh_constructor_instance env sigma pc = let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in Sigma (c, sigma, ()) diff --git a/engine/sigma.mli b/engine/sigma.mli index 6ac56bb3e2..cb948dba59 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -66,6 +66,12 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) +val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env -> + 'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma +val fresh_constant_instance : + Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma +val fresh_inductive_instance : + Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma val fresh_constructor_instance : Environ.env -> 'r t -> constructor -> (pconstructor, 'r) sigma -- cgit v1.2.3 From b58e8aa6525d45473f88fbea71bab88a2b46c825 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 25 Nov 2015 20:44:08 +0100 Subject: More invariants in UState. --- engine/uState.ml | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) (limited to 'engine') diff --git a/engine/uState.ml b/engine/uState.ml index a00d9ccd14..c1aa75c091 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -115,12 +115,14 @@ let of_binders b = in { ctx with uctx_names = names } let instantiate_variable l b v = - v := Univ.LMap.add l (Some b) !v + try v := Univ.LMap.update l (Some b) !v + with Not_found -> assert false exception UniversesDiffer -let process_universe_constraints univs vars alg cstrs = - let vars = ref vars in +let process_universe_constraints ctx cstrs = + 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 l = normalize l and r = normalize r in @@ -129,7 +131,7 @@ let process_universe_constraints univs vars alg cstrs = 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 alg) + | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l ctx.uctx_univ_algebraic) in if d == Universes.ULe then if UGraph.check_leq univs l r then @@ -210,11 +212,7 @@ let add_constraints ctx cstrs = in Universes.Constraints.add cstr' acc) cstrs Universes.Constraints.empty in - let vars, local' = - process_universe_constraints ctx.uctx_universes - ctx.uctx_univ_variables ctx.uctx_univ_algebraic - cstrs' - in + let vars, local' = process_universe_constraints ctx cstrs' in { ctx with uctx_local = (univs, Univ.Constraint.union local local'); uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } @@ -224,11 +222,7 @@ let add_constraints ctx cstrs = let add_universe_constraints ctx cstrs = let univs, local = ctx.uctx_local in - let vars, local' = - process_universe_constraints ctx.uctx_universes - ctx.uctx_univ_variables ctx.uctx_univ_algebraic - cstrs - in + let vars, local' = process_universe_constraints ctx cstrs in { ctx with uctx_local = (univs, Univ.Constraint.union local local'); uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } -- cgit v1.2.3 From 103ec7205d9038f1f3821f9287e3bb0907a1e3ec Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 19 Nov 2015 13:36:31 +0100 Subject: More efficient implementation of equality-up-to-universes in Universes. Instead of accumulating constraints which are not present in the original graph, we parametrize the equality function by a function actually merging those constraints in the current graph. This prevents doing the work twice. --- engine/evd.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 069fcbfa6e..00a869fda8 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -962,11 +962,13 @@ let test_conversion env d pb t u = exception UniversesDiffer = UState.UniversesDiffer let eq_constr_univs evd t u = - let b, c = Universes.eq_constr_univs_infer (UState.ugraph evd.universes) t u in - if b then - try let evd' = add_universe_constraints evd c in evd', b - with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false - else evd, b + let fold cstr sigma = + try Some (add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | UniversesDiffer -> None + in + match Universes.eq_constr_univs_infer (UState.ugraph evd.universes) fold t u evd with + | None -> evd, false + | Some evd -> evd, true let e_eq_constr_univs evdref t u = let evd, b = eq_constr_univs !evdref t u in -- cgit v1.2.3 From f7030a3358dda9bbc6de8058ab3357be277c031a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 Nov 2015 14:19:37 +0100 Subject: Remove unneeded fixpoint in normalize_context_set. Note that it is no longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l). --- engine/evd.ml | 34 ++++++---------------------------- engine/uState.ml | 30 ++++++++++++++---------------- engine/uState.mli | 2 +- 3 files changed, 21 insertions(+), 45 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 00a869fda8..425b67e080 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -275,9 +275,6 @@ let add_universe_constraints_context = UState.add_universe_constraints let constrain_variables = UState.constrain_variables let evar_universe_context_of_binders = UState.of_binders -(* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *) -(* let add_universe_constraints_context = *) -(* Profile.profile2 addunivconstrkey add_universe_constraints_context;; *) (*******************************************************************) (* Metamaps *) @@ -860,12 +857,9 @@ let set_eq_sort env d s1 s2 = d let has_lub evd u1 u2 = - (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *) - (* (\* let dref, norm = memo_normalize_universe d in *\) *) - (* let u1 = normalize u1 and u2 = normalize u2 in *) - if Univ.Universe.equal u1 u2 then evd - else add_universe_constraints evd - (Universes.Constraints.singleton (u1,Universes.ULub,u2)) + if Univ.Universe.equal u1 u2 then evd + else add_universe_constraints evd + (Universes.Constraints.singleton (u1,Universes.ULub,u2)) let set_eq_level d u1 u2 = add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty) @@ -883,15 +877,9 @@ let set_leq_sort env evd s1 s2 = match is_eq_sort s1 s2 with | None -> evd | Some (u1, u2) -> - (* if Univ.is_type0_univ u2 then *) - (* if Univ.is_small_univ u1 then evd *) - (* else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *) - (* else if Univ.is_type0m_univ u2 then *) - (* raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *) - (* else *) - if not (type_in_type env) then - add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) - else evd + if not (type_in_type env) then + add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) + else evd let check_eq evd s s' = UGraph.check_eq (UState.ugraph evd.universes) s s' @@ -901,10 +889,6 @@ let check_leq evd s s' = let normalize_evar_universe_context_variables = UState.normalize_variables -(* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *) -(* let normalize_evar_universe_context_variables = *) -(* Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *) - let abstract_undefined_variables = UState.abstract_undefined_variables let fix_undefined_variables evd = @@ -927,12 +911,6 @@ let nf_constraints evd = let uctx' = normalize_evar_universe_context uctx' in {evd with universes = uctx'} -let nf_constraints = - if Flags.profile then - let nfconstrkey = Profile.declare_profile "nf_constraints" in - Profile.profile1 nfconstrkey nf_constraints - else nf_constraints - let universe_of_name evd s = UState.universe_of_name evd.universes s let add_universe_name evd s l = diff --git a/engine/uState.ml b/engine/uState.ml index c1aa75c091..75c03bc89c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -434,23 +434,21 @@ let refresh_undefined_univ_variables uctx = uctx', subst let normalize uctx = - let rec fixpoint uctx = - let ((vars',algs'), us') = - Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables - uctx.uctx_univ_algebraic + let ((vars',algs'), us') = + Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables + uctx.uctx_univ_algebraic + in + if Univ.ContextSet.equal us' uctx.uctx_local then uctx + else + let us', universes = + Universes.refresh_constraints uctx.uctx_initial_universes us' in - if Univ.ContextSet.equal us' uctx.uctx_local then uctx - else - let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in - let uctx' = - { uctx_names = uctx.uctx_names; - uctx_local = us'; - uctx_univ_variables = vars'; - uctx_univ_algebraic = algs'; - uctx_universes = universes; - uctx_initial_universes = uctx.uctx_initial_universes } - in fixpoint uctx' - in fixpoint uctx + { uctx_names = uctx.uctx_names; + uctx_local = us'; + uctx_univ_variables = vars'; + uctx_univ_algebraic = algs'; + uctx_universes = universes; + uctx_initial_universes = uctx.uctx_initial_universes } let universe_of_name uctx s = UNameMap.find s (fst uctx.uctx_names) diff --git a/engine/uState.mli b/engine/uState.mli index 3a6f77e14e..a188a5269f 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -44,7 +44,7 @@ val ugraph : t -> UGraph.t val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic - universes as they appear in types and universe instances only. *) + universes as they appear in inferred types only. *) val constraints : t -> Univ.constraints (** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *) -- cgit v1.2.3 From 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Nov 2015 09:54:42 +0100 Subject: Moving three related small half-general half-ad-hoc utility functions next to each other, waiting for possible integration into a more uniform API. --- engine/termops.ml | 28 ++++++++++++++++++++++++++++ engine/termops.mli | 10 ++++++++++ 2 files changed, 38 insertions(+) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index ebd9d939aa..5716a19dd1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -846,6 +846,34 @@ let decompose_prod_letin : constr -> int * rel_context * constr = | _ -> i,l,c in prodec_rec 0 [] +(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction + * gives n (casts are ignored) *) +let nb_lam = + let rec nbrec n c = match kind_of_term c with + | Lambda (_,_,c) -> nbrec (n+1) c + | Cast (c,_,_) -> nbrec n c + | _ -> n + in + nbrec 0 + +(* similar to nb_lam, but gives the number of products instead *) +let nb_prod = + let rec nbrec n c = match kind_of_term c with + | Prod (_,_,c) -> nbrec (n+1) c + | Cast (c,_,_) -> nbrec n c + | _ -> n + in + nbrec 0 + +let nb_prod_modulo_zeta x = + let rec count n c = + match kind_of_term c with + Prod(_,_,t) -> count (n+1) t + | LetIn(_,a,_,t) -> count n (subst1 a t) + | Cast(c,_,_) -> count n c + | _ -> n + in count 0 x + let align_prod_letin c a : rel_context * constr = let (lc,_,_) = decompose_prod_letin c in let (la,l,a) = decompose_prod_letin a in diff --git a/engine/termops.mli b/engine/termops.mli index 6c680005db..5d812131ed 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -174,6 +174,16 @@ val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst val decompose_prod_letin : constr -> int * rel_context * constr val align_prod_letin : constr -> constr -> rel_context * constr +(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction + gives {% $ %}n{% $ %} (casts are ignored) *) +val nb_lam : constr -> int + +(** Similar to [nb_lam], but gives the number of products instead *) +val nb_prod : constr -> int + +(** Similar to [nb_prod], but zeta-contracts let-in on the way *) +val nb_prod_modulo_zeta : constr -> int + (** Get the last arg of a constr intended to be an application *) val last_arg : constr -> constr -- cgit v1.2.3 From ade2363e357db3ac3f258e645fe6bba988e7e7dd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 19 Nov 2015 22:49:25 +0100 Subject: About building of substitutions from instances. Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev. --- engine/termops.ml | 10 ---------- engine/termops.mli | 2 +- 2 files changed, 1 insertion(+), 11 deletions(-) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index 5716a19dd1..63baec129e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -953,16 +953,6 @@ let smash_rel_context sign = aux (List.rev (substl_rel_context [b] (List.rev acc))) l in List.rev (aux [] sign) -let adjust_subst_to_rel_context sign l = - let rec aux subst sign l = - match sign, l with - | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' - | (_,Some c,_)::sign', args' -> - aux (substl subst c :: subst) sign' args' - | [], [] -> List.rev subst - | _ -> anomaly (Pp.str "Instance and signature do not match") - in aux [] (List.rev sign) l - let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let rec mem_named_context id = function diff --git a/engine/termops.mli b/engine/termops.mli index 5d812131ed..94c485a261 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -219,7 +219,7 @@ val assums_of_rel_context : rel_context -> (Name.t * constr) list val lift_rel_context : int -> rel_context -> rel_context val substl_rel_context : constr list -> rel_context -> rel_context val smash_rel_context : rel_context -> rel_context (** expand lets in context *) -val adjust_subst_to_rel_context : rel_context -> constr list -> constr list + val map_rel_context_in_env : (env -> constr -> constr) -> env -> rel_context -> rel_context val map_rel_context_with_binders : -- cgit v1.2.3 From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:17:21 +0100 Subject: Moving extended_rel_vect/extended_rel_list to the kernel. It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. --- engine/termops.ml | 13 ------------- engine/termops.mli | 4 ---- 2 files changed, 17 deletions(-) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index 63baec129e..db0f1e4db5 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -158,19 +158,6 @@ let rel_list n m = in reln [] 1 -(* Same as [rel_list] but takes a context as argument and skips let-ins *) -let extended_rel_list n hyps = - let rec reln l p = function - | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - -let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) - - - let push_rel_assum (x,t) env = push_rel (x,None,t) env let push_rels_assum assums = diff --git a/engine/termops.mli b/engine/termops.mli index 94c485a261..87f74f7435 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -37,13 +37,9 @@ val lookup_rel_id : Id.t -> rel_context -> int * constr option * types (** Functions that build argument lists matching a block of binders or a context. [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|] - [extended_rel_vect n ctx] extends the [ctx] context of length [m] - with [n] elements. *) val rel_vect : int -> int -> constr array val rel_list : int -> int -> constr list -val extended_rel_list : int -> rel_context -> constr list -val extended_rel_vect : int -> rel_context -> constr array (** iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types -- cgit v1.2.3 From 3a29016f5b73815454ce8d9a74a017857e926706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 5 Dec 2015 10:28:09 +0100 Subject: Fixing compilation of mli documentation. Using dummy comment to @raise to please ocamldoc. Please change MS or PMP, if needed. --- engine/uState.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine') diff --git a/engine/uState.mli b/engine/uState.mli index a188a5269f..9dc96622ea 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -56,12 +56,12 @@ val context : t -> Univ.universe_context val add_constraints : t -> Univ.constraints -> t (** - @raise UniversesDiffer + @raise UniversesDiffer when universes differ *) val add_universe_constraints : t -> Universes.universe_constraints -> t (** - @raise UniversesDiffer + @raise UniversesDiffer when universes differ *) (** {5 Names} *) -- cgit v1.2.3 From a582737fc27da2c03c8c57c773fc4854c1e88d7a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Dec 2015 14:03:12 +0100 Subject: API: documenting context_chop and removing a duplicate. --- engine/termops.ml | 4 ++-- engine/termops.mli | 7 +++++++ 2 files changed, 9 insertions(+), 2 deletions(-) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index db0f1e4db5..c10c55220b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -992,8 +992,8 @@ let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type } let on_judgment_value f j = { j with uj_val = f j.uj_val } let on_judgment_type f j = { j with uj_type = f j.uj_type } -(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k - variables; skips let-in's *) +(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in + variables skips let-in's; let-in's in the middle are put in ctx2 *) let context_chop k ctx = let rec chop_aux acc = function | (0, l2) -> (List.rev acc, l2) diff --git a/engine/termops.mli b/engine/termops.mli index 87f74f7435..6083f1ab59 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -202,7 +202,14 @@ val ids_of_named_context : named_context -> Id.t list val ids_of_context : env -> Id.t list val names_of_rel_context : env -> names_context +(* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has + [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, + starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) val context_chop : int -> rel_context -> rel_context * rel_context + +(* [env_rel_context_chop n env] extracts out the [n] top declarations + of the rel_context part of [env], counting both local definitions and + hypotheses *) val env_rel_context_chop : int -> env -> env * rel_context (** Set of local names *) -- cgit v1.2.3 From 39b13903e7a6824f4405f61bb4b41a30cfbd0b3c Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 9 Dec 2015 12:30:32 +0100 Subject: CLEANUP: in the Reduction module --- engine/evd.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 425b67e080..2060141644 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -926,10 +926,10 @@ let update_sigma_env evd env = let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> - Reduction.trans_conv_universes + Reduction.conv_universes full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + | Reduction.CUMUL -> Reduction.conv_leq_universes full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u -- cgit v1.2.3 From 672f8ee0c96584735294641bb4b8760e25197b80 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 14 Dec 2015 12:52:49 +0100 Subject: CLEANUP: in the Reduction module --- engine/evd.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 2060141644..6651ff5f63 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -926,12 +926,12 @@ let update_sigma_env evd env = let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> - Reduction.conv_universes - full_transparent_state ~evars:(existential_opt_value evd) env - (UState.ugraph evd.universes) t u - | Reduction.CUMUL -> Reduction.conv_leq_universes - full_transparent_state ~evars:(existential_opt_value evd) env - (UState.ugraph evd.universes) t u + Reduction.conv env + ~evars:((existential_opt_value evd), (UState.ugraph evd.universes)) + t u + | Reduction.CUMUL -> Reduction.conv_leq env + ~evars:((existential_opt_value evd), (UState.ugraph evd.universes)) + t u let test_conversion env d pb t u = try test_conversion_gen env d pb t u; true -- cgit v1.2.3 From 42db8dc57c5d96812520e594d31a22dc242ae848 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:17:32 +0100 Subject: Remove duplicate declarations. --- engine/evd.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'engine') diff --git a/engine/evd.mli b/engine/evd.mli index 57399f2b5e..220c693ad6 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -494,8 +494,6 @@ val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map val universe_of_name : evar_map -> string -> Univ.universe_level val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map -val universes : evar_map -> UGraph.t - val add_constraints_context : evar_universe_context -> Univ.constraints -> evar_universe_context @@ -517,7 +515,6 @@ val is_sort_variable : evar_map -> sorts -> Univ.universe_level option not a local sort variable declared in [evm] *) val is_flexible_level : evar_map -> Univ.Level.t -> bool -val whd_sort_variable : evar_map -> constr -> constr (* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *) val normalize_universe : evar_map -> Univ.universe -> Univ.universe val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance -- cgit v1.2.3 From 2c8275ee3e0e5cd4eb8afd24047fda7f864e0e4e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 16:50:02 +0100 Subject: Remove useless rec flags. --- 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 d91b90caa2..8476db6646 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1230,7 +1230,7 @@ let pr_decl ((id,b,_),ok) = | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ print_constr c ++ str (if ok then ")" else "}") -let rec pr_evar_source = function +let pr_evar_source = function | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- engine/proofview_monad.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'engine') diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index a9faf0a833..88c5925ceb 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -108,11 +108,6 @@ module Info = struct and compress f = CList.map_filter compress_tree f - let rec is_empty = let open Trace in function - | Seq(Dispatch,brs) -> List.for_all is_empty brs - | Seq(DBranch,br) -> List.for_all is_empty br - | _ -> false - (** [with_sep] is [true] when [Tactic m] must be printed with a trailing semi-colon. *) let rec pr_tree with_sep = let open Trace in function -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- engine/evd.mli | 9 +++---- engine/namegen.mli | 13 +++++---- engine/termops.ml | 29 ++++++++++---------- engine/termops.mli | 77 +++++++++++++++++++++++++++--------------------------- 4 files changed, 62 insertions(+), 66 deletions(-) (limited to 'engine') diff --git a/engine/evd.mli b/engine/evd.mli index 57399f2b5e..34169b0214 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -10,7 +10,6 @@ open Util open Loc open Names open Term -open Context open Environ (** {5 Existential variables and unification states} @@ -105,8 +104,8 @@ type evar_info = { val make_evar : named_context_val -> types -> evar_info val evar_concl : evar_info -> constr -val evar_context : evar_info -> named_context -val evar_filtered_context : evar_info -> named_context +val evar_context : evar_info -> Context.Named.t +val evar_filtered_context : evar_info -> Context.Named.t val evar_hyps : evar_info -> named_context_val val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body @@ -223,7 +222,7 @@ val existential_opt_value : evar_map -> existential -> constr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) -val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info -> +val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> constr -> constr array -> constr @@ -423,7 +422,7 @@ val evar_list : constr -> existential list val evars_of_term : constr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : named_context -> Evar.Set.t +val evars_of_named_context : Context.Named.t -> Evar.Set.t val evars_of_filtered_evar_info : evar_info -> Evar.Set.t diff --git a/engine/namegen.mli b/engine/namegen.mli index f66bc6d88c..617f6e522a 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ (********************************************************************* @@ -39,13 +38,13 @@ val lambda_name : env -> Name.t * types * constr -> constr val prod_create : env -> types * types -> constr val lambda_create : env -> types * constr -> constr -val name_assumption : env -> rel_declaration -> rel_declaration -val name_context : env -> rel_context -> rel_context +val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t +val name_context : env -> Context.Rel.t -> Context.Rel.t -val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types -val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr -val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types -val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr +val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types +val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr +val it_mkProd_or_LetIn_name : env -> types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr (********************************************************************* Fresh names *) diff --git a/engine/termops.ml b/engine/termops.ml index c10c55220b..ce640bacf1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Environ (* Sorts and sort family *) @@ -700,9 +699,9 @@ let replace_term = replace_term_gen eq_constr let vars_of_env env = let s = - Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) + Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id s) (named_context env) ~init:Id.Set.empty in - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s @@ -728,12 +727,12 @@ let lookup_rel_of_name id names = let empty_names_context = [] let ids_of_rel_context sign = - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) sign ~init:[] let ids_of_named_context sign = - Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] + Context.Named.fold_outside (fun (id,_,_) idl -> id::idl) sign ~init:[] let ids_of_context env = (ids_of_rel_context (rel_context env)) @@ -788,7 +787,7 @@ let split_app c = match kind_of_term c with c::(Array.to_list prev), last | _ -> assert false -type subst = (rel_context*constr) Evar.Map.t +type subst = (Context.Rel.t * constr) Evar.Map.t exception CannotFilter @@ -825,7 +824,7 @@ let filtering env cv_pb c1 c2 = in aux env cv_pb c1 c2; !evm -let decompose_prod_letin : constr -> int * rel_context * constr = +let decompose_prod_letin : constr -> int * Context.Rel.t * constr = let rec prodec_rec i l c = match kind_of_term c with | Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c @@ -861,7 +860,7 @@ let nb_prod_modulo_zeta x = | _ -> n in count 0 x -let align_prod_letin c a : rel_context * constr = +let align_prod_letin c a : Context.Rel.t * constr = let (lc,_,_) = decompose_prod_letin c in let (la,l,a) = decompose_prod_letin a in if not (la >= lc) then invalid_arg "align_prod_letin"; @@ -899,10 +898,10 @@ let process_rel_context f env = let sign = named_context_val env in let rels = rel_context env in let env0 = reset_with_named_context sign env in - Context.fold_rel_context f rels ~init:env0 + Context.Rel.fold_outside f rels ~init:env0 let assums_of_rel_context sign = - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,c,t) l -> match c with Some _ -> l @@ -912,7 +911,7 @@ let assums_of_rel_context sign = let map_rel_context_in_env f env sign = let rec aux env acc = function | d::sign -> - aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign + aux (push_rel d env) (Context.Rel.Declaration.map (f env) d :: acc) sign | [] -> acc in @@ -920,10 +919,10 @@ let map_rel_context_in_env f env sign = let map_rel_context_with_binders f sign = let rec aux k = function - | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign + | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign | [] -> [] in - aux (rel_context_length sign) sign + aux (Context.Rel.length sign) sign let substl_rel_context l = map_rel_context_with_binders (fun k -> substnl l (k-1)) @@ -955,7 +954,7 @@ let compact_named_context_reverse sign = if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 then (i1::l2,c2,t2)::q else ([i1],c1,t1)::l - in Context.fold_named_context_reverse compact ~init:[] sign + in Context.Named.fold_inside compact ~init:[] sign let compact_named_context sign = List.rev (compact_named_context_reverse sign) @@ -976,7 +975,7 @@ let global_vars_set_of_decl env = function let dependency_closure env sign hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = - Context.fold_named_context_reverse + Context.Named.fold_inside (fun (hs,hl) (x,_,_ as d) -> if Id.Set.mem x hs then (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs), diff --git a/engine/termops.mli b/engine/termops.mli index 6083f1ab59..0fbd1ee82e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -9,7 +9,6 @@ open Pp open Names open Term -open Context open Environ (** printers *) @@ -22,7 +21,7 @@ val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds val print_constr_env : env -> constr -> std_ppcmds val print_named_context : env -> std_ppcmds -val pr_rel_decl : env -> rel_declaration -> std_ppcmds +val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds @@ -31,7 +30,7 @@ val push_rel_assum : Name.t * types -> env -> env val push_rels_assum : (Name.t * types) list -> env -> env val push_named_rec_types : Name.t array * types array * 'a -> env -> env -val lookup_rel_id : Id.t -> rel_context -> int * constr option * types +val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types (** Associates the contents of an identifier in a [rel_context]. Raise [Not_found] if there is no such identifier. *) @@ -42,20 +41,20 @@ val rel_vect : int -> int -> constr array val rel_list : int -> int -> constr list (** iterators/destructors on terms *) -val mkProd_or_LetIn : rel_declaration -> types -> types -val mkProd_wo_LetIn : rel_declaration -> types -> types +val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types +val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types val it_mkProd : types -> (Name.t * types) list -> types val it_mkLambda : constr -> (Name.t * types) list -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types -val it_mkProd_wo_LetIn : types -> rel_context -> types -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkNamedProd_or_LetIn : types -> named_context -> types -val it_mkNamedProd_wo_LetIn : types -> named_context -> types -val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr +val it_mkProd_or_LetIn : types -> Context.Rel.t -> types +val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr +val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types +val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types +val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr +val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr (** {6 Generic iterators on constr} *) @@ -63,11 +62,11 @@ val map_constr_with_named_binders : (Name.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_binders_left_to_right : - (rel_declaration -> 'a -> 'a) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate @@ -81,11 +80,11 @@ val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b val fold_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b val iter_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit (**********************************************************************) @@ -110,7 +109,7 @@ val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool val dependent_univs : constr -> constr -> bool val dependent_univs_no_evar : constr -> constr -> bool -val dependent_in_decl : constr -> named_declaration -> bool +val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool val count_occurrences : constr -> constr -> int val collect_metas : constr -> int list val collect_vars : constr -> Id.Set.t (** for visible vars only *) @@ -164,11 +163,11 @@ exception CannotFilter (context,term), or raises [CannotFilter]. Warning: Outer-kernel sort subtyping are taken into account: c1 has to be smaller than c2 wrt. sorts. *) -type subst = (rel_context*constr) Evar.Map.t -val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst +type subst = (Context.Rel.t * constr) Evar.Map.t +val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst -val decompose_prod_letin : constr -> int * rel_context * constr -val align_prod_letin : constr -> constr -> rel_context * constr +val decompose_prod_letin : constr -> int * Context.Rel.t * constr +val align_prod_letin : constr -> constr -> Context.Rel.t * constr (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) @@ -197,51 +196,51 @@ val add_name : Name.t -> names_context -> names_context val lookup_name_of_rel : int -> names_context -> Name.t val lookup_rel_of_name : Id.t -> names_context -> int val empty_names_context : names_context -val ids_of_rel_context : rel_context -> Id.t list -val ids_of_named_context : named_context -> Id.t list +val ids_of_rel_context : Context.Rel.t -> Id.t list +val ids_of_named_context : Context.Named.t -> Id.t list val ids_of_context : env -> Id.t list val names_of_rel_context : env -> names_context (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) -val context_chop : int -> rel_context -> rel_context * rel_context +val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t (* [env_rel_context_chop n env] extracts out the [n] top declarations of the rel_context part of [env], counting both local definitions and hypotheses *) -val env_rel_context_chop : int -> env -> env * rel_context +val env_rel_context_chop : int -> env -> env * Context.Rel.t (** Set of local names *) val vars_of_env: env -> Id.Set.t val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) -val process_rel_context : (rel_declaration -> env -> env) -> env -> env -val assums_of_rel_context : rel_context -> (Name.t * constr) list -val lift_rel_context : int -> rel_context -> rel_context -val substl_rel_context : constr list -> rel_context -> rel_context -val smash_rel_context : rel_context -> rel_context (** expand lets in context *) +val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env +val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list +val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t +val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t +val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *) val map_rel_context_in_env : - (env -> constr -> constr) -> env -> rel_context -> rel_context + (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t val map_rel_context_with_binders : - (int -> constr -> constr) -> rel_context -> rel_context + (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t val fold_named_context_both_sides : - ('a -> named_declaration -> named_declaration list -> 'a) -> - named_context -> init:'a -> 'a -val mem_named_context : Id.t -> named_context -> bool -val compact_named_context : named_context -> named_list_context -val compact_named_context_reverse : named_context -> named_list_context + ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> + Context.Named.t -> init:'a -> 'a +val mem_named_context : Id.t -> Context.Named.t -> bool +val compact_named_context : Context.Named.t -> Context.NamedList.t +val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t val clear_named_body : Id.t -> env -> env val global_vars : env -> constr -> Id.t list -val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t +val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) -val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list +val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -- cgit v1.2.3 From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: CLEANUP: Context.{Rel,Named}.Declaration.t Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- engine/evd.ml | 27 ++++---- engine/namegen.ml | 15 ++-- engine/termops.ml | 199 +++++++++++++++++++++++++++++++---------------------- engine/termops.mli | 2 +- 4 files changed, 139 insertions(+), 104 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 8f8b29d106..f1f65bd8af 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -16,6 +16,7 @@ open Vars open Termops open Environ open Globnames +open Context.Named.Declaration (** Generic filters *) module Filter : @@ -230,20 +231,20 @@ let evar_instance_array test_id info args = else instance_mismatch () | false :: filter, _ :: ctxt -> instrec filter ctxt i - | true :: filter, (id,_,_ as d) :: ctxt -> + | true :: filter, d :: ctxt -> if i < len then let c = Array.unsafe_get args i in if test_id d c then instrec filter ctxt (succ i) - else (id, c) :: instrec filter ctxt (succ i) + else (get_id d, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in match Filter.repr (evar_filter info) with | None -> - let map i (id,_,_ as d) = + let map i d = if (i < len) then let c = Array.unsafe_get args i in - if test_id d c then None else Some (id,c) + if test_id d c then None else Some (get_id d, c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -251,7 +252,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array (fun (id,_,_) -> isVarId id) info args + evar_instance_array (isVarId % get_id) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -660,7 +661,7 @@ let restrict evk filter ?candidates evd = evar_extra = Store.empty } in let evar_names = reassign_name_defined evk evk' evd.evar_names in let ctxt = Filter.filter_list filter (evar_context evar_info) in - let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in + let id_inst = Array.map_of_list (mkVar % get_id) ctxt in let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; @@ -722,10 +723,10 @@ let evars_of_term c = evrec Evar.Set.empty c let evars_of_named_context nc = - List.fold_right (fun (_, b, t) s -> + List.fold_right (fun decl s -> Option.fold_left (fun s t -> Evar.Set.union s (evars_of_term t)) - (Evar.Set.union s (evars_of_term t)) b) + (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl)) nc Evar.Set.empty let evars_of_filtered_evar_info evi = @@ -1228,8 +1229,9 @@ let pr_meta_map mmap = in prlist pr_meta_binding (metamap_to_list mmap) -let pr_decl ((id,b,_),ok) = - match b with +let pr_decl (decl,ok) = + let id = get_id decl in + match get_value decl with | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ print_constr c ++ str (if ok then ")" else "}") @@ -1346,8 +1348,9 @@ let print_env_short env = let pr_body n = function | None -> pr_name n | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in - let pr_named_decl (n, b, _) = pr_body (Name n) b in - let pr_rel_decl (n, b, _) = pr_body n b in + let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in + let pr_rel_decl decl = let open Context.Rel.Declaration in + pr_body (get_name decl) (get_value decl) in let nc = List.rev (named_context env) in let rc = List.rev (rel_context env) in str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ diff --git a/engine/namegen.ml b/engine/namegen.ml index fc3f0cc75b..6b2b585316 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -22,6 +22,7 @@ open Libnames open Globnames open Environ open Termops +open Context.Rel.Declaration (**********************************************************************) (* Conventional names *) @@ -113,7 +114,7 @@ let hdchar env c = | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env with + try match Environ.lookup_rel (n-k) env |> to_tuple with | (Name id,_,_) -> lowercase_first_char id | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) with Not_found -> "y") @@ -142,10 +143,9 @@ let prod_name = mkProd_name let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b) let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b) -let name_assumption env (na,c,t) = - match c with - | None -> (named_hd env t na, None, t) - | Some body -> (named_hd env body na, c, t) +let name_assumption env = function + | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) + | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) let name_context env hyps = snd @@ -277,11 +277,12 @@ let next_name_away = next_name_away_with_default default_non_dependent_string let make_all_name_different env = let avoid = ref (ids_of_named_context (named_context env)) in process_rel_context - (fun (na,c,t) newenv -> + (fun decl newenv -> + let (na,_,t) = to_tuple decl in let na = named_hd newenv t na in let id = next_name_away na !avoid in avoid := id::!avoid; - push_rel (Name id,c,t) newenv) + push_rel (set_name (Name id) decl) newenv) env (* 5- Looks for next fresh name outside a list; avoids also to use names that diff --git a/engine/termops.ml b/engine/termops.ml index b7d89ba7b1..f698f81513 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -15,6 +15,9 @@ open Term open Vars open Environ +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Sorts and sort family *) let print_sort = function @@ -98,26 +101,28 @@ let print_constr_env t = !term_printer t let print_constr t = !term_printer (Global.env()) t let set_print_constr f = term_printer := f -let pr_var_decl env (id,c,typ) = - let pbody = match c with - | None -> (mt ()) - | Some c -> +let pr_var_decl env decl = + let open NamedDecl in + let pbody = match decl with + | LocalAssum _ -> mt () + | LocalDef (_,c,_) -> (* Force evaluation *) let pb = print_constr_env env c in (str" := " ++ pb ++ cut () ) in - let pt = print_constr_env env typ in + let pt = print_constr_env env (get_type decl) in let ptyp = (str" : " ++ pt) in - (pr_id id ++ hov 0 (pbody ++ ptyp)) + (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp)) -let pr_rel_decl env (na,c,typ) = - let pbody = match c with - | None -> mt () - | Some c -> +let pr_rel_decl env decl = + let open RelDecl in + let pbody = match decl with + | LocalAssum _ -> mt () + | LocalDef (_,c,_) -> (* Force evaluation *) let pb = print_constr_env env c in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = print_constr_env env typ in - match na with + let ptyp = print_constr_env env (get_type decl) in + match get_name decl with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) @@ -157,42 +162,53 @@ let rel_list n m = in reln [] 1 -let push_rel_assum (x,t) env = push_rel (x,None,t) env +let push_rel_assum (x,t) env = + let open RelDecl in + push_rel (LocalAssum (x,t)) env let push_rels_assum assums = - push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums) + let open RelDecl in + push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums) let push_named_rec_types (lna,typarray,_) env = + let open NamedDecl in let ctxt = Array.map2_i (fun i na t -> match na with - | Name id -> (id, None, lift i t) + | Name id -> LocalAssum (id, lift i t) | Anonymous -> anomaly (Pp.str "Fix declarations must be named")) lna typarray in Array.fold_left (fun e assum -> push_named assum e) env ctxt let lookup_rel_id id sign = + let open RelDecl in let rec lookrec n = function - | [] -> raise Not_found - | (Anonymous, _, _) :: l -> lookrec (n + 1) l - | (Name id', b, t) :: l -> - if Names.Id.equal id' id then (n, b, t) else lookrec (n + 1) l + | [] -> + raise Not_found + | (LocalAssum (Anonymous, _) | LocalDef (Anonymous,_,_)) :: l -> + lookrec (n + 1) l + | LocalAssum (Name id', t) :: l -> + if Names.Id.equal id' id then (n,None,t) else lookrec (n + 1) l + | LocalDef (Name id', b, t) :: l -> + if Names.Id.equal id' id then (n,Some b,t) else lookrec (n + 1) l in lookrec 1 sign (* Constructs either [forall x:t, c] or [let x:=b:t in c] *) -let mkProd_or_LetIn (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> mkLetIn (na, b, t, c) +let mkProd_or_LetIn decl c = + let open RelDecl in + match decl with + | LocalAssum (na,t) -> mkProd (na, t, c) + | LocalDef (na,b,t) -> mkLetIn (na, b, t, c) (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *) -let mkProd_wo_LetIn (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> subst1 b c +let mkProd_wo_LetIn decl c = + let open RelDecl in + match decl with + | LocalAssum (na,t) -> mkProd (na, t, c) + | LocalDef (_,b,_) -> subst1 b c let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init @@ -208,10 +224,11 @@ let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_Le let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init let it_mkLambda_or_LetIn_from_no_LetIn c decls = + let open RelDecl in let rec aux k decls c = match decls with | [] -> c - | (na,Some b,t)::decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c)) - | (na,None,t)::decls -> mkLambda (na,t,aux (k-1) decls c) + | LocalDef (na,b,t) :: decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c)) + | LocalAssum (na,t) :: decls -> mkLambda (na,t,aux (k-1) decls c) in aux (List.length decls) (List.rev decls) c (* *) @@ -302,7 +319,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with (co-)fixpoint) *) let fold_rec_types g (lna,typarray,_) e = - let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> g assum e) e ctxt let map_left2 f a g b = @@ -317,7 +334,9 @@ let map_left2 f a g b = r, s end -let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with +let map_constr_with_binders_left_to_right g f l c = + let open RelDecl in + match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c | Cast (b,k,t) -> @@ -327,18 +346,18 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with else mkCast (b',k,t') | Prod (na,t,b) -> let t' = f l t in - let b' = f (g (na,None,t) l) b in + let b' = f (g (LocalAssum (na,t)) l) b in if t' == t && b' == b then c else mkProd (na, t', b') | Lambda (na,t,b) -> let t' = f l t in - let b' = f (g (na,None,t) l) b in + let b' = f (g (LocalAssum (na,t)) l) b in if t' == t && b' == b then c else mkLambda (na, t', b') | LetIn (na,bo,t,b) -> let bo' = f l bo in let t' = f l t in - let b' = f (g (na,Some bo,t) l) b in + let b' = f (g (LocalDef (na,bo,t)) l) b in if bo' == bo && t' == t && b' == b then c else mkLetIn (na, bo', t', b') | App (c,[||]) -> assert false @@ -379,7 +398,9 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with else mkCoFix (ln,(lna,tl',bl')) (* strong *) -let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with +let map_constr_with_full_binders g f l cstr = + let open RelDecl in + match kind_of_term cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> cstr | Cast (c,k, t) -> @@ -388,16 +409,16 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with if c==c' && t==t' then cstr else mkCast (c', k, t') | Prod (na,t,c) -> let t' = f l t in - let c' = f (g (na,None,t) l) c in + let c' = f (g (LocalAssum (na,t)) l) c in if t==t' && c==c' then cstr else mkProd (na, t', c') | Lambda (na,t,c) -> let t' = f l t in - let c' = f (g (na,None,t) l) c in + let c' = f (g (LocalAssum (na,t)) l) c in if t==t' && c==c' then cstr else mkLambda (na, t', c') | LetIn (na,b,t,c) -> let b' = f l b in let t' = f l t in - let c' = f (g (na,Some b,t) l) c in + let c' = f (g (LocalDef (na,b,t)) l) c in if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c') | App (c,al) -> let c' = f l c in @@ -418,7 +439,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with | Fix (ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -426,7 +447,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with | CoFix(ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -439,23 +460,25 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -let fold_constr_with_full_binders g f n acc c = match kind_of_term c with +let fold_constr_with_full_binders g f n acc c = + let open RelDecl in + match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c + | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd @@ -467,23 +490,25 @@ let fold_constr_with_binders g f n acc c = each binder traversal; it is not recursive and the order with which subterms are processed is not specified *) -let iter_constr_with_full_binders g f l c = match kind_of_term c with +let iter_constr_with_full_binders g f l c = + let open RelDecl in + match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () | Cast (c,_, t) -> f l c; f l t - | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c - | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c - | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c + | Prod (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c + | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c + | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c | App (c,args) -> f l c; Array.iter (f l) args | Proj (p,c) -> f l c | Evar (_,args) -> Array.iter (f l) args | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl | Fix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in Array.iter (f l) tl; Array.iter (f l') bl | CoFix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in Array.iter (f l) tl; Array.iter (f l') bl @@ -531,10 +556,11 @@ let occur_var env id c = in try occur_rec c; false with Occur -> true -let occur_var_in_decl env hyp (_,c,typ) = - match c with - | None -> occur_var env hyp typ - | Some body -> +let occur_var_in_decl env hyp decl = + let open NamedDecl in + match decl with + | LocalAssum (_,typ) -> occur_var env hyp typ + | LocalDef (_, body, typ) -> occur_var env hyp typ || occur_var env hyp body @@ -593,10 +619,11 @@ let dependent_no_evar = dependent_main true false let dependent_univs = dependent_main false true let dependent_univs_no_evar = dependent_main true true -let dependent_in_decl a (_,c,t) = - match c with - | None -> dependent a t - | Some body -> dependent a body || dependent a t +let dependent_in_decl a decl = + let open NamedDecl in + match decl with + | LocalAssum (_,t) -> dependent a t + | LocalDef (_, body, t) -> dependent a body || dependent a t let count_occurrences m t = let n = ref 0 in @@ -699,10 +726,10 @@ let replace_term = replace_term_gen eq_constr let vars_of_env env = let s = - Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id s) + Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s) (named_context env) ~init:Id.Set.empty in Context.Rel.fold_outside - (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s) + (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s let add_vname vars = function @@ -728,11 +755,11 @@ let empty_names_context = [] let ids_of_rel_context sign = Context.Rel.fold_outside - (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) + (fun decl l -> match RelDecl.get_name decl with Name id -> id::l | Anonymous -> l) sign ~init:[] let ids_of_named_context sign = - Context.Named.fold_outside (fun (id,_,_) idl -> id::idl) sign ~init:[] + Context.Named.fold_outside (fun decl idl -> NamedDecl.get_id decl :: idl) sign ~init:[] let ids_of_context env = (ids_of_rel_context (rel_context env)) @@ -740,7 +767,7 @@ let ids_of_context env = let names_of_rel_context env = - List.map (fun (na,_,_) -> na) (rel_context env) + List.map RelDecl.get_name (rel_context env) let is_section_variable id = try let _ = Global.lookup_named id in true @@ -813,7 +840,7 @@ let filtering env cv_pb c1 c2 = end | Prod (n,t1,c1), Prod (_,t2,c2) -> aux env cv_pb t1 t2; - aux ((n,None,t1)::env) cv_pb c1 c2 + aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2 | _, Evar (ev,_) -> define cv_pb env ev c1 | Evar (ev,_), _ -> define cv_pb env ev c2 | _ -> @@ -826,8 +853,8 @@ let filtering env cv_pb c1 c2 = let decompose_prod_letin : constr -> int * Context.Rel.t * constr = let rec prodec_rec i l c = match kind_of_term c with - | Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c - | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c + | Prod (n,t,c) -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c + | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c | Cast (c,_,_) -> prodec_rec i l c | _ -> i,l,c in prodec_rec 0 [] @@ -902,16 +929,16 @@ let process_rel_context f env = let assums_of_rel_context sign = Context.Rel.fold_outside - (fun (na,c,t) l -> - match c with - Some _ -> l - | None -> (na, t)::l) + (fun decl l -> + match decl with + | RelDecl.LocalDef _ -> l + | RelDecl.LocalAssum (na,t) -> (na, t)::l) sign ~init:[] let map_rel_context_in_env f env sign = let rec aux env acc = function | d::sign -> - aux (push_rel d env) (Context.Rel.Declaration.map (f env) d :: acc) sign + aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign | [] -> acc in @@ -919,7 +946,7 @@ let map_rel_context_in_env f env sign = let map_rel_context_with_binders f sign = let rec aux k = function - | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign + | d::sign -> RelDecl.map_constr (f k) d :: aux (k-1) sign | [] -> [] in aux (Context.Rel.length sign) sign @@ -933,21 +960,23 @@ let lift_rel_context n = let smash_rel_context sign = let rec aux acc = function | [] -> acc - | (_,None,_ as d) :: l -> aux (d::acc) l - | (_,Some b,_) :: l -> + | (RelDecl.LocalAssum _ as d) :: l -> aux (d::acc) l + | RelDecl.LocalDef (_,b,_) :: l -> (* Quadratic in the number of let but there are probably a few of them *) aux (List.rev (substl_rel_context [b] (List.rev acc))) l in List.rev (aux [] sign) let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init -let rec mem_named_context id = function - | (id',_,_) :: _ when Id.equal id id' -> true +let rec mem_named_context id ctxt = + match ctxt with + | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true | _ :: sign -> mem_named_context id sign | [] -> false let compact_named_context_reverse sign = - let compact l (i1,c1,t1) = + let compact l decl = + let (i1,c1,t1) = NamedDecl.to_tuple decl in match l with | [] -> [[i1],c1,t1] | (l2,c2,t2)::q -> @@ -959,16 +988,17 @@ let compact_named_context_reverse sign = let compact_named_context sign = List.rev (compact_named_context_reverse sign) let clear_named_body id env = + let open NamedDecl in let aux _ = function - | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t) + | LocalDef (id',c,t) when Id.equal id id' -> push_named (LocalAssum (id,t)) | d -> push_named d in fold_named_context aux env ~init:(reset_context env) let global_vars env ids = Id.Set.elements (global_vars_set env ids) let global_vars_set_of_decl env = function - | (_,None,t) -> global_vars_set env t - | (_,Some c,t) -> + | NamedDecl.LocalAssum (_,t) -> global_vars_set env t + | NamedDecl.LocalDef (_,c,t) -> Id.Set.union (global_vars_set env t) (global_vars_set env c) @@ -976,7 +1006,8 @@ let dependency_closure env sign hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = Context.Named.fold_inside - (fun (hs,hl) (x,_,_ as d) -> + (fun (hs,hl) d -> + let x = NamedDecl.get_id d in if Id.Set.mem x hs then (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs), x::hl) @@ -996,7 +1027,7 @@ let on_judgment_type f j = { j with uj_type = f j.uj_type } let context_chop k ctx = let rec chop_aux acc = function | (0, l2) -> (List.rev acc, l2) - | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t) + | (n, (RelDecl.LocalDef _ as h)::t) -> chop_aux (h::acc) (n, t) | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) | (_, []) -> anomaly (Pp.str "context_chop") in chop_aux [] (k,ctx) diff --git a/engine/termops.mli b/engine/termops.mli index 720ed3bd67..c2a4f33235 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -101,7 +101,7 @@ val occur_evar : existential_key -> types -> bool val occur_var : env -> Id.t -> types -> bool val occur_var_in_decl : env -> - Id.t -> 'a * types option * types -> bool + Id.t -> Context.Named.Declaration.t -> bool val free_rels : constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) -- cgit v1.2.3 From 968dfdb15cc11d48783017b2a91147b25c854ad6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Dec 2015 19:45:01 +0100 Subject: Monotonizing the Evarutil module. Some functions were left in the old paradigm because they are only used by the unification algorithms, so they are not worthwhile to change for now. --- engine/sigma.ml | 12 ++++++++++++ engine/sigma.mli | 7 +++++++ 2 files changed, 19 insertions(+) (limited to 'engine') diff --git a/engine/sigma.ml b/engine/sigma.ml index e886b0d1e7..c25aac0c14 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,6 +36,18 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) +let new_univ_level_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + +let new_univ_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + +let new_sort_variable ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in + Sigma (u, sigma, ()) + let fresh_sort_in_family ?rigid env sigma s = let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in Sigma (s, sigma, ()) diff --git a/engine/sigma.mli b/engine/sigma.mli index cb948dba59..d7ae2e4ac9 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -66,6 +66,13 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) +val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> + 'r t -> (Univ.universe_level, 'r) sigma +val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> + 'r t -> (Univ.universe, 'r) sigma +val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> + 'r t -> (Sorts.t, 'r) sigma + val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env -> 'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma val fresh_constant_instance : -- cgit v1.2.3 From 8d0ff142913fc6351ff7f0a6b8eacc6c21d36000 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Feb 2016 15:12:53 +0100 Subject: Allowing to attach location to universes in UState. --- engine/evd.ml | 42 +++++++++++++++++++++--------------------- engine/evd.mli | 20 ++++++++++---------- engine/sigma.ml | 32 ++++++++++++++++---------------- engine/sigma.mli | 24 ++++++++++++------------ engine/uState.ml | 49 +++++++++++++++++++++++++++++++++++++------------ engine/uState.mli | 4 ++-- 6 files changed, 98 insertions(+), 73 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index f751f4d922..b6849f7ffb 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -781,25 +781,25 @@ let restrict_universe_context evd vars = let universe_subst evd = UState.subst evd.universes -let merge_context_set ?(sideff=false) rigid evd ctx' = - {evd with universes = UState.merge sideff rigid evd.universes ctx'} +let merge_context_set ?loc ?(sideff=false) rigid evd ctx' = + {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'} let merge_universe_subst evd subst = {evd with universes = UState.merge_subst evd.universes subst } -let with_context_set rigid d (a, ctx) = - (merge_context_set rigid d ctx, a) +let with_context_set ?loc rigid d (a, ctx) = + (merge_context_set ?loc rigid d ctx, a) -let new_univ_level_variable ?name ?(predicative=true) rigid evd = - let uctx', u = UState.new_univ_variable rigid name evd.universes in +let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd = + let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?name ?(predicative=true) rigid evd = - let uctx', u = UState.new_univ_variable rigid name evd.universes in +let new_univ_variable ?loc ?name ?(predicative=true) rigid evd = + let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?name ?(predicative=true) rigid d = - let (d', u) = new_univ_variable rigid ?name ~predicative d in +let new_sort_variable ?loc ?name ?(predicative=true) rigid d = + let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in (d', Type u) let add_global_univ d u = @@ -815,27 +815,27 @@ let make_evar_universe_context e l = | Some us -> List.fold_left (fun uctx (loc,id) -> - fst (UState.new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) + fst (UState.new_univ_variable ~loc univ_rigid (Some (Id.to_string id)) uctx)) uctx us (****************************************) (* Operations on constants *) (****************************************) -let fresh_sort_in_family ?(rigid=univ_flexible) env evd s = - with_context_set rigid evd (Universes.fresh_sort_in_family env s) +let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = + with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s) -let fresh_constant_instance env evd c = - with_context_set univ_flexible evd (Universes.fresh_constant_instance env c) +let fresh_constant_instance ?loc env evd c = + with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c) -let fresh_inductive_instance env evd i = - with_context_set univ_flexible evd (Universes.fresh_inductive_instance env i) +let fresh_inductive_instance ?loc env evd i = + with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i) -let fresh_constructor_instance env evd c = - with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c) +let fresh_constructor_instance ?loc env evd c = + with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c) -let fresh_global ?(rigid=univ_flexible) ?names env evd gr = - with_context_set rigid evd (Universes.fresh_global_instance ?names env gr) +let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = + with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr) let whd_sort_variable evd t = t diff --git a/engine/evd.mli b/engine/evd.mli index a9ca9a7408..3ae6e586c1 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -504,9 +504,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map @@ -541,10 +541,10 @@ val universes : evar_map -> UGraph.t val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map -val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map -val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a +val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : evar_universe_context -> evar_universe_context @@ -559,12 +559,12 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts -val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant -val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts +val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> +val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** diff --git a/engine/sigma.ml b/engine/sigma.ml index c25aac0c14..c7b0bb5a50 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,36 +36,36 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) -let new_univ_level_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in +let new_univ_level_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let new_univ_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in +let new_univ_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let new_sort_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in +let new_sort_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let fresh_sort_in_family ?rigid env sigma s = - let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in +let fresh_sort_in_family ?loc ?rigid env sigma s = + let (sigma, s) = Evd.fresh_sort_in_family ?loc ?rigid env sigma s in Sigma (s, sigma, ()) -let fresh_constant_instance env sigma cst = - let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in +let fresh_constant_instance ?loc env sigma cst = + let (sigma, cst) = Evd.fresh_constant_instance ?loc env sigma cst in Sigma (cst, sigma, ()) -let fresh_inductive_instance env sigma ind = - let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in +let fresh_inductive_instance ?loc env sigma ind = + let (sigma, ind) = Evd.fresh_inductive_instance ?loc env sigma ind in Sigma (ind, sigma, ()) -let fresh_constructor_instance env sigma pc = - let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in +let fresh_constructor_instance ?loc env sigma pc = + let (sigma, c) = Evd.fresh_constructor_instance ?loc env sigma pc in Sigma (c, sigma, ()) -let fresh_global ?rigid ?names env sigma r = - let (sigma, c) = Evd.fresh_global ?rigid ?names env sigma r in +let fresh_global ?loc ?rigid ?names env sigma r = + let (sigma, c) = Evd.fresh_global ?loc ?rigid ?names env sigma r in Sigma (c, sigma, ()) (** Run *) diff --git a/engine/sigma.mli b/engine/sigma.mli index d7ae2e4ac9..643bea4036 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -66,23 +66,23 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) -val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Univ.universe_level, 'r) sigma -val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Univ.universe, 'r) sigma -val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Sorts.t, 'r) sigma - -val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env -> +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma +val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma +val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma + +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env -> 'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma val fresh_constant_instance : - Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma + ?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma val fresh_inductive_instance : - Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma -val fresh_constructor_instance : Environ.env -> 'r t -> constructor -> + ?loc:Loc.t -> Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma +val fresh_constructor_instance : ?loc:Loc.t -> Environ.env -> 'r t -> constructor -> (pconstructor, 'r) sigma -val fresh_global : ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> +val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> 'r t -> Globnames.global_reference -> (constr, 'r) sigma (** FILLME *) diff --git a/engine/uState.ml b/engine/uState.ml index 75c03bc89c..8aa9a61ab9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -25,9 +25,14 @@ module UNameMap = struct | _, _ -> r) s t end +type uinfo = { + uname : string option; + uloc : Loc.t option; +} + (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; + { uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t; uctx_local : Univ.universe_context_set; (** The local context of variables *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) @@ -104,8 +109,13 @@ let constrain_variables diff ctx = with Not_found | Option.IsNone -> cstrs) diff Univ.Constraint.empty -let add_uctx_names s l (names, names_rev) = - (UNameMap.add s l names, Univ.LMap.add l s names_rev) +let add_uctx_names ?loc s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) + +let add_uctx_loc l loc (names, names_rev) = + match loc with + | None -> (names, names_rev) + | Some _ -> (names, Univ.LMap.add l { uname = None; uloc = loc } names_rev) let of_binders b = let ctx = empty in @@ -230,8 +240,8 @@ let add_universe_constraints ctx cstrs = let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try str(Univ.LMap.find l map_rev) - with Not_found -> + try str (Option.get (Univ.LMap.find l map_rev).uname) + with Not_found | Option.IsNone -> Universes.pr_with_global_universes l let universe_context ?names ctx = @@ -252,10 +262,14 @@ let universe_context ?names ctx = in if not (Univ.LSet.is_empty left) then let n = Univ.LSet.cardinal left in - errorlabstrm "universe_context" + let loc = + let get_loc u = try (Univ.LMap.find u (snd ctx.uctx_names)).uloc with Not_found -> None in + try List.find_map get_loc (Univ.LSet.elements left) with Not_found -> Loc.ghost + in + user_err_loc (loc, "universe_context", (str(CString.plural n "Universe") ++ spc () ++ Univ.LSet.pr (pr_uctx_level ctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") + spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")) else let inst = Univ.Instance.of_array (Array.of_list newinst) in let ctx = Univ.UContext.make (inst, @@ -274,7 +288,7 @@ let univ_rigid = UnivRigid let univ_flexible = UnivFlexible false let univ_flexible_alg = UnivFlexible true -let merge sideff rigid uctx ctx' = +let merge ?loc sideff rigid uctx ctx' = let open Univ in let levels = ContextSet.levels ctx' in let uctx = if sideff then uctx else @@ -301,10 +315,21 @@ let merge sideff rigid uctx ctx' = with UGraph.AlreadyDeclared when sideff -> g) levels g in + let uctx_names = + let fold u accu = + let modify _ info = match info.uloc with + | None -> { info with uloc = loc } + | Some _ -> info + in + try LMap.modify u modify accu + with Not_found -> LMap.add u { uname = None; uloc = loc } accu + in + (fst uctx.uctx_names, LSet.fold fold levels (snd uctx.uctx_names)) + in let initial = declare uctx.uctx_initial_universes in let univs = declare uctx.uctx_universes in let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in - { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } + { uctx with uctx_names; uctx_local; uctx_universes; uctx_initial_universes = initial } let merge_subst uctx s = { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } @@ -313,7 +338,7 @@ let emit_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in List.fold_left (merge true univ_rigid) u uctxs -let new_univ_variable rigid name +let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in let ctx' = Univ.ContextSet.add_universe u ctx in @@ -328,8 +353,8 @@ let new_univ_variable rigid name in let names = match name with - | Some n -> add_uctx_names n u uctx.uctx_names - | None -> uctx.uctx_names + | Some n -> add_uctx_names ?loc n u uctx.uctx_names + | None -> add_uctx_loc u loc uctx.uctx_names in let initial = UGraph.add_universe u false uctx.uctx_initial_universes diff --git a/engine/uState.mli b/engine/uState.mli index 9dc96622ea..c5c454020c 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -84,11 +84,11 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -val merge : bool -> rigid -> t -> Univ.universe_context_set -> t +val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t val merge_subst : t -> Universes.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t -val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t +val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t val add_global_univ : t -> Univ.Level.t -> t val make_flexible_variable : t -> bool -> Univ.Level.t -> t -- cgit v1.2.3 From b2a2cb77f38549a25417d199e90d745715f3e465 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 18:08:42 +0100 Subject: Making Proofview independent of Logic. --- engine/proofview_monad.ml | 4 ++-- engine/proofview_monad.mli | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'engine') diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 2b9db60b4f..6f52b3ee90 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -154,8 +154,8 @@ end focused goals. *) type proofview = { solution : Evd.evar_map; - comb : Goal.goal list; - shelf : Goal.goal list; + comb : Evar.t list; + shelf : Evar.t list; } (** {6 Instantiation of the logic monad} *) diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 7a6ea10fe3..0aff0a7207 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -70,8 +70,8 @@ end focused goals. *) type proofview = { solution : Evd.evar_map; - comb : Goal.goal list; - shelf : Goal.goal list; + comb : Evar.t list; + shelf : Evar.t list; } (** {6 Instantiation of the logic monad} *) -- cgit v1.2.3 From 528bc26b7a6ee63bb35fc8ada56b021da65f9834 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 21:06:04 +0100 Subject: Moving Evarutil and Proofview to engine/ --- engine/engine.mllib | 2 + engine/evarutil.ml | 723 ++++++++++++++++++++++++++++++ engine/evarutil.mli | 221 +++++++++ engine/proofview.ml | 1211 ++++++++++++++++++++++++++++++++++++++++++++++++++ engine/proofview.mli | 589 ++++++++++++++++++++++++ 5 files changed, 2746 insertions(+) create mode 100644 engine/evarutil.ml create mode 100644 engine/evarutil.mli create mode 100644 engine/proofview.ml create mode 100644 engine/proofview.mli (limited to 'engine') diff --git a/engine/engine.mllib b/engine/engine.mllib index 7197a25838..70b74edca3 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -5,3 +5,5 @@ UState Evd Sigma Proofview_monad +Evarutil +Proofview diff --git a/engine/evarutil.ml b/engine/evarutil.ml new file mode 100644 index 0000000000..2bd67dcdc8 --- /dev/null +++ b/engine/evarutil.ml @@ -0,0 +1,723 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* None + +(** Combinators *) + +let evd_comb0 f evdref = + let (evd',x) = f !evdref in + evdref := evd'; + x + +let evd_comb1 f evdref x = + let (evd',y) = f !evdref x in + evdref := evd'; + y + +let evd_comb2 f evdref x y = + let (evd',z) = f !evdref x y in + evdref := evd'; + z + +let e_new_global evdref x = + evd_comb1 (Evd.fresh_global (Global.env())) evdref x + +let new_global evd x = + Sigma.fresh_global (Global.env()) evd x + +(****************************************************) +(* Expanding/testing/exposing existential variables *) +(****************************************************) + +(* flush_and_check_evars fails if an existential is undefined *) + +exception Uninstantiated_evar of existential_key + +let rec flush_and_check_evars sigma c = + match kind_of_term c with + | Evar (evk,_ as ev) -> + (match existential_opt_value sigma ev with + | None -> raise (Uninstantiated_evar evk) + | Some c -> flush_and_check_evars sigma c) + | _ -> map_constr (flush_and_check_evars sigma) c + +(* let nf_evar_key = Profile.declare_profile "nf_evar" *) +(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *) + +let rec whd_evar sigma c = + match kind_of_term c with + | Evar ev -> + let (evk, args) = ev in + let args = Array.map (fun c -> whd_evar sigma c) args in + (match safe_evar_value sigma (evk, args) with + Some c -> whd_evar sigma c + | None -> c) + | Sort (Type u) -> + let u' = Evd.normalize_universe sigma u in + if u' == u then c else mkSort (Sorts.sort_of_univ u') + | Const (c', u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkConstU (c', u') + | Ind (i, u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkIndU (i, u') + | Construct (co, u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkConstructU (co, u') + | _ -> c + +let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t) + +let j_nf_evar sigma j = + { uj_val = nf_evar sigma j.uj_val; + uj_type = nf_evar sigma j.uj_type } +let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl +let jv_nf_evar sigma = Array.map (j_nf_evar sigma) +let tj_nf_evar sigma {utj_val=v;utj_type=t} = + {utj_val=nf_evar sigma v;utj_type=t} + +let nf_evars_universes evm = + Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) + (Evd.universe_subst evm) + +let nf_evars_and_universes evm = + let evm = Evd.nf_constraints evm in + evm, nf_evars_universes evm + +let e_nf_evars_and_universes evdref = + evdref := Evd.nf_constraints !evdref; + nf_evars_universes !evdref, Evd.universe_subst !evdref + +let nf_evar_map_universes evm = + let evm = Evd.nf_constraints evm in + let subst = Evd.universe_subst evm in + if Univ.LMap.is_empty subst then evm, nf_evar evm + else + let f = nf_evars_universes evm in + Evd.raw_map (fun _ -> map_evar_info f) evm, f + +let nf_named_context_evar sigma ctx = + Context.Named.map (nf_evar sigma) ctx + +let nf_rel_context_evar sigma ctx = + Context.Rel.map (nf_evar sigma) ctx + +let nf_env_evar sigma env = + let nc' = nf_named_context_evar sigma (Environ.named_context env) in + let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in + push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) + +let nf_evar_info evc info = map_evar_info (nf_evar evc) info + +let nf_evar_map evm = + Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm + +let nf_evar_map_undefined evm = + Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm + +(*-------------------*) +(* Auxiliary functions for the conversion algorithms modulo evars + *) + +(* A probably faster though more approximative variant of + [has_undefined (nf_evar c)]: instances are not substituted and + maybe an evar occurs in an instance and it would disappear by + instantiation *) + +let has_undefined_evars evd t = + let rec has_ev t = + match kind_of_term t with + | Evar (ev,args) -> + (match evar_body (Evd.find evd ev) with + | Evar_defined c -> + has_ev c; Array.iter has_ev args + | Evar_empty -> + raise NotInstantiatedEvar) + | _ -> iter_constr has_ev t in + try let _ = has_ev t in false + with (Not_found | NotInstantiatedEvar) -> true + +let is_ground_term evd t = + not (has_undefined_evars evd t) + +let is_ground_env evd env = + let open Context.Rel.Declaration in + let is_ground_rel_decl = function + | LocalDef (_,b,_) -> is_ground_term evd b + | _ -> true in + let open Context.Named.Declaration in + let is_ground_named_decl = function + | LocalDef (_,b,_) -> is_ground_term evd b + | _ -> true in + List.for_all is_ground_rel_decl (rel_context env) && + List.for_all is_ground_named_decl (named_context env) + +(* Memoization is safe since evar_map and environ are applicative + structures *) +let memo f = + let m = ref None in + fun x y -> match !m with + | Some (x', y', r) when x == x' && y == y' -> r + | _ -> let r = f x y in m := Some (x, y, r); r + +let is_ground_env = memo is_ground_env + +(* Return the head evar if any *) + +exception NoHeadEvar + +let head_evar = + let rec hrec c = match kind_of_term c with + | Evar (evk,_) -> evk + | Case (_,_,c,_) -> hrec c + | App (c,_) -> hrec c + | Cast (c,_,_) -> hrec c + | _ -> raise NoHeadEvar + in + hrec + +(* Expand head evar if any (currently consider only applications but I + guess it should consider Case too) *) + +let whd_head_evar_stack sigma c = + let rec whrec (c, l as s) = + match kind_of_term c with + | Evar (evk,args as ev) -> + let v = + try Some (existential_value sigma ev) + with NotInstantiatedEvar | Not_found -> None in + begin match v with + | None -> s + | Some c -> whrec (c, l) + end + | Cast (c,_,_) -> whrec (c, l) + | App (f,args) -> whrec (f, args :: l) + | _ -> s + in + whrec (c, []) + +let whd_head_evar sigma c = + let (f, args) = whd_head_evar_stack sigma c in + (** optim: don't reallocate if empty/singleton *) + match args with + | [] -> f + | [arg] -> mkApp (f, arg) + | _ -> mkApp (f, Array.concat args) + +(**********************) +(* Creating new metas *) +(**********************) + +let meta_counter_summary_name = "meta counter" + +(* Generator of metavariables *) +let new_meta = + let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in + fun () -> incr meta_ctr; !meta_ctr + +let mk_new_meta () = mkMeta(new_meta()) + +(* The list of non-instantiated existential declarations (order is important) *) + +let non_instantiated sigma = + let listev = Evd.undefined_map sigma in + Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev + +(************************) +(* Manipulating filters *) +(************************) + +let make_pure_subst evi args = + let open Context.Named.Declaration in + snd (List.fold_right + (fun decl (args,l) -> + match args with + | a::rest -> (rest, (get_id decl, a)::l) + | _ -> anomaly (Pp.str "Instance does not match its signature")) + (evar_filtered_context evi) (Array.rev_to_list args,[])) + +(*------------------------------------* + * functional operations on evar sets * + *------------------------------------*) + +(* [push_rel_context_to_named_context] builds the defining context and the + * initial instance of an evar. If the evar is to be used in context + * + * Gamma = a1 ... an xp ... x1 + * \- named part -/ \- de Bruijn part -/ + * + * then the x1...xp are turned into variables so that the evar is declared in + * context + * + * a1 ... an xp ... x1 + * \----------- named part ------------/ + * + * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)" + * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed + * in context Gamma. + * + * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first) + * Remark 2: If some of the ai or xj are definitions, we keep them in the + * instance. This is necessary so that no unfolding of local definitions + * happens when inferring implicit arguments (consider e.g. the problem + * "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which + * produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want + * the hole to be instantiated by x', not by x (which would have been + * the case in [invert_definition] if x' had disappeared from the instance). + * Note that at any time, if, in some context env, the instance of + * declaration x:A is t and the instance of definition x':=phi(x) is u, then + * we have the property that u and phi(t) are convertible in env. + *) + +let subst2 subst vsubst c = + substl subst (replace_vars vsubst c) + +let push_rel_context_to_named_context env typ = + (* compute the instances relative to the named context and rel_context *) + let open Context.Named.Declaration in + let ids = List.map get_id (named_context env) in + let inst_vars = List.map mkVar ids in + let inst_rels = List.rev (rel_list 0 (nb_rel env)) in + let replace_var_named_declaration id0 id decl = + let id' = get_id decl in + let id' = if Id.equal id0 id' then id else id' in + let vsubst = [id0 , mkVar id] in + decl |> set_id id' |> map_constr (replace_vars vsubst) + in + let replace_var_named_context id0 id env = + let nc = Environ.named_context env in + let nc' = List.map (replace_var_named_declaration id0 id) nc in + Environ.reset_with_named_context (val_of_named_context nc') env + in + let extract_if_neq id = function + | Anonymous -> None + | Name id' when id_ord id id' = 0 -> None + | Name id' -> Some id' + in + (* move the rel context to a named context and extend the named instance *) + (* with vars of the rel context *) + (* We do keep the instances corresponding to local definition (see above) *) + let (subst, vsubst, _, env) = + Context.Rel.fold_outside + (fun decl (subst, vsubst, avoid, env) -> + let open Context.Rel.Declaration in + let na = get_name decl in + let c = get_value decl in + let t = get_type decl in + let open Context.Named.Declaration in + let id = + (* ppedrot: we want to infer nicer names for the refine tactic, but + keeping at the same time backward compatibility in other code + using this function. For now, we only attempt to preserve the + old behaviour of Program, but ultimately, one should do something + about this whole name generation problem. *) + if Flags.is_program_mode () then next_name_away na avoid + else next_ident_away (id_of_name_using_hdchar env t na) avoid + in + match extract_if_neq id na with + | Some id0 when not (is_section_variable id0) -> + (* spiwack: if [id<>id0], rather than introducing a new + binding named [id], we will keep [id0] (the name given + by the user) and rename [id0] into [id] in the named + context. Unless [id] is a section variable. *) + let subst = List.map (replace_vars [id0,mkVar id]) subst in + let vsubst = (id0,mkVar id)::vsubst in + let d = match c with + | None -> LocalAssum (id0, subst2 subst vsubst t) + | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) + in + let env = replace_var_named_context id0 id env in + (mkVar id0 :: subst, vsubst, id::avoid, push_named d env) + | _ -> + (* spiwack: if [id0] is a section variable renaming it is + incorrect. We revert to a less robust behaviour where + the new binder has name [id]. Which amounts to the same + behaviour than when [id=id0]. *) + let d = match c with + | None -> LocalAssum (id, subst2 subst vsubst t) + | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) + in + (mkVar id :: subst, vsubst, id::avoid, push_named d env) + ) + (rel_context env) ~init:([], [], ids, env) in + (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) + +(*------------------------------------* + * Entry points to define new evars * + *------------------------------------*) + +let default_source = (Loc.ghost,Evar_kinds.InternalHole) + +let restrict_evar evd evk filter candidates = + let evd = Sigma.to_evar_map evd in + let evd, evk' = Evd.restrict evk filter ?candidates evd in + Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) + +let new_pure_evar_full evd evi = + let evd = Sigma.to_evar_map evd in + let (evd, evk) = Evd.new_evar evd evi in + let evd = Evd.declare_future_goal evk evd in + Sigma.Unsafe.of_pair (evk, evd) + +let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = + let evd = Sigma.to_evar_map evd in + let default_naming = Misctypes.IntroAnonymous in + let naming = Option.default default_naming naming in + let evi = { + evar_hyps = sign; + evar_concl = typ; + evar_body = Evar_empty; + evar_filter = filter; + evar_source = src; + evar_candidates = candidates; + evar_extra = store; } + in + let (evd, newevk) = Evd.new_evar evd ~naming evi in + let evd = + if principal then Evd.declare_principal_goal newevk evd + else Evd.declare_future_goal newevk evd + in + Sigma.Unsafe.of_pair (newevk, evd) + +let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = + assert (not !Flags.debug || + List.distinct (ids_of_named_context (named_context_of_val sign))); + let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in + Sigma (mkEvar (newevk,Array.of_list instance), evd, p) + +(* [new_evar] declares a new existential in an env env with type typ *) +(* Converting the env into the sign of the evar to define *) +let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = + let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in + let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in + let instance = + match filter with + | None -> instance + | Some filter -> Filter.filter_list filter instance in + new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance + +let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in + (Sigma.to_evar_map evd, evk) + +let new_type_evar env evd ?src ?filter ?naming ?principal rigid = + let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in + let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in + Sigma ((e, s), evd', p +> q) + +let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = + let sigma = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in + let sigma = Sigma.to_evar_map sigma in + evdref := sigma; + c + +let new_Type ?(rigid=Evd.univ_flexible) env evd = + let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in + Sigma (mkSort s, sigma, p) + +let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = + let evd', s = new_sort_variable rigid !evdref in + evdref := evd'; mkSort s + + (* The same using side-effect *) +let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = + let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in + evdref := evd'; + ev + +(* This assumes an evar with identity instance and generalizes it over only + the De Bruijn part of the context *) +let generalize_evar_over_rels sigma (ev,args) = + let evi = Evd.find sigma ev in + let sign = named_context_of_val evi.evar_hyps in + List.fold_left2 + (fun (c,inst as x) a d -> + if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x) + (evi.evar_concl,[]) (Array.to_list args) sign + +(************************************) +(* Removing a dependency in an evar *) +(************************************) + +type clear_dependency_error = +| OccurHypInSimpleClause of Id.t option +| EvarTypingBreak of existential + +exception ClearDependencyError of Id.t * clear_dependency_error + +let cleared = Store.field () + +exception Depends of Id.t + +let rec check_and_clear_in_constr env evdref err ids c = + (* returns a new constr where all the evars have been 'cleaned' + (ie the hypotheses ids have been removed from the contexts of + evars) *) + let check id' = + if Id.Set.mem id' ids then + raise (ClearDependencyError (id',err)) + in + match kind_of_term c with + | Var id' -> + check id'; c + + | ( Const _ | Ind _ | Construct _ ) -> + let vars = Environ.vars_of_global env c in + Id.Set.iter check vars; c + + | Evar (evk,l as ev) -> + if Evd.is_defined !evdref evk then + (* If evk is already defined we replace it by its definition *) + let nc = whd_evar !evdref c in + (check_and_clear_in_constr env evdref err ids nc) + else + (* We check for dependencies to elements of ids in the + evar_info corresponding to e and in the instance of + arguments. Concurrently, we build a new evar + corresponding to e where hypotheses of ids have been + removed *) + let evi = Evd.find_undefined !evdref evk in + let ctxt = Evd.evar_filtered_context evi in + let (rids,filter) = + List.fold_right2 + (fun h a (ri,filter) -> + try + (* Check if some id to clear occurs in the instance + a of rid in ev and remember the dependency *) + let check id = if Id.Set.mem id ids then raise (Depends id) in + let () = Id.Set.iter check (collect_vars a) in + (* Check if some rid to clear in the context of ev + has dependencies in another hyp of the context of ev + and transitively remember the dependency *) + let check id _ = + if occur_var_in_decl (Global.env ()) id h + then raise (Depends id) + in + let () = Id.Map.iter check ri in + (* No dependency at all, we can keep this ev's context hyp *) + (ri, true::filter) + with Depends id -> let open Context.Named.Declaration in + (Id.Map.add (get_id h) id ri, false::filter)) + ctxt (Array.to_list l) (Id.Map.empty,[]) in + (* Check if some rid to clear in the context of ev has dependencies + in the type of ev and adjust the source of the dependency *) + let _nconcl = + try + let nids = Id.Map.domain rids in + check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi) + with ClearDependencyError (rid,err) -> + raise (ClearDependencyError (Id.Map.find rid rids,err)) in + + if Id.Map.is_empty rids then c + else + let origfilter = Evd.evar_filter evi in + let filter = Evd.Filter.apply_subfilter origfilter filter in + let evd = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (_, evd, _) = restrict_evar evd evk filter None in + let evd = Sigma.to_evar_map evd in + evdref := evd; + (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) + let evi = Evd.find !evdref evk in + let extra = evi.evar_extra in + let extra' = Store.set extra cleared true in + let evi' = { evi with evar_extra = extra' } in + evdref := Evd.add !evdref evk evi' ; + (* spiwack: /hacking session *) + whd_evar !evdref c + + | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c + +let clear_hyps_in_evi_main env evdref hyps terms ids = + (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some + hypothesis does not depend on a element of ids, and erases ids in + the contexts of the evars occurring in evi *) + let terms = + List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in + let nhyps = + let open Context.Named.Declaration in + let check_context decl = + let err = OccurHypInSimpleClause (Some (get_id decl)) in + map_constr (check_and_clear_in_constr env evdref err ids) decl + in + let check_value vk = match force_lazy_val vk with + | None -> vk + | Some (_, d) -> + if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then + (* v does depend on any of ids, it's ok *) + vk + else + (* v depends on one of the cleared hyps: + we forget the computed value *) + dummy_lazy_val () + in + remove_hyps ids check_context check_value hyps + in + (nhyps,terms) + +let clear_hyps_in_evi env evdref hyps concl ids = + match clear_hyps_in_evi_main env evdref hyps [concl] ids with + | (nhyps,[nconcl]) -> (nhyps,nconcl) + | _ -> assert false + +let clear_hyps2_in_evi env evdref hyps t concl ids = + match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with + | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl) + | _ -> assert false + +(* spiwack: a few functions to gather evars on which goals depend. *) +let queue_set q is_dependent set = + Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set +let queue_term q is_dependent c = + queue_set q is_dependent (evars_of_term c) + +let process_dependent_evar q acc evm is_dependent e = + let evi = Evd.find evm e in + (* Queues evars appearing in the types of the goal (conclusion, then + hypotheses), they are all dependent. *) + queue_term q true evi.evar_concl; + List.iter begin fun decl -> + let open Context.Named.Declaration in + queue_term q true (get_type decl); + match decl with + | LocalAssum _ -> () + | LocalDef (_,b,_) -> queue_term q true b + end (Environ.named_context_of_val evi.evar_hyps); + match evi.evar_body with + | Evar_empty -> + if is_dependent then Evar.Map.add e None acc else acc + | Evar_defined b -> + let subevars = evars_of_term b in + (* evars appearing in the definition of an evar [e] are marked + as dependent when [e] is dependent itself: if [e] is a + non-dependent goal, then, unless they are reach from another + path, these evars are just other non-dependent goals. *) + queue_set q is_dependent subevars; + if is_dependent then Evar.Map.add e (Some subevars) acc else acc + +let gather_dependent_evars q evm = + let acc = ref Evar.Map.empty in + while not (Queue.is_empty q) do + let (is_dependent,e) = Queue.pop q in + (* checks if [e] has already been added to [!acc] *) + begin if not (Evar.Map.mem e !acc) then + acc := process_dependent_evar q !acc evm is_dependent e + end + done; + !acc + +let gather_dependent_evars evm l = + let q = Queue.create () in + List.iter (fun a -> Queue.add (false,a) q) l; + gather_dependent_evars q evm + +(* /spiwack *) + +(** The following functions return the set of undefined evars + contained in the object, the defined evars being traversed. + This is roughly a combination of the previous functions and + [nf_evar]. *) + +let undefined_evars_of_term evd t = + let rec evrec acc c = + match kind_of_term c with + | Evar (n, l) -> + let acc = Array.fold_left evrec acc l in + (try match (Evd.find evd n).evar_body with + | Evar_empty -> Evar.Set.add n acc + | Evar_defined c -> evrec acc c + with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found")) + | _ -> fold_constr evrec acc c + in + evrec Evar.Set.empty t + +let undefined_evars_of_named_context evd nc = + let open Context.Named.Declaration in + Context.Named.fold_outside + (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) + nc + ~init:Evar.Set.empty + +let undefined_evars_of_evar_info evd evi = + Evar.Set.union (undefined_evars_of_term evd evi.evar_concl) + (Evar.Set.union + (match evi.evar_body with + | Evar_empty -> Evar.Set.empty + | Evar_defined b -> undefined_evars_of_term evd b) + (undefined_evars_of_named_context evd + (named_context_of_val evi.evar_hyps))) + +(* spiwack: this is a more complete version of + {!Termops.occur_evar}. The latter does not look recursively into an + [evar_map]. If unification only need to check superficially, tactics + do not have this luxury, and need the more complete version. *) +let occur_evar_upto sigma n c = + let rec occur_rec c = match kind_of_term c with + | Evar (sp,_) when Evar.equal sp n -> raise Occur + | Evar e -> Option.iter occur_rec (existential_opt_value sigma e) + | _ -> iter_constr occur_rec c + in + try occur_rec c; false with Occur -> true + +(* We don't try to guess in which sort the type should be defined, since + any type has type Type. May cause some trouble, but not so far... *) + +let judge_of_new_Type evd = + let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in + Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p) + +let subterm_source evk (loc,k) = + let evk = match k with + | Evar_kinds.SubEvar (evk) -> evk + | _ -> evk in + (loc,Evar_kinds.SubEvar evk) + + +(** Term exploration up to instantiation. *) +let kind_of_term_upto sigma t = + Constr.kind (whd_evar sigma t) + +(** [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 extention of those in [sigma1]. *) +let eq_constr_univs_test sigma1 sigma2 t u = + (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) + let open Evd in + let fold cstr sigma = + try Some (add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | UniversesDiffer -> None + in + let ans = + Universes.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 + in + match ans with None -> false | Some _ -> true + +type type_constraint = types option +type val_constraint = constr option diff --git a/engine/evarutil.mli b/engine/evarutil.mli new file mode 100644 index 0000000000..ffff2c5dd9 --- /dev/null +++ b/engine/evarutil.mli @@ -0,0 +1,221 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* metavariable +val mk_new_meta : unit -> constr + +(** {6 Creating a fresh evar given their type and context} *) +val new_evar : + env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> (constr, 'r) Sigma.sigma + +val new_pure_evar : + named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> (evar, 'r) Sigma.sigma + +val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma + +(** the same with side-effects *) +val e_new_evar : + env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> constr + +(** Create a new Type existential variable, as we keep track of + them during type-checking and unification. *) +val new_type_evar : + env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> + (constr * sorts, 'r) Sigma.sigma + +val e_new_type_evar : env -> evar_map ref -> + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts + +val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma +val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr + +val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> + constr list option -> (existential_key, 'r) Sigma.sigma + +(** Polymorphic constants *) + +val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma +val e_new_global : evar_map ref -> Globnames.global_reference -> constr + +(** Create a fresh evar in a context different from its definition context: + [new_evar_instance sign evd ty inst] creates a new evar of context + [sign] and type [ty], [inst] is a mapping of the evar context to + the context where the evar should occur. This means that the terms + of [inst] are typed in the occurrence context and their type (seen + as a telescope) is [sign] *) +val new_evar_instance : + named_context_val -> 'r Sigma.t -> types -> + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> + ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> + constr list -> (constr, 'r) Sigma.sigma + +val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list + +val safe_evar_value : evar_map -> existential -> constr option + +(** {6 Evars/Metas switching...} *) + +val non_instantiated : evar_map -> evar_info Evar.Map.t + +(** {6 Unification utils} *) + +(** [head_evar c] returns the head evar of [c] if any *) +exception NoHeadEvar +val head_evar : constr -> existential_key (** may raise NoHeadEvar *) + +(* Expand head evar if any *) +val whd_head_evar : evar_map -> constr -> constr + +(* An over-approximation of [has_undefined (nf_evars evd c)] *) +val has_undefined_evars : evar_map -> constr -> bool + +val is_ground_term : evar_map -> constr -> bool +val is_ground_env : evar_map -> env -> bool + +(** [gather_dependent_evars evm seeds] classifies the evars in [evm] + as dependent_evars and goals (these may overlap). A goal is an + evar in [seeds] or an evar appearing in the (partial) definition + of a goal. A dependent evar is an evar appearing in the type + (hypotheses and conclusion) of a goal, or in the type or (partial) + definition of a dependent evar. The value return is a map + associating to each dependent evar [None] if it has no (partial) + definition or [Some s] if [s] is the list of evars appearing in + its (partial) definition. *) +val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t + +(** The following functions return the set of undefined evars + contained in the object, the defined evars being traversed. + This is roughly a combination of the previous functions and + [nf_evar]. *) + +val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t +val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t +val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t + +(** [occur_evar_upto sigma k c] returns [true] if [k] appears in + [c]. It looks up recursively in [sigma] for the value of existential + variables. *) +val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool + +(** {6 Value/Type constraints} *) + +val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma + +(***********************************************************) + +(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains + uninstantiated; [nf_evar] leaves uninstantiated evars as is *) + +val whd_evar : evar_map -> constr -> constr +val nf_evar : evar_map -> constr -> constr +val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment +val jl_nf_evar : + evar_map -> unsafe_judgment list -> unsafe_judgment list +val jv_nf_evar : + evar_map -> unsafe_judgment array -> unsafe_judgment array +val tj_nf_evar : + evar_map -> unsafe_type_judgment -> unsafe_type_judgment + +val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t +val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t +val nf_env_evar : evar_map -> env -> env + +val nf_evar_info : evar_map -> evar_info -> evar_info +val nf_evar_map : evar_map -> evar_map +val nf_evar_map_undefined : evar_map -> evar_map + +(** Presenting terms without solved evars *) + +val nf_evars_universes : evar_map -> constr -> constr + +val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr) +val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst + +(** Normalize the evar map w.r.t. universes, after simplification of constraints. + Return the substitution function for constrs as well. *) +val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr) + +(** Replacing all evars, possibly raising [Uninstantiated_evar] *) +exception Uninstantiated_evar of existential_key +val flush_and_check_evars : evar_map -> constr -> constr + +(** {6 Term manipulation up to instantiation} *) + +(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] + as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the + value of [e] in [sigma] is (recursively) used. *) +val kind_of_term_upto : evar_map -> constr -> (constr,types) 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 extention of those in [sigma1]. *) +val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool + +(** {6 Removing hyps in evars'context} +raise OccurHypInSimpleClause if the removal breaks dependencies *) + +type clear_dependency_error = +| OccurHypInSimpleClause of Id.t option +| EvarTypingBreak of existential + +exception ClearDependencyError of Id.t * clear_dependency_error + +(* spiwack: marks an evar that has been "defined" by clear. + used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) +val cleared : bool Store.field + +val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> + Id.Set.t -> named_context_val * types + +val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> + Id.Set.t -> named_context_val * types * types + +val push_rel_context_to_named_context : Environ.env -> types -> + named_context_val * types * constr list * constr list * (identifier*constr) list + +val generalize_evar_over_rels : evar_map -> existential -> types * constr list + +(** Evar combinators *) + +val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a +val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a +val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a + +val subterm_source : existential_key -> Evar_kinds.t Loc.located -> + Evar_kinds.t Loc.located + +val meta_counter_summary_name : string + +(** Deprecater *) + +type type_constraint = types option +type val_constraint = constr option diff --git a/engine/proofview.ml b/engine/proofview.ml new file mode 100644 index 0000000000..ba664cafaf --- /dev/null +++ b/engine/proofview.ml @@ -0,0 +1,1211 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* i+1) solution 0 in + let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in + let pruned_solution = Evd.drop_all_defined solution in + let apply_subst_einfo _ ei = + Evd.({ ei with + evar_concl = nf ei.evar_concl; + evar_hyps = Environ.map_named_val nf ei.evar_hyps; + evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in + let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in + let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in + msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); + new_el, { pv with solution = new_solution; } + + +(** {6 Starting and querying a proof view} *) + +type telescope = + | TNil of Evd.evar_map + | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) + +let typeclass_resolvable = Evd.Store.field () + +let dependent_init = + (* Goals are created with a store which marks them as unresolvable + for type classes. *) + let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in + (* Goals don't have a source location. *) + let src = (Loc.ghost,Evar_kinds.GoalEvar) in + (* Main routine *) + let rec aux = function + | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } + | TCons (env, sigma, typ, t) -> + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in + let sigma = Sigma.to_evar_map sigma in + let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in + let (gl, _) = Term.destEvar econstr in + let entry = (econstr, typ) :: ret in + entry, { solution = sol; comb = gl :: comb; shelf = [] } + in + fun t -> + let entry, v = aux t in + (* The created goal are not to be shelved. *) + let solution = Evd.reset_future_goals v.solution in + entry, { v with solution } + +let init = + let rec aux sigma = function + | [] -> TNil sigma + | (env,g)::l -> TCons (env,sigma,g,(fun sigma _ -> aux sigma l)) + in + fun sigma l -> dependent_init (aux sigma l) + +let initial_goals initial = initial + +let finished = function + | {comb = []} -> true + | _ -> false + +let return { solution=defs } = defs + +let return_constr { solution = defs } c = Evarutil.nf_evar defs c + +let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry) + + +(** {6 Focusing commands} *) + +(** A [focus_context] represents the part of the proof view which has + been removed by a focusing action, it can be used to unfocus later + on. *) +(* First component is a reverse list of the goals which come before + and second component is the list of the goals which go after (in + the expected order). *) +type focus_context = Evar.t list * Evar.t list + + +(** Returns a stylised view of a focus_context for use by, for + instance, ide-s. *) +(* spiwack: the type of [focus_context] will change as we push more + refined functions to ide-s. This would be better than spawning a + new nearly identical function everytime. Hence the generic name. *) +(* In this version: the goals in the context, as a "zipper" (the first + list is in reversed order). *) +let focus_context f = f + +(** This (internal) function extracts a sublist between two indices, + and returns this sublist together with its context: if it returns + [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the + original list. The focused list has lenght [j-i-1] and contains + the goals from number [i] to number [j] (both included) the first + goal of the list being numbered [1]. [focus_sublist i j l] raises + [IndexOutOfRange] if [i > length l], or [j > length l] or [j < + i]. *) +let focus_sublist i j l = + let (left,sub_right) = CList.goto (i-1) l in + let (sub, right) = + try CList.chop (j-i+1) sub_right + with Failure _ -> raise CList.IndexOutOfRange + in + (sub, (left,right)) + +(** Inverse operation to the previous one. *) +let unfocus_sublist (left,right) s = + CList.rev_append left (s@right) + + +(** [focus i j] focuses a proofview on the goals from index [i] to + index [j] (inclusive, goals are indexed from [1]). I.e. goals + number [i] to [j] become the only focused goals of the returned + proofview. It returns the focused proofview, and a context for + the focus stack. *) +let focus i j sp = + let (new_comb, context) = focus_sublist i j sp.comb in + ( { sp with comb = new_comb } , context ) + + +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +(* spiwack: [advance] is probably performance critical, and the good + behaviour of its definition may depend sensitively to the actual + definition of [Evd.find]. Currently, [Evd.find] starts looking for + a value in the heap of undefined variable, which is small. Hence in + the most common case, where [advance] is applied to an unsolved + goal ([advance] is used to figure if a side effect has modified the + goal) it terminates quickly. *) +let rec advance sigma g = + let open Evd in + let evi = Evd.find sigma g in + match evi.evar_body with + | Evar_empty -> Some g + | Evar_defined v -> + if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then + let (e,_) = Term.destEvar v in + advance sigma e + else + None + +(** [undefined defs l] is the list of goals in [l] which are still + unsolved (after advancing cleared goals). *) +let undefined defs l = CList.map_filter (advance defs) l + +(** Unfocuses a proofview with respect to a context. *) +let unfocus c sp = + { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } + + +(** {6 The tactic monad} *) + +(** - Tactics are objects which apply a transformation to all the + subgoals of the current view at the same time. By opposition to + the old vision of applying it to a single goal. It allows tactics + such as [shelve_unifiable], tactics to reorder the focused goals, + or global automation tactic for dependent subgoals (instantiating + an evar has influences on the other goals of the proof in + progress, not being able to take that into account causes the + current eauto tactic to fail on some instances where it could + succeed). Another benefit is that it is possible to write tactics + that can be executed even if there are no focused goals. + - Tactics form a monad ['a tactic], in a sense a tactic can be + seen as a function (without argument) which returns a value of + type 'a and modifies the environment (in our case: the view). + Tactics of course have arguments, but these are given at the + meta-level as OCaml functions. Most tactics in the sense we are + used to return [()], that is no really interesting values. But + some might pass information around. The tactics seen in Coq's + Ltac are (for now at least) only [unit tactic], the return values + are kept for the OCaml toolkit. The operation or the monad are + [Proofview.tclUNIT] (which is the "return" of the tactic monad) + [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN] + (which is a specialized bind on unit-returning tactics). + - Tactics have support for full-backtracking. Tactics can be seen + having multiple success: if after returning the first success a + failure is encountered, the tactic can backtrack and use a second + success if available. The state is backtracked to its previous + value, except the non-logical state defined in the {!NonLogical} + module below. +*) +(* spiwack: as far as I'm aware this doesn't really relate to + F. Kirchner and C. Muñoz. *) + +module Proof = Logical + +(** type of tactics: + + tactics can + - access the environment, + - report unsafe status, shelved goals and given up goals + - access and change the current [proofview] + - backtrack on previous changes of the proofview *) +type +'a tactic = 'a Proof.t + +(** Applies a tactic to the current proofview. *) +let apply env t sp = + let open Logic_monad in + let ans = Proof.repr (Proof.run t false (sp,env)) in + let ans = Logic_monad.NonLogical.run ans in + match ans with + | Nil (e, info) -> iraise (TacticFailure e, info) + | Cons ((r, (state, _), status, info), _) -> + let (status, gaveup) = status in + let status = (status, state.shelf, gaveup) in + let state = { state with shelf = [] } in + r, state, status, Trace.to_tree info + + + +(** {7 Monadic primitives} *) + +(** Unit of the tactic monad. *) +let tclUNIT = Proof.return + +(** Bind operation of the tactic monad. *) +let tclBIND = Proof.(>>=) + +(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation, + it's a specialized "bind". *) +let tclTHEN = Proof.(>>) + +(** [tclIGNORE t] has the same operational content as [t], but drops + the returned value. *) +let tclIGNORE = Proof.ignore + +module Monad = Proof + + + +(** {7 Failure and backtracking} *) + + +(** [tclZERO e] fails with exception [e]. It has no success. *) +let tclZERO ?info e = + let info = match info with + | None -> Exninfo.null + | Some info -> info + in + Proof.zero (e, info) + +(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever + the successes of [t1] have been depleted and it failed with [e], + then it behaves as [t2 e]. In other words, [tclOR] inserts a + backtracking point. *) +let tclOR = Proof.plus + +(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one + success or [t2 e] if [t1] fails with [e]. It is analogous to + [try/with] handler of exception in that it is not a backtracking + point. *) +let tclORELSE t1 t2 = + let open Logic_monad in + let open Proof in + split t1 >>= function + | Nil e -> t2 e + | Cons (a,t1') -> plus (return a) t1' + +(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] + succeeds at least once then it behaves as [tclBIND a s] otherwise, + if [a] fails with [e], then it behaves as [f e]. *) +let tclIFCATCH a s f = + let open Logic_monad in + let open Proof in + split a >>= function + | Nil e -> f e + | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x')) + +(** [tclONCE t] behave like [t] except it has at most one success: + [tclONCE t] stops after the first success of [t]. If [t] fails + with [e], [tclONCE t] also fails with [e]. *) +let tclONCE = Proof.once + +exception MoreThanOneSuccess +let _ = Errors.register_handler begin function + | MoreThanOneSuccess -> Errors.error "This tactic has more than one success." + | _ -> raise Errors.Unhandled +end + +(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one + success. Otherwise it fails. The tactic [t] is run until its first + success, then a failure with exception [e] is simulated. It [t] + yields another success, then [tclEXACTLY_ONCE e t] fails with + [MoreThanOneSuccess] (it is a user error). Otherwise, + [tclEXACTLY_ONCE e t] succeeds with the first success of + [t]. Notice that the choice of [e] is relevant, as the presence of + further successes may depend on [e] (see {!tclOR}). *) +let tclEXACTLY_ONCE e t = + let open Logic_monad in + let open Proof in + split t >>= function + | Nil (e, info) -> tclZERO ~info e + | Cons (x,k) -> + Proof.split (k (e, Exninfo.null)) >>= function + | Nil _ -> tclUNIT x + | _ -> tclZERO MoreThanOneSuccess + + +(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) +type 'a case = +| Fail of iexn +| Next of 'a * (iexn -> 'a tactic) +let tclCASE t = + let open Logic_monad in + let map = function + | Nil e -> Fail e + | Cons (x, t) -> Next (x, t) + in + Proof.map map (Proof.split t) + +let tclBREAK = Proof.break + + + +(** {7 Focusing tactics} *) + +exception NoSuchGoals of int + +(* This hook returns a string to be appended to the usual message. + Primarily used to add a suggestion about the right bullet to use to + focus the next goal, if applicable. *) +let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ()) +let set_nosuchgoals_hook f = nosuchgoals_hook := f + + + +(* This uses the hook above *) +let _ = Errors.register_handler begin function + | NoSuchGoals n -> + let suffix = !nosuchgoals_hook n in + Errors.errorlabstrm "" + (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix) + | _ -> raise Errors.Unhandled +end + +(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where + only the goals numbered [i] to [j] are focused (the rest of the goals + is restored at the end of the tactic). If the range [i]-[j] is not + valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *) +let tclFOCUS_gen nosuchgoal i j t = + let open Proof in + Pv.get >>= fun initial -> + try + let (focused,context) = focus i j initial in + Pv.set focused >> + t >>= fun result -> + Pv.modify (fun next -> unfocus context next) >> + return result + with CList.IndexOutOfRange -> nosuchgoal + +let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t +let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t + +(** Like {!tclFOCUS} but selects a single goal by name. *) +let tclFOCUSID id t = + let open Proof in + Pv.get >>= fun initial -> + try + let ev = Evd.evar_key id initial.solution in + try + let n = CList.index Evar.equal ev initial.comb in + (* goal is already under focus *) + let (focused,context) = focus n n initial in + Pv.set focused >> + t >>= fun result -> + Pv.modify (fun next -> unfocus context next) >> + return result + with Not_found -> + (* otherwise, save current focus and work purely on the shelve *) + Comb.set [ev] >> + t >>= fun result -> + Comb.set initial.comb >> + return result + with Not_found -> tclZERO (NoSuchGoals 1) + +(** {7 Dispatching on goals} *) + +exception SizeMismatch of int*int +let _ = Errors.register_handler begin function + | SizeMismatch (i,_) -> + let open Pp in + let errmsg = + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str(String.plural i " tactic") ++ str")." + in + Errors.errorlabstrm "" errmsg + | _ -> raise Errors.Unhandled +end + +(** A variant of [Monad.List.iter] where we iter over the focused list + of goals. The argument tactic is executed in a focus comprising + only of the current goal, a goal which has been solved by side + effect is skipped. The generated subgoals are concatenated in + order. *) +let iter_goal i = + let open Proof in + Comb.get >>= fun initial -> + Proof.List.fold_left begin fun (subgoals as cur) goal -> + Solution.get >>= fun step -> + match advance step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal >> + Proof.map (fun comb -> comb :: subgoals) Comb.get + end [] initial >>= fun subgoals -> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) + +(** A variant of [Monad.List.fold_left2] where the first list is the + list of focused goals. The argument tactic is executed in a focus + comprising only of the current goal, a goal which has been solved + by side effect is skipped. The generated subgoals are concatenated + in order. *) +let fold_left2_goal i s l = + let open Proof in + Pv.get >>= fun initial -> + let err = + return () >>= fun () -> (* Delay the computation of list lengths. *) + tclZERO (SizeMismatch (CList.length initial.comb,CList.length l)) + in + Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> + Solution.get >>= fun step -> + match advance step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal a r >>= fun r -> + Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get + end (s,[]) initial.comb l >>= fun (r,subgoals) -> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) >> + return r + +(** Dispatch tacticals are used to apply a different tactic to each + goal under focus. They come in two flavours: [tclDISPATCH] takes a + list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL] + takes a list of ['a tactic] and returns an ['a list tactic]. + + They both work by applying each of the tactic in a focus + restricted to the corresponding goal (starting with the first + goal). In the case of [tclDISPATCHL], the tactic returns a list of + the same size as the argument list (of tactics), each element + being the result of the tactic executed in the corresponding goal. + + When the length of the tactic list is not the number of goal, + raises [SizeMismatch (g,t)] where [g] is the number of available + goals, and [t] the number of tactics passed. + + [tclDISPATCHGEN join tacs] generalises both functions as the + successive results of [tacs] are stored in reverse order in a + list, and [join] is used to convert the result into the expected + form. *) +let tclDISPATCHGEN0 join tacs = + match tacs with + | [] -> + begin + let open Proof in + Comb.get >>= function + | [] -> tclUNIT (join []) + | comb -> tclZERO (SizeMismatch (CList.length comb,0)) + end + | [tac] -> + begin + let open Proof in + Pv.get >>= function + | { comb=[goal] ; solution } -> + begin match advance solution goal with + | None -> tclUNIT (join []) + | Some _ -> Proof.map (fun res -> join [res]) tac + end + | {comb} -> tclZERO (SizeMismatch(CList.length comb,1)) + end + | _ -> + let iter _ t cur = Proof.map (fun y -> y :: cur) t in + let ans = fold_left2_goal iter [] tacs in + Proof.map join ans + +let tclDISPATCHGEN join tacs = + let branch t = InfoL.tag (Info.DBranch) t in + let tacs = CList.map branch tacs in + InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs) + +let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs + +let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs + + +(** [extend_to_list startxs rx endxs l] builds a list + [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises + [SizeMismatch] if [startxs@endxs] is already longer than [l]. *) +let extend_to_list startxs rx endxs l = + (* spiwack: I use [l] essentially as a natural number *) + let rec duplicate acc = function + | [] -> acc + | _::rest -> duplicate (rx::acc) rest + in + let rec tail to_match rest = + match rest, to_match with + | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *) + | _::rest , _::to_match -> tail to_match rest + | _ , [] -> duplicate endxs rest + in + let rec copy pref rest = + match rest,pref with + | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *) + | _::rest, a::pref -> a::(copy pref rest) + | _ , [] -> tail endxs rest + in + copy startxs l + +(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r] + tactic is "repeated" enough time such that every goal has a tactic + assigned to it ([b] is the list of tactics applied to the first + goals, [e] to the last goals, and [r] is applied to every goal in + between). *) +let tclEXTEND tacs1 rtac tacs2 = + let open Proof in + Comb.get >>= fun comb -> + try + let tacs = extend_to_list tacs1 rtac tacs2 comb in + tclDISPATCH tacs + with SizeMismatch _ -> + tclZERO (SizeMismatch( + CList.length comb, + (CList.length tacs1)+(CList.length tacs2))) +(* spiwack: failure occurs only when the number of goals is too + small. Hence we can assume that [rtac] is replicated 0 times for + any error message. *) + +(** [tclEXTEND [] tac []]. *) +let tclINDEPENDENT tac = + let open Proof in + Pv.get >>= fun initial -> + match initial.comb with + | [] -> tclUNIT () + | [_] -> tac + | _ -> + let tac = InfoL.tag (Info.DBranch) tac in + InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac)) + + + +(** {7 Goal manipulation} *) + +(** Shelves all the goals under focus. *) +let shelve = + let open Proof in + Comb.get >>= fun initial -> + Comb.set [] >> + InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> + Shelf.modify (fun gls -> gls @ initial) + + +(** [contained_in_info e evi] checks whether the evar [e] appears in + the hypotheses, the conclusion or the body of the evar_info + [evi]. Note: since we want to use it on goals, the body is actually + supposed to be empty. *) +let contained_in_info sigma e evi = + Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) + +(** [depends_on sigma src tgt] checks whether the goal [src] appears + as an existential variable in the definition of the goal [tgt] in + [sigma]. *) +let depends_on sigma src tgt = + let evi = Evd.find sigma tgt in + contained_in_info sigma src evi + +(** [unifiable sigma g l] checks whether [g] appears in another + subgoal of [l]. The list [l] may contain [g], but it does not + affect the result. *) +let unifiable sigma g l = + CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) l + +(** [partition_unifiable sigma l] partitions [l] into a pair [(u,n)] + where [u] is composed of the unifiable goals, i.e. the goals on + whose definition other goals of [l] depend, and [n] are the + non-unifiable goals. *) +let partition_unifiable sigma l = + CList.partition (fun g -> unifiable sigma g l) l + +(** Shelves the unifiable goals under focus, i.e. the goals which + appear in other goals under focus (the unfocused goals are not + considered). *) +let shelve_unifiable = + let open Proof in + Pv.get >>= fun initial -> + let (u,n) = partition_unifiable initial.solution initial.comb in + Comb.set n >> + InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> + Shelf.modify (fun gls -> gls @ u) + +(** [guard_no_unifiable] returns the list of unifiable goals if some + goals are unifiable (see {!shelve_unifiable}) in the current focus. *) +let guard_no_unifiable = + let open Proof in + Pv.get >>= fun initial -> + let (u,n) = partition_unifiable initial.solution initial.comb in + match u with + | [] -> tclUNIT None + | gls -> + let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in + let l = CList.map (fun id -> Names.Name id) l in + tclUNIT (Some l) + +(** [unshelve l p] adds all the goals in [l] at the end of the focused + goals of p *) +let unshelve l p = + (* advance the goals in case of clear *) + let l = undefined p.solution l in + { p with comb = p.comb@l } + +let with_shelf tac = + let open Proof in + Pv.get >>= fun pv -> + let { shelf; solution } = pv in + Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >> + tac >>= fun ans -> + Pv.get >>= fun npv -> + let { shelf = gls; solution = sigma } = npv in + let gls' = Evd.future_goals sigma in + let fgoals = Evd.future_goals solution in + let pgoal = Evd.principal_future_goal solution in + let sigma = Evd.restore_future_goals sigma fgoals pgoal in + Pv.set { npv with shelf; solution = sigma } >> + tclUNIT (CList.rev_append gls' gls, ans) + +(** [goodmod p m] computes the representative of [p] modulo [m] in the + interval [[0,m-1]].*) +let goodmod p m = + let p' = p mod m in + (* if [n] is negative [n mod l] is negative of absolute value less + than [l], so [(n mod l)+l] is the representative of [n] in the + interval [[0,l-1]].*) + if p' < 0 then p'+m else p' + +let cycle n = + let open Proof in + InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >> + Comb.modify begin fun initial -> + let l = CList.length initial in + let n' = goodmod n l in + let (front,rear) = CList.chop n' initial in + rear@front + end + +let swap i j = + let open Proof in + InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >> + Comb.modify begin fun initial -> + let l = CList.length initial in + let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in + let i = goodmod i l and j = goodmod j l in + CList.map_i begin fun k x -> + match k with + | k when Int.equal k i -> CList.nth initial j + | k when Int.equal k j -> CList.nth initial i + | _ -> x + end 0 initial + end + +let revgoals = + let open Proof in + InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >> + Comb.modify CList.rev + +let numgoals = + let open Proof in + Comb.get >>= fun comb -> + return (CList.length comb) + + + +(** {7 Access primitives} *) + +let tclEVARMAP = Solution.get + +let tclENV = Env.get + + + +(** {7 Put-like primitives} *) + + +let emit_side_effects eff x = + { x with solution = Evd.emit_side_effects eff x.solution } + +let tclEFFECTS eff = + let open Proof in + return () >>= fun () -> (* The Global.env should be taken at exec time *) + Env.set (Global.env ()) >> + Pv.modify (fun initial -> emit_side_effects eff initial) + +let mark_as_unsafe = Status.put false + +(** Gives up on the goal under focus. Reports an unsafe status. Proofs + with given up goals cannot be closed. *) +let give_up = + let open Proof in + Comb.get >>= fun initial -> + Comb.set [] >> + mark_as_unsafe >> + InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >> + Giveup.put initial + + + +(** {7 Control primitives} *) + + +module Progress = struct + + let eq_constr = Evarutil.eq_constr_univs_test + + (** equality function on hypothesis contexts *) + let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = + let open Environ in + let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in + let eq_named_declaration d1 d2 = + match d1, d2 with + | LocalAssum (i1,t1), LocalAssum (i2,t2) -> + Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2 + | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) -> + Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2 + && eq_constr sigma1 sigma2 t1 t2 + | _ -> + false + in List.equal eq_named_declaration c1 c2 + + let eq_evar_body sigma1 sigma2 b1 b2 = + let open Evd in + match b1, b2 with + | Evar_empty, Evar_empty -> true + | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2 + | _ -> false + + let eq_evar_info sigma1 sigma2 ei1 ei2 = + let open Evd in + eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl && + eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) && + 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 + +end + +let tclPROGRESS t = + let open Proof in + Pv.get >>= fun initial -> + t >>= fun res -> + Pv.get >>= fun final -> + (* [*_test] test absence of progress. [quick_test] is approximate + whereas [exhaustive_test] is complete. *) + let quick_test = + initial.solution == final.solution && initial.comb == final.comb + in + let exhaustive_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 + tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + +exception Timeout +let _ = Errors.register_handler begin function + | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | _ -> Pervasives.raise Errors.Unhandled +end + +let tclTIMEOUT n t = + let open Proof in + (* spiwack: as one of the monad is a continuation passing monad, it + doesn't force the computation to be threaded inside the underlying + (IO) monad. Hence I force it myself by asking for the evaluation of + a dummy value first, lest [timeout] be called when everything has + already been computed. *) + let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in + Proof.get >>= fun initial -> + Proof.current >>= fun envvar -> + Proof.lift begin + Logic_monad.NonLogical.catch + begin + let open Logic_monad.NonLogical in + timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r -> + match r with + | Logic_monad.Nil e -> return (Util.Inr e) + | Logic_monad.Cons (r, _) -> return (Util.Inl r) + end + begin let open Logic_monad.NonLogical in function (e, info) -> + match e with + | Logic_monad.Timeout -> return (Util.Inr (Timeout, info)) + | Logic_monad.TacticFailure e -> + return (Util.Inr (e, info)) + | e -> Logic_monad.NonLogical.raise ~info e + end + end >>= function + | Util.Inl (res,s,m,i) -> + Proof.set s >> + Proof.put m >> + Proof.update (fun _ -> i) >> + return res + | Util.Inr (e, info) -> tclZERO ~info e + +let tclTIME s t = + let pr_time t1 t2 n msg = + let msg = + if n = 0 then + str msg + else + str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking") + in + msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++ + System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in + let rec aux n t = + let open Proof in + tclUNIT () >>= fun () -> + let tstart = System.get_time() in + Proof.split t >>= let open Logic_monad in function + | Nil (e, info) -> + begin + let tend = System.get_time() in + pr_time tstart tend n "failure"; + tclZERO ~info e + end + | Cons (x,k) -> + let tend = System.get_time() in + pr_time tstart tend n "success"; + tclOR (tclUNIT x) (fun e -> aux (n+1) (k e)) + in aux 0 t + + + +(** {7 Unsafe primitives} *) + +module Unsafe = struct + + let tclEVARS evd = + Pv.modify (fun ps -> { ps with solution = evd }) + + let tclNEWGOALS gls = + Pv.modify begin fun step -> + let gls = undefined step.solution gls in + { step with comb = step.comb @ gls } + end + + let tclGETGOALS = Comb.get + + let tclSETGOALS = Comb.set + + let tclEVARSADVANCE evd = + Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) + + let tclEVARUNIVCONTEXT ctx = + Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) + + let reset_future_goals p = + { p with solution = Evd.reset_future_goals p.solution } + + let mark_as_goal evd content = + let info = Evd.find evd content in + let info = + { info with Evd.evar_source = match info.Evd.evar_source with + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + in + let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with + | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } + | Some () -> info + in + Evd.add evd content info + + let advance = advance + + let typeclass_resolvable = typeclass_resolvable + +end + +module UnsafeRepr = Proof.Unsafe + +let (>>=) = tclBIND +let (<*>) = tclTHEN +let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) + +(** {6 Goal-dependent tactics} *) + +let goal_env evars gl = + let evi = Evd.find evars gl in + Evd.evar_filtered_env evi + +let goal_nf_evar sigma gl = + let evi = Evd.find sigma gl in + let evi = Evarutil.nf_evar_info sigma evi in + let sigma = Evd.add sigma gl evi in + (gl, sigma) + +let goal_extra evars gl = + let evi = Evd.find evars gl in + evi.Evd.evar_extra + + +let catchable_exception = function + | Logic_monad.Exception _ -> false + | e -> Errors.noncritical e + + +module Goal = struct + + type ('a, 'r) t = { + env : Environ.env; + sigma : Evd.evar_map; + concl : Term.constr ; + self : Evar.t ; (* for compatibility with old-style definitions *) + } + + type ('a, 'b) enter = + { enter : 'r. ('a, 'r) t -> 'b } + + let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) + + let env { env=env } = env + let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma + let hyps { env=env } = Environ.named_context env + let concl { concl=concl } = concl + let extra { sigma=sigma; self=self } = goal_extra sigma self + + let raw_concl { concl=concl } = concl + + + let gmake_with info env sigma goal = + { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; + sigma = sigma ; + concl = Evd.evar_concl info ; + self = goal } + + let nf_gmake env sigma goal = + let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in + let sigma = Evd.add sigma goal info in + gmake_with info env sigma goal , sigma + + let nf_enter f = + InfoL.tag (Info.Dispatch) begin + iter_goal begin fun goal -> + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try + let (gl, sigma) = nf_gmake env sigma goal in + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + end + end + + let normalize { self } = + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + let (gl,sigma) = nf_gmake env sigma self in + tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) + + let gmake env sigma goal = + let info = Evd.find sigma goal in + gmake_with info env sigma goal + + let enter f = + let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in + InfoL.tag (Info.Dispatch) begin + iter_goal begin fun goal -> + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try f (gmake env sigma goal) + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + end + end + + type ('a, 'b) s_enter = + { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } + + let s_enter f = + InfoL.tag (Info.Dispatch) begin + iter_goal begin fun goal -> + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try + let gl = gmake env sigma goal in + let Sigma (tac, sigma, _) = f.s_enter gl in + let sigma = Sigma.to_evar_map sigma in + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + end + end + + let nf_s_enter f = + InfoL.tag (Info.Dispatch) begin + iter_goal begin fun goal -> + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try + let (gl, sigma) = nf_gmake env sigma goal in + let Sigma (tac, sigma, _) = f.s_enter gl in + let sigma = Sigma.to_evar_map sigma in + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + end + end + + let goals = + Pv.get >>= fun step -> + let sigma = step.solution in + let map goal = + match advance sigma goal with + | None -> None (** ppedrot: Is this check really necessary? *) + | Some goal -> + let gl = + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + tclUNIT (gmake env sigma goal) + in + Some gl + in + tclUNIT (CList.map_filter map step.comb) + + (* compatibility *) + let goal { self=self } = self + + let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t) + +end + + + +(** {6 Trace} *) + +module Trace = struct + + let record_info_trace = InfoL.record_trace + + let log m = InfoL.leaf (Info.Msg m) + let name_tactic m t = InfoL.tag (Info.Tactic m) t + + let pr_info ?(lvl=0) info = + assert (lvl >= 0); + Info.(print (collapse lvl info)) + +end + + + +(** {6 Non-logical state} *) + +module NonLogical = Logic_monad.NonLogical + +let tclLIFT = Proof.lift + +let tclCHECKINTERRUPT = + tclLIFT (NonLogical.make Control.check_for_interrupt) + + + + + +(*** Compatibility layer with <= 8.2 tactics ***) +module V82 = struct + type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma + + let tactic tac = + (* spiwack: we ignore the dependencies between goals here, + expectingly preserving the semantics of <= 8.2 tactics *) + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let open Proof in + Pv.get >>= fun ps -> + try + let tac gl evd = + let glsigma = + tac { Evd.it = gl ; sigma = evd; } in + let sigma = glsigma.Evd.sigma in + let g = glsigma.Evd.it in + ( g, sigma ) + in + (* Old style tactics expect the goals normalized with respect to evars. *) + let (initgoals,initevd) = + Evd.Monad.List.map (fun g s -> goal_nf_evar s g) ps.comb ps.solution + in + let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in + let sgs = CList.flatten goalss in + let sgs = undefined evd sgs in + InfoL.leaf (Info.Tactic (fun () -> Pp.str"")) >> + Pv.set { ps with solution = evd; comb = sgs; } + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + + + (* normalises the evars in the goals, and stores the result in + solution. *) + let nf_evar_goals = + Pv.modify begin fun ps -> + let map g s = goal_nf_evar s g in + let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in + { ps with solution = evd; comb = goals; } + end + + let has_unresolved_evar pv = + Evd.has_undefined pv.solution + + (* Main function in the implementation of Grab Existential Variables.*) + let grab pv = + let undef = Evd.undefined_map pv.solution in + let goals = CList.rev_map fst (Evar.Map.bindings undef) in + { pv with comb = goals } + + + + (* Returns the open goals of the proofview together with the evar_map to + interpret them. *) + let goals { comb = comb ; solution = solution; } = + { Evd.it = comb ; sigma = solution } + + let top_goals initial { solution=solution; } = + let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in + { Evd.it = goals ; sigma=solution; } + + let top_evars initial = + let evars_of_initial (c,_) = + Evar.Set.elements (Evd.evars_of_term c) + in + CList.flatten (CList.map evars_of_initial initial) + + let of_tactic t gls = + try + let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in + let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in + { Evd.sigma = final.solution ; it = final.comb } + with Logic_monad.TacticFailure e as src -> + let (_, info) = Errors.push src in + iraise (e, info) + + let put_status = Status.put + + let catchable_exception = catchable_exception + + let wrap_exceptions f = + try f () + with e when catchable_exception e -> + let (e, info) = Errors.push e in tclZERO ~info e + +end + +(** {7 Notations} *) + +module Notations = struct + let (>>=) = tclBIND + let (<*>) = tclTHEN + let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) + type ('a, 'b) enter = ('a, 'b) Goal.enter = + { enter : 'r. ('a, 'r) Goal.t -> 'b } + type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = + { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } +end diff --git a/engine/proofview.mli b/engine/proofview.mli new file mode 100644 index 0000000000..7996b7969c --- /dev/null +++ b/engine/proofview.mli @@ -0,0 +1,589 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Goal.goal list * Evd.evar_map + + +(** {6 Starting and querying a proof view} *) + +(** Abstract representation of the initial goals of a proof. *) +type entry + +(** Optimize memory consumption *) +val compact : entry -> proofview -> entry * proofview + +(** Initialises a proofview, the main argument is a list of + environments (including a [named_context] which are used as + hypotheses) pair with conclusion types, creating accordingly many + initial goals. Because a proof does not necessarily starts in an + empty [evar_map] (indeed a proof can be triggered by an incomplete + pretyping), [init] takes an additional argument to represent the + initial [evar_map]. *) +val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview + +(** A [telescope] is a list of environment and conclusion like in + {!init}, except that each element may depend on the previous + goals. The telescope passes the goals in the form of a + [Term.constr] which represents the goal as an [evar]. The + [evar_map] is threaded in state passing style. *) +type telescope = + | TNil of Evd.evar_map + | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) + +(** Like {!init}, but goals are allowed to be dependent on one + another. Dependencies between goals is represented with the type + [telescope] instead of [list]. Note that the first [evar_map] of + the telescope plays the role of the [evar_map] argument in + [init]. *) +val dependent_init : telescope -> entry * proofview + +(** [finished pv] is [true] if and only if [pv] is complete. That is, + if it has an empty list of focused goals. There could still be + unsolved subgoaled, but they would then be out of focus. *) +val finished : proofview -> bool + +(** Returns the current [evar] state. *) +val return : proofview -> Evd.evar_map + +val partial_proof : entry -> proofview -> constr list +val initial_goals : entry -> (constr * types) list + + + +(** {6 Focusing commands} *) + +(** A [focus_context] represents the part of the proof view which has + been removed by a focusing action, it can be used to unfocus later + on. *) +type focus_context + +(** Returns a stylised view of a focus_context for use by, for + instance, ide-s. *) +(* spiwack: the type of [focus_context] will change as we push more + refined functions to ide-s. This would be better than spawning a + new nearly identical function everytime. Hence the generic name. *) +(* In this version: the goals in the context, as a "zipper" (the first + list is in reversed order). *) +val focus_context : focus_context -> Goal.goal list * Goal.goal list + +(** [focus i j] focuses a proofview on the goals from index [i] to + index [j] (inclusive, goals are indexed from [1]). I.e. goals + number [i] to [j] become the only focused goals of the returned + proofview. It returns the focused proofview, and a context for + the focus stack. *) +val focus : int -> int -> proofview -> proofview * focus_context + +(** Unfocuses a proofview with respect to a context. *) +val unfocus : focus_context -> proofview -> proofview + + +(** {6 The tactic monad} *) + +(** - Tactics are objects which apply a transformation to all the + subgoals of the current view at the same time. By opposition to + the old vision of applying it to a single goal. It allows tactics + such as [shelve_unifiable], tactics to reorder the focused goals, + or global automation tactic for dependent subgoals (instantiating + an evar has influences on the other goals of the proof in + progress, not being able to take that into account causes the + current eauto tactic to fail on some instances where it could + succeed). Another benefit is that it is possible to write tactics + that can be executed even if there are no focused goals. + - Tactics form a monad ['a tactic], in a sense a tactic can be + seen as a function (without argument) which returns a value of + type 'a and modifies the environment (in our case: the view). + Tactics of course have arguments, but these are given at the + meta-level as OCaml functions. Most tactics in the sense we are + used to return [()], that is no really interesting values. But + some might pass information around. The tactics seen in Coq's + Ltac are (for now at least) only [unit tactic], the return values + are kept for the OCaml toolkit. The operation or the monad are + [Proofview.tclUNIT] (which is the "return" of the tactic monad) + [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN] + (which is a specialized bind on unit-returning tactics). + - Tactics have support for full-backtracking. Tactics can be seen + having multiple success: if after returning the first success a + failure is encountered, the tactic can backtrack and use a second + success if available. The state is backtracked to its previous + value, except the non-logical state defined in the {!NonLogical} + module below. +*) + + +(** The abstract type of tactics *) +type +'a tactic + +(** Applies a tactic to the current proofview. Returns a tuple + [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv] + is the updated proofview, [b] a boolean which is [true] if the + tactic has not done any action considered unsafe (such as + admitting a lemma), [sh] is the list of goals which have been + shelved by the tactic, and [gu] the list of goals on which the + tactic has given up. In case of multiple success the first one is + selected. If there is no success, fails with + {!Logic_monad.TacticFailure}*) +val apply : Environ.env -> 'a tactic -> proofview -> 'a + * proofview + * (bool*Goal.goal list*Goal.goal list) + * Proofview_monad.Info.tree + +(** {7 Monadic primitives} *) + +(** Unit of the tactic monad. *) +val tclUNIT : 'a -> 'a tactic + +(** Bind operation of the tactic monad. *) +val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic + +(** Interprets the ";" (semicolon) of Ltac. As a monadic operation, + it's a specialized "bind". *) +val tclTHEN : unit tactic -> 'a tactic -> 'a tactic + +(** [tclIGNORE t] has the same operational content as [t], but drops + the returned value. *) +val tclIGNORE : 'a tactic -> unit tactic + +(** Generic monadic combinators for tactics. *) +module Monad : Monad.S with type +'a t = 'a tactic + +(** {7 Failure and backtracking} *) + +(** [tclZERO e] fails with exception [e]. It has no success. *) +val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic + +(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever + the successes of [t1] have been depleted and it failed with [e], + then it behaves as [t2 e]. In other words, [tclOR] inserts a + backtracking point. *) +val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic + +(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one + success or [t2 e] if [t1] fails with [e]. It is analogous to + [try/with] handler of exception in that it is not a backtracking + point. *) +val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic + +(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] + succeeds at least once then it behaves as [tclBIND a s] otherwise, + if [a] fails with [e], then it behaves as [f e]. *) +val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic + +(** [tclONCE t] behave like [t] except it has at most one success: + [tclONCE t] stops after the first success of [t]. If [t] fails + with [e], [tclONCE t] also fails with [e]. *) +val tclONCE : 'a tactic -> 'a tactic + +(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one + success. Otherwise it fails. The tactic [t] is run until its first + success, then a failure with exception [e] is simulated. It [t] + yields another success, then [tclEXACTLY_ONCE e t] fails with + [MoreThanOneSuccess] (it is a user error). Otherwise, + [tclEXACTLY_ONCE e t] succeeds with the first success of + [t]. Notice that the choice of [e] is relevant, as the presence of + further successes may depend on [e] (see {!tclOR}). *) +exception MoreThanOneSuccess +val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic + +(** [tclCASE t] splits [t] into its first success and a + continuation. It is the most general primitive to control + backtracking. *) +type 'a case = + | Fail of iexn + | Next of 'a * (iexn -> 'a tactic) +val tclCASE : 'a tactic -> 'a case tactic + +(** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of + stopping after the first success, it succeeds like [t] until a + failure with an exception [e] such that [p e = Some e'] is raised. At + which point it drops the remaining successes, failing with [e']. + [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *) +val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic + + +(** {7 Focusing tactics} *) + +(** [tclFOCUS i j t] applies [t] after focusing on the goals number + [i] to [j] (see {!focus}). The rest of the goals is restored after + the tactic action. If the specified range doesn't correspond to + existing goals, fails with [NoSuchGoals] (a user error). this + exception is caught at toplevel with a default message + a hook + message that can be customized by [set_nosuchgoals_hook] below. + This hook is used to add a suggestion about bullets when + applicable. *) +exception NoSuchGoals of int +val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit + +val tclFOCUS : int -> int -> 'a tactic -> 'a tactic + +(** [tclFOCUSID x t] applies [t] on a (single) focused goal like + {!tclFOCUS}. The goal is found by its name rather than its + number.*) +val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic + +(** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the + specified range doesn't correspond to existing goals, behaves like + [tclUNIT ()] instead of failing. *) +val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic + + +(** {7 Dispatching on goals} *) + +(** Dispatch tacticals are used to apply a different tactic to each + goal under focus. They come in two flavours: [tclDISPATCH] takes a + list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL] + takes a list of ['a tactic] and returns an ['a list tactic]. + + They both work by applying each of the tactic in a focus + restricted to the corresponding goal (starting with the first + goal). In the case of [tclDISPATCHL], the tactic returns a list of + the same size as the argument list (of tactics), each element + being the result of the tactic executed in the corresponding goal. + + When the length of the tactic list is not the number of goal, + raises [SizeMismatch (g,t)] where [g] is the number of available + goals, and [t] the number of tactics passed. *) +exception SizeMismatch of int*int +val tclDISPATCH : unit tactic list -> unit tactic +val tclDISPATCHL : 'a tactic list -> 'a list tactic + +(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r] + tactic is "repeated" enough time such that every goal has a tactic + assigned to it ([b] is the list of tactics applied to the first + goals, [e] to the last goals, and [r] is applied to every goal in + between). *) +val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic + +(** [tclINDEPENDENT tac] runs [tac] on each goal successively, from + the first one to the last one. Backtracking in one goal is + independent of backtracking in another. It is equivalent to + [tclEXTEND [] tac []]. *) +val tclINDEPENDENT : unit tactic -> unit tactic + + +(** {7 Goal manipulation} *) + +(** Shelves all the goals under focus. The goals are placed on the + shelf for later use (or being solved by side-effects). *) +val shelve : unit tactic + +(** Shelves the unifiable goals under focus, i.e. the goals which + appear in other goals under focus (the unfocused goals are not + considered). *) +val shelve_unifiable : unit tactic + +(** [guard_no_unifiable] returns the list of unifiable goals if some + goals are unifiable (see {!shelve_unifiable}) in the current focus. *) +val guard_no_unifiable : Names.Name.t list option tactic + +(** [unshelve l p] adds all the goals in [l] at the end of the focused + goals of p *) +val unshelve : Goal.goal list -> proofview -> proofview + +(** [with_shelf tac] executes [tac] and returns its result together with the set + of goals shelved by [tac]. The current shelf is unchanged. *) +val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic + +(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] + is negative, then it puts the [n] last goals first.*) +val cycle : int -> unit tactic + +(** [swap i j] swaps the position of goals number [i] and [j] + (negative numbers can be used to address goals from the end. Goals + are indexed from [1]. For simplicity index [0] corresponds to goal + [1] as well, rather than raising an error. *) +val swap : int -> int -> unit tactic + +(** [revgoals] reverses the list of focused goals. *) +val revgoals : unit tactic + +(** [numgoals] returns the number of goals under focus. *) +val numgoals : int tactic + + +(** {7 Access primitives} *) + +(** [tclEVARMAP] doesn't affect the proof, it returns the current + [evar_map]. *) +val tclEVARMAP : Evd.evar_map tactic + +(** [tclENV] doesn't affect the proof, it returns the current + environment. It is not the environment of a particular goal, + rather the "global" environment of the proof. The goal-wise + environment is obtained via {!Proofview.Goal.env}. *) +val tclENV : Environ.env tactic + + +(** {7 Put-like primitives} *) + +(** [tclEFFECTS eff] add the effects [eff] to the current state. *) +val tclEFFECTS : Safe_typing.private_constants -> unit tactic + +(** [mark_as_unsafe] declares the current tactic is unsafe. *) +val mark_as_unsafe : unit tactic + +(** Gives up on the goal under focus. Reports an unsafe status. Proofs + with given up goals cannot be closed. *) +val give_up : unit tactic + + +(** {7 Control primitives} *) + +(** [tclPROGRESS t] checks the state of the proof after [t]. It it is + identical to the state before, then [tclePROGRESS t] fails, otherwise + it succeeds like [t]. *) +val tclPROGRESS : 'a tactic -> 'a tactic + +(** 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 + +(** [tclTIME s t] displays time for each atomic call to t, using s as an + identifying annotation if present *) +val tclTIME : string option -> 'a tactic -> 'a tactic + +(** {7 Unsafe primitives} *) + +(** The primitives in the [Unsafe] module should be avoided as much as + possible, since they can make the proof state inconsistent. They are + nevertheless helpful, in particular when interfacing the pretyping and + the proof engine. *) +module Unsafe : sig + + (** [tclEVARS sigma] replaces the current [evar_map] by [sigma]. If + [sigma] has new unresolved [evar]-s they will not appear as + goal. If goals have been solved in [sigma] they will still + appear as unsolved goals. *) + val tclEVARS : Evd.evar_map -> unit tactic + + (** Like {!tclEVARS} but also checks whether goals have been solved. *) + val tclEVARSADVANCE : Evd.evar_map -> unit tactic + + (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently + being proved, appending them to the list of focused goals. If a + goal is already solved, it is not added. *) + val tclNEWGOALS : Goal.goal list -> unit tactic + + (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a + goal is already solved, it is not set. *) + val tclSETGOALS : Goal.goal list -> unit tactic + + (** [tclGETGOALS] returns the list of goals under focus. *) + val tclGETGOALS : Goal.goal list tactic + + (** Sets the evar universe context. *) + val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic + + (** Clears the future goals store in the proof view. *) + val reset_future_goals : proofview -> proofview + + (** Give an evar the status of a goal (changes its source location + and makes it unresolvable for type classes. *) + val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map + + (** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) + val advance : Evd.evar_map -> Evar.t -> Evar.t option + + val typeclass_resolvable : unit Evd.Store.field + +end + +(** This module gives access to the innards of the monad. Its use is + restricted to very specific cases. *) +module UnsafeRepr : +sig + type state = Proofview_monad.Logical.Unsafe.state + val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t + val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic +end + +(** {6 Goal-dependent tactics} *) + +module Goal : sig + + (** Type of goals. + + The first parameter type is a phantom argument indicating whether the data + contained in the goal has been normalized w.r.t. the current sigma. If it + is the case, it is flagged [ `NF ]. You may still access the un-normalized + data using {!assume} if you known you do not rely on the assumption of + being normalized, at your own risk. + + The second parameter is a stage indicating where the goal belongs. See + module {!Sigma}. + *) + type ('a, 'r) t + + (** Assume that you do not need the goal to be normalized. *) + val assume : ('a, 'r) t -> ([ `NF ], 'r) t + + (** Normalises the argument goal. *) + val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic + + (** [concl], [hyps], [env] and [sigma] given a goal [gl] return + respectively the conclusion of [gl], the hypotheses of [gl], the + environment of [gl] (i.e. the global environment and the + hypotheses) and the current evar map. *) + val concl : ([ `NF ], 'r) t -> Term.constr + val hyps : ([ `NF ], 'r) t -> Context.Named.t + val env : ('a, 'r) t -> Environ.env + val sigma : ('a, 'r) t -> 'r Sigma.t + val extra : ('a, 'r) t -> Evd.Store.t + + (** Returns the goal's conclusion even if the goal is not + normalised. *) + val raw_concl : ('a, 'r) t -> Term.constr + + type ('a, 'b) enter = + { enter : 'r. ('a, 'r) t -> 'b } + + (** [nf_enter t] applies the goal-dependent tactic [t] in each goal + independently, in the manner of {!tclINDEPENDENT} except that + the current goal is also given as an argument to [t]. The goal + is normalised with respect to evars. *) + val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic + + (** Like {!nf_enter}, but does not normalize the goal beforehand. *) + val enter : ([ `LZ ], unit tactic) enter -> unit tactic + + type ('a, 'b) s_enter = + { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } + + (** A variant of {!enter} allows to work with a monotonic state. The evarmap + returned by the argument is put back into the current state before firing + the returned tactic. *) + val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic + + (** Like {!s_enter}, but normalizes the goal beforehand. *) + val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic + + (** Recover the list of current goals under focus, without evar-normalization. + FIXME: encapsulate the level in an existential type. *) + val goals : ([ `LZ ], 'r) t tactic list tactic + + (** Compatibility: avoid if possible *) + val goal : ([ `NF ], 'r) t -> Evar.t + + (** Every goal is valid at a later stage. FIXME: take a later evarmap *) + val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t + +end + + +(** {6 Trace} *) + +module Trace : sig + + (** [record_info_trace t] behaves like [t] except the [info] trace + is stored. *) + val record_info_trace : 'a tactic -> 'a tactic + + val log : Proofview_monad.lazy_msg -> unit tactic + val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic + + val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds + +end + + +(** {6 Non-logical state} *) + +(** The [NonLogical] module allows the execution of effects (including + I/O) in tactics (non-logical side-effects are not discarded at + failures). *) +module NonLogical : module type of Logic_monad.NonLogical + +(** [tclLIFT c] is a tactic which behaves exactly as [c]. *) +val tclLIFT : 'a NonLogical.t -> 'a tactic + + +(**/**) + +(*** Compatibility layer with <= 8.2 tactics ***) +module V82 : sig + type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma + val tactic : tac -> unit tactic + + (* normalises the evars in the goals, and stores the result in + solution. *) + val nf_evar_goals : unit tactic + + val has_unresolved_evar : proofview -> bool + + (* Main function in the implementation of Grab Existential Variables. + Resets the proofview's goals so that it contains all unresolved evars + (in chronological order of insertion). *) + val grab : proofview -> proofview + + (* Returns the open goals of the proofview together with the evar_map to + interpret them. *) + val goals : proofview -> Evar.t list Evd.sigma + + val top_goals : entry -> proofview -> Evar.t list Evd.sigma + + (* returns the existential variable used to start the proof *) + val top_evars : entry -> Evd.evar list + + (* Caution: this function loses quite a bit of information. It + should be avoided as much as possible. It should work as + expected for a tactic obtained from {!V82.tactic} though. *) + val of_tactic : 'a tactic -> tac + + (* marks as unsafe if the argument is [false] *) + val put_status : bool -> unit tactic + + (* exception for which it is deemed to be safe to transmute into + tactic failure. *) + val catchable_exception : exn -> bool + + (* transforms every Ocaml (catchable) exception into a failure in + the monad. *) + val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic +end + +(** {7 Notations} *) + +module Notations : sig + + (** {!tclBIND} *) + val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic + (** {!tclTHEN} *) + val (<*>) : unit tactic -> 'a tactic -> 'a tactic + (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) + val (<+>) : 'a tactic -> 'a tactic -> 'a tactic + + type ('a, 'b) enter = ('a, 'b) Goal.enter = + { enter : 'r. ('a, 'r) Goal.t -> 'b } + type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = + { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } +end -- cgit v1.2.3