From: acondolu Date: Mon, 24 Jul 2017 15:19:59 +0000 (+0200) Subject: Fixing the bug when eating triggers the reduction of a match X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c5ade141028e42ce4503c5c74cad2fef1a97e860;p=fireball-separation.git Fixing the bug when eating triggers the reduction of a match --- diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 456dd5b..c28f723 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -287,7 +287,8 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif p ;; -exception Dangerous +exception TriggerMatchReduction of int;; +exception Dangerous;; let arity_of arities hd = let pos,_,nargs = List.find (fun (_,hd',_) -> hd=hd') arities in @@ -322,68 +323,73 @@ and dangerous_inert arities showstoppers k args more_args = (* cut & paste from above *) let rec dangerous_conv p arities showstoppers = function - `N _ + | `N _ | `Var _ | `Lam _ - | `Pacman -> [] - | `Match(t,_,liftno,bs,args) -> + | `Pacman -> () + | `Match(t,_,liftno,bs,args) -> ( (* CSC: XXX partial dependency on the encoding *) - (match t with - `N _ -> concat_map (dangerous_conv p arities showstoppers) args - | `Match _ as t -> dangerous_conv p arities showstoppers t @ concat_map (dangerous_conv p arities showstoppers) args + try (match t with + | `N _ -> List.iter (dangerous_conv p arities showstoppers) args + | `Match _ as t -> dangerous_conv p arities showstoppers t; List.iter (dangerous_conv p arities showstoppers) args | `Var(x,_) -> dangerous_inert_conv p arities showstoppers x [] args 2 | `I((x,_),args') -> dangerous_inert_conv p arities showstoppers x (Listx.to_list args') args 2 - ) + ) with TriggerMatchReduction x -> ( + match Util.find_opt (fun (n, t) -> if hd_of (List.nth p.ps n) = Some x then Some t else None) !bs with + | None -> () + | Some t -> ( + match t with + | `Bottom -> raise Dangerous + | #nf_nob as t -> dangerous_conv p arities showstoppers t + ) + ) + ) | `I((k,_),args) -> dangerous_inert_conv p arities showstoppers k (Listx.to_list args) [] 0 and dangerous_inert_conv p arities showstoppers k args match_args more_args = let all_args = args @ match_args in - let dangerous_args = concat_map (dangerous_conv p arities showstoppers) all_args in + List.iter (dangerous_conv p arities showstoppers) all_args; let all_args = (all_args :> nf list) in - if dangerous_args = [] then ( - if List.mem k showstoppers then k :: concat_map free_vars all_args else - try - let arity = arity_of arities k in + if List.mem k showstoppers then raise Dangerous else + try + let arity = arity_of arities k in prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var p.var_names k ^ " listlenargs=" ^ (string_of_int (List.length args)) ^ " more_args=" ^ string_of_int more_args); - if more_args > 0 (* match argument*) && List.length args = arity then [] - else if List.length all_args + more_args > arity then k :: concat_map free_vars all_args else [] - with - Not_found -> [] - ) else k :: concat_map free_vars all_args + if more_args > 0 (* match argument*) && List.length args = arity then raise (TriggerMatchReduction k) + else if List.length all_args + more_args > arity then raise Dangerous else () + with + Not_found -> () (* inefficient algorithm *) -let rec edible ({div; conv; ps} as p) arities showstoppers = - let rec aux showstoppers = - function - [] -> showstoppers +let rec edible p arities showstoppers = + let rec aux f showstoppers tms = function + | [] -> showstoppers | x::xs when List.exists (fun y -> hd_of x = Some y) showstoppers -> (* se la testa di x e' uno show-stopper *) let new_showstoppers = sort_uniq (showstoppers @ free_vars (x :> nf)) in (* aggiungi tutte le variabili libere di x *) if List.length showstoppers <> List.length new_showstoppers then - aux new_showstoppers ps + aux f new_showstoppers tms tms else - aux showstoppers xs + aux f showstoppers tms xs | x::xs -> match hd_of x with - None -> aux showstoppers xs + None -> aux f showstoppers tms xs | Some h -> try - dangerous arities showstoppers (x : i_n_var :> nf_nob) ; - aux showstoppers xs + f showstoppers (x :> nf_nob) ; + aux f showstoppers tms xs with Dangerous -> - aux (sort_uniq (h::showstoppers)) ps + aux f (sort_uniq (h::showstoppers)) tms tms in - let showstoppers = sort_uniq (aux showstoppers ps) in - let dangerous_conv = - List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in + let showstoppers = sort_uniq (aux (dangerous arities) showstoppers p.ps p.ps) in + let dangerous_conv = sort_uniq (aux (dangerous_conv p arities) showstoppers p.conv p.conv) in -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 p.var_names) l))) dangerous_conv; +(* 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 p.var_names) l))) dangerous_conv; *) - let showstoppers' = showstoppers @ List.concat dangerous_conv in - let showstoppers' = sort_uniq (match div with + let showstoppers' = showstoppers @ dangerous_conv in + let showstoppers' = sort_uniq (match p.div with | None -> showstoppers' | Some div -> if List.exists ((=) (hd_of_i_var div)) showstoppers' @@ -474,13 +480,13 @@ prerr_endline ("# [INST_IN_EAT] eating: " ^ string_of_var p.var_names hd ^ " := let x = hd_of_i_var div in let inst = make_lams `Bottom n in subst_in_problem x inst p in - let dangerous_conv = showstoppers_conv in +(*let dangerous_conv = showstoppers_conv in 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 p.var_names) l))) dangerous_conv; +List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv; *) let conv = - List.map (function s,t -> + List.map (function t -> try - if s <> [] then t else ( + if let hd = hd_of t in hd <> None && not (List.mem (Util.option_get hd) showstoppers_conv) then t else ( (match t with | `Var _ -> raise Not_found | _ -> ()); let _ = List.find (fun h -> hd_of t = Some h) inedible in t) @@ -489,7 +495,7 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p. | Some h -> prerr_endline ("FREEZING " ^ string_of_var p.var_names h); convergent_dummy - ) (List.combine showstoppers_conv p.conv) in + ) p.conv in List.iter (fun bs -> bs :=