diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 39 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 9 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 1 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 2 |
5 files changed, 55 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6854a4a7c5..eb4c737914 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -603,6 +603,12 @@ let rec subst_rawconstr subst raw = if r1' == r1 && r2' == r2 then raw else RLetIn (loc,n,r1',r2') + | RRecord (loc,w,rl) -> + let w' = Option.smartmap (subst_rawconstr subst) w + and rl' = list_smartmap (fun (id, x) -> (id, subst_rawconstr subst x)) rl in + if w == w' && rl == rl' then raw else + RRecord (loc,w',rl') + | RCases (loc,sty,rtno,rl,branches) -> let rtno' = Option.smartmap (subst_rawconstr subst) rtno and rl' = list_smartmap (fun (a,x as y) -> 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) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index ea622de7f4..b2e770f65a 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -62,6 +62,7 @@ type rawconstr = | RLambda of loc * name * binding_kind * rawconstr * rawconstr | RProd of loc * name * binding_kind * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr + | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr @@ -114,6 +115,7 @@ let map_rawconstr f = function | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c) | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c) | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c) + | RRecord (loc,c,l) -> RRecord (loc,Option.map f c,List.map (fun (id,c) -> id, f c) l) | RCases (loc,sty,rtntypopt,tml,pl) -> RCases (loc,sty,Option.map f rtntypopt, List.map (fun (tm,x) -> (f tm,x)) tml, @@ -174,6 +176,8 @@ let occur_rawconstr id = | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c)) + | RRecord (loc,w,l) -> Option.cata occur false w + or List.exists (fun (_, c) -> occur c) l | RCases (loc,sty,rtntypopt,tml,pl) -> (occur_option rtntypopt) or (List.exists (fun (tm,_) -> occur tm) tml) @@ -219,7 +223,9 @@ let free_rawvars = | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in - vars bounded' vs' c + vars bounded' vs' c + | RRecord (loc,f,args) -> + List.fold_left (vars bounded) vs (Option.List.cons f (List.map snd args)) | RCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bounded vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in @@ -280,6 +286,7 @@ let loc_of_rawconstr = function | RLambda (loc,_,_,_,_) -> loc | RProd (loc,_,_,_,_) -> loc | RLetIn (loc,_,_,_) -> loc + | RRecord (loc,_,_) -> loc | RCases (loc,_,_,_,_) -> loc | RLetTuple (loc,_,_,_,_) -> loc | RIf (loc,_,_,_,_) -> loc diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 3628e2a503..5115e2d59b 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -66,6 +66,7 @@ type rawconstr = | RLambda of loc * name * binding_kind * rawconstr * rawconstr | RProd of loc * name * binding_kind * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr + | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 97fbae075b..c437d9eab2 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -25,7 +25,7 @@ open Util (* This module defines type-classes *) type typeclass = { (* The class implementation: a record parameterized by the context with defs in it or a definition if - the class is a singleton. This acts as the classe's global identifier. *) + the class is a singleton. This acts as the class' global identifier. *) cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. |