Removed bomb variable

In Pure:
- Added constructor B to Pure.t
- Added rule corresponding to B (bottom) in Pure.mwhd
In Lambda4:
- Instantiating the bomb now actually uses subst_in_problem
- Two new exceptions: Bottom and Pacman
- Fixed subst_in_problem by making expand_match raise these two exceptions,
  which are caught when tolerated

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 112f7deb7c5edc7d0951802b700649c717c6c87b..db743ffebb4df474e6b4a4ef91d5209efac7a9a4 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -3,8 +3,6 @@ open Util.Vars
 open Pure
 open Num
 
-let bomb = ref(`Var(-1,-666));;
-
 (*
  The number of arguments which can applied to numbers
  safely, depending on the encoding of numbers.
@@ -26,6 +24,9 @@ type problem =
  ; trail: discriminating_set list list
 };;
 
+(* exceptions *)
+exception Pacman
+exception Bottom
 exception Backtrack of string
 
 let first bound p var f =
@@ -34,10 +35,10 @@ let first bound p var f =
   if i > bound then
    raise (Backtrack ("no more alternatives for " ^ string_of_var var))
   else
-   try
-     f p i
-   with
-    Backtrack s ->
+   try(try
+    f p i
+   with Pacman | Bottom -> raise (Backtrack "Pacman/Bottom"))
+   with Backtrack s ->
 prerr_endline ("!!BACKTRACK!! " ^ s);
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
 prerr_endline("Now trying var="^string_of_var var^" i="^string_of_int i);
@@ -159,7 +160,7 @@ let subst_in_problem x inst ({freshno; div; conv; ps; sigma} as p) =
  let len_ps = List.length ps in
 (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
 prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
- let rec aux ((freshno,acc_ps,acc_new_ps) as acc) =
+ let rec aux_ps ((freshno,acc_ps,acc_new_ps) as acc) =
   function
   | [] -> acc
   | t::todo_ps ->
@@ -169,31 +170,31 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
      let freshno,new_t,acc_new_ps =
       expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t
      in
-      aux (freshno,acc_ps@[new_t],acc_new_ps) todo_ps
+      aux_ps (freshno,acc_ps@[new_t],acc_new_ps) todo_ps
 
   (* cut&paste from aux above *)
-  and aux' ps ((freshno,acc_conv,acc_new_ps) as acc) =
+  and aux_conv ps ((freshno,acc_conv,acc_new_ps) as acc) =
    function
    | [] -> acc
    | t::todo_conv ->
-(*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
-       let t = subst false false x inst (t :> nf) in
+   (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
+      let t = try
+       subst false false x inst (t :> nf)
+      with Pacman -> `N(-1) in (* DUMMY CONVERGENT *)
 (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
-       let freshno,new_t,acc_new_ps =
-        expand_match (freshno,ps,acc_new_ps) t
-       in
-        aux' ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
+      let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in
+      aux_conv ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
 
   (* cut&paste from aux' above *)
-  and aux'' ps (freshno,acc_new_ps) =
+  and aux_div ps (freshno,acc_new_ps) =
    function
    | None -> freshno, None, acc_new_ps
    | Some t ->
-      let t = subst false false x inst (t :> nf) in
-      let freshno,new_t,acc_new_ps =
-       expand_match (freshno,ps,acc_new_ps) t
-      in
-       freshno,Some new_t,acc_new_ps
+      try
+       let t = subst false false x inst (t :> nf) in
+       let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in
+        freshno,Some(cast_to_i_var new_t),acc_new_ps
+      with Bottom -> freshno, None, acc_new_ps
 
   and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t =
    match t with
@@ -224,15 +225,16 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
 (*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 _ -> assert false (* algorithm invariant/loose typing *)
-   | `Bottom | `Pacman -> raise (Backtrack "BOT or PAC in toplevel numeric positioon")
+   | `Bottom -> raise Bottom
+   | `Pacman -> raise Pacman
    | #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 freshno,conv,new_ps = aux' old_ps (freshno,[],new_ps) (conv :> i_num_var list) in
- let freshno,div,new_ps = aux'' old_ps (freshno,new_ps) (div :> i_num_var option) in
- let div = option_map cast_to_i_var div in
+ let freshno,old_ps,new_ps = aux_ps (freshno,[],[]) (ps :> i_num_var list) in
+ let freshno,conv,new_ps = aux_conv old_ps (freshno,[],new_ps) (conv :> i_num_var list) in
+ let freshno,div,new_ps = aux_div old_ps (freshno,new_ps) (div :> i_num_var option) in
+
  let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in
  let conv = List.map cast_to_i_n_var conv in
 (let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
@@ -428,20 +430,10 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var x ^ " := " ^ print ~l inst));
    then p
    else
     let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in
-    let p, bomb' = make_fresh_var p (-666) in
-    (if !bomb <> `Var (-1,-666) then
-     failwithProblem p
-      ("Bomb was duplicated! It was " ^ string_of_nf !bomb ^
-       ", tried to change it to " ^ string_of_nf bomb'));
-    bomb := bomb';
-    prerr_endline ("Just created bomb var: " ^ string_of_nf !bomb);
     let x = hd_of_i_var div in
-    let inst = make_lams !bomb n in
-    prerr_endline ("# INST (div): " ^ string_of_var x ^ " := " ^ string_of_nf inst);
-    let p = {p with div=None} in
-    (* subst_in_problem (hd_of_i_var div) inst p in *)
-     {p with sigma=p.sigma@[x,inst]} in
-     let dangerous_conv = showstoppers_conv in
+    let inst = make_lams `Bottom n in
+    subst_in_problem x inst p in
+ let dangerous_conv = showstoppers_conv in
 let _ = prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
 List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))) dangerous_conv; in
  let conv =
@@ -477,8 +469,6 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))
   `Continue p
 
 let instantiate p x perm n =
- (if hd_of_i_var (cast_to_i_var !bomb) = x
-   then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!"));
  let arity_of_x = max_arity_tms x (all_terms p) in
  (if arity_of_x = None then failwithProblem p "step on var non occurring in problem");
  let arity_of_x = Util.option_get(arity_of_x) in
@@ -668,7 +658,7 @@ let optimize_numerals p =
   replace_in_sigma (List.rev perm) p.sigma
 ;;
 
-let env_of_sigma freshno sigma should_explode =
+let env_of_sigma freshno sigma =
  let rec aux n =
   if n > freshno then
    []
@@ -677,10 +667,7 @@ let env_of_sigma freshno sigma should_explode =
    (try
     e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
    with
-    Not_found ->
-     if should_explode && n = hd_of_i_var (cast_to_i_var !bomb)
-      then ([], (let f t = Pure.A(t,t) in f (Pure.L (f (Pure.V 0)))), [])
-      else ([],Pure.V n,[]))::e
+    Not_found -> ([],Pure.V n,[]))::e
  in aux 0
 ;;
 
@@ -718,14 +705,12 @@ let main problems =
   List.iter
    (fun (p,n,cmds) ->
     Console.print_hline();
-    bomb := `Var (-1,-666);
     let p_finale = aux p n cmds in
     let freshno,sigma = p_finale.freshno, p_finale.sigma in
     prerr_endline ("------- <DONE> ------\n ");
     (* prerr_endline (string_of_problem "Original problem" p); *)
     prerr_endline "---------------------";
     let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
