From f804e82c47ca8a25f3044ae630988af4b8da7b25 Mon Sep 17 00:00:00 2001 From: Date: Thu, 22 Jun 2017 17:20:55 +0200 Subject: [PATCH] Removed lambda3 + Fixed lambda4 --- ocaml/Makefile | 15 +- ocaml/lambda3.ml | 550 -------------------------------------------- ocaml/lambda3.ml.ar | 550 -------------------------------------------- ocaml/lambda3.mli | 1 - ocaml/lambda4.ml | 98 ++------ ocaml/problems.ml | 3 +- ocaml/test.ml | 16 +- 7 files changed, 41 insertions(+), 1192 deletions(-) delete mode 100644 ocaml/lambda3.ml delete mode 100644 ocaml/lambda3.ml.ar delete mode 100644 ocaml/lambda3.mli diff --git a/ocaml/Makefile b/ocaml/Makefile index 6ff0e02..b4b12e0 100644 --- a/ocaml/Makefile +++ b/ocaml/Makefile @@ -2,16 +2,17 @@ OCAMLC = ocamlopt -g -rectypes LIB = unix.cmxa str.cmxa UTILS = parser.cmx console.cmx listx.cmx util.cmx pure.cmx num.cmx -all: a.out test.out test34.out +all: a.out test4.out + # test.out -a.out: $(UTILS) lambda3.cmx lambda4.cmx problems.cmx +a.out: $(UTILS) lambda4.cmx problems.cmx $(OCAMLC) -o a.out $(LIB) $^ -test.out: $(UTILS) lambda3.cmx test1.ml - $(OCAMLC) -o test.out $(LIB) $^ - -test34.out: $(UTILS) lambda3.cmx lambda4.cmx test.ml - $(OCAMLC) -o test34.out $(LIB) $^ +# test.out: $(UTILS) lambda3.cmx test1.ml +# $(OCAMLC) -o test.out $(LIB) $^ +# +test4.out: $(UTILS) lambda4.cmx test.ml + $(OCAMLC) -o test4.out $(LIB) $^ %.cmi: %.mli $(OCAMLC) -c $< diff --git a/ocaml/lambda3.ml b/ocaml/lambda3.ml deleted file mode 100644 index f61e1e5..0000000 --- a/ocaml/lambda3.ml +++ /dev/null @@ -1,550 +0,0 @@ -open Util -open Util.Vars -open Pure -open Num - -type problem = - { freshno: int - ; ps: i_n_var list (* the n-th inert must become n *) - ; sigma: (int * nf) list (* the computed substitution *) - ; deltas: (int * nf) list ref list (* collection of all branches *) - } - -let print_problem {freshno; ps; deltas} = - let deltas = String.concat "\n" (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 - deltas ^ (if deltas = "" then "" else "\n") ^ - String.concat "\n" (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps) -;; - -let make_fresh_var freshno = - freshno+1, freshno+1 - -let make_fresh_vars p m = - let rec aux = - function - 0 -> p.freshno,[] - | n when n > 0 -> - let freshno,vars = aux (n-1) in - let freshno,v = make_fresh_var freshno in - freshno,`Var v::vars - | _ -> assert false in - let freshno,vars = aux m in - {p with freshno}, vars - -let simple_expand_match ps = - let rec aux level = function - | #i_num_var as t -> aux_i_num_var level t - | `Lam(b,t) -> `Lam(b, aux (level+1) t) - and aux_i_num_var level = function - | `Match(u,bs_lift,bs,args) as torig -> - let u = aux_i_num_var level u in - bs := List.map (fun (n, x) -> n, aux 0 x) !bs; - (try - (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) bs_lift bs args 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,bs_lift,bs,List.map (aux level) args)) - | `I(k,args) -> `I(k,Listx.map (aux level) args) - | `N _ | `Var _ as t -> t -in aux_i_num_var 0;; - -let rec super_simplify_ps ps it = - let it' = List.map (fun t -> cast_to_i_num_var (simple_expand_match ps t)) (it :> i_num_var list) in - if it <> it' then super_simplify_ps ps it' else it' - -let super_simplify ({ps} as p) = - let ps = super_simplify_ps p.ps (p.ps :> i_num_var list) in - {p with ps=List.map cast_to_i_n_var ps} - -let subst_in_problem x inst ({freshno; ps; sigma} as p) = - let len_ps = List.length ps in -(*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in -prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) - let rec aux ((freshno,acc_ps,acc_new_ps) as acc) = - function - [] -> acc - | t::todo_ps -> -(*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) - let t = subst false x inst (t :> nf) in -(*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) - let freshno,new_t,acc_new_ps = - expand_match (freshno,acc_ps@`Var(max_int/3)::todo_ps,acc_new_ps) t - in - aux (freshno,acc_ps@[new_t],acc_new_ps) todo_ps - - and expand_match ((freshno,acc_ps, acc_new_ps) as acc) t = - match t with - | `Match(u',bs_lift,bs,args) -> - let freshno,u,acc_new_ps = expand_match acc (u' :> nf) in - let acc_new_ps,i = - match u with - `N i -> acc_new_ps,i - | _ -> - let ps = List.map (fun t -> cast_to_i_num_var (subst false x inst (t:> nf))) (acc_ps@acc_new_ps) in - let super_simplified_ps = super_simplify_ps ps ps in -(*prerr_endline ("CERCO u:" ^ print (fst u :> nf)); -List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps; -List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplified_ps;*) - match index_of_opt ~eq:eta_eq super_simplified_ps u with - Some i -> acc_new_ps, i - | None -> acc_new_ps@[u], len_ps + List.length acc_new_ps - in - let freshno= - if List.exists (fun (j,_) -> i=j) !bs then - freshno - else - let freshno,v = make_fresh_var freshno in - bs := !bs @ [i, `Var 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) bs_lift bs args 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 _ -> - (* the cast will fail *) - (* freshno,(cast_to_i_n_var t),acc_new_ps *) - assert false - | #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 - let freshno,old_ps,new_ps = aux (freshno,[],[]) (ps :> i_num_var list) in - let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in -(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in -prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst)); - let p = {p with freshno; ps; sigma = sigma@[x,inst]} in - let p = super_simplify p in -prerr_endline (print_problem p); p - -exception Dangerous - -let rec dangerous arities showstoppers = - function - `N _ - | `Var _ - | `Lam _ -> () - | `Match(t,liftno,bs,args) -> - (* CSC: XXX partial dependency on the encoding *) - (match t with - `N _ -> List.iter (dangerous arities showstoppers) args - | `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args - | `Var x -> dangerous_inert arities showstoppers x args 2 (* 2 coming from Scott's encoding *) - | `I(x,args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *) - ) - | `I(k,args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0 - -and dangerous_inert arities showstoppers k args more_args = - List.iter (dangerous arities showstoppers) args ; - if List.mem k showstoppers then raise Dangerous else - try - let _,_,y = List.find (fun (v,_,_) -> v=k) arities in - let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | _ -> assert false in - if List.length args + more_args > arity then raise Dangerous else () - with - Not_found -> () - -(* inefficient algorithm *) -let edible arities showstoppers ps = - let rec aux showstoppers = - function - [] -> showstoppers - | x::xs when List.exists (fun y -> hd_of x = Some y) showstoppers -> - (* se la testa di x e' uno show-stopper *) - let new_showstoppers = sort_uniq (showstoppers @ free_vars (x :> nf)) in - (* aggiungi tutte le variabili libere di x *) - if List.length showstoppers <> List.length new_showstoppers then - aux new_showstoppers ps - else - aux showstoppers xs - | x::xs -> - match hd_of x with - None -> aux showstoppers xs - | Some h -> - try - dangerous arities showstoppers (x : i_n_var :> nf) ; - aux showstoppers xs - with - Dangerous -> - aux (sort_uniq (h::showstoppers)) ps - in - aux showstoppers ps - -let precompute_edible_data {ps} xs = - List.map (fun x -> - let y = List.find (fun y -> hd_of y = Some x) ps in - x, index_of ~eq:eta_eq y ps, y) xs -;; - -let critical_showstoppers p = - let p = super_simplify p in - let showstoppers_step = - List.concat (List.map (fun bs -> - let heads = List.map (fun (i,_) -> List.nth p.ps i) !bs in - let heads = List.sort compare (filter_map hd_of heads) in - snd (split_duplicates heads) - ) p.deltas) in - let showstoppers_step = sort_uniq showstoppers_step in - let showstoppers_eat = - let heads_and_arities = - List.sort (fun (k,_) (h,_) -> compare k h) - (filter_map (function `Var k -> Some (k,0) | `I(k,args) -> Some (k,Listx.length args) | _ -> None ) p.ps) in - let rec multiple_arities = - function - [] - | [_] -> [] - | (x,i)::(y,j)::tl when x = y && i <> j -> - x::multiple_arities tl - | _::tl -> multiple_arities tl in - multiple_arities heads_and_arities in - - let showstoppers_eat = sort_uniq showstoppers_eat in - let showstoppers_eat = List.filter - (fun x -> not (List.mem x showstoppers_step)) - showstoppers_eat in - List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ string_of_var v)) showstoppers_step; - List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ string_of_var v)) showstoppers_eat; - p, showstoppers_step, showstoppers_eat - ;; - -let eat p = - let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in - let showstoppers = showstoppers_step @ showstoppers_eat in - let heads = List.sort compare (filter_map hd_of ps) in - let arities = precompute_edible_data p (uniq heads) in - let showstoppers = edible arities showstoppers ps 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)) -> - let n = match xx with `I(_,args) -> Listx.length args | _ -> 0 in - let v = `N(pos) in - let inst = make_lams v n in -(let l = Array.to_list (Array.init (p.freshno + 1) string_of_var) in - prerr_endline ("# INST_IN_EAT: " ^ string_of_var x ^ " := " ^ print ~l inst)); - (* CSC: XXX to avoid applied numbers in safe positions that - trigger assert failures subst_in_problem x inst p*) - { p with sigma = p.sigma @ [x,inst] } - ) p l in - let ps = - List.map (fun t -> - try - let _,j,_ = List.find (fun (h,_,_) -> hd_of t = Some h) l in - `N j - with Not_found -> t - ) ps in - List.iter - (fun bs -> - bs := - List.map - (fun (n,t as res) -> - match List.nth ps n with - `N m -> m,t - | _ -> res - ) !bs - ) p.deltas ; - let p = { p with ps } in - if l <> [] then prerr_endline (print_problem p); - if List.for_all (function `N _ -> true | _ -> false) ps then - `Finished p - else - `Continue p - -let instantiate p x n = - let p,vars = make_fresh_vars p n in - let freshno,zero = make_fresh_var p.freshno in - let p = {p with freshno} in - let zero = Listx.Nil (`Var zero) in - let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in - let bs = ref [] in - let inst = `Lam(false,`Match(`I(0,Listx.map (lift 1) args),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 - | `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)) - | `N _ -> 0 - | `Var _ -> 0 - ) in Listx.max (Listx.map (aux 0) tms) -;; - -let auto_instantiate (n,p) = - let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in - let x = - match showstoppers_step, showstoppers_eat with - | [], y::_ -> - prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y - | [], [] -> - let heads = List.sort compare (filter_map (fun t -> match t with `Var _ -> None | x -> hd_of x) ps) in - (match heads with - [] -> assert false - | x::_ -> - prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x); - x) - | x::_, _ -> - prerr_endline ("INSTANTIATING " ^ string_of_var x); - x in -(* Strategy that decreases the special_k to 0 first (round robin) -1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *) -let x = - try - (match hd_of (List.find (fun t -> compute_special_k (Listx.Nil (t :> nf)) > 0) ps) with - None -> assert false - | Some x -> - prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x); - x) - with - Not_found -> x -in -(* Instantiate in decreasing order of compute_special_k -1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s -let x = - try - (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) ps)))) with - None -> assert false - | Some x -> - prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x); - x) - with - Not_found -> x -in*) - let special_k = - compute_special_k (Listx.from_list (p.ps :> nf list) )in - if special_k < n then - prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@"); - let p = instantiate p x special_k in - special_k,p - -let problem_measure {ps} = - (* let rec term_size_i_n_var = - function - | `I(v,nfs) -> - (Listx.length nfs) * - (List.fold_right (fun (a,b) c -> 10 + ((a+1) * term_size b) + c) (List.mapi (fun x y -> (x,y)) (Listx.to_list nfs)) 0) - | `Var _ -> 1 - | `N _ -> 0 - and term_size = - function - | #i_n_var as t -> term_size_i_n_var t - | `Match(t,lift,bs,args) -> 1 + (term_size (t :> nf)) + 1 + (List.fold_right ((+) ++ term_size) args 0) - | `Lam(b,t) -> (if b then 0 else 1) + term_size t - (* in List.fold_right ((+) ++ term_size_i_n_var) ps 0;; *) - in ... *) - 0 - -let rec auto_eat (n,({ps} as p)) = - match eat p with - `Finished p -> p - | `Continue p -> - let p' = auto_instantiate (n,p) in - let m' = problem_measure (snd p') in - let delta = m' - problem_measure p in - (if delta >= 0 - then print_endline ("$$$$ MEASURE DID NOT DECREASE (after inst) delta=" ^ string_of_int delta)); - let p'' = auto_eat p' in - (if m' <= problem_measure p'' - then print_endline ("$$$$ MEASURE DID NOT DECREASE (after eat) $$$")); - p'' -;; - -let auto p n = - prerr_endline ("@@@@ FIRST INSTANTIATE PHASE (" ^ string_of_int n ^ ") @@@@"); - auto_eat (n,p) -;; - -(* -0 = snd - - x y = y 0 a y = k k z = z 0 c y = k y u = u h1 h2 0 h2 a = h3 -1 x a c 1 a 0 c 1 k c 1 c 0 1 k 1 k 1 k -2 x a y 2 a 0 y 2 k y 2 y 0 2 y 0 2 h2 0 2 h3 -3 x b y 3 b 0 y 3 b 0 y 3 b 0 y 3 b 0 y 3 b 0 (\u. u h1 h2 0) 3 b 0 (\u. u h1 (\w.h3) 0) -4 x b c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c -5 x (b e) 5 b e 0 5 b e 0 5 b e 0 5 b e 0 5 b e 0 5 b e 0 -6 y y 6 y y 6 y y 6 y y 6 y y 6 h1 h1 h2 0 h2 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0 - - l2 _ = l3 -b u = u l1 l2 0 e _ _ _ _ = f l3 n = n j 0 -1 k 1 k 1 k -2 h3 2 h3 2 h3 -3 l2 0 (\u. u h1 (\w. h3) 0) 3 l3 (\u. u h1 (\w. h3) 0) 3 j h1 (\w. h3) 0 0 -4 l2 0 c 4 l3 c 4 c j 0 -5 e l1 l2 0 0 5 f 5 f -6 h1 h1 (\w. h3) 0 (\w. h3) 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0 -*) - -(* - x n = n 0 ? -x a (b (a c)) a 0 = 1 ? (b (a c)) 8 -x a (b d') a 0 = 1 ? (b d') 7 -x b (a c) b 0 = 1 ? (a c) 4 -x b (a c') b 0 = 1 ? (a c') 5 - -c = 2 -c' = 3 -a 2 = 4 (* a c *) -a 3 = 5 (* a c' *) -d' = 6 -b 6 = 7 (* b d' *) -b 4 = 8 (* b (a c) *) -b 0 = 1 -a 0 = 1 -*) - -(************** Tests ************************) - -let optimize_numerals p = - let replace_in_sigma perm = - let rec aux = function - | `N n -> `N (List.nth perm n) - | `I _ | `Var _ -> assert false - | `Lam(v,t) -> `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 - let deltas' = List.mapi (fun n d -> (n, List.map fst !d)) p.deltas in - let maxs = Array.to_list (Array.init (List.length deltas') (fun _ -> 0)) in - let max = Listx.max (Listx.from_list ( - List.concat (List.map snd deltas') - )) in - let perm,_ = List.fold_left (fun (perm, maxs) (curr_n:int) -> - let containing = filter_map (fun (i, bs) -> if List.mem curr_n bs then Some i else None) deltas' in - (* (prerr_endline (string_of_int curr_n ^ " occurs in: " ^ (String.concat " " (List.map string_of_int containing)))); *) - let neww = Listx.max (Listx.from_list (List.mapi (fun n max -> if List.mem n containing then max else 0) maxs)) in - let maxs = List.mapi (fun i m -> if List.mem i containing then neww+1 else m) maxs in - (neww::perm, maxs) - ) ([],maxs) (Array.to_list (Array.init (max+1) (fun x -> x))) in - replace_in_sigma (List.rev perm) p.sigma -;; - -prerr_endline "########## main ##########";; - -(* Commands: - v ==> v := \a. a k1 .. kn \^m.0 - + ==> v := \^k. numero for every v such that ... - * ==> tries v as long as possible and then +v as long as possible -*) -let main problems = - let rec aux ({ps} as p) n l = - if List.for_all (function `N _ -> true | _ -> false) ps then begin - assert (l = []); - p - end else - let _ = prerr_endline (print_problem p) in - let x,l = - match l with - | cmd::l -> cmd,l - | [] -> read_line (),[] in - let cmd = - if x = "+" then - `DoneWith - else if x = "*" then - `Auto - else - `Step x in - match cmd with - | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *) - | `Step x -> - let x = var_of_string x in - aux (instantiate p x n) n l - | `Auto -> aux (auto p n) n l - in - List.iter - (fun (p,n,cmds) -> - let p_finale = aux p n cmds in - let freshno,sigma = p_finale.freshno, p_finale.sigma in - prerr_endline "------- ------"; - prerr_endline (print_problem p); - prerr_endline "---------------------"; - 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 ps = - List.fold_left (fun ps (x,inst) -> - (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *) - (* 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}); - List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ; -*) - prerr_endline "-------------------"; - let sigma = optimize_numerals p_finale in (* optimize numerals *) - 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 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 ps_ok = List.fold_left (fun ps (x,inst) -> - List.map (Pure.subst false x inst) ps) ps sigma in*) - let e = - let rec aux n = - if n > freshno then - [] - else - let e = aux (n+1) in - (try - e,Pure.lift (-n-1) (let t = (snd (List.find (fun (i,_) -> i = n) sigma)) in prerr_endline (string_of_var n ^ " := " ^ Pure.print t); t),[] - with - Not_found -> [],Pure.V n,[])::e - in - aux 0 in -(* - prerr_endline "------------------"; -let rec print_e e = - "[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]" -in - prerr_endline (print_e e); - List.iter (fun (t,t_ok) -> - prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok); - (*assert (Pure.unwind (e,t,[]) = t_ok)*) - ) (List.combine ps ps_ok); -*) - prerr_endline "-----------------"; - List.iteri (fun i n -> - (*prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n));*) - let t = Pure.mwhd (e,n,[]) in - prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t)); - assert (t = Scott.mk_n i) - ) ps ; - prerr_endline "-------- --------" - ) problems - -(********************** problems *******************) - -let zero = `Var 0;; - -let append_zero = - function - | `I _ - | `Var _ as i -> cast_to_i_n_var (mk_app i zero) - | _ -> assert false -;; - -type t = problem * int * string list;; - -let magic strings cmds = - let tms, _ = parse' strings in (* *) - let tms = sort_uniq ~compare:eta_compare tms in - let special_k = compute_special_k (Listx.from_list tms) in (* compute special K *) - let fv = sort_uniq (List.concat (List.map free_vars tms)) in (* free variables *) - let tms = List.map cast_to_i_n_var tms in (* cast nf list -> i_n_var list *) - let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *) - (*let _ = prerr_endline ("Free vars: " ^ String.concat ", " (List.map string_of_var fv)) in*) - let freshno = Listx.max (Listx.from_list fv) in - let dummy = `Var (max_int / 2) in - let deltas = [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in - {freshno; ps; sigma=[] ; deltas}, special_k, cmds -;; - -let magic_conv ~div:_ ~conv:_ ~nums:_ _ = assert false;; diff --git a/ocaml/lambda3.ml.ar b/ocaml/lambda3.ml.ar deleted file mode 100644 index 39e77a7..0000000 --- a/ocaml/lambda3.ml.ar +++ /dev/null @@ -1,550 +0,0 @@ -open Util -open Util.Vars -open Pure -open Num - -type problem = - { freshno: int - ; ps: i_n_var list (* the n-th inert must become n *) - ; sigma: (int * nf) list (* the computed substitution *) - ; deltas: (int * nf) list ref list (* collection of all branches *) - } - -let print_problem {freshno; ps; deltas} = - let deltas = String.concat "\n" (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 - deltas ^ (if deltas = "" then "" else "\n") ^ - String.concat "\n" (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps) -;; - -let make_fresh_var freshno = - freshno+1, freshno+1 - -let make_fresh_vars p m = - let rec aux = - function - 0 -> p.freshno,[] - | n when n > 0 -> - let freshno,vars = aux (n-1) in - let freshno,v = make_fresh_var freshno in - freshno,`Var (0,v)::vars - | _ -> assert false in - let freshno,vars = aux m in - {p with freshno}, vars - -let simple_expand_match ps = - let rec aux level = function - | #i_num_var as t -> aux_i_num_var level t - | `Lam(b,t) -> `Lam(b, aux (level+1) t) - and aux_i_num_var level = function - | `Match(ar,u,bs_lift,bs,args) as torig -> - let u = aux_i_num_var level u in - bs := List.map (fun (n, x) -> n, aux 0 x) !bs; - (try - (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 ar (`N i) bs_lift bs args in - if t <> torig then - aux level (t :> nf) - else raise Not_found - | _ -> raise Not_found) - with Not_found -> - `Match(ar,cast_to_i_num_var u,bs_lift,bs,List.map (aux level) args)) - | `I(ar,k,args) -> `I(ar,k,Listx.map (aux level) args) - | `N _ | `Var _ as t -> t -in aux_i_num_var 0;; - -let rec super_simplify_ps ps it = - let it' = List.map (fun t -> cast_to_i_num_var (simple_expand_match ps t)) (it :> i_num_var list) in - if it <> it' then super_simplify_ps ps it' else it' - -let super_simplify ({ps} as p) = - let ps = super_simplify_ps p.ps (p.ps :> i_num_var list) in - {p with ps=List.map cast_to_i_n_var ps} - -let subst_in_problem x inst ({freshno; ps; sigma} as p) = - let len_ps = List.length ps in -(*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in -prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) - let rec aux ((freshno,acc_ps,acc_new_ps) as acc) = - function - [] -> acc - | t::todo_ps -> -(*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) - let t = subst false x inst (t :> nf) in -(*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) - let freshno,new_t,acc_new_ps = - expand_match (freshno,acc_ps@`Var(-1,max_int/3)::todo_ps,acc_new_ps) t - in - aux (freshno,acc_ps@[new_t],acc_new_ps) todo_ps - - and expand_match ((freshno,acc_ps, acc_new_ps) as acc) t = - match t with - | `Match(ar,u',bs_lift,bs,args) -> - let freshno,u,acc_new_ps = expand_match acc (u' :> nf) in - let acc_new_ps,i = - match u with - `N i -> acc_new_ps,i - | _ -> - let ps = List.map (fun t -> cast_to_i_num_var (subst false x inst (t:> nf))) (acc_ps@acc_new_ps) in - let super_simplified_ps = super_simplify_ps ps ps in -(*prerr_endline ("CERCO u:" ^ print (fst u :> nf)); -List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps; -List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplified_ps;*) - match index_of_opt ~eq:eta_eq super_simplified_ps u with - Some i -> acc_new_ps, i - | None -> acc_new_ps@[u], len_ps + List.length acc_new_ps - in - let freshno= - if List.exists (fun (j,_) -> i=j) !bs then - freshno - else - let freshno,v = make_fresh_var freshno in - bs := !bs @ [i, `Var (ar - 1,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 ar (`N i) bs_lift bs args 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 _ -> - (* the cast will fail *) - (* freshno,(cast_to_i_n_var t),acc_new_ps *) - assert false - | #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 - let freshno,old_ps,new_ps = aux (freshno,[],[]) (ps :> i_num_var list) in - let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in -(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in -prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst)); - let p = {p with freshno; ps; sigma = sigma@[x,inst]} in - let p = super_simplify p in -prerr_endline (print_problem p); p - -exception Dangerous - -let rec dangerous arities showstoppers = - function - `N _ - | `Var _ - | `Lam _ -> () - | `Match(_,t,liftno,bs,args) -> - (* CSC: XXX partial dependency on the encoding *) - (match t with - `N _ -> List.iter (dangerous arities showstoppers) args - | `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args - | `Var (_,x) -> dangerous_inert arities showstoppers x args 2 (* 2 coming from Scott's encoding *) - | `I(_,x,args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *) - ) - | `I(_,k,args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0 - -and dangerous_inert arities showstoppers k args more_args = - List.iter (dangerous arities showstoppers) args ; - if List.mem k showstoppers then raise Dangerous else - try - let _,_,y = List.find (fun (v,_,_) -> v=k) arities in - let arity = match y with `Var _ -> 0 | `I(_,_,args) -> Listx.length args | _ -> assert false in - if List.length args + more_args > arity then raise Dangerous else () - with - Not_found -> () - -(* inefficient algorithm *) -let edible arities showstoppers ps = - let rec aux showstoppers = - function - [] -> showstoppers - | x::xs when List.exists (fun y -> hd_of x = Some y) showstoppers -> - (* se la testa di x e' uno show-stopper *) - let new_showstoppers = sort_uniq (showstoppers @ free_vars (x :> nf)) in - (* aggiungi tutte le variabili libere di x *) - if List.length showstoppers <> List.length new_showstoppers then - aux new_showstoppers ps - else - aux showstoppers xs - | x::xs -> - match hd_of x with - None -> aux showstoppers xs - | Some h -> - try - dangerous arities showstoppers (x : i_n_var :> nf) ; - aux showstoppers xs - with - Dangerous -> - aux (sort_uniq (h::showstoppers)) ps - in - aux showstoppers ps - -let precompute_edible_data {ps} xs = - List.map (fun x -> - let y = List.find (fun y -> hd_of y = Some x) ps in - x, index_of ~eq:eta_eq y ps, y) xs -;; - -let critical_showstoppers p = - let p = super_simplify p in - let showstoppers_step = - List.concat (List.map (fun bs -> - let heads = List.map (fun (i,_) -> List.nth p.ps i) !bs in - let heads = List.sort compare (filter_map hd_of heads) in - snd (split_duplicates heads) - ) p.deltas) in - let showstoppers_step = sort_uniq showstoppers_step in - let showstoppers_eat = - let heads_and_arities = - List.sort (fun (k,_) (h,_) -> compare k h) - (filter_map (function `Var (_,k) -> Some (k,0) | `I(_,k,args) -> Some (k,Listx.length args) | _ -> None ) p.ps) in - let rec multiple_arities = - function - [] - | [_] -> [] - | (x,i)::(y,j)::tl when x = y && i <> j -> - x::multiple_arities tl - | _::tl -> multiple_arities tl in - multiple_arities heads_and_arities in - - let showstoppers_eat = sort_uniq showstoppers_eat in - let showstoppers_eat = List.filter - (fun x -> not (List.mem x showstoppers_step)) - showstoppers_eat in - List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ string_of_var v)) showstoppers_step; - List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ string_of_var v)) showstoppers_eat; - p, showstoppers_step, showstoppers_eat - ;; - -let eat p = - let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in - let showstoppers = showstoppers_step @ showstoppers_eat in - let heads = List.sort compare (filter_map hd_of ps) in - let arities = precompute_edible_data p (uniq heads) in - let showstoppers = edible arities showstoppers ps 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)) -> - let n = match xx with `I(_,_,args) -> Listx.length args | _ -> 0 in - let v = `N(pos) in - let inst = make_lams v n in -(let l = Array.to_list (Array.init (p.freshno + 1) string_of_var) in - prerr_endline ("# INST_IN_EAT: " ^ string_of_var x ^ " := " ^ print ~l inst)); - (* CSC: XXX to avoid applied numbers in safe positions that - trigger assert failures subst_in_problem x inst p*) - { p with sigma = p.sigma @ [x,inst] } - ) p l in - let ps = - List.map (fun t -> - try - let _,j,_ = List.find (fun (h,_,_) -> hd_of t = Some h) l in - `N j - with Not_found -> t - ) ps in - List.iter - (fun bs -> - bs := - List.map - (fun (n,t as res) -> - match List.nth ps n with - `N m -> m,t - | _ -> res - ) !bs - ) p.deltas ; - let p = { p with ps } in - if l <> [] then prerr_endline (print_problem p); - if List.for_all (function `N _ -> true | _ -> false) ps then - `Finished p - else - `Continue p - -let instantiate p x n = - let p,vars = make_fresh_vars p n in - let freshno,zero = make_fresh_var p.freshno in - let p = {p with freshno} in - let zero = Listx.Nil (`Var (0,zero)) in - let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in - let bs = ref [] in - let inst = `Lam(false,`Match(-1,`I(-1,0,Listx.map (lift 1) args),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 - | `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)) - | `N _ -> 0 - | `Var _ -> 0 - ) in Listx.max (Listx.map (aux 0) tms) -;; - -let auto_instantiate (n,p) = - let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in - let x = - match showstoppers_step, showstoppers_eat with - | [], y::_ -> - prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y - | [], [] -> - let heads = List.sort compare (filter_map (fun t -> match t with `Var _ -> None | x -> hd_of x) ps) in - (match heads with - [] -> assert false - | x::_ -> - prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x); - x) - | x::_, _ -> - prerr_endline ("INSTANTIATING " ^ string_of_var x); - x in -(* Strategy that decreases the special_k to 0 first (round robin) -1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *) -let x = - try - (match hd_of (List.find (fun t -> compute_special_k (Listx.Nil (t :> nf)) > 0) ps) with - None -> assert false - | Some x -> - prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x); - x) - with - Not_found -> x -in -(* Instantiate in decreasing order of compute_special_k -1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s -let x = - try - (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) ps)))) with - None -> assert false - | Some x -> - prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x); - x) - with - Not_found -> x -in*) - let special_k = - compute_special_k (Listx.from_list (p.ps :> nf list) )in - if special_k < n then - prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@"); - let p = instantiate p x special_k in - special_k,p - -let problem_measure {ps} = - (* let rec term_size_i_n_var = - function - | `I(v,nfs) -> - (Listx.length nfs) * - (List.fold_right (fun (a,b) c -> 10 + ((a+1) * term_size b) + c) (List.mapi (fun x y -> (x,y)) (Listx.to_list nfs)) 0) - | `Var _ -> 1 - | `N _ -> 0 - and term_size = - function - | #i_n_var as t -> term_size_i_n_var t - | `Match(t,lift,bs,args) -> 1 + (term_size (t :> nf)) + 1 + (List.fold_right ((+) ++ term_size) args 0) - | `Lam(b,t) -> (if b then 0 else 1) + term_size t - (* in List.fold_right ((+) ++ term_size_i_n_var) ps 0;; *) - in ... *) - 0 - -let rec auto_eat (n,({ps} as p)) = - match eat p with - `Finished p -> p - | `Continue p -> - let p' = auto_instantiate (n,p) in - let m' = problem_measure (snd p') in - let delta = m' - problem_measure p in - (if delta >= 0 - then print_endline ("$$$$ MEASURE DID NOT DECREASE (after inst) delta=" ^ string_of_int delta)); - let p'' = auto_eat p' in - (if m' <= problem_measure p'' - then print_endline ("$$$$ MEASURE DID NOT DECREASE (after eat) $$$")); - p'' -;; - -let auto p n = - prerr_endline ("@@@@ FIRST INSTANTIATE PHASE (" ^ string_of_int n ^ ") @@@@"); - auto_eat (n,p) -;; - -(* -0 = snd - - x y = y 0 a y = k k z = z 0 c y = k y u = u h1 h2 0 h2 a = h3 -1 x a c 1 a 0 c 1 k c 1 c 0 1 k 1 k 1 k -2 x a y 2 a 0 y 2 k y 2 y 0 2 y 0 2 h2 0 2 h3 -3 x b y 3 b 0 y 3 b 0 y 3 b 0 y 3 b 0 y 3 b 0 (\u. u h1 h2 0) 3 b 0 (\u. u h1 (\w.h3) 0) -4 x b c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c -5 x (b e) 5 b e 0 5 b e 0 5 b e 0 5 b e 0 5 b e 0 5 b e 0 -6 y y 6 y y 6 y y 6 y y 6 y y 6 h1 h1 h2 0 h2 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0 - - l2 _ = l3 -b u = u l1 l2 0 e _ _ _ _ = f l3 n = n j 0 -1 k 1 k 1 k -2 h3 2 h3 2 h3 -3 l2 0 (\u. u h1 (\w. h3) 0) 3 l3 (\u. u h1 (\w. h3) 0) 3 j h1 (\w. h3) 0 0 -4 l2 0 c 4 l3 c 4 c j 0 -5 e l1 l2 0 0 5 f 5 f -6 h1 h1 (\w. h3) 0 (\w. h3) 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0 -*) - -(* - x n = n 0 ? -x a (b (a c)) a 0 = 1 ? (b (a c)) 8 -x a (b d') a 0 = 1 ? (b d') 7 -x b (a c) b 0 = 1 ? (a c) 4 -x b (a c') b 0 = 1 ? (a c') 5 - -c = 2 -c' = 3 -a 2 = 4 (* a c *) -a 3 = 5 (* a c' *) -d' = 6 -b 6 = 7 (* b d' *) -b 4 = 8 (* b (a c) *) -b 0 = 1 -a 0 = 1 -*) - -(************** Tests ************************) - -let optimize_numerals p = - let replace_in_sigma perm = - let rec aux = function - | `N n -> `N (List.nth perm n) - | `I _ | `Var _ -> assert false - | `Lam(v,t) -> `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 - let deltas' = List.mapi (fun n d -> (n, List.map fst !d)) p.deltas in - let maxs = Array.to_list (Array.init (List.length deltas') (fun _ -> 0)) in - let max = Listx.max (Listx.from_list ( - List.concat (List.map snd deltas') - )) in - let perm,_ = List.fold_left (fun (perm, maxs) (curr_n:int) -> - let containing = filter_map (fun (i, bs) -> if List.mem curr_n bs then Some i else None) deltas' in - (* (prerr_endline (string_of_int curr_n ^ " occurs in: " ^ (String.concat " " (List.map string_of_int containing)))); *) - let neww = Listx.max (Listx.from_list (List.mapi (fun n max -> if List.mem n containing then max else 0) maxs)) in - let maxs = List.mapi (fun i m -> if List.mem i containing then neww+1 else m) maxs in - (neww::perm, maxs) - ) ([],maxs) (Array.to_list (Array.init (max+1) (fun x -> x))) in - replace_in_sigma (List.rev perm) p.sigma -;; - -prerr_endline "########## main ##########";; - -(* Commands: - v ==> v := \a. a k1 .. kn \^m.0 - + ==> v := \^k. numero for every v such that ... - * ==> tries v as long as possible and then +v as long as possible -*) -let main problems = - let rec aux ({ps} as p) n l = - if List.for_all (function `N _ -> true | _ -> false) ps then begin - assert (l = []); - p - end else - let _ = prerr_endline (print_problem p) in - let x,l = - match l with - | cmd::l -> cmd,l - | [] -> read_line (),[] in - let cmd = - if x = "+" then - `DoneWith - else if x = "*" then - `Auto - else - `Step x in - match cmd with - | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *) - | `Step x -> - let x = var_of_string x in - aux (instantiate p x n) n l - | `Auto -> aux (auto p n) n l - in - List.iter - (fun (p,n,cmds) -> - let p_finale = aux p n cmds in - let freshno,sigma = p_finale.freshno, p_finale.sigma in - prerr_endline "------- ------"; - prerr_endline (print_problem p); - prerr_endline "---------------------"; - 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 ps = - List.fold_left (fun ps (x,inst) -> - (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *) - (* 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}); - List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ; -*) - prerr_endline "-------------------"; - let sigma = optimize_numerals p_finale in (* optimize numerals *) - 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 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 ps_ok = List.fold_left (fun ps (x,inst) -> - List.map (Pure.subst false x inst) ps) ps sigma in*) - let e = - let rec aux n = - if n > freshno then - [] - else - let e = aux (n+1) in - (try - e,Pure.lift (-n-1) (let t = (snd (List.find (fun (i,_) -> i = n) sigma)) in prerr_endline (string_of_var n ^ " := " ^ Pure.print t); t),[] - with - Not_found -> [],Pure.V n,[])::e - in - aux 0 in -(* - prerr_endline "------------------"; -let rec print_e e = - "[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]" -in - prerr_endline (print_e e); - List.iter (fun (t,t_ok) -> - prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok); - (*assert (Pure.unwind (e,t,[]) = t_ok)*) - ) (List.combine ps ps_ok); -*) - prerr_endline "-----------------"; - List.iteri (fun i n -> - (*prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n));*) - let t = Pure.mwhd (e,n,[]) in - prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t)); - assert (t = Scott.mk_n i) - ) ps ; - prerr_endline "-------- --------" - ) problems - -(********************** problems *******************) - -let zero = `Var (0,0);; - -let append_zero = - function - | `I _ - | `Var _ as i -> cast_to_i_n_var (mk_app i zero) - | _ -> assert false -;; - -type t = problem * int * string list;; - -let magic strings cmds = - let tms, _ = parse' strings in (* *) - let tms = sort_uniq ~compare:eta_compare tms in - let special_k = compute_special_k (Listx.from_list tms) in (* compute special K *) - let fv = sort_uniq (List.concat (List.map free_vars tms)) in (* free variables *) - let tms = List.map cast_to_i_n_var tms in (* cast nf list -> i_n_var list *) - let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *) - (*let _ = prerr_endline ("Free vars: " ^ String.concat ", " (List.map string_of_var fv)) in*) - let freshno = Listx.max (Listx.from_list fv) in - let dummy = `Var (-1,max_int / 2) in - let deltas = [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in - {freshno; ps; sigma=[] ; deltas}, special_k, cmds -;; - -let magic_conv ~div:_ ~conv:_ ~nums:_ _ = assert false;; diff --git a/ocaml/lambda3.mli b/ocaml/lambda3.mli deleted file mode 100644 index cbaf41c..0000000 --- a/ocaml/lambda3.mli +++ /dev/null @@ -1 +0,0 @@ -include Discriminator.Discriminator diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index dbd7396..25b951a 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -12,7 +12,6 @@ type problem = ; ps: i_n_var list (* the n-th inert must become n *) ; sigma: (int * nf) list (* the computed substitution *) ; deltas: (int * nf) list ref list (* collection of all branches *) - ; steps: int (* how many steps the algorithm made until now *) } @@ -33,8 +32,8 @@ let subterms tms freshno = | `I(v,ts) -> (* applicative (`Var v) (Listx.to_list ts) @ *) Util.concat_map aux (Listx.to_list ts) @ List.map apply_var (Listx.to_list ts) - | `Lam(_,t) -> aux (lift ~-1 t) - | `Match(u,bs_lift,bs,args) -> + | `Lam(_,_,t) -> aux (lift ~-1 t) + | `Match(u,_,bs_lift,bs,args) -> aux (u :> nf) @ (* applicative (`Match(u,bs_lift,bs,[])) args @ *) Util.concat_map aux args @ List.map apply_var args @@ -51,55 +50,15 @@ let all_terms p = @ p.ps ;; -let problem_measure p = - let l = Array.to_list (Array.init (p.freshno + 1) string_of_var) in - let open Listx in - (* aux |t1;t2| e' numero di step per portare la diff in testa - INVARIANTE: t1 t2 - *) - let rec aux t1 t2 = - match t1, t2 with - | `I(v1,nfs1), `I(v2,nfs2) -> - if v1 <> v2 - then 0 else 1 + find_first_diff (to_list nfs1, to_list nfs2) - | `Match (t1,bs_lift,bs,args), `Match (t2,bs_lift',bs',args') -> - if bs != bs' then 0 (* TODO *) - else if eta_eq (t1 :> nf) (t2 :> nf) then 1 + find_first_diff (args, args') else aux (t1 :> nf) (t2 :> nf) (* TODO *) - | `Match _, _ - | _, `Match _ -> 0 (* FIXME!!! *) - | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2 - | _ -> 0 - and find_first_diff = function - | [], [] -> assert false - | [], t::_ - | t::_, [] -> 1 - | t1::ts1, t2::ts2 -> - if eta_eq (t1 :> nf) (t2 :> nf) then 1 + find_first_diff (ts1, ts2) else aux t1 t2 - (* no. di step da fare per separare t1 e t2 *) - in let diff t1 t2 = ( - let res = if eta_eq t1 t2 then 0 else aux t1 t2 in - if res <> 0 then prerr_endline ("diff (" ^ print ~l t1 ^ ") (" ^ print ~l t2 ^ ") = " ^ string_of_int res); - res - ) - (* aux calcola la somma delle differenze tra i termini in una lista (quadratico) *) - in let rec sum = function - | [] -> 0 - | x::xs -> List.fold_right ((+) ++ (diff (x :> nf))) (xs :> nf list) (sum xs) - in let subterms = subterms ((all_terms p) :> nf list) p.freshno - (* let subterms = sort_uniq ~compare:eta_compare subterms in *) - in let a = sum subterms - in let b = List.fold_right (fun bs -> (+) (sum (List.map ((List.nth p.ps) ++ fst) !bs))) p.deltas 0 - in let _ = prerr_endline ("Computed measure: " ^ string_of_int a ^ "," ^ string_of_int b) - in a + b -;; +let problem_measure p = 0 ;; -let print_problem label ({freshno; div; conv; ps; deltas; steps} as p) = +let print_problem label ({freshno; div; conv; ps; deltas} as p) = Console.print_hline (); prerr_endline ("\n||||| Displaying problem: " ^ label ^ " |||||"); 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 ^ string_of_int steps ^ " steps left; measure="^string_of_int(problem_measure p)^" freshno = " ^ string_of_int freshno + nl ^ "measure="^string_of_int(problem_measure p)^" freshno = " ^ string_of_int freshno ^ nl ^ "\b> DISCRIMINATING SETS (deltas)" ^ nl ^ deltas ^ (if deltas = "" then "" else nl) ^ "\b> DIVERGENT" ^ nl @@ -134,22 +93,22 @@ let make_fresh_vars p m = let simple_expand_match ps = let rec aux level = function | #i_num_var as t -> aux_i_num_var level t - | `Lam(b,t) -> `Lam(b, aux (level+1) t) + | `Lam(b,ar,t) -> `Lam(b,ar,aux (level+1) t) and aux_i_num_var level = function - | `Match(u,bs_lift,bs,args) as torig -> + | `Match(u,ar,bs_lift,bs,args) as torig -> let u = aux_i_num_var level u in bs := List.map (fun (n, x) -> n, aux 0 x) !bs; (try (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) bs_lift bs args in + in let t = mk_match (`N i) ar bs_lift bs args 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,bs_lift,bs,List.map (aux level) args)) + `Match(cast_to_i_num_var u,ar,bs_lift,bs,List.map (aux level) args)) | `I(k,args) -> `I(k,Listx.map (aux level) args) | `N _ | `Var _ as t -> t in aux_i_num_var 0;; @@ -216,7 +175,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t = match t with - | `Match(u',bs_lift,bs,args) -> + | `Match(u',ar,bs_lift,bs,args) -> let freshno,u,acc_new_ps = expand_match acc (u' :> nf) in let acc_new_ps,i = match u with @@ -239,7 +198,7 @@ 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) bs_lift bs args in + let t = mk_match (`N i) ar bs_lift bs args 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 @@ -279,7 +238,7 @@ let rec dangerous arities showstoppers = `N _ | `Var _ | `Lam _ -> () - | `Match(t,liftno,bs,args) -> + | `Match(t,_,liftno,bs,args) -> (* CSC: XXX partial dependency on the encoding *) (match t with `N _ -> List.iter (dangerous arities showstoppers) args @@ -304,7 +263,7 @@ let rec dangerous_conv arities showstoppers = `N _ | `Var _ | `Lam _ -> [] - | `Match(t,liftno,bs,args) -> + | `Match(t,_,liftno,bs,args) -> (* CSC: XXX partial dependency on the encoding *) (match t with `N _ -> concat_map (dangerous_conv arities showstoppers) args @@ -494,16 +453,18 @@ let instantiate p x n = let zero = Listx.Nil zero in let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in let bs = ref [] in - let inst = `Lam(false,`Match(`I(0,Listx.map (lift 1) args),1,bs,[])) in + let arity1 = (assert false; -666) in + let arity2 = (assert false; -666) in + let inst = `Lam(false,arity1,`Match(`I(0,Listx.map (lift 1) args),arity2,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) -> aux (k + if b then 1 else 0) t | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms) - | `Match(t, liftno, bs, args) -> + | `Match(t,_,liftno, bs, args) -> List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs)) | `N _ -> 0 | `Var _ -> 0 @@ -572,9 +533,6 @@ let rec auto_eat (n,({ps} as p)) = prerr_endline ("Measure did not decrease (delta=" ^ string_of_int delta ^ ")")) else prerr_endline ("$ Measure decreased by " ^ string_of_int delta); - let p' = {p' with steps=(p'.steps - 1)} in - (if p'.steps < 0 then prerr_endline ">>>>>>>>>> STEPS ARE OVER <<<<<<<<<" - (*failwithProblem p' "steps are over. sorry."*) ); auto_eat (n,p) ;; @@ -632,8 +590,8 @@ 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) - | `Match(_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t + | `Lam(v,ar,t) -> `Lam(v, ar, 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 let deltas' = List.mapi (fun n d -> (n, List.map fst !d)) p.deltas in @@ -702,7 +660,7 @@ let main problems = bomb := `Var (-1); let p_finale = aux p n cmds in let freshno,sigma = p_finale.freshno, p_finale.sigma in - prerr_endline ("------- ------\n " ^ (string_of_int (p.steps - p_finale.steps)) ^ " steps of "^ (string_of_int p.steps) ^"."); + prerr_endline ("------- ------\n "); (* prerr_endline (print_problem "Original problem" p); *) prerr_endline "---------------------"; let l = Array.to_list (Array.init (freshno + 1) string_of_var) in @@ -778,21 +736,11 @@ let append_zero = | _ -> assert false ;; -let bounds_on_steps all_tms = - let rec aux = function - | `I(k,args) -> Listx.fold_left (fun acc t -> 1 + acc + (aux t)) 0 args - | `Var _ -> 1 - | `Lam (_, t) -> 1 + aux t - | _ -> assert false - in List.fold_right ((+) ++ aux) all_tms 0 -;; - type t = problem * int * string list;; let magic_conv ~div ~conv ~nums cmds = let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in let all_tms, var_names = parse' all_tms in - let steps = bounds_on_steps all_tms in let div, (tms, conv) = match div with | None -> None, list_cut (List.length nums, all_tms) | Some _ -> Some (List.hd all_tms), list_cut (List.length nums, List.tl all_tms) in @@ -800,7 +748,7 @@ let magic_conv ~div ~conv ~nums cmds = if match div with None -> false | Some div -> List.exists (eta_subterm div) (tms@conv) then ( prerr_endline "--- TEST SKIPPED ---"; - {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; steps=(-1)}, 0, [] + {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]}, 0, [] ) else let tms = sort_uniq ~compare:eta_compare tms in let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *) @@ -815,7 +763,7 @@ let magic_conv ~div ~conv ~nums cmds = let dummy = `Var (max_int / 2) in [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in - {freshno; div; conv; ps; sigma=[] ; deltas; steps}, special_k, cmds + {freshno; div; conv; ps; sigma=[] ; deltas}, special_k, cmds ;; let magic strings cmds = magic_conv None [] strings cmds;; diff --git a/ocaml/problems.ml b/ocaml/problems.ml index 6fb7b43..bf1b67a 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -1,7 +1,6 @@ let use_lambda3 = Array.length Sys.argv = 1;; -let discriminator = - if use_lambda3 then (module Lambda3 : Discriminator.Discriminator) else (module Lambda4);; +let discriminator = ( module Lambda4 : Discriminator.Discriminator );; module Pippo = (val discriminator);; open Pippo;; diff --git a/ocaml/test.ml b/ocaml/test.ml index 2f6017a..ed41f7a 100644 --- a/ocaml/test.ml +++ b/ocaml/test.ml @@ -1,9 +1,10 @@ let three = Array.length Sys.argv = 1;; let discriminator = - if three - then (module Lambda3 : Discriminator.Discriminator) - else (module Lambda4);; + (* if three *) + (* then (module Lambda3 : Discriminator.Discriminator) *) + (* else *) + (module Lambda4 : Discriminator.Discriminator);; module Pippo = (val discriminator);; open Pippo;; @@ -59,11 +60,11 @@ let rec repeat f n = if n > 0 then repeat f (n-1) ;; -let call_main3 tms = +(* let call_main3 tms = let _ = ( List.iter prerr_endline tms; prerr_newline (); ) in Lambda3.main [Lambda3.magic tms ["*"]] -;; +;; *) let call_main4 div convs nums = let _ = ( (match div with Some div -> prerr_endline ("DIV: " ^ div) | None -> ()); @@ -81,11 +82,12 @@ let main = (* let open Parser in *) - if three then repeat (fun _ -> + (* if three then repeat (fun _ -> let tms = test3 complex vars in call_main3 tms ) num - else repeat (fun _ -> + else *) + repeat (fun _ -> let div, (conv, nums) = test4 complex vars in call_main4 (Some div) conv nums ) num -- 2.39.2