From: acondolu Date: Fri, 15 Sep 2017 14:50:46 +0000 (+0200) Subject: Ultime modifiche. Andrea scappa all'estero. Au revoir X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5ca40d685df1319e8f2b7fd2464c6c99da9b0c98;p=fireball-separation.git Ultime modifiche. Andrea scappa all'estero. Au revoir --- diff --git a/ocaml_new/lambda4.ml b/ocaml_new/lambda4.ml index 08b7154..c5fe724 100644 --- a/ocaml_new/lambda4.ml +++ b/ocaml_new/lambda4.ml @@ -47,14 +47,14 @@ let first args p var f = with Backtrack s -> prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ "); (* prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1)); *) - if k = 0 then aux p.initialSpecialK is else aux (k-1) ii + if k = 0 || true then aux p.initialSpecialK is else aux (k-1) ii in aux p.initialSpecialK args let all_terms p = p.div :: p.conv ;; let measure_of_term, measure_of_terms = let rec aux = function - | `Bottom | `Pacman -> 0 + | `Bottom | `Pacman _ -> 0 | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*) | `Lam(_,t) -> aux t | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list) @@ -109,9 +109,10 @@ let subst_in_problem x inst ({div; conv} as p) = prerr_endline ("# INST0: " ^ string_of_var p.var_names x ^ " := " ^ string_of_term p inst); let div = subst false false x inst (div :> nf) in let conv = List.map (subst false false x inst) (conv :> nf list) in - let conv = Util.filter_map (function `Lam _ | `Pacman -> None | `Bottom -> raise (Backtrack "bottom in conv") | #i_var as t -> Some t) conv in + let conv = List.concat (Util.filter_map (function + | `Lam _ -> None | `Pacman ts -> Some ts | `Bottom -> raise (Backtrack "bottom in conv") | #i_var as t -> Some [t]) conv) in match div with - | `Lam _ | `Pacman | `Var _ -> raise (Backtrack "lam in div") + | `Lam _ | `Pacman _ | `Var _ -> raise (Backtrack "lam in div") | `Bottom -> `Finished p | `I _ as div -> `Continue {p with div; conv} ;; @@ -378,7 +379,7 @@ let compute_special_k tms = | `Lam(b,t) -> aux (k + if b then 1 else 0) t | `I(n, tms) -> Listx.max (Listx.map (aux 0) (tms :> nf Listx.listx)) | `Bottom - | `Pacman + | `Pacman _ | `Var _ -> 0 ) in let rec aux' top t = match t with @@ -386,7 +387,7 @@ let compute_special_k tms = | `I((_,ar), tms) -> max ar (Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx))) | `Bottom - | `Pacman + | `Pacman _ | `Var _ -> 0 in Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms) ;; @@ -431,7 +432,8 @@ let eat p = let hd, args, n = match p.div with `Var _ -> assert false | `I((x,_), l) -> x, l, Listx.length l in let rec aux = function | `Var _ | `Lam _ -> () - | `Pacman | `Bottom -> assert false + | `Pacman ts -> List.iter aux (ts :> nf list) + | `Bottom -> () | `I((x,_),args') -> if x = hd then if Listx.length args' >= n then @@ -543,7 +545,7 @@ let solve (p, todo) = let no_bombs_pacmans p = not (List.exists (eta_subterm `Bottom) p.conv) - && not (eta_subterm `Pacman p.div) + && not (eta_subterm (`Pacman[]) p.div) ;; let check p = diff --git a/ocaml_new/num.ml b/ocaml_new/num.ml index f6b9405..1e69d29 100644 --- a/ocaml_new/num.ml +++ b/ocaml_new/num.ml @@ -20,7 +20,7 @@ and i = ;;*) type var = int * (* arity of variable*) int;; type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ] -type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman | ('nf nf_nob_) i_var_ ] +type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman of (('nf nf_nob_) i_var_) list | ('nf nf_nob_) i_var_ ] type nf = [ nf nf_nob_ | `Bottom ] type nf_nob = nf nf_nob_ type i_var = nf_nob i_var_;; @@ -51,7 +51,7 @@ let lift m (t : nf) = function #i_var as x -> (aux_i_num_var l x :> nf_nob) | `Lam(b,nf) -> `Lam (b, aux (l+1) nf) - | `Pacman -> `Pacman + | `Pacman ts -> `Pacman(List.map (aux_i_num_var l) ts) and aux l = function #nf_nob as x -> (aux_nob l x :> nf) @@ -74,7 +74,8 @@ let free_vars' = (if x < n then [] else [(x-n,ar)]) @ List.concat (List.map (aux n) (Listx.to_list args :> nf list)) | `Lam(_,t) -> aux (n+1) t - | `Bottom | `Pacman -> [] + | `Bottom -> [] + | `Pacman _ -> assert false in aux 0 ;; let free_vars = (List.map fst) ++ free_vars';; @@ -87,7 +88,7 @@ let rec scott_of_nf = function | `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)))) + | `Pacman _ -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0)))) end @@ -107,7 +108,7 @@ let rec string_of_term = | `Lam(_,`Bottom) -> "BOMB" | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")" | `Bottom -> "BOT" - | `Pacman -> "PAC" + | `Pacman _ -> "PAC" and string_of_term_no_pars_app lev l = function | `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 @@ -137,7 +138,7 @@ let cast_to_i_var = let rec set_arity arity = function (* FIXME because onlt variables should be in branches of matches, one day *) | `Var(n,_) -> `Var(n,arity) -| `Bottom | `Pacman as t -> (t : nf) +| `Bottom | `Pacman _ as t -> (t : nf) | `Lam(false, t) -> `Lam(false, set_arity arity (t :> nf)) | `I _ | `Lam _ -> assert false @@ -151,7 +152,8 @@ let rec mk_app (h : nf) (arg : nf) = | `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 *) - | `Bottom | `Pacman as t -> t + | `Bottom -> `Bottom + | `Pacman ts as t -> match arg with #i_var as u -> `Pacman(u::ts) | _ -> t (*in let l = ["v0";"v1";"v2"] in prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*) @@ -165,7 +167,7 @@ and mk_appx h args = Listx.fold_left mk_app h args and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) = let rec aux_propagate_arity ar = function | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t) - | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar) + | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int || true); ar) else oldar) | _ as t -> t in let rec aux_i_var l = function @@ -186,7 +188,7 @@ and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) = | #i_var as x -> aux_i_var l x | `Lam(b, nf) -> `Lam(b, aux (l+1) nf) | `Bottom -> `Bottom - | `Pacman -> `Pacman + | `Pacman ts -> `Pacman(Util.filter_map (fun x -> match aux_i_var l x with #i_var as u -> Some u | _ -> None) ts) (*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 @@ -212,7 +214,7 @@ let eta_compare x y = | `I((n1,_), l1), `I((n2,_), l2) -> clex compare (lex aux) (n1, (Listx.to_list l1 :> nf list)) (n2, (Listx.to_list l2 :> nf list)) | `Bottom, `Bottom - | `Pacman, `Pacman -> 0 + | `Pacman _, `Pacman _ -> 0 | `Bottom, `Lam(_,t) -> -1 | `Lam(_,t), `Bottom -> 1 | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2 @@ -222,8 +224,8 @@ let eta_compare x y = | _, `I _ -> 1 | `Bottom, _ -> -1 | _, `Bottom -> 1 - | `Pacman, _ -> -1 - | _, `Pacman -> 1 + | `Pacman _, _ -> -1 + | _, `Pacman _ -> 1 in aux x y ;; @@ -234,7 +236,7 @@ let rec eta_subterm sub t = match t with | `Lam(_,t') -> eta_subterm (lift 1 sub) t' | `Bottom - | `Pacman -> false + | `Pacman _ -> false | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with | `Var(v',_) -> v = v' | `I((v',_), args') -> v = v' @@ -258,7 +260,7 @@ let max_arity_tms n = | `Var v -> aux_var l v | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms :> nf list)) | `Lam(_,t) -> aux (l+1) t - | `Bottom | `Pacman -> None + | `Bottom | `Pacman _ -> None and aux_tms l = List.fold_left (fun acc t -> max acc (aux l t)) None in fun tms -> aux_tms 0 (tms :> nf list) diff --git a/ocaml_new/num.mli b/ocaml_new/num.mli index 8b0bab4..ed8e6c9 100644 --- a/ocaml_new/num.mli +++ b/ocaml_new/num.mli @@ -4,13 +4,13 @@ type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ] type 'nf nf_nob_ = [ `I of var * 'nf nf_nob_ Listx.listx | `Lam of bool * 'nf - | `Pacman + | `Pacman of (('nf nf_nob_) i_var_) list | `Var of var ] type nf = [ `Bottom | `I of var * nf nf_nob_ Listx.listx | `Lam of bool * nf - | `Pacman + | `Pacman of ((nf nf_nob_) i_var_) list | `Var of var ] type nf_nob = nf nf_nob_ type i_var = nf_nob i_var_ diff --git a/ocaml_new/parser.ml b/ocaml_new/parser.ml index 487f042..9c36b43 100644 --- a/ocaml_new/parser.ml +++ b/ocaml_new/parser.ml @@ -186,7 +186,7 @@ let problem_of_string s = let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in let fix lev v = if v = lev + n_bot then `Bottom - else if v = lev + n_pac then `Pacman + else if v = lev + n_pac then `Pacman[] else if v = lev + n_bomb then `Lam(true, `Bottom) else if v = lev then `Var(v, min_int) (* zero *) else `Var(v,1) in (* 1 by default when variable not applied *) @@ -200,7 +200,7 @@ let problem_of_string s = | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args) | `Var(n,_) -> fix lev n | `Lam(_,t) -> `Lam (true, aux (lev+1) t) - | `Pacman -> `Pacman + | `Pacman _ as t -> t and aux lev : Num.nf -> Num.nf = function | #nf_nob as t -> aux_nob lev t | `Bottom -> assert false in diff --git a/ocaml_new/problems/2 b/ocaml_new/problems/2 index 0f3d6b1..335d635 100644 --- a/ocaml_new/problems/2 +++ b/ocaml_new/problems/2 @@ -23,6 +23,66 @@ C x BOMB z $? 2.5' D x (_. y y) C x (_. BOMB) z +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!! D x (_. BOT) !!!!!!!!!!! +!!!!!!!!!!!!!! C x (_. _. BOT) !!!!!!!!!!! +!!!!!!!!!!!!!! C x (_. z. z u) t !!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ??????????????? D x a1 a2 a3 diff --git a/ocaml_new/problems/3 b/ocaml_new/problems/3 new file mode 100644 index 0000000..a586545 --- /dev/null +++ b/ocaml_new/problems/3 @@ -0,0 +1,7 @@ +$???????????? +D x y +C x PAC (x y) + +$!!!!!!!!!!!!! +D x y z +C x PAC (x y) diff --git a/ocaml_new/problems/boh b/ocaml_new/problems/boh new file mode 100644 index 0000000..bdd3ea2 --- /dev/null +++ b/ocaml_new/problems/boh @@ -0,0 +1,5 @@ +$test.out +D z (λv0. v0) a (z (λv0. b)) (z (λv0. v0) v (λv0. v0)) (z PAC (a (λv0. w)) (λv0. λv1. v1)) (z (λv0. v0) a (z (λv0. b)) (z (λv0. v0) v (λv0. v0)) (z PAC (a (λv0. w)) (λv0. λv1. v1)) (w PAC w)) +C z (λv0. v0) a (y v (λv0. y)) (z b (z (λv0. v0) v)) (a (λv0. w) (z PAC (λv0. v0)) (z (λv0. v0) a)) +C z b (w PAC w) (z (λv0. v0) v) (λv0. w) (y v (λv0. y)) (λv0. λv1. v1) +C z PAC (λv0. v0) (λv0. w PAC) (λv0. z (λv1. v1) v) (λv0. z (λv1. v1) a (z (λv1. b)) (z (λv1. v1) v (λv1. v1)) (z PAC (a(λv1. w)) (λv1. λv2. v2))) (x (z (λv0. v0) a)) diff --git a/ocaml_new/problems/pac b/ocaml_new/problems/pac new file mode 100644 index 0000000..6b4e029 --- /dev/null +++ b/ocaml_new/problems/pac @@ -0,0 +1,3 @@ +$! +D x PAC due tre +C x uno due tre diff --git a/ocaml_new/test.ml b/ocaml_new/test.ml index 293c1e6..f345f05 100644 --- a/ocaml_new/test.ml +++ b/ocaml_new/test.ml @@ -35,7 +35,7 @@ let test3 n vars = then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams in aux (n-1) inerts lams - in aux (2*n) vars [] + in aux (2*n) vars ["PAC"; "PAC"] ;; let test4 n vars = @@ -71,7 +71,7 @@ let call_main4 div conv = let main = Random.self_init (); let num = 100 in - let complex = 1000 in + let complex = 100 in let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in (* let open Parser in *)