-    prerr_endline (" BOMB == " ^ print ~l !bomb);
     prerr_endline "---------------------";
     List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
 (*
@@ -744,14 +729,13 @@ let main problems =
     let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
     List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
     prerr_endline "---------<PURE>---------";
+
     let div = option_map (fun div -> ToScott.scott_of_nf (div :> nf)) p.div in
     let conv = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.conv in
     let ps = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.ps in
-    let sigma = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in
-    (*let ps_ok = List.fold_left (fun ps (x,inst) ->
-      List.map (Pure.subst false x inst) ps) ps sigma in*)
-    let e = env_of_sigma freshno sigma true in
-    let e' = env_of_sigma freshno sigma false in
+
+    let sigma' = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in
+    let e' = env_of_sigma freshno sigma' in
 
 (*
      prerr_endline "---------<PPP>---------";
@@ -769,17 +753,16 @@ in
       print_endline (Pure.print div);
       let t = Pure.mwhd (e',div,[]) in
       prerr_endline ("*:: " ^ (Pure.print t));
-      prerr_endline (print !bomb);
-      assert (t = ToScott.scott_of_nf (!bomb:>nf))
+      assert (t = Pure.B)
      | None -> ()) div;
      List.iter (fun n ->
        prerr_endline ("_::: " ^ (Pure.print n));
-       let t = Pure.mwhd (e,n,[]) in
+       let t = Pure.mwhd (e',n,[]) in
        prerr_endline ("_:: " ^ (Pure.print t))
      ) conv ;
      List.iteri (fun i n ->
        prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n));
-       let t = Pure.mwhd (e,n,[]) in
+       let t = Pure.mwhd (e',n,[]) in
        prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t));
        assert (t = Scott.mk_n i)
      ) ps ;

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 57cb19d068dee18d7df1cc070bc99cf448513e38..443dcdc0272c75fd4806ca18d255e413e008c502 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -99,19 +99,18 @@ let free_vars = (List.map fst) ++ free_vars';;
 module ToScott =
 struct
 
