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 check_empty_simple_arrow_line left (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)

and check_empty_arrow_line left right = 
  List.exists (check_empty_simple_arrow_line left) right

and sample_rec_arrow_aux (left,right) =
  if (check_empty_arrow_line left 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_simple result left t = 
  let ok = ref false in
  let rec aux result accu1 accu2 = function
    | (t1,s1)::left ->
        let result = 
          let accu1 = diff_t accu1 t1 in
          if non_empty accu1 then aux result accu1 accu2 left
          else (ok := true; result) in
        let result =
          let accu2 = cap_t accu2 s1 in
          aux result accu1 accu2 left in
        result
    | [] -> 
        if subtype accu2 result 
        then result
        else cup result accu2
  in
  let result = aux result t any left in
  if !ok then result else raise Not_found

let apply t1 t2 =
  if is_empty t2 
  then empty
  else
    if non_empty {t1 with arrow = []} 
    then raise Not_found
    else
      List.fold_left
        (fun accu (left,right) ->
           if Sample.check_empty_arrow_line left right 
           then accu 
           else
             apply_simple accu left t2
        )
        empty
        t1.arrow
  

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
 
  let rec print_sep f sep ppf = function
    | [] -> ()
    | [x] -> f ppf x
    | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem


  let rec print_sample ppf = function
    | Sample.Int i -> Format.fprintf ppf "%i" i
    | Sample.Atom a -> Format.fprintf ppf "`%s" (atom_name a)
    | Sample.String s -> Format.fprintf ppf "%S" s
    | Sample.Pair (x1,x2) -> 
        Format.fprintf ppf "(%a,%a)" 
        print_sample x1
        print_sample x2
    | Sample.Record r ->
        Format.fprintf ppf "{ %a }"
          (print_sep 
             (fun ppf (l,x) -> 
                Format.fprintf ppf "%s = %a"
                (label_name l)
                print_sample x
             )
             " ; "
          ) r
    | Sample.Fun iface ->
        Format.fprintf ppf "(fun ( %a ) x -> ...)"
          (print_sep
             (fun ppf (t1,t2) ->
                Format.fprintf ppf "%a -> %a; "
                print t1 print t2
             )
             " ; "
          ) iface
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	abate	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	abate	8	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	abate	1	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	abate	10	and check_empty_simple_arrow_line left (s1,s2) =
344			let rec aux accu1 accu2 = function
345			\| (t1,t2)::left ->
346			let accu1' = diff_t accu1 t1 in
347			if non_empty accu1' then aux accu1 accu2 left;
348			let accu2' = cap_t accu2 t2 in
349			if non_empty accu2' then aux accu1 accu2 left
350			\| [] -> raise NotEmpty
351			in
352			let accu1 = descr s1 in
353			(is_empty accu1) \|\|
354			(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
355
356			and check_empty_arrow_line left right =
357			List.exists (check_empty_simple_arrow_line left) right
358
359	abate	1	and sample_rec_arrow_aux (left,right) =
360	abate	10	if (check_empty_arrow_line left right) then raise Not_found
361	abate	1	else Fun left
362
363
364			and sample_rec_record memo c =
365			Record (find (sample_rec_record_aux memo) (get_record c))
366
367			and sample_rec_record_aux memo fields =
368			let aux acc (l,(o,t)) = if o then acc else (l, sample_rec memo t) :: acc in
369			List.fold_left aux [] fields
370
371			let get x = sample_rec Assumptions.empty x
372	abate	10
373	abate	1	end
374
375
376			module Product =
377			struct
378			type t = (descr * descr) list
379
380			let get d =
381			let line accu (left,right) =
382			let rec aux accu d1 d2 = function
383			\| (t1,t2)::right ->
384			let accu =
385			let d1 = diff_t d1 t1 in
386			if is_empty d1 then accu else aux accu d1 d2 right in
387			let accu =
388			let d2 = diff_t d2 t2 in
389			if is_empty d2 then accu else aux accu d1 d2 right in
390			accu
391			\| [] -> (d1,d2) :: accu
392			in
393			let (d1,d2) = cap_product left in
394			if (is_empty d1) \|\| (is_empty d2) then accu else aux accu d1 d2 right
395			in
396			List.fold_left line [] d.times
397
398			let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
399			let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
400
401			let restrict_1 rects pi1 =
402			let aux accu (t1,t2) =
403			let t1 = cap t1 pi1 in if is_empty t1 then accu else (t1,t2)::accu in
404			List.fold_left aux [] rects
405
406			type normal = t
407
408			let normal d =
409			let res = ref [] in
410
411			let add (t1,t2) =
412			let rec loop t1 t2 = function
413			\| [] -> res := (ref (t1,t2)) :: !res
414			\| ({contents = (d1,d2)} as r)::l ->
415			(OPT)
416			if d1 = t1 then r := (d1,cup d2 t2) else
417
418			let i = cap t1 d1 in
419			if is_empty i then loop t1 t2 l
420			else (
421			r := (i, cup t2 d2);
422			let k = diff d1 t1 in
423			if non_empty k then res := (ref (k,d2)) :: !res;
424
425			let j = diff t1 d1 in
426			if non_empty j then loop j t2 l
427			)
428			in
429			loop t1 t2 !res
430			in
431			List.iter add (get d);
432			List.map (!) !res
433
434			let any = { empty with times = any.times }
435			end
436
437
438			module Record =
439			struct
440			type t = (label, (bool * descr)) SortedMap.t list
441
442			let get d =
443			let line r = List.for_all (fun (l,(o,d)) -> o \|\| non_empty d) r in
444			List.filter line (get_record d.record)
445
446
447			let restrict_label_present t l =
448			let aux = SortedMap.change l (fun (_,d) -> (false,d)) (false,any) in
449			List.map aux t
450
451			let restrict_label_absent t l =
452			let restr = function (true, _) -> (true,empty) \| _ -> raise Exit in
453			let aux accu r =
454			try SortedMap.change l restr (true,empty) r :: accu
455			with Exit -> accu in
456			List.fold_left aux [] t
457
458			let restrict_field t l d =
459			let restr (_,d1) =
460			let d1 = cap d d1 in
461			if is_empty d1 then raise Exit else (false,d1) in
462			let aux accu r =
463			try SortedMap.change l restr (false,d) r :: accu
464			with Exit -> accu in
465			List.fold_left aux [] t
466
467			let project_field t l =
468			let aux accu x =
469			match List.assoc l x with
470			\| (false,t) -> cup accu t
471			\| _ -> raise Not_found
472			in
473			List.fold_left aux empty t
474
475			type normal =
476			[ `Success
477			\| `Fail
478			\| `Label of label * (descr * normal) list * normal ]
479
480			let rec merge_record n r =
481			match (n, r) with
482			\| (`Success, _) \| (_, []) -> `Success
483			\| (`Fail, r) ->
484			let aux (l,(o,t)) n = `Label (l, [t,n], if o then n else `Fail) in
485			List.fold_right aux r `Success
486			\| (`Label (l1,present,absent), (l2,(o,t2))::r') ->
487			if (l1 < l2) then
488			let pr = List.map (fun (t,x) -> (t, merge_record x r)) present in
489			`Label (l1,pr,merge_record absent r)
490			else if (l2 < l1) then
491			let n' = merge_record n r' in
492			`Label (l2, [t2, n'], if o then n' else n)
493			else
494			let res = ref [] in
495			let aux a (t,x) =
496			(let t = diff t t2 in
497			if non_empty t then res := (t,x) :: !res);
498			(let t = cap t t2 in
499			if non_empty t then res := (t, merge_record x r') :: !res);
500			diff a t
501			in
502			let t2 = List.fold_left aux t2 present in
503			let () =
504			if non_empty t2 then
505			res := (t2, merge_record `Fail r') :: !res in
506			let abs = if o then merge_record absent r' else absent in
507			`Label (l1, !res, abs)
508
509
510			let normal d =
511			List.fold_left merge_record `Fail (get d)
512
513			let project d l =
514			let aux accu x =
515			match List.assoc l x with
516			\| (false,t) -> cup accu t
517			\| _ -> raise Not_found
518			in
519			List.fold_left aux empty (get_record d.record)
520
521			let any = { empty with record = any.record }
522			let is_empty d = d = []
523			end
524
525
526			module MapDescr = Map.Make(struct type t = descr let compare = compare end)
527
528			let memo_normalize = ref MapDescr.empty
529
530			let map_sort f l =
531			SortedList.from_list (List.map f l)
532
533			let rec rec_normalize d =
534			try MapDescr.find d !memo_normalize
535			with Not_found ->
536			let n = make () in
537			memo_normalize := MapDescr.add d n !memo_normalize;
538			let times =
539			map_sort
540			(fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])
541			(Product.normal d)
542			in
543			let record =
544			map_sort
545			(fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])
546			(Record.get d)
547			in
548			define n { d with times = times; record = record };
549			n
550
551			let normalize n =
552			internalize (rec_normalize (descr n))
553	abate	6
554	abate	10	let apply_simple result left t =
555			let ok = ref false in
556			let rec aux result accu1 accu2 = function
557			\| (t1,s1)::left ->
558			let result =
559			let accu1 = diff_t accu1 t1 in
560			if non_empty accu1 then aux result accu1 accu2 left
561			else (ok := true; result) in
562			let result =
563			let accu2 = cap_t accu2 s1 in
564			aux result accu1 accu2 left in
565			result
566			\| [] ->
567			if subtype accu2 result
568			then result
569			else cup result accu2
570			in
571			let result = aux result t any left in
572			if !ok then result else raise Not_found
573	abate	6
574	abate	10	let apply t1 t2 =
575			if is_empty t2
576			then empty
577			else
578			if non_empty {t1 with arrow = []}
579			then raise Not_found
580			else
581			List.fold_left
582			(fun accu (left,right) ->
583			if Sample.check_empty_arrow_line left right
584			then accu
585			else
586			apply_simple accu left t2
587			)
588			empty
589			t1.arrow
590	abate	1
591
592			module Print =
593			struct
594			let marks = Hashtbl.create 63
595			let wh = ref []
596			let count_name = ref 0
597			let name () =
598			incr count_name;
599			"'a" ^ (string_of_int !count_name)
600
601			let bool_iter f b =
602			List.iter (fun (p,n) -> List.iter f p; List.iter f n) b
603
604			let trivial b = b = Boolean.empty \|\| b = Boolean.full
605
606			let worth_abbrev d =
607			not (trivial d.times && trivial d.arrow && trivial d.record)
608
609			let rec mark n =
610			let i = id n and d = descr n in
611			try
612			let r = Hashtbl.find marks i in
613			if (!r = None) && (worth_abbrev d) then
614			(let na = name () in
615			r := Some na;
616			wh := (na,d) :: !wh
617			)
618			with Not_found ->
619			Hashtbl.add marks i (ref None);
620			mark_descr d
621			and mark_descr d =
622			bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;
623			bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
624			bool_iter (fun (l,o,n) -> mark n) d.record
625
626
627			let rec print_union ppf = function
628			\| [] -> Format.fprintf ppf "Empty"
629			\| [h] -> h ppf
630			\| h::t -> Format.fprintf ppf "@[%t \|@ %a@]" h print_union t
631
632			let print_atom ppf a = Format.fprintf ppf "`%s" (atom_name a)
633
634			let rec print ppf n =
635			(* Format.fprintf ppf "[%i]" (id n); *)
636			match !(Hashtbl.find marks (id n)) with
637			\| Some n -> Format.fprintf ppf "%s" n
638			\| None -> print_descr ppf (descr n)
639			and print_descr ppf d =
640			if d = any then Format.fprintf ppf "Any" else
641			print_union ppf
642			(Intervals.print d.ints @
643			Strings.print d.strs @
644			Atoms.print "AnyAtom" print_atom d.atoms @
645			Boolean.print "(Any,Any)" print_times d.times @
646			Boolean.print "(Empty -> Any)" print_arrow d.arrow @
647			Boolean.print "{ }" print_record d.record
648			)
649			and print_times ppf (t1,t2) =
650			Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
651			and print_arrow ppf (t1,t2) =
652			Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
653			and print_record ppf (l,o,t) =
654			Format.fprintf ppf "@[{ %s =%s %a }@]"
655			(label_name l) (if o then "?" else "") print t
656
657
658			let end_print ppf =
659			(match List.rev !wh with
660			\| [] -> ()
661			\| (na,d)::t ->
662			Format.fprintf ppf " where@ @[%s = %a" na print_descr d;
663			List.iter
664			(fun (na,d) -> Format.fprintf ppf " and@ %s = %a" na print_descr d)
665			t;
666			Format.fprintf ppf "@]"
667			);
668			Format.fprintf ppf "@]";
669			count_name := 0;
670			wh := [];
671			Hashtbl.clear marks
672
673			let print ppf n =
674			mark n;
675			Format.fprintf ppf "@[%a" print n;
676			end_print ppf
677
678			let print_descr ppf d =
679			mark_descr d;
680			Format.fprintf ppf "@[%a" print_descr d;
681			end_print ppf
682
683	abate	10	let rec print_sep f sep ppf = function
684			\| [] -> ()
685			\| [x] -> f ppf x
686			\| x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem
687
688
689			let rec print_sample ppf = function
690			\| Sample.Int i -> Format.fprintf ppf "%i" i
691			\| Sample.Atom a -> Format.fprintf ppf "`%s" (atom_name a)
692			\| Sample.String s -> Format.fprintf ppf "%S" s
693			\| Sample.Pair (x1,x2) ->
694			Format.fprintf ppf "(%a,%a)"
695			print_sample x1
696			print_sample x2
697			\| Sample.Record r ->
698			Format.fprintf ppf "{ %a }"
699			(print_sep
700			(fun ppf (l,x) ->
701			Format.fprintf ppf "%s = %a"
702			(label_name l)
703			print_sample x
704			)
705			" ; "
706			) r
707			\| Sample.Fun iface ->
708			Format.fprintf ppf "(fun ( %a ) x -> ...)"
709			(print_sep
710			(fun ppf (t1,t2) ->
711			Format.fprintf ppf "%a -> %a; "
712			print t1 print t2
713			)
714			" ; "
715			) iface
716	abate	1	end
717
718			(*
719			let rec print_normal_record ppf = function
720			\| Success -> Format.fprintf ppf "Yes"
721			\| Fail -> Format.fprintf ppf "No"
722			\| FirstLabel (l,present,absent) ->
723			Format.fprintf ppf "%s?@[<v>@\n" (label_name l);
724			List.iter
725			(fun (t,n) ->
726			Format.fprintf ppf "(%a)=>@[%a@]@\n"
727			Print.print_descr t
728			print_normal_record n
729			) present;
730			if absent <> Fail then
731			Format.fprintf ppf "(absent)=>@[%a@]@\n" print_normal_record absent;
732			Format.fprintf ppf "@]"
733			*)
734
735
736			(*
737			let pr s = Types.Print.print Format.std_formatter (Syntax.make_type (Syntax.parse s));;
738
739			let pr' s = Types.Print.print Format.std_formatter
740			(Types.normalize (Syntax.make_type (Syntax.parse s)));;
741
742			BUG:
743			pr "'a \| 'b where 'a = ('a , 'a) and 'b= ('b , 'b)";;
744			*)
745
746
747			(*
748			let nr s =
749			let t = Types.descr (Syntax.make_type (Syntax.parse s)) in
750			let n = Types.normal_record' t.Types.record in
751			Types.print_normal_record Format.std_formatter n;;
752			*)