From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- proofs/clenv.ml | 14 ++++++------- proofs/clenvtac.ml | 6 +++--- proofs/evar_refiner.ml | 2 +- proofs/logic.ml | 56 +++++++++++++++++++++++++------------------------- proofs/logic.mli | 2 +- proofs/redexpr.ml | 2 +- 6 files changed, 41 insertions(+), 41 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index fad656223a..34bc830970 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -77,7 +77,7 @@ let clenv_push_prod cl = | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> let mv = new_meta () in - let dep = dependent (mkRel 1) u in + let dep = not (EConstr.Vars.noccurn (cl_sigma cl) 1 (EConstr.of_constr u)) in let na' = if dep then na else Anonymous in let e' = meta_declare mv t ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in @@ -332,7 +332,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let ty = clenv_meta_type clenv mv in (* Postpone the evar-ization if dependent on another meta *) (* This assumes no cycle in the dependencies - is it correct ? *) - if occur_meta ty then fold clenv (mvs@[mv]) + if occur_meta clenv.evd (EConstr.of_constr ty) then fold clenv (mvs@[mv]) else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in @@ -404,7 +404,7 @@ type arg_bindings = constr explicit_bindings * of cval, ctyp. *) let clenv_independent clenv = - let mvs = collect_metas (clenv_value clenv) in + let mvs = collect_metas clenv.evd (EConstr.of_constr (clenv_value clenv)) in let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in List.filter (fun mv -> not (Metaset.mem mv deps)) mvs @@ -522,7 +522,7 @@ let clenv_match_args bl clenv = exception NoSuchBinding let clenv_constrain_last_binding c clenv = - let all_mvs = collect_metas clenv.templval.rebus in + let all_mvs = collect_metas clenv.evd (EConstr.of_constr clenv.templval.rebus) in let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in clenv_assign_binding clenv k c @@ -612,7 +612,7 @@ let make_evar_clause env sigma ?len t = let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in let sigma = Sigma.to_evar_map sigma in - let dep = dependent (mkRel 1) t2 in + let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in let hole = { hole_evar = ev; hole_type = t1; @@ -682,9 +682,9 @@ let solve_evar_clause env sigma hyp_only clause = function if h.hole_deps then (** Some subsequent term uses the hole *) let (ev, _) = destEvar h.hole_evar in - let is_dep hole = occur_evar ev hole.hole_type in + let is_dep hole = occur_evar sigma ev (EConstr.of_constr hole.hole_type) in let in_hyp = List.exists is_dep holes in - let in_ccl = occur_evar ev clause.cl_concl in + let in_ccl = occur_evar sigma ev (EConstr.of_constr clause.cl_concl) in let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in let h = { h with hole_deps = dep } in h :: holes diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 98b5bc8b05..d8a20e08bc 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -33,12 +33,12 @@ let clenv_cast_meta clenv = | _ -> map_constr crec u and crec_hd u = - match kind_of_term (strip_outer_cast u) with + match kind_of_term (strip_outer_cast clenv.evd (EConstr.of_constr u)) with | Meta mv -> (try let b = Typing.meta_type clenv.evd mv in - assert (not (occur_meta b)); - if occur_meta b then u + assert (not (occur_meta clenv.evd (EConstr.of_constr b))); + if occur_meta clenv.evd (EConstr.of_constr b) then u else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index ff0df9179f..d4b308bbeb 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,7 +25,7 @@ let depends_on_evar evk _ (pbty,_,t1,t2) = with NoHeadEvar -> false let define_and_solve_constraints evk c env evd = - if Termops.occur_evar evk c then + if Termops.occur_evar evd evk (EConstr.of_constr c) then Pretype_errors.error_occur_check env evd evk c; let evd = define evk c evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in diff --git a/proofs/logic.ml b/proofs/logic.ml index 44c6294841..29f295682c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -138,12 +138,12 @@ let find_q x (m,q) = else find (Id.Set.union l accs) (i::acc) itl in find Id.Set.empty [] q -let occur_vars_in_decl env hyps d = +let occur_vars_in_decl env sigma hyps d = if Id.Set.is_empty hyps then false else - let ohyps = global_vars_set_of_decl env d in + let ohyps = global_vars_set_of_decl env sigma d in Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps -let reorder_context env sign ord = +let reorder_context env sigma sign ord = let ords = List.fold_right Id.Set.add ord Id.Set.empty in if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then error "Order list has duplicates"; @@ -152,13 +152,13 @@ let reorder_context env sign ord = | [] -> List.rev ctxt_tail @ ctxt_head | top::ord' when mem_q top moved_hyps -> let ((d,h),mh) = find_q top moved_hyps in - if occur_vars_in_decl env h d then + if occur_vars_in_decl env sigma h d then user_err ~hdr:"reorder_context" (str "Cannot move declaration " ++ pr_id top ++ spc() ++ str "before " ++ pr_sequence pr_id (Id.Set.elements (Id.Set.inter h - (global_vars_set_of_decl env d)))); + (global_vars_set_of_decl env sigma d)))); step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with @@ -173,16 +173,16 @@ let reorder_context env sign ord = ctxt (push_val x moved_hyps) (d::ctxt_tail)) in step ord ords sign mt_q [] -let reorder_val_context env sign ord = - val_of_named_context (reorder_context env (named_context_of_val sign) ord) +let reorder_val_context env sigma sign ord = + val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) -let check_decl_position env sign d = +let check_decl_position env sigma sign d = let x = NamedDecl.get_id d in - let needed = global_vars_set_of_decl env d in - let deps = dependency_closure env (named_context_of_val sign) needed in + let needed = global_vars_set_of_decl env sigma d in + let deps = dependency_closure env sigma (named_context_of_val sign) needed in if Id.List.mem x deps then user_err ~hdr:"Logic.check_decl_position" (str "Cannot create self-referring hypothesis " ++ pr_id x); @@ -233,12 +233,12 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp toleft (left,declfrom,right) hto = +let move_hyp sigma toleft (left,declfrom,right) hto = let env = Global.env() in let test_dep d d2 = if toleft - then occur_var_in_decl env (NamedDecl.get_id d2) d - else occur_var_in_decl env (NamedDecl.get_id d) d2 + then occur_var_in_decl env sigma (NamedDecl.get_id d2) d + else occur_var_in_decl env sigma (NamedDecl.get_id d) d2 in let rec moverec first middle = function | [] -> @@ -278,10 +278,10 @@ let move_hyp toleft (left,declfrom,right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let move_hyp_in_named_context hfrom hto sign = +let move_hyp_in_named_context sigma hfrom hto sign = let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in - move_hyp toleft (left,declfrom,right) hto + move_hyp sigma toleft (left,declfrom,right) hto (**********************************************************************) @@ -320,10 +320,10 @@ let check_conv_leq_goal env sigma arg ty conclty = else sigma exception Stop of constr list -let meta_free_prefix a = +let meta_free_prefix sigma a = try let _ = Array.fold_left (fun acc a -> - if occur_meta a then raise (Stop acc) + if occur_meta sigma (EConstr.of_constr a) then raise (Stop acc) else a :: acc) [] a in a with Stop acc -> Array.rev_of_list acc @@ -338,7 +338,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in - if (not !check) && not (occur_meta trm) then + if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) @@ -346,7 +346,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind_of_term trm with | Meta _ -> let conclty = nf_betaiota sigma conclty in - if !check && occur_meta conclty then + if !check && occur_meta sigma (EConstr.of_constr conclty) then raise (RefinerError (MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in gl::goalacc, conclty, sigma, ev @@ -367,10 +367,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env f then + if is_template_polymorphic env sigma (EConstr.of_constr f) then let ty = (* Template sort-polymorphism of definition and inductive types *) - let firstmeta = Array.findi (fun i x -> occur_meta x) l in + let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in type_of_global_reference_knowing_parameters env sigma f args in @@ -406,7 +406,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = (acc'',conclty',sigma, ans) | _ -> - if occur_meta trm then + if occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refiner called with a meta in non app/case subterm"); let t'ty = goal_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in @@ -432,9 +432,9 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env f + if is_template_polymorphic env sigma (EConstr.of_constr f) then - let l' = meta_free_prefix l in + let l' = meta_free_prefix sigma l in (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) else mk_hdgoals sigma goal goalacc f in @@ -464,7 +464,7 @@ and mk_hdgoals sigma goal goalacc trm = (acc',ty,sigma,c) | _ -> - if !check && occur_meta trm then + if !check && occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refine called with a dependent meta"); goalacc, goal_type_of env sigma trm, sigma, trm @@ -511,9 +511,9 @@ let convert_hyp check sign sigma d = if check && not (Option.equal (is_conv env sigma) b c) then user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the body of "++ pr_id id ++ str "."); - if check then reorder := check_decl_position env sign d; + if check then reorder := check_decl_position env sigma sign d; d) in - reorder_val_context env sign' !reorder + reorder_val_context env sigma sign' !reorder @@ -537,7 +537,7 @@ let prim_refiner r sigma goal = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp false ([], LocalAssum (id,t),named_context_of_val sign) + move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign) nexthyp, t,cl,sigma else diff --git a/proofs/logic.mli b/proofs/logic.mli index 0dba9ef1ee..8c8a01cada 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -57,5 +57,5 @@ val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> Context.Named.Declaration.t -> Environ.named_context_val -val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 34443b93da..a442a5e63a 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -25,7 +25,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = let ctyp = Retyping.get_type_of env sigma c in - if Termops.occur_meta_or_existential c then + if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then error "vm_compute does not support existential variables."; Vnorm.cbv_vm env c ctyp -- cgit v1.2.3 From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- proofs/clenv.ml | 10 +++++----- proofs/logic.ml | 16 ++++++++-------- proofs/redexpr.ml | 7 +++++-- proofs/tacmach.ml | 24 ++++++++++++++---------- proofs/tacmach.mli | 6 +++--- 5 files changed, 35 insertions(+), 28 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 34bc830970..d64cd9fffd 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -72,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause let clenv_push_prod cl = - let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in + let typ = whd_all (cl_env cl) (cl_sigma cl) (EConstr.of_constr (clenv_type cl)) in let rec clrec typ = match kind_of_term typ with | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> @@ -264,7 +264,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = let concl = Goal.V82.concl clenv.evd (sig_it gl) in - if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then + if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) else @@ -482,7 +482,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then + if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr u)))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else @@ -498,8 +498,8 @@ let clenv_unify_binding_type clenv c t u = TypeNotProcessed, clenv, c 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.evd (clenv_get_type_of clenv c) in + let k_typ = clenv_hnf_constr clenv (EConstr.of_constr (clenv_meta_type clenv k)) in + let c_typ = nf_betaiota clenv.evd (EConstr.of_constr (clenv_get_type_of clenv c)) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } diff --git a/proofs/logic.ml b/proofs/logic.ml index 29f295682c..0fa1930656 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -345,7 +345,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = else match kind_of_term trm with | Meta _ -> - let conclty = nf_betaiota sigma conclty in + let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in if !check && occur_meta sigma (EConstr.of_constr conclty) then raise (RefinerError (MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in @@ -423,7 +423,7 @@ and mk_hdgoals sigma goal goalacc trm = match kind_of_term trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in + let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> @@ -470,7 +470,7 @@ and mk_hdgoals sigma goal goalacc trm = and mk_arggoals sigma goal goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = - let t = whd_all (Goal.V82.env sigma goal) sigma funty in + let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in let rec collapse t = match kind_of_term t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) | _ -> t @@ -491,21 +491,21 @@ and mk_casegoals sigma goal goalacc p c = let indspec = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals") in - let (lbrty,conclty) = type_case_branches_with_names env indspec p c in + let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in - let b = NamedDecl.get_value d in + let b = Option.map EConstr.of_constr (NamedDecl.get_value d) in let env = Global.env() in let reorder = ref [] in let sign' = apply_to_hyp check sign id (fun _ d' _ -> - let c = NamedDecl.get_value d' in + let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in let env = Global.env_of_context sign in - if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then + if check && not (is_conv env sigma (EConstr.of_constr (NamedDecl.get_type d)) (EConstr.of_constr (NamedDecl.get_type d'))) then user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then @@ -532,7 +532,7 @@ let prim_refiner r sigma goal = (* Logical rules *) | Cut (b,replace,id,t) -> (* if !check && not (Retyping.get_sort_of env sigma t) then*) - let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in + let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in let sign,t,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index a442a5e63a..40a8077a72 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,10 +24,11 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = + let c = EConstr.Unsafe.to_constr c in let ctyp = Retyping.get_type_of env sigma c in if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then error "vm_compute does not support existential variables."; - Vnorm.cbv_vm env c ctyp + Vnorm.cbv_vm env sigma c ctyp let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" @@ -39,13 +40,15 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else + let c = EConstr.Unsafe.to_constr c in let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty)) - in Reductionops.Stack.zip ~refold:true state + in + EConstr.Unsafe.to_constr (Reductionops.Stack.zip ~refold:true sigma state) let strong_cbn flags = strong (whd_cbn flags) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index e41fb94cce..09f5246ab9 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -77,26 +77,27 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in let sigma = Sigma.Unsafe.of_evar_map (project gls) in - let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in + let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma (EConstr.of_constr c) in (Sigma.to_evar_map sigma, c) let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x) let pf_reduce = pf_apply +let pf_reduce' f gl c = pf_apply f gl (EConstr.of_constr c) let pf_e_reduce = pf_apply -let pf_whd_all = pf_reduce whd_all -let pf_hnf_constr = pf_reduce hnf_constr -let pf_nf = pf_reduce simpl -let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) -let pf_compute = pf_reduce compute -let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_whd_all = pf_reduce' whd_all +let pf_hnf_constr = pf_reduce' hnf_constr +let pf_nf = pf_reduce' simpl +let pf_nf_betaiota = pf_reduce' (fun _ -> nf_betaiota) +let pf_compute = pf_reduce' compute +let pf_unfoldn ubinds = pf_reduce' (unfoldn ubinds) let pf_unsafe_type_of = pf_reduce unsafe_type_of let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of -let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV +let pf_conv_x gl = pf_apply test_conversion gl Reduction.CONV let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) @@ -158,6 +159,9 @@ module New = struct let pf_apply f gl = f (Proofview.Goal.env gl) (project gl) + let pf_reduce f gl c = + f (Proofview.Goal.env gl) (project gl) (EConstr.of_constr c) + let of_old f gl = f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } @@ -217,14 +221,14 @@ module New = struct let sigma = project gl in nf_evar sigma concl - let pf_whd_all gl t = pf_apply whd_all gl t + let pf_whd_all gl t = pf_reduce whd_all gl t let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t let pf_reduce_to_quantified_ind gl t = pf_apply reduce_to_quantified_ind gl t - let pf_hnf_constr gl t = pf_apply hnf_constr gl t + let pf_hnf_constr gl t = pf_reduce hnf_constr gl t let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 727efcf6dc..16f6f88c17 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -110,7 +110,7 @@ module New : sig val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types - val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool + val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list @@ -126,8 +126,8 @@ module New : sig val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr - val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map -- cgit v1.2.3 From 2db085e62f7797cc999518eb58983ac059763e1f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:13:08 +0100 Subject: Vnorm API using EConstr. --- proofs/redexpr.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'proofs') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 40a8077a72..348cd1bcbb 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,11 +24,8 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = - let c = EConstr.Unsafe.to_constr c in - let ctyp = Retyping.get_type_of env sigma c in - if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then - error "vm_compute does not support existential variables."; - Vnorm.cbv_vm env sigma c ctyp + let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" -- cgit v1.2.3 From 6bd193ff409b01948751525ce0f905916d7a64bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:38:35 +0100 Subject: Nativenorm API using EConstr. --- proofs/redexpr.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 348cd1bcbb..62fe2c17ca 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -37,9 +37,8 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else - let c = EConstr.Unsafe.to_constr c in - let ctyp = Retyping.get_type_of env sigma c in - Nativenorm.native_norm env sigma c ctyp + let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) let whd_cbn flags env sigma t = let (state,_) = -- cgit v1.2.3 From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:48:36 +0100 Subject: Retyping API using EConstr. --- proofs/clenv.ml | 6 +++--- proofs/logic.ml | 17 +++++++++-------- proofs/redexpr.ml | 4 ++-- proofs/refine.ml | 2 +- proofs/tacmach.ml | 4 ++-- 5 files changed, 17 insertions(+), 16 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d64cd9fffd..f4ac094b80 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -67,7 +67,7 @@ let refresh_undefined_univs clenv = let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t -let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c +let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) (EConstr.of_constr c) exception NotExtensibleClause @@ -667,8 +667,8 @@ let evar_of_binder holes = function user_err (str "No such binder.") let define_with_type sigma env ev c = - let t = Retyping.get_type_of env sigma ev in - let ty = Retyping.get_type_of env sigma c in + let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in let (ev, _) = destEvar ev in diff --git a/proofs/logic.ml b/proofs/logic.ml index 0fa1930656..2df626e1c8 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -319,18 +319,19 @@ let check_conv_leq_goal env sigma arg ty conclty = else raise (RefinerError (BadType (arg,ty,conclty))) else sigma -exception Stop of constr list +exception Stop of EConstr.t list let meta_free_prefix sigma a = try + let a = Array.map EConstr.of_constr a in let _ = Array.fold_left (fun acc a -> - if occur_meta sigma (EConstr.of_constr a) then raise (Stop acc) + if occur_meta sigma a then raise (Stop acc) else a :: acc) [] a in a with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = if !check then unsafe_type_of env sigma c - else Retyping.get_type_of env sigma c + else Retyping.get_type_of env sigma (EConstr.of_constr c) let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in @@ -339,7 +340,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then - let t'ty = Retyping.get_type_of env sigma trm in + let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) else @@ -372,7 +373,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = (* Template sort-polymorphism of definition and inductive types *) let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in - type_of_global_reference_knowing_parameters env sigma f args + type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) in goalacc, ty, sigma, f else @@ -386,7 +387,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Proj (p,c) -> let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in - let ty = get_type_of env sigma c in + let ty = get_type_of env sigma (EConstr.of_constr c) in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> @@ -435,7 +436,7 @@ and mk_hdgoals sigma goal goalacc trm = if is_template_polymorphic env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in - (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) + (goalacc,type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l',sigma,f) else mk_hdgoals sigma goal goalacc f in let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in @@ -460,7 +461,7 @@ and mk_hdgoals sigma goal goalacc trm = | Proj (p,c) -> let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in - let ty = get_type_of env sigma c in + let ty = get_type_of env sigma (EConstr.of_constr c) in (acc',ty,sigma,c) | _ -> diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 62fe2c17ca..19e72e697f 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,7 +24,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) let warn_native_compute_disabled = @@ -37,7 +37,7 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) let whd_cbn flags env sigma t = diff --git a/proofs/refine.ml b/proofs/refine.ml index d4920e5051..e6e3ef47dd 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -133,7 +133,7 @@ let refine ?(unsafe = true) f = (** Useful definitions *) let with_type env evd c t = - let my_type = Retyping.get_type_of env evd c in + let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in let j = Environ.make_judge c my_type in let (evd,j') = Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 09f5246ab9..b63b2ce28a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -104,7 +104,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls +let pf_hnf_type_of gls = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv @@ -230,7 +230,7 @@ module New = struct let pf_hnf_constr gl t = pf_reduce hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_all gl (pf_get_type_of gl t) + pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t)) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t -- cgit v1.2.3 From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 03:23:13 +0100 Subject: Evarconv API using EConstr. --- proofs/evar_refiner.ml | 2 +- proofs/pfedit.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index d4b308bbeb..af5fa921f7 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -32,7 +32,7 @@ let define_and_solve_constraints evk c env evd = 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 t1 t2 + | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) | UnifFailure _ as x -> x) (Success evd) pbs with diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c7f5efd5aa..67e216745d 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -232,7 +232,7 @@ let solve_by_implicit_tactic env sigma evk = 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 - if Evarutil.has_undefined_evars sigma c then raise Exit; + if Evarutil.has_undefined_evars sigma (EConstr.of_constr c) then raise Exit; let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in let sigma = Evd.set_universe_context sigma ctx in -- cgit v1.2.3 From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- proofs/clenv.ml | 2 +- proofs/logic.ml | 4 ++-- proofs/refine.ml | 8 ++++---- proofs/tacmach.ml | 8 ++++---- 4 files changed, 11 insertions(+), 11 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f4ac094b80..c2130a64a3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -29,7 +29,7 @@ open Sigma.Notations (* Abbreviations *) let pf_env = Refiner.pf_env -let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c +let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c) (******************************************************************) (* Clausal environments *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 2df626e1c8..93b31ced16 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -86,7 +86,7 @@ let apply_to_hyp check sign id f = else sign let check_typability env sigma c = - if !check then let _ = unsafe_type_of env sigma c in () + if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () (************************************************************************) (************************************************************************) @@ -330,7 +330,7 @@ let meta_free_prefix sigma a = with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = - if !check then unsafe_type_of env sigma c + if !check then unsafe_type_of env sigma (EConstr.of_constr c) else Retyping.get_type_of env sigma (EConstr.of_constr c) let rec mk_refgoals sigma goal goalacc conclty trm = diff --git a/proofs/refine.ml b/proofs/refine.ml index e6e3ef47dd..b62f0bea48 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -28,12 +28,12 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = NamedDecl.get_type decl in + let t = EConstr.of_constr (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 body t + | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t in (!evdref, Environ.push_named decl env) in @@ -42,12 +42,12 @@ let typecheck_evar ev env sigma = 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 (Evd.evar_concl info) in + let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in !evdref let typecheck_proof c concl env sigma = let evdref = ref sigma in - let () = Typing.e_check env evdref c concl in + let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in !evdref let (pr_constrv,pr_constr) = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b63b2ce28a..148f9d6752 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -93,8 +93,8 @@ let pf_nf = pf_reduce' simpl let pf_nf_betaiota = pf_reduce' (fun _ -> nf_betaiota) let pf_compute = pf_reduce' compute let pf_unfoldn ubinds = pf_reduce' (unfoldn ubinds) -let pf_unsafe_type_of = pf_reduce unsafe_type_of -let pf_type_of = pf_reduce type_of +let pf_unsafe_type_of = pf_reduce' unsafe_type_of +let pf_type_of = pf_reduce' type_of let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x gl = pf_apply test_conversion gl Reduction.CONV @@ -175,10 +175,10 @@ module New = struct let pf_concl = Proofview.Goal.concl let pf_unsafe_type_of gl t = - pf_apply unsafe_type_of gl t + pf_apply unsafe_type_of gl (EConstr.of_constr t) let pf_type_of gl t = - pf_apply type_of gl t + pf_apply type_of gl (EConstr.of_constr t) let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2 -- cgit v1.2.3 From 258c8502eafd3e078a5c7478a452432b5c046f71 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 19:59:28 +0100 Subject: Constr_matching API using EConstr. --- proofs/tacmach.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 148f9d6752..5e9c0ba8e6 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -106,8 +106,8 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls -let pf_is_matching = pf_apply Constr_matching.is_matching_conv -let pf_matches = pf_apply Constr_matching.matches_conv +let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p (EConstr.of_constr c) +let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p (EConstr.of_constr c) (********************************************) (* Definition of the most primitive tactics *) @@ -232,7 +232,7 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t)) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t + let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat (EConstr.of_constr t) let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t -- cgit v1.2.3 From b77579ac873975a15978c5a4ecf312d577746d26 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 21:59:18 +0100 Subject: Tacred API using EConstr. --- proofs/redexpr.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 19e72e697f..d4a58da326 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -200,6 +200,9 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) +let out_with_occurrences' (occs,c) = + (Locusops.occurrences_map (List.map out_arg) occs, EConstr.of_constr c) + let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl @@ -239,8 +242,8 @@ let reduction_of_red_expr env = (e_red (strong_cbn (make_flag f)), DEFAULTcast) | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) - | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) - | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) + | Fold cl -> (e_red (fold_commands (List.map EConstr.of_constr cl)),DEFAULTcast) + | Pattern lp -> (pattern_occs (List.map out_with_occurrences' lp),DEFAULTcast) | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> -- cgit v1.2.3 From e4f066238799a4598817dfeab8a044760ab670de Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 20:33:06 +0100 Subject: Coercion API using EConstr. --- proofs/clenv.ml | 2 +- proofs/refine.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index c2130a64a3..0515e41986 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -670,7 +670,7 @@ let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let j = Environ.make_judge c ty in - let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in + let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in let (ev, _) = destEvar ev in let sigma = Evd.define ev j.Environ.uj_val sigma in sigma diff --git a/proofs/refine.ml b/proofs/refine.ml index b62f0bea48..19134bfa34 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -136,7 +136,7 @@ let with_type env evd c t = let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in let j = Environ.make_judge c my_type in let (evd,j') = - Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t + Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t) in evd , j'.Environ.uj_val -- cgit v1.2.3 From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Nov 2016 19:02:40 +0100 Subject: Pretyping API using EConstr. --- proofs/clenv.ml | 4 ++-- proofs/evar_refiner.ml | 2 +- proofs/logic.ml | 2 +- proofs/pfedit.ml | 2 +- proofs/pfedit.mli | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0515e41986..68aeaef5e1 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -337,7 +337,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in let evd = Sigma.Unsafe.of_evar_map clenv.evd in - let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in + let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src (EConstr.of_constr ty) in let evd = Sigma.to_evar_map evd in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in @@ -610,7 +610,7 @@ let make_evar_clause env sigma ?len t = | Prod (na, t1, t2) -> let store = Typeclasses.set_resolvable Evd.Store.empty false in let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in + let Sigma (ev, sigma, _) = new_evar ~store env sigma (EConstr.of_constr t1) in let sigma = Sigma.to_evar_map sigma in let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in let hole = { diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index af5fa921f7..fd6528a1e1 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -51,7 +51,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 evi.evar_concl) rawc + env sigma ltac_var (Pretyping.OfType (EConstr.of_constr 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/logic.ml b/proofs/logic.ml index 93b31ced16..093d949d5d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -314,7 +314,7 @@ let check_meta_variables c = let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma ty conclty in + let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in if b then evm else raise (RefinerError (BadType (arg,ty,conclty))) else sigma diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 67e216745d..af910810ba 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -236,6 +236,6 @@ let solve_by_implicit_tactic env sigma evk = let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in let sigma = Evd.set_universe_context sigma ctx in - sigma, ans + sigma, EConstr.of_constr ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7458109fa1..807a554dfd 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr -- cgit v1.2.3 From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Nov 2016 11:39:27 +0100 Subject: Unification API using EConstr. --- proofs/clenv.ml | 8 +++++--- proofs/clenvtac.ml | 2 +- proofs/evar_refiner.ml | 2 +- proofs/goal.ml | 2 +- proofs/refine.ml | 2 +- 5 files changed, 9 insertions(+), 7 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 68aeaef5e1..2d621e97cb 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -257,7 +257,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv = { clenv with - evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 } + evd = w_unify ~flags clenv.env clenv.evd cv_pb (EConstr.of_constr t1) (EConstr.of_constr t2) } let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } @@ -482,13 +482,15 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr u)))) then + let u = EConstr.of_constr u in + if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else (* Enough information so as to try a coercion now *) try - let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in + let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd (EConstr.of_constr c) (EConstr.of_constr t) u in + let c = EConstr.Unsafe.to_constr c in TypeProcessed, { clenv with evd = evd }, c with | PretypeError (_,_,ActualTypeNotCoercible (_,_, diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index d8a20e08bc..bc5f17bf5e 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -143,7 +143,7 @@ let unify ?(flags=fail_quick_unif_flags) m = let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in let evd = clear_metas (Tacmach.New.project gl) in try - let evd' = w_unify env evd CONV ~flags m n in + let evd' = w_unify env evd CONV ~flags (EConstr.of_constr m) (EConstr.of_constr n) in Proofview.Unsafe.tclEVARSADVANCE evd' with e when CErrors.noncritical e -> Proofview.tclZERO e end } diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index fd6528a1e1..4be03af9a6 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -26,7 +26,7 @@ let depends_on_evar evk _ (pbty,_,t1,t2) = let define_and_solve_constraints evk c env evd = if Termops.occur_evar evd evk (EConstr.of_constr c) then - Pretype_errors.error_occur_check env evd evk c; + Pretype_errors.error_occur_check env evd evk (EConstr.of_constr c); let evd = define evk c evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in match diff --git a/proofs/goal.ml b/proofs/goal.ml index a141708c2b..bcb14e2d6c 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -87,7 +87,7 @@ module V82 = struct (* Check that the goal itself does not appear in the refined term *) let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () - else Pretype_errors.error_occur_check Environ.empty_env sigma evk c + else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c) in Evd.define evk c sigma diff --git a/proofs/refine.ml b/proofs/refine.ml index 19134bfa34..0ed74c9b36 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -98,7 +98,7 @@ let make_refine_enter ?(unsafe = true) f = let self = Proofview.Goal.goal gl in let _ = if not (Evarutil.occur_evar_upto sigma self c) then () - else Pretype_errors.error_occur_check env sigma self c + else Pretype_errors.error_occur_check env sigma self (EConstr.of_constr c) in (** Proceed to the refinement *) let sigma = match evkmain with -- cgit v1.2.3 From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 00:29:02 +0100 Subject: Making judgment type generic over the type of inner constrs. This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. --- proofs/clenv.ml | 6 ++++-- proofs/refine.ml | 5 ++++- proofs/refine.mli | 2 +- 3 files changed, 9 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2d621e97cb..956be88c8a 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -669,12 +669,14 @@ let evar_of_binder holes = function user_err (str "No such binder.") let define_with_type sigma env ev c = + let c = EConstr.of_constr c in let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in - let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in + let ty = Retyping.get_type_of env sigma c in + let ty = EConstr.of_constr ty in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in let (ev, _) = destEvar ev in - let sigma = Evd.define ev j.Environ.uj_val sigma in + let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in sigma let solve_evar_clause env sigma hyp_only clause = function diff --git a/proofs/refine.ml b/proofs/refine.ml index 0ed74c9b36..067764c000 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -133,7 +133,9 @@ let refine ?(unsafe = true) f = (** Useful definitions *) let with_type env evd c t = - let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in + let c = EConstr.of_constr c in + let my_type = Retyping.get_type_of env evd c in + let my_type = EConstr.of_constr my_type in let j = Environ.make_judge c my_type in let (evd,j') = Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t) @@ -147,6 +149,7 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> let f = { run = fun h -> let Sigma (c, h, p) = f.run h in let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + let c = EConstr.Unsafe.to_constr c in Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) } in refine ?unsafe f diff --git a/proofs/refine.mli b/proofs/refine.mli index 3d140f036b..4158e446cc 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -36,7 +36,7 @@ val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic (** {7 Helper functions} *) val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * Term.constr + Term.constr -> Term.types -> Evd.evar_map * EConstr.constr (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) -- cgit v1.2.3 From 7267dfafe9215c35275a39814c8af451961e997c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 17:48:47 +0100 Subject: Goal API using EConstr. --- proofs/clenv.ml | 1 + proofs/goal.ml | 8 ++++++-- proofs/goal.mli | 10 +++++----- proofs/logic.ml | 16 ++++++++++------ proofs/tacmach.ml | 4 ++-- 5 files changed, 24 insertions(+), 15 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 956be88c8a..67ed5daaa1 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -264,6 +264,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = let concl = Goal.V82.concl clenv.evd (sig_it gl) in + let concl = EConstr.Unsafe.to_constr concl in if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) diff --git a/proofs/goal.ml b/proofs/goal.ml index bcb14e2d6c..4c598ca29e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -62,6 +62,7 @@ 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.future_goals evars in let prev_principal_goal = Evd.principal_future_goal evars in let evi = { Evd.evar_hyps = hyps; @@ -78,13 +79,14 @@ module V82 = struct let evars = Sigma.to_evar_map evars in let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in - let ev = Term.mkEvar (evk,inst) in + let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in + let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) (* Instantiates a goal with an open term *) let partial_solution sigma evk c = (* Check that the goal itself does not appear in the refined term *) + let c = EConstr.Unsafe.to_constr c in let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c) @@ -158,4 +160,6 @@ module V82 = struct t ) ~init:(concl sigma gl) env + let concl sigma gl = EConstr.of_constr (concl sigma gl) + end diff --git a/proofs/goal.mli b/proofs/goal.mli index 6a79c1f451..ca6584e76d 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -38,7 +38,7 @@ module V82 : sig val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val (* Access to ".evar_concl" *) - val concl : Evd.evar_map -> goal -> Term.constr + val concl : Evd.evar_map -> goal -> EConstr.constr (* Access to ".evar_extra" *) val extra : Evd.evar_map -> goal -> Evd.Store.t @@ -48,16 +48,16 @@ module V82 : sig the evar corresponding to the goal, and an updated evar_map. *) val mk_goal : Evd.evar_map -> Environ.named_context_val -> - Term.constr -> + EConstr.constr -> Evd.Store.t -> - goal * Term.constr * Evd.evar_map + goal * EConstr.constr * Evd.evar_map (* Instantiates a goal with an open term *) - val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map + val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map (* Instantiates a goal with an open term, reusing name of goal for second goal *) - val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map + val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map (* Principal part of the weak-progress tactical *) val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool diff --git a/proofs/logic.ml b/proofs/logic.ml index 093d949d5d..c5d6e3e083 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -349,7 +349,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in if !check && occur_meta sigma (EConstr.of_constr conclty) then raise (RefinerError (MetaInType conclty)); - let (gl,ev,sigma) = mk_goal hyps conclty in + let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr conclty) in + let ev = EConstr.Unsafe.to_constr ev in gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> @@ -424,7 +425,8 @@ and mk_hdgoals sigma goal goalacc trm = match kind_of_term trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in + let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr ty))) in + let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> @@ -526,6 +528,7 @@ let prim_refiner r sigma goal = let env = Goal.V82.env sigma goal in let sign = Goal.V82.hyps sigma goal in let cl = Goal.V82.concl sigma goal in + let cl = EConstr.Unsafe.to_constr cl in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in @@ -533,7 +536,7 @@ let prim_refiner r sigma goal = (* Logical rules *) | Cut (b,replace,id,t) -> (* if !check && not (Retyping.get_sort_of env sigma t) then*) - let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in + let (sg1,ev1,sigma) = mk_goal sign (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr t))) in let sign,t,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in @@ -546,9 +549,10 @@ let prim_refiner r sigma goal = user_err ~hdr:"Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in + let t = EConstr.of_constr t in let (sg2,ev2,sigma) = - Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = Term.mkNamedLetIn id ev1 t ev2 in + Goal.V82.mk_goal sigma sign (EConstr.of_constr cl) (Goal.V82.extra sigma goal) in + let oterm = EConstr.mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) @@ -556,5 +560,5 @@ let prim_refiner r sigma goal = check_meta_variables c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution sigma goal oterm in + let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in (sgl, sigma) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5e9c0ba8e6..c2ebb76d7a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -41,7 +41,7 @@ let project = Refiner.project let pf_env = Refiner.pf_env let pf_hyps = Refiner.pf_hyps -let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls) +let pf_concl gls = EConstr.Unsafe.to_constr (Goal.V82.concl (project gls) (sig_it gls)) let pf_hyps_types gls = let sign = Environ.named_context (pf_env gls) in List.map (function LocalAssum (id,x) @@ -137,7 +137,7 @@ open Pp let db_pr_goal sigma g = let env = Goal.V82.env sigma g in let penv = print_named_context env in - let pc = print_constr_env env (Goal.V82.concl sigma g) in + let pc = print_constr_env env (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () -- cgit v1.2.3 From 53fe23265daafd47e759e73e8f97361c7fdd331b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 18:20:29 +0100 Subject: Refine API using EConstr. --- proofs/goal.ml | 5 ++--- proofs/refine.ml | 11 ++++++----- proofs/refine.mli | 8 ++++---- 3 files changed, 12 insertions(+), 12 deletions(-) (limited to 'proofs') diff --git a/proofs/goal.ml b/proofs/goal.ml index 4c598ca29e..7499bc251b 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -86,12 +86,11 @@ module V82 = struct (* Instantiates a goal with an open term *) let partial_solution sigma evk c = (* Check that the goal itself does not appear in the refined term *) - let c = EConstr.Unsafe.to_constr c in let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () - else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c) + else Pretype_errors.error_occur_check Environ.empty_env sigma evk c in - Evd.define evk c sigma + Evd.define evk (EConstr.Unsafe.to_constr c) sigma (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = diff --git a/proofs/refine.ml b/proofs/refine.ml index 067764c000..11eabe0a90 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -47,7 +47,7 @@ let typecheck_evar ev env sigma = let typecheck_proof c concl env sigma = let evdref = ref sigma in - let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in + let () = Typing.e_check env evdref c concl in !evdref let (pr_constrv,pr_constr) = @@ -77,6 +77,7 @@ let make_refine_enter ?(unsafe = true) f = let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in + let concl = EConstr.of_constr concl in (** Save the [future_goals] state to restore them after the refinement. *) let prev_future_goals = Evd.future_goals sigma in @@ -98,9 +99,10 @@ let make_refine_enter ?(unsafe = true) f = let self = Proofview.Goal.goal gl in let _ = if not (Evarutil.occur_evar_upto sigma self c) then () - else Pretype_errors.error_occur_check env sigma self (EConstr.of_constr c) + else Pretype_errors.error_occur_check env sigma self c in (** Proceed to the refinement *) + let c = EConstr.Unsafe.to_constr c in let sigma = match evkmain with | None -> Evd.define self c sigma | Some evk -> @@ -133,23 +135,22 @@ let refine ?(unsafe = true) f = (** Useful definitions *) let with_type env evd c t = - let c = EConstr.of_constr c in let my_type = Retyping.get_type_of env evd c in let my_type = EConstr.of_constr my_type in let j = Environ.make_judge c my_type in let (evd,j') = - Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t) + Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t in evd , j'.Environ.uj_val let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in + let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in let f = { run = fun h -> let Sigma (c, h, p) = f.run h in let sigma, c = with_type env (Sigma.to_evar_map h) c concl in - let c = EConstr.Unsafe.to_constr c in Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) } in refine ?unsafe f diff --git a/proofs/refine.mli b/proofs/refine.mli index 4158e446cc..205b979747 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -21,7 +21,7 @@ val pr_constr : (** {7 Refinement primitives} *) -val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic (** In [refine ?unsafe t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the @@ -30,16 +30,16 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [unsafe] is [false] (default is [true]) [t] is type-checked beforehand. *) -val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic +val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic (** A generalization of [refine] which assumes exactly one goal under focus *) (** {7 Helper functions} *) val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * EConstr.constr + EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) -val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) -- cgit v1.2.3 From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 19:52:48 +0100 Subject: Tacmach API using EConstr. --- proofs/clenvtac.ml | 2 +- proofs/logic.ml | 1 + proofs/tacmach.ml | 45 ++++++++++++++++++++++----------------------- proofs/tacmach.mli | 50 +++++++++++++++++++++++++------------------------- 4 files changed, 49 insertions(+), 49 deletions(-) (limited to 'proofs') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index bc5f17bf5e..5b9322bfec 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -95,7 +95,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) - (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + (refine_no_check (EConstr.of_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl end open Unification diff --git a/proofs/logic.ml b/proofs/logic.ml index c5d6e3e083..829c962962 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -490,6 +490,7 @@ and mk_arggoals sigma goal goalacc funty allargs = and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in + let ct = EConstr.of_constr ct in let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let indspec = try Tacred.find_hnf_rectype env sigma ct diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c2ebb76d7a..b732e5b9d9 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -77,37 +77,36 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in let sigma = Sigma.Unsafe.of_evar_map (project gls) in - let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma (EConstr.of_constr c) in + let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in (Sigma.to_evar_map sigma, c) let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x) let pf_reduce = pf_apply -let pf_reduce' f gl c = pf_apply f gl (EConstr.of_constr c) let pf_e_reduce = pf_apply -let pf_whd_all = pf_reduce' whd_all -let pf_hnf_constr = pf_reduce' hnf_constr -let pf_nf = pf_reduce' simpl -let pf_nf_betaiota = pf_reduce' (fun _ -> nf_betaiota) -let pf_compute = pf_reduce' compute -let pf_unfoldn ubinds = pf_reduce' (unfoldn ubinds) -let pf_unsafe_type_of = pf_reduce' unsafe_type_of -let pf_type_of = pf_reduce' type_of +let pf_whd_all = pf_reduce whd_all +let pf_hnf_constr = pf_reduce hnf_constr +let pf_nf = pf_reduce simpl +let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) +let pf_compute = pf_reduce compute +let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_unsafe_type_of = pf_reduce unsafe_type_of +let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of -let pf_conv_x gl = pf_apply test_conversion gl Reduction.CONV +let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls +let pf_hnf_type_of gls = pf_get_type_of gls %> EConstr.of_constr %> pf_whd_all gls -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p (EConstr.of_constr c) -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p (EConstr.of_constr c) +let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c +let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c (********************************************) (* Definition of the most primitive tactics *) @@ -116,12 +115,15 @@ let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p (EC let refiner = refiner let internal_cut_no_check replace id t gl = + let t = EConstr.Unsafe.to_constr t in refiner (Cut (true,replace,id,t)) gl let internal_cut_rev_no_check replace id t gl = + let t = EConstr.Unsafe.to_constr t in refiner (Cut (false,replace,id,t)) gl let refine_no_check c gl = + let c = EConstr.Unsafe.to_constr c in refiner (Refine c) gl (* Versions with consistency checks *) @@ -159,9 +161,6 @@ module New = struct let pf_apply f gl = f (Proofview.Goal.env gl) (project gl) - let pf_reduce f gl c = - f (Proofview.Goal.env gl) (project gl) (EConstr.of_constr c) - let of_old f gl = f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } @@ -175,10 +174,10 @@ module New = struct let pf_concl = Proofview.Goal.concl let pf_unsafe_type_of gl t = - pf_apply unsafe_type_of gl (EConstr.of_constr t) + pf_apply unsafe_type_of gl t let pf_type_of gl t = - pf_apply type_of gl (EConstr.of_constr t) + pf_apply type_of gl t let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2 @@ -221,18 +220,18 @@ module New = struct let sigma = project gl in nf_evar sigma concl - let pf_whd_all gl t = pf_reduce whd_all gl t + let pf_whd_all gl t = pf_apply whd_all gl t let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t let pf_reduce_to_quantified_ind gl t = pf_apply reduce_to_quantified_ind gl t - let pf_hnf_constr gl t = pf_reduce hnf_constr gl t + let pf_hnf_constr gl t = pf_apply hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t)) + pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat (EConstr.of_constr t) + let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 16f6f88c17..07d02212ca 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -40,9 +40,9 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_unsafe_type_of : goal sigma -> constr -> types -val pf_type_of : goal sigma -> constr -> evar_map * types -val pf_hnf_type_of : goal sigma -> constr -> types +val pf_unsafe_type_of : goal sigma -> EConstr.constr -> types +val pf_type_of : goal sigma -> EConstr.constr -> evar_map * types +val pf_hnf_type_of : goal sigma -> EConstr.constr -> types val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types @@ -50,7 +50,7 @@ val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list -val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr +val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a @@ -63,35 +63,35 @@ val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> goal sigma -> constr -> evar_map * constr -val pf_whd_all : goal sigma -> constr -> constr -val pf_hnf_constr : goal sigma -> constr -> constr -val pf_nf : goal sigma -> constr -> constr -val pf_nf_betaiota : goal sigma -> constr -> constr -val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types -val pf_reduce_to_atomic_ind : goal sigma -> types -> pinductive * types -val pf_compute : goal sigma -> constr -> constr +val pf_whd_all : goal sigma -> EConstr.constr -> constr +val pf_hnf_constr : goal sigma -> EConstr.constr -> constr +val pf_nf : goal sigma -> EConstr.constr -> constr +val pf_nf_betaiota : goal sigma -> EConstr.constr -> constr +val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * types +val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * types +val pf_compute : goal sigma -> EConstr.constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list - -> goal sigma -> constr -> constr + -> goal sigma -> EConstr.constr -> constr val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool +val pf_matches : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map +val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool (** {6 The most primitive tactics. } *) val refiner : rule -> tactic -val internal_cut_no_check : bool -> Id.t -> types -> tactic -val refine_no_check : constr -> tactic +val internal_cut_no_check : bool -> Id.t -> EConstr.types -> tactic +val refine_no_check : EConstr.constr -> tactic (** {6 The most primitive tactics with consistency and type checking } *) -val internal_cut : bool -> Id.t -> types -> tactic -val internal_cut_rev : bool -> Id.t -> types -> tactic -val refine : constr -> tactic +val internal_cut : bool -> Id.t -> EConstr.types -> tactic +val internal_cut_rev : bool -> Id.t -> EConstr.types -> tactic +val refine : EConstr.constr -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.std_ppcmds @@ -108,8 +108,8 @@ module New : sig val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types - val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types + val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types + val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * Term.types val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier @@ -121,15 +121,15 @@ module New : sig val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * types - val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr - val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr -- cgit v1.2.3 From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 21:55:33 +0100 Subject: Clenv API using EConstr. --- proofs/clenv.ml | 129 +++++++++++++++++++++++++++------------------------- proofs/clenv.mli | 31 ++++++------- proofs/clenvtac.ml | 17 +++---- proofs/clenvtac.mli | 1 + 4 files changed, 93 insertions(+), 85 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 67ed5daaa1..3e3889cbb3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -12,11 +12,12 @@ open Util open Names open Nameops open Term -open Vars open Termops open Namegen open Environ open Evd +open EConstr +open Vars open Reduction open Reductionops open Tacred @@ -29,7 +30,7 @@ open Sigma.Notations (* Abbreviations *) let pf_env = Refiner.pf_env -let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c) +let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c (******************************************************************) (* Clausal environments *) @@ -43,12 +44,6 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let map_clenv sub clenv = - { templval = map_fl sub clenv.templval; - templtyp = map_fl sub clenv.templtyp; - evd = cmap sub clenv.evd; - env = clenv.env } - let clenv_nf_meta clenv c = nf_meta clenv.evd c let clenv_term clenv c = meta_instance clenv.evd c let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv @@ -56,30 +51,34 @@ let clenv_value clenv = meta_instance clenv.evd clenv.templval let clenv_type clenv = meta_instance clenv.evd clenv.templtyp let refresh_undefined_univs clenv = - match kind_of_term clenv.templval.rebus with + match EConstr.kind clenv.evd clenv.templval.rebus with | Var _ -> clenv, Univ.empty_level_subst - | App (f, args) when isVar f -> clenv, Univ.empty_level_subst + | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst | _ -> let evd', subst = Evd.refresh_undefined_universes clenv.evd in let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in { clenv with evd = evd'; templval = map_freelisted clenv.templval; templtyp = map_freelisted clenv.templtyp }, subst -let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t +let clenv_hnf_constr ce t = EConstr.of_constr (hnf_constr (cl_env ce) (cl_sigma ce) t) -let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) (EConstr.of_constr c) +let clenv_get_type_of ce c = EConstr.of_constr (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) (EConstr.of_constr (clenv_type cl)) in - let rec clrec typ = match kind_of_term typ with + let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in + let typ = EConstr.of_constr typ in + let rec clrec typ = match EConstr.kind cl.evd typ with | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> let mv = new_meta () in - let dep = not (EConstr.Vars.noccurn (cl_sigma cl) 1 (EConstr.of_constr u)) 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 t ~name:na' cl.evd in + let e' = meta_declare mv (EConstr.Unsafe.to_constr 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; @@ -103,14 +102,17 @@ let clenv_push_prod cl = and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) let clenv_environments evd bound t = + let open EConstr in + let open Vars in let rec clrec (e,metas) n t = - match n, kind_of_term t with + match n, EConstr.kind evd t with | (Some 0, _) -> (e, List.rev metas, t) | (n, Cast (t,_,_)) -> clrec (e,metas) n t | (n, Prod (na,t1,t2)) -> let mv = new_meta () in - let dep = not (noccurn 1 t2) 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 clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) t2) else t2) @@ -132,7 +134,7 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) +let mk_clenv_type_of gls t = mk_clenv_from gls (t,EConstr.of_constr (pf_type_of gls t)) (******************************************************************) @@ -168,13 +170,13 @@ let clenv_assign mv rhs clenv = error "clenv_assign: circularity in unification"; try if meta_defined clenv.evd mv then - if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then + if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (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 (rhs_fls.rebus,st) clenv.evd} + {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd} with Not_found -> error "clenv_assign: undefined meta" @@ -219,7 +221,7 @@ let clenv_assign mv rhs clenv = *) let clenv_metas_in_type_of_meta evd mv = - (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas + (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right @@ -257,15 +259,14 @@ let clenv_dependent ce = clenv_dependent_gen false ce let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv = { clenv with - evd = w_unify ~flags clenv.env clenv.evd cv_pb (EConstr.of_constr t1) (EConstr.of_constr t2) } + evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 } let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = let concl = Goal.V82.concl clenv.evd (sig_it gl) in - let concl = EConstr.Unsafe.to_constr concl in - if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then + if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus))))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) else @@ -275,23 +276,19 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = let adjust_meta_source evd mv = function | loc,Evar_kinds.VarInstance id -> let rec match_name c l = - match kind_of_term c, l with - | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id + match EConstr.kind evd c, l with + | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id | Lambda (_,_,c), a::l -> match_name c l | _ -> None in (* This is very ad hoc code so that an evar inherits the name of the binder 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 t.rebus in - match kind_of_term f with + let f,l = decompose_app evd (EConstr.of_constr t.rebus) in + match EConstr.kind evd f with | Meta mv'' -> (match meta_opt_fvalue evd mv'' with - | Some (c,_) -> match_name c.rebus l - | None -> None) - | Evar ev -> - (match existential_opt_value evd ev with - | Some c -> match_name c l + | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l | None -> None) | _ -> None else None in @@ -333,13 +330,14 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let ty = clenv_meta_type clenv mv in (* Postpone the evar-ization if dependent on another meta *) (* This assumes no cycle in the dependencies - is it correct ? *) - if occur_meta clenv.evd (EConstr.of_constr ty) then fold clenv (mvs@[mv]) + if occur_meta clenv.evd ty then fold clenv (mvs@[mv]) else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in let evd = Sigma.Unsafe.of_evar_map clenv.evd in - let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src (EConstr.of_constr ty) in + let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in let evd = Sigma.to_evar_map evd in + let evar = EConstr.of_constr evar in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs @@ -405,7 +403,7 @@ type arg_bindings = constr explicit_bindings * of cval, ctyp. *) let clenv_independent clenv = - let mvs = collect_metas clenv.evd (EConstr.of_constr (clenv_value clenv)) in + let mvs = collect_metas clenv.evd (clenv_value clenv) in let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in List.filter (fun mv -> not (Metaset.mem mv deps)) mvs @@ -483,15 +481,13 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - let u = EConstr.of_constr u in - if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then + if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u))))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else (* Enough information so as to try a coercion now *) try - let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd (EConstr.of_constr c) (EConstr.of_constr t) u in - let c = EConstr.Unsafe.to_constr c in + let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with | PretypeError (_,_,ActualTypeNotCoercible (_,_, @@ -501,9 +497,11 @@ let clenv_unify_binding_type clenv c t u = TypeNotProcessed, clenv, c let clenv_assign_binding clenv k c = - let k_typ = clenv_hnf_constr clenv (EConstr.of_constr (clenv_meta_type clenv k)) in - let c_typ = nf_betaiota clenv.evd (EConstr.of_constr (clenv_get_type_of clenv c)) in + let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in + let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in + let c_typ = EConstr.of_constr c_typ 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 = @@ -516,7 +514,7 @@ let clenv_match_args bl clenv = (fun clenv (loc,b,c) -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then - if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv + if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv else error_already_defined b else clenv_assign_binding clenv k c) @@ -525,7 +523,7 @@ let clenv_match_args bl clenv = exception NoSuchBinding let clenv_constrain_last_binding c clenv = - let all_mvs = collect_metas clenv.evd (EConstr.of_constr clenv.templval.rebus) in + let all_mvs = collect_metas clenv.evd clenv.templval.rebus in let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in clenv_assign_binding clenv k c @@ -560,8 +558,9 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let clause = mk_clenv_from_env env sigma n (c,t) in clenv_constrain_dep_args hyps_only largs clause | ExplicitBindings lbind -> + let t = EConstr.of_constr (rename_bound_vars_as_displayed [] [] (EConstr.Unsafe.to_constr t)) in let clause = mk_clenv_from_env env sigma n - (c,rename_bound_vars_as_displayed [] [] t) + (c, t) in clenv_match_args lbind clause | NoBindings -> mk_clenv_from_env env sigma n (c,t) @@ -579,43 +578,49 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma (* Pretty-print *) let pr_clenv clenv = + let inj = EConstr.Unsafe.to_constr in h 0 - (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ - str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ + (str"TEMPL: " ++ print_constr (inj clenv.templval.rebus) ++ + str" : " ++ print_constr (inj clenv.templtyp.rebus) ++ fnl () ++ pr_evar_map (Some 2) clenv.evd) (****************************************************************) (** Evar version of mk_clenv *) type hole = { - hole_evar : constr; - hole_type : types; + hole_evar : EConstr.constr; + hole_type : EConstr.types; hole_deps : bool; hole_name : Name.t; } type clause = { cl_holes : hole list; - cl_concl : types; + cl_concl : EConstr.types; } let make_evar_clause env sigma ?len t = + let open EConstr in + let open Vars in let bound = match len with | None -> -1 | Some n -> assert (0 <= n); n in (** FIXME: do the renaming online *) + let t = EConstr.Unsafe.to_constr t in let t = rename_bound_vars_as_displayed [] [] t in + let t = EConstr.of_constr t in let rec clrec (sigma, holes) n t = if n = 0 then (sigma, holes, t) - else match kind_of_term t with + else match EConstr.kind sigma t with | Cast (t, _, _) -> clrec (sigma, holes) n t | Prod (na, t1, t2) -> let store = Typeclasses.set_resolvable Evd.Store.empty false in let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (ev, sigma, _) = new_evar ~store env sigma (EConstr.of_constr t1) in + let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in let sigma = Sigma.to_evar_map sigma in - let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in + let ev = EConstr.of_constr ev in + let dep = not (noccurn sigma 1 t2) in let hole = { hole_evar = ev; hole_type = t1; @@ -670,26 +675,28 @@ let evar_of_binder holes = function user_err (str "No such binder.") let define_with_type sigma env ev c = - let c = EConstr.of_constr c in - let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in + let open EConstr in + let t = Retyping.get_type_of env sigma ev in + let t = EConstr.of_constr t in let ty = Retyping.get_type_of env sigma c in let ty = EConstr.of_constr ty in let j = Environ.make_judge c ty in - let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in - let (ev, _) = destEvar ev in + let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) 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 sigma let solve_evar_clause env sigma hyp_only clause = function | NoBindings -> sigma | ImplicitBindings largs -> + let open EConstr in let fold holes h = if h.hole_deps then (** Some subsequent term uses the hole *) - let (ev, _) = destEvar h.hole_evar in - let is_dep hole = occur_evar sigma ev (EConstr.of_constr hole.hole_type) in + let (ev, _) = destEvar sigma h.hole_evar in + let is_dep hole = occur_evar sigma ev hole.hole_type in let in_hyp = List.exists is_dep holes in - let in_ccl = occur_evar sigma ev (EConstr.of_constr clause.cl_concl) in + let in_ccl = occur_evar sigma ev clause.cl_concl in let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in let h = { h with hole_deps = dep } in h :: holes diff --git a/proofs/clenv.mli b/proofs/clenv.mli index e9236b1da3..e4f6f9a910 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -14,6 +14,7 @@ open Names open Term open Environ open Evd +open EConstr open Unification open Misctypes @@ -28,8 +29,6 @@ type clausenv = { templtyp : constr freelisted (** its type *)} -val map_clenv : (constr -> constr) -> clausenv -> clausenv - (** subject of clenv (instantiated) *) val clenv_value : clausenv -> constr @@ -37,16 +36,16 @@ val clenv_value : clausenv -> constr val clenv_type : clausenv -> types (** substitute resolved metas *) -val clenv_nf_meta : clausenv -> constr -> constr +val clenv_nf_meta : clausenv -> Constr.constr -> Constr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types -val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv +val mk_clenv_from : Goal.goal sigma -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : - Goal.goal sigma -> int option -> constr * types -> clausenv -val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv -val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv + Goal.goal sigma -> int option -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_type_of : Goal.goal sigma -> EConstr.constr -> clausenv +val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst @@ -92,18 +91,18 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv the optional int tells how many prods of the lemma have to be used use all of them if None *) val make_clenv_binding_env_apply : - env -> evar_map -> int option -> constr * constr -> constr bindings -> + env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv val make_clenv_binding_apply : - env -> evar_map -> int option -> constr * constr -> constr bindings -> + env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv val make_clenv_binding_env : - env -> evar_map -> constr * constr -> constr bindings -> clausenv + env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv val make_clenv_binding : - env -> evar_map -> constr * constr -> constr bindings -> clausenv + env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv (** if the clause is a product, add an extra meta for this product *) exception NotExtensibleClause @@ -134,9 +133,9 @@ val pr_clenv : clausenv -> Pp.std_ppcmds *) type hole = { - hole_evar : constr; + hole_evar : EConstr.constr; (** The hole itself. Guaranteed to be an evar. *) - hole_type : types; + hole_type : EConstr.types; (** Type of the hole in the current environment. *) hole_deps : bool; (** Whether the remainder of the clause was dependent in the hole. Note that @@ -148,10 +147,10 @@ type hole = { type clause = { cl_holes : hole list; - cl_concl : types; + cl_concl : EConstr.types; } -val make_evar_clause : env -> evar_map -> ?len:int -> types -> +val make_evar_clause : env -> evar_map -> ?len:int -> EConstr.types -> (evar_map * clause) (** An evar version of {!make_clenv_binding}. Given a type [t], [evar_environments env sigma ~len t bl] tries to eliminate at most [len] @@ -159,7 +158,7 @@ val make_evar_clause : env -> evar_map -> ?len:int -> types -> type together with the list of holes generated. Assumes that [t] is well-typed in the environment. *) -val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings -> +val solve_evar_clause : env -> evar_map -> bool -> clause -> EConstr.constr bindings -> evar_map (** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 5b9322bfec..539b1bcb21 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -11,6 +11,7 @@ open Names open Term open Termops open Evd +open EConstr open Refiner open Logic open Reduction @@ -26,19 +27,19 @@ open Proofview.Notations let clenv_cast_meta clenv = let rec crec u = - match kind_of_term u with + match EConstr.kind clenv.evd u with | App _ | Case _ -> crec_hd u - | Cast (c,_,_) when isMeta c -> u + | Cast (c,_,_) when isMeta clenv.evd c -> u | Proj (p, c) -> mkProj (p, crec_hd c) - | _ -> map_constr crec u + | _ -> EConstr.map clenv.evd crec u and crec_hd u = - match kind_of_term (strip_outer_cast clenv.evd (EConstr.of_constr u)) with + match EConstr.kind clenv.evd (EConstr.of_constr (strip_outer_cast clenv.evd u)) with | Meta mv -> (try let b = Typing.meta_type clenv.evd mv in - assert (not (occur_meta clenv.evd (EConstr.of_constr b))); - if occur_meta clenv.evd (EConstr.of_constr b) then u + assert (not (occur_meta clenv.evd b)); + if occur_meta clenv.evd b then u else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) @@ -95,7 +96,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) - (refine_no_check (EConstr.of_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl + (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl end open Unification @@ -143,7 +144,7 @@ let unify ?(flags=fail_quick_unif_flags) m = let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in let evd = clear_metas (Tacmach.New.project gl) in try - let evd' = w_unify env evd CONV ~flags (EConstr.of_constr m) (EConstr.of_constr n) in + let evd' = w_unify env evd CONV ~flags m (EConstr.of_constr n) in Proofview.Unsafe.tclEVARSADVANCE evd' with e when CErrors.noncritical e -> Proofview.tclZERO e end } diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 8a096b6457..5b7164705a 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -10,6 +10,7 @@ open Term open Clenv +open EConstr open Unification open Misctypes -- cgit v1.2.3 From 45562afa065aadc207dca4e904e309d835cb66ef Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 12 Nov 2016 01:28:45 +0100 Subject: Tacticals API using EConstr. --- proofs/clenv.ml | 2 +- proofs/clenv.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 3e3889cbb3..fd88e3c518 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -44,7 +44,7 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_nf_meta clenv c = nf_meta clenv.evd c +let clenv_nf_meta clenv c = EConstr.of_constr (nf_meta clenv.evd (EConstr.Unsafe.to_constr c)) let clenv_term clenv c = meta_instance clenv.evd c let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv let clenv_value clenv = meta_instance clenv.evd clenv.templval diff --git a/proofs/clenv.mli b/proofs/clenv.mli index e4f6f9a910..f7ff4bed34 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -36,7 +36,7 @@ val clenv_value : clausenv -> constr val clenv_type : clausenv -> types (** substitute resolved metas *) -val clenv_nf_meta : clausenv -> Constr.constr -> Constr.constr +val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types -- cgit v1.2.3 From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- proofs/clenv.ml | 2 -- proofs/tacmach.mli | 6 +++--- 2 files changed, 3 insertions(+), 5 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index fd88e3c518..514fc27e89 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -337,7 +337,6 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let evd = Sigma.Unsafe.of_evar_map clenv.evd in let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in let evd = Sigma.to_evar_map evd in - let evar = EConstr.of_constr evar in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs @@ -619,7 +618,6 @@ let make_evar_clause env sigma ?len t = let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in let sigma = Sigma.to_evar_map sigma in - let ev = EConstr.of_constr ev in let dep = not (noccurn sigma 1 t2) in let hole = { hole_evar = ev; diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 07d02212ca..cfbfe12b17 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -67,8 +67,8 @@ val pf_whd_all : goal sigma -> EConstr.constr -> constr val pf_hnf_constr : goal sigma -> EConstr.constr -> constr val pf_nf : goal sigma -> EConstr.constr -> constr val pf_nf_betaiota : goal sigma -> EConstr.constr -> constr -val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * types -val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * types +val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types +val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types val pf_compute : goal sigma -> EConstr.constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list -> goal sigma -> EConstr.constr -> constr @@ -121,7 +121,7 @@ module New : sig val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * EConstr.types val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types -- cgit v1.2.3 From 34e86e839be251717db96f1f5969d7724ab43097 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Nov 2016 02:45:54 +0100 Subject: Hints API using EConstr. --- proofs/evar_refiner.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 4be03af9a6..0d65faf12c 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -18,17 +18,19 @@ open Pp (* Instantiation of existential variables *) (******************************************) -let depends_on_evar evk _ (pbty,_,t1,t2) = - try Evar.equal (head_evar t1) evk +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 t2) evk + try Evar.equal (head_evar sigma t2) evk with NoHeadEvar -> false let define_and_solve_constraints evk c env evd = if Termops.occur_evar evd evk (EConstr.of_constr c) then Pretype_errors.error_occur_check env evd evk (EConstr.of_constr c); let evd = define evk c evd in - let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) 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 -- cgit v1.2.3 From c72bf7330bb32970616be4dddc7571f3b91c1562 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 01:08:53 +0100 Subject: Eqdecide API using EConstr. --- proofs/tacmach.ml | 2 ++ proofs/tacmach.mli | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b732e5b9d9..aa54e4f9bb 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -23,6 +23,8 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration +let compute env sigma c = EConstr.of_constr (compute env sigma c) + let re_sig it gc = { it = it; sigma = gc; } (**************************************************************) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index cfbfe12b17..340c7addca 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -69,7 +69,7 @@ val pf_nf : goal sigma -> EConstr.constr -> constr val pf_nf_betaiota : goal sigma -> EConstr.constr -> constr val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types -val pf_compute : goal sigma -> EConstr.constr -> constr +val pf_compute : goal sigma -> EConstr.constr -> EConstr.constr val pf_unfoldn : (occurrences * evaluable_global_reference) list -> goal sigma -> EConstr.constr -> constr @@ -127,7 +127,7 @@ module New : sig val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr - val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map -- cgit v1.2.3 From d833b81b49366e95cf20a1d00f9c63883adb8942 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 03:04:13 +0100 Subject: Rewrite API using EConstr. --- proofs/clenv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 514fc27e89..d986696604 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -44,7 +44,7 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_nf_meta clenv c = EConstr.of_constr (nf_meta clenv.evd (EConstr.Unsafe.to_constr c)) +let clenv_nf_meta clenv c = nf_meta clenv.evd c let clenv_term clenv c = meta_instance clenv.evd c let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv let clenv_value clenv = meta_instance clenv.evd clenv.templval -- cgit v1.2.3 From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- proofs/clenv.ml | 4 ++-- proofs/clenvtac.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d986696604..572db1d408 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -266,7 +266,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = let concl = Goal.V82.concl clenv.evd (sig_it gl) in - if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus))))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus)))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) else @@ -480,7 +480,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u))))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u)))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 539b1bcb21..84cdc09eec 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -34,7 +34,7 @@ let clenv_cast_meta clenv = | _ -> EConstr.map clenv.evd crec u and crec_hd u = - match EConstr.kind clenv.evd (EConstr.of_constr (strip_outer_cast clenv.evd u)) with + match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with | Meta mv -> (try let b = Typing.meta_type clenv.evd mv in -- cgit v1.2.3 From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 22:16:08 +0100 Subject: Proofview.Goal primitive now return EConstrs. --- proofs/clenvtac.ml | 2 +- proofs/refine.ml | 2 -- proofs/tacmach.ml | 8 ++++---- proofs/tacmach.mli | 10 +++++----- 4 files changed, 10 insertions(+), 12 deletions(-) (limited to 'proofs') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 84cdc09eec..32c887ff59 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -144,7 +144,7 @@ let unify ?(flags=fail_quick_unif_flags) m = let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in let evd = clear_metas (Tacmach.New.project gl) in try - let evd' = w_unify env evd CONV ~flags m (EConstr.of_constr n) in + let evd' = w_unify env evd CONV ~flags m n in Proofview.Unsafe.tclEVARSADVANCE evd' with e when CErrors.noncritical e -> Proofview.tclZERO e end } diff --git a/proofs/refine.ml b/proofs/refine.ml index 11eabe0a90..32064aff50 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -77,7 +77,6 @@ let make_refine_enter ?(unsafe = true) f = let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in (** Save the [future_goals] state to restore them after the refinement. *) let prev_future_goals = Evd.future_goals sigma in @@ -146,7 +145,6 @@ let with_type env evd c t = let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in let f = { run = fun h -> let Sigma (c, h, p) = f.run h in diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index aa54e4f9bb..f3f19e8542 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -220,7 +220,7 @@ module New = struct let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = project gl in - nf_evar sigma concl + EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl)) let pf_whd_all gl t = pf_apply whd_all gl t @@ -229,13 +229,13 @@ module New = struct let pf_reduce_to_quantified_ind gl t = pf_apply reduce_to_quantified_ind gl t - let pf_hnf_constr gl t = pf_apply hnf_constr gl t + let pf_hnf_constr gl t = EConstr.of_constr (pf_apply hnf_constr gl t) let pf_hnf_type_of gl t = - pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) + EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t + let pf_whd_all gl t = EConstr.of_constr (pf_apply whd_all gl t) let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 340c7addca..7b387ac9ad 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -106,7 +106,7 @@ module New : sig val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env - val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * Term.types @@ -120,13 +120,13 @@ module New : sig val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t - val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> EConstr.types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * EConstr.types - val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types - val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types - val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr + val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- proofs/clenv.ml | 8 +++----- proofs/logic.ml | 12 +++++++----- proofs/logic.mli | 2 +- proofs/redexpr.ml | 2 +- proofs/tacmach.ml | 8 +++----- proofs/tacmach.mli | 14 +++++++------- 6 files changed, 22 insertions(+), 24 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 572db1d408..a428ab0ed0 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -60,7 +60,7 @@ let refresh_undefined_univs clenv = { clenv with evd = evd'; templval = map_freelisted clenv.templval; templtyp = map_freelisted clenv.templtyp }, subst -let clenv_hnf_constr ce t = EConstr.of_constr (hnf_constr (cl_env ce) (cl_sigma ce) t) +let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c) @@ -71,7 +71,6 @@ let mk_freelisted c = let clenv_push_prod cl = let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in - let typ = EConstr.of_constr typ in let rec clrec typ = match EConstr.kind cl.evd typ with | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> @@ -266,7 +265,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = let concl = Goal.V82.concl clenv.evd (sig_it gl) in - if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus)))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) else @@ -480,7 +479,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u)))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else @@ -498,7 +497,6 @@ let clenv_unify_binding_type clenv c t u = 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.evd (clenv_get_type_of clenv c) in - let c_typ = EConstr.of_constr c_typ 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 } diff --git a/proofs/logic.ml b/proofs/logic.ml index 829c962962..98ad9ebe3e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -34,7 +34,7 @@ type refiner_error = | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr - | MetaInType of constr + | MetaInType of EConstr.constr (* Errors raised by the tactics *) | IntroNeedsProduct @@ -347,10 +347,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind_of_term trm with | Meta _ -> let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in - if !check && occur_meta sigma (EConstr.of_constr conclty) then + if !check && occur_meta sigma conclty then raise (RefinerError (MetaInType conclty)); - let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr conclty) in + let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in + let conclty = EConstr.Unsafe.to_constr conclty in gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> @@ -425,7 +426,7 @@ and mk_hdgoals sigma goal goalacc trm = match kind_of_term trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr ty))) in + let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev @@ -474,6 +475,7 @@ and mk_hdgoals sigma goal goalacc trm = and mk_arggoals sigma goal goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in + let t = EConstr.Unsafe.to_constr t in let rec collapse t = match kind_of_term t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) | _ -> t @@ -537,7 +539,7 @@ let prim_refiner r sigma goal = (* Logical rules *) | Cut (b,replace,id,t) -> (* if !check && not (Retyping.get_sort_of env sigma t) then*) - let (sg1,ev1,sigma) = mk_goal sign (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr t))) in + let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in let sign,t,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in diff --git a/proofs/logic.mli b/proofs/logic.mli index 8c8a01cada..5fe28ac76a 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -43,7 +43,7 @@ type refiner_error = | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr - | MetaInType of constr + | MetaInType of EConstr.constr (*i Errors raised by the tactics i*) | IntroNeedsProduct diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index d4a58da326..a830e25d9e 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -44,7 +44,7 @@ let whd_cbn flags env sigma t = let (state,_) = (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty)) in - EConstr.Unsafe.to_constr (Reductionops.Stack.zip ~refold:true sigma state) + Reductionops.Stack.zip ~refold:true sigma state let strong_cbn flags = strong (whd_cbn flags) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index f3f19e8542..7ecf0a9e83 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -23,8 +23,6 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -let compute env sigma c = EConstr.of_constr (compute env sigma c) - let re_sig it gc = { it = it; sigma = gc; } (**************************************************************) @@ -229,13 +227,13 @@ module New = struct let pf_reduce_to_quantified_ind gl t = pf_apply reduce_to_quantified_ind gl t - let pf_hnf_constr gl t = EConstr.of_constr (pf_apply hnf_constr gl t) + let pf_hnf_constr gl t = pf_apply hnf_constr gl t let pf_hnf_type_of gl t = - EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))) + pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = EConstr.of_constr (pf_apply whd_all gl t) + let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7b387ac9ad..21511b6f98 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -42,7 +42,7 @@ val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> EConstr.constr -> types val pf_type_of : goal sigma -> EConstr.constr -> evar_map * types -val pf_hnf_type_of : goal sigma -> EConstr.constr -> types +val pf_hnf_type_of : goal sigma -> EConstr.constr -> EConstr.types val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types @@ -50,7 +50,7 @@ val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list -val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * constr +val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * EConstr.constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a @@ -63,15 +63,15 @@ val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> goal sigma -> constr -> evar_map * constr -val pf_whd_all : goal sigma -> EConstr.constr -> constr -val pf_hnf_constr : goal sigma -> EConstr.constr -> constr -val pf_nf : goal sigma -> EConstr.constr -> constr -val pf_nf_betaiota : goal sigma -> EConstr.constr -> constr +val pf_whd_all : goal sigma -> EConstr.constr -> EConstr.constr +val pf_hnf_constr : goal sigma -> EConstr.constr -> EConstr.constr +val pf_nf : goal sigma -> EConstr.constr -> EConstr.constr +val pf_nf_betaiota : goal sigma -> EConstr.constr -> EConstr.constr val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types val pf_compute : goal sigma -> EConstr.constr -> EConstr.constr val pf_unfoldn : (occurrences * evaluable_global_reference) list - -> goal sigma -> EConstr.constr -> constr + -> goal sigma -> EConstr.constr -> EConstr.constr val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool -- cgit v1.2.3 From a327ae04966aa1c7786ae32157516e934068ea89 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 21:33:14 +0100 Subject: Quote API using EConstr. --- proofs/tacmach.ml | 5 +++++ proofs/tacmach.mli | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 7ecf0a9e83..d9caadd54e 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -41,6 +41,11 @@ let project = Refiner.project let pf_env = Refiner.pf_env let pf_hyps = Refiner.pf_hyps +let test_conversion cb env sigma c1 c2 = + let c1 = EConstr.Unsafe.to_constr c1 in + let c2 = EConstr.Unsafe.to_constr c2 in + test_conversion cb env sigma c1 c2 + let pf_concl gls = EConstr.Unsafe.to_constr (Goal.V82.concl (project gls) (sig_it gls)) let pf_hyps_types gls = let sign = Environ.named_context (pf_env gls) in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 21511b6f98..06b3e39812 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -74,8 +74,8 @@ val pf_unfoldn : (occurrences * evaluable_global_reference) list -> goal sigma -> EConstr.constr -> EConstr.constr val pf_const_value : goal sigma -> pconstant -> constr -val pf_conv_x : goal sigma -> constr -> constr -> bool -val pf_conv_x_leq : goal sigma -> constr -> constr -> bool +val pf_conv_x : goal sigma -> EConstr.constr -> EConstr.constr -> bool +val pf_conv_x_leq : goal sigma -> EConstr.constr -> EConstr.constr -> bool val pf_matches : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool -- cgit v1.2.3 From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 17:15:15 +0100 Subject: Removing compatibility layers in Retyping --- proofs/clenv.ml | 4 +--- proofs/logic.ml | 8 ++++++-- proofs/redexpr.ml | 4 ++-- proofs/refine.ml | 1 - proofs/tacmach.ml | 4 ++-- proofs/tacmach.mli | 4 ++-- 6 files changed, 13 insertions(+), 12 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index a428ab0ed0..393e958d38 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -62,7 +62,7 @@ let refresh_undefined_univs clenv = let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t -let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c) +let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause @@ -673,9 +673,7 @@ let evar_of_binder holes = function let define_with_type sigma env ev c = let open EConstr in let t = Retyping.get_type_of env sigma ev in - let t = EConstr.of_constr t in let ty = Retyping.get_type_of env sigma c in - let ty = EConstr.of_constr ty in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in let (ev, _) = destEvar sigma ev in diff --git a/proofs/logic.ml b/proofs/logic.ml index 98ad9ebe3e..8b890f6f81 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -331,7 +331,7 @@ let meta_free_prefix sigma a = let goal_type_of env sigma c = if !check then unsafe_type_of env sigma (EConstr.of_constr c) - else Retyping.get_type_of env sigma (EConstr.of_constr c) + else EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)) let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in @@ -341,6 +341,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = in if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in + let t'ty = EConstr.Unsafe.to_constr t'ty in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) else @@ -377,6 +378,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) in + let ty = EConstr.Unsafe.to_constr ty in goalacc, ty, sigma, f else mk_hdgoals sigma goal goalacc f @@ -390,6 +392,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in + let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> @@ -439,7 +442,7 @@ and mk_hdgoals sigma goal goalacc trm = if is_template_polymorphic env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in - (goalacc,type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l',sigma,f) + (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) else mk_hdgoals sigma goal goalacc f in let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in @@ -465,6 +468,7 @@ and mk_hdgoals sigma goal goalacc trm = let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in + let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | _ -> diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index a830e25d9e..8878051c89 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -25,7 +25,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = let ctyp = Retyping.get_type_of env sigma c in - Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) + Vnorm.cbv_vm env sigma c ctyp let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" @@ -38,7 +38,7 @@ let cbv_native env sigma c = cbv_vm env sigma c) else let ctyp = Retyping.get_type_of env sigma c in - Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) + Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = diff --git a/proofs/refine.ml b/proofs/refine.ml index 32064aff50..c36bb143e8 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -135,7 +135,6 @@ let refine ?(unsafe = true) f = let with_type env evd c t = let my_type = Retyping.get_type_of env evd c in - let my_type = EConstr.of_constr my_type in let j = Environ.make_judge c my_type in let (evd,j') = Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d9caadd54e..7ffb30fa8d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -108,7 +108,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = pf_get_type_of gls %> EConstr.of_constr %> pf_whd_all gls +let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c @@ -234,7 +234,7 @@ module New = struct let pf_hnf_constr gl t = pf_apply hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) + pf_whd_all gl (pf_get_type_of gl t) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 06b3e39812..f0471bf660 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,7 +41,7 @@ val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> EConstr.constr -> types -val pf_type_of : goal sigma -> EConstr.constr -> evar_map * types +val pf_type_of : goal sigma -> EConstr.constr -> evar_map * EConstr.types val pf_hnf_type_of : goal sigma -> EConstr.constr -> EConstr.types val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t @@ -109,7 +109,7 @@ module New : sig val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types - val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * Term.types + val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * EConstr.types val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier -- cgit v1.2.3 From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 18:18:17 +0100 Subject: Ltac now uses evar-based constrs. --- proofs/clenv.ml | 5 ++--- proofs/redexpr.ml | 13 +++++++------ proofs/redexpr.mli | 1 + proofs/tacmach.ml | 2 +- 4 files changed, 11 insertions(+), 10 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 393e958d38..7269c61e3d 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -575,10 +575,9 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma (* Pretty-print *) let pr_clenv clenv = - let inj = EConstr.Unsafe.to_constr in h 0 - (str"TEMPL: " ++ print_constr (inj clenv.templval.rebus) ++ - str" : " ++ print_constr (inj clenv.templtyp.rebus) ++ fnl () ++ + (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ + str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ pr_evar_map (Some 2) clenv.evd) (****************************************************************) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 8878051c89..0fe5c73f15 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -11,6 +11,7 @@ open CErrors open Util open Names open Term +open EConstr open Declarations open Globnames open Genredexpr @@ -200,9 +201,6 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) -let out_with_occurrences' (occs,c) = - (Locusops.occurrences_map (List.map out_arg) occs, EConstr.of_constr c) - let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl @@ -242,8 +240,8 @@ let reduction_of_red_expr env = (e_red (strong_cbn (make_flag f)), DEFAULTcast) | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) - | Fold cl -> (e_red (fold_commands (List.map EConstr.of_constr cl)),DEFAULTcast) - | Pattern lp -> (pattern_occs (List.map out_with_occurrences' lp),DEFAULTcast) + | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) + | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> @@ -256,9 +254,12 @@ let reduction_of_red_expr env = in reduction_of_red_expr +let subst_mps subst c = + EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) + let subst_red_expr subs = Miscops.map_red_expr_gen - (Mod_subst.subst_mps subs) + (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) (Patternops.subst_pattern subs) diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index d4c2c4a6c9..45e4610661 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -10,6 +10,7 @@ open Names open Term +open EConstr open Pattern open Genredexpr open Reductionops diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 7ffb30fa8d..3641ad74d7 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -144,7 +144,7 @@ open Pp let db_pr_goal sigma g = let env = Goal.V82.env sigma g in let penv = print_named_context env in - let pc = print_constr_env env (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in + let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () -- cgit v1.2.3 From a5499688bd76def8de3d8e1089a49c7a08430903 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 14:54:40 +0100 Subject: Funind API using EConstr. --- proofs/goal.ml | 5 ++--- proofs/goal.mli | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/goal.ml b/proofs/goal.ml index 7499bc251b..410e738de7 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -49,7 +49,7 @@ module V82 = struct (* Access to ".evar_concl" *) let concl evars gl = let evi = Evd.find evars gl in - evi.Evd.evar_concl + EConstr.of_constr evi.Evd.evar_concl (* Access to ".evar_extra" *) let extra evars gl = @@ -146,6 +146,7 @@ module V82 = struct (* Goal represented as a type, doesn't take into account section variables *) let abstract_type sigma gl = + let open EConstr in let (gl,sigma) = nf_evar sigma gl in let env = env sigma gl in let genv = Global.env () in @@ -159,6 +160,4 @@ module V82 = struct t ) ~init:(concl sigma gl) env - let concl sigma gl = EConstr.of_constr (concl sigma gl) - end diff --git a/proofs/goal.mli b/proofs/goal.mli index ca6584e76d..a2fa34c05e 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -75,6 +75,6 @@ module V82 : sig val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map (* Goal represented as a type, doesn't take into account section variables *) - val abstract_type : Evd.evar_map -> goal -> Term.types + val abstract_type : Evd.evar_map -> goal -> EConstr.types end -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- proofs/clenv.ml | 2 +- proofs/evar_refiner.ml | 6 ++--- proofs/logic.ml | 2 +- proofs/tacmach.ml | 18 +++++++------- proofs/tacmach.mli | 65 +++++++++++++++++++++++++------------------------- 5 files changed, 47 insertions(+), 46 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 7269c61e3d..e580bccc3f 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -133,7 +133,7 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_type_of gls t = mk_clenv_from gls (t,EConstr.of_constr (pf_type_of gls t)) +let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) (******************************************************************) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0d65faf12c..1ddb67edd2 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -27,9 +27,9 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) = with NoHeadEvar -> false let define_and_solve_constraints evk c env evd = - if Termops.occur_evar evd evk (EConstr.of_constr c) then - Pretype_errors.error_occur_check env evd evk (EConstr.of_constr c); - let evd = define evk c evd in + 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,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in match List.fold_left diff --git a/proofs/logic.ml b/proofs/logic.ml index 8b890f6f81..59ce8ffa6d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -330,7 +330,7 @@ let meta_free_prefix sigma a = with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = - if !check then unsafe_type_of env sigma (EConstr.of_constr c) + if !check then EConstr.Unsafe.to_constr (unsafe_type_of env sigma (EConstr.of_constr c)) else EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)) let rec mk_refgoals sigma goal goalacc conclty trm = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 3641ad74d7..2fab026eab 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -46,11 +46,11 @@ let test_conversion cb env sigma c1 c2 = let c2 = EConstr.Unsafe.to_constr c2 in test_conversion cb env sigma c1 c2 -let pf_concl gls = EConstr.Unsafe.to_constr (Goal.V82.concl (project gls) (sig_it gls)) +let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls) let pf_hyps_types gls = let sign = Environ.named_context (pf_env gls) in List.map (function LocalAssum (id,x) - | LocalDef (id,_,x) -> id, x) + | LocalDef (id,_,x) -> id, EConstr.of_constr x) sign let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id @@ -64,7 +64,7 @@ let pf_get_hyp gls id = raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - id |> pf_get_hyp gls |> NamedDecl.get_type + id |> pf_get_hyp gls |> NamedDecl.get_type |> EConstr.of_constr let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -77,7 +77,7 @@ let pf_get_new_ids ids gls = (fun id acc -> (next_ident_away id (acc@avoid))::acc) ids [] -let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id +let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in @@ -103,7 +103,7 @@ let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL -let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) +let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c)) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind @@ -173,7 +173,7 @@ module New = struct (** We only check for the existence of an [id] in [hyps] *) let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in - Constrintern.construct_reference hyps id + EConstr.of_constr (Constrintern.construct_reference hyps id) let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl @@ -205,13 +205,13 @@ module New = struct sign let pf_get_hyp_typ id gl = - pf_get_hyp id gl |> NamedDecl.get_type + pf_get_hyp id gl |> NamedDecl.get_type |> EConstr.of_constr let pf_hyps_types gl = let env = Proofview.Goal.env gl in let sign = Environ.named_context env in List.map (function LocalAssum (id,x) - | LocalDef (id,_,x) -> id, x) + | LocalDef (id,_,x) -> id, EConstr.of_constr x) sign let pf_last_hyp gl = @@ -241,6 +241,6 @@ module New = struct let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t - let pf_nf_evar gl t = nf_evar (project gl) t + let pf_nf_evar gl t = EConstr.of_constr (nf_evar (project gl) (EConstr.Unsafe.to_constr t)) end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f0471bf660..efc3dbf550 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -9,6 +9,7 @@ open Names open Term open Environ +open EConstr open Evd open Proof_type open Redexpr @@ -40,9 +41,9 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_unsafe_type_of : goal sigma -> EConstr.constr -> types -val pf_type_of : goal sigma -> EConstr.constr -> evar_map * EConstr.types -val pf_hnf_type_of : goal sigma -> EConstr.constr -> EConstr.types +val pf_unsafe_type_of : goal sigma -> constr -> types +val pf_type_of : goal sigma -> constr -> evar_map * types +val pf_hnf_type_of : goal sigma -> constr -> types val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types @@ -50,7 +51,7 @@ val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list -val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * EConstr.constr +val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a @@ -63,35 +64,35 @@ val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> goal sigma -> constr -> evar_map * constr -val pf_whd_all : goal sigma -> EConstr.constr -> EConstr.constr -val pf_hnf_constr : goal sigma -> EConstr.constr -> EConstr.constr -val pf_nf : goal sigma -> EConstr.constr -> EConstr.constr -val pf_nf_betaiota : goal sigma -> EConstr.constr -> EConstr.constr -val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types -val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types -val pf_compute : goal sigma -> EConstr.constr -> EConstr.constr +val pf_whd_all : goal sigma -> constr -> constr +val pf_hnf_constr : goal sigma -> constr -> constr +val pf_nf : goal sigma -> constr -> constr +val pf_nf_betaiota : goal sigma -> constr -> constr +val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types +val pf_reduce_to_atomic_ind : goal sigma -> types -> pinductive * types +val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list - -> goal sigma -> EConstr.constr -> EConstr.constr + -> goal sigma -> constr -> constr val pf_const_value : goal sigma -> pconstant -> constr -val pf_conv_x : goal sigma -> EConstr.constr -> EConstr.constr -> bool -val pf_conv_x_leq : goal sigma -> EConstr.constr -> EConstr.constr -> bool +val pf_conv_x : goal sigma -> constr -> constr -> bool +val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool +val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map +val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool (** {6 The most primitive tactics. } *) val refiner : rule -> tactic -val internal_cut_no_check : bool -> Id.t -> EConstr.types -> tactic -val refine_no_check : EConstr.constr -> tactic +val internal_cut_no_check : bool -> Id.t -> types -> tactic +val refine_no_check : constr -> tactic (** {6 The most primitive tactics with consistency and type checking } *) -val internal_cut : bool -> Id.t -> EConstr.types -> tactic -val internal_cut_rev : bool -> Id.t -> EConstr.types -> tactic -val refine : EConstr.constr -> tactic +val internal_cut : bool -> Id.t -> types -> tactic +val internal_cut_rev : bool -> Id.t -> types -> tactic +val refine : constr -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.std_ppcmds @@ -106,11 +107,11 @@ module New : sig val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env - val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types - val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * EConstr.types - val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool + val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types + val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list @@ -120,16 +121,16 @@ module New : sig val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t - val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> EConstr.types - val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * EConstr.types + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types - val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types - val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr - val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr + val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr - val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr -- cgit v1.2.3 From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- proofs/pfedit.ml | 4 +++- proofs/pfedit.mli | 10 +++++----- proofs/proof.mli | 6 +++--- proofs/proof_global.ml | 5 +++-- proofs/proof_global.mli | 4 ++-- proofs/tacmach.ml | 4 ++-- 6 files changed, 18 insertions(+), 15 deletions(-) (limited to 'proofs') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index af910810ba..142fd9a899 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -199,6 +199,7 @@ let refine_by_tactic env sigma ty tac = | _ -> assert false in let ans = Reductionops.nf_evar sigma ans in + let ans = EConstr.Unsafe.to_constr ans in (** [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in (** Reset the old side-effects *) @@ -232,7 +233,8 @@ let solve_by_implicit_tactic env sigma evk = 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 - if Evarutil.has_undefined_evars sigma (EConstr.of_constr c) then raise Exit; + let c = EConstr.of_constr c in + if Evarutil.has_undefined_evars sigma c then raise Exit; let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in let sigma = Evd.set_universe_context sigma ctx in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 807a554dfd..516125ea18 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -60,7 +60,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards type universe_binders = Id.t Loc.located list val start_proof : - Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr -> + Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit @@ -106,7 +106,7 @@ val get_current_context : unit -> Evd.evar_map * env (** [current_proof_statement] *) val current_proof_statement : - unit -> Id.t * goal_kind * types + unit -> Id.t * goal_kind * EConstr.types (** {6 ... } *) (** [get_current_proof_name ()] return the name of the current focused @@ -166,15 +166,15 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> - types -> unit Proofview.tactic -> + EConstr.types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> - types -> unit Proofview.tactic -> + EConstr.types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context -val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic -> +val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> constr * Evd.evar_map (** A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other diff --git a/proofs/proof.mli b/proofs/proof.mli index 5053fc7fb9..8dcc5b76ec 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -66,9 +66,9 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre (*** General proof functions ***) -val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof +val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof val dependent_start : Proofview.telescope -> proof -val initial_goals : proof -> (Term.constr * Term.types) list +val initial_goals : proof -> (EConstr.constr * EConstr.types) list val initial_euctx : proof -> Evd.evar_universe_context (* Returns [true] if the considered proof is completed, that is if no goal remain @@ -79,7 +79,7 @@ val is_done : proof -> bool val is_complete : proof -> bool (* Returns the list of partial proofs to initial goals. *) -val partial_proof : proof -> Term.constr list +val partial_proof : proof -> EConstr.constr list val compact : proof -> proof diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2956d623fd..eb1bea8974 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -375,6 +375,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = in let entries = Future.map2 (fun p (_, t) -> + let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in { Entries. @@ -406,7 +407,7 @@ let return_proof ?(allow_partial=false) () = (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) - let proofs = List.map (fun c -> c, eff) proofs in + let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd end else let initial_goals = Proof.initial_goals proof in @@ -430,7 +431,7 @@ let return_proof ?(allow_partial=false) () = side-effects... This may explain why one need to uniquize side-effects thereafter... *) let proofs = - List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in + List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 97a21cf225..3b2cc6b23b 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -86,7 +86,7 @@ val apply_terminator : proof_terminator -> proof_ending -> unit end of the proof to close the proof. *) val start_proof : Evd.evar_map -> Names.Id.t -> ?pl:universe_binders -> - Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> + Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between @@ -201,7 +201,7 @@ end val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig - val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * + val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * Decl_kinds.goal_kind) end diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 2fab026eab..3ed262d6e8 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -223,7 +223,7 @@ module New = struct let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = project gl in - EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl)) + nf_evar sigma concl let pf_whd_all gl t = pf_apply whd_all gl t @@ -241,6 +241,6 @@ module New = struct let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t - let pf_nf_evar gl t = EConstr.of_constr (nf_evar (project gl) (EConstr.Unsafe.to_constr t)) + let pf_nf_evar gl t = nf_evar (project gl) t end -- cgit v1.2.3 From 78a8d59b39dfcb07b94721fdcfd9241d404905d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 15:30:02 +0100 Subject: Introducing contexts parameterized by the inner term type. This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms. --- proofs/pfedit.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 142fd9a899..09b924c7e6 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in (try -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- proofs/goal.ml | 1 + proofs/logic.ml | 21 +++++++++++++-------- proofs/logic.mli | 2 +- proofs/refiner.ml | 6 +++--- proofs/refiner.mli | 3 ++- proofs/tacmach.ml | 6 +++--- proofs/tacmach.mli | 10 +++++----- 7 files changed, 28 insertions(+), 21 deletions(-) (limited to 'proofs') diff --git a/proofs/goal.ml b/proofs/goal.ml index 410e738de7..9046f45341 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -155,6 +155,7 @@ module V82 = struct with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> if is_proof_var decl then + let decl = Termops.map_named_decl EConstr.of_constr decl in mkNamedProd_or_LetIn decl t else t diff --git a/proofs/logic.ml b/proofs/logic.ml index 59ce8ffa6d..a31cadd88c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -174,12 +174,14 @@ let reorder_context env sigma sign ord = step ord ords sign mt_q [] let reorder_val_context env sigma sign ord = + let open EConstr in val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) let check_decl_position env sigma sign d = + let open EConstr in let x = NamedDecl.get_id d in let needed = global_vars_set_of_decl env sigma d in let deps = dependency_closure env sigma (named_context_of_val sign) needed in @@ -266,6 +268,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = else moverec first' middle' right in + let open EConstr in if toleft then let right = List.fold_right push_named_context_val right empty_named_context_val in @@ -279,6 +282,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = right left let move_hyp_in_named_context sigma hfrom hto sign = + let open EConstr in let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in move_hyp sigma toleft (left,declfrom,right) hto @@ -507,7 +511,7 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in - let b = Option.map EConstr.of_constr (NamedDecl.get_value d) in + let b = NamedDecl.get_value d in let env = Global.env() in let reorder = ref [] in let sign' = @@ -515,14 +519,14 @@ let convert_hyp check sign sigma d = (fun _ d' _ -> let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in let env = Global.env_of_context sign in - if check && not (is_conv env sigma (EConstr.of_constr (NamedDecl.get_type d)) (EConstr.of_constr (NamedDecl.get_type d'))) then + if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the body of "++ pr_id id ++ str "."); if check then reorder := check_decl_position env sigma sign d; - d) in + map_named_decl EConstr.Unsafe.to_constr d) in reorder_val_context env sigma sign' !reorder @@ -535,15 +539,16 @@ let prim_refiner r sigma goal = let env = Goal.V82.env sigma goal in let sign = Goal.V82.hyps sigma goal in let cl = Goal.V82.concl sigma goal in - let cl = EConstr.Unsafe.to_constr cl in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let open EConstr in match r with (* Logical rules *) | Cut (b,replace,id,t) -> (* if !check && not (Retyping.get_sort_of env sigma t) then*) - let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in + let t = EConstr.of_constr t in + let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in let sign,t,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in @@ -556,14 +561,14 @@ let prim_refiner r sigma goal = user_err ~hdr:"Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in - let t = EConstr.of_constr t in let (sg2,ev2,sigma) = - Goal.V82.mk_goal sigma sign (EConstr.of_constr cl) (Goal.V82.extra sigma goal) in - let oterm = EConstr.mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in + Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in + let oterm = mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) | Refine c -> + let cl = EConstr.Unsafe.to_constr cl in check_meta_variables c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in diff --git a/proofs/logic.mli b/proofs/logic.mli index 5fe28ac76a..f98248e4d1 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -55,7 +55,7 @@ exception RefinerError of refiner_error val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> - Context.Named.Declaration.t -> Environ.named_context_val + EConstr.named_declaration -> Environ.named_context_val val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 9a0b56b84b..5c7659ac0e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -22,7 +22,7 @@ let project x = x.sigma (* Getting env *) let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) -let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) +let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) let refiner pr goal_sigma = let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in @@ -198,10 +198,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.Named.t = pf_hyps goal in + let oldhyps = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.Named.t list = + let hyps = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in let newhyps = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 6dcafb77a4..56f5facf89 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -10,6 +10,7 @@ open Evd open Proof_type +open EConstr (** The refiner (handles primitive rules and high-level tactics). *) @@ -17,7 +18,7 @@ val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> Context.Named.t +val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 3ed262d6e8..4b027a1273 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -64,7 +64,7 @@ let pf_get_hyp gls id = raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - id |> pf_get_hyp gls |> NamedDecl.get_type |> EConstr.of_constr + id |> pf_get_hyp gls |> NamedDecl.get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -199,13 +199,13 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.env gl in let sign = - try Environ.lookup_named id hyps + try EConstr.lookup_named id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign let pf_get_hyp_typ id gl = - pf_get_hyp id gl |> NamedDecl.get_type |> EConstr.of_constr + pf_get_hyp id gl |> NamedDecl.get_type let pf_hyps_types gl = let env = Proofview.Goal.env gl in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index efc3dbf550..3b23a6ab42 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,18 +34,18 @@ val apply_sig_tac : val pf_concl : goal sigma -> types val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> Context.Named.t +val pf_hyps : goal sigma -> named_context (*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> Context.Named.Declaration.t +val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t +val pf_get_hyp : goal sigma -> Id.t -> named_declaration val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t @@ -117,9 +117,9 @@ module New : sig val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types -- cgit v1.2.3 From d549d9d3d169fbfc5f555e3e4f22f46301161d53 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 16:30:00 +0100 Subject: Do not ask for a normalized goal to get hypotheses and conclusions. This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization. --- proofs/tacmach.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'proofs') diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3b23a6ab42..1992cec65c 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -107,19 +107,19 @@ module New : sig val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env - val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_concl : ('a, 'r) Proofview.Goal.t -> types val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool - val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier + val pf_get_new_id : identifier -> ('a, 'r) Proofview.Goal.t -> identifier val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration + val pf_get_hyp : identifier -> ('a, 'r) Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : identifier -> ('a, 'r) Proofview.Goal.t -> types + val pf_last_hyp : ('a, 'r) Proofview.Goal.t -> named_declaration val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types -- cgit v1.2.3 From 390fd4ac0a969103caeb5db3e5138e26f9a533de Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 17:49:11 +0100 Subject: Chasing a few unsafe constr coercions. --- proofs/tacmach.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4b027a1273..97c5cda770 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -41,10 +41,8 @@ let project = Refiner.project let pf_env = Refiner.pf_env let pf_hyps = Refiner.pf_hyps -let test_conversion cb env sigma c1 c2 = - let c1 = EConstr.Unsafe.to_constr c1 in - let c2 = EConstr.Unsafe.to_constr c2 in - test_conversion cb env sigma c1 c2 +let test_conversion env sigma pb c1 c2 = + Reductionops.check_conv ~pb env sigma c1 c2 let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls) let pf_hyps_types gls = -- cgit v1.2.3 From 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 23:48:28 +0100 Subject: Moving printing code from Evd to Termops. --- proofs/evar_refiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 1ddb67edd2..59a41792a0 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -58,6 +58,6 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let loc = Glob_ops.loc_of_glob_constr rawc in user_err ~loc (str "Instance is not well-typed in the environment of " ++ - pr_existential_key sigma evk ++ str ".") + Termops.pr_existential_key sigma evk ++ str ".") in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) -- cgit v1.2.3 From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: Namegen primitives now apply on evar constrs. Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. --- proofs/clenv.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index e580bccc3f..5645850b23 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -555,7 +555,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let clause = mk_clenv_from_env env sigma n (c,t) in clenv_constrain_dep_args hyps_only largs clause | ExplicitBindings lbind -> - let t = EConstr.of_constr (rename_bound_vars_as_displayed [] [] (EConstr.Unsafe.to_constr t)) in + let t = rename_bound_vars_as_displayed sigma [] [] t in let clause = mk_clenv_from_env env sigma n (c, t) in clenv_match_args lbind clause @@ -603,9 +603,7 @@ let make_evar_clause env sigma ?len t = | Some n -> assert (0 <= n); n in (** FIXME: do the renaming online *) - let t = EConstr.Unsafe.to_constr t in - let t = rename_bound_vars_as_displayed [] [] t in - let t = EConstr.of_constr t in + let t = rename_bound_vars_as_displayed sigma [] [] t in let rec clrec (sigma, holes) n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with -- cgit v1.2.3 From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Dec 2016 10:45:19 +0100 Subject: Removing most nf_enter in tactics. Now they are useless because all of the primitives are (should?) be evar-insensitive. --- proofs/clenv.ml | 17 +++++++++++++---- proofs/clenv.mli | 11 +++++++---- proofs/clenvtac.ml | 4 ++-- 3 files changed, 22 insertions(+), 10 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 5645850b23..f9ebc42330 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -129,11 +129,13 @@ let mk_clenv_from_env env sigma n (c,cty) = env = env } let mk_clenv_from_n gls n (c,cty) = - mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty) + let env = Proofview.Goal.env gls in + let sigma = Tacmach.New.project gls in + mk_clenv_from_env env sigma n (c, cty) let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) +let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t) (******************************************************************) @@ -263,8 +265,7 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv = let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } -let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = - let concl = Goal.V82.concl clenv.evd (sig_it gl) in +let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) @@ -272,6 +273,14 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = clenv_unify CUMUL ~flags (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv +let old_clenv_unique_resolver ?flags clenv gl = + let concl = Goal.V82.concl clenv.evd (sig_it gl) in + clenv_unique_resolver_gen ?flags clenv concl + +let clenv_unique_resolver ?flags clenv gl = + let concl = Proofview.Goal.concl gl in + clenv_unique_resolver_gen ?flags clenv concl + let adjust_meta_source evd mv = function | loc,Evar_kinds.VarInstance id -> let rec match_name c l = diff --git a/proofs/clenv.mli b/proofs/clenv.mli index f7ff4bed34..4bcd50591c 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -41,10 +41,10 @@ val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types -val mk_clenv_from : Goal.goal sigma -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : - Goal.goal sigma -> int option -> EConstr.constr * EConstr.types -> clausenv -val mk_clenv_type_of : Goal.goal sigma -> EConstr.constr -> clausenv + ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) @@ -62,9 +62,12 @@ val clenv_unify : ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv (** unifies the concl of the goal with the type of the clenv *) -val clenv_unique_resolver : +val old_clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv +val clenv_unique_resolver : + ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv + val clenv_dependent : clausenv -> metavariable list val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 32c887ff59..0722ea0470 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -105,8 +105,8 @@ let dft = default_unify_flags let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = Proofview.Goal.enter { enter = begin fun gl -> - let clenv gl = clenv_unique_resolver ~flags clenv gl in - clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl)) + let clenv = clenv_unique_resolver ~flags clenv gl in + clenv_refine with_evars ~with_classes clenv end } (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en -- cgit v1.2.3 From 1cf91df6e0617c316dff7d99c7603a26b694e647 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 29 Mar 2017 16:04:15 +0200 Subject: Fix call to broken unsafe_type_of in apply tactic. This broke the build of iris-coq in the EConstr branch. Each time you use unsafe_type_of, I loose a night of sleep, so please stop. --- proofs/logic.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index a31cadd88c..b38a901c2f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -334,8 +334,10 @@ let meta_free_prefix sigma a = with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = - if !check then EConstr.Unsafe.to_constr (unsafe_type_of env sigma (EConstr.of_constr c)) - else EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)) + if !check then + let (sigma,t) = type_of env sigma (EConstr.of_constr c) in + (sigma, EConstr.Unsafe.to_constr t) + else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in @@ -418,7 +420,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | _ -> if occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refiner called with a meta in non app/case subterm"); - let t'ty = goal_type_of env sigma trm in + let (sigma, t'ty) = goal_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma, trm) @@ -478,7 +480,8 @@ and mk_hdgoals sigma goal goalacc trm = | _ -> if !check && occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refine called with a dependent meta"); - goalacc, goal_type_of env sigma trm, sigma, trm + let (sigma, ty) = goal_type_of env sigma trm in + goalacc, ty, sigma, trm and mk_arggoals sigma goal goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = -- cgit v1.2.3 From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- proofs/logic.ml | 3 ++- proofs/tacmach.mli | 6 +++--- 2 files changed, 5 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index b38a901c2f..e6024785db 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -505,9 +505,10 @@ and mk_casegoals sigma goal goalacc p c = let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in let ct = EConstr.of_constr ct in let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in - let indspec = + let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals") in + let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 1b05bc7d63..627a8e0e7e 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -68,8 +68,8 @@ val pf_whd_all : goal sigma -> constr -> constr val pf_hnf_constr : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr val pf_nf_betaiota : goal sigma -> constr -> constr -val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types -val pf_reduce_to_atomic_ind : goal sigma -> types -> pinductive * types +val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types +val pf_reduce_to_atomic_ind : goal sigma -> types -> (inductive * EInstance.t) * types val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list -> goal sigma -> constr -> constr @@ -131,7 +131,7 @@ module New : sig val pf_last_hyp : ('a, 'r) Proofview.Goal.t -> named_declaration val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> (inductive * EInstance.t) * types val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types -- cgit v1.2.3