X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fandrea.ml;h=8535988b7c48fc490342951fd68691f460897811;hb=ea2c84fbe45361b8e3e13e5eb54d25854d58cf48;hp=8066a3d79f76e5a845cdaa67de2212afdcf14834;hpb=d1b1a90fbe6cfb7270de165ba0060b888c1e2201;p=fireball-separation.git

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 8066a3d..8535988 100644
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -1,5 +1,6 @@
 let (++) f g x = f (g x);;
 let id x = x;;
+let rec fold_nat f x n = if n = 0 then x else f (fold_nat f x (n-1)) n ;;
 
 let print_hline = Console.print_hline;;
 
@@ -9,7 +10,6 @@ type t =
  | A of t * t
  | L of t
  | B (* bottom *)
- | P (* pacman *)
 ;;
 
 let eta_eq =
@@ -23,49 +23,50 @@ let eta_eq =
  in aux 0 0
 ;;
 
-type problem = {
-   orig_freshno: int
- ; freshno : int
- ; div : t
- ; conv : t
- ; sigma : (var * t) list (* substitutions *)
- ; stepped : var list
-}
+(* does NOT lift t *)
+let mk_lams = fold_nat (fun x _ -> L x) ;;
 
-exception Done of (var * t) list (* substitution *);;
-exception Fail of int * string;;
-
-let string_of_t p =
-  let bound_vars = ["x"; "y"; "z"; "w"; "q"] in
+let string_of_t =
+  let string_of_bvar =
+   let bound_vars = ["x"; "y"; "z"; "w"; "q"] in
+   let bvarsno = List.length bound_vars in
+   fun nn -> if nn < bvarsno then List.nth bound_vars nn else "x" ^ (string_of_int (nn - bvarsno + 1)) in
   let rec string_of_term_w_pars level = function
     | V v -> if v >= level then "`" ^ string_of_int (v-level) else
-     let nn = level - v-1 in
-      if nn < 5 then List.nth bound_vars nn else "x" ^ (string_of_int (nn-4))
+       string_of_bvar (level - v-1)
     | A _
-    | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"
+    | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"
     | B -> "BOT"
-    | P -> "PAC"
   and string_of_term_no_pars_app level = function
-    | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)
+    | A(t1,t2) -> string_of_term_no_pars_app level t1 ^ " " ^ string_of_term_w_pars level t2
     | _ as t -> string_of_term_w_pars level t
-  and string_of_term_no_pars_lam level = function
-    | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)
-    | _ as t -> string_of_term_no_pars level t
   and string_of_term_no_pars level = function
-    | L _ as t -> string_of_term_no_pars_lam level t
+    | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t
     | _ as t -> string_of_term_no_pars_app level t
   in string_of_term_no_pars 0
 ;;
 
+type problem = {
+   orig_freshno: int
+ ; freshno : int
+ ; div : t
+ ; conv : t
+ ; sigma : (var * t) list (* substitutions *)
+ ; stepped : var list
+}
+
 let string_of_problem p =
  let lines = [
   "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);
-  "[DV] " ^ (string_of_t p p.div);
-  "[CV] " ^ (string_of_t p p.conv);
+  "[DV] " ^ string_of_t p.div;
+  "[CV] " ^ string_of_t p.conv;
  ] in
  String.concat "\n" lines
 ;;
 
+exception Done of (var * t) list (* substitution *);;
+exception Fail of int * string;;
+
 let problem_fail p reason =
  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";
  print_endline (string_of_problem p);
@@ -80,86 +81,75 @@ let rec is_inert =
  function
  | A(t,_) -> is_inert t
  | V _ -> true
- | L _ | B | P -> false
+ | L _ | B -> false
 ;;
 
 let is_var = function V _ -> true | _ -> false;;
 let is_lambda = function L _ -> true | _ -> false;;
 
-let rec head_of_inert = function
- | V n -> n
- | A(t, _) -> head_of_inert t
- | _ -> assert false
+let rec no_leading_lambdas = function
+ | L t -> 1 + no_leading_lambdas t
+ | _ -> 0
 ;;
 
-let rec args_no = function
- | V _ -> 0
- | A(t, _) -> 1 + args_no t
+let rec get_inert = function
+ | V n -> (n,0)
+ | A(t, _) -> let hd,args = get_inert t in hd,args+1
  | _ -> assert false
 ;;
 
