Implemented garbage in Num

- Implemented parsing of garbage
  e.g. (x. x x , A , B , ...) where the garbage is A and B and ...
- Garbage is not implemented in Lambda4, but implemented in Num (except in subst i.e. reduction)
  (see `assert g = []`)
- Added sample problems with garbage

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 83c1b1dab20be45651ca6ead3406f005f173c7b9..d927411a1598dae8d06b599eb4a85deb520bb8e1 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -53,7 +53,7 @@ let measure_of_term, measure_of_terms =
  let rec aux = function
  | `N _ -> 0
  | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
- | `Lam(_,t) -> aux t
+ | `Lam(_,t,g) -> assert (g = []); aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
  | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 then 0 else ar - 1) + aux_many args
  and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
@@ -66,7 +66,7 @@ let count_fakevars p =
  let rec aux = function
  | `N _ -> 0
  | `Var(_,ar) -> if ar = min_int then 1 else 0
- | `Lam(_,t) -> aux t
+ | `Lam(_,t,g) -> assert (g = []); aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
  | `Match(u,v,_,_,args) -> aux (u :> nf) + aux (`Var v) + aux_many args
  and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
@@ -120,7 +120,7 @@ let make_fresh_vars p arities =
 let simple_expand_match ps =
  let rec aux level = function
   | #i_num_var as t -> (aux_i_num_var level t :> nf)
-  | `Lam(b,t) -> `Lam(b,aux (level+1) t)
+  | `Lam(b,t,g) -> assert (g = []); `Lam(b,aux (level+1) t,[])
  and aux_i_num_var level = function
   | `Match(u,v,bs_lift,bs,args) as torig ->
     let (u : i_num_var) = aux_i_num_var level u in
@@ -486,14 +486,14 @@ let instantiate p x n =
  let args = Listx.from_list (vars :> nf list) in
  let bs = ref [] in
  (* 666, since it will be replaced anyway during subst: *)
- let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,-666),1,bs,[])) in
+ let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,-666),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,g) -> assert (g = []); 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))
@@ -501,7 +501,7 @@ let compute_special_k tms =
  | `Var _ -> 0
  ) in
  let rec aux' top t = match t with
- | `Lam(_,t) -> aux' false t
+ | `Lam(_,t,g) -> assert (g = []); aux' false t
  | `I((_,ar), tms) -> max ar
      (Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
  | `Match(t, _, liftno, bs, args) ->
@@ -615,7 +615,7 @@ 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)
+    | `Lam(v,t,g) -> assert (g = []); `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

diff --git a/ocaml/num.ml b/ocaml/num.ml
index dda88a78fe8ddd34253ca7e5f0fe33a36837b327..c1a84b0e35dc57197d8a365a6d1cdf1aa7fbb65a 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -25,7 +25,7 @@ type 'nf i_num_var_ = [
   | 'nf i_n_var_
   | `Match of 'nf i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list
 ]
-type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ | 'nf i_num_var_ ]
+type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ * ('nf nf_) list | 'nf i_num_var_ ]
 type nf = nf nf_
 type i_var = nf i_var_;;
 type i_n_var = nf i_n_var_;;
@@ -61,7 +61,7 @@ let lift m (t : nf) =
  and aux l =
   function
      #i_num_var as x -> (aux_i_num_var l x :> nf)
-   | `Lam(b,nf) -> `Lam (b, aux (l+1) nf)
+   | `Lam(b,nf,g) -> `Lam (b, aux (l+1) nf, List.map (aux (l+1)) g)
  in
   (aux 0 t : nf)
 ;;
@@ -70,7 +70,7 @@ let lift m (t : nf) =
 let rec make_lams t =
  function
    0 -> t
- | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1)))
+ | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1)), [])
  | _ -> assert false
 
 let free_vars' =
@@ -80,7 +80,7 @@ let free_vars' =
   | `I((x,ar),args) ->
       (if x < n then [] else [(x-n,ar)]) @
       List.concat (List.map (aux n) (Listx.to_list args))
-  | `Lam(_,t) -> aux (n+1) t
+  | `Lam(_,t,g) -> List.concat (List.map (aux (n+1)) (t::g))
   | `Match(t,_,liftno,bs,args) ->
       aux n (t :> nf) @
       List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @
@@ -114,7 +114,10 @@ let rec t_of_i_num_var =
 and t_of_nf =
  function
   | #i_num_var as x -> t_of_i_num_var x
-  | `Lam(b,f) -> Pure.L (t_of_nf f)
+  | `Lam(b,f,g) ->
+    let t = t_of_nf (lift (List.length g) f) in
+    let t = List.fold_left (fun t g -> Pure.A(Pure.L t, t_of_nf g)) t g in
+    Pure.L t
 
 end
 
