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