-let rec subst level delift fromdiv sub =
+let rec subst level delift sub =
  function
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)
- | L t -> L (subst (level + 1) delift fromdiv sub t)
+ | L t -> L (subst (level + 1) delift sub t)
  | A (t1,t2) ->
-  let t1 = subst level delift fromdiv sub t1 in
-  let t2 = subst level delift fromdiv sub t2 in
-  if t1 = B || t2 = B then B else mk_app fromdiv t1 t2
+  let t1 = subst level delift sub t1 in
+  let t2 = subst level delift sub t2 in
+  mk_app t1 t2
  | B -> B
- | P -> P
-and mk_app fromdiv t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with
+and mk_app t1 t2 = match t1 with
  | B | _ when t2 = B -> B
- | L t1 -> subst 0 true fromdiv (0, t2) t1
+ | L t1 -> subst 0 true (0, t2) t1
  | t1 -> A (t1, t2)
 and lift n =
- let rec aux n' =
+ let rec aux lev =
   function
-  | V m -> V (if m >= n' then m + n else m)
-  | L t -> L (aux (n'+1) t)
-  | A (t1, t2) -> A (aux n' t1, aux n' t2)
+  | V m -> V (if m >= lev then m + n else m)
+  | L t -> L (aux (lev+1) t)
+  | A (t1, t2) -> A (aux lev t1, aux lev t2)
   | B -> B
-  | P -> P
  in aux 0
 ;;
 let subst = subst 0 false;;
 
 let subst_in_problem (sub: var * t) (p: problem) =
-print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));
- let p = {p with stepped=(fst sub)::p.stepped} in
- let conv = subst false sub p.conv in
- let div = subst true sub p.div in
- let p = {p with div; conv} in
- (* print_endline ("after sub: \n" ^ string_of_problem p); *)
- {p with sigma=sub::p.sigma}
+print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));
+ {p with
+  div=subst sub p.div;
+  conv=subst sub p.conv;
+  stepped=(fst sub)::p.stepped;
+  sigma=sub::p.sigma}
 ;;
 
 let get_subterm_with_head_and_args hd_var n_args =
- let rec aux = function
- | V _ | L _ | B | P -> None
+ let rec aux lev = function
+ | V _ | B -> None
+ | L t -> aux (lev+1) t
  | A(t1,t2) as t ->
-   if head_of_inert t1 = hd_var && n_args <= 1 + args_no t1
-    then Some t
-    else match aux t2 with
-    | None -> aux t1
+   let hd_var', n_args' = get_inert t1 in
+   if hd_var' = hd_var + lev && n_args <= 1 + n_args'
+    then Some (lift ~-lev t)
+    else match aux lev t2 with
+    | None -> aux lev t1
     | Some _ as res -> res
- in aux
+ in aux 0
 ;;
 
-(* let rec simple_explode p =
- match p.div with
- | V var ->
-  let subst = var, B in
-  sanity (subst_in_problem subst p)
- | _ -> p *)
-
 let sanity p =
  print_endline (string_of_problem p); (* non cancellare *)
- if p.div = B then raise (Done p.sigma);
- if not (is_inert p.div) then problem_fail p "p.div converged";
  if p.conv = B then problem_fail p "p.conv diverged";
- (* let p = if is_var p.div then simple_explode p else p in *)
- p
+ if p.div = B then raise (Done p.sigma);
+ if not (is_inert p.div) then problem_fail p "p.div converged"
 ;;
 
 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
@@ -168,68 +158,47 @@ let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
  It does NOT perform any check, may fail if done unsafely *)
 let eat p =
 print_cmd "EAT" "";
- let var = head_of_inert p.div in
- let n = args_no p.div in
- let rec aux m t =
-  if m = 0
-   then lift n t
-   else L (aux (m-1) t) in
- let subst = var, aux n B in
- sanity (subst_in_problem subst p)
+ let var, n = get_inert p.div in
+ let subst = var, mk_lams B n in
+ let p = subst_in_problem subst p in
+ sanity p; p
 ;;
 
 (* step on the head of div, on the k-th argument, with n fresh vars *)
 let step k n p =
