aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/indfun.ml2
-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/subtac/subtac_pretyping_F.ml39
-rw-r--r--interp/constrextern.ml5
-rw-r--r--interp/constrintern.ml3
-rw-r--r--interp/implicit_quantifiers.ml42
-rw-r--r--interp/implicit_quantifiers.mli17
-rw-r--r--interp/reserve.ml1
-rw-r--r--interp/topconstr.ml16
-rw-r--r--interp/topconstr.mli2
-rw-r--r--lib/option.ml6
-rw-r--r--lib/option.mli2
-rw-r--r--parsing/g_constr.ml424
-rw-r--r--parsing/ppconstr.ml11
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/pretyping.ml39
-rw-r--r--pretyping/rawterm.ml9
-rw-r--r--pretyping/rawterm.mli1
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--toplevel/classes.ml6
-rw-r--r--toplevel/whelp.ml44
23 files changed, 211 insertions, 40 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 46e33360cf..320bac8302 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -212,6 +212,7 @@ 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) ->
@@ -612,6 +613,7 @@ let rec add_args id new_args b =
CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
| CCast(loc,b1,CastCoerce) ->
CCast(loc,add_args id new_args b1,CastCoerce)
+ | CRecord _ -> anomaly "add_args : CRecord"
| CNotation _ -> anomaly "add_args : CNotation"
| CGeneralization _ -> anomaly "add_args : CGeneralization"
| CPrim _ -> b
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 08a97fd221..7534ce2ca7 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -583,6 +583,7 @@ 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 *)
@@ -685,6 +686,7 @@ 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"
@@ -1024,7 +1026,7 @@ let rec compute_cst_params relnames params = function
discriminitation ones *)
| RSort _ -> params
| RHole _ -> params
- | RIf _ | RRec _ | RCast _ | RDynamic _ ->
+ | RIf _ | RRecord _ | 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 92396af590..ffd7cd007d 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -176,6 +176,7 @@ 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
@@ -358,6 +359,7 @@ 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)) ->
@@ -409,6 +411,7 @@ 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
@@ -507,6 +510,7 @@ 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)) ->
@@ -604,6 +608,8 @@ 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 *)
@@ -661,6 +667,7 @@ 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
@@ -705,6 +712,7 @@ 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 203bc9e3dd..e7c6c5bcbf 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,6 +210,8 @@ 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/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 8201e8fdcc..3c32c40682 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -501,6 +501,45 @@ 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 add71a8b09..67946e3a28 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -676,6 +676,11 @@ let rec extern inctx scopes vars r =
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
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' =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cfa88f3cd0..ef7ad36f12 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -946,6 +946,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
(* Now compact "(f args') args" *)
| 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)
| 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 876af8f54b..0bfc109ab3 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -63,6 +63,24 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
| c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
in aux bound l c
+let ids_of_names l =
+ List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
+
+let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
+ let rec aux bdvars l c = match c with
+ ((LocalRawAssum (n, _, c)) :: tl) ->
+ let bound = ids_of_names n in
+ let l' = free_vars_of_constr_expr c ~bound:bdvars l in
+ aux (Idset.union (ids_of_list bound) bdvars) l' tl
+
+ | ((LocalRawDef (n, c)) :: tl) ->
+ let bound = match snd n with Anonymous -> [] | Name n -> [n] in
+ let l' = free_vars_of_constr_expr c ~bound:bdvars l in
+ aux (Idset.union (ids_of_list bound) bdvars) l' tl
+
+ | [] -> bdvars, l
+ in aux bound l binders
+
let add_name_to_ids set na =
match na with
| Anonymous -> set
@@ -80,6 +98,8 @@ 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
@@ -128,33 +148,11 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) =
in
fun rt -> List.rev (vars bound [] rt)
-
-let ids_of_names l =
- List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
-
-let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
- let rec aux bdvars l c = match c with
- ((LocalRawAssum (n, _, c)) :: tl) ->
- let bound = ids_of_names n in
- let l' = free_vars_of_constr_expr c ~bound:bdvars l in
- aux (Idset.union (ids_of_list bound) bdvars) l' tl
-
- | ((LocalRawDef (n, c)) :: tl) ->
- let bound = match snd n with Anonymous -> [] | Name n -> [n] in
- let l' = free_vars_of_constr_expr c ~bound:bdvars l in
- aux (Idset.union (ids_of_list bound) bdvars) l' tl
-
- | [] -> bdvars, l
- in aux bound l binders
-
let rec make_fresh ids env x =
if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
let freevars_of_ids env ids =
List.filter (is_freevar env (Global.env())) ids
-
-let binder_list_of_ids ids =
- List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids
let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 5934272091..dc83e2135c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -28,19 +28,20 @@ val ids_of_list : identifier list -> Idset.t
val destClassApp : constr_expr -> loc * reference * constr_expr list
val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
-val free_vars_of_constr_expr : Topconstr.constr_expr ->
- ?bound:Idset.t ->
- Names.identifier list -> Names.identifier list
+(* Fragile, should be used only for construction a set of identifiers to avoid *)
-val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
-
-val binder_list_of_ids : identifier list -> local_binder list
-
-val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
+ identifier list -> identifier list
val free_vars_of_binders :
?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
+(* Returns the free ids in left-to-right order with the location of their first occurence *)
+
+val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
+
+val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+
val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
val combine_params_freevar :
diff --git a/interp/reserve.ml b/interp/reserve.ml
index f49c42a55d..2479f1f04e 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -57,6 +57,7 @@ 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 c0b81c90c3..3dc77dd604 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -37,6 +37,7 @@ 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
@@ -82,6 +83,8 @@ 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
@@ -146,7 +149,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 _ | RCases _ | RRec _ | RDynamic _
+ | (RLetIn _ | RRecord _ | RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
| _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
@@ -192,6 +195,7 @@ 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,
@@ -319,6 +323,12 @@ 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
@@ -637,6 +647,7 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
+ | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
| CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
@@ -709,6 +720,7 @@ let constr_loc = function
| CLetIn (loc,_,_,_) -> loc
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
+ | CRecord (loc,_,_) -> loc
| CCases (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
@@ -806,6 +818,7 @@ let fold_constr_expr_with_binders g f n acc = function
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ ->
acc
+ | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
| CCases (loc,sty,rtnpo,al,bl) ->
let ids = ids_of_cases_tomatch al in
let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
@@ -919,6 +932,7 @@ let map_constr_expr_with_binders g f e = function
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CDynamic _ | CRef _ as x -> x
+ | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
| CCases (loc,sty,rtnpo,a,bl) ->
(* TODO: apply g on the binding variables in pat... *)
let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 0064d238d1..b6e2927bbd 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -33,6 +33,7 @@ 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
@@ -133,6 +134,7 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
+ | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
| CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
diff --git a/lib/option.ml b/lib/option.ml
index 543c108ab9..3d98034256 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id:$ i*)
+(*i $Id$ i*)
(** Module implementing basic combinators for OCaml option type.
It tries follow closely the style of OCaml standard library.
@@ -97,6 +97,10 @@ let fold_right f x a =
| Some y -> f y a
| _ -> a
+(** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *)
+let cata f a = function
+ | Some c -> f c
+ | None -> a
(** {6 More Specific operations} ***)
diff --git a/lib/option.mli b/lib/option.mli
index c1260d9acf..04f3ca37d0 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -66,6 +66,8 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
+(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
+val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
(** {6 More Specific Operations} ***)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 77b4f003cd..5ecbab90ed 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -25,7 +25,7 @@ let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
"end"; "as"; "let"; "if"; "then"; "else"; "return";
"Prop"; "Set"; "Type"; ".("; "_"; "..";
- "`{"; "`("; ]
+ "`{"; "`("; "{|"; "|}" ]
let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
@@ -125,6 +125,18 @@ let ident_colon =
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
+let ident_with =
+ Gram.Entry.of_parser "ident_with"
+ (fun strm ->
+ match Stream.npeek 1 strm with
+ | [("IDENT",s)] ->
+ (match Stream.npeek 2 strm with
+ | [_; ("", "with")] ->
+ Stream.junk strm; Stream.junk strm;
+ Names.id_of_string s
+ | _ -> raise Stream.Failure)
+ | _ -> raise Stream.Failure)
+
let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
GEXTEND Gram
@@ -205,6 +217,7 @@ GEXTEND Gram
CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
CNotation(loc,"( _ )",([c],[]))
| _ -> c)
+ | "{|"; c = record_declaration; "|}" -> c
| "`{"; c = operconstr LEVEL "200"; "}" ->
CGeneralization (loc, Implicit, None, c)
| "`("; c = operconstr LEVEL "200"; ")" ->
@@ -221,6 +234,15 @@ GEXTEND Gram
| IDENT "λ" -> ()
] ]
;
+ record_declaration:
+ [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
+ | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" ->
+ CRecord (loc, Some c, fs)
+ ] ]
+ ;
+ record_field_declaration:
+ [ [ id = identref; ":="; c = lconstr -> (id, c) ] ]
+ ;
binder_constr:
[ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
mkCProdN loc bl c
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index a2cad8e170..19446b7d19 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -552,6 +552,17 @@ let rec pr sep inherited a =
else
p, lproj
| CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
+ | CRecord (_,w,l) ->
+ let beg =
+ match w with
+ | None -> spc ()
+ | Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc ()
+ in
+ hv 0 (str"{" ++ beg ++
+ prlist_with_sep (fun () -> spc () ++ str";" ++ spc ())
+ (fun ((_,id), c) -> pr_id id ++ spc () ++ str":=" ++ spc () ++ pr spc ltop c)
+ l), latom
+
| CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
hv 0 (
str "let '" ++
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.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4e87109187..4eca304c24 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -257,7 +257,9 @@ let new_class id par ar sup props =
type binder_def_list = (identifier located * identifier located list * constr_expr) list
let binders_of_lidents l =
- List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l
+ List.map (fun (loc, id) ->
+ LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
+ CHole (loc, Some (BinderType (Name id))))) l
let type_ctx_instance isevars env ctx inst subst =
let (s, _) =
@@ -312,7 +314,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
let tclass =
match bk with
| Implicit ->
- Implicit_quantifiers.implicit_application Idset.empty
+ Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false
(fun avoid (clname, (id, _, t)) ->
match clname with
| Some (cl, b) ->
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 82a2a84495..094c931968 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
- | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
- error "Whelp does not support pattern-matching and (co-)fixpoint."
+ | RRecord _ | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
+ error "Whelp does not support records, 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.25.1) at 2026-03-19 07:24:56 +0000