cduce.ml 10.4 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" Eval.empty
9
10
11
12
13
14
let compile_env = State.ref "Cduce.compile_env" Compile.empty

let do_compile = ref false

let get_global_value v =
  if !do_compile 
15
  then Eval.L.var (Compile.find v !compile_env)
16
  else Eval.find_value v !eval_env
17
18
19

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
  if !do_compile 
  then (compile_env := Compile.enter_global !compile_env x; Eval.L.push v)
26
  else eval_env := Eval.enter_value x v !eval_env
27
  
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
48
49
50
let dump_value ppf x t v =
  Format.fprintf ppf "@[val %a : @[%a = %a@]@]@."
    U.print (Id.value x) print_norm t print_value v

51
let dump_env ppf =
52
53
  Format.fprintf ppf "Types:%a@." Typer.dump_types !typing_env;
  Format.fprintf ppf "Namespace prefixes:@\n%a" Typer.dump_ns !typing_env;
54
  Format.fprintf ppf "Namespace prefixes used for pretty-printing:@.%t"
55
    Ns.InternalPrinter.dump;
56
  Format.fprintf ppf "Values:@.";
57
58
  Typer.iter_values !typing_env
    (fun x t -> dump_value ppf x t (get_global_value x))
59

60
61
62
63
64
65
66
67
68
let directive_help ppf =
  Format.fprintf ppf
"Toplevel directives:
  #quit;;         quit the interpreter
  #env;;          dump current environment
  #reinit_ns;;    reinitialize namespace processing
  #help;;         shows this help message
"

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

123

124
125
126
127
128
let display ppf l =
  if not !quiet then
    List.iter
      (fun (x,t) -> dump_value ppf x t (get_global_value x))
      l
129
130

let eval ppf e =
131
  let (e,t) = Typer.type_expr !typing_env e in
132
133
134
  
  if not !quiet then
    Location.dump_loc ppf (e.Typed.exp_loc,`Full);
135
136
137

  let v =   
    if !do_compile then
138
139
      let e = Compile.compile_eval !compile_env e in 
      Eval.L.expr e
140
141
142
143
144
145
146
    else
      Eval.eval !eval_env e
  in
  if not !quiet then
    Format.fprintf ppf "- : @[@[%a@] =@ @[%a@]@]@." 
      print_norm t print_value v; 
  v
147
  
148
let let_decl ppf p e =
149
  let (tenv,decl,typs) = Typer.type_let_decl !typing_env p e in
150
151
152
153
  
  let () =
    if !do_compile then
      let (env,decl) = Compile.compile_let_decl !compile_env decl in
154
      Eval.L.eval decl;
155
156
157
158
      compile_env := env
    else
      eval_env := Eval.eval_let_decl !eval_env decl
  in
159
  typing_env := tenv;
160
161
162
163
  display ppf typs
  

let let_funs ppf funs =
164
  let (tenv,funs,typs) = Typer.type_let_funs !typing_env funs in
165
  
166
167
168
  let () =
    if !do_compile then
      let (env,funs) = Compile.compile_rec_funs !compile_env funs in
169
      Eval.L.eval funs;
170
171
172
173
      compile_env := env;
    else 
      eval_env := Eval.eval_rec_funs !eval_env funs 
  in
174
  typing_env := tenv;
175
176
  display ppf typs

177

178
let debug ppf = function
179
  | `Subtype (t1,t2) ->
180
      Format.fprintf ppf "[DEBUG:subtype]@.";
181
182
      let t1 = Types.descr (Typer.typ !typing_env t1)
      and t2 = Types.descr (Typer.typ !typing_env t2) in
183
184
      let s = Types.subtype t1 t2 in
      Format.fprintf ppf "%a %a %a : %b@." print_norm t1 print_protect "<=" print_norm t2 s
185
  | `Sample t ->
186
187
      Format.fprintf ppf "[DEBUG:sample]@.";
      (try
188
	 let t = Types.descr (Typer.typ !typing_env t) in
189
190
191
	 Format.fprintf ppf "%a@." print_sample (Sample.get t)
       with Not_found ->
	 Format.fprintf ppf "Empty type : no sample !@.")
192
  | `Filter (t,p) -> 
193
      Format.fprintf ppf "[DEBUG:filter]@.";
194
195
      let t = Typer.typ !typing_env t
      and p = Typer.pat !typing_env p in
196
197
      let f = Patterns.filter (Types.descr t) p in
      List.iter (fun (x,t) ->
198
		   Format.fprintf ppf " %a:%a@." U.print (Id.value x)
199
200
		     print_norm (Types.descr t)) f
  | `Accept p ->
201
      Format.fprintf ppf "[DEBUG:accept]@.";
202
      let p = Typer.pat !typing_env p in
203
      let t = Patterns.accept p in
204
      Format.fprintf ppf " %a@." Types.Print.print (Types.descr t)
205
  | `Compile (t,pl) ->
206
      Format.fprintf ppf "[DEBUG:compile]@.";
207
208
      let t = Typer.typ !typing_env t
      and pl = List.map (Typer.pat !typing_env) pl in
209
      Patterns.Compile.debug_compile ppf t pl
210
211
212
213
214
215
216
217
218
  | `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@.")
219

220

221
222
223
let rec collect_funs ppf accu = function
  | { descr = Ast.FunDecl e } :: rest -> collect_funs ppf (e::accu) rest
  | rest -> let_funs ppf accu; rest
224
225
226
227
228

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

233

234
235
236
237
238
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)
239
240
241
  | { descr = Ast.SchemaDecl (name, schema) } :: rest ->
      Typer.register_schema name schema;
      phrases ppf rest
242
  | { descr = Ast.Namespace (pr,ns) } :: rest ->
243
      typing_env := Typer.enter_ns pr ns !typing_env;
244
      phrases ppf rest
245
  | { descr = Ast.EvalStatement e } :: rest ->
246
      ignore (eval ppf e);
247
248
      phrases ppf rest
  | { descr = Ast.LetDecl (p,e) } :: rest ->
249
      let_decl ppf p e;
250
251
      phrases ppf rest
  | { descr = Ast.Debug l } :: rest -> 
252
      debug ppf l; 
253
      phrases ppf rest
254
255
256
257
258
259
  | { 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
260
  | { descr = Ast.Directive `Reinit_ns } :: rest ->
