aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/indfun.ml1
-rw-r--r--contrib/funind/rawterm_to_relation.ml4
-rw-r--r--contrib/funind/rawtermops.ml8
-rw-r--r--contrib/interface/depends.ml2
-rw-r--r--contrib/interface/xlate.ml2
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml39
-rw-r--r--interp/constrextern.ml5
-rw-r--r--interp/constrintern.ml34
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/reserve.ml1
-rw-r--r--interp/topconstr.ml12
-rw-r--r--interp/topconstr.mli1
-rw-r--r--library/libnames.ml12
-rw-r--r--library/libnames.mli1
-rw-r--r--parsing/g_constr.ml48
-rw-r--r--parsing/g_vernac.ml48
-rw-r--r--parsing/ppvernac.ml35
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/pretyping.ml47
-rw-r--r--pretyping/rawterm.ml7
-rw-r--r--pretyping/rawterm.mli1
-rw-r--r--pretyping/recordops.ml17
-rwxr-xr-xpretyping/recordops.mli11
-rw-r--r--toplevel/record.ml32
-rw-r--r--toplevel/record.mli4
-rw-r--r--toplevel/vernacentries.ml2
-rw-r--r--toplevel/vernacexpr.ml7
-rw-r--r--toplevel/whelp.ml44
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 _ ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 06:31:09 +0000