viewcvs.cgi/types/builtin.ml

open Builtin_defs

(* Types *)

let types =
  [ 
    "Empty",   Types.empty;
    "Any",     any;
    "Int",     int;
    "Char",    Types.char Chars.any;
    "Byte",    char_latin1;
    "Atom",    atom;
    "Pair",    Types.Product.any;
    "Arrow",   Types.Arrow.any;
    "Record",  Types.Record.any;
    "String",  string;
    "Latin1",  string_latin1;
    "Bool",    bool
  ]

let () =
  List.iter
    (fun (n,t) -> 
       Typer.register_global_types 
         [ Ident.U.mk n, 
           Location.mknoloc (Ast.Internal t)]) 
    types

(* Operators *)

let binary_op_gen name typ run =
  Typer.register_binary_op name 
    (fun _ -> { Typed.bin_op_typer = typ; Typed.bin_op_eval = run })

let unary_op_gen name typ run =
  Typer.register_unary_op name 
    (fun _ -> { Typed.un_op_typer = typ; Typed.un_op_eval = run })


let binary_op name t1 t2 f run =
  binary_op_gen
    name
    (fun loc arg1 arg2 constr precise ->
       f (arg1 t1 true) (arg2 t2 true))
    run

let binary_op_cst name t1 t2 t run =
  binary_op_gen name
    (fun loc arg1 arg2 constr precise ->
       ignore (arg1 t1 false); 
       ignore (arg2 t2 false); 
       t)
    run

let binary_op_warning2 name t1 t2 w2 t run =
  binary_op_gen name
    (fun loc arg1 arg2 constr precise ->
       ignore (arg1 t1 false); 
       let r = arg2 t2 true in
       if not (Types.subtype r w2) then
         Typer.warning loc "This operator may fail";
       t)
    run

let unary_op_warning name targ w t run =
  Typer.register_unary_op name 
    (fun _ ->
       { Typed.un_op_typer = 
           (fun loc arg constr precise ->
              let res = arg targ true in
              if not (Types.subtype res w) then
                Typer.warning loc "This operator may fail";
              t);
         Typed.un_op_eval = run })

let unary_op_cst name targ t run =
  Typer.register_unary_op name 
    (fun _ ->
       { Typed.un_op_typer = 
           (fun loc arg constr precise ->
              ignore (arg targ false);
              t);
         Typed.un_op_eval = run })

open Ident

let exn_load_file_utf8 = 
  Value.CDuceExn (
    Value.Pair (
      Value.Atom (Atoms.mk_ascii "load_file_utf8"),
      Value.string_latin1 "File is not a valid UTF-8 stream"))

let exn_int_of = 
  Value.CDuceExn (
    Value.Pair (
      Value.Atom (Atoms.mk_ascii "Invalid_argument"),
      Value.string_latin1 "int_of"))

let eval_load_file ~utf8 e =
  Location.protect_op "load_file";
  let ic = open_in (Value.get_string_latin1 e) in
  let len = in_channel_length ic in
  let s = String.create len in
  really_input ic s 0 len;
  close_in ic;
  if utf8 then 
    if U.check s 
    then Value.string_utf8 (U.mk s) 
    else raise exn_load_file_utf8
  else Value.string_latin1 s


let () = ();;

(* Comparison operators *)

binary_op "=" 
  any any 
  (fun t1 t2 ->
     if Types.is_empty (Types.cap t1 t2) then false_type
     else bool)
  (fun v1 v2 ->
     Value.vbool (Value.compare v1 v2 == 0));;
  
binary_op_cst "<=" 
  any any bool
  (fun v1 v2 -> Value.vbool (Value.compare v1 v2 <= 0));;
  
binary_op_cst "<" 
  any any bool
  (fun v1 v2 -> Value.vbool (Value.compare v1 v2 < 0));;
  
