aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/command.ml13
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/metasyntax.ml32
-rw-r--r--vernac/metasyntax.mli11
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml64
-rw-r--r--vernac/vernacentries.mli16
8 files changed, 92 insertions, 50 deletions
diff --git a/vernac/command.ml b/vernac/command.ml
index a1a87d54e..f58ed065c 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function
let (_, c) = redfun env sigma c in
EConstr.Unsafe.to_constr c
in
- { ce with const_entry_body = Future.chain ~pure:true proof_out
+ { ce with const_entry_body = Future.chain proof_out
(fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
let warn_implicits_in_term =
@@ -550,13 +550,12 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in
- let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
let constructors =
Metasyntax.with_syntax_protection (fun () ->
(* Temporary declaration of notations and scopes *)
- List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations;
+ List.iter (Metasyntax.set_notation_for_interpretation env_params impls) notations;
(* Interpret the constructor types *)
List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl)
() in
@@ -708,7 +707,7 @@ let do_mutual_inductive indl cum poly prv finite =
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations mie pl impls);
(* Declare the possible notations of inductive types *)
- List.iter Metasyntax.add_notation_interpretation ntns;
+ List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
(* Declare the coercions *)
List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes;
(* If positivity is assumed declares itself as unsafe. *)
@@ -1110,7 +1109,7 @@ let interp_recursive isfix fixl notations =
(* Interp bodies with rollback because temp use of notations/implicit *)
let fixdefs =
Metasyntax.with_syntax_protection (fun () ->
- List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
+ List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations;
List.map4
(fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls))
fixctximpenvs fixctxs fixl fixccls)
@@ -1176,7 +1175,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
fixpoint_message (Some indexes) fixnames;
end;
(* Declare notations *)
- List.iter Metasyntax.add_notation_interpretation ntns
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
if List.exists Option.is_empty fixdefs then
@@ -1207,7 +1206,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
cofixpoint_message fixnames
end;
(* Declare notations *)
- List.iter Metasyntax.add_notation_interpretation ntns
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
let extract_decreasing_argument limit = function
| (na,CStructRec) -> na
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d45665dd4..9ab89c883 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function
(* Try all combinations... not optimal *)
let env = Global.env() in
{ const with const_entry_body =
- Future.chain ~pure:true const.const_entry_body
+ Future.chain const.const_entry_body
(fun ((body, ctx), eff) ->
match kind_of_term body with
| Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index b2d48bb2f..9376afa8c 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1318,7 +1318,7 @@ let to_map l =
let fold accu (x, v) = Id.Map.add x v accu in
List.fold_left fold Id.Map.empty l
-let add_notation_in_scope local df c mods scope =
+let add_notation_in_scope local df env c mods scope =
let open SynData in
let sd = compute_syntax_data df mods in
(* Prepare the interpretation *)
@@ -1329,7 +1329,7 @@ let add_notation_in_scope local df c mods scope =
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map sd.recvars;
} in
- let (acvars, ac, reversible) = interp_notation_constr nenv c in
+ let (acvars, ac, reversible) = interp_notation_constr env nenv c in
let interp = make_interpretation_vars sd.recvars acvars in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
let onlyparse = is_not_printable sd.only_parsing (not reversible) ac in
@@ -1349,7 +1349,7 @@ let add_notation_in_scope local df c mods scope =
Lib.add_anonymous_leaf (inNotation notation);
sd.info
-let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
+let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
let dfs = split_notation_string df in
let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
@@ -1368,7 +1368,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map recvars;
} in
- let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in
+ let (acvars, ac, reversible) = interp_notation_constr env ~impls nenv c in
let interp = make_interpretation_vars recvars acvars in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
let onlyparse = is_not_printable onlyparse (not reversible) ac in
@@ -1395,33 +1395,33 @@ let add_syntax_extension local ((loc,df),mods) = let open SynData in
(* Notations with only interpretation *)
-let add_notation_interpretation ((loc,df),c,sc) =
- let df' = add_notation_interpretation_core false df c sc false false None in
+let add_notation_interpretation env ((loc,df),c,sc) =
+ let df' = add_notation_interpretation_core false df env c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
-let set_notation_for_interpretation impls ((_,df),c,sc) =
+let set_notation_for_interpretation env impls ((_,df),c,sc) =
(try ignore
- (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
+ (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ());
with NoSyntaxRule ->
user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
(* Main entry point *)
-let add_notation local c ((loc,df),modifiers) sc =
+let add_notation local env c ((loc,df),modifiers) sc =
let df' =
if no_syntax_modifiers modifiers then
(* No syntax data: try to rely on a previously declared rule *)
let onlyparse = is_only_parsing modifiers in
let onlyprint = is_only_printing modifiers in
let compat = get_compat_version modifiers in
- try add_notation_interpretation_core local df c sc onlyparse onlyprint compat
+ try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat
with NoSyntaxRule ->
(* Try to determine a default syntax rule *)
- add_notation_in_scope local df c modifiers sc
+ add_notation_in_scope local df env c modifiers sc
else
(* Declare both syntax and interpretation *)
- add_notation_in_scope local df c modifiers sc
+ add_notation_in_scope local df env c modifiers sc
in
Dumpglob.dump_notation (loc,df') sc true
@@ -1436,13 +1436,13 @@ let add_notation_extra_printing_rule df k v =
let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None)
-let add_infix local ((loc,inf),modifiers) pr sc =
+let add_infix local env ((loc,inf),modifiers) pr sc =
check_infix_modifiers modifiers;
(* check the precedence *)
let metas = [inject_var "x"; inject_var "y"] in
let c = mkAppC (pr,metas) in
let df = "x "^(quote_notation_token inf)^" y" in
- add_notation local c ((loc,df),modifiers) sc
+ add_notation local env c ((loc,df),modifiers) sc
(**********************************************************************)
(* Delimiters and classes bound to scopes *)
@@ -1498,7 +1498,7 @@ let try_interp_name_alias = function
| [], { CAst.v = CRef (ref,_) } -> intern_reference ref
| _ -> raise Not_found
-let add_syntactic_definition ident (vars,c) local onlyparse =
+let add_syntactic_definition env ident (vars,c) local onlyparse =
let nonprintable = ref false in
let vars,pat =
try [], NRef (try_interp_name_alias (vars,c))
@@ -1509,7 +1509,7 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
ninterp_var_type = i_vars;
ninterp_rec_vars = Id.Map.empty;
} in
- let nvars, pat, reversible = interp_notation_constr nenv c in
+ let nvars, pat, reversible = interp_notation_constr env nenv c in
let () = nonprintable := not reversible in
let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
List.map map vars, pat
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 9cd00cbcb..b3049f1b7 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -11,15 +11,16 @@ open Vernacexpr
open Notation
open Constrexpr
open Notation_term
+open Environ
val add_token_obj : string -> unit
(** Adding a (constr) notation in the environment*)
-val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
+val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) ->
constr_expr -> scope_name option -> unit
-val add_notation : locality_flag -> constr_expr ->
+val add_notation : locality_flag -> env -> constr_expr ->
(lstring * syntax_modifier list) -> scope_name option -> unit
val add_notation_extra_printing_rule : string -> string -> string -> unit
@@ -33,11 +34,11 @@ val add_class_scope : scope_name -> scope_class list -> unit
(** Add only the interpretation of a notation that already has pa/pp rules *)
val add_notation_interpretation :
- (lstring * constr_expr * scope_name option) -> unit
+ env -> (lstring * constr_expr * scope_name option) -> unit
(** Add a notation interpretation for supporting the "where" clause *)
-val set_notation_for_interpretation : Constrintern.internalization_env ->
+val set_notation_for_interpretation : env -> Constrintern.internalization_env ->
(lstring * constr_expr * scope_name option) -> unit
(** Add only the parsing/printing rule of a notation *)
@@ -47,7 +48,7 @@ val add_syntax_extension :
(** Add a syntactic definition (as in "Notation f := ...") *)
-val add_syntactic_definition : Id.t -> Id.t list * constr_expr ->
+val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
bool -> Flags.compat_version option -> unit
(** Print the Camlp4 state of a grammar *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 81218308f..785c842ba 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -556,7 +556,7 @@ let declare_mutual_definition l =
let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
- List.iter Metasyntax.add_notation_interpretation first.prg_notations;
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
diff --git a/vernac/record.ml b/vernac/record.ml
index 18e7796ca..9a8657c3c 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -72,7 +72,7 @@ let interp_fields_evars env evars impls_env nots l =
| None -> LocalAssum (i,t')
| Some b' -> LocalDef (i,b',t')
in
- List.iter (Metasyntax.set_notation_for_interpretation impls) no;
+ List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
(EConstr.push_rel d env, impl :: uimpls, d::params, impls))
(env, [], [], impls_env) nots l
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 66427b709..e08cb8387 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -430,11 +430,11 @@ let vernac_arguments_scope locality r scl =
let vernac_infix locality local =
let local = enforce_module_locality locality local in
- Metasyntax.add_infix local
+ Metasyntax.add_infix local (Global.env())
let vernac_notation locality local =
let local = enforce_module_locality locality local in
- Metasyntax.add_notation local
+ Metasyntax.add_notation local (Global.env())
(***********)
(* Gallina *)
@@ -953,7 +953,7 @@ let vernac_hints locality poly local lb h =
let vernac_syntactic_definition locality lid x local y =
Dumpglob.dump_definition lid false "syndef";
let local = enforce_module_locality locality local in
- Metasyntax.add_syntactic_definition (snd lid) x local y
+ Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y
let vernac_declare_implicits locality r l =
let local = make_section_locality locality in
@@ -2148,23 +2148,48 @@ let locate_if_not_already ?loc (e, info) =
exception HasNotFailed
exception HasFailed of Pp.t
-let with_fail b f =
- if not b then f ()
+type interp_state = { (* TODO: inline records in OCaml 4.03 *)
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.state; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
+}
+
+let s_cache = ref (States.freeze ~marshallable:`No)
+let s_proof = ref (Proof_global.freeze ~marshallable:`No)
+
+let invalidate_cache () =
+ s_cache := Obj.magic 0;
+ s_proof := Obj.magic 0
+
+let freeze_interp_state marshallable =
+ { system = (s_cache := States.freeze ~marshallable; !s_cache);
+ proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
+ shallow = marshallable = `Shallow }
+
+let unfreeze_interp_state { system; proof } =
+ if (!s_cache != system) then (s_cache := system; States.unfreeze system);
+ if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof)
+
+(* XXX STATE: this type hints that restoring the state should be the
+ caller's responsibility *)
+let with_fail st b f =
+ if not b
+ then f ()
else begin try
(* If the command actually works, ignore its effects on the state.
* Note that error has to be printed in the right state, hence
* within the purified function *)
- Future.purify
- (fun v ->
- try f v; raise HasNotFailed
- with
- | HasNotFailed as e -> raise e
- | e ->
- let e = CErrors.push e in
- raise (HasFailed (CErrors.iprint
- (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))))
- ()
+ try f (); raise HasNotFailed
+ with
+ | HasNotFailed as e -> raise e
+ | e ->
+ let e = CErrors.push e in
+ raise (HasFailed (CErrors.iprint
+ (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
with e when CErrors.noncritical e ->
+ (* Restore the previous state XXX Careful here with the cache! *)
+ invalidate_cache ();
+ unfreeze_interp_state st;
let (e, _) = CErrors.push e in
match e with
| HasNotFailed ->
@@ -2175,7 +2200,7 @@ let with_fail b f =
| _ -> assert false
end
-let interp ?(verbosely=true) ?proof (loc,c) =
+let interp ?(verbosely=true) ?proof st (loc,c) =
let orig_program_mode = Flags.is_program_mode () in
let rec aux ?locality ?polymorphism isprogcmd = function
@@ -2188,7 +2213,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
| VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
| VernacLocal _ -> user_err Pp.(str "Locality specified twice")
| VernacFail v ->
- with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
+ with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v)
| VernacTimeout (n,v) ->
current_timeout := Some n;
aux ?locality ?polymorphism isprogcmd v
@@ -2227,3 +2252,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
in
if verbosely then Flags.verbosely (aux false) c
else aux false c
+
+let interp ?verbosely ?proof st cmd =
+ unfreeze_interp_state st;
+ interp ?verbosely ?proof st cmd;
+ freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index a09011d24..56635c801 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -14,11 +14,21 @@ val dump_global : Libnames.reference or_by_notation -> unit
val vernac_require :
Libnames.reference option -> bool option -> Libnames.reference list -> unit
+type interp_state = { (* TODO: inline records in OCaml 4.03 *)
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.state; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
+}
+
+val freeze_interp_state : Summary.marshallable -> interp_state
+val unfreeze_interp_state : interp_state -> unit
+
(** The main interpretation function of vernacular expressions *)
val interp :
?verbosely:bool ->
?proof:Proof_global.closed_proof ->
- Vernacexpr.vernac_expr Loc.located -> unit
+ interp_state ->
+ Vernacexpr.vernac_expr Loc.located -> interp_state
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
@@ -28,7 +38,9 @@ val interp :
val make_cases : string -> string list list
-val with_fail : bool -> (unit -> unit) -> unit
+(* XXX STATE: this type hints that restoring the state should be the
+ caller's responsibility *)
+val with_fail : interp_state -> bool -> (unit -> unit) -> unit
val command_focus : unit Proof.focus_kind
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-29 11:49:23 +0000