From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 31 Mar 2018 17:43:18 +0200 Subject: Evar maps contain econstrs. We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr. --- proofs/clenv.ml | 23 +++++++++-------------- proofs/evar_refiner.ml | 8 +++----- proofs/goal.ml | 9 +++++---- proofs/pfedit.ml | 2 +- proofs/proof_global.ml | 2 +- proofs/refine.ml | 16 ++++++++-------- 6 files changed, 27 insertions(+), 33 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 03ff580ad..aeaf16723 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -62,9 +62,6 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause -let mk_freelisted c = - map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c)) - let clenv_push_prod cl = let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in let rec clrec typ = match EConstr.kind cl.evd typ with @@ -73,7 +70,7 @@ let clenv_push_prod cl = let mv = new_meta () in let dep = not (noccurn (cl_sigma cl) 1 u) in let na' = if dep then na else Anonymous in - let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in + let e' = meta_declare mv t ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in let def = applist (cl.templval.rebus,[mkMeta mv]) in { templval = mk_freelisted def; @@ -107,8 +104,7 @@ let clenv_environments evd bound t = let mv = new_meta () in let dep = not (noccurn evd 1 t2) in let na' = if dep then na else Anonymous in - let t1 = EConstr.Unsafe.to_constr t1 in - let e' = meta_declare mv t1 ~name:na' e in + let e' = meta_declare mv t1 ~name:na' e in clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) t2) else t2) | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t) @@ -167,13 +163,13 @@ let clenv_assign mv rhs clenv = user_err Pp.(str "clenv_assign: circularity in unification"); try if meta_defined clenv.evd mv then - if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then + if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then error_incompatible_inst clenv mv else clenv else let st = (Conv,TypeNotProcessed) in - {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd} + {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} with Not_found -> user_err Pp.(str "clenv_assign: undefined meta") @@ -218,7 +214,7 @@ let clenv_assign mv rhs clenv = *) let clenv_metas_in_type_of_meta evd mv = - (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas + (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right @@ -288,11 +284,11 @@ let adjust_meta_source evd mv = function in situations like "ex_intro (fun x => P) ?ev p" *) let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) -> if Metaset.mem mv t.freemetas then - let f,l = decompose_app evd (EConstr.of_constr t.rebus) in + let f,l = decompose_app evd t.rebus in match EConstr.kind evd f with | Meta mv'' -> (match meta_opt_fvalue evd mv'' with - | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l + | Some (c,_) -> match_name c.rebus l | None -> None) | _ -> None else None in @@ -502,7 +498,6 @@ let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in - let c = EConstr.Unsafe.to_constr c in { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } let clenv_match_args bl clenv = @@ -515,7 +510,7 @@ let clenv_match_args bl clenv = (fun clenv {CAst.loc;v=(b,c)} -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then - if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv + if EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv else error_already_defined b else clenv_assign_binding clenv k c) @@ -677,7 +672,7 @@ let define_with_type sigma env ev c = let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in let (ev, _) = destEvar sigma ev in - let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in + let sigma = Evd.define ev j.Environ.uj_val sigma in sigma let solve_evar_clause env sigma hyp_only clause = function diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0d197c92c..c80f370fd 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,8 +25,6 @@ open Ltac_pretype type glob_constr_ltac_closure = ltac_var_map * glob_constr let depends_on_evar sigma evk _ (pbty,_,t1,t2) = - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in try Evar.equal (head_evar sigma t1) evk with NoHeadEvar -> try Evar.equal (head_evar sigma t2) evk @@ -35,12 +33,12 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) = let define_and_solve_constraints evk c env evd = if Termops.occur_evar evd evk c then Pretype_errors.error_occur_check env evd evk c; - let evd = define evk (EConstr.Unsafe.to_constr c) evd in + let evd = define evk c evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in match List.fold_left (fun p (pbty,env,t1,t2) -> match p with - | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) + | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 | UnifFailure _ as x -> x) (Success evd) pbs with @@ -59,7 +57,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = Pretyping.fail_evar = false; Pretyping.expand_evars = true } in try Pretyping.understand_ltac flags - env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc + env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when CErrors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err ?loc diff --git a/proofs/goal.ml b/proofs/goal.ml index 6912db364..1440d1636 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -48,7 +48,7 @@ module V82 = struct (* Access to ".evar_concl" *) let concl evars gl = let evi = Evd.find evars gl in - EConstr.of_constr evi.Evd.evar_concl + evi.Evd.evar_concl (* Access to ".evar_extra" *) let extra evars gl = @@ -61,7 +61,6 @@ module V82 = struct be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is created. *) - let concl = EConstr.Unsafe.to_constr concl in let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; @@ -86,7 +85,7 @@ module V82 = struct if not (Evarutil.occur_evar_upto sigma evk c) then () else Pretype_errors.error_occur_check Environ.empty_env sigma evk c in - Evd.define evk (EConstr.Unsafe.to_constr c) sigma + Evd.define evk c sigma (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = @@ -100,7 +99,9 @@ module V82 = struct let same_goal evars1 gl1 evars2 gl2 = let evi1 = Evd.find evars1 gl1 in let evi2 = Evd.find evars2 gl2 in - Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl && + let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in + let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in + Constr.equal c1 c2 && Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps let weak_progress glss gls = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 8725f51cd..abda04ff1 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -233,7 +233,7 @@ let apply_implicit_tactic tac = (); fun env sigma evk -> (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in (try - let c = Evarutil.nf_evars_universes sigma evi.evar_concl in + let c = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr evi.evar_concl) in let c = EConstr.of_constr c in if Evarutil.has_undefined_evars sigma c then raise Exit; let (ans, _, ctx) = diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d6c0e3341..fc7c437e6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -340,7 +340,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now have existential variables in the initial types of goals, we need to normalise them for the kernel. *) let subst_evar k = - Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in + Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in let nf = Universes.nf_evars_and_universes_opt_subst subst_evar (UState.subst universes) in let make_body = diff --git a/proofs/refine.ml b/proofs/refine.ml index 909556b1e..5a2d82977 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -15,7 +15,7 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration let extract_prefix env info = - let ctx1 = List.rev (Environ.named_context env) in + let ctx1 = List.rev (EConstr.named_context env) in let ctx2 = List.rev (Evd.evar_context info) in let rec share l1 l2 accu = match l1, l2 with | d1 :: l1, d2 :: l2 -> @@ -29,21 +29,21 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = EConstr.of_constr (NamedDecl.get_type decl) in + let t = NamedDecl.get_type decl in let evdref = ref sigma in let _ = Typing.e_sort_of env evdref t in let () = match decl with | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t + | LocalDef (_,body,_) -> Typing.e_check env evdref body t in - (!evdref, Environ.push_named decl env) + (!evdref, EConstr.push_named decl env) in let (common, changed) = extract_prefix env info in - let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in + let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in + let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in !evdref let typecheck_proof c concl env sigma = @@ -106,7 +106,6 @@ let generic_refine ~typecheck f gl = let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in (** Proceed to the refinement *) - let c = EConstr.Unsafe.to_constr c in let sigma = match Proofview.Unsafe.advance sigma self with | None -> (** Nothing to do, the goal has been solved by side-effect *) @@ -124,7 +123,8 @@ let generic_refine ~typecheck f gl = (** Mark goals *) let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in - let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in + let trace () = Pp.(hov 2 (str"simple refine"++spc()++ + Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> -- cgit v1.2.3