From 744a6d34d9a52e406d4ab9786d8ab19a2b0091d0 Mon Sep 17 00:00:00 2001 From: acondolu Date: Wed, 12 Jul 2017 17:24:54 +0200 Subject: [PATCH] Towards `Bottom and `Pacman 1) Num updated to handle them 2) lambda4 compiles: safety conditions for projections hopefully implemented; strategy code not changed, therefore it will step over bombs and friends --- ocaml/lambda4.ml | 108 +++++++++-------- ocaml/num.ml | 176 ++++++++++++++-------------- ocaml/num.mli | 37 +++--- ocaml/numx.ml | 294 ----------------------------------------------- ocaml/numx.mli | 44 ------- 5 files changed, 155 insertions(+), 504 deletions(-) delete mode 100644 ocaml/numx.ml delete mode 100644 ocaml/numx.mli diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 86194cb..821da4c 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -34,46 +34,32 @@ let all_terms p = let sum_arities p = let rec aux = function - | `N _ -> 0 + | `N _ | `Bottom | `Pacman -> 0 | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*) | `Lam(_,t) -> aux t - | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args) - | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many args + | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list) + | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many (args :> nf list) and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in aux_many (all_terms p :> nf list) ;; -let count_fakevars p = - let rec aux = function - | `N _ -> 0 - | `Var(_,ar) -> if ar = min_int then 1 else 0 - | `Lam(_,t) -> 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 - aux_many (all_terms p :> nf list) -;; - -(* let problem_measure p = count_fakevars p, sum_arities p;; -let string_of_measure (a,b) = "(fakevars="^string_of_int a^",sum_arities="^string_of_int b^")" *) - let problem_measure p = sum_arities p;; let string_of_measure = string_of_int;; -let print_problem label ({freshno; div; conv; ps; deltas} as p) = +let string_of_problem label ({freshno; div; conv; ps; deltas} as p) = Console.print_hline (); prerr_endline ("\n||||| Displaying problem: " ^ label ^ " |||||"); - let nl = "\n| " in + let nl = "\n " in let deltas = String.concat nl (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in let l = Array.to_list (Array.init (freshno + 1) string_of_var) in nl ^ "measure="^string_of_measure(problem_measure p)^" freshno = " ^ string_of_int freshno - ^ nl ^ "\b> DISCRIMINATING SETS (deltas)" - ^ nl ^ deltas ^ (if deltas = "" then "" else nl) - ^ "\b> DIVERGENT" ^ nl - ^ "*: " ^ (match div with None -> "*" | Some div -> print ~l (div :> nf)) ^ "\n| " - ^ "\b> CONVERGENT" ^ nl - ^ String.concat "\n| " (List.map (fun t -> "_: " ^ (if t = `N (-1) then "_" else print ~l (t :> nf))) conv) ^ - (if conv = [] then "" else "\n| ") + ^nl^"\b> DISCRIMINATING SETS (deltas)" + ^nl^deltas^(if deltas = "" then "" else nl) + ^"\b (* DIVERGENT *)" ^ nl + ^" "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\" ") ^ nl + ^"\b (* CONVERGENT *) [" ^ nl + ^ String.concat " " (List.map (fun t -> "_: " ^ (if t = `N (-1) then "_" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ + (if conv = [] then "" else nl) ^ "\b> NUMERIC" ^ nl ^ String.concat "\n| " (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps) ^ nl @@ -81,7 +67,7 @@ let print_problem label ({freshno; div; conv; ps; deltas} as p) = let failwithProblem p reason = - print_endline (print_problem "FAIL" p); + print_endline (string_of_problem "FAIL" p); failwith reason ;; @@ -98,9 +84,13 @@ let make_fresh_vars p arities = ;; let simple_expand_match ps = - let rec aux level = function + let rec aux_nob level = function | #i_num_var as t -> aux_i_num_var level t | `Lam(b,t) -> `Lam(b,aux (level+1) t) + | `Pacman as t -> t + and aux level = function + | `Bottom as t -> t + | #nf_nob as t -> aux_nob level t and aux_i_num_var level = function | `Match(u,v,bs_lift,bs,args) as torig -> let u = aux_i_num_var level u in @@ -109,14 +99,14 @@ let simple_expand_match ps = (match u with | #i_n_var as u -> let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *) - in let t = mk_match (`N i) v bs_lift bs args in + in let t = mk_match (`N i) v bs_lift bs (args :> nf list) in if t <> torig then aux level (t :> nf) else raise Not_found | _ -> raise Not_found) with Not_found -> - `Match(cast_to_i_num_var u,v,bs_lift,bs,List.map (aux level) args)) - | `I(v,args) -> `I(v,Listx.map (aux level) args) + mk_appl (`Match(cast_to_i_num_var u,v,bs_lift,bs,[])) (List.map (aux_nob level) args)) + | `I(v,args) -> mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args)) | `N _ | `Var _ as t -> t in aux_i_num_var 0 ;; @@ -137,8 +127,6 @@ let super_simplify ({div; ps; conv} as p) = List.hd divs) div in {p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv} -exception ExpandedToLambda;; - let subst_in_problem x inst ({freshno; div; conv; ps; sigma} as p) = let len_ps = List.length ps in (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in @@ -161,14 +149,12 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) | [] -> acc | t::todo_conv -> (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) - (* try *) let t = subst false false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in aux' ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv - (* with ExpandedToLambda -> aux' ps (freshno,acc_conv@[`N(-1)],acc_new_ps) todo_conv *) (* cut&paste from aux' above *) and aux'' ps (freshno,acc_new_ps) = @@ -206,10 +192,11 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif bs := !bs @ [i, v] ; freshno in (*prerr_endlie ("t DA RIDURRE:" ^ print (`Match(`N i,arity,bs_lift,bs,args) :> nf) ^ " more_args=" ^ string_of_int more_args);*) - let t = mk_match (`N i) orig bs_lift bs args in + let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*) expand_match (freshno,acc_ps,acc_new_ps) t - | `Lam _ -> raise ExpandedToLambda + | `Lam _ | `Pacman -> assert false (* loose typing *) + | `Bottom -> assert false (* algorithm invariant *) | #i_n_var as x -> let x = simple_expand_match (acc_ps@acc_new_ps) x in freshno,cast_to_i_num_var x,acc_new_ps in @@ -229,7 +216,7 @@ prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst)); ); let p = {p with sigma = sigma@[x,inst]} in let p = super_simplify p in - prerr_endline (print_problem "instantiate" p); + prerr_endline (string_of_problem "instantiate" p); p ;; @@ -245,7 +232,8 @@ let rec dangerous arities showstoppers = function `N _ | `Var _ - | `Lam _ -> () + | `Lam _ + | `Pacman -> () | `Match(t,_,liftno,bs,args) -> (* CSC: XXX partial dependency on the encoding *) (match t with @@ -270,7 +258,8 @@ let rec dangerous_conv arities showstoppers = function `N _ | `Var _ - | `Lam _ -> [] + | `Lam _ + | `Pacman -> [] | `Match(t,_,liftno,bs,args) -> (* CSC: XXX partial dependency on the encoding *) (match t with @@ -284,6 +273,7 @@ let rec dangerous_conv arities showstoppers = and dangerous_inert_conv arities showstoppers k args match_args more_args = let all_args = args @ match_args in let dangerous_args = concat_map (dangerous_conv arities showstoppers) all_args in + let all_args = (all_args :> nf list) in if dangerous_args = [] then ( if List.mem k showstoppers then k :: concat_map free_vars all_args else try @@ -313,7 +303,7 @@ let rec edible arities div ps conv showstoppers = None -> aux showstoppers xs | Some h -> try - dangerous arities showstoppers (x : i_n_var :> nf) ; + dangerous arities showstoppers (x : i_n_var :> nf_nob) ; aux showstoppers xs with Dangerous -> @@ -321,7 +311,7 @@ let rec edible arities div ps conv showstoppers = in let showstoppers = sort_uniq (aux showstoppers ps) in let dangerous_conv = - List.map (dangerous_conv arities showstoppers) (conv :> nf list) in + List.map (dangerous_conv arities showstoppers) conv in prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv)); List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))) dangerous_conv; @@ -383,7 +373,7 @@ let eat p = let heads = List.sort compare (filter_map hd_of ps) in let arities = precompute_edible_data p (uniq heads) in let showstoppers, showstoppers_conv = - edible arities p.div ps p.conv showstoppers in + edible arities p.div ps (p.conv :> nf_nob list) showstoppers in let l = List.filter (fun (x,_,_) -> not (List.mem x showstoppers)) arities in let p = List.fold_left (fun p (x,pos,(xx : i_n_var)) -> if pos = -1 then p else @@ -452,7 +442,7 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) let old_conv = p.conv in let p = { p with ps; conv } in if l <> [] || old_conv <> conv - then prerr_endline (print_problem "eat" p); + then prerr_endline (string_of_problem "eat" p); if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then `Finished p else @@ -471,13 +461,15 @@ let instantiate p x perm n = let n = (prerr_endline "WARNING: using constant initialSpecialK"); p.initialSpecialK in let arities = Array.to_list (Array.make (n+1) min_int) in let p,vars = make_fresh_vars p arities in - let args = Listx.from_list (vars :> nf list) in + (* manual lifting of vars by perm in next line *) + let vars = List.map (function `Var (n,ar) -> `Var (n+perm,ar)) vars in + let args = Listx.from_list vars in let bs = ref [] in (* other_vars are the variables which are delayed and re-applied to the match *) let other_vars = Array.mapi (fun n () -> `Var(n+1,min_int)) (Array.make (perm-1) ()) in let other_vars = Array.to_list other_vars in (* 666, since it will be replaced anyway during subst: *) - let inst = `Match(`I((0,min_int),Listx.map (lift perm) args),(x,-666),perm,bs,other_vars) in + let inst = `Match(`I((0,min_int),args),(x,-666),perm,bs,other_vars) in (* Add a number of 'perm' leading lambdas *) let inst = Array.fold_left (fun t () -> `Lam(false, t)) inst (Array.make perm ()) in let p = {p with deltas=bs::p.deltas} in @@ -487,10 +479,12 @@ let instantiate p x perm n = 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 - | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms) + | `I(n, tms) -> Listx.max (Listx.map (aux 0) (tms :> nf Listx.listx)) | `Match(t, _, liftno, bs, args) -> - List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs)) + List.fold_left max 0 (List.map (aux 0) ((t :> nf)::(args :> nf list)@List.map snd !bs)) | `N _ + | `Bottom + | `Pacman | `Var _ -> 0 ) in Listx.max (Listx.map (aux 0) tms) ;; @@ -643,10 +637,12 @@ let optimize_numerals p = let replace_in_sigma perm = let rec aux = function | `N n -> `N (List.nth perm n) + | `Pacman | `I _ -> assert false | `Var _ as t -> t | `Lam(v,t) -> `Lam(v, aux t) | `Match(_,_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t + | `Bottom as t -> t in List.map (fun (n,t) -> (n,aux t)) in let deltas' = List.mapi (fun n d -> (n, List.map fst !d)) p.deltas in @@ -690,7 +686,7 @@ let main problems = if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then begin p end else - let _ = prerr_endline (print_problem "main" p) in + let _ = prerr_endline (string_of_problem "main" p) in let x,l = match l with | cmd::l -> cmd,l @@ -716,7 +712,7 @@ let main problems = let p_finale = aux p n cmds in let freshno,sigma = p_finale.freshno, p_finale.sigma in prerr_endline ("------- ------\n "); - (* prerr_endline (print_problem "Original problem" p); *) + (* prerr_endline (string_of_problem "Original problem" p); *) prerr_endline "---------------------"; let l = Array.to_list (Array.init (freshno + 1) string_of_var) in prerr_endline (" BOMB == " ^ print ~l !bomb); @@ -730,7 +726,7 @@ let main problems = (* In this non-recursive version, the intermediate states may containt Matchs *) List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps) (p.ps :> i_num_var list) sigma in - prerr_endline (print_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno}); + prerr_endline (string_of_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno}); List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ; *) prerr_endline "-------------------"; @@ -738,10 +734,10 @@ let main problems = let l = Array.to_list (Array.init (freshno + 1) string_of_var) in List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; prerr_endline "------------------"; - let div = option_map (fun div -> ToScott.t_of_nf (div :> nf)) p.div in - let conv = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.conv in - let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.ps in - let sigma = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in + let div = option_map (fun div -> ToScott.scott_of_nf (div :> nf)) p.div in + let conv = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.conv in + let ps = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.ps in + let sigma = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in (*let ps_ok = List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma in*) let e = env_of_sigma freshno sigma true in @@ -764,7 +760,7 @@ in let t = Pure.mwhd (e',div,[]) in prerr_endline ("*:: " ^ (Pure.print t)); prerr_endline (print !bomb); - assert (t = ToScott.t_of_nf (!bomb:>nf)) + assert (t = ToScott.scott_of_nf (!bomb:>nf)) | None -> ()) div; List.iter (fun n -> prerr_endline ("_::: " ^ (Pure.print n)); diff --git a/ocaml/num.ml b/ocaml/num.ml index eb37e4c..a3d9bcf 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -16,17 +16,18 @@ and i = | I of int * nf listx ;;*) type var = int * (* arity of variable*) int;; -type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ] -type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ] -type 'nf i_num_var_ = [ - | 'nf i_n_var_ - | `Match of 'nf i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list +type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ] +type 'nf_nob i_n_var_ = [ `N of int | 'nf_nob i_var_ ] +type ('nf_nob,'nf) i_num_var_ = [ + | 'nf_nob i_n_var_ + | `Match of ('nf_nob,'nf) i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf_nob list ] -type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ | 'nf i_num_var_ ] -type nf = nf nf_ -type i_var = nf i_var_;; -type i_n_var = nf i_n_var_;; -type i_num_var = nf i_num_var_;; +type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman | ('nf nf_nob_,'nf) i_num_var_ ] +type nf = [ nf nf_nob_ | `Bottom ] +type nf_nob = nf nf_nob_ +type i_var = nf_nob i_var_;; +type i_n_var = nf_nob i_n_var_;; +type i_num_var = (nf_nob,nf) i_num_var_;; let hd_of_i_var = function @@ -50,15 +51,20 @@ let lift m (t : nf) = let aux_var l (n, ar) = (if n < l then n else n+m), ar in let rec aux_i_num_var l = function - `I(v,args) -> `I(aux_var l v, Listx.map (aux l) args) + `I(v,args) -> `I(aux_var l v, Listx.map (aux_nob l) args) | `Var v -> `Var(aux_var l v) | `N _ as x -> x | `Match(t,v,lift,bs,args) -> - `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux l) args) - and aux l = + `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux_nob l) args) + and aux_nob l = function - #i_num_var as x -> (aux_i_num_var l x :> nf) + #i_num_var as x -> (aux_i_num_var l x :> nf_nob) | `Lam(b,nf) -> `Lam (b, aux (l+1) nf) + | `Pacman -> `Pacman + and aux l = + function + #nf_nob as x -> (aux_nob l x :> nf) + | `Bottom -> `Bottom in (aux 0 t : nf) ;; @@ -76,12 +82,13 @@ let free_vars' = | `Var(x,ar) -> if x < n then [] else [(x-n,ar)] | `I((x,ar),args) -> (if x < n then [] else [(x-n,ar)]) @ - List.concat (List.map (aux n) (Listx.to_list args)) + List.concat (List.map (aux n) (Listx.to_list args :> nf list)) | `Lam(_,t) -> aux (n+1) t | `Match(t,_,liftno,bs,args) -> aux n (t :> nf) @ List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @ - List.concat (List.map (aux n) args) + List.concat (List.map (aux n) (args :> nf list)) + | `Bottom | `Pacman -> [] in aux 0 ;; let free_vars = (List.map fst) ++ free_vars';; @@ -89,51 +96,53 @@ let free_vars = (List.map fst) ++ free_vars';; module ToScott = struct -let rec t_of_i_num_var = +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, t_of_nf (lift liftno t)) !bs in - let t = t_of_i_num_var t in + 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,t_of_nf t)) m args - | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args -and t_of_nf = - function - | #i_num_var as x -> t_of_i_num_var x - | `Lam(b,f) -> Pure.L (t_of_nf f) - + 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)))) end (************ Pretty-printing ************************************) -let rec string_of_term l = - let rec string_of_term_w_pars l = function +(* 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) -> print_name l n ^ ":" ^ string_of_int ar | `N n -> string_of_int n - | `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")" + | `I _ as t -> "(" ^ string_of_term_no_pars_app l t ^ ")" | `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)) + " 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 -> "TNT" + | `Pacman -> "PAC" + 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 :> 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) | _ as t -> string_of_term_no_pars l t - and string_of_term_no_pars l : nf -> string = function + and string_of_term_no_pars l = function | `Lam _ as t -> string_of_term_no_pars_lam l t | #nf as t -> string_of_term_no_pars_app l t in string_of_term_no_pars l ;; let print ?(l=[]) = string_of_term l;; -let string_of_nf t = string_of_term [] (t:>nf);; +let string_of_nf t = string_of_term [] (t :> nf);; (************ Hereditary substitutions ************************************) @@ -160,7 +169,7 @@ let cast_to_i_num_var = let rec set_arity arity = function | `Var(n,_) -> `Var(n,arity) -| `N _ as t -> t +| `N _ | `Bottom | `Pacman as t -> t | `Lam(false, t) -> `Lam(false, set_arity arity t) | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args) | `I _ | `Lam _ -> assert false @@ -168,13 +177,16 @@ let rec set_arity arity = function let minus1 n = if n = min_int then n else n - 1;; let rec mk_app (h : nf) (arg : nf) = -(*let res =*) - match h with - `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args) - | `Var v -> `I(v, Listx.Nil arg) - | `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 *) + match arg with + | `Bottom -> `Bottom + | #nf_nob as arg -> + match h with + | `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args) + | `Var v -> `I(v, Listx.Nil arg) + | `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]) + | `Bottom | `Pacman as t -> t + | `N _ -> assert false (* Numbers cannot be applied *) (*in let l = ["v0";"v1";"v2"] in prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*) @@ -186,18 +198,20 @@ and mk_appx h args = Listx.fold_left mk_app h args and mk_match t (n,ar) bs_lift bs args = (*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*) - match t with + let m = + match t with `N m -> (try let h = List.assoc m !bs in let h = set_arity (minus1 ar) h in let h = lift bs_lift h in - mk_appl h args + h with Not_found -> - `Match (t,(n,ar),bs_lift,bs,args)) - | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args) + `Match (t,(n,ar),bs_lift,bs,[])) + | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,[]) in + mk_appl m args -and subst truelam delift_by_one what (with_what : nf) (where : nf) = +and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) = let rec aux_propagate_arity ar = function | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t) | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one -> @@ -208,28 +222,31 @@ and subst truelam delift_by_one what (with_what : nf) (where : nf) = function `I((n,ar),args) -> if n = what + l then - mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args) + let args = Listx.map (aux l) (args :> nf Listx.listx) in + mk_appx (lift l (aux_propagate_arity ar (with_what :> nf))) args else - `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args) + mk_appl (`Var ((if delift_by_one && n >= l then n-1 else n), ar)) (List.map (aux l) (Listx.to_list (args :> nf Listx.listx))) | `Var(n,ar) -> if n = what + l then - lift l (aux_propagate_arity ar with_what) + lift l (aux_propagate_arity ar (with_what :> nf)) else `Var((if delift_by_one && n >= l then n-1 else n), ar) | `N _ as x -> x | `Match(t,v,bs_lift,bs,args) -> let bs_lift = bs_lift + if delift_by_one then -1 else 0 in let l' = l - bs_lift in - let with_what' = lift l' with_what in + let with_what' = lift l' (with_what :> nf) 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 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) + mk_match (cast_to_i_num_var (aux_i_num_var l t)) v bs_lift bs (List.map (aux l) (args :> nf list)) and aux l(*lift*) = (*function iii -> let res = match iii with*) function | #i_num_var as x -> aux_i_num_var l x | `Lam(b, nf) -> `Lam(b, aux (l+1) nf) + | `Bottom -> `Bottom + | `Pacman -> `Pacman (*in let ll = ["v0";"v1";"v2"] in prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*) in @@ -265,9 +282,13 @@ let eta_compare x y = let rec aux t1 t2 = match t1, t2 with | `Var(n,_) , `Var(m,_) -> compare n m | `I((n1,_), l1), `I((n2,_), l2) -> - clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2) + clex compare (lex aux) (n1, (Listx.to_list l1 :> nf list)) (n2, (Listx.to_list l2 :> nf list)) + | `Bottom, `Bottom + | `Pacman, `Pacman -> 0 | `Lam _, `N _ -> -1 | `N _, `Lam _ -> 1 + | `Bottom, `Lam _ + | `Lam _, `Bottom -> assert false (* TO BE UNDERSTOOD *) | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2 | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666))) | t2, `Lam(_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var(0,-666))) @@ -275,13 +296,17 @@ let eta_compare x y = | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') -> let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in - clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args')) + clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, (args :> nf list))) ((u' :> nf), (bs', (args' :> nf list))) | `Match _, _ -> -1 | _, `Match _ -> 1 | `N _, _ -> -1 | _, `N _ -> 1 | `I _, _ -> -1 | _, `I _ -> 1 + | `Bottom, _ -> -1 + | _, `Bottom -> 1 + | `Pacman, _ -> -1 + | _, `Pacman -> 1 in aux x y ;; @@ -291,15 +316,17 @@ let rec eta_subterm sub t = if eta_eq sub t then true else match t with | `Lam(_,t') -> eta_subterm (lift 1 sub) t' + | `Bottom + | `Pacman -> false | `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 + || 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')) + && 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 ) | `N _ | `Var _ -> false @@ -307,7 +334,6 @@ let rec eta_subterm sub t = let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;; - let max_arity_tms n = let max a b = match a, b with | None, None -> None @@ -317,37 +343,11 @@ let max_arity_tms n = let aux_var l (m,a) = if n + l = m then Some a else None in let rec aux l = function | `Var v -> aux_var l v - | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms)) + | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms :> nf list)) | `Lam(_,t) -> aux (l+1) t - | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs)) - | `N _ -> None + | `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 fun tms -> aux_tms 0 (tms :> nf list) ;; - -let get_first_args var = -let rec aux l = function -| `Lam(_,t) -> aux (l+1) t -| `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args -| `I((n,_), args) -> if n = var + l then [Listx.last args] else [] -| `N _ -| `Var _ -> [] -in aux 0 -;; - -let compute_arities m = - let rec aux n tms = - if n = 0 - then [] - else - let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in - let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in - arity :: (aux (n-1) tms) - in fun tms -> List.rev (aux m tms) -;; - -let compute_arities var special_k all_tms = - let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in - compute_arities special_k tms -;; diff --git a/ocaml/num.mli b/ocaml/num.mli index 9cf81cc..bf9cae5 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -1,21 +1,16 @@ -type var = int * int -type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ] -type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ] -type 'nf i_num_var_ = - [ `I of var * 'nf Listx.listx - | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list - | `N of int - | `Var of var ] -type 'nf nf_ = - [ `I of var * 'nf Listx.listx - | `Lam of bool * 'nf nf_ - | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list - | `N of int - | `Var of var ] -type nf = nf nf_ -type i_var = nf i_var_ -type i_n_var = nf i_n_var_ -type i_num_var = nf i_num_var_ +type var = int * (* arity of variable*) int;; +type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ] +type 'nf_nob i_n_var_ = [ `N of int | 'nf_nob i_var_ ] +type ('nf_nob,'nf) i_num_var_ = [ + | 'nf_nob i_n_var_ + | `Match of ('nf_nob,'nf) i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf_nob list +] +type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman | ('nf nf_nob_,'nf) i_num_var_ ] +type nf = [ nf nf_nob_ | `Bottom ] +type nf_nob = nf nf_nob_ +type i_var = nf_nob i_var_;; +type i_n_var = nf_nob i_n_var_;; +type i_num_var = (nf_nob,nf) i_num_var_;; val hd_of_i_var : i_var -> int val hd_of : i_n_var -> int option val arity_of_hd : i_n_var -> int @@ -26,8 +21,7 @@ val free_vars' : nf -> var list val free_vars : nf -> int list module ToScott : sig - val t_of_i_num_var : nf i_num_var_ -> Pure.Pure.t - val t_of_nf : nf -> Pure.Pure.t + val scott_of_nf : nf -> Pure.Pure.t end val print : ?l:string list -> nf -> string val string_of_nf : [ string @@ -38,12 +32,11 @@ val set_arity : int -> nf -> nf val mk_app : nf -> nf -> nf val mk_appl : nf -> nf list -> nf val mk_appx : nf -> nf Listx.listx -> nf -val mk_match : nf i_num_var_ -> var -> int -> (int * nf) list ref -> nf list -> nf +val mk_match : i_num_var -> var -> int -> (int * nf) list ref -> nf list -> nf val subst : bool -> bool -> int -> nf -> nf -> nf val parse' : string list -> nf list * string list val eta_compare : nf -> nf -> int val eta_eq : [< nf ] -> [< nf ] -> bool val eta_subterm : [< nf ] -> [< nf ] -> bool val max_arity_tms : int -> [< nf] list -> int option -val compute_arities : int -> int -> nf list -> int list val minus1 : int -> int diff --git a/ocaml/numx.ml b/ocaml/numx.ml deleted file mode 100644 index b958ed5..0000000 --- a/ocaml/numx.ml +++ /dev/null @@ -1,294 +0,0 @@ -open Util -open Util.Vars -open Pure - -(************ Syntax ************************************) - -(* Normal forms*) - -(* Var n = n-th De Bruijn index, 0-based *) - -(*type nf = - | Lam of nf - | Var of int - | i -and i = - | I of int * nf listx -;;*) -type 'nf i_var_ = [ `I of int * 'nf Listx.listx | `Var of int ] -type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ] -type 'nf i_num_var_ = [ - | 'nf i_n_var_ - | `Match of 'nf i_num_var_ * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list -] -type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ | `Bomb | `Pacman | 'nf i_num_var_ ] -type nf = nf nf_ -type i_var = nf i_var_;; -type i_n_var = nf i_n_var_;; -type i_num_var = nf i_num_var_;; - -let hd_of_i_var = - function - `I (v,_) - | `Var v -> v - -let hd_of = - function - `I (v,_) - | `Var v -> Some v - | `N _ -> None - | `Match _ | `Bomb -> assert false - -let lift m (t : nf) = - let rec aux_i_num_var l = - function - `I(n,args) -> (`I((if n < l then n else n+m),Listx.map (aux l) args) : i_num_var) - | `Var n -> `Var (if n < l then n else n+m) - | `N _ as x -> x - | `Match(t,lift,bs,args) -> - `Match(aux_i_num_var l t, lift + m, bs, List.map (aux l) args) - and aux l = - function - #i_num_var as x -> (aux_i_num_var l x :> nf) - | `Lam(b,nf) -> `Lam (b,aux (l+1) nf) - | `Bomb -> `Bomb - | `Pacman -> `Pacman - in - (aux 0 t : nf) -;; - -(* put t under n lambdas, lifting t accordingtly *) -let rec make_lams t = - function - 0 -> t - | n when n > 0 -> `Lam (false,lift 1 (make_lams t (n-1))) - | _ -> assert false - -let free_vars = - let rec aux n = function - `N _ -> [] - | `Var x -> if x < n then [] else [x-n] - | `I(x,args) -> - (if x < n then [] else [x-n]) @ - List.concat (List.map (aux n) (Listx.to_list args)) - | `Lam(_,t) -> aux (n+1) t - | `Match(t,liftno,bs,args) -> - aux n (t :> nf) @ - List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @ - List.concat (List.map (aux n) args) - | `Bomb | `Pacman -> [] - in aux 0 -;; - -module ToScott = -struct - -let rec t_of_i_num_var = - 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, t_of_nf (lift liftno t)) !bs in - let t = t_of_i_num_var t in - let m = Scott.mk_match t bs in - List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args - | `I(v, args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args -and t_of_nf = - function - | #i_num_var as x -> t_of_i_num_var x - | `Lam(b,f) -> Pure.L (t_of_nf f) - | `Bomb -> 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)))) - -end - - -(************ Pretty-printing ************************************) - -(* let rec print ?(l=[]) = - function - `Var n -> print_name l n - | `N n -> string_of_int n - | `Match(t,bs_lift,bs,args) -> - "([" ^ print ~l (t :> nf) ^ - " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (lift bs_lift t)) !bs) ^ "] " ^ - String.concat " " (List.map (print ~l) args) ^ ")" - | `I(n,args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")" - | `Lam(_,nf) -> - let name = string_of_var (List.length l) in - "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf) -;; *) - -let rec string_of_term l = - let rec string_of_term_w_pars l = function - | `Var n -> print_name l n - | `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,bs_lift,bs,args) -> - "(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)) !bs) ^ "] " ^ - String.concat " " (List.map (string_of_term l) args) ^ ")" - | `Bomb -> "TNT" - | `Pacman -> "PAC" - and string_of_term_no_pars_app l = function - | `I(n, args) -> print_name l n ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args)) - | #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) - | _ 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 - | #nf as t -> string_of_term_no_pars_app l t - in string_of_term_no_pars l -;; - -let rec print ?(l=[]) = string_of_term l;; - -(************ Hereditary substitutions ************************************) - -let cast_to_i_var = - function - #i_var as y -> (y : i_var) - | t -> - prerr_endline (print (t :> nf)); - assert false (* algorithm failed *) - -let cast_to_i_n_var = - function - #i_n_var as y -> (y : i_n_var) - | t -> - prerr_endline (print (t :> nf)); - assert false (* algorithm failed *) - -let cast_to_i_num_var = - function - #i_num_var as y -> (y : i_num_var) - | t -> - prerr_endline (print (t :> nf)); - assert false (* algorithm failed *) - -let rec mk_app (h : nf) (arg : nf) = -(*let res =*) - match h with - `I(n,args) -> `I(n,Listx.append (Listx.Nil arg) args) - | `Var n -> `I(n, Listx.Nil arg) - | `Lam(_,nf) -> subst true 0 arg (nf : nf) - | `Match(t,lift,bs,args) -> `Match(t,lift,bs,List.append args [arg]) - | `N _ -> assert false (* Numbers cannot be applied *) - | `Bomb | `Pacman -> failwith "mk_app su bomba o pacman" -(*in let l = ["v0";"v1";"v2"] in -prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*) - -and mk_appl h args = - (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*) - List.fold_left mk_app h args - -and mk_appx h args = Listx.fold_left mk_app h args - -and mk_match t bs_lift bs args = - (*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*) - match t with - `N m -> - (try - let h = List.assoc m !bs in - let h = lift bs_lift h in - mk_appl h args - with Not_found -> - `Match (t,bs_lift,bs,args)) - | `I _ | `Var _ | `Match _ -> `Match(t,bs_lift,bs,args) - -and subst delift_by_one what (with_what : nf) (where : nf) = - let rec aux_i_num_var l = - function - `I(n,args) -> - if n = what + l then - mk_appx (lift l with_what) (Listx.map (aux l) args) - else - `I ((if delift_by_one && n >= l then n-1 else n), Listx.map (aux l) args) - | `Var n -> - if n = what + l then - lift l with_what - else - `Var (if delift_by_one && n >= l then n-1 else n) - | `N _ as x -> x - | `Match(t,bs_lift,bs,args) -> - let bs_lift = bs_lift + if delift_by_one then -1 else 0 in - let l' = l - bs_lift in - 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 ; - mk_match (cast_to_i_num_var (aux_i_num_var l t)) bs_lift bs (List.map (aux l) args) - and aux l(*lift*) = -(*function iii -> let res = match iii with*) - function - | #i_num_var as x -> aux_i_num_var l x - | `Lam(b,nf) -> `Lam(b,aux (l+1) nf) - | `Bomb -> `Bomb - | `Pacman -> `Pacman -(*in let ll = ["v0";"v1";"v2"] in -prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*) - in - aux 0 where -;; - -(************ Parsing ************************************) - -let parse' strs = - let rec aux = function - | Parser.Lam t -> `Lam (true,aux t) - | Parser.App (t1, t2) -> mk_app (aux t1) (aux t2) - | Parser.Var v -> `Var v - in let (tms, free) = Parser.parse_many strs - in (List.map aux tms, free) -;; - -(************** Algorithm(s) ************************) - -let eta_eq x y = - let rec aux = function - | `Var n , `Var m -> n = m - | `I(n1, l1), `I(n2, l2) -> - n1 = n2 && Listx.length l1 = Listx.length l2 && - List.for_all aux (List.combine (Listx.to_list l1) (Listx.to_list l2)) - | `Lam(_,t1), `Lam(_,t2) -> aux (t1,t2) - | `Lam(_,t1), t2 - | t2, `Lam(_,t1) -> aux( t1, (mk_app (lift 1 t2) (`Var 0)) ) - | `N n1, `N n2 -> n1 = n2 - | `Match(u,bs_lift,bs,args), `Match(u',bs_lift',bs',args') -> - aux ((u :> nf), (u' :> nf)) && List.length !bs = List.length !bs' && - let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in - let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in - List.for_all (fun ((n,t),(n',t')) -> n = n' && aux (t, t')) (List.combine bs bs') && List.length args = List.length args' && - List.for_all aux (List.combine args args') - | _ -> false - in aux (x, y) -;; - -let eta_compare x y = - if eta_eq x y then 0 else compare x y -;; - -let eta_eq (#nf as x) (#nf as y) = eta_eq x y;; - -let rec eta_subterm sub t = - if eta_eq sub t then true else - match t with - | `Lam(_,t') -> eta_subterm (lift 1 sub) t' - | `Match(u,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' - && 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 - ) - | `N _ | `Var _ | `Bomb | `Pacman -> false -;; - -let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;; diff --git a/ocaml/numx.mli b/ocaml/numx.mli deleted file mode 100644 index 206c32f..0000000 --- a/ocaml/numx.mli +++ /dev/null @@ -1,44 +0,0 @@ -type 'nf i_var_ = [ `I of int * 'nf Listx.listx | `Var of int ] -type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ] -type 'nf i_num_var_ = - [ `I of int * 'nf Listx.listx - | `Match of 'nf i_num_var_ * int * (int * 'nf) list ref * 'nf list - | `N of int - | `Var of int ] -type 'nf nf_ = - [ `I of int * 'nf Listx.listx - | `Lam of bool * 'nf nf_ - | `Match of 'nf i_num_var_ * int * (int * 'nf) list ref * 'nf list - | `N of int - | `Var of int - | `Bomb - | `Pacman ] -type nf = nf nf_ -type i_var = nf i_var_ -type i_n_var = nf i_n_var_ -type i_num_var = nf i_num_var_ -val hd_of_i_var : i_var -> int -val hd_of : - [< `I of 'a * 'b | `Match of 'c | `N of 'd | `Var of 'a ] -> 'a option -(* put t under n lambdas, lifting t accordingtly *) -val make_lams : nf -> int -> nf -val lift : int -> nf -> nf -val free_vars : nf -> int list -module ToScott : - sig - val t_of_i_num_var : nf i_num_var_ -> Pure.Pure.t - val t_of_nf : nf -> Pure.Pure.t - end -val print : ?l:string list -> nf -> string -val cast_to_i_var : [< nf > `I `Var] -> i_var -val cast_to_i_n_var : [< nf > `I `N `Var] -> i_n_var -val cast_to_i_num_var : [< nf > `I `N `Match `Var] -> i_num_var -val mk_app : nf -> nf -> nf -val mk_appl : nf -> nf list -> nf -val mk_appx : nf -> nf Listx.listx -> nf -val mk_match : nf i_num_var_ -> int -> (int * nf) list ref -> nf list -> nf -val subst : bool -> int -> nf -> nf -> nf -val parse' : string list -> nf list * string list -val eta_compare : nf -> nf -> int -val eta_eq : [< nf ] -> [< nf ] -> bool -val eta_subterm : [< nf ] -> [< nf ] -> bool -- 2.39.2