From: Date: Mon, 12 Jun 2017 20:44:12 +0000 (+0200) Subject: Moved andrea's stuff to its branch X-Git-Tag: weak-reduction-separation~78 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=382508ec4c624977ad2950cbe0e9ae26ce7e41c8;p=fireball-separation.git Moved andrea's stuff to its branch --- diff --git a/ocaml/Makefile b/ocaml/Makefile index 3310c6e..6ff0e02 100644 --- a/ocaml/Makefile +++ b/ocaml/Makefile @@ -13,12 +13,6 @@ test.out: $(UTILS) lambda3.cmx test1.ml test34.out: $(UTILS) lambda3.cmx lambda4.cmx test.ml $(OCAMLC) -o test34.out $(LIB) $^ -andrea.out: $(UTILS) a.out andrea6.ml - $(OCAMLC) -o andrea.out $(LIB) $(UTILS) andrea6.ml - -#test2.out: $(UTILS) lambda3.ml test2.ml andrea -# ocamlc -o test2.out $(LIB) $(UTILS) lambda3.ml andrea4.ml test2.ml - %.cmi: %.mli $(OCAMLC) -c $< diff --git a/ocaml/andrea3.ml b/ocaml/andrea3.ml deleted file mode 100644 index 2796107..0000000 --- a/ocaml/andrea3.ml +++ /dev/null @@ -1,364 +0,0 @@ -type var = (* unique name *) int * (int * term) option * (*level*) int -and term = - | Tvar of var - | Tapp of term * term - | Tlam of int * term -;; - -let zero = Tvar(1010, None, 0);; -let dummy = Tvar(333, None, 0);; - -(* mk_app & subst implementano la beta *) -let rec mk_app t1 t2 = match t1 with - | Tlam(v, t1') -> subst v t2 t1' - | _ -> Tapp(t1, t2) -and subst v tv = - let rec aux = function - | Tapp(t1, t2) -> mk_app (aux t1) (aux t2) - | Tvar(v', _, _) as t -> if v = v' then tv else t - | Tlam(v', t') as t -> if v = v' then t else Tlam(v', aux t') - in aux -;; - -(* PARSING AND PRINTING *) - -let parse = - let rec minus1 = function - | Tvar(n, None, x) -> Tvar(n-1, None, x) - | Tvar _ -> assert false - | Tapp(t1, t2) -> Tapp(minus1 t1, minus1 t2) - | Tlam(n, t) -> Tlam(n-1, minus1 t) - (* in let open Parser *) - in let rec myterm_of_term = function - | Parser.Var n -> Tvar(n, None, 0) - | Parser.App(t1, t2) -> (*Tapp(myterm_of_term t1, myterm_of_term t2) WARNING! BETA DOWN HERE! *) - mk_app (myterm_of_term t1) (myterm_of_term t2) - | Parser.Lam(t) -> minus1 (Tlam(0, myterm_of_term t)) - in fun strs -> ( - let (tms, free) = Parser.parse_many strs - in List.map myterm_of_term tms - ) -;; - -(* PRETTY PRINTING *) -open Console;; - -let fancy_of_term t = -let rec string_of_term = - let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"] in - let bound = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"] in - let string_of_int' n = if n >= 0 then List.nth free (n) else List.nth bound (-n-1) in - let rec string_of_var t = - if Tvar t = dummy then "_" else if Tvar t = zero then "ZZ" else match t with - | (n, None, _) -> (string_of_int' n) - (* | (_, Some(n,t), _) -> "?" ^ string_of_int n *) - | (_, Some(n,t), _) -> "{" ^ (string_of_term_no_pars t) ^ "|" ^ (string_of_int n) ^ "}" - and string_of_term_w_pars = function - | Tvar v -> string_of_var v - | Tapp(t1, t2) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")" - | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")" - and string_of_term_no_pars_app = function - | Tapp(t1, t2) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) - | _ as t -> string_of_term_w_pars t - and string_of_term_no_pars_lam = function - | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t) - | _ as t -> string_of_term_no_pars t - and string_of_term_no_pars = function - | Tlam(_, _) as t -> string_of_term_no_pars_lam t - | _ as t -> string_of_term_no_pars_app t - in string_of_term_no_pars -in let rec html_of_term = - let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"] in - let bound = ["x"; "y"; "z"; "w"; "q"] in - let string_of_int' n = if n >= 0 then List.nth free (n) else List.nth bound (-n-1) in - let rec string_of_var t = - if Tvar t = dummy then "#" else if Tvar t = zero then "Z" else match t with - | (n, None, _) -> (string_of_int' n) - | (_, Some(n,t), _) -> "α" ^ (string_of_term_no_pars t) ^ "" ^ (string_of_int n) ^ "" - and string_of_term_w_pars = function - | Tvar v -> string_of_var v - | Tapp(t1, t2) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")" - | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")" - and string_of_term_no_pars_app = function - | Tapp(t1, t2) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) - | _ as t -> string_of_term_w_pars t - and string_of_term_no_pars_lam = function - | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t) - | _ as t -> string_of_term_no_pars t - and string_of_term_no_pars = function - | Tlam(_, _) as t -> string_of_term_no_pars_lam t - | _ as t -> string_of_term_no_pars_app t - in string_of_term_no_pars -in - string_of_term t / html_of_term t -;; - -let fancy_of_nf t: Console.fancyobj = -let rec print ?(l=[]) = - function - `Var n -> Lambda3.print_name l n - | `N n -> string_of_int n - | `Match(t,bs_lift,bs,args) -> - "([" ^ print ~l (t :> Lambda3.nf) ^ - " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (Lambda3.lift bs_lift t)) !bs) ^ "] " ^ - String.concat " " (List.map (print ~l) args) ^ ")" - | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")" - | `Lam nf -> - let name = Lambda3.string_of_var (List.length l) in - "" ^ name ^ "." ^ print ~l:(name::l) (nf : Lambda3.nf) - -in let rec print_html ?(l=[]) = - function - `Var n -> Lambda3.print_name l n - | `N n -> string_of_int n - | `Match(t,bs_lift,bs,args) -> - "(match " ^ print_html ~l (t :> Lambda3.nf) ^ - " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " ⇒ " ^ print_html ~l (Lambda3.lift bs_lift t)) !bs) ^ "..." (* Attenzion non sto stampando gli argomenti applicati! Perche' non ce ne sono mai *) - | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print_html ~l) args)) ^ ")" - | `Lam nf -> - let name = Lambda3.string_of_var (List.length l) in - "λ" ^ name ^ ". " ^ print_html ~l:(name::l) (nf : Lambda3.nf) -in - print t / print_html t -;; - -let print_term t = print_endline (fancy_of_term t :> Console.fancyobj);; -(* *) - - -let varcount = ref 0;; - -let freshvar () = ( - varcount := (!varcount + 1); - !varcount -);; - -let rec hd = - function - | Tvar x -> x - | Tapp(t1,t2) -> hd t1 - | Tlam _ -> assert false -;; - -let alive (_, _, n) = n;; -let rec setalive c = function - | Tvar(a,b,_) as v -> if v <> zero && v <> dummy then Tvar(a,b,c) else v - | Tapp(a,b) -> Tapp(setalive c a, setalive c b) - | Tlam(n, t) -> Tlam(n, setalive c t) -;; - -let mk_vars t lev = - let rec aux n = - if n = 0 - then [] - else Tvar(0, Some(n, t), lev) :: (aux (n-1)) - in aux -;; - -let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *) - - -let compute_special_k tms = - let rec aux k t = match t with - | Tvar _ -> 0 - | Tapp(t1,t2) -> Pervasives.max (aux 0 t1) (aux 0 t2) - | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t) - in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms -;; - -let compute_special_h tms = - let rec eat_lam = function - | Tlam(_,t) -> eat_lam t - | _ as t -> t - in - let rec aux t = match t with - | Tvar _ -> 0 - | Tapp(t1,t2) -> Pervasives.max (aux t1) (aux t2) - | Tlam(v,t) -> 1 + (aux (eat_lam t)) - in 1 + List.fold_left (fun b a -> Pervasives.max (aux a) b) 0 tms -;; - -(* funzione di traduzione brutta & cattiva *) -let translate k = - let rec aux = function - | Tlam _ -> assert false - | Tvar _ as v -> v - | Tapp(t1, t2) -> - let v = hd t1 in - let a = alive v in - let t1' = aux t1 in - let t2' = if a = 0 - then t2 - else mk_apps t2 ((List.rev (mk_vars t1' (a-1) k)) @ [zero]) - in Tapp(t1', aux t2') - in aux -;; - -(* sostituisce gli argomenti dummy (delle variabili morte) con 'dummy' *) -let rec dummize = function - | Tlam _ -> assert false - | Tvar (a,Some(b,t), c) -> Tvar(a, Some (b, dummize t), c) - | Tvar _ as v -> v - | Tapp(t1, t2) -> - if alive (hd t1) = 0 - then Tapp(dummize t1, dummy) - else Tapp(dummize t1, dummize t2) -;; - -(* lista di sottotermini applicativi *) -let rec subterms = function - | Tlam _ -> assert false - | Tvar _ as v -> [v] - | Tapp(t1, t2) -> Tapp(t1, t2) :: ((subterms t1) @ (subterms t2)) -;; - -(* filtra dai sottotermini le variabili *) -let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;; - - -let rec stupid_uniq = function - | [] -> [] - | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs) -;; -let stupid_compare a b = - let rec size = function - | Tvar(_,None,_) -> 0 - | Tvar(_,Some(_,t),_) -> 1 + size t - | Tapp(t1,t2) -> 1 + size t1 + size t2 - | Tlam _ -> assert false - in compare (size a) (size b) -;; -let stupid_sort_uniq l = stupid_uniq (List.sort stupid_compare l);; - -(* crea i match ricorsivamente. - - k e' lo special-K - - subs e' l'insieme dei sottotermini - TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione - *) -let crea_match k subs (acc : (term * Lambda3.nf) list) : term -> Lambda3.nf = - let req t = try List.assoc t acc with Not_found -> `Var 9999 in - let aux t1 = ( - if t1 = dummy then `Var 99999 else - (* let _ = print_term t1 in *) - let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2)) subs) subs - in if cont = [] then - try `N (Lambda3.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else - let a = alive (hd t1) in - if a = 0 then `Lam (req (Tapp(t1, dummy))) - else ( - let vars = (List.rev (mk_vars t1 (a-1) k)) @ [zero] - (* in let _ = print_endline (String.concat " " (List.map string_of_term vars)) - in let _ = print_term (mk_apps dummy vars) *) - in let vars = List.map req vars - in let vars = List.map (Lambda3.lift 1) vars (* forse lift non necessario *) - in let vars = Listx.from_list vars - in let body = `I(0, vars) - in let branches = List.map (fun t2 -> (Lambda3.index_of t2 subs, req (Tapp(t1, t2)))) cont - in let bs = ref(branches) - in let lift = 1 - in let args = [] - in `Lam (`Match(body, lift, bs, args)) - ) - ) in aux -;; - -let mk_zeros k = - let rec aux n prev = - if n = 0 then [zero] - else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev - in aux (k+1) [] -;; - -let is_scott_n t n = - let open Lambda3 in let open Pure in - let rec aux n = function - | L (L (A (V 1, L (V 0)))) -> n = 0 - | L (L (A (V 0, t))) -> aux (n-1) t - | _ -> assert false - in aux n t -;; - -(* do the magic *) -let magic strings k h = ( - let tms = parse strings - in let tms = List.map (fun x -> Tapp(x, zero)) tms - in let tms' = List.map (setalive h) tms - in let tms' = List.map (translate k) tms' - in let tms' = List.map dummize tms' - in let progress s = print_bullet (fancy_of_string s) - in let _ = progress "traduzione completata" - (* in let _ = List.map print_term tms' *) - in let _ = progress "ordino i sottotermini" - in let subs = List.concat (List.map subterms tms') - in let subs = stupid_sort_uniq subs - (* metti gli zeri in testa, perche' vanno calcolati per primi *) - in let zeros = mk_zeros k - in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros) - in let _ = progress ("sottotermini generati: " ^ string_of_int (List.length subs)) - in let vars = vars subs - (* in let _ = List.iter print_term subs *) - (* in let _ = 0/0 *) - in let fv = List.filter (function Tvar(_, None, _) as v -> v <> dummy | _ -> false) vars - (* in let _ = print_string ("> free vars: " ^ String.concat ", " (List.map (string_of_term) fv)) *) - in let _ = progress "sto creando i match" - (* in let sigma = List.map (fun x -> x, crea_match k subs x) fv *) - in let f t acc = let res = crea_match k subs acc t in (t,res)::acc - in let acc = List.fold_right f subs [] - in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc - in let _ = progress "match creati" - in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " ↦ ") ^^ fancy_of_nf y)) sigma - - in let _ = progress "controllo di purezza"; - in let open Lambda3 - in let ps, _ = Lambda3.parse' strings - in let ps = List.map (fun x -> Lambda3.mk_app x (`Var 1010)) ps - in let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) ps - in let sigma = List.map ( - function (Tvar(n,_,_), inst) -> n, ToScott.t_of_nf inst | _ -> assert false - ) sigma - in let ps = - List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma - in let _ = List.iteri (fun i n -> - (* print_string_endline ((string_of_int i) ^ ":: " ^ (Pure.print (Pure.whd n))); *) - (* assert (Pure.whd n = Scott.mk_n (Lambda3.index_of (List.nth tms' i) subs))) ps *) - assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs))) ps - in let _ = progress "fatto." in () -);; - -let do_everything tms = -let tms' = parse tms in -let _ = List.iter print_term tms' in -let k = compute_special_k tms' in -let h = compute_special_h tms' in -(* let _ = print_string_endline (string_of_int h) in *) -magic tms k h -;; - -let _ = - let tms = ["a a"; "a b"; "b a"; "b (x. y.x y a)"] in - (* 1 2 *) - (* let tms = ["x c" ; "b (x c d e)"; "b"] in *) - (* 0 1 *) - (* let tms = ["x x x"] in *) - let tms' = parse tms in - let _ = List.iter print_term tms' in - let k = compute_special_k tms' in - let h = compute_special_h tms' in - (* let _ = print_string_endline (string_of_int h) in *) - magic tms k h -;; - -(* type var' = (* unique name *) int * (int * term') option * (*dead*) bool option -and term' = - | Tvar' of var' - | Tapp' of term' * term' * (* active *) bool - | Tlam' of int * term' -;; - -let rec iter mustapply = - let aux = function - | Tvar'(n, Some(m,t), b) -> Tvar(n, Some(m, aux t), b) - | Tvar' _ as v -> v - | Tapp'(t1, t2, b) -> if b && - in aux -;; *) diff --git a/ocaml/andrea5.ml b/ocaml/andrea5.ml deleted file mode 100644 index eadb645..0000000 --- a/ocaml/andrea5.ml +++ /dev/null @@ -1,27 +0,0 @@ -(* percorsi di differenza etc. *) - -open Lambda3;; - -type formula = - | Var of int - | And of formula * formula - | Or of formula * formula -;; - -let rec mk_k_vars k = - if k = 0 then [] - else `Var (k-1) :: (mk_k_vars (k-1)) -;; - -let is_lambda = function - | `Lam _ -> true - | _ -> false -;; - -let rec diff k level t1 t2 = - if is_lambda t1 || is_lambda t2 - then let vars = mk_k_vars k in - let level = level + k in - diff k level (mk_appl (lift k t1) vars) (mk_appl (lift k t2) vars) - else assert false -;; diff --git a/ocaml/andrea6.ml b/ocaml/andrea6.ml deleted file mode 100644 index 34c0788..0000000 --- a/ocaml/andrea6.ml +++ /dev/null @@ -1,474 +0,0 @@ -let print_hline = Console.print_hline;; - -type var = int;; - -type t = - | V of var - | A of t * t - | L of t - | LM of - t list (* body of the match *) - * int (* explicit liftno *) - * int (* variable which originated this match (id) *) - | B (* bottom *) - | P (* pacman *) -;; - - -type problem = { - freshno : int - ; div : t - ; conv : t list - ; matches : (var (* variable originating this match *) * (t (* term to discriminate *) * t (* continuation *)) list) list - ; sigma : (var * t) list (* substitutions *) -} - -let string_of_t p = - let bound_vars = ["x"; "y"; "z"; "z1"; "z2"] in - let rec aux level = function - | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1) - | A (t1,t2) -> "("^aux level t1^" "^aux level t2^")" - | L t -> "(\\" ^ aux (level+1) (V 0) ^ ". " ^ aux (level+1) t ^ ")" - | LM (ts,liftno,id) -> "[match orig="^aux 0 (V id)^"]" - | B -> "BOT" - | P -> "PAC" - in aux 0 -;; - -let string_of_problem p = - let lines = [ - "[DV] " ^ string_of_t p p.div; - "[CV] " ^ String.concat "\n " (List.map (string_of_t p) p.conv); - "" ; - ] @ Util.concat_map (fun (_, lst) -> "[<>]" :: List.map (fun (t,c) -> " " ^ string_of_t p t - (* ^" -> " ^ string_of_t p c *) - ) lst) p.matches @ [""] in - String.concat "\n" lines -;; - -let problem_fail p reason = - print_endline " FAIL FAIL FAIL FAIL FAIL FAIL FAIL FAIL FAIL"; - print_endline (string_of_problem p); - failwith reason -;; - -let freshvar ({freshno} as p) = - {p with freshno=freshno+1}, freshno+1 -;; - -let add_to_match p id entry = - let matches = try - let _ = List.assoc id p.matches in - List.map (fun (id',lst as x) -> if id <> id' then x else (id, entry::lst) ) p.matches - with - | Not_found -> (id,[entry]) :: p.matches in - {p with matches=matches} -;; - -let free_in v = - let rec aux level = function - | V v' -> v + level = v' - | A(t1,t2) -> (aux level t1) || (aux level t2) - | L t -> aux (level+1) t - | LM(ts,_,_) -> List.fold_left (fun a b -> a || aux (level+1) b) false ts - | B -> false - | P -> false - in aux 0 -;; - -let rec is_inert = - function - | A(t,_) -> is_inert t - | L _ | LM _ | B -> false - | _ -> true -;; - -let is_var = function V _ -> true | _ -> false;; -let is_lambda = function L _ -> true | _ -> false;; -let is_pacman = function P -> true | _ -> false;; - -let rec subst level delift sub p = - function - | V v -> p, if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v) - | L t -> let p, t = subst (level + 1) delift sub p t in p, L t - | A (t1,t2) -> - let p, t1 = subst level delift sub p t1 in - let p, t2 = subst level delift sub p t2 in - if t1 = B || t2 = B then p, B else - if level = 0 then mk_app p t1 t2 else p, A (t1, t2) - | LM (ts, liftno, id) -> - let p, ts = - let rec aux p = function - | [] -> p, [] - | t::ts -> - let p, ts = aux p ts in - let p, t = subst (level+1) delift sub p t in - p, t::ts in - aux p ts in - p, LM(ts, liftno, id) - | B -> p, B - | P -> p, P -and mk_app p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with - | L t1 -> - let p = if is_inert t2 && not (is_var t2) && free_in 0 t1 then {p with conv=t2::p.conv} else p in - subst 0 true (0, t2) p t1 - | LM(ts,liftno,id) -> - let p, t = mk_apps p t2 (List.map (lift ~-1) ts) in - if t = B - then p, B - else - let p, cont = freshvar p in - let newvar = V cont in - let p = add_to_match p id (t,newvar) in - p, newvar - | B - | _ when t2 = B -> p, B - | t1 -> p, A (t1, t2) -and mk_apps p t = - function - | [] -> p, t - | t'::ts -> let p, t = mk_app p t t' in mk_apps p t ts -and lift n = function - | V m -> V (m + n) - | L t -> L (lift n t) - | A (t1, t2) -> A (lift n t1, lift n t2) - | LM (ts, liftno, id) -> LM (List.map (lift n) ts, n + liftno, id) - | B -> B - | P -> P - ;; - -let subst = subst 0 false;; - -let mk_lambda t = L (lift 1 t) ;; - -let subst_many sub = - let rec aux p = function - | [] -> p, [] - | t::tms -> - let p, t = subst sub p t in - let p, tms = aux p tms in - p, t :: tms - in aux -;; - -let rec subst_in_matches sub p = - function - | [] -> p, [] - | (v, branches) :: ms-> - let a, b = List.split branches in - let p, a = subst_many sub p a in - let p, b = subst_many sub p b in - let branches = List.combine a b in - let p, ms = subst_in_matches sub p ms in - p, (v, branches) :: ms -;; - -let subst_in_problem (sub: var * t) (p: problem) = -(* print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " " ^ string_of_t p (snd sub)); *) - let p', div = subst sub p p.div in - let p = {p' with conv=p.conv} in - let p, conv = subst_many sub p p.conv in - let p, matches = subst_in_matches sub p p.matches in - {p with div=div; conv=conv; matches=matches; sigma=sub::p.sigma} -;; - -(* FIXME *) -let unify_terms p t1 t2 = - match t1 with - | V v -> subst_in_problem (v, t2) p - | _ -> problem_fail p "The collapse of a match came after too many steps :(";; - -let rec unify p = - let rec give_duplicates = - let rec aux' t = function - | [] -> [], None - | (t',c')::ts -> if t = t' then ts, Some c' else ( - let ts, res = aux' t ts in (t',c')::ts, res) in - let rec aux = function - | [] -> [], None - | (t,c)::rest -> ( - match aux' t rest with - | rest, None -> aux rest - | rest, Some c' -> (t,c)::rest, Some (c', c) - ) in - function - | [] -> [], None - | (orig,branches) :: ms -> - match aux branches with - | _, None -> let ms, res = give_duplicates ms in (orig,branches) :: ms, res - | branches', Some subst -> (orig,branches') :: ms, Some subst in - let matches, vars_to_be_unified = give_duplicates p.matches in - let p = {p with matches=matches} in - match vars_to_be_unified with - | None -> p - | Some(t', t) -> - (* print_endline ("> unify " ^ string_of_t p (t') ^ " with " ^ string_of_t p t); *) - unify (unify_terms p t' t) -;; - -let problem_done p = - let all_separated = List.for_all (fun (_, lst) -> List.length lst = 1 || List.for_all (fun (t,_) -> is_var t) lst) p.matches in - all_separated && p.div = B -;; - -exception Done;; - -let sanity p = - (* Sanity checks: *) - if is_lambda p.div || is_pacman p.div then problem_fail p "p.div converged" ; - List.iter (function | B -> problem_fail p "p.conv diverged" | _ -> ()) p.conv; - if not (List.for_all (fun (_, lst) -> List.for_all (fun (t,_) -> is_inert t) lst) p.matches) - then problem_fail p "Lambda in a match: k was not big enough?"; - - (* Remove lambdas from conv TODO remove duplicates *) - let conv = List.filter is_inert p.conv in - let p = {p with conv=conv} in - (* unify! :( *) - let p = unify p in - print_endline (string_of_problem p); - if problem_done p then raise Done else p -;; - -let ignore var n p = -print_endline ( - "--- EAT on " ^ string_of_t p (V var) - ^ " (of:" ^ string_of_int n ^ ")"); - let rec aux m t = - if m = 0 - then lift n t - else L (aux (m-1) t) in - let subst = var, aux n (V var) in - sanity (subst_in_problem subst p) -;; - -let explode' var p = - print_endline ( - "--- EXPLODE on " ^ string_of_t p (V var) - ); - let subst = var, B in - sanity (subst_in_problem subst p) - ;; - -let explode p = - match p.div with - | V var -> explode' var p - | _ -> problem_fail p "premature explosion" -;; - -let step var p = - print_endline ( - "--- STEP on " ^ string_of_t p (V var)); - let subst = var, LM([], 0, var) in - sanity (subst_in_problem subst p) -;; - -let id var p = - print_endline ( - "--- ID on " ^ string_of_t p (V var)); - let subst = var, L(V 0) in - sanity (subst_in_problem subst p) -;; - -let apply var appk p = - print_endline ( - "--- APPLY_CONSTS on " ^ string_of_t p (V var) - ^ " (special_k:" ^ string_of_int appk ^ ")"); - let rec mk_freshvars n p = - if n = 0 - then p, [] - else - let p, vs = mk_freshvars (n-1) p in - let p, v = freshvar p in - p, V(v)::vs in - let p, vars = mk_freshvars appk p in - let p, t = mk_apps p (V 0) (List.map (lift 1) vars) in - let t = L (A (lift 1 (V var), t)) in - let subst = var, t in - sanity (subst_in_problem subst p) -;; - -let perm var n p = - print_endline ( - "--- PERM on " ^ string_of_t p (V var) - ^ " (of:" ^ string_of_int n ^ ")"); - (* let p, v = freshvar p in *) - let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V m) in - let rec aux m t = - if m = 0 - then aux' (n-1) t - else L (aux (m-1) t) in - let t = aux n (lift n (V var)) in - let subst = var, t in - sanity (subst_in_problem subst p) -;; - -(* TODO: -- cosi' come e' possibile unificare rami di branch solo se vanno -> a variabili, - allo stesso modo e' possibile ignorare dei rami se vanno in variabili, e quelle variabili - vengono sostituite ovunque: con bombe in conv e con pacman in div -*) -(* let forget var n p = - let remove_from_branch p var n = ... in - let p, (tm, c) = remove_from_branch p var n in - print_endline ( - "--- FORGET " ^ string_of_t p tm ^ " from the match of " ^ string_of_t p (V var) - ^ " (of:" ^ string_of_int n ^ ")"); - sanity p -;; *) - -let parse strs = - let dummy_p = {freshno=0; div=V 0; conv=[]; matches=[]; sigma=[]} in - let rec aux level = function - | Parser.Lam t -> L (aux (level + 1) t) - | Parser.App (t1, t2) -> - if level = 0 then snd (mk_app dummy_p (aux level t1) (aux level t2)) - else A(aux level t1, aux level t2) - | Parser.Var v -> V v - in let (tms, free) = Parser.parse_many strs - in (List.map (aux 0) tms, free) -;; - -let magic6 div conv cmds = - print_hline (); - let all_tms, var_names = parse (div :: conv) in - let div, conv = List.hd all_tms, List.tl all_tms in - let freshno = 1 + List.length var_names in - let p = {freshno; div; conv; matches=[]; sigma=[]} in - let p = try - let subst = Util.index_of "BOMB" var_names, L B in - let p = subst_in_problem subst p in p - with Not_found -> p in - let p = sanity p in - try - problem_fail (List.fold_left (|>) p cmds) "Problem not completed" - with - | Done -> () -;; - -let interactive div conv cmds = - print_hline (); - let all_tms, var_names = parse (div :: conv) in - let div, conv = List.hd all_tms, List.tl all_tms in - let freshno = 1 + List.length var_names in - let p = {freshno; div; conv; matches=[]; sigma=[]} in - let p = try - let subst = Util.index_of "BOMB" var_names, L B in - let p = subst_in_problem subst p in p - with Not_found -> p in - let p = sanity p in - let p = List.fold_left (|>) p cmds in - let rec f p cmds = - let nth spl n = int_of_string (List.nth spl n) in - let read_cmd () = - let s = read_line () in - let spl = Str.split (Str.regexp " +") s in - s, let uno = List.hd spl in - try if uno = "explode" then explode - else if uno = "ignore" then ignore (nth spl 1) (nth spl 2) - else if uno = "step" then step (nth spl 1) - else if uno = "perm" then perm (nth spl 1) (nth spl 2) - else if uno = "apply" then apply (nth spl 1) (nth spl 2) - else if uno = "id" then id (nth spl 1) - else failwith "unknown" - with Failure _ -> print_endline "Wrong input."; (fun x -> x) in - let str, cmd = read_cmd () in - let cmds = str::cmds in - try - let p = cmd p in f p cmds - with - | Done -> List.iter print_endline (List.rev cmds) - in f p [] -;; - -let _ = magic6 - "x x" - [ "_. BOMB" ] - [ ignore 1 1; explode ] -;; - - let _ = magic6 - "x y BOMB b" - [ "x BOMB y c" ] - [ perm 1 3; step 1 ; ignore 8 2; explode; ];; - -let _ = magic6 - "x BOMB a1 c" - [ "x y BOMB d"; "x BOMB a2 c" ] - [ perm 1 3 ; step 1 ; step 12; ignore 13 1; explode; ] -;; - -let _ = magic6 - "x (x x)" - [ "x x" ; "x x x" ] [ - apply 1 1; - step 1; - explode; - step 9; -];; - -let _ = magic6 - "x (_.BOMB)" - [ "x (_._. BOMB)" ] - [ apply 1 2; ] -;; - -let _ = magic6 - "x (_.y)" - [ "y (_. x)" ] - [ apply 1 1; ignore 1 1; explode; ] -;; - -let _ = magic6 - "y (x a1 BOMB c) (x BOMB b1 d)" - [ "y (x a2 BOMB c) (x BOMB b1 d)"; - "y (x a1 BOMB c) (x BOMB b2 d)";] - [ perm 2 3; step 2; step 17; perm 16 2; step 16; ignore 19 1; ignore 20 1; ignore 22 1; ignore 23 1; step 1; step 26; explode; ] -;; - -let _ = magic6 - "z (y x)" - [ "z (y (x.x))"; "y (_. BOMB)" ] - [ apply 2 1; step 3; explode' 8; ] -;; - -let _ = magic6 - "y x" - [ "y (x.x)"; "x (_. BOMB)" ] - [ apply 1 1; ignore 2 1; step 1; explode; ] -;; - -let _ = magic6 - "z (y x)" - [ "z (y (x.x))"; "y (_. BOMB)" ] - [ step 1; explode; apply 2 1; id 2; ignore 3 1; ] -;; - -let _ = magic6 - "y (x a)" - [ "y (x b)"; "x BOMB" ] [ - id 2; - step 1; - explode; -];; - -magic6 - "y (x a)" [ "y (x b)"; "x BOMB"; "y a" ] - [ - apply 1 1; - perm 2 2; - perm 2 2; - step 3; - apply 2 1; - ignore 4 1; - step 2; - ignore 12 1; - ignore 13 1; - step 1; - explode; -];; - -interactive - "y (x a)" -[ "y (x b)"; "x BOMB"; "y a" ] [];; - -print_endline "ALL DONE. " diff --git a/ocaml/mk_andrea b/ocaml/mk_andrea deleted file mode 100644 index a29f203..0000000 --- a/ocaml/mk_andrea +++ /dev/null @@ -1,3 +0,0 @@ -ocamlc -c parser.ml -ocamlc -o andrea andrea.ml parser.cmo -./andrea