261
      Typer.set_ns_table_for_printer !typing_env;
262
      phrases ppf rest
263
264
265
  | { descr = Ast.Directive `Help } :: rest ->
      directive_help ppf;
      phrases ppf rest
266
267
  | [] -> ()

268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
let catch_exn ppf_err = function
  | (End_of_file | Failure _ | Not_found | Invalid_argument _ | Sys.Break) 
      as e -> 
      raise e
  | exn -> 
      print_exn ppf_err exn;
      Format.fprintf ppf_err "@."

let parse rule input =
  try Some (rule input)
  with
      | Stdpp.Exc_located (_, (Location _ as e)) ->
	  Parser.sync (); raise e
      | Stdpp.Exc_located ((i,j), e) -> 
	  Parser.sync (); raise_loc i j e

284
let run rule ppf ppf_err input =
285
286
287
288
  try match parse rule input with
    | Some phs -> phrases ppf phs; true
    | None -> false
  with exn -> catch_exn ppf_err exn; false
289

290
let script = run Parser.prog
291
let topinput = run Parser.top_phrases
292

293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
let comp_unit src = 
  try 
    let ic = open_in src in
    Location.push_source (`File src);
    let input = Stream.of_channel ic in
    match parse Parser.prog input with
      | Some p ->
	  close_in ic;
	  let argv = ident (U.mk "argv") in
	  let (tenv,cenv,codes) = 
	    Compile.comp_unit 
	      (Typer.enter_value argv (Sequence.star Sequence.string)
		 Builtin.env)
	      (Compile.enter_global Compile.empty argv)
	      p in
	  codes
      | None -> exit 1
    with exn -> catch_exn Format.err_formatter exn; exit 1

let run_code argv codes =
  try
    Eval.L.push argv;
    List.iter Eval.L.eval codes
  with exn -> catch_exn Format.err_formatter exn; exit 1


let compile src =
  let codes = comp_unit src in
  let oc = open_out (src ^ ".out") in
  let codes_s = Serialize.Put.run Lambda.Put.compunit codes in
  output_string oc codes_s;
  close_out oc;
  exit 0
  
let compile_run src argv =
  run_code argv (comp_unit src)

let run obj argv =  
  let ic = open_in obj in
  let len = in_channel_length ic in
  let codes = String.create len in
  really_input ic codes 0 len;
  close_in ic;
  let codes = Serialize.Get.run Lambda.Get.compunit codes in
  run_code argv codes


340
341
342
343
344
let serialize_typing_env t () =
  Typer.serialize t !typing_env

let deserialize_typing_env t =
  typing_env := Typer.deserialize t