@@ -143,7 +146,8 @@ let string_of_term =
   | `I((n,ar), args) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars lev l) (Listx.to_list args :> nf list))
   | #nf as t -> string_of_term_w_pars lev l t
  and string_of_term_no_pars_lam lev l  = function
-  | `Lam(_,t) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
+  | `Lam(_,t,g) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
+     ^ (if g = [] then "" else String.concat ", " ("" :: List.map (string_of_term_no_pars (lev+1) l) g))
   | _ as t -> string_of_term_no_pars lev l t
  and string_of_term_no_pars lev l = function
   | `Lam _ as t -> string_of_term_no_pars_lam lev l t
@@ -182,7 +186,7 @@ let rec set_arity arity = function
 (* FIXME because onlt variables should be in branches of matches, one day *)
 | `Var(n,_) -> `Var(n,arity)
 | `N _ as t -> t
-| `Lam(false, t) -> `Lam(false, set_arity arity t)
+| `Lam(false, t, []) -> `Lam(false, set_arity arity t, [])
 | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
 | `I _ | `Lam _ -> assert false
 
@@ -193,7 +197,7 @@ let rec mk_app (h : nf) (arg : nf) =
  match h with
     `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
   | `Var v -> `I(v, Listx.Nil arg)
-  | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
+  | `Lam(truelam,nf,g) -> assert (g = []); subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
   | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
   | `N _ -> assert false (* Numbers cannot be applied *)
 (*in let l = ["v0";"v1";"v2"] in
@@ -220,7 +224,7 @@ and mk_match t (n,ar) bs_lift bs args =
 
 and subst truelam delift_by_one what (with_what : nf) (where : nf) =
  let rec aux_propagate_arity ar = function
- | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
+ | `Lam(false,t,g) when not delift_by_one -> assert (g = []); `Lam(false,aux_propagate_arity ar t,[])
  | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
     `Match(`I(v,args),(x,ar),liftno,bs,args')
  | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
@@ -254,7 +258,7 @@ and subst truelam delift_by_one what (with_what : nf) (where : nf) =
 (*function iii -> let res = match iii with*)
   function
    | #i_num_var as x -> aux_i_num_var l x
-   | `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
+   | `Lam(b, nf, g) -> `Lam(b, aux (l+1) nf, List.map (aux (l+1)) g)
 (*in let ll = ["v0";"v1";"v2"] in
 prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*)
  in
@@ -279,9 +283,9 @@ let eta_compare x y =
     clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
   | `Lam _, `N _ -> -1
   | `N _, `Lam _ -> 1
-  | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
-  | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
-  | t2, `Lam(_,t1) ->   aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
+  | `Lam(_,t1,_), `Lam(_,t2,_) -> aux t1 t2
+  | `Lam(_,t1,_), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
+  | t2, `Lam(_,t1,_) ->   aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
   | `N n1, `N n2 -> compare n1 n2
   | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
     let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
@@ -301,7 +305,7 @@ let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
 let rec eta_subterm sub t =
  if eta_eq sub t then true else
   match t with
-  | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
+  | `Lam(_,t,g) -> List.exists (eta_subterm (lift 1 sub)) (t::g)
   | `Match(u,ar,liftno,bs,args) ->
      eta_subterm sub (u :> nf)
      || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
@@ -329,7 +333,7 @@ let max_arity_tms n =
  let rec aux l = function
   | `Var v -> aux_var l v
   | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
-  | `Lam(_,t) -> aux (l+1) t
+  | `Lam(_,t, g) -> List.fold_left (fun n t -> max n (aux (l+1) t)) None (t::g)
   | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
   | `N _ -> None
  and aux_tms l =
@@ -339,7 +343,7 @@ let max_arity_tms n =
 
 let get_first_args var =
 let rec aux l = function
-| `Lam(_,t) -> aux (l+1) t
+| `Lam(_,t,_) -> aux (l+1) t
 | `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
 | `I((n,_), args) -> if n = var + l then [Listx.last args] else []
 | `N _
@@ -352,7 +356,7 @@ let compute_arities m =
   if n = 0
    then []
    else
-    let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in
+    let tms = Util.filter_map (function `Lam(_,t,_) -> Some t | _ -> None ) tms in
     let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
      arity :: (aux (n-1) tms)
  in fun tms -> List.rev (aux m tms)

diff --git a/ocaml/num.mli b/ocaml/num.mli
index f1ea4f843d6ec261f551ee343394077b7e20f8b3..57526a0d9737956718b737b2984fc78061f17636 100644 (file)
--- a/ocaml/num.mli
+++ b/ocaml/num.mli
@@ -8,7 +8,7 @@ type 'nf i_num_var_ =
     | `Var of var ]
 type 'nf nf_ =
     [ `I of var * 'nf Listx.listx