binary_op_cst "<=" 
  any any bool
  (fun v1 v2 -> 
     Value.vbool (Value.compare v1 v2 >= 0));;
  
binary_op_cst ">" 
  any any bool
  (fun v1 v2 -> 
     Value.vbool (Value.compare v1 v2 > 0));;

(* I/O *)
  
unary_op_cst "string_of" 
  any string_latin1
  (fun v -> 
     let b = Buffer.create 16 in
     let ppf = Format.formatter_of_buffer b in
     Value.print ppf v;
     Format.pp_print_flush ppf ();
     Value.string_latin1 (Buffer.contents b)
  );;

unary_op_cst "load_xml" 
  string any
  (fun v -> Load_xml.load_xml (Value.get_string_latin1 v));;
  
unary_op_cst "load_html" 
  string any
  (fun v -> Load_xml.load_html  (Value.get_string_latin1 v));;

unary_op_cst "load_file_utf8" 
  string string
  (eval_load_file ~utf8:true);;

unary_op_cst "load_file" string string_latin1
  (eval_load_file ~utf8:false);;
  

Typer.register_unary_op "print_xml"
  (fun tenv ->
     let ns_table = Typer.get_ns_table tenv in
     { Typed.un_op_typer = (fun loc arg constr precise -> string_latin1);
       Typed.un_op_eval = Print_xml.print_xml ~utf8:false ns_table });;

Typer.register_unary_op "print_xml_utf8"
  (fun tenv ->
     let ns_table = Typer.get_ns_table tenv in
     { Typed.un_op_typer = (fun loc arg constr precise -> string);
       Typed.un_op_eval = Print_xml.print_xml ~utf8:true ns_table });;

unary_op_warning "print"
  string string_latin1 nil
  (fun v ->
     Location.protect_op "print";
     print_string (Value.get_string_latin1 v);
     flush stdout;
     Value.nil
  );;

unary_op_warning "int_of"
  string intstr int
  (fun v ->
     let (s,_) = Value.get_string_utf8 v in
     try Value.Integer (Intervals.mk (U.get_str s)) (* UTF-8 is ASCII compatible ! *)
     with Failure _ -> raise exn_int_of);;

unary_op_cst "atom_of"
  string atom
  (fun v ->
     let (s,_) = Value.get_string_utf8 v in (* TODO: check that s is a correct Name wrt XML *)
     Value.Atom (Atoms.mk Ns.empty s));;

binary_op_warning2 "dump_to_file"
  string string string_latin1 nil
  (fun f v ->
     Location.protect_op "dump_to_file";
     let oc = open_out (Value.get_string_latin1 f) in
     output_string oc (Value.get_string_latin1 v);
     close_out oc;
     Value.nil);;
    
binary_op_cst "dump_to_file_utf8"
  string string nil
  (fun f v ->
     Location.protect_op "dump_to_file_utf8";
     let oc = open_out (Value.get_string_latin1 f) in
     let (v,_) = Value.get_string_utf8 v in
     output_string oc (U.get_str v);
     close_out oc;
     Value.nil);;

(* Integer operators *)

binary_op_gen "+"
  (fun loc arg1 arg2 constr precise ->
     let t1 = arg1 (Types.cup int Types.Record.any) true in
     if Types.subtype t1 int 
     then (
       let t2 = arg2 int true in
       Types.interval
         (Intervals.add (Types.Int.get t1) (Types.Int.get t2))
     )
     else if Types.subtype t1 Types.Record.any 
     then (
       let t2 = arg2 Types.Record.any true in 
       Types.Record.merge t1 t2
     )
     else Typer.error loc "The first argument mixes integers and records")
  (fun v1 v2 -> match (v1,v2) with
     | (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vadd x y)
     | (Value.Record r1, Value.Record r2) -> Value.Record (LabelMap.merge (fun x y -> y) r1 r2)
     | _ -> assert false);;
      
