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. --- pretyping/evarconv.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d06009dce5..194d0b297c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -141,9 +141,10 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = match kind_of_term t2 with Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd (Evarutil.nf_evar sigma t2) in - if dependent (mkRel 1) b then raise Not_found - else lookup_canonical_conversion (proji, Prod_cs), - (Stack.append_app [|a;pop b|] Stack.empty) + if EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) then + lookup_canonical_conversion (proji, Prod_cs), + (Stack.append_app [|a;pop (EConstr.of_constr b)|] Stack.empty) + else raise Not_found | Sort s -> lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] @@ -178,7 +179,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let c' = subst_univs_level_constr subst c in let t' = subst_univs_level_constr subst t' in let bs' = List.map (subst_univs_level_constr subst) bs in - let h, _ = decompose_app_vect t' in + let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, (n,Stack.zip(t2,sk2)) @@ -372,7 +373,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = nf_evar evd tM in - let t2 = solve_pattern_eqn env l1' t2 in + let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (evar_conv_x ts) env evd (position_problem on_left pbty,ev,t2) in @@ -893,7 +894,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); test; (fun i -> evar_conv_x trs env i CONV h2 - (fst (decompose_app_vect (substl ks h))))] + (fst (decompose_app_vect i (EConstr.of_constr (substl ks h)))))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = @@ -973,14 +974,14 @@ let apply_on_subterm env evdref f c t = in applyrec (env,(0,c)) t -let filter_possible_projections c ty ctxt args = +let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the fv of args to have a well-typed filter; don't know how necessary it is however to have a well-typed filter here *) - let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in - let fv2 = collect_vars (mkApp (c,args)) in + let fv1 = free_rels evd (EConstr.of_constr (mkApp (c,args))) (* Hack: locally untyped *) in + let fv2 = collect_vars evd (EConstr.of_constr (mkApp (c,args))) in let len = Array.length args in - let tyvars = collect_vars ty in + let tyvars = collect_vars evd (EConstr.of_constr ty) in List.map_i (fun i decl -> let () = assert (i < len) in let a = Array.unsafe_get args i in @@ -1039,7 +1040,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let t = NamedDecl.get_type decl' in let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in - let filter' = filter_possible_projections c ty ctxt args in + let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in -- 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. --- pretyping/evarconv.ml | 177 ++++++++++++++++++++++++++++---------------------- 1 file changed, 98 insertions(+), 79 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 194d0b297c..f54a57d57d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -78,6 +78,7 @@ type flex_kind_of_term = | Flexible of existential let flex_kind_of_term ts env evd c sk = + let c = EConstr.Unsafe.to_constr c in match kind_of_term c with | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c) @@ -88,10 +89,12 @@ let flex_kind_of_term ts env evd c sk = | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false +let zip evd (c, stk) = EConstr.Unsafe.to_constr (Stack.zip evd (c, stk)) + let apprec_nohdbeta ts env evd c = - let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in + let (t,sk as appr) = Reductionops.whd_nored_state evd (EConstr.of_constr c, []) in if Stack.not_purely_applicative sk - then Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state + then zip evd (fst (whd_betaiota_deltazeta_for_iota_state ts env evd Cst_stack.empty appr)) else c @@ -135,6 +138,8 @@ let occur_rigidly (evk,_ as ev) evd t = projection would have been reduced) *) let check_conv_record env sigma (t1,sk1) (t2,sk2) = + let t1 = EConstr.Unsafe.to_constr t1 in + let t2 = EConstr.Unsafe.to_constr t2 in let (proji, u), arg = Universes.global_app_of_constr t1 in let canon_s,sk2_effective = try @@ -143,7 +148,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let _, a, b = destProd (Evarutil.nf_evar sigma t2) in if EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) then lookup_canonical_conversion (proji, Prod_cs), - (Stack.append_app [|a;pop (EConstr.of_constr b)|] Stack.empty) + (Stack.append_app [|EConstr.of_constr a;EConstr.of_constr (pop (EConstr.of_constr b))|] Stack.empty) else raise Not_found | Sort s -> lookup_canonical_conversion @@ -162,12 +167,12 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Some c -> (* A primitive projection applied to c *) let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = - try Inductiveops.find_mrectype env sigma ty + try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) with _ -> raise Not_found - in Stack.append_app_list ind_args Stack.empty, c, sk1 + in Stack.append_app_list (List.map EConstr.of_constr ind_args) Stack.empty, c, sk1 | None -> match Stack.strip_n_app nparams sk1 with - | Some (params1, c1, extra_args1) -> params1, c1, extra_args1 + | Some (params1, c1, extra_args1) -> params1, EConstr.Unsafe.to_constr c1, extra_args1 | _ -> raise Not_found in let us2,extra_args2 = let l_us = List.length us in @@ -180,9 +185,9 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let t' = subst_univs_level_constr subst t' in let bs' = List.map (subst_univs_level_constr subst) bs in let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in - ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), - (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, - (n,Stack.zip(t2,sk2)) + ctx',(h, t2),c',bs',(Stack.append_app_list (List.map EConstr.of_constr params) Stack.empty,params1), + (Stack.append_app_list (List.map EConstr.of_constr us) Stack.empty,us2),(extra_args1,extra_args2),c1, + (n, zip sigma (EConstr.of_constr t2,sk2)) (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) @@ -212,10 +217,11 @@ let ise_exact ise x1 x2 = | Some _, Success i -> UnifFailure (i,NotSameArgSize) let ise_array2 evd f v1 v2 = + let inj c = EConstr.Unsafe.to_constr c in let rec allrec i = function | -1 -> Success i | n -> - match f i v1.(n) v2.(n) with + match f i (inj v1.(n)) (inj v2.(n)) with | Success i' -> allrec i' (n-1) | UnifFailure _ as x -> x in let lv1 = Array.length v1 in @@ -225,28 +231,35 @@ let ise_array2 evd f v1 v2 = (* Applicative node of stack are read from the outermost to the innermost but are unified the other way. *) let rec ise_app_stack2 env f evd sk1 sk2 = + let inj = EConstr.Unsafe.to_constr in match sk1,sk2 with | Stack.App node1 :: q1, Stack.App node2 :: q2 -> let (t1,l1) = Stack.decomp_node_last node1 q1 in let (t2,l2) = Stack.decomp_node_last node2 q2 in begin match ise_app_stack2 env f evd l1 l2 with |(_,UnifFailure _) as x -> x - |x,Success i' -> x,f env i' CONV t1 t2 + |x,Success i' -> x,f env i' CONV (inj t1) (inj t2) end | _, _ -> (sk1,sk2), Success evd +let push_rec_types pfix env = + let (i, c, t) = pfix in + let inj c = EConstr.Unsafe.to_constr c in + push_rec_types (i, Array.map inj c, Array.map inj t) env + (* This function tries to unify 2 stacks element by element. It works from the end to the beginning. If it unifies a non empty suffix of stacks but not the entire stacks, the first part of the answer is Some(the remaining prefixes to tackle)) *) let ise_stack2 no_app env evd f sk1 sk2 = + let inj = EConstr.Unsafe.to_constr in let rec ise_stack2 deep i sk1 sk2 = let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i else None, x in match sk1, sk2 with | [], [] -> None, Success i | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 -> - (match f env i CONV t1 t2 with + (match f env i CONV (inj t1) (inj t2) with | Success i' -> (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with | Success i'' -> ise_stack2 true i'' q1 q2 @@ -279,6 +292,7 @@ let ise_stack2 no_app env evd f sk1 sk2 = (* Make sure that the matching suffix is the all stack *) let exact_ise_stack2 env evd f sk1 sk2 = + let inj = EConstr.Unsafe.to_constr in let rec ise_stack2 i sk1 sk2 = match sk1, sk2 with | [], [] -> Success i @@ -286,7 +300,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_and i [ (fun i -> ise_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2); - (fun i -> f env i CONV t1 t2)] + (fun i -> f env i CONV (inj t1) (inj t2))] | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 -> if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then @@ -344,19 +358,19 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let term2 = apprec_nohdbeta (fst ts) env evd term2 in let default () = evar_eqappr_x ts env evd pbty - (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty) - (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty) + (whd_nored_state evd (EConstr.of_constr term1,Stack.empty), Cst_stack.empty) + (whd_nored_state evd (EConstr.of_constr term2,Stack.empty), Cst_stack.empty) in begin match kind_of_term term1, kind_of_term term2 with | Evar ev, _ when Evd.is_undefined evd (fst ev) -> (match solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,ev,term2) with + (position_problem true pbty,ev, EConstr.of_constr term2) with | UnifFailure (_,OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) | _, Evar ev when Evd.is_undefined evd (fst ev) -> (match solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,ev,term1) with + (position_problem false pbty,ev, EConstr.of_constr term1) with | UnifFailure (_, OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) @@ -369,23 +383,25 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (i, NotSameHead) in let miller_pfenning on_left fallback ev lF tM evd = + let lF = List.map EConstr.Unsafe.to_constr lF in match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = nf_evar evd tM in let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (evar_conv_x ts) env evd - (position_problem on_left pbty,ev,t2) + (position_problem on_left pbty,ev, EConstr.of_constr t2) in let consume_stack on_left (termF,skF) (termO,skO) evd = + let inj = EConstr.Unsafe.to_constr in let switch f a b = if on_left then f a b else f b a in let not_only_app = Stack.not_purely_applicative skO in match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) + switch (evar_conv_x ts env i' pbty) (zip evd (termF,l)) (zip evd (termO,r)) |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) - |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO + switch (evar_conv_x ts env i' pbty) (zip evd (termF,l)) (zip evd (termO,r)) + |None, Success i' -> switch (evar_conv_x ts env i' pbty) (inj termF) (inj termO) |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) in let eta env evd onleft sk term sk' term' = @@ -394,15 +410,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let c = nf_evar evd c1 in let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state - (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in + (fst ts) env' evd Cst_stack.empty (EConstr.of_constr c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), + (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let univs = Universes.eq_constr_universes term term' in + let univs = EConstr.eq_constr_universes evd term term' in match univs with | Some univs -> ise_and evd [(fun i -> @@ -420,10 +436,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty match Stack.list_of_app_stack skF with | None -> quick_fail evd | Some lF -> - let tM = Stack.zip apprM in + let tM = zip evd apprM in miller_pfenning on_left (fun () -> if not_only_app then (* Postpone the use of an heuristic *) - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (zip evd apprF) tM else quick_fail i) ev lF tM i and consume (termF,skF as apprF) (termM,skM as apprM) i = @@ -437,7 +453,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in let default i = ise_try i [f1; consume apprF apprM; delta] in - match kind_of_term termM with + match EConstr.kind evd termM with | Proj (p, c) when not (Stack.is_empty skF) -> (* Might be ?X args = p.c args', and we have to eta-expand the primitive projection if |args| >= |args'|+1. *) @@ -448,10 +464,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else let f = try - let termM' = Retyping.expand_projection env evd p c [] in + let termM' = Retyping.expand_projection env evd p (EConstr.Unsafe.to_constr c) [] in let apprM', cstsM' = whd_betaiota_deltazeta_for_iota_state - (fst ts) env evd cstsM (termM',skM) + (fst ts) env evd cstsM (EConstr.of_constr termM',skM) in let delta' i = switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') @@ -467,9 +483,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in let eta evd = - match kind_of_term termR with + match EConstr.kind evd termR with | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> - eta env evd false skR termR skF termF + eta env evd false skR (EConstr.Unsafe.to_constr termR) skF termF | Construct u -> eta_constructor ts env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in @@ -477,7 +493,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None -> ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> - let tR = Stack.zip apprR in + let tR = zip evd apprR in miller_pfenning on_left (fun () -> ise_try evd @@ -487,10 +503,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let i,tF = if isRel tR || isVar tR then (* Optimization so as to generate candidates *) - let i,ev = evar_absorb_arguments env i ev lF in + let i,ev = evar_absorb_arguments env i ev (List.map EConstr.Unsafe.to_constr lF) in i,mkEvar ev else - i,Stack.zip apprF in + i,zip evd apprF in switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) tF tR else @@ -516,20 +532,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let ev1' = whd_evar i' (mkEvar ev1) in if isEvar ev1' then solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar ev1',term2) + (position_problem true pbty,destEvar ev1', term2) else evar_eqappr_x ts env evd pbty - ((ev1', sk1), csts1) ((term2, sk2), csts2) + ((EConstr.of_constr ev1', sk1), csts1) ((term2, sk2), csts2) | Some (r,[]), Success i' -> (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) (* we now unify r[?ev1] and ?ev2 *) let ev2' = whd_evar i' (mkEvar ev2) in if isEvar ev2' then solve_simple_eqn (evar_conv_x ts) env i' - (position_problem false pbty,destEvar ev2',Stack.zip(term1,r)) + (position_problem false pbty,destEvar ev2',Stack.zip evd (term1,r)) else evar_eqappr_x ts env evd pbty - ((ev2', sk1), csts1) ((term2, sk2), csts2) + ((EConstr.of_constr ev2', sk1), csts1) ((term2, sk2), csts2) | Some ([],r), Success i' -> (* Symmetrically *) (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) @@ -537,9 +553,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let ev1' = whd_evar i' (mkEvar ev1) in if isEvar ev1' then solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar ev1',Stack.zip(term2,r)) + (position_problem true pbty,destEvar ev1',Stack.zip evd (term2,r)) else evar_eqappr_x ts env evd pbty - ((ev1', sk1), csts1) ((term2, sk2), csts2) + ((EConstr.of_constr ev1', sk1), csts1) ((term2, sk2), csts2) | None, (UnifFailure _ as x) -> (* sk1 and sk2 have no common outer part *) if Stack.not_purely_applicative sk2 then @@ -584,13 +600,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] | Flexible ev1, MaybeFlexible v2 -> - flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2 + flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) (EConstr.of_constr v2) | MaybeFlexible v1, Flexible ev2 -> - flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1 + flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) (EConstr.of_constr v1) | MaybeFlexible v1, MaybeFlexible v2 -> begin - match kind_of_term term1, kind_of_term term2 with + match kind_of_term (EConstr.Unsafe.to_constr term1), kind_of_term (EConstr.Unsafe.to_constr term2) with | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> let f1 i = (* FO *) ise_and i @@ -605,8 +621,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) + let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (EConstr.of_constr v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (EConstr.of_constr v2,sk2) in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1; f2] @@ -618,8 +634,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c c'); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) + let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (EConstr.of_constr v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (EConstr.of_constr v2,sk2) in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1; f2] @@ -627,7 +643,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Catch the p.c ~= p c' cases *) | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> let res = - try Some (destApp (Retyping.expand_projection env evd p c [])) + try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c []))) with Retyping.RetypeError _ -> None in (match res with @@ -638,7 +654,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> let res = - try Some (destApp (Retyping.expand_projection env evd p' c' [])) + try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' []))) with Retyping.RetypeError _ -> None in (match res with @@ -653,7 +669,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty allow this identification (first-order unification of universes). Otherwise fallback to unfolding. *) - let univs = Universes.eq_constr_universes term1 term2 in + let univs = EConstr.eq_constr_universes evd term1 term2 in match univs with | Some univs -> ise_and i [(fun i -> @@ -675,7 +691,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if the first argument is a beta-redex (expand a constant only if necessary) or the second argument is potentially usable as a canonical projection or canonical value *) - let rec is_unnamed (hd, args) = match kind_of_term hd with + let rec is_unnamed (hd, args) = match EConstr.kind i hd with | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) -> Stack.not_purely_applicative args | (CoFix _|Meta _|Rel _)-> true @@ -684,7 +700,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Lambda _ -> assert (match args with [] -> true | _ -> false); true | LetIn (_,b,_,c) -> is_unnamed (fst (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i Cst_stack.empty (subst1 b c, args))) + (fst ts) env i Cst_stack.empty (EConstr.Vars.subst1 b c, args))) | Fix _ -> true (* Partially applied fix can be the result of a whd call *) | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args | Case _ | App _| Cast _ -> assert false in @@ -692,34 +708,35 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let applicative_stack = fst (Stack.strip_app sk2) in is_unnamed (fst (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in + (fst ts) env i Cst_stack.empty (EConstr.of_constr v2, applicative_stack))) in let rhs_is_already_stuck = rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in - if (isLambda term1 || rhs_is_already_stuck) + if (EConstr.isLambda i term1 || rhs_is_already_stuck) && (not (Stack.not_purely_applicative sk1)) then evar_eqappr_x ~rhs_is_already_stuck ts env i pbty (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) + (fst ts) env i (Cst_stack.add_cst term1 csts1) (EConstr.of_constr v1,sk1)) (appr2,csts2) else evar_eqappr_x ts env i pbty (appr1,csts1) (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) + (fst ts) env i (Cst_stack.add_cst term2 csts2) (EConstr.of_constr v2,sk2)) in ise_try evd [f1; f2; f3] end - | Rigid, Rigid when isLambda term1 && isLambda term2 -> - let (na1,c1,c'1) = destLambda term1 in - let (na2,c2,c'2) = destLambda term2 in + | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 -> + let (na1,c1,c'1) = EConstr.destLambda evd term1 in + let (na2,c2,c'2) = EConstr.destLambda evd term2 in + let inj = EConstr.Unsafe.to_constr in assert app_empty; ise_and evd - [(fun i -> evar_conv_x ts env i CONV c1 c2); + [(fun i -> evar_conv_x ts env i CONV (inj c1) (inj c2)); (fun i -> - let c = nf_evar i c1 in + let c = nf_evar i (inj c1) in let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] + evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV (inj c'1) (inj c'2))] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 @@ -733,7 +750,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty and f4 i = evar_eqappr_x ts env i pbty (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) + (fst ts) env i (Cst_stack.add_cst term1 csts1) (EConstr.of_constr v1,sk1)) (appr2,csts2) in ise_try evd [f3; f4] @@ -747,19 +764,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty and f4 i = evar_eqappr_x ts env i pbty (appr1,csts1) (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) + (fst ts) env i (Cst_stack.add_cst term2 csts2) (EConstr.of_constr v2,sk2)) in ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 -> - eta env evd true sk1 term1 sk2 term2 + | Rigid, _ when EConstr.isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> + eta env evd true sk1 (EConstr.Unsafe.to_constr term1) sk2 term2 - | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 -> - eta env evd false sk2 term2 sk1 term1 + | _, Rigid when EConstr.isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> + eta env evd false sk2 (EConstr.Unsafe.to_constr term2) sk1 term1 | Rigid, Rigid -> begin - match kind_of_term term1, kind_of_term term2 with + let inj = EConstr.Unsafe.to_constr in + match EConstr.kind evd term1, EConstr.kind evd term2 with | Sort s1, Sort s2 when app_empty -> (try @@ -774,11 +792,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd - [(fun i -> evar_conv_x ts env i CONV c1 c2); + [(fun i -> evar_conv_x ts env i CONV (inj c1) (inj c2)); (fun i -> - let c = nf_evar i c1 in + let c = nf_evar i (inj c1) in let na = Nameops.name_max n1 n2 in - evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] + evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty (inj c'1) (inj c'2))] | Rel x1, Rel x2 -> if Int.equal x1 x2 then @@ -822,10 +840,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else UnifFailure (evd,NotSameHead) | (Meta _, _) | (_, Meta _) -> + let inj = EConstr.Unsafe.to_constr in begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with |_, (UnifFailure _ as x) -> x - |None, Success i' -> evar_conv_x ts env i' CONV term1 term2 - |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2')) + |None, Success i' -> evar_conv_x ts env i' CONV (inj term1) (inj term2) + |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (inj (Stack.zip i' (term1,sk1'))) (inj (Stack.zip i' (term2,sk2'))) end | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ -> @@ -905,8 +924,8 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = (try let l1' = Stack.tail pars sk1 in let l2' = - let term = Stack.zip (term2,sk2) in - List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs) + let term = Stack.zip evd (term2,sk2) in + List.map (fun p -> EConstr.mkProj (Projection.make p false, term)) (Array.to_list projs) in exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' (Stack.append_app_list l2' Stack.empty) @@ -938,14 +957,14 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) = let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in ise_and evd (* First compare extra args for better failure message *) - [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1); + [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) (Array.map EConstr.of_constr rest2) (Array.map EConstr.of_constr l1)); (fun i -> (* Then instantiate evar unless already done by unifying args *) let t2 = mkApp(term2,deb2) in if is_defined i (fst ev1) then evar_conv_x ts env i CONV t2 (mkEvar ev1) else - solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))] + solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1, EConstr.of_constr t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in @@ -1153,7 +1172,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in + let f env evd pbty x y = is_fconv ~reds:ts pbty env evd (EConstr.of_constr x) (EConstr.of_constr y) in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> -- 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. --- pretyping/evarconv.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f54a57d57d..47db71cc65 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -165,7 +165,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let params1, c1, extra_args1 = match arg with | Some c -> (* A primitive projection applied to c *) - let ty = Retyping.get_type_of ~lax:true env sigma c in + let ty = Retyping.get_type_of ~lax:true env sigma (EConstr.of_constr c) in let (i,u), ind_args = try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) with _ -> raise Not_found @@ -464,7 +464,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else let f = try - let termM' = Retyping.expand_projection env evd p (EConstr.Unsafe.to_constr c) [] in + let termM' = Retyping.expand_projection env evd p c [] in let apprM', cstsM' = whd_betaiota_deltazeta_for_iota_state (fst ts) env evd cstsM (EConstr.of_constr termM',skM) @@ -643,7 +643,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Catch the p.c ~= p c' cases *) | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> let res = - try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c []))) + try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p (EConstr.of_constr c) []))) with Retyping.RetypeError _ -> None in (match res with @@ -654,7 +654,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> let res = - try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' []))) + try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' (EConstr.of_constr c') []))) with Retyping.RetypeError _ -> None in (match res with @@ -888,7 +888,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) List.fold_left (fun (i,ks,m,test) b -> if match n with Some n -> Int.equal m n | None -> false then - let ty = Retyping.get_type_of env i t2 in + let ty = Retyping.get_type_of env i (EConstr.of_constr t2) in let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else @@ -1058,7 +1058,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let id = NamedDecl.get_id decl' in let t = NamedDecl.get_type decl' in let evs = ref [] in - let ty = Retyping.get_type_of env_rhs evd c in + let ty = Retyping.get_type_of env_rhs evd (EConstr.of_constr c) in let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] -- cgit v1.2.3 From 147afe827dc83602cc160a8b1357e84ecea910ff Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Nov 2016 20:13:32 +0100 Subject: Evardefine API using EConstr. --- pretyping/evarconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 47db71cc65..4540af28b9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -503,7 +503,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let i,tF = if isRel tR || isVar tR then (* Optimization so as to generate candidates *) - let i,ev = evar_absorb_arguments env i ev (List.map EConstr.Unsafe.to_constr lF) in + let i,ev = evar_absorb_arguments env i (fst ev, Array.map EConstr.of_constr (snd ev)) lF in i,mkEvar ev else i,zip evd apprF in -- cgit v1.2.3 From b7fd585b89ac5e0b7770f52739c33fe179f2eed8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Nov 2016 21:36:40 +0100 Subject: Evarsolve API using EConstr. --- pretyping/evarconv.ml | 85 +++++++++++++++++++++++++++------------------------ 1 file changed, 45 insertions(+), 40 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4540af28b9..8f3f671abf 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -42,6 +42,9 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } +let to_conv_fun f = (); fun env sigma pb c1 c2 -> + f env sigma pb (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) + let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then @@ -341,7 +344,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = env evd term1 term2 in if b then Success evd - else UnifFailure (evd, ConversionFailed (env,term1,term2)) + else UnifFailure (evd, ConversionFailed (env,EConstr.of_constr term1,EConstr.of_constr term2)) with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with @@ -361,15 +364,15 @@ let rec evar_conv_x ts env evd pbty term1 term2 = (whd_nored_state evd (EConstr.of_constr term1,Stack.empty), Cst_stack.empty) (whd_nored_state evd (EConstr.of_constr term2,Stack.empty), Cst_stack.empty) in - begin match kind_of_term term1, kind_of_term term2 with + begin match EConstr.kind evd (EConstr.of_constr term1), EConstr.kind evd (EConstr.of_constr term2) with | Evar ev, _ when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (evar_conv_x ts) env evd + (match solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd (position_problem true pbty,ev, EConstr.of_constr term2) with | UnifFailure (_,OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) | _, Evar ev when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (evar_conv_x ts) env evd + (match solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd (position_problem false pbty,ev, EConstr.of_constr term1) with | UnifFailure (_, OccurCheck _) -> (* Eta-expansion might apply *) default () @@ -383,13 +386,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (i, NotSameHead) in let miller_pfenning on_left fallback ev lF tM evd = - let lF = List.map EConstr.Unsafe.to_constr lF in match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) - let t2 = nf_evar evd tM in + let t2 = EConstr.of_constr (nf_evar evd (EConstr.Unsafe.to_constr tM)) (** FIXME *) in let t2 = solve_pattern_eqn env evd l1' t2 in - solve_simple_eqn (evar_conv_x ts) env evd + solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd (position_problem on_left pbty,ev, EConstr.of_constr t2) in let consume_stack on_left (termF,skF) (termO,skO) evd = @@ -441,7 +443,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun () -> if not_only_app then (* Postpone the use of an heuristic *) switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (zip evd apprF) tM else quick_fail i) - ev lF tM i + ev lF (EConstr.of_constr tM) i and consume (termF,skF as apprF) (termM,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then consume_stack on_left apprF apprM i @@ -510,8 +512,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) tF tR else - UnifFailure (evd,OccurCheck (fst ev,tR)))]) - ev lF tR evd + UnifFailure (evd,OccurCheck (fst ev,EConstr.of_constr tR)))]) + (fst ev, Array.map EConstr.of_constr (snd ev)) lF (EConstr.of_constr tR) evd in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) @@ -529,33 +531,33 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None, Success i' -> (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) - let ev1' = whd_evar i' (mkEvar ev1) in - if isEvar ev1' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar ev1', term2) + let ev1' = EConstr.of_constr (whd_evar i' (mkEvar ev1)) in + if EConstr.isEvar i' ev1' then + solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' + (position_problem true pbty,EConstr.destEvar i' ev1', term2) else evar_eqappr_x ts env evd pbty - ((EConstr.of_constr ev1', sk1), csts1) ((term2, sk2), csts2) + ((ev1', sk1), csts1) ((term2, sk2), csts2) | Some (r,[]), Success i' -> (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) (* we now unify r[?ev1] and ?ev2 *) - let ev2' = whd_evar i' (mkEvar ev2) in - if isEvar ev2' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem false pbty,destEvar ev2',Stack.zip evd (term1,r)) + let ev2' = EConstr.of_constr (whd_evar i' (mkEvar ev2)) in + if EConstr.isEvar i' ev2' then + solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' + (position_problem false pbty,EConstr.destEvar i' ev2',Stack.zip evd (term1,r)) else evar_eqappr_x ts env evd pbty - ((EConstr.of_constr ev2', sk1), csts1) ((term2, sk2), csts2) + ((ev2', sk1), csts1) ((term2, sk2), csts2) | Some ([],r), Success i' -> (* Symmetrically *) (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) (* we now unify ?ev1 and r[?ev2] *) - let ev1' = whd_evar i' (mkEvar ev1) in - if isEvar ev1' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar ev1',Stack.zip evd (term2,r)) + let ev1' = EConstr.of_constr (whd_evar i' (mkEvar ev1)) in + if EConstr.isEvar i' ev1' then + solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' + (position_problem true pbty,EConstr.destEvar i' ev1',Stack.zip evd (term2,r)) else evar_eqappr_x ts env evd pbty - ((EConstr.of_constr ev1', sk1), csts1) ((term2, sk2), csts2) + ((ev1', sk1), csts1) ((term2, sk2), csts2) | None, (UnifFailure _ as x) -> (* sk1 and sk2 have no common outer part *) if Stack.not_purely_applicative sk2 then @@ -590,9 +592,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if Evar.equal sp1 sp2 then match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with |None, Success i' -> - Success (solve_refl (fun env i pbty a1 a2 -> - is_success (evar_conv_x ts env i pbty a1 a2)) - env i' (position_problem true pbty) sp1 al1 al2) + Success (solve_refl (to_conv_fun (fun env i pbty a1 a2 -> + is_success (evar_conv_x ts env i pbty a1 a2))) + env i' (position_problem true pbty) sp1 (Array.map EConstr.of_constr al1) (Array.map EConstr.of_constr al2)) |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (i,NotSameArgSize) else UnifFailure (i,NotSameHead) @@ -600,10 +602,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] | Flexible ev1, MaybeFlexible v2 -> - flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) (EConstr.of_constr v2) + flex_maybeflex true (fst ev1, Array.map EConstr.of_constr (snd ev1)) (appr1,csts1) (appr2,csts2) (EConstr.of_constr v2) | MaybeFlexible v1, Flexible ev2 -> - flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) (EConstr.of_constr v1) + flex_maybeflex false (fst ev2, Array.map EConstr.of_constr (snd ev2)) (appr2,csts2) (appr1,csts1) (EConstr.of_constr v1) | MaybeFlexible v1, MaybeFlexible v2 -> begin match kind_of_term (EConstr.Unsafe.to_constr term1), kind_of_term (EConstr.Unsafe.to_constr term2) with @@ -964,7 +966,8 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) = if is_defined i (fst ev1) then evar_conv_x ts env i CONV t2 (mkEvar ev1) else - solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1, EConstr.of_constr t2))] + let ev1 = (fst ev1, Array.map EConstr.of_constr (snd ev1)) in + solve_simple_eqn ~choose:true (to_conv_fun (evar_conv_x ts)) env i (None,ev1, EConstr.of_constr t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in @@ -1109,7 +1112,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> - match reconsider_conv_pbs (evar_conv_x ts) evd with + match reconsider_conv_pbs (to_conv_fun (evar_conv_x ts)) evd with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> evd @@ -1123,8 +1126,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = force_instantiation evd !evsref | [] -> let evd = - try Evarsolve.check_evar_instance evd evk rhs - (evar_conv_x full_transparent_state) + try Evarsolve.check_evar_instance evd evk (EConstr.of_constr rhs) + (to_conv_fun (evar_conv_x full_transparent_state)) with IllTypedInstance _ -> raise (TypingFailed evd) in Evd.define evk rhs evd @@ -1173,11 +1176,13 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_fconv ~reds:ts pbty env evd (EConstr.of_constr x) (EConstr.of_constr y) in - Success (solve_refl ~can_drop:true f env evd - (position_problem true pbty) evk1 args1 args2) + Success (solve_refl ~can_drop:true (to_conv_fun f) env evd + (position_problem true pbty) evk1 (Array.map EConstr.of_constr args1) (Array.map EConstr.of_constr args2)) | Evar ev1, Evar ev2 when app_empty -> + let ev1 = (fst ev1, Array.map EConstr.of_constr (snd ev1)) in + let ev2 = (fst ev2, Array.map EConstr.of_constr (snd ev2)) in Success (solve_evar_evar ~force:true - (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd + (evar_define (to_conv_fun (evar_conv_x ts)) ~choose:true) (to_conv_fun (evar_conv_x ts)) env evd (position_problem true pbty) ev1 ev2) | Evar ev1,_ when Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) @@ -1239,9 +1244,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | a::l -> try let conv_algo = evar_conv_x ts in - let evd = check_evar_instance evd evk a conv_algo in + let evd = check_evar_instance evd evk (EConstr.of_constr a) (to_conv_fun conv_algo) in let evd = Evd.define evk a evd in - match reconsider_conv_pbs conv_algo evd with + match reconsider_conv_pbs (to_conv_fun conv_algo) evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with @@ -1260,7 +1265,7 @@ let solve_unconstrained_impossible_cases env evd = let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in - let evd' = check_evar_instance evd' evk ty conv_algo in + let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) (to_conv_fun conv_algo) in Evd.define evk ty evd' | _ -> evd') evd evd -- 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. --- pretyping/evarconv.ml | 342 +++++++++++++++++++++++++------------------------- 1 file changed, 172 insertions(+), 170 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8f3f671abf..c8dcb19b40 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -30,7 +30,7 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type unify_fun = transparent_state -> - env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result + env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result let debug_unification = ref (false) let _ = Goptions.declare_bool_option { @@ -42,33 +42,32 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } -let to_conv_fun f = (); fun env sigma pb c1 c2 -> - f env sigma pb (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) - let unfold_projection env evd ts p c = + let open EConstr in let cst = Projection.constant p in if is_transparent_constant ts cst then Some (mkProj (Projection.make cst true, c)) else None let eval_flexible_term ts env evd c = - match kind_of_term c with + let open EConstr in + match EConstr.kind evd c with | Const (c,u as cu) -> if is_transparent_constant ts c - then constant_opt_value_in env cu + then Option.map EConstr.of_constr (constant_opt_value_in env cu) else None | Rel n -> (try match lookup_rel n env with | RelDecl.LocalAssum _ -> None - | RelDecl.LocalDef (_,v,_) -> Some (lift n v) + | RelDecl.LocalDef (_,v,_) -> Some (Vars.lift n (EConstr.of_constr v)) with Not_found -> None) | Var id -> (try if is_transparent_variable ts id then - env |> lookup_named id |> NamedDecl.get_value + Option.map EConstr.of_constr (env |> lookup_named id |> NamedDecl.get_value) else None with Not_found -> None) - | LetIn (_,b,_,c) -> Some (subst1 b c) + | LetIn (_,b,_,c) -> Some (Vars.subst1 b c) | Lambda _ -> Some c | Proj (p, c) -> if Projection.unfolded p then assert false @@ -77,12 +76,11 @@ let eval_flexible_term ts env evd c = type flex_kind_of_term = | Rigid - | MaybeFlexible of Constr.t (* reducible but not necessarily reduced *) - | Flexible of existential + | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *) + | Flexible of EConstr.existential let flex_kind_of_term ts env evd c sk = - let c = EConstr.Unsafe.to_constr c in - match kind_of_term c with + match EConstr.kind evd c with | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c) | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c @@ -92,12 +90,13 @@ let flex_kind_of_term ts env evd c sk = | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false -let zip evd (c, stk) = EConstr.Unsafe.to_constr (Stack.zip evd (c, stk)) +let add_conv_pb (pb, env, x, y) sigma = + Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma let apprec_nohdbeta ts env evd c = - let (t,sk as appr) = Reductionops.whd_nored_state evd (EConstr.of_constr c, []) in + let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in if Stack.not_purely_applicative sk - then zip evd (fst (whd_betaiota_deltazeta_for_iota_state + then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state ts env evd Cst_stack.empty appr)) else c @@ -106,8 +105,9 @@ let position_problem l2r = function | CUMUL -> Some l2r let occur_rigidly (evk,_ as ev) evd t = + let open EConstr in let rec aux t = - match kind_of_term (whd_evar evd t) with + match EConstr.kind evd t with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true | Proj (p, c) -> not (aux c) @@ -117,7 +117,7 @@ let occur_rigidly (evk,_ as ev) evd t = | Const _ -> false | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false - | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false + | Case (_,_,c,_) -> if eq_constr evd (mkEvar ev) c then raise Occur else false in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose @@ -141,23 +141,22 @@ let occur_rigidly (evk,_ as ev) evd t = projection would have been reduced) *) let check_conv_record env sigma (t1,sk1) (t2,sk2) = - let t1 = EConstr.Unsafe.to_constr t1 in - let t2 = EConstr.Unsafe.to_constr t2 in - let (proji, u), arg = Universes.global_app_of_constr t1 in + let open EConstr in + let (proji, u), arg = Termops.global_app_of_constr sigma t1 in let canon_s,sk2_effective = try - match kind_of_term t2 with + match EConstr.kind sigma t2 with Prod (_,a,b) -> (* assert (l2=[]); *) - let _, a, b = destProd (Evarutil.nf_evar sigma t2) in - if EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) then + let _, a, b = destProd sigma t2 in + if Vars.noccurn sigma 1 b then lookup_canonical_conversion (proji, Prod_cs), - (Stack.append_app [|EConstr.of_constr a;EConstr.of_constr (pop (EConstr.of_constr b))|] Stack.empty) + (Stack.append_app [|a;EConstr.of_constr (pop b)|] Stack.empty) else raise Not_found | Sort s -> lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] | _ -> - let c2 = global_of_constr t2 in + let c2 = global_of_constr (EConstr.to_constr sigma t2) in lookup_canonical_conversion (proji, Const_cs c2),sk2 with Not_found -> let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in @@ -165,17 +164,19 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = in let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in + let us = List.map EConstr.of_constr us in + let params = List.map EConstr.of_constr params in let params1, c1, extra_args1 = match arg with | Some c -> (* A primitive projection applied to c *) - let ty = Retyping.get_type_of ~lax:true env sigma (EConstr.of_constr c) in + let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) with _ -> raise Not_found in Stack.append_app_list (List.map EConstr.of_constr ind_args) Stack.empty, c, sk1 | None -> match Stack.strip_n_app nparams sk1 with - | Some (params1, c1, extra_args1) -> params1, EConstr.Unsafe.to_constr c1, extra_args1 + | Some (params1, c1, extra_args1) -> params1, c1, extra_args1 | _ -> raise Not_found in let us2,extra_args2 = let l_us = List.length us in @@ -184,13 +185,13 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in - let c' = subst_univs_level_constr subst c in + let c' = EConstr.of_constr (subst_univs_level_constr subst c) in let t' = subst_univs_level_constr subst t' in - let bs' = List.map (subst_univs_level_constr subst) bs in + let bs' = List.map (subst_univs_level_constr subst %> EConstr.of_constr) bs in let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in - ctx',(h, t2),c',bs',(Stack.append_app_list (List.map EConstr.of_constr params) Stack.empty,params1), - (Stack.append_app_list (List.map EConstr.of_constr us) Stack.empty,us2),(extra_args1,extra_args2),c1, - (n, zip sigma (EConstr.of_constr t2,sk2)) + ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), + (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, + (n, Stack.zip sigma (t2,sk2)) (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) @@ -220,11 +221,10 @@ let ise_exact ise x1 x2 = | Some _, Success i -> UnifFailure (i,NotSameArgSize) let ise_array2 evd f v1 v2 = - let inj c = EConstr.Unsafe.to_constr c in let rec allrec i = function | -1 -> Success i | n -> - match f i (inj v1.(n)) (inj v2.(n)) with + match f i v1.(n) v2.(n) with | Success i' -> allrec i' (n-1) | UnifFailure _ as x -> x in let lv1 = Array.length v1 in @@ -234,14 +234,13 @@ let ise_array2 evd f v1 v2 = (* Applicative node of stack are read from the outermost to the innermost but are unified the other way. *) let rec ise_app_stack2 env f evd sk1 sk2 = - let inj = EConstr.Unsafe.to_constr in match sk1,sk2 with | Stack.App node1 :: q1, Stack.App node2 :: q2 -> let (t1,l1) = Stack.decomp_node_last node1 q1 in let (t2,l2) = Stack.decomp_node_last node2 q2 in begin match ise_app_stack2 env f evd l1 l2 with |(_,UnifFailure _) as x -> x - |x,Success i' -> x,f env i' CONV (inj t1) (inj t2) + |x,Success i' -> x,f env i' CONV t1 t2 end | _, _ -> (sk1,sk2), Success evd @@ -255,14 +254,13 @@ let push_rec_types pfix env = stacks but not the entire stacks, the first part of the answer is Some(the remaining prefixes to tackle)) *) let ise_stack2 no_app env evd f sk1 sk2 = - let inj = EConstr.Unsafe.to_constr in let rec ise_stack2 deep i sk1 sk2 = let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i else None, x in match sk1, sk2 with | [], [] -> None, Success i | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 -> - (match f env i CONV (inj t1) (inj t2) with + (match f env i CONV t1 t2 with | Success i' -> (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with | Success i'' -> ise_stack2 true i'' q1 q2 @@ -295,7 +293,6 @@ let ise_stack2 no_app env evd f sk1 sk2 = (* Make sure that the matching suffix is the all stack *) let exact_ise_stack2 env evd f sk1 sk2 = - let inj = EConstr.Unsafe.to_constr in let rec ise_stack2 i sk1 sk2 = match sk1, sk2 with | [], [] -> Success i @@ -303,7 +300,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_and i [ (fun i -> ise_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2); - (fun i -> f env i CONV (inj t1) (inj t2))] + (fun i -> f env i CONV t1 t2)] | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 -> if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then @@ -341,10 +338,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let e = try let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) - env evd term1 term2 + env evd (EConstr.Unsafe.to_constr term1) (EConstr.Unsafe.to_constr term2) in if b then Success evd - else UnifFailure (evd, ConversionFailed (env,EConstr.of_constr term1,EConstr.of_constr term2)) + else UnifFailure (evd, ConversionFailed (env,term1,term2)) with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with @@ -361,19 +358,19 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let term2 = apprec_nohdbeta (fst ts) env evd term2 in let default () = evar_eqappr_x ts env evd pbty - (whd_nored_state evd (EConstr.of_constr term1,Stack.empty), Cst_stack.empty) - (whd_nored_state evd (EConstr.of_constr term2,Stack.empty), Cst_stack.empty) + (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty) + (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty) in - begin match EConstr.kind evd (EConstr.of_constr term1), EConstr.kind evd (EConstr.of_constr term2) with + begin match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar ev, _ when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd - (position_problem true pbty,ev, EConstr.of_constr term2) with + (match solve_simple_eqn (evar_conv_x ts) env evd + (position_problem true pbty,ev, term2) with | UnifFailure (_,OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) | _, Evar ev when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd - (position_problem false pbty,ev, EConstr.of_constr term1) with + (match solve_simple_eqn (evar_conv_x ts) env evd + (position_problem false pbty,ev, term1) with | UnifFailure (_, OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) @@ -382,6 +379,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = + let open EConstr in let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in @@ -391,28 +389,27 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = EConstr.of_constr (nf_evar evd (EConstr.Unsafe.to_constr tM)) (** FIXME *) in let t2 = solve_pattern_eqn env evd l1' t2 in - solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd - (position_problem on_left pbty,ev, EConstr.of_constr t2) + solve_simple_eqn (evar_conv_x ts) env evd + (position_problem on_left pbty,ev,EConstr.of_constr t2) in let consume_stack on_left (termF,skF) (termO,skO) evd = - let inj = EConstr.Unsafe.to_constr in let switch f a b = if on_left then f a b else f b a in let not_only_app = Stack.not_purely_applicative skO in match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (zip evd (termF,l)) (zip evd (termO,r)) + switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (zip evd (termF,l)) (zip evd (termO,r)) - |None, Success i' -> switch (evar_conv_x ts env i' pbty) (inj termF) (inj termO) + switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) + |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) in let eta env evd onleft sk term sk' term' = assert (match sk with [] -> true | _ -> false); - let (na,c1,c'1) = destLambda term in - let c = nf_evar evd c1 in + let (na,c1,c'1) = destLambda evd term in + let c = EConstr.to_constr evd c1 in let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state - (fst ts) env' evd Cst_stack.empty (EConstr.of_constr c'1, Stack.empty) in + (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in @@ -438,12 +435,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty match Stack.list_of_app_stack skF with | None -> quick_fail evd | Some lF -> - let tM = zip evd apprM in + let tM = Stack.zip evd apprM in miller_pfenning on_left (fun () -> if not_only_app then (* Postpone the use of an heuristic *) - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (zip evd apprF) tM + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) - ev lF (EConstr.of_constr tM) i + ev lF tM i and consume (termF,skF as apprF) (termM,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then consume_stack on_left apprF apprM i @@ -487,7 +484,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let eta evd = match EConstr.kind evd termR with | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> - eta env evd false skR (EConstr.Unsafe.to_constr termR) skF termF + eta env evd false skR termR skF termF | Construct u -> eta_constructor ts env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in @@ -495,7 +492,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None -> ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> - let tR = zip evd apprR in + let tR = Stack.zip evd apprR in miller_pfenning on_left (fun () -> ise_try evd @@ -503,17 +500,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> if not (occur_rigidly ev i tR) then let i,tF = - if isRel tR || isVar tR then + if isRel i tR || isVar i tR then (* Optimization so as to generate candidates *) - let i,ev = evar_absorb_arguments env i (fst ev, Array.map EConstr.of_constr (snd ev)) lF in + let i,ev = evar_absorb_arguments env i ev lF in i,mkEvar ev else - i,zip evd apprF in + i,Stack.zip evd apprF in switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) tF tR else - UnifFailure (evd,OccurCheck (fst ev,EConstr.of_constr tR)))]) - (fst ev, Array.map EConstr.of_constr (snd ev)) lF (EConstr.of_constr tR) evd + UnifFailure (evd,OccurCheck (fst ev,tR)))]) + ev lF tR evd in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) @@ -531,20 +528,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None, Success i' -> (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) - let ev1' = EConstr.of_constr (whd_evar i' (mkEvar ev1)) in - if EConstr.isEvar i' ev1' then - solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' - (position_problem true pbty,EConstr.destEvar i' ev1', term2) + let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in + if isEvar i' ev1' then + solve_simple_eqn (evar_conv_x ts) env i' + (position_problem true pbty,destEvar i' ev1', term2) else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) | Some (r,[]), Success i' -> (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) (* we now unify r[?ev1] and ?ev2 *) - let ev2' = EConstr.of_constr (whd_evar i' (mkEvar ev2)) in - if EConstr.isEvar i' ev2' then - solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' - (position_problem false pbty,EConstr.destEvar i' ev2',Stack.zip evd (term1,r)) + let ev2' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev2))) in + if isEvar i' ev2' then + solve_simple_eqn (evar_conv_x ts) env i' + (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r)) else evar_eqappr_x ts env evd pbty ((ev2', sk1), csts1) ((term2, sk2), csts2) @@ -552,10 +549,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Symmetrically *) (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) (* we now unify ?ev1 and r[?ev2] *) - let ev1' = EConstr.of_constr (whd_evar i' (mkEvar ev1)) in - if EConstr.isEvar i' ev1' then - solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' - (position_problem true pbty,EConstr.destEvar i' ev1',Stack.zip evd (term2,r)) + let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in + if isEvar i' ev1' then + solve_simple_eqn (evar_conv_x ts) env i' + (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r)) else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) | None, (UnifFailure _ as x) -> @@ -592,9 +589,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if Evar.equal sp1 sp2 then match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with |None, Success i' -> - Success (solve_refl (to_conv_fun (fun env i pbty a1 a2 -> - is_success (evar_conv_x ts env i pbty a1 a2))) - env i' (position_problem true pbty) sp1 (Array.map EConstr.of_constr al1) (Array.map EConstr.of_constr al2)) + Success (solve_refl (fun env i pbty a1 a2 -> + is_success (evar_conv_x ts env i pbty a1 a2)) + env i' (position_problem true pbty) sp1 al1 al2) |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (i,NotSameArgSize) else UnifFailure (i,NotSameHead) @@ -602,13 +599,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] | Flexible ev1, MaybeFlexible v2 -> - flex_maybeflex true (fst ev1, Array.map EConstr.of_constr (snd ev1)) (appr1,csts1) (appr2,csts2) (EConstr.of_constr v2) + flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2 | MaybeFlexible v1, Flexible ev2 -> - flex_maybeflex false (fst ev2, Array.map EConstr.of_constr (snd ev2)) (appr2,csts2) (appr1,csts1) (EConstr.of_constr v1) + flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1 | MaybeFlexible v1, MaybeFlexible v2 -> begin - match kind_of_term (EConstr.Unsafe.to_constr term1), kind_of_term (EConstr.Unsafe.to_constr term2) with + match EConstr.kind evd term1, EConstr.kind evd term2 with | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> let f1 i = (* FO *) ise_and i @@ -617,14 +614,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> evar_conv_x ts env i CUMUL t2 t1)]); (fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> - let b = nf_evar i b1 in - let t = nf_evar i t1 in + let b = EConstr.to_constr i b1 in + let t = EConstr.to_constr i t1 in let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (EConstr.of_constr v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (EConstr.of_constr v2,sk2) + let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1; f2] @@ -636,8 +633,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c c'); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (EConstr.of_constr v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (EConstr.of_constr v2,sk2) + let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1; f2] @@ -645,7 +642,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Catch the p.c ~= p c' cases *) | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> let res = - try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p (EConstr.of_constr c) []))) + try Some (destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c []))) with Retyping.RetypeError _ -> None in (match res with @@ -656,7 +653,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> let res = - try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' (EConstr.of_constr c') []))) + try Some (destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' []))) with Retyping.RetypeError _ -> None in (match res with @@ -710,7 +707,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let applicative_stack = fst (Stack.strip_app sk2) in is_unnamed (fst (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i Cst_stack.empty (EConstr.of_constr v2, applicative_stack))) in + (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in let rhs_is_already_stuck = rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in @@ -718,12 +715,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty && (not (Stack.not_purely_applicative sk1)) then evar_eqappr_x ~rhs_is_already_stuck ts env i pbty (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term1 csts1) (EConstr.of_constr v1,sk1)) + (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) (appr2,csts2) else evar_eqappr_x ts env i pbty (appr1,csts1) (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term2 csts2) (EConstr.of_constr v2,sk2)) + (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) in ise_try evd [f1; f2; f3] end @@ -731,14 +728,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 -> let (na1,c1,c'1) = EConstr.destLambda evd term1 in let (na2,c2,c'2) = EConstr.destLambda evd term2 in - let inj = EConstr.Unsafe.to_constr in assert app_empty; ise_and evd - [(fun i -> evar_conv_x ts env i CONV (inj c1) (inj c2)); + [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> - let c = nf_evar i (inj c1) in + let c = EConstr.to_constr i c1 in let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV (inj c'1) (inj c'2))] + evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 @@ -752,7 +748,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty and f4 i = evar_eqappr_x ts env i pbty (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term1 csts1) (EConstr.of_constr v1,sk1)) + (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) (appr2,csts2) in ise_try evd [f3; f4] @@ -766,19 +762,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty and f4 i = evar_eqappr_x ts env i pbty (appr1,csts1) (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term2 csts2) (EConstr.of_constr v2,sk2)) + (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) in ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid, _ when EConstr.isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> - eta env evd true sk1 (EConstr.Unsafe.to_constr term1) sk2 term2 + | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> + eta env evd true sk1 term1 sk2 term2 - | _, Rigid when EConstr.isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> - eta env evd false sk2 (EConstr.Unsafe.to_constr term2) sk1 term1 + | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> + eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin - let inj = EConstr.Unsafe.to_constr in match EConstr.kind evd term1, EConstr.kind evd term2 with | Sort s1, Sort s2 when app_empty -> @@ -794,11 +789,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd - [(fun i -> evar_conv_x ts env i CONV (inj c1) (inj c2)); + [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> - let c = nf_evar i (inj c1) in + let c = EConstr.to_constr i c1 in let na = Nameops.name_max n1 n2 in - evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty (inj c'1) (inj c'2))] + evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then @@ -842,11 +837,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else UnifFailure (evd,NotSameHead) | (Meta _, _) | (_, Meta _) -> - let inj = EConstr.Unsafe.to_constr in begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with |_, (UnifFailure _ as x) -> x - |None, Success i' -> evar_conv_x ts env i' CONV (inj term1) (inj term2) - |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (inj (Stack.zip i' (term1,sk1'))) (inj (Stack.zip i' (term2,sk2'))) + |None, Success i' -> evar_conv_x ts env i' CONV term1 term2 + |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) end | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ -> @@ -884,38 +878,39 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) had to be initially resolved *) + let open EConstr in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in if Reductionops.Stack.compare_shape sk1 sk2 then let (evd',ks,_,test) = List.fold_left (fun (i,ks,m,test) b -> if match n with Some n -> Int.equal m n | None -> false then - let ty = Retyping.get_type_of env i (EConstr.of_constr t2) in - let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in + let ty = EConstr.of_constr (Retyping.get_type_of env i t2) in + let test i = evar_conv_x trs env i CUMUL ty (Vars.substl ks b) in (i,t2::ks, m-1, test) else let dloc = (Loc.ghost,Evar_kinds.InternalHole) in let i = Sigma.Unsafe.of_evar_map i in - let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in + let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (EConstr.Unsafe.to_constr (Vars.substl ks b)) in let i' = Sigma.to_evar_map i' in - (i', ev :: ks, m - 1,test)) + (i', EConstr.of_constr ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs in let app = mkApp (c, Array.rev_of_list ks) in ise_and evd' [(fun i -> exact_ise_stack2 env i - (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x)) + (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (Vars.substl ks x)) params1 params); (fun i -> exact_ise_stack2 env i - (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u)) + (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (Vars.substl ks u)) us2 us); (fun i -> evar_conv_x trs env i CONV c1 app); (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); test; (fun i -> evar_conv_x trs env i CONV h2 - (fst (decompose_app_vect i (EConstr.of_constr (substl ks h)))))] + (EConstr.of_constr (fst (decompose_app_vect i (Vars.substl ks h)))))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = @@ -956,66 +951,69 @@ let set_evar_conv f = Hook.set evar_conv_hook_set f (* We assume here |l1| <= |l2| *) let first_order_unification ts env evd (ev1,l1) (term2,l2) = + let open EConstr in let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in ise_and evd (* First compare extra args for better failure message *) - [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) (Array.map EConstr.of_constr rest2) (Array.map EConstr.of_constr l1)); + [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1); (fun i -> (* Then instantiate evar unless already done by unifying args *) let t2 = mkApp(term2,deb2) in if is_defined i (fst ev1) then evar_conv_x ts env i CONV t2 (mkEvar ev1) else - let ev1 = (fst ev1, Array.map EConstr.of_constr (snd ev1)) in - solve_simple_eqn ~choose:true (to_conv_fun (evar_conv_x ts)) env i (None,ev1, EConstr.of_constr t2))] + solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in let subst = make_pure_subst evi args in - let subst' = List.filter (fun (id,c) -> Term.eq_constr c term) subst in + let subst' = List.filter (fun (id,c) -> EConstr.eq_constr evd c term) subst in match subst' with | [] -> None - | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) + | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd) let apply_on_subterm env evdref f c t = + let open EConstr in let rec applyrec (env,(k,c) as acc) t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) (* such that c occurs in u *) - if e_eq_constr_univs evdref c t then f k + if e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) then f k else - match kind_of_term t with - | Evar (evk,args) when Evd.is_undefined !evdref evk -> + match EConstr.kind !evdref t with + | Evar (evk,args) -> let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in let g decl a = if is_local_assum decl then applyrec acc a else a in mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) | _ -> - map_constr_with_binders_left_to_right - (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) - applyrec acc t + let self acc c = EConstr.Unsafe.to_constr (applyrec acc (EConstr.of_constr c)) in + EConstr.of_constr (map_constr_with_binders_left_to_right + (fun d (env,(k,c)) -> (push_rel d env, (k+1,Vars.lift 1 c))) + self acc (EConstr.Unsafe.to_constr t)) in applyrec (env,(0,c)) t let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the fv of args to have a well-typed filter; don't know how necessary - it is however to have a well-typed filter here *) - let fv1 = free_rels evd (EConstr.of_constr (mkApp (c,args))) (* Hack: locally untyped *) in - let fv2 = collect_vars evd (EConstr.of_constr (mkApp (c,args))) in + it is however to have a well-typed filter here *) + let open EConstr in + let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in + let fv2 = collect_vars evd (mkApp (c,args)) in let len = Array.length args in - let tyvars = collect_vars evd (EConstr.of_constr ty) in + let tyvars = collect_vars evd ty in List.map_i (fun i decl -> let () = assert (i < len) in let a = Array.unsafe_get args i in (match decl with | NamedDecl.LocalAssum _ -> false - | NamedDecl.LocalDef (_,c,_) -> not (isRel c || isVar c)) || + | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr c))) || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) (* in u *) - isRel a && Int.Set.mem (destRel a) fv1 || - isVar a && Id.Set.mem (destVar a) fv2 || + isRel evd a && Int.Set.mem (destRel evd a) fv1 || + isVar evd a && Id.Set.mem (destVar evd a) fv2 || Id.Set.mem (NamedDecl.get_id decl) tyvars) 0 ctxt @@ -1042,6 +1040,7 @@ let set_solve_evars f = solve_evars := f exception TypingFailed of evar_map let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = + let open EConstr in try let evi = Evd.find_undefined evd evk in let env_evar = evar_filtered_env evi in @@ -1050,7 +1049,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in let rec make_subst = function - | decl'::ctxt', c::l, occs::occsl when isVarId (NamedDecl.get_id decl') c -> + | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with | Some _ -> error "Cannot force abstraction on identity instance." @@ -1059,9 +1058,9 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = end | decl'::ctxt', c::l, occs::occsl -> let id = NamedDecl.get_id decl' in - let t = NamedDecl.get_type decl' in + let t = EConstr.of_constr (NamedDecl.get_type decl') in let evs = ref [] in - let ty = Retyping.get_type_of env_rhs evd (EConstr.of_constr c) in + let ty = EConstr.of_constr (Retyping.get_type_of env_rhs evd c) in let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] @@ -1075,13 +1074,13 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | Some _ -> error "Selection of specific occurrences not supported" | None -> let evty = set_holes evdref cty subst in - let instance = Filter.filter_list filter instance in + let instance = List.map EConstr.Unsafe.to_constr (Filter.filter_list filter instance) in let evd = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in + let Sigma (ev, evd, _) = new_evar_instance sign evd (EConstr.Unsafe.to_constr evty) ~filter instance in let evd = Sigma.to_evar_map evd in evdref := evd; - evsref := (fst (destEvar ev),evty)::!evsref; - ev in + evsref := (fst (destEvar !evdref (EConstr.of_constr ev)),evty)::!evsref; + EConstr.of_constr ev in set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst | [] -> rhs in @@ -1108,11 +1107,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* We force abstraction over this unconstrained occurrence *) (* and we use typing to propagate this instantiation *) (* This is an arbitrary choice *) - let evd = Evd.define evk (mkVar id) evd in + let evd = Evd.define evk (Constr.mkVar id) evd in match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> - match reconsider_conv_pbs (to_conv_fun (evar_conv_x ts)) evd with + match reconsider_conv_pbs (evar_conv_x ts) evd with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> evd @@ -1126,16 +1125,20 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = force_instantiation evd !evsref | [] -> let evd = - try Evarsolve.check_evar_instance evd evk (EConstr.of_constr rhs) - (to_conv_fun (evar_conv_x full_transparent_state)) + try Evarsolve.check_evar_instance evd evk rhs + (evar_conv_x full_transparent_state) with IllTypedInstance _ -> raise (TypingFailed evd) in - Evd.define evk rhs evd + Evd.define evk (EConstr.Unsafe.to_constr rhs) evd in abstract_free_holes evd subst, true with TypingFailed evd -> evd, false +let to_pb (pb, env, t1, t2) = + (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2) + let second_order_matching_with_args ts env evd pbty ev l t = + let open EConstr in (* let evd,ev = evar_absorb_arguments env evd ev l in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in @@ -1144,18 +1147,19 @@ let second_order_matching_with_args ts env evd pbty ev l t = else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) if b then Success evd else *) - let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = + let open EConstr in let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in - let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in - let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in + let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in + let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in - match kind_of_term term1, kind_of_term term2 with + match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty - && List.for_all (fun a -> Term.eq_constr a term2 || isEvar a) + && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a) (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return type inference *) @@ -1163,9 +1167,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Some evd -> Success evd | None -> let reason = ProblemBeyondCapabilities in - UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) + UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty - && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a) + && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) (remove_instance_local_defs evd evk2 args2) -> (* The typical kind of constraint coming from pattern-matching return type inference *) @@ -1173,16 +1177,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Some evd -> Success evd | None -> let reason = ProblemBeyondCapabilities in - UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) + UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f env evd pbty x y = is_fconv ~reds:ts pbty env evd (EConstr.of_constr x) (EConstr.of_constr y) in - Success (solve_refl ~can_drop:true (to_conv_fun f) env evd - (position_problem true pbty) evk1 (Array.map EConstr.of_constr args1) (Array.map EConstr.of_constr args2)) + let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in + Success (solve_refl ~can_drop:true f env evd + (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> - let ev1 = (fst ev1, Array.map EConstr.of_constr (snd ev1)) in - let ev2 = (fst ev2, Array.map EConstr.of_constr (snd ev2)) in Success (solve_evar_evar ~force:true - (evar_define (to_conv_fun (evar_conv_x ts)) ~choose:true) (to_conv_fun (evar_conv_x ts)) env evd + (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd (position_problem true pbty) ev1 ev2) | Evar ev1,_ when Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) @@ -1244,9 +1246,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | a::l -> try let conv_algo = evar_conv_x ts in - let evd = check_evar_instance evd evk (EConstr.of_constr a) (to_conv_fun conv_algo) in + let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in let evd = Evd.define evk a evd in - match reconsider_conv_pbs (to_conv_fun conv_algo) evd with + match reconsider_conv_pbs conv_algo evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with @@ -1265,7 +1267,7 @@ let solve_unconstrained_impossible_cases env evd = let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in - let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) (to_conv_fun conv_algo) in + let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) conv_algo in Evd.define evk ty evd' | _ -> evd') evd evd @@ -1275,7 +1277,7 @@ let consider_remaining_unif_problems env let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> - (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with + (match apply_conversion_problem_heuristic ts env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with | Success evd' -> let (evd', rest) = extract_all_conv_pbs evd' in begin match rest with -- 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. --- pretyping/evarconv.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c8dcb19b40..cdcb993b5e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -986,10 +986,9 @@ let apply_on_subterm env evdref f c t = let g decl a = if is_local_assum decl then applyrec acc a else a in mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) | _ -> - let self acc c = EConstr.Unsafe.to_constr (applyrec acc (EConstr.of_constr c)) in - EConstr.of_constr (map_constr_with_binders_left_to_right + map_constr_with_binders_left_to_right !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,Vars.lift 1 c))) - self acc (EConstr.Unsafe.to_constr t)) + applyrec acc t in applyrec (env,(0,c)) t -- 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. --- pretyping/evarconv.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cdcb993b5e..683b33b89f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -338,7 +338,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let e = try let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) - env evd (EConstr.Unsafe.to_constr term1) (EConstr.Unsafe.to_constr term2) + env evd term1 term2 in if b then Success evd else UnifFailure (evd, ConversionFailed (env,term1,term2)) @@ -891,7 +891,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) else let dloc = (Loc.ghost,Evar_kinds.InternalHole) in let i = Sigma.Unsafe.of_evar_map i in - let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (EConstr.Unsafe.to_constr (Vars.substl ks b)) in + let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (Vars.substl ks b) in let i' = Sigma.to_evar_map i' in (i', EConstr.of_constr ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs @@ -1075,7 +1075,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let evty = set_holes evdref cty subst in let instance = List.map EConstr.Unsafe.to_constr (Filter.filter_list filter instance) in let evd = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (ev, evd, _) = new_evar_instance sign evd (EConstr.Unsafe.to_constr evty) ~filter instance in + let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in let evd = Sigma.to_evar_map evd in evdref := evd; evsref := (fst (destEvar !evdref (EConstr.of_constr ev)),evty)::!evsref; -- 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. --- pretyping/evarconv.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 683b33b89f..3b420347b9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -390,7 +390,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let t2 = EConstr.of_constr (nf_evar evd (EConstr.Unsafe.to_constr tM)) (** FIXME *) in let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (evar_conv_x ts) env evd - (position_problem on_left pbty,ev,EConstr.of_constr t2) + (position_problem on_left pbty,ev,t2) in let consume_stack on_left (termF,skF) (termO,skO) evd = let switch f a b = if on_left then f a b else f b a in @@ -1216,7 +1216,7 @@ let error_cannot_unify env evd pb ?reason t1 t2 = let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2) | _ -> () let max_undefined_with_candidates evd = @@ -1276,7 +1276,9 @@ let consider_remaining_unif_problems env let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> - (match apply_conversion_problem_heuristic ts env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with + let t1 = EConstr.of_constr t1 in + let t2 = EConstr.of_constr t2 in + (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with | Success evd' -> let (evd', rest) = extract_all_conv_pbs evd' in begin match rest with @@ -1292,6 +1294,8 @@ let consider_remaining_unif_problems env match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> + let t1 = EConstr.of_constr t1 in + let t2 = EConstr.of_constr t2 in (* There remains stuck problems *) error_cannot_unify env evd pb t1 t2 in -- 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. --- pretyping/evarconv.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3b420347b9..639d6260ea 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1266,8 +1266,8 @@ let solve_unconstrained_impossible_cases env evd = let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in - let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) conv_algo in - Evd.define evk ty evd' + let evd' = check_evar_instance evd' evk ty conv_algo in + Evd.define evk (EConstr.Unsafe.to_constr ty) evd' | _ -> evd') evd evd let consider_remaining_unif_problems env -- cgit v1.2.3 From 536026f3e20f761e8ef366ed732da7d3b626ac5e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 15:39:01 +0100 Subject: Cleaning up opening of the EConstr module in pretyping folder. --- pretyping/evarconv.ml | 49 ++++++++++++++++++++----------------------------- 1 file changed, 20 insertions(+), 29 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 639d6260ea..77e91095fc 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,15 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module CVars = Vars + open CErrors open Util open Names open Term +open Termops +open EConstr open Vars open CClosure open Reduction open Reductionops -open Termops open Environ open Recordops open Evarutil @@ -43,14 +46,12 @@ let _ = Goptions.declare_bool_option { } let unfold_projection env evd ts p c = - let open EConstr in let cst = Projection.constant p in if is_transparent_constant ts cst then Some (mkProj (Projection.make cst true, c)) else None let eval_flexible_term ts env evd c = - let open EConstr in match EConstr.kind evd c with | Const (c,u as cu) -> if is_transparent_constant ts c @@ -59,7 +60,7 @@ let eval_flexible_term ts env evd c = | Rel n -> (try match lookup_rel n env with | RelDecl.LocalAssum _ -> None - | RelDecl.LocalDef (_,v,_) -> Some (Vars.lift n (EConstr.of_constr v)) + | RelDecl.LocalDef (_,v,_) -> Some (lift n (EConstr.of_constr v)) with Not_found -> None) | Var id -> (try @@ -67,7 +68,7 @@ let eval_flexible_term ts env evd c = Option.map EConstr.of_constr (env |> lookup_named id |> NamedDecl.get_value) else None with Not_found -> None) - | LetIn (_,b,_,c) -> Some (Vars.subst1 b c) + | LetIn (_,b,_,c) -> Some (subst1 b c) | Lambda _ -> Some c | Proj (p, c) -> if Projection.unfolded p then assert false @@ -105,7 +106,6 @@ let position_problem l2r = function | CUMUL -> Some l2r let occur_rigidly (evk,_ as ev) evd t = - let open EConstr in let rec aux t = match EConstr.kind evd t with | App (f, c) -> if aux f then Array.exists aux c else false @@ -141,14 +141,13 @@ let occur_rigidly (evk,_ as ev) evd t = projection would have been reduced) *) let check_conv_record env sigma (t1,sk1) (t2,sk2) = - let open EConstr in let (proji, u), arg = Termops.global_app_of_constr sigma t1 in let canon_s,sk2_effective = try match EConstr.kind sigma t2 with Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd sigma t2 in - if Vars.noccurn sigma 1 b then + if noccurn sigma 1 b then lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;EConstr.of_constr (pop b)|] Stack.empty) else raise Not_found @@ -185,9 +184,9 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in - let c' = EConstr.of_constr (subst_univs_level_constr subst c) in - let t' = subst_univs_level_constr subst t' in - let bs' = List.map (subst_univs_level_constr subst %> EConstr.of_constr) bs in + let c' = EConstr.of_constr (CVars.subst_univs_level_constr subst c) in + let t' = CVars.subst_univs_level_constr subst t' in + let bs' = List.map (CVars.subst_univs_level_constr subst %> EConstr.of_constr) bs in let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, @@ -379,7 +378,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = - let open EConstr in let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in @@ -466,7 +464,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let termM' = Retyping.expand_projection env evd p c [] in let apprM', cstsM' = whd_betaiota_deltazeta_for_iota_state - (fst ts) env evd cstsM (EConstr.of_constr termM',skM) + (fst ts) env evd cstsM (termM',skM) in let delta' i = switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') @@ -642,7 +640,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Catch the p.c ~= p c' cases *) | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> let res = - try Some (destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c []))) + try Some (destApp evd (Retyping.expand_projection env evd p c [])) with Retyping.RetypeError _ -> None in (match res with @@ -653,7 +651,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> let res = - try Some (destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' []))) + try Some (destApp evd (Retyping.expand_projection env evd p' c' [])) with Retyping.RetypeError _ -> None in (match res with @@ -699,7 +697,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Lambda _ -> assert (match args with [] -> true | _ -> false); true | LetIn (_,b,_,c) -> is_unnamed (fst (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i Cst_stack.empty (EConstr.Vars.subst1 b c, args))) + (fst ts) env i Cst_stack.empty (subst1 b c, args))) | Fix _ -> true (* Partially applied fix can be the result of a whd call *) | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args | Case _ | App _| Cast _ -> assert false in @@ -878,7 +876,6 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) had to be initially resolved *) - let open EConstr in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in if Reductionops.Stack.compare_shape sk1 sk2 then let (evd',ks,_,test) = @@ -886,12 +883,12 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fun (i,ks,m,test) b -> if match n with Some n -> Int.equal m n | None -> false then let ty = EConstr.of_constr (Retyping.get_type_of env i t2) in - let test i = evar_conv_x trs env i CUMUL ty (Vars.substl ks b) in + let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else let dloc = (Loc.ghost,Evar_kinds.InternalHole) in let i = Sigma.Unsafe.of_evar_map i in - let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (Vars.substl ks b) in + let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in let i' = Sigma.to_evar_map i' in (i', EConstr.of_constr ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs @@ -900,17 +897,17 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) ise_and evd' [(fun i -> exact_ise_stack2 env i - (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (Vars.substl ks x)) + (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x)) params1 params); (fun i -> exact_ise_stack2 env i - (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (Vars.substl ks u)) + (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u)) us2 us); (fun i -> evar_conv_x trs env i CONV c1 app); (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); test; (fun i -> evar_conv_x trs env i CONV h2 - (EConstr.of_constr (fst (decompose_app_vect i (Vars.substl ks h)))))] + (EConstr.of_constr (fst (decompose_app_vect i (substl ks h)))))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = @@ -951,7 +948,6 @@ let set_evar_conv f = Hook.set evar_conv_hook_set f (* We assume here |l1| <= |l2| *) let first_order_unification ts env evd (ev1,l1) (term2,l2) = - let open EConstr in let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in ise_and evd (* First compare extra args for better failure message *) @@ -973,7 +969,6 @@ let choose_less_dependent_instance evk evd term args = | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd) let apply_on_subterm env evdref f c t = - let open EConstr in let rec applyrec (env,(k,c) as acc) t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) @@ -987,7 +982,7 @@ let apply_on_subterm env evdref f c t = mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) | _ -> map_constr_with_binders_left_to_right !evdref - (fun d (env,(k,c)) -> (push_rel d env, (k+1,Vars.lift 1 c))) + (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t in applyrec (env,(0,c)) t @@ -996,7 +991,6 @@ let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the fv of args to have a well-typed filter; don't know how necessary it is however to have a well-typed filter here *) - let open EConstr in let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in let fv2 = collect_vars evd (mkApp (c,args)) in let len = Array.length args in @@ -1039,7 +1033,6 @@ let set_solve_evars f = solve_evars := f exception TypingFailed of evar_map let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = - let open EConstr in try let evi = Evd.find_undefined evd evk in let env_evar = evar_filtered_env evi in @@ -1137,7 +1130,6 @@ let to_pb (pb, env, t1, t2) = (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2) let second_order_matching_with_args ts env evd pbty ev l t = - let open EConstr in (* let evd,ev = evar_absorb_arguments env evd ev l in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in @@ -1150,7 +1142,6 @@ let second_order_matching_with_args ts env evd pbty ev l t = UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = - let open EConstr in let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in -- 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. --- pretyping/evarconv.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 77e91095fc..ee6355736b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module CVars = Vars - open CErrors open Util open Names @@ -184,10 +182,12 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in - let c' = EConstr.of_constr (CVars.subst_univs_level_constr subst c) in - let t' = CVars.subst_univs_level_constr subst t' in - let bs' = List.map (CVars.subst_univs_level_constr subst %> EConstr.of_constr) bs in - let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in + let c = EConstr.of_constr c in + let c' = subst_univs_level_constr subst c in + let t' = EConstr.of_constr t' in + let t' = subst_univs_level_constr subst t' in + let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in + let h, _ = decompose_app_vect sigma t' in ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, (n, Stack.zip sigma (t2,sk2)) -- 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. --- pretyping/evarconv.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ee6355736b..a968af7ff2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -890,7 +890,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) let i = Sigma.Unsafe.of_evar_map i in let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in let i' = Sigma.to_evar_map i' in - (i', EConstr.of_constr ev :: ks, m - 1,test)) + (i', ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs in let app = mkApp (c, Array.rev_of_list ks) in @@ -1066,13 +1066,13 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | Some _ -> error "Selection of specific occurrences not supported" | None -> let evty = set_holes evdref cty subst in - let instance = List.map EConstr.Unsafe.to_constr (Filter.filter_list filter instance) in + let instance = Filter.filter_list filter instance in let evd = Sigma.Unsafe.of_evar_map !evdref in let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in let evd = Sigma.to_evar_map evd in evdref := evd; - evsref := (fst (destEvar !evdref (EConstr.of_constr ev)),evty)::!evsref; - EConstr.of_constr ev in + evsref := (fst (destEvar !evdref ev),evty)::!evsref; + ev in set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst | [] -> rhs in -- 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 --- pretyping/evarconv.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a968af7ff2..9675ae2ea9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -170,7 +170,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let (i,u), ind_args = try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) with _ -> raise Not_found - in Stack.append_app_list (List.map EConstr.of_constr ind_args) Stack.empty, c, sk1 + in Stack.append_app_list ind_args Stack.empty, c, sk1 | None -> match Stack.strip_n_app nparams sk1 with | Some (params1, c1, extra_args1) -> params1, c1, extra_args1 @@ -188,7 +188,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let t' = subst_univs_level_constr subst t' in let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in let h, _ = decompose_app_vect sigma t' in - ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), + ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, (n, Stack.zip sigma (t2,sk2)) @@ -907,7 +907,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); test; (fun i -> evar_conv_x trs env i CONV h2 - (EConstr.of_constr (fst (decompose_app_vect i (substl ks h)))))] + (fst (decompose_app_vect i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = -- cgit v1.2.3 From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 15:50:17 +0100 Subject: Removing some return type compatibility layers in Termops. --- pretyping/evarconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9675ae2ea9..6dce8627da 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -147,7 +147,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then lookup_canonical_conversion (proji, Prod_cs), - (Stack.append_app [|a;EConstr.of_constr (pop b)|] Stack.empty) + (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> lookup_canonical_conversion -- 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 --- pretyping/evarconv.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6dce8627da..afb0bf6d5a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -168,7 +168,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Some c -> (* A primitive projection applied to c *) let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = - try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) + try Inductiveops.find_mrectype env sigma ty with _ -> raise Not_found in Stack.append_app_list ind_args Stack.empty, c, sk1 | None -> @@ -882,7 +882,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) List.fold_left (fun (i,ks,m,test) b -> if match n with Some n -> Int.equal m n | None -> false then - let ty = EConstr.of_constr (Retyping.get_type_of env i t2) in + let ty = Retyping.get_type_of env i t2 in let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else @@ -1052,7 +1052,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let id = NamedDecl.get_id decl' in let t = EConstr.of_constr (NamedDecl.get_type decl') in let evs = ref [] in - let ty = EConstr.of_constr (Retyping.get_type_of env_rhs evd c) in + let ty = Retyping.get_type_of env_rhs evd c in let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] -- cgit v1.2.3 From 778e863b77bcafc8ed339dd02226e85e5fee2532 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 11:36:09 +0100 Subject: Removing compatibility layers related to printing. --- pretyping/evarconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index afb0bf6d5a..87267d5389 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -385,7 +385,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) - let t2 = EConstr.of_constr (nf_evar evd (EConstr.Unsafe.to_constr tM)) (** FIXME *) in + let t2 = tM in let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (evar_conv_x ts) env evd (position_problem on_left pbty,ev,t2) -- 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. --- pretyping/evarconv.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 87267d5389..3ae2e35e6d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -526,7 +526,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None, Success i' -> (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) - let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in + let ev1' = whd_evar i' (mkEvar ev1) in if isEvar i' ev1' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem true pbty,destEvar i' ev1', term2) @@ -536,7 +536,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Some (r,[]), Success i' -> (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) (* we now unify r[?ev1] and ?ev2 *) - let ev2' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev2))) in + let ev2' = whd_evar i' (mkEvar ev2) in if isEvar i' ev2' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r)) @@ -547,7 +547,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Symmetrically *) (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) (* we now unify ?ev1 and r[?ev2] *) - let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in + let ev1' = whd_evar i' (mkEvar ev1) in if isEvar i' ev1' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r)) -- 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. --- pretyping/evarconv.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3ae2e35e6d..f5cab070ed 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -11,12 +11,12 @@ open Util open Names open Term open Termops +open Environ open EConstr open Vars open CClosure open Reduction open Reductionops -open Environ open Recordops open Evarutil open Evardefine @@ -58,12 +58,12 @@ let eval_flexible_term ts env evd c = | Rel n -> (try match lookup_rel n env with | RelDecl.LocalAssum _ -> None - | RelDecl.LocalDef (_,v,_) -> Some (lift n (EConstr.of_constr v)) + | RelDecl.LocalDef (_,v,_) -> Some (lift n v) with Not_found -> None) | Var id -> (try if is_transparent_variable ts id then - Option.map EConstr.of_constr (env |> lookup_named id |> NamedDecl.get_value) + env |> lookup_named id |> NamedDecl.get_value else None with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) @@ -404,7 +404,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let eta env evd onleft sk term sk' term' = assert (match sk with [] -> true | _ -> false); let (na,c1,c'1) = destLambda evd term in - let c = EConstr.to_constr evd c1 in + let c = nf_evar evd c1 in let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in @@ -612,8 +612,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> evar_conv_x ts env i CUMUL t2 t1)]); (fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> - let b = EConstr.to_constr i b1 in - let t = EConstr.to_constr i t1 in + let b = nf_evar i b1 in + let t = nf_evar i t1 in let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] @@ -730,7 +730,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> - let c = EConstr.to_constr i c1 in + let c = nf_evar i c1 in let na = Nameops.name_max na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] @@ -789,7 +789,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> - let c = EConstr.to_constr i c1 in + let c = nf_evar i c1 in let na = Nameops.name_max n1 n2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] -- 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. --- pretyping/evarconv.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f5cab070ed..1cbea68dda 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -973,7 +973,13 @@ let apply_on_subterm env evdref f c t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) (* such that c occurs in u *) - if e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) then f k + let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with + | None -> false + | Some cstr -> + try ignore (Evd.add_universe_constraints !evdref cstr); true + with UniversesDiffer -> false + in + if eq_constr c t then f k else match EConstr.kind !evdref t with | Evar (evk,args) -> -- cgit v1.2.3 From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 Mar 2017 23:20:25 +0200 Subject: Actually exporting delayed universes in the EConstr implementation. For now we only normalize sorts, and we leave instances for the next commit. --- pretyping/evarconv.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 85cc8762ee..b6fa257691 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -150,6 +150,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> + let s = ESorts.kind sigma s in lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] | _ -> @@ -775,6 +776,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Sort s1, Sort s2 when app_empty -> (try + let s1 = ESorts.kind evd s1 in + let s2 = ESorts.kind evd s2 in let evd' = if pbty == CONV then Evd.set_eq_sort env evd s1 s2 -- 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. --- pretyping/evarconv.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b6fa257691..9c9350ab10 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -51,9 +51,9 @@ let unfold_projection env evd ts p c = let eval_flexible_term ts env evd c = match EConstr.kind evd c with - | Const (c,u as cu) -> + | Const (c, u) -> if is_transparent_constant ts c - then Option.map EConstr.of_constr (constant_opt_value_in env cu) + then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u)) else None | Rel n -> (try match lookup_rel n env with -- cgit v1.2.3 From 2794b3c91bbbef115303b40f2e494ad97467dc9e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 5 Apr 2017 14:05:42 +0200 Subject: Removing a normalization hotspot from EConstr. It was not necessary to normalize a term just to check whether it was a global reference. The hotspot appeared in mathcomp. --- pretyping/evarconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9c9350ab10..44b771283b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -154,7 +154,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] | _ -> - let c2 = global_of_constr (EConstr.to_constr sigma t2) in + let (c2, _) = Termops.global_of_constr sigma t2 in lookup_canonical_conversion (proji, Const_cs c2),sk2 with Not_found -> let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in -- cgit v1.2.3