Commit 9f679fcd authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Also lex and parse terms from dedukti

parent b2949b10
......@@ -36,6 +36,9 @@ rule dktoken = parse
| "dk_nat.S" { NAT_S }
| "dk_domain.nil" { DNIL }
| "dk_domain.cons" { DCONS }
| "dk_obj.preselect" { PSEL }
| "dk_obj.preupdate" { PUPD }
| "lab_" (id as s ) { LABEL (s) }
| 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)) }
......
......@@ -36,15 +36,18 @@
%}
%token <string> ID CID
%token <string> ID CID LABEL
%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
%token PSEL PUPD
%start prog
%type <unit> prog
%start term
%type <unit> term
%%
prog: error_msg INCONTEXT context EXPECTED sty DOT INFERED sty DOT
......@@ -97,7 +100,8 @@ sty: EPS LPAR PO ty LPAR ASSOC ty RPAR domain RPAR { assert ($4 = $7); assert
string: SNIL { "" }
| SCONS char string { Printf.sprintf "%c%s" $2 $3 }
| LPAR string RPAR { $2 }
| LPAR string RPAR { $2 }
| LABEL { $1 }
;
char: mint { let (length, n) = $1 in
......@@ -125,4 +129,8 @@ domain: DNIL { [] }
| LPAR domain RPAR { $2 }
;
term: PSEL ty LPAR ASSOC ty RPAR domain string term {}
| PUPD ty LPAR ASSOC ty RPAR domain string term {}
| ID {}
;
%%
......@@ -5,7 +5,7 @@ let main () =
let input = open_in file in
let lb = Lexing.from_channel input in
try
Dk_parser.prog Dk_lexer.dktoken lb
Dk_parser.term Dk_lexer.dktoken lb
with
| e ->
let start = lb.Lexing.lex_start_p in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment