cduce.ml 9.65 KB
Newer Older
1
open Location
2
open Ident
3

4
let quiet = ref false
5
let toplevel = ref false
6

7
let typing_env = State.ref "Cduce.typing_env" Builtin.env
8
let eval_env = State.ref "Cduce.eval_env" Env.empty
9
10
11
12
13
14
15
16
17
18
19
let compile_env = State.ref "Cduce.compile_env" Compile.empty

let do_compile = ref false

let get_global_value v =
  if !do_compile 
  then Eval.L.eval_var (Compile.find v !compile_env)
  else Env.find v !eval_env

let get_global_type v =
  Typer.find_value v !typing_env
20

21
let enter_global_value x v t =
22
  typing_env := Typer.enter_value x t !typing_env;
23

24
25
26
27
  if !do_compile 
  then (compile_env := Compile.enter_global !compile_env x; Eval.L.push v)
  else eval_env := Env.add x v !eval_env
  
28
29
30
31
32
let rec is_abstraction = function
  | Ast.Abstraction _ -> true
  | Ast.LocatedExpr (_,e) -> is_abstraction e
  | _ -> false

33
let print_norm ppf d = 
34
  Location.protect ppf 
35
    (fun ppf -> Types.Print.print ppf ((*Types.normalize*) d))
36

37
38
39
40
let print_sample ppf s =
  Location.protect ppf
    (fun ppf -> Sample.print ppf s)

41
42
43
let print_protect ppf s =
  Location.protect ppf (fun ppf -> Format.fprintf ppf "%s" s)

44
45
let print_value ppf v =
  Location.protect ppf (fun ppf -> Value.print ppf v)
46

47
let dump_env ppf =
48
49
  Format.fprintf ppf "Types:%a@." Typer.dump_types !typing_env;
  Format.fprintf ppf "Namespace prefixes:@\n%a" Typer.dump_ns !typing_env;
50
  Format.fprintf ppf "Namespace prefixes used for pretty-printing:@.%t"
51
    Ns.InternalPrinter.dump;
52
  Format.fprintf ppf "Values:@.";
53
  Env.iter 
54
    (fun x v ->
55
       let t = Typer.find_value x !typing_env in
56
57
       Format.fprintf ppf "@[val %a : @[%a = %a@]@]@."
	 U.print (Id.value x) print_norm t print_value v
58
    )
59
60
    !eval_env;
  Eval.L.dump ppf
61

62
let rec print_exn ppf = function
63
64
  | Location (loc, w, exn) ->
      Format.fprintf ppf "Error %a:@." Location.print_loc (loc,w);
65
      Format.fprintf ppf "%a" Location.html_hilight (loc,w); 
66
      print_exn ppf exn
67
  | Value.CDuceExn v ->
68
      Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@."
69
        print_value v
70
  | Eval.MultipleDeclaration v ->
71
      Format.fprintf ppf "Multiple declaration for global value %a@." 
72
        U.print (Id.value v)
73
  | Typer.WrongLabel (t,l) ->
74
      Format.fprintf ppf "Wrong record selection; field %a " 
75
        Label.print (LabelPool.value l);
76
      Format.fprintf ppf "not present in an expression of type:@.%a@."
77
        print_norm t
78
  | Typer.ShouldHave (t,msg) ->
79
      Format.fprintf ppf "This expression should have type:@.%a@.%a@." 
80
        print_norm t
81
        print_protect msg
82
  | Typer.ShouldHave2 (t1,msg,t2) ->
83
      Format.fprintf ppf "This expression should have type:@.%a@.%a %a@." 
84
        print_norm t1
85
        print_protect msg
86
        print_norm t2
87
  | Typer.Error s ->
88
      Format.fprintf ppf "%a@." print_protect s
89
  | Typer.Constraint (s,t) ->
90
      Format.fprintf ppf "This expression should have type:@.%a@." 
91
        print_norm t;
92
      Format.fprintf ppf "but its inferred type is:@.%a@." 
93
        print_norm s;
94
      Format.fprintf ppf "which is not a subtype, as shown by the sample:@.%a@." 
95
	print_sample (Sample.get (Types.diff s t))
96
  | Typer.NonExhaustive t ->
97
98
      Format.fprintf ppf "This pattern matching is not exhaustive@.";
      Format.fprintf ppf "Residual type:@.%a@."
99
	print_norm t;
100
      Format.fprintf ppf "Sample:@.%a@." print_sample (Sample.get t)
