viewcvs.cgi/types/types.ml

open Recursive
open Printf


type label = int
type atom  = int

type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t

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;
    chars : Chars.t;
  }

  let empty = { 
    times = Boolean.empty; 
    arrow = Boolean.empty; 
    record= Boolean.empty;
    ints  = Intervals.empty;
    atoms = Atoms.empty;
    chars = Chars.empty;
  }

  let any =  {
    times = Boolean.full; 
    arrow = Boolean.full; 
    record= Boolean.full; 
    ints  = Intervals.any;
    atoms = Atoms.full;
    chars = Chars.full;
  }
               
  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 char c = { empty with chars = Chars.atom c }
  let char_class c1 c2 = { empty with chars = Chars.char_class c1 c2 }
  let constant = function
    | Integer i -> interval i i
    | Atom a -> atom a
    | Char c -> char c

                   
  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;
      chars = Chars.cup x.chars y.chars;
    }
      
  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;
      chars = Chars.cap x.chars y.chars;
    }
      
  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;
      chars = Chars.diff x.chars y.chars;
    }

  let neg x = diff any x
                   
  let equal e a b =
    if not (Intervals.equal a.ints b.ints) then raise NotEqual;
    if a.atoms <> b.atoms then raise NotEqual;
    if a.chars <> b.chars 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;
      chars = a.chars;
    }
    
  let hash h a =
    (Hashtbl.hash { map h a with ints = Intervals.empty })
    + (Intervals.hash a.ints)
      
  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 (Chars.is_empty d.chars) 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 Big_int.big_int
  | Atom of atom
  | Char of Chars.Unichar.t
  | 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 Char (Chars.sample d.chars) 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))

module Print =
struct
  module DescrHash = 
    Hashtbl.Make(
      struct 
        type t = descr
        let hash = hash_descr
        let equal = (=)
      end
    )

  let named = DescrHash.create 10
  let register_global name d = DescrHash.add named d name

  let marks = DescrHash.create 63
  let wh = ref []
  let count_name = ref 0
  let name () =
    incr count_name;
    "X" ^ (string_of_int !count_name)
(* TODO: 
   check that these generated names does not conflict with declared types *)

  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 = mark_descr (descr n)
  and mark_descr d =
    if not (DescrHash.mem named d) then
      try 
        let r = DescrHash.find marks d in
        if (!r = None) && (worth_abbrev d) then 
          let na = name () in 
          r := Some na;
          wh := (na,d) :: !wh
      with Not_found -> 
        DescrHash.add marks d (ref None);
        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 = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
      let name = DescrHash.find named d in
      Format.fprintf ppf "%s" name
    with Not_found ->
      match !(DescrHash.find marks d) with
        | Some n -> Format.fprintf ppf "%s" n
        | None -> real_print_descr ppf d
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
      print_union ppf 
        (Intervals.print d.ints @
         Chars.print d.chars @
         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 real_print_descr d;
           List.iter 
             (fun (na,d) -> 
                Format.fprintf ppf " and@ %s = %a" na real_print_descr d)
             t;
           Format.fprintf ppf "@]"
    );
    Format.fprintf ppf "@]";
    count_name := 0;
    wh := [];
    DescrHash.clear marks

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

   let print ppf n = print_descr ppf (descr n)

  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 "%s" (Big_int.string_of_big_int i)
    | Sample.Atom a -> Format.fprintf ppf "`%s" (atom_name a)
    | Sample.Char c -> Chars.Unichar.print ppf c
    | 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

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

  let get t =
    List.fold_left
      (fun ((dom,arr) as accu) (left,right) ->
         if Sample.check_empty_arrow_line left right 
         then accu
         else (
           let left =
             List.map 
               (fun (t,s) -> (descr t, descr s)) left in
           let d = List.fold_left (fun d (t,_) -> cup d t) empty left in
           (cap dom d, left :: arr)
         )
      )
      (any, [])
      t.arrow

  let domain (dom,_) = dom

  let apply_simple t result left = 
    let rec aux result accu1 accu2 = function
      | (t1,s1)::left ->
          let result = 
            let accu1 = diff accu1 t1 in
            if non_empty accu1 then aux result accu1 accu2 left
            else result in
          let result =
            let accu2 = cap accu2 s1 in
            aux result accu1 accu2 left in
          result
      | [] -> 
          if subtype accu2 result 
          then result
          else cup result accu2
    in
    aux result t any left
      
  let apply (_,arr) t =
    List.fold_left (apply_simple t) empty arr

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