Fixes to how arities are assigned and propagated

[fireball-separation.git] / ocaml / num.ml

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 81bb1dafe0bb1dbfb1f0a05ad896edae95a594a2..3c84f4f6236f937ed4eec92efbf3f5eabd261ef4 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -169,7 +169,7 @@ let rec mk_app (h : nf) (arg : nf) =
  match h with
     `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
   | `Var v -> `I(v, Listx.Nil arg)
-  | `Lam(_,nf) -> subst true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
+  | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
   | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
   | `N _ -> assert false (* Numbers cannot be applied *)
 (*in let l = ["v0";"v1";"v2"] in
@@ -194,10 +194,11 @@ and mk_match t (n,ar) bs_lift bs args =
         `Match (t,(n,ar),bs_lift,bs,args))
   | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
 
-and subst delift_by_one what (with_what : nf) (where : nf) =
+and subst truelam delift_by_one what (with_what : nf) (where : nf) =
  let aux_propagate_arity ar = function
- | `Lam(false,`Match(`I(v,args),(x,_),liftno,bs,args')) ->
+ | `Lam(false,`Match(`I(v,args),(x,_),liftno,bs,args')) when not delift_by_one ->
     `Lam(false,`Match(`I(v,args),(x,ar),liftno,bs,args'))
+ | `Var(i,_) -> `Var(i,ar)
  | _ as t -> t in
  let rec aux_i_num_var l =
   function
@@ -218,7 +219,7 @@ and subst delift_by_one what (with_what : nf) (where : nf) =
        let with_what' = lift l' with_what in
        (* The following line should be the identity when delift_by_one = true because we
           are assuming the ts to not contain lambda-bound variables. *)
-       bs := List.map (fun (n,t) -> n,subst false what with_what' t) !bs ;
+       bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
        mk_match (cast_to_i_num_var (aux_i_num_var l t)) v bs_lift bs (List.map (aux l) args)
  and aux l(*lift*) =
 (*function iii -> let res = match iii with*)