aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/indfun.ml9
-rw-r--r--contrib/funind/rawterm_to_relation.ml76
-rw-r--r--contrib/funind/rawtermops.ml4
3 files changed, 68 insertions, 21 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index b1e561e923..f6d554a85c 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -95,7 +95,14 @@ let rec is_rec names =
(lookup names b) || (lookup names lhs) || (lookup names rhs)
| RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b) ->
lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
- | RLetTuple(_,_,_,t,b) -> error "RLetTuple not handled"
+ | RLetTuple(_,nal,_,t,b) -> lookup names t ||
+ lookup
+ (List.fold_left
+ (fun acc na -> Nameops.name_fold Idset.remove na acc)
+ names
+ nal
+ )
+ b
| RApp(_,f,args) -> List.exists (lookup names) (f::args)
| RCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index b0c4f4cda7..b6f26dfdd3 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -341,7 +341,7 @@ let make_pattern_eq_precond id e pat =
res
-let build_constructors_of_type msg ind' =
+let build_constructors_of_type msg ind' argl =
let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
let npar = mib.Declarations.mind_nparams in
Array.mapi (fun i _ ->
@@ -355,29 +355,33 @@ let build_constructors_of_type msg ind' =
(Global.env ())
construct
in
+ let argl =
+ if argl = []
+ then
+ Array.to_list
+ (Array.init (cst_narg - npar) (fun _ -> mkRHole ())
+ )
+ else argl
+ in
let pat_as_term =
- mkRApp(mkRRef (ConstructRef(ind',i+1)),
- Array.to_list
- (Array.init (cst_narg - npar) (fun _ -> mkRHole ())
- )
- )
+ mkRApp(mkRRef (ConstructRef(ind',i+1)),argl)
in
(* Pp.msgnl (str "new constructor := " ++ Printer.pr_rawconstr pat_as_term); *)
cases_pattern_of_rawconstr Anonymous pat_as_term
)
ind.Declarations.mind_consnames
-let find_constructors_of_raw_type msg t =
+let find_constructors_of_raw_type msg t argl : Rawterm.cases_pattern array =
let ind,args = raw_decompose_app t in
match ind with
| RRef(_,IndRef ind') ->
(* let _,ind = Global.lookup_inductive ind' in *)
- build_constructors_of_type msg ind'
+ build_constructors_of_type msg ind' argl
| _ -> error msg
-let rec find_type_of b =
+let rec find_type_of nb b =
let f,_ = raw_decompose_app b in
match f with
| RRef(_,ref) ->
@@ -399,11 +403,11 @@ let rec find_type_of b =
| ConstructRef c -> fst c
in
let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in
- if not (Array.length ind_type_info.Declarations.mind_consnames = 2 )
- then raise (Invalid_argument "find_type_of : not an if inductive");
+ if not (Array.length ind_type_info.Declarations.mind_consnames = nb )
+ then raise (Invalid_argument "find_type_of : not a valid inductive");
ind_type
end
- | RCast(_,b,_,_) -> find_type_of b
+ | RCast(_,b,_,_) -> find_type_of nb b
| RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *)
| _ -> raise (Invalid_argument "not a ref")
@@ -472,14 +476,13 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
funnames
avoid
(mkRLetIn(new_n,t,mkRApp(new_b,args)))
- | RCases _ | RLambda _ | RIf _ ->
+ | RCases _ | RLambda _ | RIf _ | RLetTuple _ ->
let f_res = build_entry_lc funnames args_res.to_avoid f in
combine_results combine_app f_res args_res
| RDynamic _ ->error "Not handled RDynamic"
| RCast(_,b,_,_) ->
build_entry_lc funnames avoid (mkRApp(b,args))
| RRec _ -> error "Not handled RRec"
- | RLetTuple _ -> error "Not handled RLetTuple"
| RProd _ -> error "Cannot apply a type"
end
| RLambda(_,n,t,b) ->
@@ -507,7 +510,7 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
match b with
| RCast(_,b,_,t) ->
let msg = "If construction must be used with cast" in
- let case_pat = find_constructors_of_raw_type msg t in
+ let case_pat = find_constructors_of_raw_type msg t [] in
assert (Array.length case_pat = 2);
let brl =
list_map_i
@@ -522,8 +525,8 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
build_entry_lc funnames avoid match_expr
| _ ->
try
- let ind = find_type_of b in
- let case_pat = build_constructors_of_type (str "") ind in
+ let ind = find_type_of 2 b in
+ let case_pat = build_constructors_of_type (str "") ind [] in
let brl =
list_map_i
(fun i x -> (dummy_loc,[],[case_pat.(i)],x))
@@ -540,8 +543,43 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
error msg
end
-
- | RLetTuple _ -> error "Not handled RLetTuple"
+ | RLetTuple(_,nal,_,b,e) ->
+ begin
+ let nal_as_rawconstr =
+ List.map
+ (function
+ Name id -> mkRVar id
+ | Anonymous -> mkRHole ()
+ )
+ nal
+ in
+ match b with
+ | RCast(_,b,_,t) ->
+ let case_pat =
+ find_constructors_of_raw_type
+ "LetTuple construction must be used with cast" t nal_as_rawconstr in
+ assert (Array.length case_pat = 1);
+ let br =
+ (dummy_loc,[],[case_pat.(0)],e)
+ in
+ let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+ build_entry_lc funnames avoid match_expr
+ | _ ->
+ try
+ let ind = find_type_of 1 b in
+ let case_pat =
+ build_constructors_of_type
+ (str "LetTuple construction must be used with cast") ind nal_as_rawconstr in
+ let br =
+ (dummy_loc,[],[case_pat.(0)],e)
+ in
+ let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+ build_entry_lc funnames avoid match_expr
+ with Invalid_argument s ->
+ let msg = "LetTuple construction must be used with cast : "^ s in
+ error msg
+
+ end
| RRec _ -> error "Not handled RRec"
| RCast(_,b,_,_) ->
build_entry_lc funnames avoid b
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index f99aa86c8b..92efd3b470 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -109,7 +109,9 @@ let change_vars =
change_vars mapping def,
change_vars mapping b
)
- | RLetTuple(_,nal,(na,_),_,_) when List.exists (function Name id -> Idmap.mem id mapping | _ -> false) (na::nal) -> rt
+ | RLetTuple(_,nal,(na,_),_,_) when
+ List.exists (function Name id -> Idmap.mem id mapping | _ -> false) (na::nal) ->
+ rt
| RLetTuple(loc,nal,(na,rto),b,e) ->
RLetTuple(loc,
nal,
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:49:42 +0000