| `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
| `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 then 0 else ar - 1) + aux_many args
and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
| `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
| `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 then 0 else ar - 1) + aux_many args
and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
| `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
| `Match(u,v,_,_,args) -> aux (u :> nf) + aux (`Var v) + aux_many args
and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
| `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
| `Match(u,v,_,_,args) -> aux (u :> nf) + aux (`Var v) + aux_many args
and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
let simple_expand_match ps =
let rec aux level = function
| #i_num_var as t -> (aux_i_num_var level t :> nf)
let simple_expand_match ps =
let rec aux level = function
| #i_num_var as t -> (aux_i_num_var level t :> nf)
- | `Lam(b,t) -> `Lam(b,aux (level+1) t)
+ | `Lam(b,t,g) -> assert (g = []); `Lam(b,aux (level+1) t,[])
and aux_i_num_var level = function
| `Match(u,v,bs_lift,bs,args) as torig ->
let (u : i_num_var) = aux_i_num_var level u in
and aux_i_num_var level = function
| `Match(u,v,bs_lift,bs,args) as torig ->
let (u : i_num_var) = aux_i_num_var level u in
let args = Listx.from_list (vars :> nf list) in
let bs = ref [] in
(* 666, since it will be replaced anyway during subst: *)
let args = Listx.from_list (vars :> nf list) in
let bs = ref [] in
(* 666, since it will be replaced anyway during subst: *)
- let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,-666),1,bs,[])) in
+ let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,-666),1,bs,[]),[]) in
let p = {p with deltas=bs::p.deltas} in
subst_in_problem x inst p
;;
let compute_special_k tms =
let rec aux k (t: nf) = Pervasives.max k (match t with
let p = {p with deltas=bs::p.deltas} in
subst_in_problem x inst p
;;
let compute_special_k tms =
let rec aux k (t: nf) = Pervasives.max k (match t with
| `I(n, tms) -> Listx.max (Listx.map (aux 0) tms)
| `Match(t, _, liftno, bs, args) ->
List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
| `I(n, tms) -> Listx.max (Listx.map (aux 0) tms)
| `Match(t, _, liftno, bs, args) ->
List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
| `I((_,ar), tms) -> max ar
(Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
| `Match(t, _, liftno, bs, args) ->
| `I((_,ar), tms) -> max ar
(Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
| `Match(t, _, liftno, bs, args) ->
- | `Lam(v,t) -> `Lam(v, aux t)
+ | `Lam(v,t,g) -> assert (g = []); `Lam(v, aux t,[])
| `Match(_,_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t
in List.map (fun (n,t) -> (n,aux t))
in
| `Match(_,_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t
in List.map (fun (n,t) -> (n,aux t))
in