aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-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
5 files changed, 54 insertions, 1 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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-08 11:18:02 +0000