cduce.ml 6.81 KB
Newer Older
1 2
open Location

3
let print_norm ppf d = 
4 5 6 7 8
  Location.protect ppf 
    (fun ppf -> Types.Print.print_descr ppf ((*Types.normalize*) d))

let print_value ppf v =
  Location.protect ppf (fun ppf -> Value.print ppf v)
9

10
let rec print_exn ppf = function
11
  | Location (loc, exn) ->
12
      Format.fprintf ppf "Error %a:@\n" Location.print_loc loc;
13
      Format.fprintf ppf "%a" Location.html_hilight loc;
14
      print_exn ppf exn
15 16
  | Value.CDuceExn v ->
      Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@\n"
17
        print_value v
18 19
  | Typer.WrongLabel (t,l) ->
      Format.fprintf ppf "Wrong record selection: the label %s@\n" 
20
        (Types.LabelPool.value l);
21
      Format.fprintf ppf "applied to an expression of type %a@\n"
22
        print_norm t
23 24
  | Typer.MultipleLabel l ->
      Format.fprintf ppf "Multiple occurences for the record label %s@\n"
25
        (Types.LabelPool.value l);
26 27
  | Typer.ShouldHave (t,msg) ->
      Format.fprintf ppf "This expression should have type %a@\n%s@\n" 
28
        print_norm t
29
        msg
30
  | Typer.Constraint (s,t,msg) ->
31
      Format.fprintf ppf "This expression should have type %a@\n" 
32
        print_norm t;
33
      Format.fprintf ppf "but its infered type is: %a@\n" 
34
        print_norm s;
35
      Format.fprintf ppf "which is not a subtype, as shown by the value %a@\n" 
36
	Types.Sample.print (Types.Sample.get (Types.diff s t));
37
      Format.fprintf ppf "%s@\n" msg
38 39 40
  | Typer.NonExhaustive t ->
      Format.fprintf ppf "This pattern matching is not exhaustive@\n";
      Format.fprintf ppf "Residual type: %a@\n"
41
	print_norm t;
42
      Format.fprintf ppf "Sample value: %a@\n" 
43
	Types.Sample.print (Types.Sample.get t)
44 45
  | Typer.UnboundId x ->
      Format.fprintf ppf "Unbound identifier %s@\n" x
46 47 48 49 50 51 52 53
  | 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"
54
  | Parser.Error s | Stream.Error s -> 
55
      Format.fprintf ppf "Parsing error: %s@\n" s
56 57
  | Location.Generic s ->
      Format.fprintf ppf "%s@\n" s
58 59 60
  | exn ->
      Format.fprintf ppf "%s@\n" (Printexc.to_string exn)

61
let debug ppf = function
62 63 64 65 66 67
  | `Filter (t,p) -> 
      Format.fprintf ppf "[DEBUG:filter]@\n";
      let t = Typer.typ t
      and p = Typer.pat p in
      let f = Patterns.filter (Types.descr t) p in
      List.iter (fun (x,t) ->
68
		   Format.fprintf ppf " %s:%a@\n" x
69 70 71 72 73 74 75 76 77 78 79 80 81 82
		     print_norm (Types.descr t)) f
  | `Accept p ->
      Format.fprintf ppf "[DEBUG:accept]@\n";
      let p = Typer.pat p in
      let t = Patterns.accept p in
      Format.fprintf ppf " %a@\n" Types.Print.print t
  | `Compile (t,pl) ->
      Format.fprintf ppf "[DEBUG:compile]@\n";
      let t = Typer.typ t
      and pl = List.map Typer.pat pl in
      let pl = Array.of_list 
		 (List.map (fun p -> Patterns.Compile.normal 
			      (Patterns.descr p)) pl) in
      Patterns.Compile.show ppf (Types.descr t) pl
83 84 85 86 87 88 89 90 91
  | `Normal_record t ->
      Format.fprintf ppf "[DEBUG:normal_record]@\n";
      let t = Types.descr (Typer.typ t) in
      let count = ref 0 and seen = ref [] in
      match Types.Record.first_label t with
	    | `Empty -> Format.fprintf ppf "Empty"
	    | `Any -> Format.fprintf ppf "Any"
	    | `Label l ->
		let (pr,ab) = Types.Record.normal' t l in
92
		Format.fprintf ppf "Label (%s,@[" (Types.LabelPool.value l);
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
		List.iter (fun (d,n) ->
			     Format.fprintf ppf "%a => @[%a@];@\n"
			     Types.Print.print_descr d
			     Types.Print.print_descr n
			  ) pr;
		Format.fprintf ppf "@] Absent: @[%a@])@\n" 
		  Types.Print.print_descr 
		  (match ab with Some x -> x | None -> Types.empty)
(*
  | `Normal_record t ->
      Format.fprintf ppf "[DEBUG:normal_record]@\n";
      let t = Types.descr (Typer.typ t) in
      let r = Types.Record.normal t in
      let count = ref 0 and seen = ref [] in
      let rec aux ppf x =
	try 
	  let no = List.assq x !seen in
	  Format.fprintf ppf "[[%i]]" no
	with Not_found ->
	  incr count;
	  seen := (x, !count) :: !seen;
	  Format.fprintf ppf "[[%i]]:" !count;
	  match x with
	    | `Success -> Format.fprintf ppf "Success"
	    | `Fail -> Format.fprintf ppf "Fail"
	    | `Label (l,pr,ab) ->
		Format.fprintf ppf "Label (%s,@[" (Types.label_name l);
		List.iter (fun (d,n) ->
			     Format.fprintf ppf "%a => @[%a@];@\n"
			     Types.Print.print_descr d
			     aux n
			  ) pr;
		Format.fprintf ppf "@] Absent: @[%a@])" aux ab
      in
      Format.fprintf ppf "%a@\n" aux r
*)
129 130


131
let mk_builtin () =
132
  List.iter 
133 134
    (fun (n,t) -> Typer.register_global_types [n, mk noloc (Ast.Internal t)])
    Builtin.types
135

136 137 138 139 140
let () = mk_builtin ()

let typing_env = State.ref "Cduce.typing_env" Typer.Env.empty
let eval_env = State.ref "Cduce.eval_env" Eval.Env.empty

141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
let run ppf input =
  let insert_type_bindings = 
    List.iter (fun (x,t) ->
		 typing_env := Typer.Env.add x t !typing_env;
		 Format.fprintf ppf "|- %s : %a@\n@." x print_norm t) 
  in
  
  let type_decl decl =
    insert_type_bindings (Typer.type_let_decl !typing_env decl)
  in

  let eval_decl decl =
    let bindings = Eval.eval_let_decl !eval_env decl in
    List.iter 
      (fun (x,v) ->
	 Eval.enter_global x v;
157
	 Format.fprintf ppf "=> %s : @[%a@]@\n@." x print_value v
158 159 160 161 162 163 164 165
      ) bindings
  in

  let phrase ph =
    match ph.descr with
      | Ast.EvalStatement e ->
	  let (fv,e) = Typer.expr e in
	  let t = Typer.type_check !typing_env e Types.any true in
166
	  Location.dump_loc ppf e.Typed.exp_loc;
167 168
	  Format.fprintf ppf "|- %a@\n@." print_norm t;
	  let v = Eval.eval !eval_env e in
169
	  Format.fprintf ppf "=> @[%a@]@\n@." print_value v
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
      | Ast.LetDecl (p,{descr=Ast.Abstraction _}) -> ()
      | Ast.LetDecl (p,e) ->
	  let decl = Typer.let_decl p e in
	  type_decl decl;
	  eval_decl decl
      | Ast.TypeDecl _ -> ()
      | Ast.Debug l -> debug ppf l
      | _ -> assert false
  in

  let do_fun_decls decls =
    let decls = List.map (fun (p,e) -> Typer.let_decl p e) decls in
    insert_type_bindings (Typer.type_rec_funs !typing_env decls);
    List.iter eval_decl decls
  in
185
  try 
186 187 188 189 190 191
    let p = 
      try Parser.prog input
      with
	| Stdpp.Exc_located (_, (Location _ as e)) -> raise e
	| Stdpp.Exc_located (loc, e) -> raise (Location (loc, e))
    in
192
    let (type_decls,fun_decls) = 
193
      List.fold_left
194 195 196 197
	(fun ((typs,funs) as accu) ph -> match ph.descr with
	   | Ast.TypeDecl (x,t) -> ((x,t) :: typs,funs)
	   | Ast.LetDecl (p,({descr=Ast.Abstraction _} as e)) -> 
	       (typs, (p,e)::funs)
198
	   | _ -> accu
199
	) ([],[]) p in
200
    Typer.register_global_types type_decls;
201
    do_fun_decls fun_decls;
202 203
    List.iter phrase p;
    true
204
  with 
205
    | (Failure _ | Not_found | Invalid_argument _) as e -> 
206
	raise e  (* To get ocamlrun stack trace *)
207
    | exn -> print_exn ppf exn; false
208
	
209