~thon/thon

ref: e1c37a8074e0966021671defe79956699db8ecd6 thon/parse/thon.grm -rw-r--r-- 2.7 KiB
e1c37a80Evan Bergeron Lower Type.Plus precedence; parse `data eq` tyrec 10 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
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
structure A = Ast

%%
%header (functor ThonLrValsFn (structure Token : TOKEN))

%eop EOF

%term
   EOF
 | ZERO
 | SUCC
 | LPAREN | RPAREN
 | PIPE
 | LAM
 | SARROW
 | COLON
 | NAT
 | REC
 | APP
 | TYPEOR
 | IDX of int
 | ID of string
 | GO
 | POLY
 | LEFT
 | RIGHT
 | FST
 | SND
 | COMMA
 | STAR
 | ALL
 | SOME
 | TYPEREC
 | DOT
 | UNIT
 | FOLD
 | UNFOLD
 | WITH
 | IMPL
 | AS
 | USE
 | IN
 | CASE
 | OF
 | LET
 | EQ
 | IFZ
 | FIX
 | FUN
 | DATA

%nonterm
   exp of A.Exp
 | typ of A.Typ
 | program of A.Exp

%verbose
%pos int
%start exp (* i think likely this should be program, but I really dont like that hack *)
%eop EOF

%name Thon

(* Each rule is then assigned the precedence of its rightmost terminal *)
(* If the rule has the higher precedence, the reduction is chosen. *)

(* The precedence grows down *)
%nonassoc TYPEOR (* Deliberately first *)
%nonassoc EOF ZERO SUCC LPAREN RPAREN LAM COLON NAT IDX ID REC PIPE POLY COMMA STAR LEFT RIGHT FST SND ALL SOME TYPEREC DOT UNIT FOLD UNFOLD WITH AS USE IN CASE OF IMPL LET EQ IFZ FIX FUN DATA
%right SARROW
%nonassoc APP GO (* Deliberately last *)

%%

(* program: *)
(*     GO exp (exp) *)

exp:
    LPAREN exp RPAREN (exp)
  | exp exp %prec APP (A.App(exp1, exp2))
  | exp typ %prec APP (A.TypApp(typ, exp))
  | ID (A.Var (ID, ~1))
  | ZERO (A.Zero)
  | SUCC exp (A.Succ exp)
  | UNIT (A.TmUnit)
  | LAM ID COLON typ SARROW exp (A.Lam (ID, typ, exp))
  | LET ID COLON typ EQ exp IN exp (A.Let (ID, typ, exp1, exp2))
  | IFZ exp OF ZERO SARROW exp PIPE SUCC ID SARROW exp (A.Ifz (exp1, exp2, ID, exp3))
  | REC exp OF ZERO SARROW exp PIPE ID SARROW exp (A.Rec (exp1, exp2, ID, exp3))
  | FUN ID COLON typ EQ exp IN exp (A.Let(ID1, typ1, A.Fix(ID1, typ1, exp1), exp2))
  | FIX ID COLON typ IN exp (A.Fix (ID, typ, exp))
  | POLY ID SARROW exp (A.TypAbs (ID, exp))
  | LPAREN exp COMMA exp RPAREN (A.Tuple(exp1, exp2))
  | FST exp (A.ProdLeft exp)
  | SND exp (A.ProdRight exp)
  | LEFT exp COLON typ (A.PlusLeft(typ, exp))
  | RIGHT exp COLON typ (A.PlusRight(typ, exp))
  | FOLD typ WITH exp (A.Fold(typ, exp))
  | UNFOLD exp (A.Unfold(exp))
  | IMPL typ WITH typ AS exp (A.Impl(typ2, exp, typ1))
  | USE exp AS LPAREN ID COMMA ID RPAREN IN exp (A.Use(exp1, ID1, ID2, exp2))
  | CASE exp OF ID SARROW exp PIPE ID SARROW exp (A.Case(exp1, ID1, exp2, ID2, exp3))

typ:
    NAT (A.Nat)
  | UNIT (A.Unit)
  | typ SARROW typ (A.Arr(typ1, typ2))
  | typ STAR typ (A.Prod(typ1, typ2))
  | LPAREN typ RPAREN (typ)
  | IDX (A.TypVar ("t", IDX)) 
  | ID (A.TypVar (ID, ~1)) 
  | ALL ID DOT typ (A.All (ID, typ))
  | SOME ID DOT typ (A.Some (ID, typ))
  | TYPEREC ID DOT typ (A.TyRec (ID, typ))
  | DATA ID EQ typ (A.TyRec (ID, typ))
  (* TODO should this take precedence below star and arrow? *)
  | typ PIPE typ %prec TYPEOR (A.Plus (typ1, typ2))