aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/indfun.ml8
-rw-r--r--contrib/funind/rawterm_to_relation.ml6
-rw-r--r--contrib/funind/rawtermops.ml35
3 files changed, 31 insertions, 18 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 3fb6641879..dc1dc2cfb2 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -209,7 +209,7 @@ let rec is_rec names =
let rec lookup names = function
| RVar(_,id) -> check_id id names
| RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false
- | RCast(_,b,_,_) -> lookup names b
+ | RCast(_,b,_) -> lookup names b
| RRec _ -> error "RRec not handled"
| RIf(_,b,_,lhs,rhs) ->
(lookup names b) || (lookup names lhs) || (lookup names rhs)
@@ -611,8 +611,10 @@ let rec add_args id new_args b =
| CPatVar _ -> b
| CEvar _ -> b
| CSort _ -> b
- | CCast(loc,b1,ck,b2) ->
- CCast(loc,add_args id new_args b1,ck,add_args id new_args b2)
+ | CCast(loc,b1,CastConv(ck,b2)) ->
+ 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)
| CNotation _ -> anomaly "add_args : CNotation"
| CPrim _ -> b
| CDelimiters _ -> anomaly "add_args : CDelimiters"
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index aca84f0627..b34a1097a3 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -351,7 +351,7 @@ let rec find_type_of nb b =
then raise (Invalid_argument "find_type_of : not a valid inductive");
ind_type
end
- | RCast(_,b,_,_) -> find_type_of nb 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")
@@ -575,7 +575,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
let f_res = build_entry_lc env funnames args_res.to_avoid f in
combine_results combine_app f_res args_res
| RDynamic _ ->error "Not handled RDynamic"
- | RCast(_,b,_,_) ->
+ | RCast(_,b,_) ->
(* for an applied cast we just trash the cast part
and restart the work.
@@ -685,7 +685,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
end
| RRec _ -> error "Not handled RRec"
- | RCast(_,b,_,_) ->
+ | RCast(_,b,_) ->
build_entry_lc env funnames avoid b
| RDynamic _ -> error "Not handled RDynamic"
and build_entry_lc_from_case env funname make_discr
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 6af8d2c36c..f9e188dacf 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
let mkRSort s = RSort(dummy_loc,s)
let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t)
+let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
(*
Some basic functions to decompose rawconstrs
@@ -177,8 +177,10 @@ let change_vars =
| RRec _ -> error "Local (co)fixes are not supported"
| RSort _ -> rt
| RHole _ -> rt
- | RCast(loc,b,k,t) ->
- RCast(loc,change_vars mapping b,k,change_vars mapping t)
+ | RCast(loc,b,CastConv (k,t)) ->
+ RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
+ | RCast(loc,b,CastCoerce) ->
+ RCast(loc,change_vars mapping b,CastCoerce)
| RDynamic _ -> error "Not handled RDynamic"
and change_vars_br mapping ((loc,idl,patl,res) as br) =
let new_mapping = List.fold_right Idmap.remove idl mapping in
@@ -356,8 +358,10 @@ let rec alpha_rt excluded rt =
| RRec _ -> error "Not handled RRec"
| RSort _ -> rt
| RHole _ -> rt
- | RCast (loc,b,k,t) ->
- RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t)
+ | RCast (loc,b,CastConv (k,t)) ->
+ RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
+ | RCast (loc,b,CastCoerce) ->
+ RCast(loc,alpha_rt excluded b,CastCoerce)
| RDynamic _ -> error "Not handled RDynamic"
| RApp(loc,f,args) ->
RApp(loc,
@@ -407,7 +411,8 @@ let is_free_in id =
| RRec _ -> raise (UserError("",str "Not handled RRec"))
| RSort _ -> false
| RHole _ -> false
- | RCast (_,b,_,t) -> is_free_in b || is_free_in t
+ | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
+ | RCast (_,b,CastCoerce) -> is_free_in b
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
and is_free_in_br (_,ids,_,rt) =
(not (List.mem id ids)) && is_free_in rt
@@ -501,8 +506,10 @@ let replace_var_by_term x_id term =
| RRec _ -> raise (UserError("",str "Not handled RRec"))
| RSort _ -> rt
| RHole _ -> rt
- | RCast(loc,b,k,t) ->
- RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t)
+ | RCast(loc,b,CastConv(k,t)) ->
+ RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
+ | RCast(loc,b,CastCoerce) ->
+ RCast(loc,replace_var_by_pattern b,CastCoerce)
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
if List.exists (fun id -> id_ord id x_id == 0) idl
@@ -586,7 +593,8 @@ let ids_of_rawterm c =
| RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
| RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
| RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
- | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+ | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+ | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
| RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
| RLetTuple (_,nal,(na,po),b,c) ->
List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
@@ -651,8 +659,10 @@ let zeta_normalize =
| RRec _ -> raise (UserError("",str "Not handled RRec"))
| RSort _ -> rt
| RHole _ -> rt
- | RCast(loc,b,k,t) ->
- RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t)
+ | RCast(loc,b,CastConv(k,t)) ->
+ RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
+ | RCast(loc,b,CastCoerce) ->
+ RCast(loc,zeta_normalize_term b,CastCoerce)
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
and zeta_normalize_br (loc,idl,patl,res) =
(loc,idl,patl,zeta_normalize_term res)
@@ -692,7 +702,8 @@ let expand_as =
expand_as map br1, expand_as map br2)
| RRec _ -> error "Not handled RRec"
| RDynamic _ -> error "Not handled RDynamic"
- | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t)
+ | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
+ | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
| RCases(loc,po,el,brl) ->
RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 23:11:53 +0000