From: acondolu Date: Sun, 10 Jun 2018 11:37:51 +0000 (+0200) Subject: Implemented garbage in Num X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0197354468e40860a3a104b9ea5b68854a22cfca;p=fireball-separation.git 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 83c1b1d..d927411 100644 --- 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 dda88a7..c1a84b0 100644 --- 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 f1ea4f8..57526a0 100644 --- 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 8003226..f9e7989 100644 --- a/ocaml/parser.ml +++ b/ocaml/parser.ml @@ -1,7 +1,7 @@ exception ParsingError of string;; let mk_app x y = Num.mk_app x y;; -let mk_lam x = `Lam(true, x);; +let mk_lam x g = `Lam(true, x, g);; let mk_var x = `Var(x, -666);; let isAlphaNum c = let n = Char.code c in @@ -74,18 +74,27 @@ let rec read_smt vars = | Some x, cs -> match strip_spaces cs with | [] -> false | c::_ -> c = '.' + in let rec read_garbage (bound, free) = function + | ',' :: cs -> + (match read_smt (bound,free) cs with + | Some [x], cs, (_, free) -> + let g, cs, free = read_garbage (bound,free) cs in x::g, cs, free + | _, _, _ -> raise (ParsingError "Garbage expected after ','")) + | cs -> [], cs, free in let read_lambda (bound, free) cs = ( match read_var (strip_spaces cs) with | Some varname, cs -> - let vars' = (varname::bound, free) in + let bound' = varname::bound in (match strip_spaces cs with | [] -> raise (ParsingError "Lambda expression incomplete") - | c::cs -> (if c = '.' then (match read_smt vars' cs with + | '.' :: cs -> (match read_smt (bound', free) cs with | None, _, _ -> raise (ParsingError "Lambda body expected") - | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free) + | Some [t], cs, (_, free) -> + let g, cs, free = read_garbage (bound', free) (strip_spaces cs) in + Some [mk_lam t g], cs, (bound, free) | Some _, _, _ -> assert false - ) else raise (ParsingError "Expected `.` after variable in lambda") - )) + ) + | _::_ -> raise (ParsingError "Expected `.` after variable in lambda")) | _, _ -> assert false ) in let rec aux vars cs = match strip_spaces cs with @@ -93,7 +102,7 @@ let rec read_smt vars = | c::_ as x -> let tms, cs, vars = ( if c = '(' then read_pars vars x - else if c = ')' then (None, x, vars) + else if c = ')' || c = ',' then (None, x, vars) else if check_if_lambda x then read_lambda vars x else read_var' vars x) in match tms with @@ -180,7 +189,7 @@ let problem_of_string s = let rec aux lev : nf -> nf = function | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (aux lev) args) | `Var(n,_) -> fix lev n - | `Lam(_,t) -> `Lam (true, aux (lev+1) t) + | `Lam(_,t,g) -> `Lam (true, aux (lev+1) t, List.map (aux (lev+1)) g) | `Match _ | `N _ -> assert false in let all_tms = List.map (aux 0) (tms :> Num.nf list) in diff --git a/ocaml/problems/simple.garbage.0 b/ocaml/problems/simple.garbage.0 new file mode 100644 index 0000000..0382a1b --- /dev/null +++ b/ocaml/problems/simple.garbage.0 @@ -0,0 +1,7 @@ +$? check for eta_subterms in garbage +D x a +C x (y. y , x a) + +$! garbage may be `dangerous` +D x @ +C @ (y. y, x @, x @) diff --git a/ocaml/simple.ml b/ocaml/simple.ml index 274b100..16b4e69 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -383,7 +383,7 @@ let auto p = let problem_of (label, div, convs, ps, var_names) = print_hline (); let rec aux lev = function - | `Lam(_, t) -> L (aux (lev+1) t, []) + | `Lam(_, t, g) -> L (aux (lev+1) t, List.map (aux (lev+1)) g) | `I (v, args) -> Listx.fold_left (fun x y -> fst (mk_app x (aux lev y))) (aux lev (`Var v)) args | `Var(v,_) -> if v >= lev && List.nth var_names (v-lev) = "C" then C else V v | `N _ | `Match _ -> assert false in