From 0de302096ed1cbd654313e98cc5c65cf8dc82466 Mon Sep 17 00:00:00 2001 From: acondolu Date: Mon, 24 Jul 2017 14:55:31 +0200 Subject: [PATCH] Fixed bug in computing special k --- ocaml/lambda4.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) 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) = -- 2.39.2