diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 62 |
1 files changed, 30 insertions, 32 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 11fba7b94..7c91b1a93 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -42,6 +42,7 @@ open Glob_ops open Evarconv open Pattern open Misctypes +open Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t @@ -319,7 +320,7 @@ let ltac_interp_name_env k0 lvar env = let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let env = pop_rel_context n env in - let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in + let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in push_rel_context ctxt env let invert_ltac_bound_name lvar env id0 id = @@ -372,8 +373,7 @@ let pretype_id pretype k0 loc env evdref lvar id = str "Variable " ++ pr_id id ++ str " should be bound to a term."); (* Check if [id] is a section or goal variable *) try - let (_,_,typ) = lookup_named id env in - { uj_val = mkVar id; uj_type = typ } + { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found_loc loc id @@ -418,8 +418,7 @@ let pretype_ref loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try let (_,_,ty) = lookup_named id env in - make_judge (mkVar id) ty + (try make_judge (mkVar id) (get_type (lookup_named id env)) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -459,6 +458,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in + let open Context.Rel.Declaration in match t with | GRef (loc,ref,u) -> inh_conv_coerce_to_tycon loc env evdref @@ -518,14 +518,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ [] -> ctxt | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let dcl = (na,None,ty'.utj_val) in - let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in + let dcl = LocalAssum (na, ty'.utj_val) in + let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in - let dcl = (na,Some bd'.uj_val,ty'.utj_val) in - let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in + let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in + let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = @@ -694,7 +694,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = (name,None,j.utj_val) in + let var = LocalAssum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env (orelse_name name name') j j' in @@ -738,7 +738,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = (name,Some j.uj_val,t) in + let var = LocalDef (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in @@ -763,17 +763,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ int cs.cs_nargs ++ str " variables."); let fsign, record = match get_projections env indf with - | None -> List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args, false + | None -> + List.map2 set_name (List.rev nal) cs.cs_args, false | Some ps -> let rec aux n k names l = match names, l with - | na :: names, ((_, None, t) :: l) -> + | na :: names, (LocalAssum (_,t) :: l) -> let proj = Projection.make ps.(cs.cs_nargs - k) true in - (na, Some (lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val))), t) + LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l - | na :: names, ((_, c, t) :: l) -> - (na, c, t) :: aux (n+1) k names l + | na :: names, (decl :: l) -> + set_name na decl :: aux (n+1) k names l | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in @@ -781,7 +781,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if not record then let nal = List.map (fun na -> ltac_interp_name lvar na) nal in let nal = List.rev nal in - let fsign = List.map2 (fun na (_,b,t) -> (na,b,t)) nal fsign in + let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info env (fst ind) LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) @@ -792,10 +792,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let arsgn = let arsgn,_ = get_arity env indf in if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + List.map (set_name Anonymous) arsgn else arsgn in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in + let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in let nar = List.length arsgn in (match po with | Some p -> @@ -851,11 +851,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let arsgn,_ = get_arity env indf in if not !allow_anonymous_refs then (* Make dependencies from arity signature impossible *) - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + List.map (set_name Anonymous) arsgn else arsgn in let nar = List.length arsgn in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in + let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in let pred,p = match po with | Some p -> let env_p = push_rel_context psign env in @@ -880,14 +880,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let pi = beta_applist (pi, [build_dependent_constructor cs]) in let csgn = if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args + List.map (set_name Anonymous) cs.cs_args else - List.map - (fun (n, b, t) -> - match n with - Name _ -> (n, b, t) - | Anonymous -> (Name Namegen.default_non_dependent_ident, b, t)) - cs.cs_args + List.map (map_name (function Name _ as n -> n + | Anonymous -> Name Namegen.default_non_dependent_ident)) + cs.cs_args in let env_c = push_rel_context csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in @@ -949,8 +946,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ in inh_conv_coerce_to_tycon loc env evdref cj tycon and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = - let f (id,_,t) (subst,update) = - let t = replace_vars subst t in + let f decl (subst,update) = + let id = get_id decl in + let t = replace_vars subst (get_type decl) in let c, update = try let c = List.assoc id update in @@ -962,7 +960,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = if is_conv env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try - let (_,_,t') = lookup_named id env in + let t' = lookup_named id env |> get_type in if is_conv env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ |