with Backtrack s ->
prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
-prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int i);
+prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1));
aux (i+1)
in
aux 1
@ p.ps
;;
-let sum_arities p =
+let measure_of_term, measure_of_terms =
let rec aux = function
| `N _ | `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)
- | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many (args :> nf list)
+ | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 then 0 else ar - 1) + aux_many (args :> nf list)
and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
- aux_many (all_terms p :> nf list)
- ;;
+ (fun t -> aux (t :> nf)), (fun l -> aux_many (l :> nf list))
+;;
+
+let sum_arities p = measure_of_terms (all_terms p)
let problem_measure p = sum_arities p;;
let string_of_measure = string_of_int;;
) else "# ";
"#";
"$" ^ p.label;
- (match div with None -> "# no D" | Some div -> "D " ^ print ~l (div :> nf));
+ (match div with None -> "# no D" | Some div -> "D ("^string_of_int (measure_of_term div)^")"^ print ~l (div :> nf));
]
- @ List.map (fun t -> if t = convergent_dummy then "#C" else "C " ^ print ~l (t :> nf)) conv
- @ List.mapi (fun i t -> string_of_int i ^ " " ^ print ~l (t :> nf)) ps
+ @ List.map (fun t -> if t = convergent_dummy then "#C" else "C ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) conv
+ @ List.mapi (fun i t -> string_of_int i ^ " ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) ps
@ [""])
;;
exception Dangerous
-let arity_of arities k =
- let _,pos,y = List.find (fun (v,_,_) -> v=k) arities in
- let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | `N _ -> assert false in
- arity + if pos = -1 then - 1 else 0
+let arity_of arities hd =
+ let pos,_,nargs = List.find (fun (_,hd',_) -> hd=hd') arities in
+ nargs + if pos = -1 then - 1 else 0
;;
let rec dangerous arities showstoppers =
aux showstoppers xs
with
Dangerous ->
- aux (sort_uniq (h::showstoppers)) ps
- in
- let showstoppers = sort_uniq (aux showstoppers ps) in
- let dangerous_conv =
- List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
+ aux (sort_uniq (h::showstoppers)) ps in
+
+ let showstoppers = sort_uniq (aux showstoppers ps) in
+ let dangerous_conv =
+ List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) 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;
- let showstoppers' = showstoppers @ List.concat dangerous_conv in
- let showstoppers' = sort_uniq (match div with
- | None -> showstoppers'
- | Some div ->
- if List.exists ((=) (hd_of_i_var div)) showstoppers'
- then showstoppers' @ free_vars (div :> nf) else showstoppers') in
- if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
+ let showstoppers' = showstoppers @ List.concat dangerous_conv in
+ let showstoppers' = sort_uniq (match div with
+ | None -> showstoppers'
+ | Some div ->
+ if List.exists ((=) (hd_of_i_var div)) showstoppers'
+ then showstoppers' @ free_vars (div :> nf) else showstoppers') in
+ if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
;;
let precompute_edible_data {ps; div} xs =
- (match div with None -> [] | Some div -> [hd_of_i_var div, -1, (div :> i_n_var)]) @
- List.map (fun hd ->
+ 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
- hd, i, tm
- ) xs
+ i, hd, aux tm
+ ) xs)
;;
+(** 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 hd_of_div = match p.div with None -> [] | Some t -> [hd_of_i_var t] in
let showstoppers_eat = List.filter
(fun x -> not (List.mem x showstoppers_step))
showstoppers_eat in
- List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
- List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
+List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
+List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
p, showstoppers_step, showstoppers_eat
;;
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 showstoppers, showstoppers_conv =
- edible p arities showstoppers in
- let l = List.filter (fun (x,_,_) -> not (List.mem x showstoppers)) arities in
+ let inedible, showstoppers_conv = edible p arities showstoppers in
+ let l = List.filter (fun (_,hd,_) -> not (List.mem hd inedible)) arities in
let p =
- List.fold_left (fun p (x,pos,(xx : i_n_var)) -> if pos = -1 then p else
- let n = match xx with `I(_,args) -> Listx.length args | _ -> 0 in
- let v = `N(pos) in
- let inst = make_lams v n in
-prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names x ^ " := " ^ string_of_term p inst);
- { p with sigma = p.sigma @ [x,inst] }
+ List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
+ let v = `N pos in
+ let inst = make_lams v nargs in
+prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
+ { p with sigma = p.sigma @ [hd,inst] }
) p l in
(* to avoid applied numbers in safe positions that
trigger assert failures subst_in_problem x inst p*)
let ps =
List.map (fun t ->
try
- let _,j,_ = List.find (fun (h,_,_) -> hd_of t = Some h) l in
+ let j,_,_ = List.find (fun (_,hd,_) -> hd_of t = Some hd) l in
`N j
with Not_found -> t
) ps in
let p = match p.div with
| None -> p
| Some div ->
- if List.mem (hd_of_i_var div) showstoppers
+ if List.mem (hd_of_i_var div) inedible
then p
else
let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 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 p.var_names) l))) dangerous_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;
let conv =
List.map (function s,t ->
try
if s <> [] then t else (
(match t with | `Var _ -> raise Not_found | _ -> ());
- let _ = List.find (fun h -> hd_of t = Some h) showstoppers in
+ let _ = List.find (fun h -> hd_of t = Some h) inedible in
t)
with Not_found -> match hd_of t with
| None -> assert (t = convergent_dummy); t
projects / fireball-separation.git / blobdiff