viewcvs.cgi/types/type_bool.ml

open Recursive
open Printf

let equal_list e l1 l2 =
  if List.length l1 <> List.length l2 then raise NotEqual;
  List.iter2 e l1 l2

let equal_line e (p1,n1) (p2,n2) =
  equal_list e p1 p2;
  equal_list e n1 n2

let equal_bool e a b =
  equal_list (equal_line e) a b


module E = struct
  (* Internal algebra *)

  module I = struct
    type 'a t = {
      times : ('a * 'a) Boolean.t;
      arrow : ('a * 'a) Boolean.t;
      atom  : string Boolean.t
    }

    let empty = { 
      times = Boolean.empty; 
      arrow = Boolean.empty; 
      atom = Boolean.empty 
    }
    let any =  {
      times = Boolean.full; 
      arrow = Boolean.full; 
      atom = Boolean.full 
    }
                  
    let atom x = { empty with atom = Boolean.atom x }
    let times x y = { empty with times = Boolean.atom (x,y) }
    let arrow x y = { empty with arrow = Boolean.atom (x,y) }
    let cup x y = { 
      times = Boolean.cup x.times y.times;
      arrow = Boolean.cup x.arrow y.arrow;
      atom  = Boolean.cup x.atom  y.atom
    }
    let cap x y = { 
      times = Boolean.cap x.times y.times;
      arrow = Boolean.cap x.arrow y.arrow;
      atom  = Boolean.cap x.atom  y.atom
    }
    let diff x y = { 
      times = Boolean.diff x.times y.times;
      arrow = Boolean.diff x.arrow y.arrow;
      atom  = Boolean.diff x.atom  y.atom
    }
                  
    let equal e a b =
      equal_bool 
        (fun (x:string) (y:string) -> if x <> y then raise NotEqual) 
        a.atom b.atom;
      equal_bool (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;
      equal_bool (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow
        
    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;
        atom  = a.atom }
      
    let hash h a =
      Hashtbl.hash (map h a)

    let iter f a =
      ignore (map f a)
        
    let deep = 4
  end

  type t =
    | Arrow of t * t
    | Times of t * t
    | Diff  of t * t
    | Or    of t * t
    | And   of t * t
    | Atom  of string
    | Var   of string
        
  let make_parser expr = 
    EXTEND
      expr: [ 
          [ x = expr; "->"; y = expr -> Arrow (x,y) ]
        | [ x = expr; "*"; y = expr -> Times (x,y) ]
        | [ x = expr; "&"; y = expr -> And (x,y) 
          | x = expr; "-"; y = expr -> Diff (x,y) ]
        | [ x = expr; "|"; y = expr -> Or (x,y) ] 
        | [ "~"; x = expr -> Diff (Atom "Any", x)
          | a = LIDENT -> Var a
          | a = UIDENT -> Atom a
          | "("; x = expr; ")" -> x ] 
      ];
    END

  let rec compile f var = function
    | Atom "Any" -> I.any
    | Atom "Empty" -> I.empty
    | Atom i -> I.atom i
    | Times (a,b) -> I.times (f a) (f b)
    | Arrow (a,b) -> I.arrow (f a) (f b)
    | Diff (a,b) ->  I.diff (compile f var a) (compile f var b)
    | And (a,b) -> I.cap (compile f var a) (compile f var b)
    | Or (a,b) -> I.cup (compile f var a) (compile f var b)
    | Var v ->
        (try var v 
         with Exit -> failwith ("Cyclic definition for " ^ v))


  let rec print_list oc f sep un = function
    | [] -> fprintf oc "%s" un
    | [h] -> f oc h
    | h::t -> f oc h; fprintf oc "%s" sep; print_list oc f sep un t

  let print_line u f oc (p,n) =
    print_list oc f " & " u p;
    if n <> [] then
      (
        fprintf oc " \ ";
        print_list oc f " \ " "Empty" n
      )
      
  let print_bool u oc f a =
    print_list oc (print_line u f) " | " "Empty" a


  let print_arrow f oc (i1,i2) =
  fprintf oc "%a -> %a" f i1 f i2

  let print_times f oc (i1,i2) = 
    fprintf oc "%a * %a" f i1 f i2

  let print_atom f oc x =
    fprintf oc "%s" x


  let print f oc d =
    let b = ref false in
    if d.I.atom <> [] then
      (
        print_bool "AnyAtom" oc (print_atom f) d.I.atom;
        b := true
      );
    if d.I.times <> [] then
      (
        if !b then fprintf oc " | ";
        print_bool "AnyProd" oc (print_times f) d.I.times;
        b := true;
      );
    if d.I.arrow <> [] then
      (
        if !b then fprintf oc " | ";
        print_bool "AnyFun" oc (print_arrow f) d.I.arrow;
        b := true;
      );
    if not !b then fprintf oc "Empty"
end

module M = Example.Make(E)

let _ = M.main ()

1	open Recursive
2	open Printf
3
4	let equal_list e l1 l2 =
5	if List.length l1 <> List.length l2 then raise NotEqual;
6	List.iter2 e l1 l2
7
8	let equal_line e (p1,n1) (p2,n2) =
9	equal_list e p1 p2;
10	equal_list e n1 n2
11
12	let equal_bool e a b =
13	equal_list (equal_line e) a b
14
15
16	module E = struct
17	(* Internal algebra *)
18
19	module I = struct
20	type 'a t = {
21	times : ('a * 'a) Boolean.t;
22	arrow : ('a * 'a) Boolean.t;
23	atom : string Boolean.t
24	}
25
26	let empty = {
27	times = Boolean.empty;
28	arrow = Boolean.empty;
29	atom = Boolean.empty
30	}
31	let any = {
32	times = Boolean.full;
33	arrow = Boolean.full;
34	atom = Boolean.full
35	}
36
37	let atom x = { empty with atom = Boolean.atom x }
38	let times x y = { empty with times = Boolean.atom (x,y) }
39	let arrow x y = { empty with arrow = Boolean.atom (x,y) }
40	let cup x y = {
41	times = Boolean.cup x.times y.times;
42	arrow = Boolean.cup x.arrow y.arrow;
43	atom = Boolean.cup x.atom y.atom
44	}
45	let cap x y = {
46	times = Boolean.cap x.times y.times;
47	arrow = Boolean.cap x.arrow y.arrow;
48	atom = Boolean.cap x.atom y.atom
49	}
50	let diff x y = {
51	times = Boolean.diff x.times y.times;
52	arrow = Boolean.diff x.arrow y.arrow;
53	atom = Boolean.diff x.atom y.atom
54	}
55
56	let equal e a b =
57	equal_bool
58	(fun (x:string) (y:string) -> if x <> y then raise NotEqual)
59	a.atom b.atom;
60	equal_bool (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;
61	equal_bool (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow
62
63	let map f a =
64	{ times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;
65	arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;
66	atom = a.atom }
67
68	let hash h a =
69	Hashtbl.hash (map h a)
70
71	let iter f a =
72	ignore (map f a)
73
74	let deep = 4
75	end
76
77	type t =
78	\| Arrow of t * t
79	\| Times of t * t
80	\| Diff of t * t
81	\| Or of t * t
82	\| And of t * t
83	\| Atom of string
84	\| Var of string
85
86	let make_parser expr =
87	EXTEND
88	expr: [
89	[ x = expr; "->"; y = expr -> Arrow (x,y) ]
90	\| [ x = expr; "*"; y = expr -> Times (x,y) ]
91	\| [ x = expr; "&"; y = expr -> And (x,y)
92	\| x = expr; "-"; y = expr -> Diff (x,y) ]
93	\| [ x = expr; "\|"; y = expr -> Or (x,y) ]
94	\| [ "~"; x = expr -> Diff (Atom "Any", x)
95	\| a = LIDENT -> Var a
96	\| a = UIDENT -> Atom a
97	\| "("; x = expr; ")" -> x ]
98	];
99	END
100
101	let rec compile f var = function
102	\| Atom "Any" -> I.any
103	\| Atom "Empty" -> I.empty
104	\| Atom i -> I.atom i
105	\| Times (a,b) -> I.times (f a) (f b)
106	\| Arrow (a,b) -> I.arrow (f a) (f b)
107	\| Diff (a,b) -> I.diff (compile f var a) (compile f var b)
108	\| And (a,b) -> I.cap (compile f var a) (compile f var b)
109	\| Or (a,b) -> I.cup (compile f var a) (compile f var b)
110	\| Var v ->
111	(try var v
112	with Exit -> failwith ("Cyclic definition for " ^ v))
113
114
115	let rec print_list oc f sep un = function
116	\| [] -> fprintf oc "%s" un
117	\| [h] -> f oc h
118	\| h::t -> f oc h; fprintf oc "%s" sep; print_list oc f sep un t
119
120	let print_line u f oc (p,n) =
121	print_list oc f " & " u p;
122	if n <> [] then
123	(
124	fprintf oc " \ ";
125	print_list oc f " \ " "Empty" n
126	)
127
128	let print_bool u oc f a =
129	print_list oc (print_line u f) " \| " "Empty" a
130
131
132	let print_arrow f oc (i1,i2) =
133	fprintf oc "%a -> %a" f i1 f i2
134
135	let print_times f oc (i1,i2) =
136	fprintf oc "%a * %a" f i1 f i2
137
138	let print_atom f oc x =
139	fprintf oc "%s" x
140
141
142	let print f oc d =
143	let b = ref false in
144	if d.I.atom <> [] then
145	(
146	print_bool "AnyAtom" oc (print_atom f) d.I.atom;
147	b := true
148	);
149	if d.I.times <> [] then
150	(
151	if !b then fprintf oc " \| ";
152	print_bool "AnyProd" oc (print_times f) d.I.times;
153	b := true;
154	);
155	if d.I.arrow <> [] then
156	(
157	if !b then fprintf oc " \| ";
158	print_bool "AnyFun" oc (print_arrow f) d.I.arrow;
159	b := true;
160	);
161	if not !b then fprintf oc "Empty"
162	end
163
164	module M = Example.Make(E)
165
166	let _ = M.main ()
167