From 954fbd3b102060ed1e2122f571a430f05a174e42 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 9 May 2017 22:14:35 +0200 Subject: Remove the Sigma (monotonous state) API. Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good. --- vernac/auto_ind_decl.ml | 40 ++++++++++++++++++++-------------------- vernac/classes.ml | 3 +-- vernac/command.ml | 9 +++------ vernac/indschemes.ml | 9 ++------- vernac/record.ml | 9 ++------- vernac/vernacentries.ml | 4 +--- 6 files changed, 29 insertions(+), 45 deletions(-) (limited to 'vernac') diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index b99ccbf4a2..9e6e5e313b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -365,7 +365,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = ))) ) in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in let sigma = Tacmach.New.project gl in let u,v = destruct_ind sigma type_of_pq @@ -397,7 +397,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; Equality.replace p q ; apply app ; Auto.default_auto] - end } + end (* used in the bool -> leib side *) let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = @@ -430,7 +430,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let rec aux l1 l2 = match (l1,l2) with | (t1::q1,t2::q2) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in let sigma = Tacmach.New.project gl in if EConstr.eq_constr sigma t1 t2 then aux q1 q2 @@ -472,7 +472,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = aux q1 q2 ] ) ) - end } + end | ([],[]) -> Proofview.tclUNIT () | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.") in @@ -581,7 +581,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -604,18 +604,18 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [ Simple.apply_in freshz (EConstr.of_constr (andb_prop())); - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in destruct_on_as (EConstr.mkVar freshz) (IntroOrPattern [[Loc.tag @@ IntroNaming (IntroIdentifier fresht); Loc.tag @@ IntroNaming (IntroIdentifier freshz)]]) - end } + end ]); (* Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto *) - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in match EConstr.kind sigma concl with @@ -635,10 +635,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") ) | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") - end } + end ] - end } + end let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -725,7 +725,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -748,7 +748,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro())); simplest_split ;Auto.default_auto ] ); - Proofview.Goal.enter { enter = begin fun gls -> + Proofview.Goal.enter begin fun gls -> let concl = Proofview.Goal.concl gls in let sigma = Tacmach.New.project gl in (* assume the goal to be eq (eq_type ...) = true *) @@ -765,9 +765,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = ) | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") - end } + end ] - end } + end let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") @@ -873,7 +873,7 @@ let compute_dec_tact ind lnamesparrec nparrec = let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -904,7 +904,7 @@ let compute_dec_tact ind lnamesparrec nparrec = )) (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto); - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let freshH2 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [ (* left *) @@ -916,7 +916,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ; (*right *) - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; @@ -938,11 +938,11 @@ let compute_dec_tact ind lnamesparrec nparrec = true; Equality.discr_tac false None ] - end } + end ] - end } + end ] - end } + end let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in diff --git a/vernac/classes.ml b/vernac/classes.ml index 004083dcf9..dc5ce1a537 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -20,7 +20,6 @@ open Libnames open Globnames open Constrintern open Constrexpr -open Sigma.Notations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -342,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine { run = fun evm -> Sigma (EConstr.of_constr (Option.get term), evm, Sigma.refl) }; + Refine.refine (fun evm -> (evm,EConstr.of_constr (Option.get term))); Proofview.Unsafe.tclNEWGOALS gls; Tactics.New.reduce_after_refine; ] diff --git a/vernac/command.ml b/vernac/command.ml index ad84c17b7f..b1425d7034 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -35,7 +35,6 @@ open Evarconv open Indschemes open Misctypes open Vernacexpr -open Sigma.Notations open Context.Rel.Declaration open Entries @@ -78,8 +77,7 @@ let red_constant_entry n ce sigma = function let env = Global.env () in let (redfun, _) = reduction_of_red_expr env red in let redfun env sigma c = - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (c, _, _) = redfun.e_redfun env sigma c in + let (_, c) = redfun env sigma c in EConstr.Unsafe.to_constr c in { ce with const_entry_body = Future.chain ~pure:true proof_out @@ -908,9 +906,8 @@ let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.coq_reference "Command" dir s let init_constant dir s evdref = - let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map !evdref) - (Coqlib.coq_reference "Command" dir s) - in evdref := Sigma.to_evar_map sigma; c + let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s) + in evdref := sigma; c let make_ref l s = init_reference l s let fix_proto = init_constant tactics_module "fix_proto" diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index a678d20bba..c2c27eb78e 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -453,13 +453,8 @@ let fold_left' f = function [] -> invalid_arg "fold_left'" | hd :: tl -> List.fold_left f hd tl -let new_global sigma gr = - let open Sigma in - let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr - in Sigma.to_evar_map sigma, c - -let mk_coq_and sigma = new_global sigma (Coqlib.build_coq_and ()) -let mk_coq_conj sigma = new_global sigma (Coqlib.build_coq_conj ()) +let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ()) +let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ()) let build_combined_scheme env schemes = let evdref = ref (Evd.from_env env) in diff --git a/vernac/record.ml b/vernac/record.ml index 8cde88dc9c..2400fa6814 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -24,7 +24,6 @@ open Type_errors open Constrexpr open Constrexpr_ops open Goptions -open Sigma.Notations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -365,15 +364,11 @@ let structure_signature ctx = match l with [] -> Evd.empty | [decl] -> let env = Environ.empty_named_context_val in - let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in - let evm = Sigma.to_evar_map evm in + let (evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in evm | decl::tl -> let env = Environ.empty_named_context_val in - let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in - let evm = Sigma.to_evar_map evm in + let (evm, ev) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in let new_tl = Util.List.map_i (fun pos decl -> RelDecl.map_type (fun t -> EConstr.Unsafe.to_constr (Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t))) decl) 1 tl in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c6ec89c5e6..1332a7052b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -31,7 +31,6 @@ open Redexpr open Lemmas open Misctypes open Locality -open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -1550,8 +1549,7 @@ let vernac_check_may_eval ?loc redexp glopt rc = let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = let (redfun, _) = reduction_of_red_expr env r_interp in - let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in + let (_, c) = redfun env evm c in c in Feedback.msg_notice (print_eval redfun env sigma' rc j) -- cgit v1.2.3