diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 5 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 | ||||
| -rw-r--r-- | engine/engine.mllib | 1 | ||||
| -rw-r--r-- | engine/evarutil.ml | 52 | ||||
| -rw-r--r-- | engine/evarutil.mli | 28 | ||||
| -rw-r--r-- | engine/ftactic.ml | 18 | ||||
| -rw-r--r-- | engine/ftactic.mli | 13 | ||||
| -rw-r--r-- | engine/proofview.ml | 63 | ||||
| -rw-r--r-- | engine/proofview.mli | 51 | ||||
| -rw-r--r-- | engine/sigma.ml | 117 | ||||
| -rw-r--r-- | engine/sigma.mli | 131 |
11 files changed, 63 insertions, 418 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 33d7acc319..078f2fc333 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -780,9 +780,8 @@ 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) diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 94b7ca96ae..07a4dc8e23 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -259,7 +259,7 @@ 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 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 59ad4ef472..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 *) @@ -368,20 +367,17 @@ let push_rel_context_to_named_context env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole let restrict_evar evd evk filter ?src candidates = - let evd = Sigma.to_evar_map evd in let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in - Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) + 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 496ec5bc43..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 -> - ?src:Evar_kinds.t Loc.located -> 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/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 29bb1ef397..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 = [] } @@ -1012,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 @@ -1048,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 @@ -1066,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 -> @@ -1091,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 @@ -1156,8 +1115,6 @@ module Goal = struct (* compatibility *) let goal { self=self } = self - let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t) - end @@ -1281,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 |