From 0a50c398d9eef65620f18f99ef675770b50a920c Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
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