aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/rawtermops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind/rawtermops.ml')
-rw-r--r--contrib/funind/rawtermops.ml62
1 files changed, 34 insertions, 28 deletions
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index e8cce47ad..0c03c1e61 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -12,8 +12,8 @@ let idmap_is_empty m = m = Idmap.empty
let mkRRef ref = RRef(dummy_loc,ref)
let mkRVar id = RVar(dummy_loc,id)
let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
-let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b)
-let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b)
+let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
+let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
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)
@@ -26,7 +26,7 @@ let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
*)
let raw_decompose_prod =
let rec raw_decompose_prod args = function
- | RProd(_,n,t,b) ->
+ | RProd(_,n,k,t,b) ->
raw_decompose_prod ((n,t)::args) b
| rt -> args,rt
in
@@ -34,7 +34,7 @@ let raw_decompose_prod =
let raw_decompose_prod_or_letin =
let rec raw_decompose_prod args = function
- | RProd(_,n,t,b) ->
+ | RProd(_,n,k,t,b) ->
raw_decompose_prod ((n,None,Some t)::args) b
| RLetIn(_,n,t,b) ->
raw_decompose_prod ((n,Some t,None)::args) b
@@ -58,7 +58,7 @@ let raw_decompose_prod_n n =
if i<=0 then args,c
else
match c with
- | RProd(_,n,t,b) ->
+ | RProd(_,n,_,t,b) ->
raw_decompose_prod (i-1) ((n,t)::args) b
| rt -> args,rt
in
@@ -70,7 +70,7 @@ let raw_decompose_prod_or_letin_n n =
if i<=0 then args,c
else
match c with
- | RProd(_,n,t,b) ->
+ | RProd(_,n,_,t,b) ->
raw_decompose_prod (i-1) ((n,None,Some t)::args) b
| RLetIn(_,n,t,b) ->
raw_decompose_prod (i-1) ((n,Some t,None)::args) b
@@ -135,15 +135,17 @@ let change_vars =
change_vars mapping rt',
List.map (change_vars mapping) rtl
)
- | RLambda(loc,name,t,b) ->
+ | RLambda(loc,name,k,t,b) ->
RLambda(loc,
name,
+ k,
change_vars mapping t,
change_vars (remove_name_from_mapping mapping name) b
)
- | RProd(loc,name,t,b) ->
+ | RProd(loc,name,k,t,b) ->
RProd(loc,
name,
+ k,
change_vars mapping t,
change_vars (remove_name_from_mapping mapping name) b
)
@@ -261,21 +263,21 @@ let rec alpha_rt excluded rt =
let new_rt =
match rt with
| RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
- | RLambda(loc,Anonymous,t,b) ->
+ | RLambda(loc,Anonymous,k,t,b) ->
let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in
let new_excluded = new_id :: excluded in
let new_t = alpha_rt new_excluded t in
let new_b = alpha_rt new_excluded b in
- RLambda(loc,Name new_id,new_t,new_b)
- | RProd(loc,Anonymous,t,b) ->
+ RLambda(loc,Name new_id,k,new_t,new_b)
+ | RProd(loc,Anonymous,k,t,b) ->
let new_t = alpha_rt excluded t in
let new_b = alpha_rt excluded b in
- RProd(loc,Anonymous,new_t,new_b)
+ RProd(loc,Anonymous,k,new_t,new_b)
| RLetIn(loc,Anonymous,t,b) ->
let new_t = alpha_rt excluded t in
let new_b = alpha_rt excluded b in
RLetIn(loc,Anonymous,new_t,new_b)
- | RLambda(loc,Name id,t,b) ->
+ | RLambda(loc,Name id,k,t,b) ->
let new_id = Nameops.next_ident_away id excluded in
let t,b =
if new_id = id
@@ -287,8 +289,8 @@ let rec alpha_rt excluded rt =
let new_excluded = new_id::excluded in
let new_t = alpha_rt new_excluded t in
let new_b = alpha_rt new_excluded b in
- RLambda(loc,Name new_id,new_t,new_b)
- | RProd(loc,Name id,t,b) ->
+ RLambda(loc,Name new_id,k,new_t,new_b)
+ | RProd(loc,Name id,k,t,b) ->
let new_id = Nameops.next_ident_away id excluded in
let new_excluded = new_id::excluded in
let t,b =
@@ -300,7 +302,7 @@ let rec alpha_rt excluded rt =
in
let new_t = alpha_rt new_excluded t in
let new_b = alpha_rt new_excluded b in
- RProd(loc,Name new_id,new_t,new_b)
+ RProd(loc,Name new_id,k,new_t,new_b)
| RLetIn(loc,Name id,t,b) ->
let new_id = Nameops.next_ident_away id excluded in
let t,b =
@@ -389,7 +391,7 @@ let is_free_in id =
| REvar _ -> false
| RPatVar _ -> false
| RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
- | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) ->
+ | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) ->
let check_in_b =
match n with
| Name id' -> id_ord id' id <> 0
@@ -460,17 +462,19 @@ let replace_var_by_term x_id term =
replace_var_by_pattern rt',
List.map replace_var_by_pattern rtl
)
- | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt
- | RLambda(loc,name,t,b) ->
+ | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+ | RLambda(loc,name,k,t,b) ->
RLambda(loc,
name,
+ k,
replace_var_by_pattern t,
replace_var_by_pattern b
)
- | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt
- | RProd(loc,name,t,b) ->
+ | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+ | RProd(loc,name,k,t,b) ->
RProd(loc,
name,
+ k,
replace_var_by_pattern t,
replace_var_by_pattern b
)
@@ -590,8 +594,8 @@ let ids_of_rawterm c =
| RVar (_,id) -> id::acc
| RApp (loc,g,args) ->
ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
- | 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
+ | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+ | RProd (loc,na,k,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,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
| RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
@@ -622,15 +626,17 @@ let zeta_normalize =
zeta_normalize_term rt',
List.map zeta_normalize_term rtl
)
- | RLambda(loc,name,t,b) ->
+ | RLambda(loc,name,k,t,b) ->
RLambda(loc,
name,
+ k,
zeta_normalize_term t,
zeta_normalize_term b
)
- | RProd(loc,name,t,b) ->
+ | RProd(loc,name,k,t,b) ->
RProd(loc,
- name,
+ name,
+ k,
zeta_normalize_term t,
zeta_normalize_term b
)
@@ -691,8 +697,8 @@ let expand_as =
with Not_found -> rt
end
| RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
- | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b)
- | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
+ | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b)
+ | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b)
| RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
| RLetTuple(loc,nal,(na,po),v,b) ->
RLetTuple(loc,nal,(na,Option.map (expand_as map) po),
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 02:21:32 +0000