From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 12:55:31 +0000 (+0200)
Subject: Fixed bug in computing special k
X-Git-Tag: weak-reduction-separation~6
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0de302096ed1cbd654313e98cc5c65cf8dc82466;p=fireball-separation.git

Fixed bug in computing special k
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 721f822..4726122 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -510,7 +510,16 @@ let compute_special_k tms =
      List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
  | `N _
  | `Var _ -> 0
- ) in Listx.max (Listx.map (aux 0) tms)
+ ) in
+ let rec aux' top t = match t with
+ | `Lam(_,t) -> aux' false t
+ | `I((_,ar), tms) -> max ar
+     (Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
+ | `Match(t, _, liftno, bs, args) ->
+     List.fold_left max 0 (List.map (aux' false) ((t :> nf)::(args :> nf list)@List.map snd !bs))
+ | `N _
+ | `Var _ -> 0 in
+ Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms)
 ;;
 
 let auto_instantiate (n,p) =