diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 08ecae12e8..c114a922c0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -587,6 +587,45 @@ module Pretyping_F (Coercion : Coercion.S) = struct in { uj_val = v; uj_type = p } + | RRecord (loc,w,l) -> + let cw = Option.map (pretype tycon env evdref lvar) w in + let cj = match cw with + | None -> + (match tycon with + | None -> user_err_loc (loc,"pretype",(str "Unnable to infer the record type.")) + | Some (_, ty) -> {uj_val=ty;uj_type=ty}) + | Some cj -> cj + in + let constructor = + let (IndType (indf,realargs)) = + try find_rectype env (evars_of !evdref) cj.uj_type + with Not_found -> + error_case_not_inductive_loc loc env (evars_of !evdref) cj + in + let cstrs = get_constructors env indf in + if Array.length cstrs <> 1 then + user_err_loc (loc,"pretype",(str "Inductive is not a singleton.")) + else + let info = cstrs.(0) in + let fields, rest = + List.fold_left (fun (args, rest as acc) (na, b, t) -> + if b = None then + try + let id = out_name na in + let _, t = List.assoc id rest in + t :: args, List.remove_assoc id rest + with _ -> RHole (loc, Evd.QuestionMark (Evd.Define false)) :: args, rest + else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) l) info.cs_args + in + if rest <> [] then + let id, (loc, t) = List.hd rest in + user_err_loc (loc,"pretype",(str "Unknown field name " ++ pr_id id)) + else + RApp (loc, + RDynamic (loc, constr_in (applistc (mkConstruct info.cs_cstr) info.cs_params)), + fields) + in pretype tycon env evdref lvar constructor + | RCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) |