[r2004-12-21 16:09:03 by afrisch] Empty log message

Original author: afrisch
Date: 2004-12-21 16:09:03+00:00

Makefile.distrib

@@ -155,8 +155,8 @@ OBJECTS = \
  types/sortedList.cmo types/boolean.cmo types/ident.cmo \
  types/intervals.cmo types/chars.cmo types/atoms.cmo \
  types/normal.cmo \
- types/types.cmo types/patterns.cmo types/sequence.cmo \
- types/sample.cmo types/builtin_defs.cmo \
+ types/types.cmo types/sample.cmo types/patterns.cmo types/sequence.cmo \
+ types/builtin_defs.cmo \
  \
  compile/lambda.cmo \
  runtime/value.cmo \

driver/cduce.ml

@@ -204,6 +204,33 @@ let debug ppf tenv cenv = function
 	       Explain.print_path p
 	 | None ->
 	     Format.fprintf ppf "Explanation: value has given type@.")
+  | `Single t ->
+      Format.fprintf ppf "[DEBUG:single]@.";
+      let t = Typer.typ tenv t in
+      (try 
+	 let c = Sample.single (Types.descr t) in
+	 Format.fprintf ppf "Constant:%a@." Types.Print.print_const c
+       with
+	 | Exit -> Format.fprintf ppf "Non constant@." 
+	 | Not_found ->  Format.fprintf ppf "Empty@.")
+  | `Approx (p,t) ->
+      Format.fprintf ppf "[DEBUG:approx]@.";
+      let t = Typer.typ tenv t in
+      let p = Typer.pat tenv p in
+      let c = Patterns.approx (Patterns.descr p) (Types.descr t) in
+      List.iter 
+	(fun (x,c) ->
+	   Format.fprintf ppf "%a:" U.print (Id.value x);
+	   (match c with
+	      | None -> Format.fprintf ppf "*"
+	      | Some (v,c) ->
+		  if v then Format.fprintf ppf "# ";
+		  match c with
+		    | Some c -> 
+			Format.fprintf ppf "%a" Types.Print.print_const c
+		    | None -> ());
+	   Format.fprintf ppf "@."
+	) c
 
 
 let flush_ppf ppf = Format.fprintf ppf "@."

parser/ast.ml

@@ -22,6 +22,8 @@ and debug_directive =
   | `Compile of ppat * ppat list 
   | `Subtype of ppat * ppat
   | `Explain of ppat * pexpr
+  | `Single of ppat
+  | `Approx of ppat * ppat
   ]
 and toplevel_directive =
   [ `Quit

parser/parser.ml

@@ -190,6 +190,8 @@ EXTEND
     | IDENT "sample"; t = pat -> `Sample t
     | IDENT "subtype"; t1 = pat; t2 = pat -> `Subtype (t1,t2)
     | IDENT "explain"; t = pat; e = expr -> `Explain (t,e)
+    | IDENT "single"; t = pat -> `Single t
+    | IDENT "approx"; p = pat; t = pat -> `Approx (p,t)
     ]
   ];
 

types/atoms.ml

@@ -53,6 +53,11 @@ let print_symbolset ns ppf = function
 
 include SortedList.FiniteCofiniteMap(Ns)(SymbolSet)
 
+let single s = match get s with
+  | `Finite [ns, SymbolSet.Finite [a]] -> (ns,a)
+  | `Finite [] -> raise Not_found
+  | _ -> raise Exit
+
 let print_tag s = match get s with
   | `Finite [ns, SymbolSet.Finite [a]] -> 
       Some (fun ppf -> V.print ppf (ns,a))

types/atoms.mli

@@ -28,6 +28,7 @@ val disjoint : t -> t -> bool
 val is_empty : t -> bool
 val print_tag : t -> (Format.formatter -> unit) option
 
