diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 10 | ||||
| -rw-r--r-- | engine/eConstr.mli | 6 | ||||
| -rw-r--r-- | engine/engine.mllib | 1 | ||||
| -rw-r--r-- | engine/evarutil.ml | 58 | ||||
| -rw-r--r-- | engine/evarutil.mli | 28 | ||||
| -rw-r--r-- | engine/evd.ml | 21 | ||||
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/ftactic.ml | 18 | ||||
| -rw-r--r-- | engine/ftactic.mli | 13 | ||||
| -rw-r--r-- | engine/proofview.ml | 69 | ||||
| -rw-r--r-- | engine/proofview.mli | 51 | ||||
| -rw-r--r-- | engine/sigma.ml | 117 | ||||
| -rw-r--r-- | engine/sigma.mli | 131 | ||||
| -rw-r--r-- | engine/termops.ml | 27 | ||||
| -rw-r--r-- | engine/universes.ml | 2 |
15 files changed, 106 insertions, 448 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index c0485e4e76..078f2fc333 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -45,6 +45,7 @@ val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt +val to_rel_decl : Evd.evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt end = struct @@ -131,6 +132,7 @@ let of_named_decl d = d let unsafe_to_named_decl d = d let of_rel_decl d = d let unsafe_to_rel_decl d = d +let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d end @@ -778,9 +780,11 @@ let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e) let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e) let fresh_global ?loc ?rigid ?names env sigma reference = - let Sigma.Sigma (t,sigma,p) = - Sigma.fresh_global ?loc ?rigid ?names env sigma reference in - Sigma.Sigma (of_constr t,sigma,p) + let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in + evd, of_constr t + +let is_global sigma gr c = + Globnames.is_global gr (to_constr sigma c) module Unsafe = struct diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 9d705b4d55..07a4dc8e23 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -259,13 +259,17 @@ val lookup_named_val : variable -> named_context_val -> named_declaration (* XXX Missing Sigma proxy *) val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> - 'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma + Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t + +val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool (** {5 Extra} *) val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt +val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt + (** {5 Unsafe operations} *) module Unsafe : diff --git a/engine/engine.mllib b/engine/engine.mllib index 1b670d3667..afc02d7f6d 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,7 +2,6 @@ Logic_monad Universes UState Evd -Sigma EConstr Namegen Termops diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6cba6f6075..e8d184632e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -15,7 +15,6 @@ open Namegen open Pre_env open Environ open Evd -open Sigma.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -45,8 +44,8 @@ let e_new_global evdref x = EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x) let new_global evd x = - let Sigma (c, sigma, p) = Sigma.fresh_global (Global.env()) evd x in - Sigma (EConstr.of_constr c, sigma, p) + let (evd, c) = Evd.fresh_global (Global.env()) evd x in + (evd, EConstr.of_constr c) (****************************************************) (* Expanding/testing/exposing existential variables *) @@ -220,7 +219,7 @@ let make_pure_subst evi args = (fun decl (args,l) -> match args with | a::rest -> (rest, (NamedDecl.get_id decl, a)::l) - | _ -> anomaly (Pp.str "Instance does not match its signature")) + | _ -> anomaly (Pp.str "Instance does not match its signature.")) (evar_filtered_context evi) (Array.rev_to_list args,[])) (*------------------------------------* @@ -367,21 +366,18 @@ let push_rel_context_to_named_context env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let restrict_evar evd evk filter candidates = - let evd = Sigma.to_evar_map evd in +let restrict_evar evd evk filter ?src candidates = let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in - let evd, evk' = Evd.restrict evk filter ?candidates evd in - Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) + let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in + Evd.declare_future_goal evk' evd, evk' 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) + (evd, evk) let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = let typ = EConstr.Unsafe.to_constr typ in - let evd = Sigma.to_evar_map evd in let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in @@ -407,19 +403,19 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca if principal then Evd.declare_principal_goal newevk evd else Evd.declare_future_goal newevk evd in - Sigma.Unsafe.of_pair (newevk, evd) + (evd, newevk) let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = let open EConstr in 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) + let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in + evd, mkEvar (newevk,Array.of_list instance) (* [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 (Sigma.to_evar_map evd) typ in + let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env evd typ in let map c = subst2 subst vsubst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = @@ -428,27 +424,20 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = | 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 (EConstr.mkSort s) in - Sigma ((e, s), evd', p +> q) + let (evd', s) = new_sort_variable rigid evd in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in + evd', (e, s) 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; + let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in + evdref := evd; c let new_Type ?(rigid=Evd.univ_flexible) env evd = let open EConstr in - let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in - Sigma (mkSort s, sigma, p) + let (evd, s) = new_sort_variable rigid evd in + (evd, mkSort s) let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = let evd', s = new_sort_variable rigid !evdref in @@ -456,7 +445,7 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = (* 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 + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in evdref := evd'; ev @@ -552,9 +541,8 @@ let rec check_and_clear_in_constr env evdref err ids global 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 + let evd = !evdref in + let (evd,_) = restrict_evar evd evk filter None in evdref := evd; (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) let evi = Evd.find !evdref evk in @@ -723,8 +711,8 @@ let occur_evar_upto sigma n c = let judge_of_new_Type evd = let open EConstr in - 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 (evd', s) = new_univ_variable univ_rigid evd in + (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }) let subterm_source evk (loc,k) = let evk = match k with diff --git a/engine/evarutil.mli b/engine/evarutil.mli index fcc435a2ec..90c5c3dc0d 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -22,18 +22,18 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar : - env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> (constr, 'r) Sigma.sigma + ?principal:bool -> types -> evar_map * EConstr.t val new_pure_evar : - named_context_val -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> (evar, 'r) Sigma.sigma + ?principal:bool -> types -> evar_map * evar -val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma +val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar (** the same with side-effects *) val e_new_evar : @@ -45,23 +45,23 @@ val e_new_evar : (** 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:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> - (constr * sorts, 'r) Sigma.sigma + evar_map * (constr * sorts) val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?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 new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr 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 +val restrict_evar : evar_map -> existential_key -> Filter.t -> + ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * existential_key (** Polymorphic constants *) -val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma +val new_global : evar_map -> Globnames.global_reference -> evar_map * constr val e_new_global : evar_map ref -> Globnames.global_reference -> constr (** Create a fresh evar in a context different from its definition context: @@ -71,11 +71,11 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr 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 -> + named_context_val -> evar_map -> types -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> - constr list -> (constr, 'r) Sigma.sigma + constr list -> evar_map * constr val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list @@ -133,7 +133,7 @@ val occur_evar_upto : evar_map -> Evar.t -> constr -> bool (** {6 Value/Type constraints} *) -val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma +val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment (***********************************************************) diff --git a/engine/evd.ml b/engine/evd.ml index b677705bc9..08d26f40d4 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -155,7 +155,7 @@ let make_evar hyps ccl = { } let instance_mismatch () = - anomaly (Pp.str "Signature and its instance do not match") + anomaly (Pp.str "Signature and its instance do not match.") let evar_concl evi = evi.evar_concl @@ -400,7 +400,7 @@ let rename evk id (evtoid, idtoev) = match id' with | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev) | Some id' -> - if Idmap.mem id idtoev then anomaly (str "Evar name already in use"); + if Idmap.mem id idtoev then anomaly (str "Evar name already in use."); (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev)) let reassign_name_defined evk evk' (evtoid, idtoev as names) = @@ -553,7 +553,7 @@ let existential_type d (n, args) = let info = try find d n with Not_found -> - anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in + anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared.") in instantiate_evar_array info info.evar_concl args let add_constraints d c = @@ -635,9 +635,9 @@ let define_aux def undef evk body = try EvMap.find evk undef with Not_found -> if EvMap.mem evk def then - anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice") + anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.") else - anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar") + anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") in let () = assert (oldinfo.evar_body == Evar_empty) in let newinfo = { oldinfo with evar_body = Evar_defined body } in @@ -653,12 +653,13 @@ let define evk body evd = let evar_names = EvNames.remove_name_defined evk evd.evar_names in { evd with defn_evars; undf_evars; last_mods; evar_names } -let restrict evk filter ?candidates evd = +let restrict evk filter ?candidates ?src 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; evar_candidates = candidates; + evar_source = (match src with None -> evar_info.evar_source | Some src -> src); evar_extra = Store.empty } in let last_mods = match evd.conv_pbs with | [] -> evd.last_mods @@ -1021,7 +1022,7 @@ let try_meta_fvalue evd mv = let meta_fvalue evd mv = try try_meta_fvalue evd mv - with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value") + with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value.") let meta_value evd mv = (fst (try_meta_fvalue evd mv)).rebus @@ -1040,7 +1041,7 @@ let meta_declare mv v ?(name=Anonymous) evd = let meta_assign mv (v, pb) evd = let modify _ = function | Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty) - | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined") + | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.") in let metas = Metamap.modify mv modify evd.metas in set_metas evd metas @@ -1048,7 +1049,7 @@ let meta_assign mv (v, pb) evd = let meta_reassign mv (v, pb) evd = let modify _ = function | Clval(na, _, ty) -> Clval (na, (mk_freelisted v, pb), ty) - | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined") + | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined.") in let metas = Metamap.modify mv modify evd.metas in set_metas evd metas @@ -1089,7 +1090,7 @@ let dependent_evar_ident ev evd = let evi = find evd ev in match evi.evar_source with | (_,Evar_kinds.VarInstance id) -> id - | _ -> anomaly (str "Not an evar resulting of a dependent binding") + | _ -> anomaly (str "Not an evar resulting of a dependent binding.") (**********************************************************) (* Extra data *) diff --git a/engine/evd.mli b/engine/evd.mli index 0053324706..86755c360b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -240,7 +240,7 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> (** {6 Misc} *) val restrict : evar -> Filter.t -> ?candidates:constr list -> - evar_map -> evar_map * evar + ?src:Evar_kinds.t located -> 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 *) diff --git a/engine/ftactic.ml b/engine/ftactic.ml index aeaaea7e48..68368e38fa 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -53,31 +53,17 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function Proofview.tclUNIT (Depends filtered) let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l) -let set_sigma r = - let Sigma.Sigma (ans, sigma, _) = r in - Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () -> ans let nf_enter f = bind goals (fun gl -> gl >>= fun gl -> Proofview.Goal.normalize gl >>= fun nfgl -> - Proofview.V82.wrap_exceptions (fun () -> f.enter nfgl)) - -let nf_s_enter f = - bind goals - (fun gl -> - gl >>= fun gl -> - Proofview.Goal.normalize gl >>= fun nfgl -> - Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter nfgl))) + Proofview.V82.wrap_exceptions (fun () -> f nfgl)) let enter f = bind goals - (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f.enter gl)) - -let s_enter f = - bind goals - (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter gl))) + (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) let with_env t = t >>= function diff --git a/engine/ftactic.mli b/engine/ftactic.mli index 5db373199e..97bebe9da8 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Proofview.Notations - (** This module defines potentially focussing tactics. They are used by Ltac to emulate the historical behaviour of always-focussed tactics while still allowing to remain global when the goal is not needed. *) @@ -41,20 +39,13 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** {5 Focussing} *) -val nf_enter : ([ `NF ], 'a t) enter -> 'a t +val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal. The resulting tactic is focussed. *) -val enter : ([ `LZ ], 'a t) enter -> 'a t +val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is focussed. *) -val s_enter : ([ `LZ ], 'a t) s_enter -> 'a t -(** Enter a goal and put back an evarmap. The resulting tactic is focussed. *) - -val nf_s_enter : ([ `NF ], 'a t) s_enter -> 'a t -(** Enter a goal, without evar normalization and put back an evarmap. The - resulting tactic is focussed. *) - val with_env : 'a t -> (Environ.env*'a) t (** [with_env t] returns, in addition to the return type of [t], an environment, which is the global environment if [t] does not focus on diff --git a/engine/proofview.ml b/engine/proofview.ml index ddfc0e39dd..39ef65dab1 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -16,7 +16,6 @@ open Pp open Util open Proofview_monad -open Sigma.Notations open Context.Named.Declaration (** Main state of tactics *) @@ -71,10 +70,8 @@ let dependent_init = 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 (gl, _) = EConstr.destEvar (Sigma.to_evar_map sigma) econstr in - let sigma = Sigma.to_evar_map sigma in + let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in + let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (econstr, typ) :: ret in entry, { solution = sol; comb = gl :: comb; shelf = [] } @@ -696,6 +693,12 @@ let mark_in_evm ~goal evd content = let info = if goal then { info with Evd.evar_source = match info.Evd.evar_source with + (* Two kinds for goal evars: + - GoalEvar (morally not dependent) + - VarInstance (morally dependent of some name). + This is a heuristic for naming these evars. *) + | loc, (Evar_kinds.QuestionMark (_,Names.Name id) | + Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x | loc,_ -> loc,Evar_kinds.GoalEvar } else info @@ -1006,20 +1009,17 @@ let catchable_exception = function module Goal = struct - type ('a, 'r) t = { + type 'a t = { env : Environ.env; sigma : Evd.evar_map; concl : EConstr.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 assume (gl : 'a t) = (gl :> [ `NF ] t) let env {env} = env - let sigma {sigma} = Sigma.Unsafe.of_evar_map sigma + let sigma {sigma} = sigma let hyps {env} = EConstr.named_context env let concl {concl} = concl let extra {sigma; self} = goal_extra sigma self @@ -1042,7 +1042,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) with e when catchable_exception e -> let (e, info) = CErrors.push e in tclZERO ~info e @@ -1060,7 +1060,7 @@ module Goal = struct gmake_with info env sigma goal let enter f = - let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in + let f gl = InfoL.tag (Info.DBranch) (f gl) in InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> Env.get >>= fun env -> @@ -1085,48 +1085,13 @@ module Goal = struct | [goal] -> begin Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> - try f.enter (gmake env sigma goal) + try f (gmake env sigma goal) with e when catchable_exception e -> let (e, info) = CErrors.push e in tclZERO ~info e end | _ -> tclZERO NotExactlyOneSubgoal - 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) = CErrors.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) = CErrors.push e in - tclZERO ~info e - end - end - let goals = Pv.get >>= fun step -> let sigma = step.solution in @@ -1150,8 +1115,6 @@ module Goal = struct (* compatibility *) let goal { self=self } = self - let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t) - end @@ -1275,8 +1238,4 @@ 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 index da8a8fecdd..aae25b6f8f 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -469,67 +469,48 @@ module Goal : sig 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 + type 'a t (** Assume that you do not need the goal to be normalized. *) - val assume : ('a, 'r) t -> ([ `NF ], 'r) t + val assume : 'a t -> [ `NF ] t (** Normalises the argument goal. *) - val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic + val normalize : 'a t -> [ `NF ] 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 : ('a, 'r) t -> constr - val hyps : ('a, 'r) t -> named_context - val env : ('a, 'r) t -> Environ.env - val sigma : ('a, 'r) t -> 'r Sigma.t - val extra : ('a, 'r) t -> Evd.Store.t - - type ('a, 'b) enter = - { enter : 'r. ('a, 'r) t -> 'b } + val concl : 'a t -> constr + val hyps : 'a t -> named_context + val env : 'a t -> Environ.env + val sigma : 'a t -> Evd.evar_map + val extra : 'a t -> Evd.Store.t (** [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 + val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ], unit tactic) enter -> unit tactic + val enter : ([ `LZ ] t -> unit tactic) -> unit tactic (** Like {!enter}, but assumes exactly one goal under focus, raising *) (** an error otherwise. *) - val enter_one : ([ `LZ ], 'a tactic) enter -> 'a 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 + val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a 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 + val goals : [ `LZ ] t tactic list tactic (** [unsolved g] is [true] if [g] is still unsolved in the current proof state. *) - val unsolved : ('a, 'r) t -> bool tactic + val unsolved : 'a t -> bool 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 + val goal : [ `NF ] t -> Evar.t end @@ -616,8 +597,4 @@ module Notations : sig (** {!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 diff --git a/engine/sigma.ml b/engine/sigma.ml deleted file mode 100644 index 001f8be80a..0000000000 --- a/engine/sigma.ml +++ /dev/null @@ -1,117 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -type 'a t = Evd.evar_map - -type ('a, 'b) le = unit - -let refl = () -let cons _ _ = () -let (+>) = 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 - -let here x s = Sigma (x, s, ()) - -(** API *) - -type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh - -let new_evar sigma ?name info = - let (sigma, evk) = Evd.new_evar sigma ?name info in - Fresh (evk, sigma, ()) - -let define evk c sigma = - Sigma ((), Evd.define evk c sigma, ()) - -let new_univ_level_variable ?loc ?name rigid sigma = - let (sigma, u) = Evd.new_univ_level_variable ?loc ?name rigid sigma in - Sigma (u, sigma, ()) - -let new_univ_variable ?loc ?name rigid sigma = - let (sigma, u) = Evd.new_univ_variable ?loc ?name rigid sigma in - Sigma (u, sigma, ()) - -let new_sort_variable ?loc ?name rigid sigma = - let (sigma, u) = Evd.new_sort_variable ?loc ?name rigid sigma in - Sigma (u, sigma, ()) - -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 ?loc env sigma cst = - let (sigma, cst) = Evd.fresh_constant_instance ?loc env sigma cst in - Sigma (cst, sigma, ()) - -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 ?loc env sigma pc = - let (sigma, c) = Evd.fresh_constructor_instance ?loc env sigma pc in - Sigma (c, sigma, ()) - -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 *) - -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 deleted file mode 100644 index 8e8df02f29..0000000000 --- a/engine/sigma.mli +++ /dev/null @@ -1,131 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * 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, - and in particular statically suppress evar leaks and the like. To this - ends, it defines a type of indexed evarmaps whose phantom typing ensures - monotonous use. -*) - -(** {5 Stages} *) - -type ('a, 'b) le -(** Relationship stating that stage ['a] is anterior to stage ['b] *) - -val refl : ('a, 'a) le -(** Reflexivity of anteriority *) - -val cons : ('a, 'b) le -> ('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. This is just a plain evarmap with a phantom type. *) - -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 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 -(** 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 -> ?name:Id.t -> - Evd.evar_info -> 'r fresh - -val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma - -(** Polymorphic universes *) - -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> - Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma -val new_univ_variable : ?loc:Loc.t -> ?name:string -> - Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma -val new_sort_variable : ?loc:Loc.t -> ?name:string -> - 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 : - ?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma -val fresh_inductive_instance : - ?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 : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> - 'r t -> Globnames.global_reference -> (constr, '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 diff --git a/engine/termops.ml b/engine/termops.ml index ca32c06a75..92016d4af4 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -31,10 +31,6 @@ let pr_sort_family = function | InProp -> (str "Prop") | InType -> (str "Type") -let pr_name = function - | Name id -> pr_id id - | Anonymous -> str "_" - let pr_con sp = str(string_of_con sp) let pr_fix pr_constr ((t,i),(lna,tl,bl)) = @@ -42,7 +38,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = hov 1 (str"fix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ + Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") @@ -65,10 +61,10 @@ let rec pr_constr c = match kind_of_term c with (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ pr_constr c ++ str")") | Lambda (na,t,c) -> hov 1 - (str"fun " ++ pr_name na ++ str":" ++ + (str"fun " ++ Name.print na ++ str":" ++ pr_constr t ++ str" =>" ++ spc() ++ pr_constr c) | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++ + (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++ str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++ pr_constr c) | App (c,l) -> hov 1 @@ -93,7 +89,7 @@ let rec pr_constr c = match kind_of_term c with hov 1 (str"cofix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - pr_name na ++ str":" ++ pr_constr ty ++ + Name.print na ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") @@ -112,6 +108,7 @@ let pr_evar_suggested_name evk sigma = | None -> match evi.evar_source with | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id | _,Evar_kinds.VarInstance id -> id + | _,Evar_kinds.QuestionMark (_,Name id) -> id | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" | _ -> let env = reset_with_named_context evi.evar_hyps (Global.env()) in @@ -308,8 +305,8 @@ let pr_evar_universe_context ctx = let print_env_short env = let print_constr = print_kconstr in let pr_rel_decl = function - | RelDecl.LocalAssum (n,_) -> pr_name n - | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" + | RelDecl.LocalAssum (n,_) -> Name.print n + | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")" in let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in @@ -506,7 +503,7 @@ let push_named_rec_types (lna,typarray,_) env = (fun i na t -> match na with | Name id -> LocalAssum (id, lift i t) - | Anonymous -> anomaly (Pp.str "Fix declarations must be named")) + | Anonymous -> anomaly (Pp.str "Fix declarations must be named.")) lna typarray in Array.fold_left (fun e assum -> push_named assum e) env ctxt @@ -582,7 +579,7 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with (* Get the last arg of an application *) let last_arg sigma c = match EConstr.kind sigma c with | App (f,cl) -> Array.last cl - | _ -> anomaly (Pp.str "last_arg") + | _ -> anomaly (Pp.str "last_arg.") (* Get the last arg of an application *) let decompose_app_vect sigma c = @@ -1289,7 +1286,7 @@ let rec eta_reduce_head sigma c = (match EConstr.kind sigma (eta_reduce_head sigma c') with | App (f,cl) -> let lastn = (Array.length cl) - 1 in - if lastn < 0 then anomaly (Pp.str "application without arguments") + if lastn < 0 then anomaly (Pp.str "application without arguments.") else (match EConstr.kind sigma cl.(lastn) with | Rel 1 -> @@ -1442,7 +1439,7 @@ let prod_applist sigma c l = match EConstr.kind sigma c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> Vars.substl subst c - | _ -> anomaly (Pp.str "Not enough prod's") in + | _ -> anomaly (Pp.str "Not enough prod's.") in app [] c l (* Combinators on judgments *) @@ -1458,7 +1455,7 @@ let context_chop k ctx = | (0, l2) -> (List.rev acc, l2) | (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") + | (_, []) -> anomaly (Pp.str "context_chop.") in chop_aux [] (k,ctx) (* Do not skip let-in's *) diff --git a/engine/universes.ml b/engine/universes.ml index 1900112dde..f201081862 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -101,7 +101,7 @@ let enforce_eq_instances_univs strict x y c = let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ - Pp.str " instances of different lengths"); + Pp.str " instances of different lengths."); CArray.fold_right2 (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) ax ay c |