viewcvs.cgi/types/types.ml

open Recursive
open Printf


type label = int
type atom  = int

type const = Integer of int | Atom of atom | String of string

module I = struct
  type 'a t = {
    ints  : Intervals.t;
    atoms : atom Atoms.t;
    times : ('a * 'a) Boolean.t;
    arrow : ('a * 'a) Boolean.t;
    record: (label * bool * 'a) Boolean.t;
    strs  : Strings.t;
  }
                
  let empty = { 
    times = Boolean.empty; 
    arrow = Boolean.empty; 
    record= Boolean.empty;
    ints  = Intervals.empty;
    atoms = Atoms.empty;
    strs  = Strings.empty;
  }
  let any =  {
    times = Boolean.full; 
    arrow = Boolean.full; 
    record= Boolean.full; 
    ints  = Intervals.full;
    atoms = Atoms.full;
    strs  = Strings.any;
  }
               
  let interval i j = { empty with ints = Intervals.atom (i,j) }
  let times x y = { empty with times = Boolean.atom (x,y) }
  let arrow x y = { empty with arrow = Boolean.atom (x,y) }
  let record label opt t = { empty with record = Boolean.atom (label,opt,t) }
  let atom a = { empty with atoms = Atoms.atom a }
  let string r = { empty with strs = Strings.Regexp.compile r }
  let constant = function
    | Integer i -> interval i i
    | Atom a -> atom a
    | String s -> string (Strings.Regexp.str s)

                   
  let any_record = { empty with record = any.record }

  let cup x y = 
    if x = y then x else { 
      times = Boolean.cup x.times y.times;
      arrow = Boolean.cup x.arrow y.arrow;
      record= Boolean.cup x.record y.record;
      ints  = Intervals.cup x.ints  y.ints;
      atoms = Atoms.cup x.atoms y.atoms;
      strs  = Strings.cup x.strs y.strs;
    }
      
  let cap x y = 
    if x = y then x else {
      times = Boolean.cap x.times y.times;
      record= Boolean.cap x.record y.record;
      arrow = Boolean.cap x.arrow y.arrow;
      ints  = Intervals.cap x.ints  y.ints;
      atoms = Atoms.cap x.atoms y.atoms;
      strs  = Strings.cap x.strs y.strs;
    }
      
  let diff x y = 
    if x = y then empty else { 
      times = Boolean.diff x.times y.times;
      arrow = Boolean.diff x.arrow y.arrow;
      record= Boolean.diff x.record y.record;
      ints  = Intervals.diff x.ints  y.ints;
      atoms = Atoms.diff x.atoms y.atoms;
      strs  = Strings.diff x.strs y.strs;
    }

  let neg x = diff any x
                   
  let equal e a b =
    if a.ints <> b.ints then raise NotEqual;
    if a.atoms <> b.atoms then raise NotEqual;
    if a.strs <> b.strs then raise NotEqual;
    Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;
    Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;
    Boolean.equal (fun (l1,o1,x1) (l2,o2,x2) -> 
                     if (l1 <> l2) || (o1 <> o2) then raise NotEqual;
                     e x1 x2) a.record b.record
      
  let map f a =
    { times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;
      arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;
      record= Boolean.map (fun (l,o,x) -> (l,o, f x)) a.record;
      ints  = a.ints;
      atoms = a.atoms;
      strs  = a.strs;
    }
    
  let hash h a =
    Hashtbl.hash (map h a)
      
  let iter f a =
    ignore (map f a)
      
  let deep = 4
end

             
module Algebra = Recursive.Make(I)
include I
include Algebra

let check d =
  Boolean.check d.times;
  Boolean.check d.arrow;
  Boolean.check d.record;
  ()

(*
let define n d = check d; define n d
*)

let cons d =
  let n = make () in
  define n d;
  internalize n


module Positive =
struct
  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]
  and v = { mutable def : rhs; mutable node : node option }


  let rec make_descr seen v =
    if List.memq v seen then empty
    else
      let seen = v :: seen in
      match v.def with
        | `Type d -> d
        | `Cup vl -> 
            List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
        | `Times (v1,v2) -> times (make_node v1) (make_node v2)

  and make_node v =
    match v.node with
      | Some n -> n
      | None ->
          let n = make () in
          v.node <- Some n;
          let d = make_descr [] v in
          define n d;
          n

  let forward () = { def = `Cup []; node = None }
  let def v d = v.def <- d
  let cons d = let v = forward () in def v d; v
  let ty d = cons (`Type d)
  let cup vl = cons (`Cup vl)
  let times d1 d2 = cons (`Times (d1,d2))
  let define v1 v2 = def v1 (`Cup [v2]) 

  let solve v = internalize (make_node v)
end


let get_record r =
  let add = SortedMap.add (fun (o1,t1) (o2,t2) -> (o1&&o2, cap t1 t2)) in
  let line (p,n) =
    let accu = List.fold_left 
                 (fun accu (l,o,t) -> add l (o,descr t) accu) [] p in
    List.fold_left 
      (fun accu (l,o,t) -> add l (not o,neg (descr t)) accu) accu n in
  List.map line r
    

let counter_label = ref 0
let label_table = Hashtbl.create 63
let label_names = Hashtbl.create 63

