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