| 1 |
open Location |
open Location |
| 2 |
|
open Ident |
| 3 |
|
|
| 4 |
let () = |
let quiet = ref false |
| 5 |
List.iter |
|
| 6 |
(fun (n,t) -> Typer.register_global_types [n, mk noloc (Ast.Internal t)]) |
let typing_env = State.ref "Cduce.typing_env" Typer.Env.empty |
| 7 |
Builtin.types |
|
| 8 |
|
let print_norm ppf d = |
| 9 |
|
Location.protect ppf |
| 10 |
|
(fun ppf -> Types.Print.print_descr ppf ((*Types.normalize*) d)) |
| 11 |
|
|
| 12 |
|
let print_value ppf v = |
| 13 |
|
Location.protect ppf (fun ppf -> Value.print ppf v) |
| 14 |
|
|
| 15 |
|
let dump_env ppf = |
| 16 |
|
Format.fprintf ppf "Global types:"; |
| 17 |
|
Typer.dump_global_types ppf; |
| 18 |
|
Format.fprintf ppf ".@\n"; |
| 19 |
|
Eval.Env.iter |
| 20 |
|
(fun x v -> |
| 21 |
|
let t = Typer.Env.find x !typing_env in |
| 22 |
|
Format.fprintf ppf "@[|- %s : %a@ => %a@]@\n" |
| 23 |
|
(Id.value x) |
| 24 |
|
print_norm t |
| 25 |
|
print_value v |
| 26 |
|
) |
| 27 |
|
!Eval.global_env |
| 28 |
|
|
|
let input = Stream.of_channel stdin |
|
|
let ppf = Format.std_formatter |
|
|
let prog () = |
|
|
try Parser.prog input |
|
|
with |
|
|
| Stdpp.Exc_located (loc, e) -> |
|
|
raise (Location (loc, e)) |
|
| 29 |
|
|
| 30 |
let rec print_exn ppf = function |
let rec print_exn ppf = function |
| 31 |
| Location ((i,j), exn) -> |
| Location (loc, exn) -> |
| 32 |
Format.fprintf ppf "Error at chars %i-%i@\n" i j; |
Format.fprintf ppf "Error %a:@\n" Location.print_loc loc; |
| 33 |
|
Format.fprintf ppf "%a" Location.html_hilight loc; |
| 34 |
print_exn ppf exn |
print_exn ppf exn |
| 35 |
|
| Value.CDuceExn v -> |
| 36 |
|
Format.fprintf ppf "Uncaught CDuce exception: @[%a@]@\n" |
| 37 |
|
print_value v |
| 38 |
|
| Typer.WrongLabel (t,l) -> |
| 39 |
|
Format.fprintf ppf "Wrong record selection: the label %s@\n" |
| 40 |
|
(LabelPool.value l); |
| 41 |
|
Format.fprintf ppf "applied to an expression of type %a@\n" |
| 42 |
|
print_norm t |
| 43 |
| Typer.ShouldHave (t,msg) -> |
| Typer.ShouldHave (t,msg) -> |
| 44 |
Format.fprintf ppf "This expression should have type %a@\n%s@\n" |
Format.fprintf ppf "This expression should have type %a@\n%s@\n" |
| 45 |
Types.Print.print_descr t |
print_norm t |
| 46 |
msg |
msg |
| 47 |
| Typer.Constraint (s,t,msg) -> |
| Typer.Constraint (s,t,msg) -> |
| 48 |
Format.fprintf ppf "This expression should have type %a@\n" |
Format.fprintf ppf "This expression should have type %a@\n" |
| 49 |
Types.Print.print_descr t; |
print_norm t; |
| 50 |
Format.fprintf ppf "but its infered type is: %a@\n" |
Format.fprintf ppf "but its infered type is: %a@\n" |
| 51 |
Types.Print.print_descr s; |
print_norm s; |
| 52 |
Format.fprintf ppf "which is not a subtype, as shown by the value %a@\n" |
Format.fprintf ppf "which is not a subtype, as shown by the value %a@\n" |
| 53 |
Types.Print.print_sample (Types.Sample.get (Types.diff s t)); |
Types.Sample.print (Types.Sample.get (Types.diff s t)); |
| 54 |
Format.fprintf ppf "%s@\n" msg |
Format.fprintf ppf "%s@\n" msg |
| 55 |
| Typer.NonExhaustive t -> |
| Typer.NonExhaustive t -> |
| 56 |
Format.fprintf ppf "This pattern matching is not exhaustive@\n"; |
Format.fprintf ppf "This pattern matching is not exhaustive@\n"; |
| 57 |
Format.fprintf ppf "Residual type: %a@\n" |
Format.fprintf ppf "Residual type: %a@\n" |
| 58 |
Types.Print.print_descr t; |
print_norm t; |
| 59 |
Format.fprintf ppf "Sample value: %a@\n" |
Format.fprintf ppf "Sample value: %a@\n" |
| 60 |
Types.Print.print_sample (Types.Sample.get t) |
Types.Sample.print (Types.Sample.get t) |
| 61 |
|
| Typer.UnboundId x -> |
| 62 |
|
Format.fprintf ppf "Unbound identifier %s@\n" x |
| 63 |
|
| Wlexer.Illegal_character c -> |
| 64 |
|
Format.fprintf ppf "Illegal character (%s)@\n" (Char.escaped c) |
| 65 |
|
| Wlexer.Unterminated_comment -> |
| 66 |
|
Format.fprintf ppf "Comment not terminated@\n" |
| 67 |
|
| Wlexer.Unterminated_string -> |
| 68 |
|
Format.fprintf ppf "String literal not terminated@\n" |
| 69 |
|
| Wlexer.Unterminated_string_in_comment -> |
| 70 |
|
Format.fprintf ppf "This comment contains an unterminated string literal@\n" |
| 71 |
|
| Parser.Error s | Stream.Error s -> |
| 72 |
|
Format.fprintf ppf "Parsing error: %s@\n" s |
| 73 |
|
| Location.Generic s -> |
| 74 |
|
Format.fprintf ppf "%s@\n" s |
| 75 |
| exn -> |
| exn -> |
| 76 |
|
raise exn |
| 77 |
|
(* |
| 78 |
Format.fprintf ppf "%s@\n" (Printexc.to_string exn) |
Format.fprintf ppf "%s@\n" (Printexc.to_string exn) |
| 79 |
|
*) |
| 80 |
|
|
| 81 |
|
let debug ppf = function |
| 82 |
|
| `Subtype (t1,t2) -> |
| 83 |
|
Format.fprintf ppf "[DEBUG:subtype]@\n"; |
| 84 |
|
let t1 = Types.descr (Typer.typ t1) |
| 85 |
|
and t2 = Types.descr (Typer.typ t2) in |
| 86 |
|
Format.fprintf ppf "%a <= %a : %b@\n" print_norm t1 print_norm t2 |
| 87 |
|
(Types.subtype t1 t2) |
| 88 |
|
| `Filter (t,p) -> |
| 89 |
|
Format.fprintf ppf "[DEBUG:filter]@\n"; |
| 90 |
|
let t = Typer.typ t |
| 91 |
|
and p = Typer.pat p in |
| 92 |
|
let f = Patterns.filter (Types.descr t) p in |
| 93 |
|
List.iter (fun (x,t) -> |
| 94 |
|
Format.fprintf ppf " %s:%a@\n" (Id.value x) |
| 95 |
|
print_norm (Types.descr t)) f |
| 96 |
|
| `Compile2 (t,pl) -> |
| 97 |
|
Format.fprintf ppf "[DEBUG:compile2]@\n"; |
| 98 |
|
(* let t = Types.descr (Typer.typ t) in |
| 99 |
|
let pl = List.map (fun p -> |
| 100 |
|
let p = Typer.pat p in |
| 101 |
|
let a = Types.descr (Patterns.accept p) in |
| 102 |
|
(Some p, Types.cap a t)) pl in |
| 103 |
|
let d = Patterns.Compiler.make_dispatcher t pl in |
| 104 |
|
Patterns.Compiler.print_disp ppf d *) |
| 105 |
|
() |
| 106 |
|
|
| 107 |
|
| `Accept p -> |
| 108 |
|
Format.fprintf ppf "[DEBUG:accept]@\n"; |
| 109 |
|
let p = Typer.pat p in |
| 110 |
|
let t = Patterns.accept p in |
| 111 |
|
Format.fprintf ppf " %a@\n" Types.Print.print t |
| 112 |
|
| `Compile (t,pl) -> |
| 113 |
|
Format.fprintf ppf "[DEBUG:compile]@\n"; |
| 114 |
|
let t = Typer.typ t |
| 115 |
|
and pl = List.map Typer.pat pl in |
| 116 |
|
Patterns.Compile.debug_compile ppf t pl |
| 117 |
|
| `Normal_record p -> assert false |
| 118 |
|
|
| 119 |
|
|
| 120 |
|
|
| 121 |
|
let mk_builtin () = |
| 122 |
|
let bi = List.map (fun (n,t) -> [n, mknoloc (Ast.Internal t)]) |
| 123 |
|
Builtin.types in |
| 124 |
|
List.iter Typer.register_global_types bi |
| 125 |
|
|
| 126 |
|
let () = mk_builtin () |
| 127 |
|
|
| 128 |
|
|
| 129 |
|
let run ppf ppf_err input = |
| 130 |
|
let insert_type_bindings = |
| 131 |
|
List.iter (fun (x,t) -> |
| 132 |
|
typing_env := Typer.Env.add x t !typing_env; |
| 133 |
|
if not !quiet then |
| 134 |
|
Format.fprintf ppf "|- %s : %a@\n@." (Id.value x) print_norm t) |
| 135 |
|
in |
| 136 |
|
|
| 137 |
|
let type_decl decl = |
| 138 |
|
insert_type_bindings (Typer.type_let_decl !typing_env decl) |
| 139 |
|
in |
| 140 |
|
|
| 141 |
|
let eval_decl decl = |
| 142 |
|
let bindings = Eval.eval_let_decl Eval.Env.empty decl in |
| 143 |
|
List.iter |
| 144 |
|
(fun (x,v) -> |
| 145 |
|
Eval.enter_global x v; |
| 146 |
|
if not !quiet then |
| 147 |
|
Format.fprintf ppf "=> %s : @[%a@]@\n@." (Id.value x) print_value v |
| 148 |
|
) bindings |
| 149 |
|
in |
| 150 |
|
|
| 151 |
let phrase ph = |
let phrase ph = |
| 152 |
match ph.descr with |
match ph.descr with |
| 153 |
| Ast.EvalStatement e -> |
| Ast.EvalStatement e -> |
| 154 |
let (fv,e) = Typer.expr e in |
let (fv,e) = Typer.expr e in |
| 155 |
let t = Typer.type_check Typer.Env.empty e Types.any true in |
let t = Typer.type_check !typing_env e Types.any true in |
| 156 |
Format.fprintf ppf "%a@\n" Types.Print.print_descr t; |
Location.dump_loc ppf e.Typed.exp_loc; |
| 157 |
|
if not !quiet then |
| 158 |
|
Format.fprintf ppf "|- %a@\n@." print_norm t; |
| 159 |
|
let v = Eval.eval Eval.Env.empty e in |
| 160 |
|
if not !quiet then |
| 161 |
|
Format.fprintf ppf "=> @[%a@]@\n@." print_value v |
| 162 |
|
| Ast.LetDecl (p,{descr=Ast.Abstraction _}) -> () |
| 163 |
|
| Ast.LetDecl (p,e) -> |
| 164 |
|
let decl = Typer.let_decl p e in |
| 165 |
|
type_decl decl; |
| 166 |
|
eval_decl decl |
| 167 |
| Ast.TypeDecl _ -> () |
| Ast.TypeDecl _ -> () |
| 168 |
|
| Ast.Debug l -> debug ppf l |
| 169 |
| _ -> assert false |
| _ -> assert false |
| 170 |
|
in |
| 171 |
|
|
| 172 |
let () = |
let do_fun_decls decls = |
| 173 |
|
let decls = List.map (fun (p,e) -> Typer.let_decl p e) decls in |
| 174 |
|
insert_type_bindings (Typer.type_rec_funs !typing_env decls); |
| 175 |
|
List.iter eval_decl decls |
| 176 |
|
in |
| 177 |
|
let rec phrases funs = function |
| 178 |
|
| { descr = Ast.LetDecl (p,({descr=Ast.Abstraction _} as e))} :: phs -> |
| 179 |
|
phrases ((p,e)::funs) phs |
| 180 |
|
| ph :: phs -> |
| 181 |
|
do_fun_decls funs; |
| 182 |
|
phrase ph; |
| 183 |
|
phrases [] phs |
| 184 |
|
| _ -> |
| 185 |
|
do_fun_decls funs |
| 186 |
|
in |
| 187 |
try |
try |
| 188 |
let p = prog () in |
let p = |
| 189 |
let type_decls = |
try Parser.prog input |
| 190 |
|
with |
| 191 |
|
| Stdpp.Exc_located (_, (Location _ as e)) -> raise e |
| 192 |
|
| Stdpp.Exc_located ((i,j), e) -> raise_loc i j e |
| 193 |
|
in |
| 194 |
|
let (type_decls,fun_decls) = |
| 195 |
List.fold_left |
List.fold_left |
| 196 |
(fun accu ph -> match ph.descr with |
(fun ((typs,funs) as accu) ph -> match ph.descr with |
| 197 |
| Ast.TypeDecl (x,t) -> (x,t) :: accu |
| Ast.TypeDecl (x,t) -> ((x,t) :: typs,funs) |
| 198 |
|
| Ast.LetDecl (p,({descr=Ast.Abstraction _} as e)) -> |
| 199 |
|
(typs, (p,e)::funs) |
| 200 |
| _ -> accu |
| _ -> accu |
| 201 |
) [] p in |
) ([],[]) p in |
| 202 |
Typer.register_global_types type_decls; |
Typer.register_global_types type_decls; |
| 203 |
List.iter phrase p |
phrases [] p; |
| 204 |
with (Failure _) as e -> raise e | exn -> print_exn ppf exn |
true |
| 205 |
|
with |
| 206 |
|
| (Failure _ | Not_found | Invalid_argument _) as e -> |
| 207 |
|
raise e (* To get ocamlrun stack trace *) |
| 208 |
|
| exn -> print_exn ppf_err exn; false |
| 209 |
|
|
| 210 |
|
|