let label s =
  try Hashtbl.find label_table s
  with Not_found ->
    incr counter_label;
    Hashtbl.add label_table s !counter_label;
    Hashtbl.add label_names !counter_label s;
    !counter_label

let label_name l =
  Hashtbl.find label_names l

let mk_atom = label

let atom_name = label_name

(* Subtyping algorithm *)

let diff_t d t = diff d (descr t)
let cap_t d t = cap d (descr t)
let cap_product l = 
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
    (any,any)
    l


module Assumptions = Set.Make(struct type t = descr let compare = compare end)

let memo = ref Assumptions.empty
let cache_false = ref Assumptions.empty

exception NotEmpty

let rec empty_rec d =
  if Assumptions.mem d !cache_false then false 
  else if Assumptions.mem d !memo then true
  else if not (Intervals.is_empty d.ints) then false
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Strings.is_empty d.strs) then false
  else (
    let backup = !memo in
    memo := Assumptions.add d backup;
    if 
      (empty_rec_times d.times) &&
      (empty_rec_arrow d.arrow) &&
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
      cache_false := Assumptions.add d !cache_false;
      false
    )
  )

and empty_rec_times c =
  List.for_all empty_rec_times_aux c

and empty_rec_times_aux (left,right) =
  let rec aux accu1 accu2 = function
    | (t1,t2)::right ->
        let accu1' = diff_t accu1 t1 in
        if not (empty_rec accu1') then aux accu1' accu2 right;
        let accu2' = diff_t accu2 t2 in
        if not (empty_rec accu2') then aux accu1 accu2' right
    | [] -> raise NotEmpty
  in
  let (accu1,accu2) = cap_product left in
  (empty_rec accu1) || (empty_rec accu2) ||
  (try aux accu1 accu2 right; true with NotEmpty -> false)

and empty_rec_arrow c =
  List.for_all empty_rec_arrow_aux c

and empty_rec_arrow_aux (left,right) =
  let single_right (s1,s2) =
    let rec aux accu1 accu2 = function
      | (t1,t2)::left ->
          let accu1' = diff_t accu1 t1 in
          if not (empty_rec accu1') then aux accu1 accu2 left;
          let accu2' = cap_t accu2 t2 in
          if not (empty_rec accu2') then aux accu1 accu2 left
      | [] -> raise NotEmpty
    in
    let accu1 = descr s1 in
    (empty_rec accu1) ||
    (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
  in
  List.exists single_right right

and empty_rec_record c =
  let aux = List.exists (fun (_,(opt,t)) -> (not opt) && (empty_rec t)) in
  List.for_all aux (get_record c)

let is_empty d =
  let r = empty_rec d in
  memo := Assumptions.empty;
  cache_false := Assumptions.empty;
  r

let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

(* Sample value *)
module Sample =
struct

let rec find f = function
  | [] -> raise Not_found
  | x::r -> try f x with Not_found -> find f r

type t =
  | Int of int
  | Atom of atom
  | String of string
  | Pair of t * t
  | Record of (label * t) list
  | Fun of (node * node) list

let rec gen_atom i l =
  if SortedList.mem l i then gen_atom (succ i) l  else i

let rec sample_rec memo d =
  if (Assumptions.mem d memo) || (is_empty d) then raise Not_found 
  else 
    try Int (Intervals.sample d.ints) with Not_found ->
    try Atom (Atoms.sample (gen_atom 0) d.atoms) with Not_found ->
    try String (Strings.sample d.strs) with Not_found ->
    try sample_rec_arrow d.arrow with Not_found ->

    let memo = Assumptions.add d memo in
    try sample_rec_times memo d.times with Not_found ->
    try sample_rec_record memo d.record with Not_found -> 
    raise Not_found


and sample_rec_times memo c = 
  find (sample_rec_times_aux memo) c

and sample_rec_times_aux memo (left,right) =
  let rec aux accu1 accu2 = function
    | (t1,t2)::right ->
        let accu1' = diff_t accu1 t1 in
        if non_empty accu1' then aux accu1' accu2 right else
          let accu2' = diff_t accu2 t2 in
          if non_empty accu2' then aux accu1 accu2' right else
            raise Not_found
    | [] -> Pair (sample_rec memo accu1, sample_rec memo accu2)
  in
  let (accu1,accu2) = cap_product left in
  if (is_empty accu1) || (is_empty accu2) then raise Not_found;
  aux accu1 accu2 right

and sample_rec_arrow c =
  find sample_rec_arrow_aux c

and sample_rec_arrow_aux (left,right) =
  let single_right (s1,s2) =
    let rec aux accu1 accu2 = function
      | (t1,t2)::left ->
          let accu1' = diff_t accu1 t1 in
          if non_empty accu1' then aux accu1 accu2 left;
          let accu2' = cap_t accu2 t2 in
          if non_empty accu2' then aux accu1 accu2 left
      | [] -> raise NotEmpty
    in
    let accu1 = descr s1 in
    (is_empty accu1) ||
    (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
  in
  if List.exists single_right right then raise Not_found
  else Fun left


and sample_rec_record memo c =
  Record (find (sample_rec_record_aux memo) (get_record c))

and sample_rec_record_aux memo fields =
  let aux acc (l,(o,t)) = if o then acc else (l, sample_rec memo t) :: acc in
  List.fold_left aux [] fields

let get x = sample_rec Assumptions.empty x
end


module Product =
struct
  type t = (descr * descr) list

  let get d =
    let line accu (left,right) =
      let rec aux accu d1 d2 = function
        | (t1,t2)::right ->
            let accu = 
              let d1 = diff_t d1 t1 in
              if is_empty d1 then accu else aux accu d1 d2 right in
            let accu =
              let d2 = diff_t d2 t2 in
              if is_empty d2 then accu else aux accu d1 d2 right in
            accu
        | [] ->  (d1,d2) :: accu
      in
      let (d1,d2) = cap_product left in
      if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right
    in
    List.fold_left line [] d.times

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty

  let restrict_1 rects pi1 =
    let aux accu (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then accu else (t1,t2)::accu in
    List.fold_left aux [] rects
  
  type normal = t

  let normal d =
    let res = ref [] in

    let add (t1,t2) =
      let rec loop t1 t2 = function
        | [] -> res := (ref (t1,t2)) :: !res
        | ({contents = (d1,d2)} as r)::l ->
            (*OPT*) 
            if d1 = t1 then r := (d1,cup d2 t2) else
              
              let i = cap t1 d1 in
              if is_empty i then loop t1 t2 l
              else (
                r := (i, cup t2 d2);
                let k = diff d1 t1 in 
                if non_empty k then res := (ref (k,d2)) :: !res;
                
                let j = diff t1 d1 in 
                if non_empty j then loop j t2 l
              )
      in
      loop t1 t2 !res
    in
    List.iter add (get d);
    List.map (!) !res

  let any = { empty with times = any.times }
end


module Record = 
struct
  type t = (label, (bool * descr)) SortedMap.t list

  let get d =
    let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in
    List.filter line (get_record d.record)


  let restrict_label_present t l =
    let aux = SortedMap.change l (fun (_,d) -> (false,d)) (false,any) in
    List.map aux t

  let restrict_label_absent t l =
    let restr = function (true, _) -> (true,empty) | _ -> raise Exit in
    let aux accu r =  
      try SortedMap.change l restr (true,empty) r :: accu
      with Exit -> accu in
    List.fold_left aux [] t

  let restrict_field t l d =
    let restr (_,d1) = 
      let d1 = cap d d1 in 
      if is_empty d1 then raise Exit else (false,d1) in
    let aux accu r = 
      try SortedMap.change l restr (false,d) r :: accu 
      with Exit -> accu in
    List.fold_left aux [] t

  let project_field t l =
    let aux accu x =
      match List.assoc l x with
        | (false,t) -> cup accu t
        | _ -> raise Not_found
    in
    List.fold_left aux empty t

  type normal = 
      [ `Success
      | `Fail
      | `Label of label * (descr * normal) list * normal ]

  let rec merge_record n r =
    match (n, r) with
      | (`Success, _) | (_, []) -> `Success
      | (`Fail, r) ->
          let aux (l,(o,t)) n = `Label (l, [t,n], if o then n else `Fail) in
          List.fold_right aux r `Success
      | (`Label (l1,present,absent), (l2,(o,t2))::r') ->
          if (l1 < l2) then
            let pr =  List.map (fun (t,x) -> (t, merge_record x r)) present in
            `Label (l1,pr,merge_record absent r)
          else if (l2 < l1) then
            let n' = merge_record n r' in
            `Label (l2, [t2, n'], if o then n' else n)
          else
            let res = ref [] in
            let aux a (t,x) = 
              (let t = diff t t2 in 
               if non_empty t then res := (t,x) :: !res);
              (let t = cap t t2 in
               if non_empty t then res := (t, merge_record x r') :: !res);
              diff a t 
            in
            let t2 = List.fold_left aux t2 present in
            let () = 
              if non_empty t2 then 
              res := (t2, merge_record `Fail r') :: !res in
            let abs = if o then merge_record absent r' else absent in
            `Label (l1, !res, abs)


  let normal d =
    List.fold_left merge_record `Fail (get d)

  let project d l =
    let aux accu x =
      match List.assoc l x with
        | (false,t) -> cup accu t
        | _ -> raise Not_found
    in
    List.fold_left aux empty (get_record d.record)

  let any = { empty with record = any.record }
  let is_empty d = d = []
end


module MapDescr = Map.Make(struct type t = descr let compare = compare end)

let memo_normalize = ref MapDescr.empty

let map_sort f l =
  SortedList.from_list (List.map f l)

let rec rec_normalize d =
  try MapDescr.find d !memo_normalize
  with Not_found ->
    let n = make () in
    memo_normalize := MapDescr.add d n !memo_normalize;
    let times = 
      map_sort
        (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])
        (Product.normal d)
    in
    let record = 
      map_sort
        (fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])
        (Record.get d)
    in
    define n { d with times = times; record = record };
    n

let normalize n =
  internalize (rec_normalize (descr n))


let apply t1 t2 = 
  failwith "apply: not yet implemented"
  

module Print =
struct
  let marks = Hashtbl.create 63
  let wh = ref []
  let count_name = ref 0
  let name () =
    incr count_name;
    "'a" ^ (string_of_int !count_name)

  let bool_iter f b =
    List.iter (fun (p,n) -> List.iter f p; List.iter f n) b

  let trivial b = b = Boolean.empty || b = Boolean.full

  let worth_abbrev d = 
    not (trivial d.times && trivial d.arrow && trivial d.record) 

  let rec mark n =
    let i = id n and d = descr n in
    try 
      let r = Hashtbl.find marks i in
      if (!r = None) && (worth_abbrev d) then 
        (let na = name () in 
         r := Some na;
         wh := (na,d) :: !wh
        )
    with Not_found -> 
      Hashtbl.add marks i (ref None);
      mark_descr d
  and mark_descr d = 
    bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
    bool_iter (fun (l,o,n) -> mark n) d.record

    
  let rec print_union ppf = function
    | [] -> Format.fprintf ppf "Empty"
    | [h] -> h ppf
    | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t

  let print_atom ppf a = Format.fprintf ppf "`%s" (atom_name a)

  let rec print ppf n =
(*    Format.fprintf ppf "[%i]" (id n); *)
    match !(Hashtbl.find marks (id n)) with
      | Some n -> Format.fprintf ppf "%s" n
      | None -> print_descr ppf (descr n)
  and print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
    print_union ppf 
      (Intervals.print d.ints @
       Strings.print d.strs @
       Atoms.print "AnyAtom" print_atom d.atoms @
       Boolean.print "(Any,Any)" print_times d.times @
       Boolean.print "(Empty -> Any)" print_arrow d.arrow @
       Boolean.print "{ }" print_record d.record
      )
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
  and print_record ppf (l,o,t) =
    Format.fprintf ppf "@[{ %s =%s %a }@]" 
      (label_name l) (if o then "?" else "") print t

          
  let end_print ppf =
    (match List.rev !wh with
       | [] -> ()
       | (na,d)::t ->
           Format.fprintf ppf " where@ @[%s = %a" na print_descr d;
           List.iter 
             (fun (na,d) -> Format.fprintf ppf " and@ %s = %a" na print_descr d)
             t;
           Format.fprintf ppf "@]"
    );
    Format.fprintf ppf "@]";
    count_name := 0;
    wh := [];
    Hashtbl.clear marks

  let print ppf n =
    mark n;
    Format.fprintf ppf "@[%a" print n;
    end_print ppf

  let print_descr ppf d =
    mark_descr d;
    Format.fprintf ppf "@[%a" print_descr d;
    end_print ppf
 
end

(*
let rec print_normal_record ppf = function
  | Success -> Format.fprintf ppf "Yes"
  | Fail -> Format.fprintf ppf "No"
  | FirstLabel (l,present,absent) ->
      Format.fprintf ppf "%s?@[<v>@\n" (label_name l);
      List.iter
        (fun (t,n) ->
           Format.fprintf ppf "(%a)=>@[%a@]@\n" 
             Print.print_descr t
             print_normal_record n
        ) present;
      if absent <> Fail then
        Format.fprintf ppf "(absent)=>@[%a@]@\n" print_normal_record absent;
      Format.fprintf ppf "@]" 
*)


(* 
let pr s = Types.Print.print Format.std_formatter (Syntax.make_type (Syntax.parse s));;

let pr' s = Types.Print.print Format.std_formatter 
   (Types.normalize (Syntax.make_type (Syntax.parse s)));;

BUG:
pr "'a | 'b where 'a = ('a , 'a) and 'b= ('b , 'b)";;
*)


(*
  let nr s =
    let t = Types.descr (Syntax.make_type (Syntax.parse s)) in
    let n = Types.normal_record' t.Types.record in
    Types.print_normal_record Format.std_formatter n;;
*)
1	open Recursive
2	open Printf
3
4
5
6	type label = int
7	type atom = int
8
9	type const = Integer of int \| Atom of atom \| String of string
10
11	module I = struct
12	type 'a t = {
13	ints : Intervals.t;
14	atoms : atom Atoms.t;
15	times : ('a * 'a) Boolean.t;
16	arrow : ('a * 'a) Boolean.t;
17	record: (label * bool * 'a) Boolean.t;
18	strs : Strings.t;
19	}
20
21	let empty = {
22	times = Boolean.empty;
23	arrow = Boolean.empty;
24	record= Boolean.empty;
25	ints = Intervals.empty;
26	atoms = Atoms.empty;
27	strs = Strings.empty;
28	}
29	let any = {
30	times = Boolean.full;
31	arrow = Boolean.full;
32	record= Boolean.full;
33	ints = Intervals.full;
34	atoms = Atoms.full;
35	strs = Strings.any;
36	}
37
38	let interval i j = { empty with ints = Intervals.atom (i,j) }
39	let times x y = { empty with times = Boolean.atom (x,y) }
40	let arrow x y = { empty with arrow = Boolean.atom (x,y) }
41	let record label opt t = { empty with record = Boolean.atom (label,opt,t) }
42	let atom a = { empty with atoms = Atoms.atom a }
43	let string r = { empty with strs = Strings.Regexp.compile r }
44	let constant = function
45	\| Integer i -> interval i i
46	\| Atom a -> atom a
47	\| String s -> string (Strings.Regexp.str s)
48
49
50	let any_record = { empty with record = any.record }
51
52	let cup x y =
53	if x = y then x else {
54	times = Boolean.cup x.times y.times;
55	arrow = Boolean.cup x.arrow y.arrow;
56	record= Boolean.cup x.record y.record;
57	ints = Intervals.cup x.ints y.ints;
58	atoms = Atoms.cup x.atoms y.atoms;
59	strs = Strings.cup x.strs y.strs;
60	}
61
62	let cap x y =
63	if x = y then x else {
64	times = Boolean.cap x.times y.times;
65	record= Boolean.cap x.record y.record;
66	arrow = Boolean.cap x.arrow y.arrow;
67	ints = Intervals.cap x.ints y.ints;
68	atoms = Atoms.cap x.atoms y.atoms;
69	strs = Strings.cap x.strs y.strs;
70	}
71
72	let diff x y =
73	if x = y then empty else {
74	times = Boolean.diff x.times y.times;
75	arrow = Boolean.diff x.arrow y.arrow;
76	record= Boolean.diff x.record y.record;
77	ints = Intervals.diff x.ints y.ints;
78	atoms = Atoms.diff x.atoms y.atoms;
79	strs = Strings.diff x.strs y.strs;
80	}
81
82	let neg x = diff any x
83
84	let equal e a b =
85	if a.ints <> b.ints then raise NotEqual;
86	if a.atoms <> b.atoms then raise NotEqual;
87	if a.strs <> b.strs then raise NotEqual;
88	Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;
89	Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;
90	Boolean.equal (fun (l1,o1,x1) (l2,o2,x2) ->
91	if (l1 <> l2) \|\| (o1 <> o2) then raise NotEqual;
92	e x1 x2) a.record b.record
93
94	let map f a =
95	{ times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;
96	arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;
97	record= Boolean.map (fun (l,o,x) -> (l,o, f x)) a.record;
98	ints = a.ints;
99	atoms = a.atoms;
100	strs = a.strs;
101	}
102
103	let hash h a =
104	Hashtbl.hash (map h a)
105
106	let iter f a =
107	ignore (map f a)
108
109	let deep = 4
110	end
111
112
113	module Algebra = Recursive.Make(I)
114	include I
115	include Algebra
116
117	let check d =
118	Boolean.check d.times;
119	Boolean.check d.arrow;
120	Boolean.check d.record;
121	()
122
123	(*
124	let define n d = check d; define n d
125	*)
126
127	let cons d =
128	let n = make () in
129	define n d;
130	internalize n
131
132
133	module Positive =
134	struct
135	type rhs = [ `Type of descr \| `Cup of v list \| `Times of v * v ]
136	and v = { mutable def : rhs; mutable node : node option }
137
138
139	let rec make_descr seen v =
140	if List.memq v seen then empty
141	else
142	let seen = v :: seen in
143	match v.def with
144	\| `Type d -> d
145	\| `Cup vl ->
146	List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
147	\| `Times (v1,v2) -> times (make_node v1) (make_node v2)
148
149	and make_node v =
150	match v.node with
151	\| Some n -> n
152	\| None ->
153	let n = make () in
154	v.node <- Some n;
155	let d = make_descr [] v in
156	define n d;
157	n
158
159	let forward () = { def = `Cup []; node = None }
160	let def v d = v.def <- d
161	let cons d = let v = forward () in def v d; v
162	let ty d = cons (`Type d)
163	let cup vl = cons (`Cup vl)
164	let times d1 d2 = cons (`Times (d1,d2))
165	let define v1 v2 = def v1 (`Cup [v2])
166
167	let solve v = internalize (make_node v)
168	end
169
170
171	let get_record r =
172	let add = SortedMap.add (fun (o1,t1) (o2,t2) -> (o1&&o2, cap t1 t2)) in
173	let line (p,n) =
174	let accu = List.fold_left
175	(fun accu (l,o,t) -> add l (o,descr t) accu) [] p in
176	List.fold_left
177	(fun accu (l,o,t) -> add l (not o,neg (descr t)) accu) accu n in
178	List.map line r
179
180
181	let counter_label = ref 0
182	let label_table = Hashtbl.create 63
183	let label_names = Hashtbl.create 63
184
185	let label s =
186	try Hashtbl.find label_table s
187	with Not_found ->
188	incr counter_label;
189	Hashtbl.add label_table s !counter_label;
190	Hashtbl.add label_names !counter_label s;
191	!counter_label
192
193	let label_name l =
194	Hashtbl.find label_names l
195
196	let mk_atom = label
197
198	let atom_name = label_name
199
200	(* Subtyping algorithm *)
201
202	let diff_t d t = diff d (descr t)
203	let cap_t d t = cap d (descr t)
204	let cap_product l =
205	List.fold_left
206	(fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
207	(any,any)
208	l
209
210
211	module Assumptions = Set.Make(struct type t = descr let compare = compare end)
212
213	let memo = ref Assumptions.empty
214	let cache_false = ref Assumptions.empty
215
216	exception NotEmpty
217
218	let rec empty_rec d =
219	if Assumptions.mem d !cache_false then false
220	else if Assumptions.mem d !memo then true
221	else if not (Intervals.is_empty d.ints) then false
222	else if not (Atoms.is_empty d.atoms) then false
223	else if not (Strings.is_empty d.strs) then false
224	else (
225	let backup = !memo in
226	memo := Assumptions.add d backup;
227	if
228	(empty_rec_times d.times) &&
229	(empty_rec_arrow d.arrow) &&
230	(empty_rec_record d.record)
231	then true
232	else (
233	memo := backup;
234	cache_false := Assumptions.add d !cache_false;
235	false
236	)
237	)
238
239	and empty_rec_times c =
240	List.for_all empty_rec_times_aux c
241
242	and empty_rec_times_aux (left,right) =
243	let rec aux accu1 accu2 = function
244	\| (t1,t2)::right ->
245	let accu1' = diff_t accu1 t1 in
246	if not (empty_rec accu1') then aux accu1' accu2 right;
247	let accu2' = diff_t accu2 t2 in
248	if not (empty_rec accu2') then aux accu1 accu2' right
249	\| [] -> raise NotEmpty
250	in
251	let (accu1,accu2) = cap_product left in
252	(empty_rec accu1) \|\| (empty_rec accu2) \|\|
253	(try aux accu1 accu2 right; true with NotEmpty -> false)
254
255	and empty_rec_arrow c =
256	List.for_all empty_rec_arrow_aux c
257
258	and empty_rec_arrow_aux (left,right) =
259	let single_right (s1,s2) =
260	let rec aux accu1 accu2 = function
261	\| (t1,t2)::left ->
262	let accu1' = diff_t accu1 t1 in
263	if not (empty_rec accu1') then aux accu1 accu2 left;
264	let accu2' = cap_t accu2 t2 in
265	if not (empty_rec accu2') then aux accu1 accu2 left
266	\| [] -> raise NotEmpty
267	in
268	let accu1 = descr s1 in
269	(empty_rec accu1) \|\|
270	(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
271	in
272	List.exists single_right right
273
274	and empty_rec_record c =
275	let aux = List.exists (fun (_,(opt,t)) -> (not opt) && (empty_rec t)) in
276	List.for_all aux (get_record c)
277
278	let is_empty d =
279	let r = empty_rec d in
280	memo := Assumptions.empty;
281	cache_false := Assumptions.empty;
282	r
283
284	let non_empty d =
285	not (is_empty d)
286
287	let subtype d1 d2 =
288	is_empty (diff d1 d2)
289
290	(* Sample value *)
291	module Sample =
292	struct
293
294	let rec find f = function
295	\| [] -> raise Not_found
296	\| x::r -> try f x with Not_found -> find f r
297
298	type t =
299	\| Int of int
300	\| Atom of atom
301	\| String of string
302	\| Pair of t * t
303	\| Record of (label * t) list
304	\| Fun of (node * node) list
305
306	let rec gen_atom i l =
307	if SortedList.mem l i then gen_atom (succ i) l else i
308
309	let rec sample_rec memo d =
310	if (Assumptions.mem d memo) \|\| (is_empty d) then raise Not_found
311	else
312	try Int (Intervals.sample d.ints) with Not_found ->
313	try Atom (Atoms.sample (gen_atom 0) d.atoms) with Not_found ->
314	try String (Strings.sample d.strs) with Not_found ->
315	try sample_rec_arrow d.arrow with Not_found ->
316
317	let memo = Assumptions.add d memo in
318	try sample_rec_times memo d.times with Not_found ->
319	try sample_rec_record memo d.record with Not_found ->
320	raise Not_found
321
322
323	and sample_rec_times memo c =
324	find (sample_rec_times_aux memo) c
325
326	and sample_rec_times_aux memo (left,right) =
327	let rec aux accu1 accu2 = function
328	\| (t1,t2)::right ->
329	let accu1' = diff_t accu1 t1 in
330	if non_empty accu1' then aux accu1' accu2 right else
331	let accu2' = diff_t accu2 t2 in
332	if non_empty accu2' then aux accu1 accu2' right else
333	raise Not_found
334	\| [] -> Pair (sample_rec memo accu1, sample_rec memo accu2)
335	in
336	let (accu1,accu2) = cap_product left in
337	if (is_empty accu1) \|\| (is_empty accu2) then raise Not_found;
338	aux accu1 accu2 right
339
340	and sample_rec_arrow c =
341	find sample_rec_arrow_aux c
342
343	and sample_rec_arrow_aux (left,right) =
344	let single_right (s1,s2) =
345	let rec aux accu1 accu2 = function
346	\| (t1,t2)::left ->
347	let accu1' = diff_t accu1 t1 in
348	if non_empty accu1' then aux accu1 accu2 left;
349	let accu2' = cap_t accu2 t2 in
350	if non_empty accu2' then aux accu1 accu2 left
351	\| [] -> raise NotEmpty
352	in
353	let accu1 = descr s1 in
354	(is_empty accu1) \|\|
355	(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
356	in
357	if List.exists single_right right then raise Not_found
358	else Fun left
359
360
361	and sample_rec_record memo c =
362	Record (find (sample_rec_record_aux memo) (get_record c))
363
364	and sample_rec_record_aux memo fields =
365	let aux acc (l,(o,t)) = if o then acc else (l, sample_rec memo t) :: acc in
366	List.fold_left aux [] fields
367
368	let get x = sample_rec Assumptions.empty x
369	end
370
371
372	module Product =
373	struct
374	type t = (descr * descr) list
375
376	let get d =
377	let line accu (left,right) =
378	let rec aux accu d1 d2 = function
379	\| (t1,t2)::right ->
380	let accu =
381	let d1 = diff_t d1 t1 in
382	if is_empty d1 then accu else aux accu d1 d2 right in
383	let accu =
384	let d2 = diff_t d2 t2 in
385	if is_empty d2 then accu else aux accu d1 d2 right in
386	accu
387	\| [] -> (d1,d2) :: accu
388	in
389	let (d1,d2) = cap_product left in
390	if (is_empty d1) \|\| (is_empty d2) then accu else aux accu d1 d2 right
391	in
392	List.fold_left line [] d.times
393
394	let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
395	let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
396
397	let restrict_1 rects pi1 =
398	let aux accu (t1,t2) =
399	let t1 = cap t1 pi1 in if is_empty t1 then accu else (t1,t2)::accu in
400	List.fold_left aux [] rects
401
402	type normal = t
403
404	let normal d =
405	let res = ref [] in
406
407	let add (t1,t2) =
408	let rec loop t1 t2 = function
409	\| [] -> res := (ref (t1,t2)) :: !res
410	\| ({contents = (d1,d2)} as r)::l ->
411	(OPT)
412	if d1 = t1 then r := (d1,cup d2 t2) else
413
414	let i = cap t1 d1 in
415	if is_empty i then loop t1 t2 l
416	else (
417	r := (i, cup t2 d2);
418	let k = diff d1 t1 in
419	if non_empty k then res := (ref (k,d2)) :: !res;
420
421	let j = diff t1 d1 in
422	if non_empty j then loop j t2 l
423	)
424	in
425	loop t1 t2 !res
426	in
427	List.iter add (get d);
428	List.map (!) !res
429
430	let any = { empty with times = any.times }
431	end
432
433
434	module Record =
435	struct
436	type t = (label, (bool * descr)) SortedMap.t list
437
438	let get d =
439	let line r = List.for_all (fun (l,(o,d)) -> o \|\| non_empty d) r in
440	List.filter line (get_record d.record)
441
442
443	let restrict_label_present t l =
444	let aux = SortedMap.change l (fun (_,d) -> (false,d)) (false,any) in
445	List.map aux t
446
447	let restrict_label_absent t l =
448	let restr = function (true, _) -> (true,empty) \| _ -> raise Exit in
449	let aux accu r =
450	try SortedMap.change l restr (true,empty) r :: accu
451	with Exit -> accu in
452	List.fold_left aux [] t
453
454	let restrict_field t l d =
455	let restr (_,d1) =
456	let d1 = cap d d1 in
457	if is_empty d1 then raise Exit else (false,d1) in
458	let aux accu r =
459	try SortedMap.change l restr (false,d) r :: accu
460	with Exit -> accu in
461	List.fold_left aux [] t
462
463	let project_field t l =
464	let aux accu x =
465	match List.assoc l x with
466	\| (false,t) -> cup accu t
467	\| _ -> raise Not_found
468	in
469	List.fold_left aux empty t
470
471	type normal =
472	[ `Success
473	\| `Fail
474	\| `Label of label * (descr * normal) list * normal ]
475
476	let rec merge_record n r =
477	match (n, r) with
478	\| (`Success, _) \| (_, []) -> `Success
479	\| (`Fail, r) ->
480	let aux (l,(o,t)) n = `Label (l, [t,n], if o then n else `Fail) in
481	List.fold_right aux r `Success
482	\| (`Label (l1,present,absent), (l2,(o,t2))::r') ->
483	if (l1 < l2) then
484	let pr = List.map (fun (t,x) -> (t, merge_record x r)) present in
485	`Label (l1,pr,merge_record absent r)
486	else if (l2 < l1) then
487	let n' = merge_record n r' in
488	`Label (l2, [t2, n'], if o then n' else n)
489	else
490	let res = ref [] in
491	let aux a (t,x) =
492	(let t = diff t t2 in
493	if non_empty t then res := (t,x) :: !res);
494	(let t = cap t t2 in
495	if non_empty t then res := (t, merge_record x r') :: !res);
496	diff a t
497	in
498	let t2 = List.fold_left aux t2 present in
499	let () =
500	if non_empty t2 then
501	res := (t2, merge_record `Fail r') :: !res in
502	let abs = if o then merge_record absent r' else absent in
503	`Label (l1, !res, abs)
504
505
506	let normal d =
507	List.fold_left merge_record `Fail (get d)
508
509	let project d l =
510	let aux accu x =
511	match List.assoc l x with
512	\| (false,t) -> cup accu t
513	\| _ -> raise Not_found
514	in
515	List.fold_left aux empty (get_record d.record)
516
517	let any = { empty with record = any.record }
518	let is_empty d = d = []
519	end
520
521
522	module MapDescr = Map.Make(struct type t = descr let compare = compare end)
523
524	let memo_normalize = ref MapDescr.empty
525
526	let map_sort f l =
527	SortedList.from_list (List.map f l)
528
529	let rec rec_normalize d =
530	try MapDescr.find d !memo_normalize
531	with Not_found ->
532	let n = make () in
533	memo_normalize := MapDescr.add d n !memo_normalize;
534	let times =
535	map_sort
536	(fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])
537	(Product.normal d)
538	in
539	let record =
540	map_sort
541	(fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])
542	(Record.get d)
543	in
544	define n { d with times = times; record = record };
545	n
546
547	let normalize n =
548	internalize (rec_normalize (descr n))
549
550
551	let apply t1 t2 =
552	failwith "apply: not yet implemented"
553
554
555	module Print =
556	struct
557	let marks = Hashtbl.create 63
558	let wh = ref []
559	let count_name = ref 0
560	let name () =
561	incr count_name;
562	"'a" ^ (string_of_int !count_name)
563
564	let bool_iter f b =
565	List.iter (fun (p,n) -> List.iter f p; List.iter f n) b
566
567	let trivial b = b = Boolean.empty \|\| b = Boolean.full
568
569	let worth_abbrev d =
570	not (trivial d.times && trivial d.arrow && trivial d.record)
571
572	let rec mark n =
573	let i = id n and d = descr n in
574	try
575	let r = Hashtbl.find marks i in
576	if (!r = None) && (worth_abbrev d) then
577	(let na = name () in
578	r := Some na;
579	wh := (na,d) :: !wh
580	)
581	with Not_found ->
582	Hashtbl.add marks i (ref None);
583	mark_descr d
584	and mark_descr d =
585	bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;
586	bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
587	bool_iter (fun (l,o,n) -> mark n) d.record
588
589
590	let rec print_union ppf = function
591	\| [] -> Format.fprintf ppf "Empty"
592	\| [h] -> h ppf
593	\| h::t -> Format.fprintf ppf "@[%t \|@ %a@]" h print_union t
594
595	let print_atom ppf a = Format.fprintf ppf "`%s" (atom_name a)
596
597	let rec print ppf n =
598	(* Format.fprintf ppf "[%i]" (id n); *)
599	match !(Hashtbl.find marks (id n)) with
600	\| Some n -> Format.fprintf ppf "%s" n
601	\| None -> print_descr ppf (descr n)
602	and print_descr ppf d =
603	if d = any then Format.fprintf ppf "Any" else
604	print_union ppf
605	(Intervals.print d.ints @
606	Strings.print d.strs @
607	Atoms.print "AnyAtom" print_atom d.atoms @
608	Boolean.print "(Any,Any)" print_times d.times @
609	Boolean.print "(Empty -> Any)" print_arrow d.arrow @
610	Boolean.print "{ }" print_record d.record
611	)
612	and print_times ppf (t1,t2) =
613	Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
614	and print_arrow ppf (t1,t2) =
615	Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
616	and print_record ppf (l,o,t) =
617	Format.fprintf ppf "@[{ %s =%s %a }@]"
618	(label_name l) (if o then "?" else "") print t
619
620
621	let end_print ppf =
622	(match List.rev !wh with
623	\| [] -> ()
624	\| (na,d)::t ->
625	Format.fprintf ppf " where@ @[%s = %a" na print_descr d;
626	List.iter
627	(fun (na,d) -> Format.fprintf ppf " and@ %s = %a" na print_descr d)
628	t;
629	Format.fprintf ppf "@]"
630	);
631	Format.fprintf ppf "@]";
632	count_name := 0;
633	wh := [];
634	Hashtbl.clear marks
635
636	let print ppf n =
637	mark n;
638	Format.fprintf ppf "@[%a" print n;
639	end_print ppf
640
641	let print_descr ppf d =
642	mark_descr d;
643	Format.fprintf ppf "@[%a" print_descr d;
644	end_print ppf
645
646	end
647
648	(*
649	let rec print_normal_record ppf = function
650	\| Success -> Format.fprintf ppf "Yes"
651	\| Fail -> Format.fprintf ppf "No"
652	\| FirstLabel (l,present,absent) ->
653	Format.fprintf ppf "%s?@[<v>@\n" (label_name l);
654	List.iter
655	(fun (t,n) ->
656	Format.fprintf ppf "(%a)=>@[%a@]@\n"
657	Print.print_descr t
658	print_normal_record n
659	) present;
660	if absent <> Fail then
661	Format.fprintf ppf "(absent)=>@[%a@]@\n" print_normal_record absent;
662	Format.fprintf ppf "@]"
663	*)
664
665
666	(*
667	let pr s = Types.Print.print Format.std_formatter (Syntax.make_type (Syntax.parse s));;
668
669	let pr' s = Types.Print.print Format.std_formatter
670	(Types.normalize (Syntax.make_type (Syntax.parse s)));;
671
672	BUG:
673	pr "'a \| 'b where 'a = ('a , 'a) and 'b= ('b , 'b)";;
674	*)
675
676
677	(*
678	let nr s =
679	let t = Types.descr (Syntax.make_type (Syntax.parse s)) in
680	let n = Types.normal_record' t.Types.record in
681	Types.print_normal_record Format.std_formatter n;;
682	*)