From: acondolu Date: Wed, 12 Jul 2017 21:11:54 +0000 (+0200) Subject: Removed bomb variable X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=28250e81c87d7247f0786ca5b62e9bbdc241daab;p=fireball-separation.git 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 112f7de..db743ff 100644 --- 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 ("------- ------\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 "------------------"; + 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 "------------------"; @@ -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 57cb19d..443dcdc 100644 --- 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 78c6c4c..95dae15 100644 --- 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 f360074..a6b90ac 100644 --- 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