X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fnum.ml;h=2bc253d0554bbdec893c04d6878e2354cfb31020;hb=dcb2ece094f794f4e9f4f98b92f378998e92a919;hp=eb37e4ca41d0c1b2b6f27f6ddf24edadacaba842;hpb=415e18c6bfb1bbd125123ff9eb22b2caa7c42187;p=fireball-separation.git

diff --git a/ocaml/num.ml b/ocaml/num.ml
index eb37e4c..2bc253d 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -2,6 +2,9 @@ open Util
 open Util.Vars
 open Pure
 
+(* debug options *)
+let debug_display_arities = false;;
+
 (************ Syntax ************************************)
 
 (* Normal forms*)
@@ -109,22 +112,24 @@ end
 
 (************ Pretty-printing ************************************)
 
-let rec string_of_term l =
- let rec string_of_term_w_pars l = function
-  | `Var(n,ar) -> print_name l n ^ ":" ^ string_of_int ar
+(* let rec string_of_term l  = fun _ -> "";; *)
+
+let rec string_of_term l  =
+ let rec string_of_term_w_pars l  = function
+  | `Var(n,ar) -> List.nth l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
   | `N n -> string_of_int n
   | `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")"
   | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")"
   | `Match(t,(v,ar),bs_lift,bs,args) ->
-     "[match("^ string_of_var v ^":"^ string_of_int ar ^") " ^ string_of_term_no_pars l (t :> nf) ^
-     " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift t)) !bs) ^ "] " ^
-     String.concat " " (List.map (string_of_term l) args) ^ ")"
- and string_of_term_no_pars_app l = function
-  | `I((n,ar), args) -> print_name l n  ^ ":" ^ string_of_int ar ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args))
+     "["^ List.nth l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars l (t :> nf) ^
+     " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift (t :> nf))) !bs) ^ "] " ^
+     String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
+ and string_of_term_no_pars_app l  = function
+  | `I((n,ar), args) -> List.nth l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args :> nf list))
   | #nf as t -> string_of_term_w_pars l t
  and string_of_term_no_pars_lam l  = function
-  | `Lam(_,t) -> let name = string_of_var (List.length l) in
-   "λ" ^ name ^ ". " ^ (string_of_term_no_pars_lam (name::l) t)
+  | `Lam(_,t) -> let name = "x" ^ string_of_int (List.length l) in
+     "λ" ^ name ^ ". " ^ (string_of_term_no_pars_lam (name::l) t)
   | _ as t -> string_of_term_no_pars l t
  and string_of_term_no_pars l : nf -> string = function
   | `Lam _ as t -> string_of_term_no_pars_lam l t
@@ -159,6 +164,7 @@ let cast_to_i_num_var =
     assert false (* algorithm failed *)
 
 let rec set_arity arity = function
+(* FIXME because onlt variables should be in branches of matches, one day *)
 | `Var(n,_) -> `Var(n,arity)
 | `N _ as t -> t
 | `Lam(false, t) -> `Lam(false, set_arity arity t)
@@ -236,20 +242,6 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool
   aux 0 where
 ;;
 
-(************ Parsing ************************************)
-
-let parse' strs =
-  let fix_arity = function
-  | `I((n,_),args) -> `I((n,1+Listx.length args),args)
-  | _ -> assert false in
-  let rec aux = function
-  | Parser.Lam t -> `Lam (true, aux t)
-  | Parser.App (t1, t2) -> fix_arity (mk_app (aux t1) (aux t2))
-  | Parser.Var v -> `Var(v,1) in
-  let (tms, free) = Parser.parse_many strs in
-  List.map aux tms, free
-;;
-
 (************** Algorithm(s) ************************)
 
 let eta_compare x y =
@@ -294,10 +286,10 @@ let rec eta_subterm sub t =
   | `Match(u,ar,liftno,bs,args) ->
      eta_subterm sub (u :> nf)
      || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
-     || List.exists (eta_subterm sub) args
-  | `I(v, args) -> List.exists (eta_subterm sub) (Listx.to_list args) || (match sub with
-   | `Var v' -> v = v'
-   | `I(v', args') -> v = v'
+     || List.exists (eta_subterm sub) (args :> nf list)
+  | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
+   | `Var(v',_) -> v = v'
+   | `I((v',_), args') -> v = v'
     && Listx.length args' < Listx.length args
     && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args)) (Listx.to_list args'))
    | _ -> false
@@ -322,7 +314,7 @@ let max_arity_tms n =
   | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
   | `N _ -> None
  and aux_tms l =
-  List.fold_left (fun acc t -> Pervasives.max acc (aux l t)) None in
+  List.fold_left (fun acc t -> max acc (aux l t)) None in
  fun tms -> aux_tms 0 (tms :> nf list)
 ;;