From 0a50c398d9eef65620f18f99ef675770b50a920c Mon Sep 17 00:00:00 2001 From: acondolu Date: Sat, 22 Jul 2017 22:35:44 +0200 Subject: [PATCH] Comments, fix indentation and --- ocaml/lambda4.ml | 35 ++++++++++++++++++++--------------- 1 file changed, 20 insertions(+), 15 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 392784f..4826263 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -58,7 +58,7 @@ let first bound p var f = 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 @@ -368,22 +368,22 @@ let rec edible ({div; conv; ps} as p) 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 = @@ -397,6 +397,11 @@ let precompute_edible_data {ps; div} xs = ) 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 @@ -426,8 +431,8 @@ let critical_showstoppers p = 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 ;; -- 2.39.2