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

4
5
let quiet = ref false

6
let typing_env = State.ref "Cduce.typing_env" Env.empty
7

8
9
let eval_env = State.ref "Cduce.eval_env" Env.empty

10
let enter_global_value x v t =
11
  eval_env := Env.add x v !eval_env;
12
  typing_env := Env.add x t !typing_env
13

14
15
16
17
18
let rec is_abstraction = function
  | Ast.Abstraction _ -> true
  | Ast.LocatedExpr (_,e) -> is_abstraction e
  | _ -> false

19
let print_norm ppf d = 
20
  Location.protect ppf 
21
    (fun ppf -> Types.Print.print ppf ((*Types.normalize*) d))
22

23
24
25
26
27
let print_sample ppf s =
  Location.protect ppf
    (fun ppf -> Sample.print ppf s)


28
29
let print_value ppf v =
  Location.protect ppf (fun ppf -> Value.print ppf v)
30

31
let dump_env ppf =
32
33
34
  Format.fprintf ppf "Global types:";
  Typer.dump_global_types ppf;
  Format.fprintf ppf ".@\n";
35
  Env.iter 
36
    (fun x v ->
37
       let t = Env.find x !typing_env in
38
39
       Format.fprintf ppf "@[|- %a : %a@ => %a@]@\n"
	 U.print (Id.value x)
40
41
42
	 print_norm t
	 print_value v
    )
43
    !eval_env
44
45
  

46
let rec print_exn ppf = function
47
  | Location (loc, exn) ->
48
      Format.fprintf ppf "Error %a:@\n" Location.print_loc loc;
49
      Format.fprintf ppf "%a" Location.html_hilight loc;
50
      print_exn ppf exn
51
52
  | Value.CDuceExn v ->
      Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@\n"
53
        print_value v
54
  | Eval.MultipleDeclaration v ->
55
56
      Format.fprintf ppf "Multiple declaration for global value %a@\n" 
        U.print (Id.value v)
57
  | Typer.WrongLabel (t,l) ->
58
59
      Format.fprintf ppf "Wrong record selection: the label %a@\n" 
        U.print (LabelPool.value l);
60
      Format.fprintf ppf "applied to an expression of type:@\n%a@\n"
61
        print_norm t
62
  | Typer.ShouldHave (t,msg) ->
63
      Format.fprintf ppf "This expression should have type:@\n%a@\n%s@\n" 
64
        print_norm t
65
        msg
66
  | Typer.ShouldHave2 (t1,msg,t2) ->
67
      Format.fprintf ppf "This expression should have type:@\n%a@\n%s %a@\n" 
68
69
70
        print_norm t1
        msg
        print_norm t2
71
72
73
  | Typer.Error s ->
      Format.fprintf ppf "%s@\n" s
  | Typer.Constraint (s,t) ->
74
      Format.fprintf ppf "This expression should have type:@\n%a@\n" 
75
        print_norm t;
76
      Format.fprintf ppf "but its inferred type is:@\n%a@\n" 
77
        print_norm s;
78
79
      Format.fprintf ppf "which is not a subtype, as shown by the sample:@\n%a@\n" 
	print_sample (Sample.get (Types.diff s t))
80
81
  | Typer.NonExhaustive t ->
      Format.fprintf ppf "This pattern matching is not exhaustive@\n";
82
      Format.fprintf ppf "Residual type:@\n%a@\n"
83
	print_norm t;
84
      Format.fprintf ppf "Sample:@\n%a@\n" print_sample (Sample.get t)
85
  | Typer.UnboundId x ->
86
      Format.fprintf ppf "Unbound identifier %a@\n" U.print (Id.value x)
87
88
89
90
91
92
93
94
  | Wlexer.Illegal_character c ->
      Format.fprintf ppf "Illegal character (%s)@\n" (Char.escaped c)
  | Wlexer.Unterminated_comment ->
      Format.fprintf ppf "Comment not terminated@\n"
  | Wlexer.Unterminated_string ->
      Format.fprintf ppf "String literal not terminated@\n"
  | Wlexer.Unterminated_string_in_comment ->
      Format.fprintf ppf "This comment contains an unterminated string literal@\n"
95
  | Parser.Error s | Stream.Error s -> 
96
      Format.fprintf ppf "Parsing error: %s@\n" s
97
98
  | Location.Generic s ->
      Format.fprintf ppf "%s@\n" s
99
  | exn ->
100
(*      raise exn *)
101
102
      Format.fprintf ppf "%s@\n" (Printexc.to_string exn)