-let rec scott_of_nf =
- function
-  | `N n -> Scott.mk_n n
-  | `Var(v,_) -> Pure.V v
-  | `Match(t,_,liftno,bs,args) ->
-      let bs = List.map (fun (n,t) -> n, scott_of_nf (lift liftno (t :> nf))) !bs in
-      let t = scott_of_nf (t :> nf) in
-      let m = Scott.mk_match t bs in
-      List.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) m (args :> nf list)
-  | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) (Pure.V v) (args :> nf Listx.listx)
-  | `Lam(b,f) -> Pure.L (scott_of_nf f)
-  | `Bottom -> let f x = Pure.A (x,x) in f (Pure.L (f (Pure.V 0)))
-  | `Pacman -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0))))
+let rec scott_of_nf = function
+ | `N n -> Scott.mk_n n
+ | `Var(v,_) -> Pure.V v
+ | `Match(t,_,liftno,bs,args) ->
+ let bs = List.map (fun (n,t) -> n, scott_of_nf (lift liftno (t :> nf))) !bs in
+     let t = scott_of_nf (t :> nf) in
+     let m = Scott.mk_match t bs in
+     List.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) m (args :> nf list)
+ | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) (Pure.V v) (args :> nf Listx.listx)
+ | `Lam(_,t) -> Pure.L (scott_of_nf t)
+ | `Bottom -> Pure.B
+ | `Pacman -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0))))
 end
 
 

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 78c6c4cbcbdbb5ae05e179eb85fe8b1145f500a7..95dae1513d166833d6ba2fd69868b86e7c1a2ee7 100644 (file)
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -7,6 +7,7 @@ type t =
   | V of int
   | A of t * t
   | L of t
+  | B
 
 let rec print ?(l=[]) =
  function
@@ -15,6 +16,7 @@ let rec print ?(l=[]) =
   | L t ->
      let name = string_of_var (List.length l) in
      "λ" ^ name ^ "." ^ print ~l:(name::l) t
+  | B -> "B"
 
 let lift m =
  let rec aux l =
@@ -22,6 +24,7 @@ let lift m =
    | V n -> V (if n < l then n else n+m)
    | A (t1,t2) -> A (aux l t1, aux l t2)
    | L t -> L (aux (l+1) t)
+   | B -> B
  in
   aux 0
 
@@ -72,7 +75,8 @@ let unwind ?(tbl = Hashtbl.create 317) m =
        (try
          lift l (cache_unwind (List.nth e (n - l)))
         with Failure _ -> V (n - l))
-    | L t -> L (aux (l+1) t) in
+    | L t -> L (aux (l+1) t)
+    | B -> B in
   let t = aux 0 t in
   List.fold_left (fun f a -> A(f,a)) t s
 in
@@ -81,15 +85,19 @@ in
 let mwhd m =
  let rec aux =
   function
-     (e,A(t1,t2),s) ->
+   | (e,A(t1,t2),s) ->
        let t2' = aux (e,t2,[]) in
-       aux (e,t1,t2'::s)
+       let (_,t,_) = t2' in
+       if t = B
+        then t2'
+        else aux (e,t1,t2'::s)
    | (e,L t,x::s) -> aux (x::e,t,s)
    | (e,V n,s) as m ->
       (try
         let e,t,s' = List.nth e n in
         aux (e,t,s'@s)
        with Failure _ -> m)
+   | (e, B, _) -> (e, B, [])
    | (_,L _,[]) as m -> m
  in
   unwind (aux m)

diff --git a/ocaml/pure.mli b/ocaml/pure.mli
index f36007498ca1556eeb20708641560cef3b725cc3..a6b90acf7e16c6be71967352756223cbefb70f6d 100644 (file)
--- a/ocaml/pure.mli
+++ b/ocaml/pure.mli
@@ -1,6 +1,6 @@
 module Pure :
   sig
-    type t = V of int | A of t * t | L of t
+    type t = V of int | A of t * t | L of t | B
     val print : ?l:string list -> t -> string
     val lift : int -> t -> t
     val unwind : ?tbl:('a list * t * 'a list as 'a, t) Hashtbl.t -> 'a -> t