93 lines
2.2 KiB
OCaml
93 lines
2.2 KiB
OCaml
%{
|
|
open Lam
|
|
open Types
|
|
open Proof
|
|
open Parser_entry
|
|
%}
|
|
|
|
%token EOF
|
|
|
|
%token DOT COMMA
|
|
%token BOT EXFALSO TILDE
|
|
%token LPAREN RPAREN
|
|
%token FUN ARR COLON TARR
|
|
%token AND OR
|
|
%token <string> VARID
|
|
%token <string> TYID
|
|
|
|
%token GOAL UNDO QED CHECK
|
|
%token EXACT ASSUMPTION INTRO INTROS CUT APPLY
|
|
%token LEFT RIGHT SPLIT TRY
|
|
%token L R
|
|
|
|
%right TARR
|
|
%right OR
|
|
%right AND
|
|
%right TILDE
|
|
|
|
|
|
%start main
|
|
%type <parser_entry> main
|
|
|
|
%%
|
|
main:
|
|
| e=expression EOF { Lam e }
|
|
| ts=nonempty_list(instr) EOF { Instr ts }
|
|
|
|
instr:
|
|
| c=command DOT { Cmd c }
|
|
| t=tactic DOT { Tact t }
|
|
|
|
command:
|
|
| GOAL t=ty { Goal t }
|
|
| UNDO { Undo }
|
|
| QED { Qed }
|
|
| CHECK { Check }
|
|
|
|
tactic:
|
|
| EXACT e=expression { TExact_term e }
|
|
| EXACT s=TYID { TExact_proof s }
|
|
| ASSUMPTION { TAssumption }
|
|
| INTROS { TIntros }
|
|
| INTRO { TIntro }
|
|
| SPLIT { TSplit }
|
|
| RIGHT { TRight }
|
|
| LEFT { TLeft }
|
|
| CUT t=ty { TCut t }
|
|
| APPLY s=TYID { TApply s }
|
|
| TRY t=tactic { TTry t }
|
|
|
|
ty_annot:
|
|
| id=VARID COLON t=ty { (id, t) }
|
|
|
|
ty:
|
|
| id=TYID { TVar(id) }
|
|
| BOT { Bot }
|
|
| LPAREN t=ty RPAREN { t }
|
|
| TILDE t=ty { Arr(t, Bot) }
|
|
| t1=ty AND t2=ty { And(t1, t2) }
|
|
| t1=ty OR t2=ty { Or(t1, t2) }
|
|
| t1=ty TARR t2=ty { Arr(t1, t2) }
|
|
|
|
expression:
|
|
| FUN LPAREN annot=ty_annot RPAREN ARR e=expression
|
|
{ Fun (annot, e) }
|
|
| EXFALSO LPAREN e=expression COLON t=ty RPAREN
|
|
{ Exf (e, t) }
|
|
| LPAREN e1=expression COMMA e2=expression RPAREN
|
|
{ Pair(e1, e2) }
|
|
| L LPAREN e=expression COLON t=ty RPAREN
|
|
{ Left(e, t) }
|
|
| R LPAREN e=expression COLON t=ty RPAREN
|
|
{ Right(e, t) }
|
|
| e=app_expr { e }
|
|
|
|
app_expr:
|
|
| e=app_expr a=atomic { App (e, a) }
|
|
| a=atomic { a }
|
|
|
|
atomic:
|
|
| id=VARID { Var id }
|
|
| LPAREN e=expression RPAREN
|
|
{ e }
|