101
102
103
  | Typer.UnboundId (x,tn) ->
      Format.fprintf ppf "Unbound identifier %a%s@." U.print (Id.value x)
        (if tn then " (it is a type name)" else "")
104
105
106
107
  | Ulexer.Error (i,j,s) ->
      let loc = Location.loc_of_pos (i,j), `Full in
      Format.fprintf ppf "Error %a:@." Location.print_loc loc;
      Format.fprintf ppf "%a%s" Location.html_hilight loc s
108
  | Parser.Error s | Stream.Error s -> 
109
      Format.fprintf ppf "Parsing error: %a@." print_protect s
110
  | Location.Generic s ->
111
      Format.fprintf ppf "%a@." print_protect s
112
  | exn ->
113
(*      raise exn *)
114
      Format.fprintf ppf "%a@." print_protect (Printexc.to_string exn)
115

116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158

let insert_bindings ppf =
  List.iter2 
    (fun (x,t) (y,v) ->
       assert (x = y);
       typing_env := Typer.enter_value x t !typing_env;
       eval_env := Env.add x v !eval_env;
       if not !quiet then
	 Format.fprintf ppf "val %a : @[@[%a@] =@ @[%a@]@]@." 
	   U.print (Id.value x) print_norm t print_value v)

let display ppf =
  List.iter
    (fun x ->
       let t = get_global_type x in
       let v = get_global_value x in
       if not !quiet then
	 Format.fprintf ppf "val %a : @[@[%a@] =@ @[%a@]@]@." 
	   U.print (Id.value x) print_norm t print_value v)

let eval ppf e =
  let (fv,e) = Typer.expr !typing_env e in
  let t = Typer.type_check !typing_env e Types.any true in
  Typer.report_unused_branches ();
  
  if not !quiet then
    Location.dump_loc ppf (e.Typed.exp_loc,`Full);
  
  if !do_compile then
    let e = Compile.compile !compile_env false e in 
    let v = Eval.L.eval e in
    if not !quiet then
      Format.fprintf ppf "- : @[@[%a@] =@ @[%a@]@]@." 
	print_norm t print_value v; 
    v
  else
    let v = Eval.eval !eval_env e in
     if not !quiet then
       Format.fprintf ppf "- : @[@[%a@] =@ @[%a@]@]@." 
	 print_norm t print_value v;
    v
  

159
let debug ppf = function
160
  | `Subtype (t1,t2) ->
161
      Format.fprintf ppf "[DEBUG:subtype]@.";
162
163
      let t1 = Types.descr (Typer.typ !typing_env t1)
      and t2 = Types.descr (Typer.typ !typing_env t2) in
164
165
      let s = Types.subtype t1 t2 in
      Format.fprintf ppf "%a %a %a : %b@." print_norm t1 print_protect "<=" print_norm t2 s
166
  | `Sample t ->
167
168
      Format.fprintf ppf "[DEBUG:sample]@.";
      (try
169
	 let t = Types.descr (Typer.typ !typing_env t) in
170
171
172
	 Format.fprintf ppf "%a@." print_sample (Sample.get t)
       with Not_found ->
	 Format.fprintf ppf "Empty type : no sample !@.")
173
  | `Filter (t,p) -> 
174
      Format.fprintf ppf "[DEBUG:filter]@.";
175
176
      let t = Typer.typ !typing_env t
      and p = Typer.pat !typing_env p in
177
178
      let f = Patterns.filter (Types.descr t) p in
      List.iter (fun (x,t) ->
179
		   Format.fprintf ppf " %a:%a@." U.print (Id.value x)
180
181
		     print_norm (Types.descr t)) f
  | `Accept p ->
182
      Format.fprintf ppf "[DEBUG:accept]@.";
183
      let p = Typer.pat !typing_env p in
184
      let t = Patterns.accept p in
185
      Format.fprintf ppf " %a@." Types.Print.print (Types.descr t)
186
  | `Compile (t,pl) ->
187
      Format.fprintf ppf "[DEBUG:compile]@.";
188
189
      let t = Typer.typ !typing_env t
      and pl = List.map (Typer.pat !typing_env) pl in
190
      Patterns.Compile.debug_compile ppf t pl
191
192
193
194
195
196
197
198
199
  | `Explain (t,e) ->
      Format.fprintf ppf "[DEBUG:explain]@.";
      let t = Typer.typ !typing_env t in
      (match Explain.explain (Types.descr t) (eval ppf e) with
	 | Some p ->
	     Format.fprintf ppf "Explanation: @[%a@]@." 
	       Explain.print_path p
	 | None ->
	     Format.fprintf ppf "Explanation: value has given type@.")
