exception Lambda
exception Backtrack of string
-(*
- The number of arguments which can applied to numbers
- safely, depending on the encoding of numbers.
- For Scott's encoding, two.
-*)
-let num_more_args = 2;;
(* verbosity *)
let _very_verbose = false;;
(** Display measure of every term when printing problem *)
);
let p = {p with sigma = sigma@[x,inst]} in
let p = super_simplify p in
- prerr_endline (string_of_problem "instantiate" p);
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
(match t with
`N _ -> List.iter (dangerous arities showstoppers) args
| `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args
- | `Var(x,_) -> dangerous_inert arities showstoppers x args num_more_args
- | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) num_more_args
+ | `Var(x,_) -> dangerous_inert arities showstoppers x args 2
+ | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2
)
| `I((k,_),args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0
(* 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
-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 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 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
-
-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 = 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
- 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'
then showstoppers' @ free_vars (div :> nf) else showstoppers') in
- if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
+ if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers'
;;
let precompute_edible_data {ps; div} xs =
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;
+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 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, showstoppers_conv = edible p arities showstoppers 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
- let p =
- List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
- let v = `N pos in
+ let new_sigma = List.map (fun (pos,hd,nargs) ->
+ let v = if pos = -1 then `Bottom else `N pos in
let inst = make_lams v nargs in
prerr_endline ("# [INST_IN_EAT] eating: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
- { p with sigma = p.sigma @ [hd,inst] }
- ) p l in
+ hd,inst
+ ) l in
(* to avoid applied numbers in safe positions that
trigger assert failures subst_in_problem x inst p*)
let ps =
`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) inedible
- then p
- else
- let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in
- 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 (
(match t with | `Var _ -> raise Not_found | _ -> ());
- 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
- | Some h ->
- prerr_endline ("FREEZING " ^ string_of_var p.var_names h);
- convergent_dummy
- ) (List.combine showstoppers_conv p.conv) 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)
+ | Some h -> prerr_endline ("FREEZING " ^ string_of_var p.var_names h));
+ convergent_dummy)
+ ) p.conv in
List.iter
(fun bs ->
bs :=
) p.deltas ;
let old_conv = p.conv in
let p = { p with ps; conv } 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
if l <> [] || old_conv <> conv
then prerr_endline (string_of_problem "eat" p);
if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then
;;
let rec auto_eat p =
- prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}";
+(* prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; *)
let m = problem_measure p in
let x, arity_of = choose_step p in
first arity_of p x (fun p j ->
let p' = instantiate p x j in
+ prerr_endline (string_of_problem "after instantiate" p');
match eat p' with
| `Finished p -> p
| `Continue p ->
- prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}";
+(* prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}"; *)
let delta = problem_measure p - m in
if delta >= 0
then
projects / fireball-separation.git / blobdiff