+val single : t -> V.t
 
 type 'a map
 val mk_map: (t * 'a) list -> 'a map

types/chars.ml

@@ -104,6 +104,11 @@ let sample = function
   | (i,j) :: _ -> i
   | _ -> raise Not_found
 
+let single = function
+  | [ (i,j) ] when i = j -> i
+  | [] -> raise Not_found
+  | _ -> raise Exit
+
 let is_char = function
   | [(i,j) ] when i = j -> Some i
   | _ -> None

types/chars.mli

@@ -26,6 +26,7 @@ val is_empty : t -> bool
 val contains : V.t-> t -> bool
 val sample : t -> V.t
 val is_char : t -> V.t option
+val single : t -> V.t
 
 
 type 'a map

types/intervals.ml

@@ -263,6 +263,10 @@ let sample = function
   | Any :: _ -> zero_big_int
   | [] -> raise Not_found
   
+let single = function
+  | [ Bounded (x,y) ] when eq_big_int x y -> x
+  | [] -> raise Not_found
+  | _ -> raise Exit
 
 let print =
   List.map 

types/intervals.mli

@@ -52,6 +52,9 @@ val disjoint : t -> t -> bool
 val is_empty : t -> bool
 val contains : V.t -> t -> bool
 val sample : t -> V.t
+val single : t -> V.t
+  (* raise Not_found if empty.
+     raise Exit if empty and not singleton *)
 
 
 val add : t -> t -> t

types/patterns.ml

@@ -234,7 +234,7 @@ end
 
 (* Pretty-print *)
 
-module P = struct
+module Pat = struct
   type t = descr
   let rec compare (t1,fv1,d1) (t2,fv2,d2) = if d1 == d2 then 0 else
     match (d1,d2) with
@@ -271,8 +271,8 @@ module P = struct
 end
 
 module Print = struct
-  module M = Map.Make(P)
-  module S = Set.Make(P)
+  module M = Map.Make(Pat)
+  module S = Set.Make(Pat)
 
   let names = ref M.empty
   let printed = ref S.empty
@@ -1528,3 +1528,112 @@ struct
 end
 
 
+
+
+(* New compilation procedure *)
+
+module Compile2 = struct
+
+  module PatList = SortedList.Make(
+    struct
+      include Custom.Dummy
+      include Pat
+    end)
+  module TypesFv = Custom.Pair(Types)(IdSet)
+  module Request = PatList.MakeMap(TypesFv)
+    (* Invariant for (p |-> (t,X)):
+       i)  t != Empty
+       ii) X \subset fv(p) *)
+
+  module Approx = struct
+    type t = (bool * Types.const option) option
+	(* - None: cannot match
+	   - Some (true,_): can only bind to the matched value
+	   - Some (_, Some c): can only bind to the constant c *)
+
+    let merge a b = match (a,b) with
+      | None, x | x, None -> x
+      | Some (x1, c1), Some (x2,c2) ->
+	  Some (x1 && x2,
+		match c1,c2 with
+		  | Some c1, Some c2 when 
+		      Types.Const.compare c1 c2 = 0 -> Some c1
+(* Note: the same constant can have several representations.
+   Currently, Const.compare will distinguish them. E.g.:
+# debug approx (x := "ab") & Int | (x := ('a',"b")) Any;;
+[DEBUG:approx]
+*)
+		  | _ -> None)
+
+  let rec approx (a,fv,d) t xs =
+    assert (Types.subtype t a);
+    assert (IdSet.subset xs fv);
+    if IdSet.is_empty xs then IdSet.Map.empty
+    else if Types.is_empty t then IdSet.Map.constant None xs
+    else match d with
+      | Cup ((a1,_,_) as p1,p2) ->
+	  IdSet.Map.merge merge 
+	    (approx p1 (Types.cap t a1) xs) 
+	    (approx p2 (Types.diff t a1) xs)
+      | Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
+	  IdSet.Map.union_disj
+	    (approx p1 t (IdSet.cap fv1 xs))
+	    (approx p2 t (IdSet.cap fv2 xs))
+      | Capture x ->
+	  IdSet.Map.singleton x 
+	    (Some (true, Sample.single_opt t))
+      | Constant (x,c) -> 
+	  IdSet.Map.singleton x 
+	    (Some (Types.subtype t (Types.constant c), Some c))
+      | _ ->
+	  IdSet.Map.constant (Some (false, None)) xs
+	  (* TODO: recursive factorization   (x,x) -> x *)
+  end
+
+  type dpat =
+    | TFail
+    | TSucceed
+    | TConstr of Types.t
+    | TCup of pat * pat
+    | TCap of pat * pat
+    | TTimes of req * req
+    | TXml of req * req
+    | TCapture of id
+    | TConstant of id * Types.const
+  and pat = dpat
+  and req = descr * Types.t * fv
+
+  let pi1 t = Types.Product.pi1 (Types.Product.get t)
+  let pi2 t = Types.Product.pi2 (Types.Product.get t)
+
+  let rec eval_pat (a,fv,d) t xs =
+    if Types.disjoint a t then TFail
+    else if (IdSet.is_empty xs) && (Types.subtype t a) then TSucceed
+    else eval_d t xs d
+  and eval_d t xs = function
+    | Constr t ->
+	TConstr t
+    | Cup ((a1,_,_) as p1,p2) ->
+	TCup (eval_pat p1 t xs, eval_pat p2 (Types.diff t a1) xs)
+    | Cap ((a1,fv1,_) as p1,((_,fv2,_) as p2)) ->
+	TCap (eval_pat p1 t (IdSet.cap xs fv1), 
+	      eval_pat p2 (Types.cap t a1) (IdSet.cap xs fv2))
+    | Constant (x,c) when Types.subtype t (Types.constant c) ->
+	TCapture x
+    | Constant (x,c) ->
+	TConstant (x,c)
+    | Capture x ->
+	TCapture x
+    | Times (q1,q2) ->
+	TTimes ((q1.descr, pi1 t, IdSet.cap xs q1.fv),
+		(q2.descr, pi2 t, IdSet.cap xs q2.fv))
+    | Xml (q1,q2) ->
+	TXml ((q1.descr, pi1 t, IdSet.cap xs q1.fv),
+	      (q2.descr, pi2 t, IdSet.cap xs q2.fv))
+    | Record (l,q) ->
+	assert false
+    | Dummy -> assert false
+end
+
+let approx ((_,fv,_) as  p) t = 
+  IdSet.Map.get (Compile2.Approx.approx p t fv)