binary_op "-"
  int int
  (fun t1 t2 ->
     Types.interval 
     (Intervals.sub (Types.Int.get t1) (Types.Int.get t2)))
  (fun v1 v2 -> match (v1,v2) with
     | (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vsub x y)
     | _ -> assert false);;

binary_op_cst "*"
  int int int
  (fun v1 v2 -> match (v1,v2) with
     | (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vmult x y)
     | _ -> assert false);;

binary_op_cst "/"
  int int int
  (fun v1 v2 -> match (v1,v2) with
     | (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vdiv x y)
     | _ -> assert false);;

binary_op_cst "mod"
  int int int
  (fun v1 v2 -> match (v1,v2) with
     | (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vmod x y)
     | _ -> assert false);;


binary_op_gen "@"
  (fun loc arg1 arg2 constr precise ->
     let constr' = Sequence.star 
                     (Sequence.approx (Types.cap Sequence.any constr)) in
     let exact = Types.subtype constr' constr in
     if exact then
       let t1 = arg1 constr' precise
       and t2 = arg2 constr' precise in
       if precise then Sequence.concat t1 t2 else constr
     else
       (* Note:
          the knownledge of t1 may makes it useless to
          check t2 with 'precise' ... *)
       let t1 = arg1 constr' true
       and t2 = arg2 constr' true in
       Sequence.concat t1 t2)
  Value.concat;;

unary_op_gen "flatten"
  Typer.flatten
  Value.flatten;;
  

unary_op_cst "raise"
  any Types.empty
  (fun v -> raise (Value.CDuceExn v))
