|
1 | 1 |
|
| 2 | +preprocess-index-types := (); |
| 3 | + |
2 | 4 | preprocess := λprogram . (tail(
|
3 |
| - () |
| 5 | + (preprocess-index-typedefs program) |
4 | 6 | (preprocess-apply-macros program)
|
5 | 7 | ));
|
6 | 8 |
|
| 9 | +preprocess-index-typedefs := λprogram . (tail( |
| 10 | + (while program ( |
| 11 | + (preprocess-index-typedef (tail program)) |
| 12 | + (set program (head program)) |
| 13 | + )) |
| 14 | +)); |
| 15 | + |
| 16 | +preprocess-index-typedef := λterm . (match term ( |
| 17 | + () |
| 18 | + ( (Type( l ds )) ( |
| 19 | + (preprocess-index-indices( ds 0 )) |
| 20 | + )) |
| 21 | +)); |
| 22 | + |
| 23 | +preprocess-index-indices := λdef index . (match def ( |
| 24 | + () |
| 25 | + ( (App( (App( tds (Variable '|) )) body )) (tail( |
| 26 | + (preprocess-index-indices( tds (i2s(inc(s2i index))) )) |
| 27 | + (preprocess-index-index( body index )) |
| 28 | + ))) |
| 29 | + ( body ( |
| 30 | + (preprocess-index-index( body index )) |
| 31 | + )) |
| 32 | +)); |
| 33 | + |
| 34 | +preprocess-index-index := λbody index . (match body ( |
| 35 | + () |
| 36 | + ( (Literal tag) (tail( |
| 37 | + (set preprocess-index-types (preprocess-index-types (tag index))) |
| 38 | + ))) |
| 39 | + ( (App( (Literal tag) args )) (tail( |
| 40 | + (set preprocess-index-types (preprocess-index-types (tag index))) |
| 41 | + ))) |
| 42 | +)); |
| 43 | + |
| 44 | +preprocess-index-of-tag := λtag . (tail( |
| 45 | + (local indices) |
| 46 | + (local index) |
| 47 | + (set indices preprocess-index-types) |
| 48 | + (while indices ( |
| 49 | + (if (eq( (head(tail indices)) tag )) ( |
| 50 | + (set index (tail(tail indices))) |
| 51 | + ) ()) |
| 52 | + (set indices (head indices)) |
| 53 | + )) |
| 54 | + index |
| 55 | +)); |
| 56 | + |
7 | 57 | substitute-macro-body := λkvs e . (match e (
|
8 | 58 | ()
|
9 | 59 | ((Variable n) (tail(
|
@@ -53,7 +103,24 @@ try-destructure-macro := λlhs e . (match (lhs e) (
|
53 | 103 | (if (eq( pl el )) Accept ())
|
54 | 104 | ))
|
55 | 105 | ( ( (App( (Literal :Literal:) (Variable pv) )) (Literal el)) (
|
56 |
| - (Accept (KV( pv e ))) |
| 106 | + (if (typecheck-is-constructor el) |
| 107 | + () |
| 108 | + (Accept (KV( pv e ))) |
| 109 | + ) |
| 110 | + )) |
| 111 | + ( ( (App( (Literal :Tag:) (Variable pv) )) (Literal el)) ( |
| 112 | + (if (typecheck-is-constructor el) |
| 113 | + (Accept (KV( pv |
| 114 | + (App( |
| 115 | + (App( |
| 116 | + (Literal :) |
| 117 | + (Literal (preprocess-index-of-tag el)) |
| 118 | + )) |
| 119 | + (preprocess-restructure-type(parse-type( Constant+Literal+U64 ))) |
| 120 | + )) |
| 121 | + ))) |
| 122 | + () |
| 123 | + ) |
57 | 124 | ))
|
58 | 125 | ( ( (App( (Literal :Variable:) (Variable pv) )) (Variable el)) (
|
59 | 126 | (Accept (KV( pv e )))
|
|
0 commit comments