X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=d927411a1598dae8d06b599eb4a85deb520bb8e1;hb=0197354468e40860a3a104b9ea5b68854a22cfca;hp=83c1b1dab20be45651ca6ead3406f005f173c7b9;hpb=5664c5924f59c805c6e658698cc2fa535cab27f6;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 83c1b1d..d927411 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -53,7 +53,7 @@ let measure_of_term, measure_of_terms =
  let rec aux = function
  | `N _ -> 0
  | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
- | `Lam(_,t) -> aux t
+ | `Lam(_,t,g) -> assert (g = []); aux t
  | `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
@@ -66,7 +66,7 @@ let count_fakevars p =
  let rec aux = function
  | `N _ -> 0
  | `Var(_,ar) -> if ar = min_int then 1 else 0
- | `Lam(_,t) -> aux t
+ | `Lam(_,t,g) -> assert (g = []); aux t
  | `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
@@ -120,7 +120,7 @@ let make_fresh_vars p arities =
 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
@@ -486,14 +486,14 @@ let instantiate p x n =
  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
- | `Lam(b,t) -> aux (k + if b then 1 else 0) t
+ | `Lam(b,t,g) -> assert (g = []); aux (k + if b then 1 else 0) t
  | `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))
@@ -501,7 +501,7 @@ let compute_special_k tms =
  | `Var _ -> 0
  ) in
  let rec aux' top t = match t with
- | `Lam(_,t) -> aux' false t
+ | `Lam(_,t,g) -> assert (g = []); aux' false t
  | `I((_,ar), tms) -> max ar
      (Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
  | `Match(t, _, liftno, bs, args) ->
@@ -615,7 +615,7 @@ let optimize_numerals p =
     | `N n -> `N (List.nth perm n)
     | `I _ -> assert false
     | `Var _ as t -> t
-    | `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