diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 34 |
1 files changed, 20 insertions, 14 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 99e51330e..020f998aa 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -23,6 +23,7 @@ open Globnames open Evd open Pretype_errors open Sigma.Notations +open Context.Rel.Declaration type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result @@ -55,12 +56,15 @@ let eval_flexible_term ts env evd c = then constant_opt_value_in env cu else None | Rel n -> - (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v - with Not_found -> None) + (try match lookup_rel n env with + | LocalAssum _ -> None + | LocalDef (_,v,_) -> Some (lift n v) + with Not_found -> None) | Var id -> (try if is_transparent_variable ts id then - let (_,v,_) = lookup_named id env in v + let open Context.Named.Declaration in + lookup_named id env |> get_value else None with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) @@ -394,7 +398,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty assert (match sk with [] -> true | _ -> false); let (na,c1,c'1) = destLambda term in let c = nf_evar evd c1 in - let env' = push_rel (na,None,c) env in + let env' = push_rel (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 let out2 = whd_nored_state evd @@ -561,7 +565,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty 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 (na,Some b,t) env) i pbty c'1 c'2); + evar_conv_x ts (push_rel (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) @@ -676,7 +680,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let c = nf_evar i c1 in let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)] + evar_conv_x ts (push_rel (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 @@ -735,7 +739,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let c = nf_evar i c1 in let na = Nameops.name_max n1 n2 in - evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)] + evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then @@ -912,6 +916,7 @@ let choose_less_dependent_instance evk evd term args = | [] -> None | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) +open Context.Named.Declaration let apply_on_subterm env evdref f c t = let rec applyrec (env,(k,c) as acc) t = (* By using eq_constr, we make an approximation, for instance, we *) @@ -922,7 +927,7 @@ let apply_on_subterm env evdref f c t = match kind_of_term t with | Evar (evk,args) when Evd.is_undefined !evdref evk -> let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in - let g (_,b,_) a = if Option.is_empty b then applyrec acc a else a 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 @@ -939,17 +944,17 @@ let filter_possible_projections c ty ctxt args = let fv2 = collect_vars (mkApp (c,args)) in let len = Array.length args in let tyvars = collect_vars ty in - List.map_i (fun i (id,b,_) -> + List.map_i (fun i decl -> let () = assert (i < len) in let a = Array.unsafe_get args i in - (match b with None -> false | Some c -> not (isRel c || isVar c)) || + (match decl with LocalAssum _ -> false | LocalDef (_,c,_) -> not (isRel c || isVar 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 || - Id.Set.mem id tyvars) + Id.Set.mem (get_id decl) tyvars) 0 ctxt let solve_evars = ref (fun _ -> failwith "solve_evars not installed") @@ -980,17 +985,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - let instance = List.map mkVar (List.map pi1 ctxt) in + let instance = List.map mkVar (List.map get_id ctxt) in let rec make_subst = function - | (id,_,t)::ctxt', c::l, occs::occsl when isVarId id c -> + | decl'::ctxt', c::l, occs::occsl when isVarId (get_id decl') c -> begin match occs with | Some _ -> error "Cannot force abstraction on identity instance." | None -> make_subst (ctxt',l,occsl) end - | (id,_,t)::ctxt', c::l, occs::occsl -> + | decl'::ctxt', c::l, occs::occsl -> + let (id,_,t) = to_tuple 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 |