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