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

114

115
116
117
118
119
let display ppf l =
  if not !quiet then
    List.iter
      (fun (x,t) -> dump_value ppf x t (get_global_value x))
      l
120
121

let eval ppf e =
122
  let (e,t) = Typer.type_expr !typing_env e in
123
124
125
  
  if not !quiet then
    Location.dump_loc ppf (e.Typed.exp_loc,`Full);
126
127
128

  let v =   
    if !do_compile then
129
130
      let e = Compile.compile_eval !compile_env e in 
      Eval.L.expr e
131
132
133
134
135
136
137
    else
      Eval.eval !eval_env e
  in
  if not !quiet then
    Format.fprintf ppf "- : @[@[%a@] =@ @[%a@]@]@." 
      print_norm t print_value v; 
  v
138
  
139
let let_decl ppf p e =
140
  let (tenv,decl,typs) = Typer.type_let_decl !typing_env p e in
141
142
143
144
  
  let () =
    if !do_compile then
      let (env,decl) = Compile.compile_let_decl !compile_env decl in
145
      Eval.L.eval decl;
146
147
148
149
      compile_env := env
    else
      eval_env := Eval.eval_let_decl !eval_env decl
  in
150
  typing_env := tenv;
151
152
153
154
  display ppf typs
  

let let_funs ppf funs =
155
  let (tenv,funs,typs) = Typer.type_let_funs !typing_env funs in
156
  
157
158
159
  let () =
    if !do_compile then
      let (env,funs) = Compile.compile_rec_funs !compile_env funs in
160
      Eval.L.eval funs;
161
162
163
164
      compile_env := env;
    else 
      eval_env := Eval.eval_rec_funs !eval_env funs 
  in
165
  typing_env := tenv;
166
167
  display ppf typs

168

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

211

212
213
214
let rec collect_funs ppf accu = function
  | { descr = Ast.FunDecl e } :: rest -> collect_funs ppf (e::accu) rest
  | rest -> let_funs ppf accu; rest
215
216
217
218
219

let rec collect_types ppf accu = function
  | { descr = Ast.TypeDecl (x,t) } :: rest -> 
      collect_types ppf ((x,t) :: accu) rest
  | rest ->
220
221
      typing_env := 
        Typer.enter_types (Typer.type_defs !typing_env accu) !typing_env;
222
223
      rest

224

225
226
227
228
229
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)
230
231
232
  | { descr = Ast.SchemaDecl (name, schema) } :: rest ->
      Typer.register_schema name schema;
      phrases ppf rest
233
  | { descr = Ast.Namespace (pr,ns) } :: rest ->
234
      typing_env := Typer.enter_ns pr ns !typing_env;
235
      phrases ppf rest
236
  | { descr = Ast.EvalStatement e } :: rest ->
237
      ignore (eval ppf e);
238
239
      phrases ppf rest
  | { descr = Ast.LetDecl (p,e) } :: rest ->
240
      let_decl ppf p e;
241
242
      phrases ppf rest
  | { descr = Ast.Debug l } :: rest -> 
243
      debug ppf l; 
244
      phrases ppf rest
245
246
247
248
249
250
  | { 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
251
  | { descr = Ast.Directive `Reinit_ns } :: rest ->
252
      Typer.set_ns_table_for_printer !typing_env;
253
      phrases ppf rest
254
255
  | [] -> ()

256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
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

272
let run rule ppf ppf_err input =
273
274
275
276
  try match parse rule input with
    | Some phs -> phrases ppf phs; true
    | None -> false
  with exn -> catch_exn ppf_err exn; false
277

278
let script = run Parser.prog
279
let topinput = run Parser.top_phrases
280

281
282
283
284
285
286
287
288
289
290
291
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
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


328
329
330
331
332
let serialize_typing_env t () =
  Typer.serialize t !typing_env

let deserialize_typing_env t =
  typing_env := Typer.deserialize t