]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Renamed in critical_showstoppers: showstoppers -> inedible (I don't know why)
authoracondolu <andrea.condoluci@unibo.it>
Sat, 22 Jul 2017 19:58:31 +0000 (21:58 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 09:11:37 +0000 (11:11 +0200)
(cherry picked from commit dc829653c03f7bf0977addabe480e7c8b178bad1)

ocaml/lambda4.ml

index e56a496a88cf83cc4eb8727a1f0b59274fd4a7eb..a87fe79e9e93a3d106ea30934bc68db48a39efb0 100644 (file)
@@ -404,11 +404,11 @@ let eat p =
   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 (_,hd,_) -> not (List.mem hd 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 (pos,hd,nargs) -> if pos = -1 then p else
-   let v = `N(pos) in
+   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] }
@@ -425,7 +425,7 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
  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
@@ -442,14 +442,14 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
     (* subst_in_problem (hd_of_i_var div) inst p in *)
      {p with sigma=p.sigma@[x,inst]} 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