X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=ocaml%2Fsimple.ml;h=28603258c04539410f98afb02d2ac301f97c793c;hb=62d2aea15e05a7366e0bbdc71574ad50cda28ff5;hp=8b47f88a5693153a630fdad73b9a20a2f3556226;hpb=3d8ab5897c6aa3d9c1b317e1137b3fcd2668f25e;p=fireball-separation.git diff --git a/ocaml/simple.ml b/ocaml/simple.ml index 8b47f88..2860325 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -17,7 +17,7 @@ type t = let delta = L(A(V 0, V 0));; -let eta_eq = +let eta_eq' = let rec aux l1 l2 t1 t2 = match t1, t2 with | L t1, L t2 -> aux l1 l2 t1 t2 | L t1, t2 -> aux l1 (l2+1) t1 t2 @@ -26,10 +26,19 @@ let eta_eq = | C a, C b -> a = b | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2 | _, _ -> false - in aux 0 0 + in aux ;; +let eta_eq = eta_eq' 0 0;; + +(* is arg1 eta-subterm of arg2 ? *) +let eta_subterm u = + let rec aux lev t = eta_eq' lev 0 u t || match t with + | L t -> aux (lev+1) t + | A(t1, t2) -> aux lev t1 || aux lev t2 + | _ -> false + in aux 0 ;; -(* does NOT lift t *) +(* does NOT lift the argument *) let mk_lams = fold_nat (fun x _ -> L x) ;; let string_of_t = @@ -175,7 +184,9 @@ let check p sigma = let freshno = List.fold_right (fun (x,_) -> max x) sigma 0 in let env = Pure.env_of_sigma freshno sigma in assert (Pure.diverged (Pure.mwhd (env,div,[]))); + print_endline " D diverged."; assert (not (Pure.diverged (Pure.mwhd (env,conv,[])))); + print_endline " C converged."; () ;; @@ -184,7 +195,8 @@ let sanity p = if p.conv = B then problem_fail p "p.conv diverged"; if p.div = B then raise (Done p.sigma); if p.phase = `Two && p.div = delta then raise (Done p.sigma); - if not (is_inert p.div) then problem_fail p "p.div converged" + if not (is_inert p.div) then problem_fail p "p.div converged"; + p ;; (* drops the arguments of t after the n-th *) @@ -205,7 +217,7 @@ let find_eta_difference p t n_args = let rec aux t u k = match t, u with | V _, V _ -> assert false (* div subterm of conv *) | A(t1,t2), A(u1,u2) -> - if not (eta_eq t2 u2) then (print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2)); k) + if not (eta_eq t2 u2) then ((*print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2));*) k) else aux t1 u1 (k-1) | _, _ -> assert false in aux p.div t n_args @@ -249,8 +261,9 @@ print_cmd "EAT" ""; | `Two -> p, delta in let subst = var, mk_lams t k in let p = subst_in_problem subst p in + sanity p; let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in - sanity p; p + sanity p ;; (* step on the head of div, on the k-th argument, with n fresh vars *) @@ -267,7 +280,8 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")") let t = mk_lams t (k+1) in (* make leading lambdas *) let subst = var, t in let p = subst_in_problem subst p in - sanity p; p + sanity p +;; ;; let parse strs = @@ -281,23 +295,6 @@ let parse strs = (List.map (aux 0) tms, free) ;; -let problem_of div conv = - print_hline (); - let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in - let varno = List.length var_names in - let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in - (* initial sanity check *) - sanity p; p -;; - -let exec div conv cmds = - let p = problem_of div conv in - try - problem_fail (List.fold_left (|>) p cmds) "Problem not completed" - with - | Done _ -> () -;; - let rec auto p = let hd_var, n_args = get_inert p.div in match get_subterm_with_head_and_args hd_var n_args p.conv with @@ -318,7 +315,30 @@ let rec auto p = auto p ;; -let interactive div conv cmds = +let problem_of div convs = + let rec conv_join = function + | [] -> "@" + | x::xs -> conv_join xs ^ " ("^ x ^")" in + print_hline (); + let conv = conv_join convs in + let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in + let varno = List.length var_names in + let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in + (* initial sanity check *) + sanity p +;; + +let solve p = + if eta_subterm p.div p.conv + then print_endline "!!! div is subterm of conv. Problem was not run !!!" + else check p (auto p) +;; + +let run x y = solve (problem_of x y);; + +(* Example usage of interactive: *) + +(* let interactive div conv cmds = let p = problem_of div conv in try ( let p = List.fold_left (|>) p cmds in @@ -340,40 +360,19 @@ let interactive div conv cmds = | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds) in f p [] ) with Done _ -> () -;; - -let rec conv_join = function - | [] -> "@" - | x::xs -> conv_join xs ^ " ("^ x ^")" -;; - -let auto' a b = - let p = problem_of a (conv_join b) in - let sigma = auto p in - check p sigma -;; +;; *) -(* Example usage of exec, interactive: - -exec - "x x" - (conv_join["x y"; "y y"; "y x"]) - [ step 0 1; eat ] -;; - -interactive "x y" +(* interactive "x y" "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat] -;; +;; *) -*) +run "x x" ["x y"; "y y"; "y x"] ;; +run "x y" ["x (_. x)"; "y z"; "y x"] ;; +run "a (x. x b) (x. x c)" ["a (x. b b) @"; "a @ c"; "a (x. x x) a"; "a (a a a) (a c c)"] ;; -auto' "x x" ["x y"; "y y"; "y x"] ;; -auto' "x y" ["x (_. x)"; "y z"; "y x"] ;; -auto' "a (x. x b) (x. x c)" ["a (x. b b) @"; "a @ c"; "a (x. x x) a"; "a (a a a) (a c c)"] ;; +run "x (y. x y y)" ["x (y. x y x)"] ;; -auto' "x (y. x y y)" ["x (y. x y x)"] ;; - -auto' "x a a a a" [ +run "x a a a a" [ "x b a a a"; "x a b a a"; "x a a b a"; @@ -381,11 +380,10 @@ auto' "x a a a a" [ ] ;; (* Controesempio ad usare un conto dei lambda che non considere le permutazioni *) -auto' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [ +run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [ "x a a a a (_. a) b b b"; "x a a a a (_. _. _. _. x. y. x y)"; ] ;; - print_hline(); -print_endline "ALL DONE. " +print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"