(* exceptions *)
exception Pacman
exception Bottom
+exception Lambda
exception Backtrack of string
(*
For Scott's encoding, two.
*)
let num_more_args = 2;;
+(* verbosity *)
let _very_verbose = false;;
+(** Display measure of every term when printing problem *)
+let _measure_of_terms = false;;
let verbose s =
if _very_verbose then prerr_endline s
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
let string_of_measure = string_of_int;;
let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
+ let aux_measure_terms t = if _measure_of_terms then "(" ^ string_of_int (measure_of_term t) ^ ") " else "" in
let deltas = String.concat ("\n# ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
let l = p.var_names in
String.concat "\n" ([
) else "# ";
"#";
"$" ^ p.label;
- (match div with None -> "# no D" | Some div -> "D ("^string_of_int (measure_of_term div)^")"^ print ~l (div :> nf));
+ (match div with None -> "# D" | Some div -> "D " ^ aux_measure_terms div ^ print ~l (div :> nf));
]
- @ 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
+ @ List.map (fun t -> if t = convergent_dummy then "# C" else "C " ^ aux_measure_terms t ^ print ~l (t :> nf)) conv
+ @ List.mapi (fun i t -> string_of_int i ^ " " ^ aux_measure_terms t ^ print ~l (t :> nf)) ps
@ [""])
;;
let freshno,new_t,acc_new_ps =
try
expand_match (freshno,ps,acc_new_ps) t
- with Pacman -> freshno,convergent_dummy,acc_new_ps
+ with Pacman | Lambda -> freshno,convergent_dummy,acc_new_ps
| Bottom -> raise (Backtrack "Bottom in conv") in
aux_conv ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in
(*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 *)
+ | `Lam _ -> raise Lambda (* assert false (* algorithm invariant/loose typing *) *)
| `Bottom -> raise Bottom
| `Pacman -> raise Pacman
| #i_n_var as x ->
| `Bottom
| `Pacman
| `Var _ -> 0 in
- Listx.max (Listx.map (fun t -> max (aux 0 t) (aux' true t)) tms)
+ Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms)
;;
let choose_step p =