1	open Builtin_defs
2
3	(* Types *)
4
5	let types =
6	[
7	"Empty", Types.empty;
8	"Any", any;
9	"Int", int;
10	"Char", Types.char Chars.any;
11	"Byte", char_latin1;
12	"Atom", atom;
13	"Pair", Types.Product.any;
14	"Arrow", Types.Arrow.any;
15	"Record", Types.Record.any;
16	"String", string;
17	"Latin1", string_latin1;
18	"Bool", bool
19	]
20
21	let () =
22	List.iter
23	(fun (n,t) ->
24	Typer.register_global_types
25	[ Ident.U.mk n,
26	Location.mknoloc (Ast.Internal t)])
27	types
28
29	(* Operators *)
30
31	let binary_op_gen name typ run =
32	Typer.register_binary_op name
33	(fun _ -> { Typed.bin_op_typer = typ; Typed.bin_op_eval = run })
34
35	let unary_op_gen name typ run =
36	Typer.register_unary_op name
37	(fun _ -> { Typed.un_op_typer = typ; Typed.un_op_eval = run })
38
39
40	let binary_op name t1 t2 f run =
41	binary_op_gen
42	name
43	(fun loc arg1 arg2 constr precise ->
44	f (arg1 t1 true) (arg2 t2 true))
45	run
46
47	let binary_op_cst name t1 t2 t run =
48	binary_op_gen name
49	(fun loc arg1 arg2 constr precise ->
50	ignore (arg1 t1 false);
51	ignore (arg2 t2 false);
52	t)
53	run
54
55	let binary_op_warning2 name t1 t2 w2 t run =
56	binary_op_gen name
57	(fun loc arg1 arg2 constr precise ->
58	ignore (arg1 t1 false);
59	let r = arg2 t2 true in
60	if not (Types.subtype r w2) then
61	Typer.warning loc "This operator may fail";
62	t)
63	run
64
65	let unary_op_warning name targ w t run =
66	Typer.register_unary_op name
67	(fun _ ->
68	{ Typed.un_op_typer =
69	(fun loc arg constr precise ->
70	let res = arg targ true in
71	if not (Types.subtype res w) then
72	Typer.warning loc "This operator may fail";
73	t);
74	Typed.un_op_eval = run })
75
76	let unary_op_cst name targ t run =
77	Typer.register_unary_op name
78	(fun _ ->
79	{ Typed.un_op_typer =
80	(fun loc arg constr precise ->
81	ignore (arg targ false);
82	t);
83	Typed.un_op_eval = run })
84
85	open Ident
86
87	let exn_load_file_utf8 =
88	Value.CDuceExn (
89	Value.Pair (
90	Value.Atom (Atoms.mk_ascii "load_file_utf8"),
91	Value.string_latin1 "File is not a valid UTF-8 stream"))
92
93	let exn_int_of =
94	Value.CDuceExn (
95	Value.Pair (
96	Value.Atom (Atoms.mk_ascii "Invalid_argument"),
97	Value.string_latin1 "int_of"))
98
99	let eval_load_file ~utf8 e =
100	Location.protect_op "load_file";
101	let ic = open_in (Value.get_string_latin1 e) in
102	let len = in_channel_length ic in
103	let s = String.create len in
104	really_input ic s 0 len;
105	close_in ic;
106	if utf8 then
107	if U.check s
108	then Value.string_utf8 (U.mk s)
109	else raise exn_load_file_utf8
110	else Value.string_latin1 s
111
112
113	let () = ();;
114
115	(* Comparison operators *)
116
117	binary_op "="
118	any any
119	(fun t1 t2 ->
120	if Types.is_empty (Types.cap t1 t2) then false_type
121	else bool)
122	(fun v1 v2 ->
123	Value.vbool (Value.compare v1 v2 == 0));;
124
125	binary_op_cst "<="
126	any any bool
127	(fun v1 v2 -> Value.vbool (Value.compare v1 v2 <= 0));;
128
129	binary_op_cst "<"
130	any any bool
131	(fun v1 v2 -> Value.vbool (Value.compare v1 v2 < 0));;
132
133	binary_op_cst "<="
134	any any bool
135	(fun v1 v2 ->
136	Value.vbool (Value.compare v1 v2 >= 0));;
137
138	binary_op_cst ">"
139	any any bool
140	(fun v1 v2 ->
141	Value.vbool (Value.compare v1 v2 > 0));;
142
143	(* I/O *)
144
145	unary_op_cst "string_of"
146	any string_latin1
147	(fun v ->
148	let b = Buffer.create 16 in
149	let ppf = Format.formatter_of_buffer b in
150	Value.print ppf v;
151	Format.pp_print_flush ppf ();
152	Value.string_latin1 (Buffer.contents b)
153	);;
154
155	unary_op_cst "load_xml"
156	string any
157	(fun v -> Load_xml.load_xml (Value.get_string_latin1 v));;
158
159	unary_op_cst "load_html"
160	string any
161	(fun v -> Load_xml.load_html (Value.get_string_latin1 v));;
162
163	unary_op_cst "load_file_utf8"
164	string string
165	(eval_load_file ~utf8:true);;
166
167	unary_op_cst "load_file" string string_latin1
168	(eval_load_file ~utf8:false);;
169
170
171	Typer.register_unary_op "print_xml"
172	(fun tenv ->
173	let ns_table = Typer.get_ns_table tenv in
174	{ Typed.un_op_typer = (fun loc arg constr precise -> string_latin1);
175	Typed.un_op_eval = Print_xml.print_xml ~utf8:false ns_table });;
176
177	Typer.register_unary_op "print_xml_utf8"
178	(fun tenv ->
179	let ns_table = Typer.get_ns_table tenv in
180	{ Typed.un_op_typer = (fun loc arg constr precise -> string);
181	Typed.un_op_eval = Print_xml.print_xml ~utf8:true ns_table });;
182
183	unary_op_warning "print"
184	string string_latin1 nil
185	(fun v ->
186	Location.protect_op "print";
187	print_string (Value.get_string_latin1 v);
188	flush stdout;
189	Value.nil
190	);;
191
192	unary_op_warning "int_of"
193	string intstr int
194	(fun v ->
195	let (s,_) = Value.get_string_utf8 v in
196	try Value.Integer (Intervals.mk (U.get_str s)) (* UTF-8 is ASCII compatible ! *)
197	with Failure _ -> raise exn_int_of);;
198
199	unary_op_cst "atom_of"
200	string atom
201	(fun v ->
202	let (s,_) = Value.get_string_utf8 v in (* TODO: check that s is a correct Name wrt XML *)
203	Value.Atom (Atoms.mk Ns.empty s));;
204
205	binary_op_warning2 "dump_to_file"
206	string string string_latin1 nil
207	(fun f v ->
208	Location.protect_op "dump_to_file";
209	let oc = open_out (Value.get_string_latin1 f) in
210	output_string oc (Value.get_string_latin1 v);
211	close_out oc;
212	Value.nil);;
213
214	binary_op_cst "dump_to_file_utf8"
215	string string nil
216	(fun f v ->
217	Location.protect_op "dump_to_file_utf8";
218	let oc = open_out (Value.get_string_latin1 f) in
219	let (v,_) = Value.get_string_utf8 v in
220	output_string oc (U.get_str v);
221	close_out oc;
222	Value.nil);;
223
224	(* Integer operators *)
225
226	binary_op_gen "+"
227	(fun loc arg1 arg2 constr precise ->
228	let t1 = arg1 (Types.cup int Types.Record.any) true in
229	if Types.subtype t1 int
230	then (
231	let t2 = arg2 int true in
232	Types.interval
233	(Intervals.add (Types.Int.get t1) (Types.Int.get t2))
234	)
235	else if Types.subtype t1 Types.Record.any
236	then (
237	let t2 = arg2 Types.Record.any true in
238	Types.Record.merge t1 t2
239	)
240	else Typer.error loc "The first argument mixes integers and records")
241	(fun v1 v2 -> match (v1,v2) with
242	\| (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vadd x y)
243	\| (Value.Record r1, Value.Record r2) -> Value.Record (LabelMap.merge (fun x y -> y) r1 r2)
244	\| _ -> assert false);;
245
246	binary_op "-"
247	int int
248	(fun t1 t2 ->
249	Types.interval
250	(Intervals.sub (Types.Int.get t1) (Types.Int.get t2)))
251	(fun v1 v2 -> match (v1,v2) with
252	\| (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vsub x y)
253	\| _ -> assert false);;
254
255	binary_op_cst "*"
256	int int int
257	(fun v1 v2 -> match (v1,v2) with
258	\| (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vmult x y)
259	\| _ -> assert false);;
260
261	binary_op_cst "/"
262	int int int
263	(fun v1 v2 -> match (v1,v2) with
264	\| (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vdiv x y)
265	\| _ -> assert false);;
266
267	binary_op_cst "mod"
268	int int int
269	(fun v1 v2 -> match (v1,v2) with
270	\| (Value.Integer x, Value.Integer y) -> Value.Integer (Intervals.vmod x y)
271	\| _ -> assert false);;
272
273
274	binary_op_gen "@"
275	(fun loc arg1 arg2 constr precise ->
276	let constr' = Sequence.star
277	(Sequence.approx (Types.cap Sequence.any constr)) in
278	let exact = Types.subtype constr' constr in
279	if exact then
280	let t1 = arg1 constr' precise
281	and t2 = arg2 constr' precise in
282	if precise then Sequence.concat t1 t2 else constr
283	else
284	(* Note:
285	the knownledge of t1 may makes it useless to
286	check t2 with 'precise' ... *)
287	let t1 = arg1 constr' true
288	and t2 = arg2 constr' true in
289	Sequence.concat t1 t2)
290	Value.concat;;
291
292	unary_op_gen "flatten"
293	Typer.flatten
294	Value.flatten;;
295
296
297	unary_op_cst "raise"
298	any Types.empty
299	(fun v -> raise (Value.CDuceExn v))