[r2006-04-24 16:47:52 by afrisch] New subtyping algo

Original author: afrisch
Date: 2006-04-24 16:47:52+00:00

driver/cduce.ml

@@ -107,7 +107,8 @@ let rec print_exn ppf = function
       Format.fprintf ppf "but its inferred type is:@.%a@." 
         print_norm s;
       Format.fprintf ppf "which is not a subtype, as shown by the sample:@.%a@." 
-	print_sample (Sample.get (Types.diff s t))
+	(* print_sample (Sample.get (Types.diff s t)) *)
+	Types.Witness.print_witness (Types.witness (Types.diff s t))
   | Typer.NonExhaustive t ->
       Format.fprintf ppf "This pattern matching is not exhaustive@.";
       Format.fprintf ppf "Residual type:@.%a@."
@@ -192,7 +193,7 @@ let debug ppf tenv cenv = function
       (try
 	 let t = Types.descr (Typer.typ tenv t) in
 	 Format.fprintf ppf "%a@." print_sample (Sample.get t);
-	 Format.fprintf ppf "witness: %a@." Types.print_witness (Types.witness t);
+	 Format.fprintf ppf "witness: %a@." Types.Witness.print_witness (Types.witness t);
        with Not_found ->
 	 Format.fprintf ppf "Empty type : no sample !@.")
   | `Filter (t,p) -> 

types/types.mli

@@ -276,10 +276,12 @@ sig
   val to_string: t -> string
 end
 
+module Witness: sig
+  type witness
+  val print_witness: Format.formatter -> witness -> unit
+end
+val witness: t -> Witness.witness
 
-type witness
-val witness: t -> witness
-val print_witness: Format.formatter -> witness -> unit
 
 module Cache: sig
   type 'a cache