- let var = head_of_inert p.div in
- print_cmd "STEP" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");
- let rec aux' p m t =
-  if m < 0
-   then p, t
-    else
-     let p, v = freshvar p in
-     let p, t = aux' p (m-1) t in
-      p, A(t, V (v + k + 1)) in
- let p, t = aux' p n (V 0) in
- let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (k-m)) in
- let rec aux m t =
-  if m < 0
-   then aux' (k-1) t
-   else L (aux (m-1) t) in
- let t = aux k t in
+ let var, _ = get_inert p.div in
+print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");
+ let p, t = (* apply fresh vars *)
+  fold_nat (fun (p, t) _ ->
+    let p, v = freshvar p in
+    p, A(t, V (v + k + 1))
+  ) (p, V 0) n in
+ let t = (* apply unused bound variables V_{k-1}..V_1 *)
+  fold_nat (fun t m -> A(t, V (k-m+1))) t k in
+ let t = mk_lams t (k+1) in (* make leading lambdas *)
  let subst = var, t in
- sanity (subst_in_problem subst p)
+ let p = subst_in_problem subst p in
+ sanity p; p
 ;;
 
 let parse strs =
   let rec aux level = function
   | Parser_andrea.Lam t -> L (aux (level + 1) t)
   | Parser_andrea.App (t1, t2) ->
-   if level = 0 then mk_app false (aux level t1) (aux level t2)
+   if level = 0 then mk_app (aux level t1) (aux level t2)
     else A(aux level t1, aux level t2)
-  | Parser_andrea.Var v -> V v
-  in let (tms, free) = Parser_andrea.parse_many strs
-  in (List.map (aux 0) tms, free)
+  | Parser_andrea.Var v -> V v in
+  let (tms, free) = Parser_andrea.parse_many strs in
+  (List.map (aux 0) tms, free)
 ;;
 
 let problem_of div conv =
  print_hline ();
- let all_tms, var_names = parse ([div; conv]) in
- let div, conv = List.hd all_tms, List.hd (List.tl all_tms) 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=[]} in
- (* activate bombs *)
- let p = try
-  let subst = Util.index_of "BOMB" var_names, L B in
-   subst_in_problem subst p
-  with Not_found -> p in
- (* activate pacmans *)
- let p = try
-  let subst = Util.index_of "PACMAN" var_names, P in
-   let p = subst_in_problem subst p in
-   (print_endline ("after subst in problem " ^ string_of_problem p); p)
-  with Not_found -> p in
  (* initial sanity check *)
- sanity p
+ sanity p; p
 ;;
 
 let exec div conv cmds =
@@ -240,6 +209,7 @@ let exec div conv cmds =
  | Done _ -> ()
 ;;
 
+(* drops the arguments of t after the n-th *)
 let inert_cut_at n t =
  let rec aux t =
   match t with
@@ -257,24 +227,19 @@ 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 p t2) ^ " <> " ^ (string_of_t p 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
 ;;
 
-let rec no_leading_lambdas = function
- | L t -> 1 + no_leading_lambdas t
- | _ -> 0
-;;
-
 let compute_max_lambdas_at hd_var j =
  let rec aux hd = function
  | A(t1,t2) ->
-    (if head_of_inert t1 = hd && args_no t1 = j
-      then max (
-       if is_inert t2 && head_of_inert t2 = hd
-        then j - args_no t2
+    (if get_inert t1 = (hd, j)
+      then max ( (*FIXME*)
+       if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd
+        then let hd', j' = get_inert t2 in j - j'
         else no_leading_lambdas t2)
       else id) (max (aux hd t1) (aux hd t2))
  | L t -> aux (hd+1) t
@@ -284,14 +249,13 @@ let compute_max_lambdas_at hd_var j =
 ;;
 
 let rec auto p =
- let hd_var = head_of_inert p.div in
- let n_args = args_no p.div in
+ let hd_var, n_args = get_inert p.div in
  match get_subterm_with_head_and_args hd_var n_args p.conv with
  | None ->
-    (try let p = eat p in problem_fail p "Auto did not complete the problem"  with Done _ -> ())
+    (try problem_fail (eat p) "Auto did not complete the problem"  with Done _ -> ())
  | Some t ->
   let j = find_eta_difference p t n_args - 1 in
-  let k = max
+  let k = 1 + max
    (compute_max_lambdas_at hd_var j p.div)
     (compute_max_lambdas_at hd_var j p.conv) in
   let p = step j k p in
@@ -334,11 +298,11 @@ let auto' a b = auto (problem_of a (conv_join b));;
 exec
  "x x"
  (conv_join["x y"; "y y"; "y x"])
- [ step 0 0; eat ]
+ [ step 0 1; eat ]
 ;;
 
 interactive "x y"
- "@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat]
+ "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]
 ;;
 
 *)