From 5438bfe94fd1cb0d22de54df53bd0e09328a90a4 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 5 Nov 2008 20:16:13 +0000 Subject: Move Record desugaring to constrintern and add ability to use notations for record fields (using "someproj : sometype where not := constr" syntax). Only one notation allowed currently and no redeclaration after the record declaration either (will be done for typeclasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/funind/indfun.ml | 1 - contrib/funind/rawterm_to_relation.ml | 4 +-- contrib/funind/rawtermops.ml | 8 ------ contrib/interface/depends.ml | 2 -- contrib/interface/xlate.ml | 2 +- contrib/subtac/subtac_pretyping_F.ml | 39 ----------------------------- interp/constrextern.ml | 5 ---- interp/constrintern.ml | 34 +++++++++++++++++++++++-- interp/implicit_quantifiers.ml | 2 -- interp/reserve.ml | 1 - interp/topconstr.ml | 12 +-------- interp/topconstr.mli | 1 - library/libnames.ml | 12 ++++++--- library/libnames.mli | 1 + parsing/g_constr.ml4 | 8 +++++- parsing/g_vernac.ml4 | 8 +++--- parsing/ppvernac.ml | 35 +++++++++++++------------- pretyping/detyping.ml | 6 ----- pretyping/pretyping.ml | 47 +++-------------------------------- pretyping/rawterm.ml | 7 ------ pretyping/rawterm.mli | 1 - pretyping/recordops.ml | 17 ++++++++----- pretyping/recordops.mli | 11 +++++++- toplevel/record.ml | 32 ++++++++++++++---------- toplevel/record.mli | 4 +-- toplevel/vernacentries.ml | 2 +- toplevel/vernacexpr.ml | 7 +++--- toplevel/whelp.ml4 | 4 +-- 28 files changed, 123 insertions(+), 190 deletions(-) diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 320bac830..b6b2cbd11 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -212,7 +212,6 @@ let rec is_rec names = | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false | RCast(_,b,_) -> lookup names b | RRec _ -> error "RRec not handled" - | RRecord _ -> error "Not handled RRecord" | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 48a96f8b6..c16e645c7 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -583,7 +583,6 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = *) build_entry_lc env funnames avoid (mkRApp(b,args)) | RRec _ -> error "Not handled RRec" - | RRecord _ -> error "Not handled RRecord" | RProd _ -> error "Cannot apply a type" end (* end of the application treatement *) @@ -686,7 +685,6 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = end | RRec _ -> error "Not handled RRec" - | RRecord _ -> error "Not handled RRecord" | RCast(_,b,_) -> build_entry_lc env funnames avoid b | RDynamic _ -> error "Not handled RDynamic" @@ -1026,7 +1024,7 @@ let rec compute_cst_params relnames params = function discriminitation ones *) | RSort _ -> params | RHole _ -> params - | RIf _ | RRecord _ | RRec _ | RCast _ | RDynamic _ -> + | RIf _ | RRec _ | RCast _ | RDynamic _ -> raise (UserError("compute_cst_params", str "Not handled case")) and compute_cst_params_from_app acc (params,rtl) = match params,rtl with diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index ffd7cd007..92396af59 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -176,7 +176,6 @@ let change_vars = change_vars mapping lhs, change_vars mapping rhs ) - | RRecord _ -> error "Records are not supported" | RRec _ -> error "Local (co)fixes are not supported" | RSort _ -> rt | RHole _ -> rt @@ -359,7 +358,6 @@ let rec alpha_rt excluded rt = alpha_rt excluded rhs ) | RRec _ -> error "Not handled RRec" - | RRecord _ -> error "Not handled RRecord" | RSort _ -> rt | RHole _ -> rt | RCast (loc,b,CastConv (k,t)) -> @@ -411,7 +409,6 @@ let is_free_in id = | RIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | RRecord _ -> raise (UserError ("", str "Not handled RRecord")) | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> false | RHole _ -> false @@ -510,7 +507,6 @@ let replace_var_by_term x_id term = replace_var_by_pattern rhs ) | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RRecord _ -> raise (UserError("",str "Not handled RRecord")) | RSort _ -> rt | RHole _ -> rt | RCast(loc,b,CastConv(k,t)) -> @@ -608,8 +604,6 @@ let ids_of_rawterm c = | RCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) | RRec _ -> failwith "Fix inside a constructor branch" - | RRecord (loc,w,l) -> Option.cata (ids_of_rawterm []) [] w @ - List.flatten (List.map (fun ((_,id), x) -> id :: ids_of_rawterm [] x) l) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> [] in (* build the set *) @@ -667,7 +661,6 @@ let zeta_normalize = zeta_normalize_term lhs, zeta_normalize_term rhs ) - | RRecord _ -> raise (UserError("",str "Not handled RRecord")) | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt @@ -712,7 +705,6 @@ let expand_as = | RIf(loc,e,(na,po),br1,br2) -> RIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) - | RRecord _ -> error "Not handled RRecord" | RRec _ -> error "Not handled RRec" | RDynamic _ -> error "Not handled RDynamic" | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index e7c6c5bcb..203bc9e3d 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -210,8 +210,6 @@ let rec depends_of_rawconstr rc acc = match rc with | RLambda (_, _, _, rct, rcb) | RProd (_, _, _, rct, rcb) | RLetIn (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc) - | RRecord (_, w, l) -> depends_of_rawconstr_list (List.map snd l) - (Option.fold_right depends_of_rawconstr w acc) | RCases (_, _, rco, tmt, cc) -> (* LEM TODO: handle the cc *) (Option.fold_right depends_of_rawconstr rco diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 2b6f681f1..73acbf0f3 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1501,7 +1501,7 @@ let build_constructors l = CT_constr_list (List.map f l) let build_record_field_list l = - let build_record_field (coe,d) = match d with + let build_record_field ((coe,d),not) = match d with | AssumExpr (id,c) -> if coe then CT_recconstr_coercion (xlate_id_opt id, xlate_formula c) else diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 3c32c4068..8201e8fdc 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -501,45 +501,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct in { uj_val = v; uj_type = p } - | RRecord (loc,w,l) -> - let cw = Option.map (pretype tycon env isevars 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 !isevars) cj.uj_type - with Not_found -> - error_case_not_inductive_loc loc env (evars_of !isevars) 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 isevars lvar constructor - | RCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty ((fun vtyc env isevars -> pretype vtyc env isevars lvar),isevars) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 67946e3a2..237ffb55b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -677,11 +677,6 @@ let rec extern inctx scopes vars r = let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) - | RRecord (loc,w,l) -> - let t' = Option.map (extern inctx scopes vars) w in - let l' = List.map (fun (id, c) -> (id, extern inctx scopes vars c)) l in - CRecord (loc, t', l') - | RCases (loc,sty,rtntypopt,tml,eqns) -> let vars' = List.fold_right (name_fold Idset.add) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index dd94bf42d..660da5525 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -948,8 +948,38 @@ let internalise sigma globalenv env allow_patvar lvar c = | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) | _ -> RApp (loc, c, args)) | CRecord (loc, w, fs) -> - RRecord (loc, Option.map (intern env) w, - List.map (fun (id, c) -> (id, intern env c)) fs) + let id, _ = List.hd fs in + let record = + let (id,_,_,_),_ = intern_applied_reference intern env lvar [] (Ident id) in + match id with + | RRef (loc, ref) -> + (try Recordops.find_projection ref + with Not_found -> user_err_loc (loc, "intern", str"Not a projection")) + | c -> user_err_loc (loc_of_rawconstr id, "intern", str"Not a projection") + in + let args = + let pars = list_make record.Recordops.s_EXPECTEDPARAM (CHole (loc, None)) in + let fields, rest = + List.fold_left (fun (args, rest as acc) (na, b) -> + if b then + try + let id = out_name na in + let _, t = List.assoc id rest in + t :: args, List.remove_assoc id rest + with _ -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: args, rest + else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) fs) record.Recordops.s_PROJKIND + in + if rest <> [] then + let id, (loc, t) = List.hd rest in + user_err_loc (loc,"intern",(str "Unknown field name " ++ pr_id id)) + else pars @ List.rev fields + in + let constrname = + Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef record.Recordops.s_CONST)) + in + let app = CAppExpl (loc, (None, constrname), args) in + intern env app + | CCases (loc, sty, rtnpo, tms, eqns) -> let tms,env' = List.fold_right (fun citm (inds,env) -> diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 0bfc109ab..d48c85616 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -98,8 +98,6 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) = let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in vars bound' vs' c - | RRecord (loc,w,l) -> List.fold_left (vars bound) vs - (Option.List.cons w (List.map snd l)) | RCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bound vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in diff --git a/interp/reserve.ml b/interp/reserve.ml index 2479f1f04..f49c42a55 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -57,7 +57,6 @@ let rec unloc = function | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c) | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c) | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RRecord (_,w,l) -> RRecord (dummy_loc,w,l) | RCases (_,sty,rtntypopt,tml,pl) -> RCases (dummy_loc,sty, (Option.map unloc rtntypopt), diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 3dc77dd60..2cbe53981 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -37,7 +37,6 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ARecord of aconstr option * (identifier * aconstr) list | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * (cases_pattern list * aconstr) list @@ -83,8 +82,6 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c) | ALetIn (na,b,c) -> let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c) - | ARecord (b,l) -> - RRecord (loc, Option.map (f e) b, List.map (fun (id, x) -> ((loc,id),f e x)) l) | ACases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -149,7 +146,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with f ty1 ty2 & f c1 c2 | RHole _, RHole _ -> true | RSort (_,s1), RSort (_,s2) -> s1 = s2 - | (RLetIn _ | RRecord _ | RCases _ | RRec _ | RDynamic _ + | (RLetIn _ | RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) @@ -195,7 +192,6 @@ let aconstr_and_vars_of_rawconstr a = | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) - | RRecord (_,w,l) -> ARecord (Option.map aux w,List.map (fun ((_,id), x) -> id, aux x) l) | RCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in ACases (sty,Option.map aux rtntypopt, @@ -323,12 +319,6 @@ let rec subst_aconstr subst bound raw = if r1' == r1 && r2' == r2 then raw else ALetIn (n,r1',r2') - | ARecord (r1,r2) -> - let r1' = Option.smartmap (subst_aconstr subst bound) r1 - and r2' = list_smartmap (fun (id, x) -> id,subst_aconstr subst bound x) r2 in - if r1' == r1 && r2' == r2 then raw else - ARecord (r1',r2') - | ACases (sty,rtntypopt,rl,branches) -> let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt and rl' = list_smartmap diff --git a/interp/topconstr.mli b/interp/topconstr.mli index b6e2927bb..2d293eacb 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -33,7 +33,6 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ARecord of aconstr option * (identifier * aconstr) list | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * (cases_pattern list * aconstr) list diff --git a/library/libnames.ml b/library/libnames.ml index 04ab34baa..bf02efb03 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -24,6 +24,11 @@ type global_reference = let isVarRef = function VarRef _ -> true | _ -> false +let subst_constructor subst ((kn,i),j as ref) = + let kn' = subst_kn subst kn in + if kn==kn' then ref, mkConstruct ref + else ((kn',i),j), mkConstruct ((kn',i),j) + let subst_global subst ref = match ref with | VarRef var -> ref, mkVar var | ConstRef kn -> @@ -32,10 +37,9 @@ let subst_global subst ref = match ref with | IndRef (kn,i) -> let kn' = subst_kn subst kn in if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i) - | ConstructRef ((kn,i),j) -> - let kn' = subst_kn subst kn in - if kn==kn' then ref, mkConstruct ((kn,i),j) - else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j) + | ConstructRef ((kn,i),j as c) -> + let c',t = subst_constructor subst c in + if c'==c then ref,t else ConstructRef c', t let global_of_constr c = match kind_of_term c with | Const sp -> ConstRef sp diff --git a/library/libnames.mli b/library/libnames.mli index 890a442e3..399387dd7 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -25,6 +25,7 @@ type global_reference = val isVarRef : global_reference -> bool +val subst_constructor : substitution -> constructor -> constructor * constr val subst_global : substitution -> global_reference -> global_reference * constr (* Turn a global reference into a construction *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 5ecbab90e..b061da5a8 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -42,6 +42,11 @@ let loc_of_binder_let = function | LocalRawDef ((loc,_),_)::_ -> loc | _ -> dummy_loc +let binders_of_lidents l = + List.map (fun (loc, id) -> + LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, + CHole (loc, Some (Evd.BinderType (Name id))))) l + let rec index_and_rec_order_of_annot loc bl ann = match names_of_local_assums bl,ann with | [loc,Name id], (None, r) -> Some (loc, id), r @@ -241,7 +246,8 @@ GEXTEND Gram ] ] ; record_field_declaration: - [ [ id = identref; ":="; c = lconstr -> (id, c) ] ] + [ [ id = identref; params = LIST0 identref; ":="; c = lconstr -> + (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ] ; binder_constr: [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3f8adb92f..e1df1cf49 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -172,11 +172,6 @@ GEXTEND Gram ":="; cstr = OPT identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> VernacRecord (b,(oc,name),ps,s,cstr,fs) -(* Non porté ? - | f = finite_token; s = csort; id = identref; - indpar = LIST0 simple_binder; ":="; lc = constructor_list -> - VernacInductive (f,[id,None,indpar,s,lc]) -*) ] ] ; typeclass_context: @@ -331,6 +326,9 @@ GEXTEND Gram *) (* ... with coercions *) record_field: + [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ] + ; + record_binder: [ [ id = name -> (false,AssumExpr(id,CHole (loc, None))) | id = name; oc = of_type_with_opt_coercion; t = lconstr -> (oc,AssumExpr (id,t)) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index e2237450c..3c8613aad 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -411,23 +411,22 @@ let pr_intarg n = spc () ++ int n in let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l ++ sep ++ pr_constrarg c in - - let pr_record_field = function - | (oc,AssumExpr (id,t)) -> - hov 1 (pr_lname id ++ - (if oc then str" :>" else str" :") ++ spc() ++ - pr_lconstr_expr t) - | (oc,DefExpr(id,b,opt)) -> - (match opt with - | Some t -> - hov 1 (pr_lname id ++ - (if oc then str" :>" else str" :") ++ spc() ++ - pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) - | None -> - hov 1 (pr_lname id ++ str" :=" ++ spc() ++ - pr_lconstr b)) +let pr_record_field (x, ntn) = + let prx = match x with + | (oc,AssumExpr (id,t)) -> + hov 1 (pr_lname id ++ + (if oc then str" :>" else str" :") ++ spc() ++ + pr_lconstr_expr t) + | (oc,DefExpr(id,b,opt)) -> (match opt with + | Some t -> + hov 1 (pr_lname id ++ + (if oc then str" :>" else str" :") ++ spc() ++ + pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) + | None -> + hov 1 (pr_lname id ++ str" :=" ++ spc() ++ + pr_lconstr b)) in + prx ++ pr_decl_notation pr_constr ntn in - let pr_record_decl c fs = pr_opt pr_lident c ++ str"{" ++ hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") @@ -708,7 +707,7 @@ let rec pr_vernac = function (* prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ *) pr_and_type_binders_arg par ++ (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++ - spc () ++ str"where" ++ spc () ++ + spc () ++ str":=" ++ spc () ++ prlist_with_sep (fun () -> str";" ++ spc()) (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) @@ -720,7 +719,7 @@ let rec pr_vernac = function str"=>" ++ spc () ++ (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++ pr_constr_expr cl ++ spc () ++ - spc () ++ str"where" ++ spc () ++ + spc () ++ str":=" ++ spc () ++ prlist_with_sep (fun () -> str";" ++ spc()) (pr_instance_def (spc () ++ str":=" ++ spc())) props) | VernacContext l -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index eb4c73791..6854a4a7c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -603,12 +603,6 @@ 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 83594466e..7400cdd9c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -586,45 +586,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct mkCase (ci, pred, cj.uj_val, [|b1;b2|]) 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 @@ -644,8 +605,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct (* ... except for Correctness *) let v = mkCast (cj.uj_val, k, tj.utj_val) in { uj_val = v; uj_type = tj.utj_val } - in - inh_conv_coerce_to_tycon loc env evdref cj tycon + in inh_conv_coerce_to_tycon loc env evdref cj tycon | RDynamic (loc,d) -> if (tag d) = "constr" then @@ -732,13 +692,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in let c = pretype_gen_aux evdref env lvar kind c in - let evd,_ = consider_remaining_unif_problems env !evdref in if fail_evar then - let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env !evdref in let c = Evarutil.nf_isevar evd c in check_evars env Evd.empty evd c; evd, c - else evd, c + else !evdref, c (** Entry points of the high-level type synthesis algorithm *) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index b2e770f65..4d3348407 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -62,7 +62,6 @@ 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 @@ -115,7 +114,6 @@ 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, @@ -176,8 +174,6 @@ 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) @@ -224,8 +220,6 @@ let free_rawvars = let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in 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 @@ -286,7 +280,6 @@ 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 5115e2d59..3628e2a50 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -66,7 +66,6 @@ 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/recordops.ml b/pretyping/recordops.ml index a9fcaa4c4..99f439224 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -32,9 +32,9 @@ open Reductionops projection ou bien une fonction constante (associée à un LetIn) *) type struc_typ = { - s_CONST : identifier; + s_CONST : constructor; s_EXPECTEDPARAM : int; - s_PROJKIND : bool list; + s_PROJKIND : (name * bool) list; s_PROJ : constant option list } let structure_table = ref (Indmap.empty : struc_typ Indmap.t) @@ -61,8 +61,9 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = (Option.smartmap (fun kn -> fst (subst_con subst kn))) projs in - if projs' == projs && kn' == kn then obj else - ((kn',i),id,kl,projs') + let id' = fst (subst_constructor subst id) in + if projs' == projs && kn' == kn && id' == id then obj else + ((kn',i),id',kl,projs') let discharge_structure (_,(ind,id,kl,projs)) = Some (Lib.discharge_inductive ind, id, kl, @@ -88,6 +89,10 @@ let find_projection_nparams = function | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM | _ -> raise Not_found +let find_projection = function + | ConstRef cst -> Cmap.find cst !projection_table + | _ -> raise Not_found + (************************************************************************) (*s A canonical structure declares "canonical" conversion hints between *) @@ -135,7 +140,7 @@ let canonical_projections () = !object_table [] let keep_true_projections projs kinds = - map_succeed (function (p,true) -> p | _ -> failwith "") + map_succeed (function (p,(_,true)) -> p | _ -> failwith "") (List.combine projs kinds) let cs_pattern_of_constr t = @@ -237,7 +242,7 @@ let check_and_decompose_canonical_structure ref = | Construct (indsp,1) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in - let ntrue_projs = List.length (List.filter (fun x -> x) s.s_PROJKIND) in + let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref; (sp,indsp) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 020687009..638cc4304 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -21,8 +21,14 @@ open Library (*s A structure S is a non recursive inductive type with a single constructor (the name of which defaults to Build_S) *) +type struc_typ = { + s_CONST : constructor; + s_EXPECTEDPARAM : int; + s_PROJKIND : (name * bool) list; + s_PROJ : constant option list } + val declare_structure : - inductive * identifier * bool list * constant option list -> unit + inductive * constructor * (name * bool) list * constant option list -> unit (* [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise @@ -32,6 +38,9 @@ val lookup_projections : inductive -> constant option list (* raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int +(* raise [Not_found] if not a projection *) +val find_projection : global_reference -> struc_typ + (*s A canonical structure declares "canonical" conversion hints between *) (* the effective components of a structure and the projections of the *) (* structure *) diff --git a/toplevel/record.ml b/toplevel/record.ml index 8d3dd67e7..5ebd89789 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -40,9 +40,9 @@ let mk_interning_data env na impls typ = let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) -let interp_fields_evars isevars env l = - List.fold_left - (fun (env, uimpls, params, impls) ((loc, i), b, t) -> +let interp_fields_evars isevars env nots l = + List.fold_left2 + (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in let impls = @@ -51,8 +51,10 @@ let interp_fields_evars isevars env l = | Name na -> (fst impls, mk_interning_data env na impl t' :: snd impls) in let d = (i,b',t') in + (* Temporary declaration of notations and scopes *) + Option.iter (declare_interning_data impls) no; (push_rel d env, impl :: uimpls, d::params, impls)) - (env, [], [], ([], [])) l + (env, [], [], ([], [])) nots l let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) @@ -60,14 +62,14 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields id t ps fs = +let typecheck_params_and_fields id t ps nots fs = let env0 = Global.env () in let (env1,newps), imps = interp_context Evd.empty env0 ps in let fullarity = it_mkProd_or_LetIn t newps in let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let evars = ref (Evd.create_evar_defs Evd.empty) in let env2,impls,newfs,data = - interp_fields_evars evars env_ar (binders_of_decls fs) + interp_fields_evars evars env_ar nots (binders_of_decls fs) in let newps = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newps in let newfs = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newfs in @@ -213,7 +215,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls with NotDefinable why -> warning_or_error coe indsp why; (None::sp_projs,NoProjection fi::subst) in - (nfi-1,(optci=None)::kinds,sp_projs,subst)) + (nfi-1,(fi, optci=None)::kinds,sp_projs,subst)) (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) @@ -239,12 +241,13 @@ let declare_structure finite id idbuild paramimpls params arity fieldimpls field let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in let build = ConstructRef (rsp,1) in if is_coe then Class.try_add_new_coercion build Global; - Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs); + Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs); kn (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) let definition_structure (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) = + let cfs,notations = List.split cfs in let coers,fs = List.split cfs in let extract_name acc = function Vernacexpr.AssumExpr((_,Name id),_) -> id::acc @@ -253,8 +256,11 @@ let definition_structure (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let allnames = idstruc::(List.fold_left extract_name [] fs) in if not (list_distinct allnames) then error "Two objects have the same name"; (* Now, younger decl in params and fields is on top *) - let implpars, params, implfs, fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in - let implfs = List.map - (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - declare_structure finite idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers - + let implpars, params, implfs, fields = + States.with_heavy_rollback (fun () -> + typecheck_params_and_fields idstruc (mkSort s) ps notations fs) () + in + let implfs = + List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs + in declare_structure finite idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers + diff --git a/toplevel/record.mli b/toplevel/record.mli index 9ac96641a..7aea948f3 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -24,7 +24,7 @@ open Impargs val declare_projections : inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> manual_explicitation list list -> rel_context -> - bool list * constant option list + (name * bool) list * constant option list val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> manual_explicitation list -> rel_context -> (* params *) @@ -37,4 +37,4 @@ val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> val definition_structure : bool (*coinductive?*)*lident with_coercion * local_binder list * - (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name + (local_decl_expr with_coercion with_notation) list * identifier * sorts -> kernel_name diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5a28d60cf..504561100 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -387,7 +387,7 @@ let vernac_record finite struc binders sort nameopt cfs = (constr_loc sort,"definition_structure", str "Sort expected.") in if Dumpglob.dump () then ( Dumpglob.dump_definition (snd struc) false "rec"; - List.iter (fun (_, x) -> + List.iter (fun ((_, x), _) -> match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ca539f28a..2727100bf 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -159,12 +159,13 @@ type decl_notation = (string * constr_expr * scope_name option) option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a +type 'a with_notation = 'a * decl_notation type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_coercion list + | RecordDecl of lident option * local_decl_expr with_coercion with_notation list type inductive_expr = - lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr + lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr type module_binder = bool option * lident list * module_type_ast @@ -217,7 +218,7 @@ type vernac_expr = (* Gallina extensions *) | VernacRecord of (bool*bool) (* = Record or Structure * Inductive or CoInductive *) * lident with_coercion * local_binder list - * constr_expr * lident option * local_decl_expr with_coercion list + * constr_expr * lident option * local_decl_expr with_coercion with_notation list | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 094c93196..82a2a8449 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -166,8 +166,8 @@ let rec uri_of_constr c = uri_of_constr b; url_string " in "; uri_of_constr c | RCast (_,c, CastConv (_,t)) -> uri_of_constr c; url_string ":"; uri_of_constr t - | RRecord _ | RRec _ | RIf _ | RLetTuple _ | RCases _ -> - error "Whelp does not support records, pattern-matching and (co-)fixpoint." + | RRec _ | RIf _ | RLetTuple _ | RCases _ -> + error "Whelp does not support pattern-matching and (co-)fixpoint." | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) -> anomaly "Written w/o parenthesis" | RPatVar _ | RDynamic _ -> -- cgit v1.2.3