200

201
      
202
  
203
204
let rec collect_funs ppf accu = function
  | { descr = Ast.FunDecl e } :: rest -> 
205
      let (_,e) = Typer.expr !typing_env e in
206
207
      collect_funs ppf (e::accu) rest
  | rest ->
208
      let typs = Typer.type_rec_funs !typing_env accu in
209
      Typer.report_unused_branches ();
210
211
212
213
214
215
216
217
218
219
220

      if !do_compile then
	let (names,env,funs) = Compile.compile_rec_funs !compile_env accu in
	Eval.L.eval_rec_funs funs;
	typing_env := Typer.enter_values typs !typing_env;
	compile_env := env;
	display ppf names
      else (
	let vals = Eval.eval_rec_funs !eval_env accu in
	insert_bindings ppf typs vals);
	
221
222
223
224
225
226
      rest

let rec collect_types ppf accu = function
  | { descr = Ast.TypeDecl (x,t) } :: rest -> 
      collect_types ppf ((x,t) :: accu) rest
  | rest ->
227
228
      typing_env := 
        Typer.enter_types (Typer.type_defs !typing_env accu) !typing_env;
229
230
      rest

231

232
233
234
235
236
let rec phrases ppf phs = match phs with
  | { descr = Ast.FunDecl _ } :: _ -> 
      phrases ppf (collect_funs ppf [] phs)
  | { descr = Ast.TypeDecl (_,_) } :: _ ->
      phrases ppf (collect_types ppf [] phs)
237
238
239
  | { descr = Ast.SchemaDecl (name, schema) } :: rest ->
      Typer.register_schema name schema;
      phrases ppf rest
240
  | { descr = Ast.Namespace (pr,ns) } :: rest ->
241
      typing_env := Typer.enter_ns pr ns !typing_env;
242
      phrases ppf rest
243
  | { descr = Ast.EvalStatement e } :: rest ->
244
      ignore (eval ppf e);
245
246
      phrases ppf rest
  | { descr = Ast.LetDecl (p,e) } :: rest ->
247
      let decl = Typer.let_decl !typing_env p e in
248
      let typs = Typer.type_let_decl !typing_env decl in
249
      Typer.report_unused_branches ();
250
251
252
253
254
255
256
257
258
259
260

      if !do_compile then
	let (names,env,decl) = Compile.compile_let_decl !compile_env decl in
	Eval.L.eval_let_decl decl;
	typing_env := Typer.enter_values typs !typing_env;
	compile_env := env;
	display ppf names
      else
	(let vals = Eval.eval_let_decl !eval_env decl in
	insert_bindings ppf typs vals);

261
262
      phrases ppf rest
  | { descr = Ast.Debug l } :: rest -> 
263
      debug ppf l; 
264
      phrases ppf rest
265
266
267
268
269
270
  | { descr = Ast.Directive `Quit } :: rest ->
      if !toplevel then raise End_of_file;
      phrases ppf rest
  | { descr = Ast.Directive `Env } :: rest ->
      dump_env ppf;
      phrases ppf rest
271
  | { descr = Ast.Directive `Reinit_ns } :: rest ->
272
      Typer.set_ns_table_for_printer !typing_env;
273
      phrases ppf rest
274
275
276
  | [] -> ()

let run rule ppf ppf_err input =
277
  Typer.clear_unused_branches ();
278
  try 
279
    let p = 
280
      try rule input
281
      with
282
	| Stdpp.Exc_located (_, (Location _ as e)) ->
283
	    Parser.sync (); raise e
284
	| Stdpp.Exc_located ((i,j), e) -> 
285
	    Parser.sync (); raise_loc i j e
286
    in
287
    phrases ppf p;
288
    true
289
  with 
290
291
292
    | (End_of_file | Failure _ | Not_found | Invalid_argument _ | Sys.Break) 
	as e -> 
	raise e
293
294
295
296
    | exn -> 
	print_exn ppf_err exn;
	Format.fprintf ppf_err "@.";
	false
297

298
let script = run Parser.prog
299
let topinput = run Parser.top_phrases
300
301
302
303
304
305

let serialize_typing_env t () =
  Typer.serialize t !typing_env

let deserialize_typing_env t =
  typing_env := Typer.deserialize t