if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers'
;;
-let precompute_edible_data {ps; div} xs =
+let precompute_edible_data {ps; div} =
+ let heads = uniq (List.sort compare ((match div with None -> [] | Some h -> [hd_of_i_var h]) @ filter_map hd_of ps)) in
let aux t = match t with `Var _ -> 0 | `I(_, args) -> Listx.length args | `N _ -> assert false in
- (fun l -> match div with
- | None -> l
- | Some div -> (-1, hd_of_i_var div, aux div) :: l)
- (List.map (fun hd ->
- let i, tm = Util.findi (fun y -> hd_of y = Some hd) ps in
- i, hd, aux tm
- ) xs)
+ List.map (fun hd ->
+ let i_tm = Util.find_alli (fun y -> hd_of y = Some hd) ps in
+ let i_tm = match div with Some div when hd_of_i_var div = hd -> (-1, (div :> i_n_var))::i_tm | _ -> i_tm in
+ let i_ar = List.map (fun (i,tm) -> i,aux tm) i_tm in
+ (* let's compute the minimal arity *)
+ match List.sort (fun (_,tm1) (_,tm2) -> compare tm1 tm2) i_ar with
+ [] -> assert false
+ | (i,ar)::_ -> i, hd, ar
+ ) heads
;;
+let rec dangerous_for_showstoppers_eat arities =
+ function
+ `N _
+ | `Var _
+ | `Lam _
+ | `Pacman -> []
+ | `Match(t,_,liftno,bs,args) ->
+ (* CSC: XXX partial dependency on the encoding *)
+ (match t with
+ `N _ -> []
+ | `Match _ as t -> dangerous_for_showstoppers_eat arities t
+ | `Var(x,_) -> dangerous_for_showstoppers_eat_inert arities x [] true
+ | `I((x,_),args') -> dangerous_for_showstoppers_eat_inert arities x (Listx.to_list args') true
+ ) @ List.concat (List.map (dangerous_for_showstoppers_eat arities ) args)
+ | `I((k,_),args) -> dangerous_for_showstoppers_eat_inert arities k (Listx.to_list args) false
+
+and dangerous_for_showstoppers_eat_inert arities k args in_match =
+ List.concat (List.map (dangerous_for_showstoppers_eat arities ) args) @
+ try
+ let arity = arity_of arities k in
+ if in_match && List.length args <> arity then [k]
+ else if List.length args > arity then [k]
+ else []
+ with
+ Not_found -> []
+
+let multiple_arities p arities =
+ List.concat (List.map (dangerous_for_showstoppers_eat arities) ((p.ps :> nf_nob list) @ (p.conv :> nf_nob list)))
+
(** Returns (p, showstoppers_step, showstoppers_eat) where:
- showstoppers_step are the heads occurring twice
in the same discriminating set
- showstoppers_eat are the heads in ps having different number
of arguments *)
-let critical_showstoppers p =
- let p = super_simplify p in
+let critical_showstoppers p arities =
let hd_of_div = match p.div with None -> [] | Some t -> [hd_of_i_var t] in
let showstoppers_step =
concat_map (fun bs ->
if List.exists (fun t -> [hd_of t] = List.map (fun x -> Some x) hd_of_div) p.conv
then hd_of_div else [] in
let showstoppers_step = sort_uniq showstoppers_step in
- let showstoppers_eat =
- let heads_and_arities =
- List.sort (fun (k,_) (h,_) -> compare k h)
- (filter_map (function `Var(k,_) -> Some (k,0) | `I((k,_),args) -> Some (k,Listx.length args) | _ -> None ) p.ps) in
- let rec multiple_arities =
- function
- []
- | [_] -> []
- | (x,i)::(y,j)::tl when x = y && i <> j ->
- x::multiple_arities tl
- | _::tl -> multiple_arities tl in
- multiple_arities heads_and_arities in
-
+ let showstoppers_eat = multiple_arities p arities in
let showstoppers_eat = sort_uniq showstoppers_eat in
- let showstoppers_eat = List.filter
- (fun x -> not (List.mem x showstoppers_step))
- showstoppers_eat in
+ let showstoppers_eat =
+ List.filter (fun x -> not (List.mem x showstoppers_step)) showstoppers_eat in
prerr_endline ("DANGEROUS STEP: " ^ String.concat " " (List.map (string_of_var p.var_names) showstoppers_step));
prerr_endline ("DANGEROUS EAT: " ^ String.concat " " (List.map (string_of_var p.var_names) showstoppers_eat));
p, showstoppers_step, showstoppers_eat
;;
let eat p =
- let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in
+ let p = super_simplify p in
+ let arities = precompute_edible_data p in
+ let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p arities in
let showstoppers = showstoppers_step @ showstoppers_eat in
- let heads = List.sort compare (filter_map hd_of ps) in
- let arities = precompute_edible_data p (uniq heads) in
let inedible = edible p arities showstoppers in
prerr_endline ("showstoppers (in eat)" ^ String.concat " " (List.map (string_of_var p.var_names) inedible));
let l = List.filter (fun (_,hd,_) -> not (List.mem hd inedible)) arities in
| Some h -> prerr_endline ("FREEZING " ^ string_of_var p.var_names h));
convergent_dummy)
) p.conv in
+ let div =
+ match p.div with
+ None -> None
+ | Some div -> if List.mem (hd_of_i_var div) inedible then Some div else None in
List.iter
(fun bs ->
bs :=
) !bs
) p.deltas ;
let old_conv = p.conv in
- let p = { p with ps; conv } in
+ let p = { p with ps; conv; div } in
(* In case (match x ... with ...) and we are eating x,
so we need to substitute *)
let p = List.fold_left (fun p (x,inst) -> subst_in_problem x inst p) p new_sigma in
;;
let choose_step p =
- let p, showstoppers_step, showstoppers_eat = critical_showstoppers p in
+ let p = super_simplify p in
+ let arities = precompute_edible_data p in
+ let p, showstoppers_step, showstoppers_eat = critical_showstoppers p arities in
let x =
match showstoppers_step, showstoppers_eat with
| [], y::_ ->
projects / fireball-separation.git / commitdiff