A pretty-printer for Dedukti error messages

dk_lexer.mll

+{
+  open Dk_parser
+  exception Unexpected_char of string
+}
+
+let id = [ 'a'-'z' '_' '0'-'9' ] ['a'-'z' 'A'-'Z' '_' '0'-'9' '.' ]*
+let num = [ '0'-'9' ]+
+
+rule dktoken = parse
+    | "ERROR file: " (id as s) ' ' { ERRORFILE (s) }
+    | "line:" (num as n) ' ' { LINE (n) }
+    | "column:" (num as n) ' ' { COLUMN (n) }
+    | "Expected: " { EXPECTED }
+    | "Inferred: " { INFERED }
+    | "Error while typing " { ERR_TYPING }
+    | "in context:" { INCONTEXT }
+    | '\''([^ '\'']+ as s)'\'' { QTERM (s) }
+    | [ ' ' '\t' ] { dktoken lexbuf }
+    | '\n' { dktoken lexbuf }
+    | '(' { LPAR }
+    | ')' { RPAR }
+    | '.' { DOT }
+    | ':' { COL }
+    | "pts.eT" { EPS }
+    | "dk_obj.preObj" { PO }
+    | "dk_obj.Expr" { EXPR }
+    | "dk_type.assoc" { ASSOC }
+    | "dk_type.nil" { TNIL }
+    | "dk_type.cons" { TCONS }
+    | "dk_string.nil" { SNIL }
+    | "dk_string.cons" { SCONS }
+    | "dk_machine_int.O" { MINT_0 }
+    | "dk_machine_int.S0" { MINT_S0 }
+    | "dk_machine_int.S1" { MINT_S1 }
+    | "dk_nat.O" { NAT_0 }
+    | "dk_nat.S" { NAT_S }
+    | "dk_domain.nil" { DNIL }
+    | "dk_domain.cons" { DCONS }
+    | id as s { ID (s) }
+    | [ 'A'-'Z' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']* as s { CID (s) }
+    | _ as c { raise (Unexpected_char (Printf.sprintf"'%c'" c)) }
+    | eof { raise End_of_file }

dk_parser.mly

+%{
+  open Parsetree
+
+  let parse_error s = print_endline s
+
+  exception Parse_list_error of label * stype * stype
+  exception Invalid_char_length of int * int
+
+  let rec print_ty = function
+    | Tcid (Cid s) -> Format.eprintf "%s" s
+    | Tlist ll ->
+      Format.eprintf "[@[";
+      print_object ll;
+      Format.eprintf "@]]"
+    | Tarr (ty1, ty2) ->
+      Format.eprintf "(";
+      print_ty ty1;
+      Format.eprintf ")@ (";
+      print_ty ty2;
+      Format.eprintf ")";
+  and print_object = function
+    | [] -> ()
+    | [ (Label l, ty) ] ->
+      Format.eprintf "%s :@ " l;
+      print_ty ty
+    | (Label l, ty) :: ll ->
+      Format.eprintf "%s :@ " l;
+      print_ty ty;
+      Format.eprintf " ;@ ";
+      print_object ll
+
+  let domain = function
+    | Tcid _
+    | Tarr _ -> []
+    | Tlist ll -> List.map fst ll
+
+%}
+
+%token <string> ID CID
+%token LPAR RPAR DOT COL
+%token EPS EXPR PO TNIL TCONS SNIL SCONS MINT_0 MINT_S0 MINT_S1 NAT_0 NAT_S DNIL DCONS ASSOC
+%token EXPECTED INFERED ERR_TYPING INCONTEXT
+%token <string> ERRORFILE LINE COLUMN QTERM
+
+%start prog
+%type <unit> prog
+
+%%
+
+prog:  error_msg context EXPECTED sty DOT INFERED sty DOT
+  {
+    $1 ();
+    $2 ();
+    Format.eprintf "Expected: ";
+    print_ty $4;
+    Format.eprintf ".\nInfered: ";
+    print_ty $7;
+    Format.eprintf ".\n";
+  };
+
+error_msg: ERRORFILE LINE COLUMN ERR_TYPING QTERM INCONTEXT
+  {
+    fun () ->
+      Format.eprintf "Error file: %s line:%s column:%s Error while typing '%s' in context:\n"
+        $1 $2 $3 $5
+  }
+;
+
+context:   /* empty */ { fun () -> () }
+         | decl context { fun () -> ($1 (); $2 ()) }
+;
+
+decl: ID COL sty { fun () -> Printf.eprintf "%s: " $1; print_ty $3; Printf.eprintf "\n"};
+
+ty:   CID                       { Tcid (Cid ($1)) }
+    | LPAR ty RPAR                { $2 }
+    | TNIL                     { Tlist [] }
+    | TCONS string ty ty       { match $4 with
+                                    | Tlist ll ->
+                                      Tlist ((Label $2, $3) :: ll)
+                                    | _ -> raise (Parse_list_error (Label $2, $3, $4))
+                                  }
+;
+
+sty:   EPS LPAR PO ty LPAR ASSOC ty RPAR domain RPAR { assert ($4 = $7); assert ($9 = domain $4); $4 }
+     | EXPR ty                                       { $2 }
+;
+
+string:   SNIL              { "" }
+        | SCONS char string { Printf.sprintf "%c%s" $2 $3 }
+        | LPAR string RPAR     { $2 }
+;
+
+char: mint  { let (length, n) = $1 in
+              if length = 7 then
+                Char.chr n
+              else raise (Invalid_char_length (length, n)) };
+
+mint:   MINT_0 { (0, 0) }
+      | MINT_S0 nat mint { let (length, n) = $3 in
+                              if $2 = length then (length+1, 2*n)
+                              else raise (Invalid_char_length (length, n)) }
+      | MINT_S1 nat mint { let (length, n) = $3 in
+                              if $2 = length then (length+1, 2*n+1)
+                              else raise (Invalid_char_length (length, n)) }
+      | LPAR mint RPAR     { $2 }
+;
+
+nat:   NAT_0 { 0 }
+     | NAT_S nat { $2 + 1 }
+     | LPAR nat RPAR { $2 }
+;
+
+domain:   DNIL { [] }
+        | DCONS string domain { (Label $2) :: $3 }
+        | LPAR domain RPAR { $2 }
+;
+
+%%

sigmaid_err.ml

+
+let main () =
+  Arg.parse [] (fun file ->
+    Base.labels := [];
+    let input = open_in file in
+    let lb = Lexing.from_channel input in
+    try
+      Dk_parser.prog Dk_lexer.dktoken lb
+    with
+    | e ->
+      let start = lb.Lexing.lex_start_p in
+      let file = start.Lexing.pos_fname in
+      let line = start.Lexing.pos_lnum  in
+      let cnum = start.Lexing.pos_cnum - start.Lexing.pos_bol in
+      let tok = Lexing.lexeme lb in
+      Format.eprintf "Error File: %s, line: %d, column: %d, Token \"%s\"@\n@."
+        file line cnum tok;
+      raise e)
+    "Please provide a file name."
+
+let _ = main ()