Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 108 lines (90 sloc) 2.232 kb
9c6ca0f @andrejbauer Initial version
authored
1 %{
8a0ef44 @andrejbauer Abstract syntax with variable names.
authored
2 open Syntax
0f16e93 @andrejbauer Support for iterated binders
authored
3
4 (* Build nested lambdas *)
5 let rec make_lambda e = function
6 | [] -> e
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
7 | ((xs, t), loc) :: lst ->
0f16e93 @andrejbauer Support for iterated binders
authored
8 let e = make_lambda e lst in
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
9 List.fold_left (fun e x -> (Lambda (x, t, e), loc)) e xs
0f16e93 @andrejbauer Support for iterated binders
authored
10
11 (* Build nested pies *)
12 let rec make_pi e = function
13 | [] -> e
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
14 | ((xs, t), loc) :: lst ->
15 let e = make_pi e lst in
16 List.fold_left (fun e x -> (Pi (x, t, e), loc)) e xs
0f16e93 @andrejbauer Support for iterated binders
authored
17
9c6ca0f @andrejbauer Initial version
authored
18 %}
19
20 %token FORALL FUN TYPE
21 %token <int> NUMERAL
22 %token <string> NAME
1235d47 @andrejbauer Syntax closer to Coq
authored
23 %token LPAREN RPAREN
0c0b6af @andrejbauer Definitions
authored
24 %token COLON COMMA PERIOD COLONEQUAL
1235d47 @andrejbauer Syntax closer to Coq
authored
25 %token ARROW DARROW
0c0b6af @andrejbauer Definitions
authored
26 %token QUIT HELP PARAMETER CHECK EVAL CONTEXT DEFINITION
9c6ca0f @andrejbauer Initial version
authored
27 %token EOF
28
8a0ef44 @andrejbauer Abstract syntax with variable names.
authored
29 %start <Syntax.directive list> directives
9c6ca0f @andrejbauer Initial version
authored
30
31 %%
32
33 (* Toplevel syntax *)
34
1235d47 @andrejbauer Syntax closer to Coq
authored
35 directives:
36 | dir = directive PERIOD EOF
37 { [dir] }
38 | dir = directive PERIOD lst = directives
39 { dir :: lst }
9c6ca0f @andrejbauer Initial version
authored
40
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
41 directive: mark_position(plain_directive) { $1 }
42 plain_directive:
9c6ca0f @andrejbauer Initial version
authored
43 | QUIT
44 { Quit }
45 | HELP
46 { Help }
1235d47 @andrejbauer Syntax closer to Coq
authored
47 | PARAMETER x = NAME COLON e = expr
48 { Parameter (String x, e) }
49 | CHECK e = expr
50 { Check e }
51 | EVAL e = expr
52 { Eval e}
0c0b6af @andrejbauer Definitions
authored
53 | DEFINITION x = NAME COLONEQUAL e = expr
54 { Definition (String x, e) }
9c6ca0f @andrejbauer Initial version
authored
55 | CONTEXT
56 { Context }
57
58 (* Main syntax tree *)
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
59 expr: mark_position(plain_expr) { $1 }
60 plain_expr:
61 | e = plain_app_expr
9c6ca0f @andrejbauer Initial version
authored
62 { e }
0f16e93 @andrejbauer Support for iterated binders
authored
63 | FORALL lst = abstraction COMMA e = expr
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
64 { fst (make_pi e lst) }
65 | FUN lst = abstraction DARROW e = expr
66 { fst (make_lambda e lst) }
9c6ca0f @andrejbauer Initial version
authored
67 | t1 = app_expr ARROW t2 = expr
68 { Pi (Dummy, t1, t2) }
69
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
70 app_expr: mark_position(plain_app_expr) { $1 }
71 plain_app_expr:
72 | e = plain_simple_expr
9c6ca0f @andrejbauer Initial version
authored
73 { e }
74 | e1 = app_expr e2 = simple_expr
75 { App (e1, e2) }
76
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
77 simple_expr: mark_position(plain_simple_expr) { $1 }
78 plain_simple_expr:
9c6ca0f @andrejbauer Initial version
authored
79 | n = NAME
80 { Var (String n) }
81 | TYPE k = NUMERAL
82 { Universe k }
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
83 | LPAREN e = plain_expr RPAREN
9c6ca0f @andrejbauer Initial version
authored
84 { e }
85
0f16e93 @andrejbauer Support for iterated binders
authored
86 abstraction:
87 | b = bind1
88 { [b] }
89 | bs = binds
90 { bs }
91
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
92 bind1: mark_position(plain_bind1) { $1 }
93 plain_bind1:
0f16e93 @andrejbauer Support for iterated binders
authored
94 | xs = nonempty_list(NAME) COLON t = expr
95 { (List.map (fun x -> String x) xs, t) }
9c6ca0f @andrejbauer Initial version
authored
96
0f16e93 @andrejbauer Support for iterated binders
authored
97 binds:
98 | LPAREN b = bind1 RPAREN
99 { [b] }
100 | LPAREN b = bind1 RPAREN lst = binds
101 { b :: lst }
9c6ca0f @andrejbauer Initial version
authored
102
d51e1e6 @andrejbauer Added source code positions and normalization by evaluation.
authored
103 mark_position(X):
104 x = X
105 { x, Position ($startpos, $endpos) }
106
9c6ca0f @andrejbauer Initial version
authored
107 %%
Something went wrong with that request. Please try again.