X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fnum.ml;h=962feaf3011efa95e31f0e64e0f995a394800350;hb=a34071ed728b8de44b198de4e73a52207557ed81;hp=57cb19d068dee18d7df1cc070bc99cf448513e38;hpb=d97b1a852472085bf3449e34f3b25aee349686fd;p=fireball-separation.git diff --git a/ocaml/num.ml b/ocaml/num.ml index 57cb19d..962feaf 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -99,19 +99,18 @@ let free_vars = (List.map fst) ++ free_vars';; module ToScott = struct -let rec scott_of_nf = - function - | `N n -> Scott.mk_n n - | `Var(v,_) -> Pure.V v - | `Match(t,_,liftno,bs,args) -> - let bs = List.map (fun (n,t) -> n, scott_of_nf (lift liftno (t :> nf))) !bs in - let t = scott_of_nf (t :> nf) in - let m = Scott.mk_match t bs in - List.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) m (args :> nf list) - | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) (Pure.V v) (args :> nf Listx.listx) - | `Lam(b,f) -> Pure.L (scott_of_nf f) - | `Bottom -> let f x = Pure.A (x,x) in f (Pure.L (f (Pure.V 0))) - | `Pacman -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0)))) +let rec scott_of_nf = function + | `N n -> Scott.mk_n n + | `Var(v,_) -> Pure.V v + | `Match(t,_,liftno,bs,args) -> + let bs = List.map (fun (n,t) -> n, scott_of_nf (lift liftno (t :> nf))) !bs in + let t = scott_of_nf (t :> nf) in + let m = Scott.mk_match t bs in + List.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) m (args :> nf list) + | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) (Pure.V v) (args :> nf Listx.listx) + | `Lam(_,t) -> Pure.L (scott_of_nf t) + | `Bottom -> Pure.B + | `Pacman -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0)))) end @@ -127,7 +126,7 @@ let rec string_of_term l = | `Lam(_,`Bottom) -> "BOMB" | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")" | `Match(t,(v,ar),bs_lift,bs,args) -> - "[match_"^ string_of_var v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^"_ " ^ string_of_term_no_pars l (t :> nf) ^ + "["^ string_of_var 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)) ^ ")" | `Bottom -> "BOT" @@ -173,6 +172,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 _ | `Bottom | `Pacman as t -> t | `Lam(false, t) -> `Lam(false, set_arity arity t) @@ -267,28 +267,6 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool (************ Parsing ************************************) -let parse' strs = - let fix_arity = function - | `I((n,_),args) -> `I((n,1+Listx.length args),args) - | _ -> assert false in - let (tms, free) = Parser.parse_many strs in - (* Replace pacmans and bottoms *) - let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in - let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in - let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in - let fix lev v = - if v = lev + n_bot then `Bottom - else if v = lev + n_pac then `Pacman - else if v = lev + n_bomb then `Lam(true, `Bottom) - else `Var(v,1) in (* 1 by default when variable not applied *) - (* Fix arity *) - let rec aux lev = function - | Parser.Lam t -> `Lam (true, aux (lev+1) t) - | Parser.App (t1, t2) -> fix_arity (mk_app (aux lev t1) (aux lev t2)) - | Parser.Var v -> fix lev v in - List.map (aux 0) tms, free -;; - (************** Algorithm(s) ************************) let eta_compare x y = @@ -344,9 +322,9 @@ let rec eta_subterm sub t = eta_subterm sub (u :> nf) || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs || 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' + | `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 :> nf list)) (Listx.to_list args' :> nf list)) | _ -> false @@ -370,6 +348,6 @@ let max_arity_tms n = | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l (args :> nf list))) (aux_tms l (List.map snd !bs)) | `N _ | `Bottom | `Pacman -> 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) ;;