]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Added variable convergent_dummy
authoracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 08:56:07 +0000 (10:56 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 09:08:44 +0000 (11:08 +0200)
ocaml/lambda4.ml

index 2b08e72c3bb282046a81497ea2b1e38bcff91bab..62837b2fd9842ce177e507737d3b8ffd89a6ea4c 100644 (file)
@@ -12,6 +12,8 @@ let bomb = ref(`Var(-1,-666));;
 *)
 let num_more_args = 2;;
 
+let convergent_dummy = `N ~-1;
+
 type problem =
  { freshno: int
  ; div: i_var option (* None = bomb *)
@@ -68,7 +70,7 @@ let print_problem label ({freshno; div; conv; ps; deltas} as p) =
  ^"(* DIVERGENT  *)" ^ nl
  ^"     "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\")") ^ nl
  ^"  (* CONVERGENT *) [" ^ nl ^ "  "
- ^ String.concat "\n  " (List.map (fun t -> "(* _ *) " ^ (if t = `N (-1) then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^
+ ^ String.concat "\n  " (List.map (fun t -> "(* _ *) " ^ (if t = convergent_dummy then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^
  (if conv = [] then "" else nl)
  ^ "] (* NUMERIC    *) [" ^ nl ^ " "
  ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps)
@@ -430,10 +432,10 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))
      let _ = List.find (fun h -> hd_of t = Some h) showstoppers in
       t)
     with Not_found -> match hd_of t with
-     | None -> assert (t = `N ~-1); t
+     | None -> assert (t = convergent_dummy); t
      | Some h ->
       prerr_endline ("FREEZING " ^ string_of_var h);
-      `N ~-1 (* convergent dummy*)
+      convergent_dummy
    ) (List.combine showstoppers_conv p.conv) in
  List.iter
   (fun bs ->