103
let debug ppf = function
104
105
  | `Subtype (t1,t2) ->
      Format.fprintf ppf "[DEBUG:subtype]@\n";
106
107
      let t1 = Types.descr (Typer.typ t1)
      and t2 = Types.descr (Typer.typ t2) in
108
109
      Format.fprintf ppf "%a <= %a : %b@\n" print_norm t1 print_norm t2
	(Types.subtype t1 t2)
110
111
112
  | `Sample t ->
      Format.fprintf ppf "[DEBUG:sample]@\n";
      let t = Types.descr (Typer.typ t) in
113
      Format.fprintf ppf "%a@\n" print_sample (Sample.get t)
114
115
  | `Filter (t,p) -> 
      Format.fprintf ppf "[DEBUG:filter]@\n";
116
117
      let t = Typer.typ t
      and p = Typer.pat p in
118
119
      let f = Patterns.filter (Types.descr t) p in
      List.iter (fun (x,t) ->
120
		   Format.fprintf ppf " %a:%a@\n" U.print (Id.value x)
121
122
123
		     print_norm (Types.descr t)) f
  | `Accept p ->
      Format.fprintf ppf "[DEBUG:accept]@\n";
124
      let p = Typer.pat p in
125
      let t = Patterns.accept p in
126
      Format.fprintf ppf " %a@\n" Types.Print.print (Types.descr t)
127
128
  | `Compile (t,pl) ->
      Format.fprintf ppf "[DEBUG:compile]@\n";
129
130
      let t = Typer.typ t
      and pl = List.map Typer.pat pl in
131
      Patterns.Compile.debug_compile ppf t pl
132
133


134

135
136
137
138
139
140
141
let insert_type_bindings ppf = 
  List.iter 
    (fun (x,t) ->
       typing_env := Env.add x t !typing_env;
       if not !quiet then
	 Format.fprintf ppf "|- %a : %a@." 
	   U.print (Id.value x) print_norm t) 
142

143
144
145
146
147
148
149
150
let insert_eval_bindings ppf =
  List.iter 
    (fun (x,v) ->
       eval_env := Env.add x v !eval_env;
       if not !quiet then
	 Format.fprintf ppf "=> %a : @[%a@]@." 
	   U.print (Id.value x) print_value v
    )
151
  
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
let rec collect_funs ppf accu = function
  | { descr = Ast.FunDecl e } :: rest -> 
      let (_,e) = Typer.expr e in
      collect_funs ppf (e::accu) rest
  | rest ->
      insert_type_bindings ppf (Typer.type_rec_funs !typing_env accu);
      Typer.report_unused_branches ();
      insert_eval_bindings ppf (Eval.eval_rec_funs !eval_env accu);
      rest

let rec collect_types ppf accu = function
  | { descr = Ast.TypeDecl (x,t) } :: rest -> 
      collect_types ppf ((x,t) :: accu) rest
  | rest ->
      Typer.register_global_types accu;
      rest

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)
  | { descr = Ast.EvalStatement e } :: rest ->
      let (fv,e) = Typer.expr 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;
      if not !quiet then
	Format.fprintf ppf "|- %a@." print_norm t;
      let v = Eval.eval !eval_env e in
      if not !quiet then
	Format.fprintf ppf "=> @[%a@]@." print_value v;
      phrases ppf rest
  | { descr = Ast.LetDecl (p,e) } :: rest ->
      let decl = Typer.let_decl p e in
      insert_type_bindings ppf (Typer.type_let_decl !typing_env decl);
      Typer.report_unused_branches ();
      insert_eval_bindings ppf (Eval.eval_let_decl !eval_env decl);
      phrases ppf rest
  | { descr = Ast.Debug l } :: rest -> 
      debug ppf l;
      phrases ppf rest
  | [] -> ()
  | _ -> assert false

let run rule ppf ppf_err input =
199
  try 
200
    let p = 
201
      try rule input
202
      with
203
204
205
206
	| Stdpp.Exc_located (_, (Location _ as e)) ->
	    Parser.sync input; raise e
	| Stdpp.Exc_located ((i,j), e) -> 
	    Parser.sync input; raise_loc i j e
207
    in
208
    phrases ppf p;
209
    true
210
  with 
211
    | (End_of_file | Failure _ | Not_found | Invalid_argument _) as e -> 
212
	raise e  (* To get ocamlrun stack trace *)
213
214
215
216
    | exn -> 
	print_exn ppf_err exn;
	Format.fprintf ppf_err "@.";
	false
217

218
219
let script = run Parser.prog
let toplevel = run Parser.top_phrases