types/patterns.mli

@@ -80,3 +80,9 @@ module Compile: sig
 
   val debug_compile : Format.formatter -> Types.Node.t -> node list -> unit
 end
+
+
+val approx :
+  descr ->
+  Types.descr ->
+  (id * (bool * Types.Const.t option) option) list

types/sample.ml

@@ -16,8 +16,8 @@ let rec get memo t =
   let cons t = Types.cons (get memo t) in
   let pair (t1,t2) = Types.times (cons t1) (cons t2) in
   let xml (t1,t2) = Types.xml (cons t1) (cons t2) in
-  let rec fields = function
-    | (true,_) -> absent
+  let fields = function
+    | (true,_) -> assert false (* absent *)
     | (false,t) -> cons t in
   let record (r,some,none) = 
     let r = LabelMap.filter (fun l (o,t) -> not o) r in
@@ -41,3 +41,50 @@ let rec get memo t =
 let get = get D.empty
 
 let print = Types.Print.print
+
+
+let try_single r f x =
+  try
+    let v = f x in
+    match !r with
+      | None -> r := Some v
+      | Some v' -> if (Types.Const.compare v v' !=0) then raise Exit
+  with Not_found -> ()
+
+let rec single memo t =
+  if D.mem t memo then raise Exit;
+  let memo = D.add t memo in
+  let pair (t1,t2) = Types.Pair (single memo t1, single memo t2) in
+  let xml (t1,t2) = Types.Xml (single memo t1, single memo t2) in
+  let int t = Types.Integer (Intervals.single (Types.Int.get t)) in
+  let atom t = Types.Atom (Atoms.single (Types.Atom.get t)) in
+  let char t = Types.Char (Chars.single (Types.Char.get t)) in
+  let fields = function
+    | (true,_) -> assert false
+    | (false,t) -> single memo t in
+  let record = function
+    | (r,false,true) -> 
+	let r = 
+	  LabelMap.filter 
+	    (fun l (o,t) -> 
+	       if o then if (Types.non_empty t) then raise Exit else false
+	       else true) r in
+	Types.Record (LabelMap.map fields r)
+    | _ -> raise Exit in
+  let r = ref None in
+  try_single r int t;
+  try_single r char t;
+  try_single r atom t;
+  List.iter (try_single r pair) (Types.Product.get t);
+  List.iter (try_single r xml) (Types.Product.get ~kind:`XML t);
+  List.iter (try_single r record) (Types.Record.get t);
+  (try ignore (Types.Arrow.sample t); raise Exit with Not_found -> ());
+  match !r with
+    | None -> raise Not_found
+    | Some c -> c
+
+let single = single D.empty
+
+let single_opt t =
+  try Some (single t)
+  with Not_found | Exit -> None

types/sample.mli

@@ -18,3 +18,11 @@ val get : Types.descr -> t
   **)
 
 val print : Format.formatter -> t -> unit
+
+
+val single : Types.descr -> Types.const
+  (**
+     Raises Not_found for an empty type.
+     Raises Exit if at least two values in the type.
+  **)
+val single_opt : Types.descr -> Types.const option

types/types.ml

@@ -947,6 +947,9 @@ let non_empty d =
 let subtype d1 d2 =
   is_empty (diff d1 d2)
 
+let disjoint d1 d2 =
+  is_empty (cap d1 d2)
+
 module Product =
 struct
   type t = (descr * descr) list
@@ -1864,4 +1867,3 @@ let empty_closed_record = rec_of_list ~opened:false []
 let empty_opened_record = rec_of_list ~opened:true []
 
   (* </helpers> *)
-

types/types.mli

@@ -247,6 +247,7 @@ val normalize : t -> t
 val is_empty : t -> bool
 val non_empty: t -> bool
 val subtype  : t -> t -> bool
+val disjoint : t -> t -> bool
 
 module Print :
 sig