-    | `Lam of bool * 'nf nf_
+    | `Lam of bool * 'nf nf_ * ('nf nf_) list
     | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list
     | `N of int
     | `Var of var ]

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 800322677a102f3aa324df8ddb35ca4daa6afcda..f9e7989176ce0402bf25c056124fa08c0ebe3433 100644 (file)
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -1,7 +1,7 @@
 exception ParsingError of string;;\r
 \r
 let mk_app x y = Num.mk_app x y;;\r
-let mk_lam x = `Lam(true, x);;\r
+let mk_lam x g = `Lam(true, x, g);;\r
 let mk_var x = `Var(x, -666);;\r
 \r
 let isAlphaNum c = let n = Char.code c in\r
@@ -74,18 +74,27 @@ let rec read_smt vars =
     | Some x, cs -> match strip_spaces cs with\r
       | [] -> false\r
       | c::_ -> c = '.'\r
+  in let rec read_garbage (bound, free) = function\r
+  | ',' :: cs ->\r
+     (match read_smt (bound,free) cs with\r
+     | Some [x], cs, (_, free) ->\r
+       let g, cs, free = read_garbage (bound,free) cs in x::g, cs, free\r
+     | _, _, _ -> raise (ParsingError "Garbage expected after ','"))\r
+  | cs -> [], cs, free\r
   in let read_lambda (bound, free) cs = (\r
     match read_var (strip_spaces cs) with\r
       | Some varname, cs ->\r
-      let vars' = (varname::bound, free) in\r
+      let bound' = varname::bound in\r
       (match strip_spaces cs with\r
         | [] -> raise (ParsingError "Lambda expression incomplete")\r
-        | c::cs -> (if c = '.' then (match read_smt vars' cs with\r
+        | '.' :: cs -> (match read_smt (bound', free) cs with\r
           | None, _, _ -> raise (ParsingError "Lambda body expected")\r
-          | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free)\r
+          | Some [t], cs, (_, free) ->\r
+             let g, cs, free = read_garbage (bound', free) (strip_spaces cs) in\r
+             Some [mk_lam t g], cs, (bound, free)\r
           | Some _, _, _ -> assert false\r
-          ) else raise (ParsingError "Expected `.` after variable in lambda")\r
-        ))\r
+          )\r
+        | _::_ -> raise (ParsingError "Expected `.` after variable in lambda"))\r
       | _, _ -> assert false\r
  ) in let rec aux vars cs =\r
   match strip_spaces cs with\r
@@ -93,7 +102,7 @@ let rec read_smt vars =
   | c::_ as x ->\r
       let tms, cs, vars = (\r
            if c = '(' then read_pars vars x\r
-      else if c = ')' then (None, x, vars)\r
+      else if c = ')' || c = ',' then (None, x, vars)\r
       else if check_if_lambda x then read_lambda vars x\r
       else read_var' vars x) in\r
       match tms with\r
@@ -180,7 +189,7 @@ let problem_of_string s =
  let rec aux lev : nf -> nf = function\r
  | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (aux lev) args)\r
  | `Var(n,_) -> fix lev n\r
- | `Lam(_,t) -> `Lam (true, aux (lev+1) t)\r
+ | `Lam(_,t,g) -> `Lam (true, aux (lev+1) t, List.map (aux (lev+1)) g)\r
  | `Match _ | `N _ -> assert false in\r
 let all_tms = List.map (aux 0) (tms :> Num.nf list) in\r
 \r

diff --git a/ocaml/problems/simple.garbage.0 b/ocaml/problems/simple.garbage.0
new file mode 100644 (file)
index 0000000..0382a1b
--- /dev/null
+++ b/ocaml/problems/simple.garbage.0
@@ -0,0 +1,7 @@
+$? check for eta_subterms in garbage\r
+D x a\r
+C x (y. y , x a)\r
+\r
+$! garbage may be `dangerous`\r
+D x @\r
+C @ (y. y, x @, x @)\r

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 274b100b8a57e6ff0740ca07ee97b9d17e601110..16b4e69c9f69e2ef02fea0d61545779657937492 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -383,7 +383,7 @@ let auto p =
 let problem_of (label, div, convs, ps, var_names) =\r
  print_hline ();\r
  let rec aux lev = function\r
- | `Lam(_, t) -> L (aux (lev+1) t, [])\r
+ | `Lam(_, t, g) -> L (aux (lev+1) t, List.map (aux (lev+1)) g)\r
  | `I (v, args) -> Listx.fold_left (fun x y -> fst (mk_app x (aux lev y))) (aux lev (`Var v)) args\r
  | `Var(v,_) -> if v >= lev && List.nth var_names (v-lev) = "C" then C else V v\r
  | `N _ | `Match _ -> assert false in\r