Skip to content

Commit d4e97f4

Browse files
arthurpaulinoarthurpaulino
committed
Aiur2 execution tests
1 parent 90d3bc9 commit d4e97f4

File tree

10 files changed

+478
-17
lines changed

10 files changed

+478
-17
lines changed

‎Ix/Aiur2/Bytecode.lean

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,19 +16,20 @@ inductive Op
1616
| call : FunIdx → Array ValIdx → Op
1717
| store : Array ValIdx → Op
1818
| load : (width : Nat) → ValIdx → Op
19+
deriving Repr
1920

2021
mutual
2122
inductive Ctrl where
2223
| match : ValIdx → Array (G × Block) → Option Block → Ctrl
2324
| return : SelIdx → Array ValIdx → Ctrl
24-
deriving Inhabited
25+
deriving Inhabited, Repr
2526

2627
structure Block where
2728
ops : Array Op
2829
ctrl : Ctrl
2930
minSelIncluded: SelIdx
3031
maxSelExcluded: SelIdx
31-
deriving Inhabited
32+
deriving Inhabited, Repr
3233
end
3334

3435
/-- The circuit layout of a function -/
@@ -41,17 +42,27 @@ structure CircuitLayout where
4142
auxiliaries : Nat
4243
/-- Constraint slots that can be shared in different paths of the circuit. -/
4344
sharedConstraints : Nat
44-
deriving Inhabited
45+
deriving Inhabited, Repr
4546

4647
structure Function where
4748
inputSize : Nat
4849
outputSize : Nat
4950
body : Block
5051
circuitLayout: CircuitLayout
52+
deriving Inhabited, Repr
5153

5254
structure Toplevel where
5355
functions : Array Function
5456
memoryWidths : Array Nat
57+
deriving Repr
58+
59+
@[extern "c_rs_toplevel_execute_test"]
60+
private opaque Toplevel.executeTest' :
61+
@& Toplevel → @& FunIdx → @& Array G → USize → Array G
62+
63+
def Toplevel.executeTest (toplevel : Toplevel) (funIdx : FunIdx) (args : Array G) : Array G :=
64+
let function := toplevel.functions[funIdx]!
65+
toplevel.executeTest' funIdx args function.outputSize.toUSize
5566

5667
end Bytecode
5768

‎Ix/Aiur2/Compile.lean

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,10 @@ def setSharedData (sharedData : SharedData) : LayoutM Unit :=
5353
auxiliaries := sharedData.auxiliaries
5454
sharedConstraints := sharedData.constraints } }
5555

56-
def opLayout : Bytecode.Op → LayoutM Unit := fun _ => pure () -- TODO
56+
def opLayout : Bytecode.Op → LayoutM Unit
57+
| .store values => addMemWidth values.size
58+
| .load width _ => addMemWidth width
59+
| _ => pure () -- TODO
5760

5861
partial def blockLayout (block : Bytecode.Block) : LayoutM Unit := do -- TODO
5962
block.ops.forM opLayout
@@ -299,15 +302,15 @@ partial def toIndex
299302
let arg ← toIndex layoutMap bindings arg
300303
pure $ arg.extract offset (offset + length)
301304
| .store arg => do
302-
let arg ← toIndex layoutMap bindings arg
303-
pushOp (Bytecode.Op.store arg)
305+
let args ← toIndex layoutMap bindings arg
306+
pushOp (Bytecode.Op.store args)
304307
| .load ptr => do
305308
let size := match ptr.typ.unwrap with
306309
| .pointer typ => typSize layoutMap typ
307310
| _ => unreachable!
308311
let ptr ← toIndex layoutMap bindings ptr
309312
assert! (ptr.size == 1)
310-
pushOp (Bytecode.Op.load size (ptr[0]!)) size
313+
pushOp (Bytecode.Op.load size ptr[0]!) size
311314
| .ptrVal ptr => toIndex layoutMap bindings ptr
312315
-- | .trace str expr => do
313316
-- let arr ← toIndex layoutMap bindings expr

‎Ix/Aiur2/Meta.lean

Lines changed: 235 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,235 @@
1+
import Lean
2+
import Ix.Aiur2.Term
3+
4+
namespace Aiur
5+
6+
open Lean Elab Meta
7+
8+
abbrev ElabStxCat name := TSyntax name → TermElabM Expr
9+
10+
declare_syntax_cat pattern
11+
syntax ("." noWs)? ident : pattern
12+
syntax "_" : pattern
13+
syntax ident "(" pattern (", " pattern)* ")" : pattern
14+
syntax num : pattern
15+
syntax "(" pattern (", " pattern)* ")" : pattern
16+
syntax pattern "|" pattern : pattern
17+
18+
def elabListCore (head : α) (tail : Array α) (elabFn : α → TermElabM Expr)
19+
(listEltType : Expr) (isArray := false) : TermElabM Expr := do
20+
let mut elaborated := Array.mkEmpty (tail.size + 1)
21+
elaborated := elaborated.push $ ← elabFn head
22+
for elt in tail do
23+
elaborated := elaborated.push $ ← elabFn elt
24+
if isArray
25+
then mkArrayLit listEltType elaborated.toList
26+
else mkListLit listEltType elaborated.toList
27+
28+
def elabList (head : α) (tail : Array α) (elabFn : α → TermElabM Expr)
29+
(listEltTypeName : Name) (isArray := false) : TermElabM Expr :=
30+
elabListCore head tail elabFn (mkConst listEltTypeName) isArray
31+
32+
def elabEmptyList (listEltTypeName : Name) : TermElabM Expr :=
33+
mkListLit (mkConst listEltTypeName) []
34+
35+
def elabG (n : TSyntax `num) : TermElabM Expr :=
36+
mkAppM ``Fin.ofNat' #[mkConst ``gSize, mkNatLit n.getNat]
37+
38+
partial def elabPattern : ElabStxCat `pattern
39+
| `(pattern| $v:ident($p:pattern $[, $ps:pattern]*)) => do
40+
let g ← mkAppM ``Global.mk #[toExpr v.getId]
41+
mkAppM ``Pattern.ref #[g, ← elabList p ps elabPattern ``Pattern]
42+
| `(pattern| .$i:ident) => do
43+
let g ← mkAppM ``Global.mk #[toExpr i.getId]
44+
mkAppM ``Pattern.ref #[g, ← elabEmptyList ``Pattern]
45+
| `(pattern| $i:ident) => match i.getId with
46+
| .str .anonymous name => do
47+
mkAppM ``Pattern.var #[← mkAppM ``Local.str #[toExpr name]]
48+
| name@(.str _ _) => do
49+
let g ← mkAppM ``Global.mk #[toExpr name]
50+
mkAppM ``Pattern.ref #[g, ← elabEmptyList ``Pattern]
51+
| _ => throw $ .error i "Illegal pattern name"
52+
| `(pattern| _) => pure $ mkConst ``Pattern.wildcard
53+
| `(pattern| $n:num) => do mkAppM ``Pattern.field #[← elabG n]
54+
| `(pattern| ($p:pattern $[, $ps:pattern]*)) => do
55+
mkAppM ``Pattern.tuple #[← elabList p ps elabPattern ``Pattern true]
56+
| `(pattern| $p₁:pattern | $p₂:pattern) => do
57+
mkAppM ``Pattern.or #[← elabPattern p₁, ← elabPattern p₂]
58+
| stx => throw $ .error stx "Invalid syntax for pattern"
59+
60+
declare_syntax_cat typ
61+
syntax "G" : typ
62+
syntax "(" typ (", " typ)* ")" : typ
63+
syntax "&" typ : typ
64+
syntax ("." noWs)? ident : typ
65+
syntax "fn" "(" ")" " -> " typ : typ
66+
syntax "fn" "(" typ (", " typ)* ")" " -> " typ : typ
67+
68+
partial def elabTyp : ElabStxCat `typ
69+
| `(typ| G) => pure $ mkConst ``Typ.field
70+
| `(typ| ($t:typ $[, $ts:typ]*)) => do
71+
mkAppM ``Typ.tuple #[← elabList t ts elabTyp ``Typ true]
72+
| `(typ| &$t:typ) => do
73+
mkAppM ``Typ.pointer #[← elabTyp t]
74+
| `(typ| $[.]?$i:ident) => do
75+
let g ← mkAppM ``Global.mk #[toExpr i.getId]
76+
mkAppM ``Typ.dataType #[g]
77+
| `(typ| fn() -> $t:typ) => do
78+
mkAppM ``Typ.function #[← elabEmptyList ``Typ, ← elabTyp t]
79+
| `(typ| fn($t$[, $ts:typ]*) -> $t':typ) => do
80+
mkAppM ``Typ.function #[← elabList t ts elabTyp ``Typ, ← elabTyp t']
81+
| stx => throw $ .error stx "Invalid syntax for type"
82+
83+
declare_syntax_cat trm
84+
syntax ("." noWs)? ident : trm
85+
syntax num : trm
86+
syntax "(" trm (", " trm)* ")" : trm
87+
syntax "return " trm : trm
88+
syntax "let " pattern " = " trm "; " trm : trm
89+
syntax "match " trm " { " (pattern " => " trm ", ")+ " }" : trm
90+
syntax ("." noWs)? ident "(" ")" : trm
91+
syntax ("." noWs)? ident "(" trm (", " trm)* ")" : trm
92+
syntax "add" "(" trm ", " trm ")" : trm
93+
syntax "sub" "(" trm ", " trm ")" : trm
94+
syntax "mul" "(" trm ", " trm ")" : trm
95+
syntax "get" "(" trm ", " num ")" : trm
96+
syntax "slice" "(" trm ", " num ", " num ")" : trm
97+
syntax "store" "(" trm ")" : trm
98+
syntax "load" "(" trm ")" : trm
99+
syntax "ptr_val" "(" trm ")" : trm
100+
syntax trm ": " typ : trm
101+
102+
partial def elabTrm : ElabStxCat `trm
103+
| `(trm| .$i:ident) => do
104+
mkAppM ``Term.ref #[← mkAppM ``Global.mk #[toExpr i.getId]]
105+
| `(trm| $i:ident) => match i.getId with
106+
| .str .anonymous name => do
107+
mkAppM ``Term.var #[← mkAppM ``Local.str #[toExpr name]]
108+
| name@(.str _ _) => do
109+
mkAppM ``Term.ref #[← mkAppM ``Global.mk #[toExpr name]]
110+
| _ => throw $ .error i "Illegal name"
111+
| `(trm| $n:num) => do
112+
let data ← mkAppM ``Data.field #[← elabG n]
113+
mkAppM ``Term.data #[data]
114+
| `(trm| ($t:trm $[, $ts:trm]*)) => do
115+
let data ← mkAppM ``Data.tuple #[← elabList t ts elabTrm ``Term true]
116+
mkAppM ``Term.data #[data]
117+
| `(trm| return $t:trm) => do
118+
mkAppM ``Term.ret #[← elabTrm t]
119+
| `(trm| let $p:pattern = $t:trm; $t':trm) => do
120+
mkAppM ``Term.let #[← elabPattern p, ← elabTrm t, ← elabTrm t']
121+
| `(trm| match $t:trm {$[$ps:pattern => $ts:trm,]*}) => do
122+
let mut prods := Array.mkEmpty (ps.size + 1)
123+
for (p, t) in ps.zip ts do
124+
prods := prods.push $ ← mkAppM ``Prod.mk #[← elabPattern p, ← elabTrm t]
125+
let prodType ← mkAppM ``Prod #[mkConst ``Pattern, mkConst ``Term]
126+
mkAppM ``Term.match #[← elabTrm t, ← mkListLit prodType prods.toList]
127+
| `(trm| $[.]?$f:ident ()) => do
128+
let g ← mkAppM ``Global.mk #[toExpr f.getId]
129+
mkAppM ``Term.app #[g, ← elabEmptyList ``Term]
130+
| `(trm| $[.]?$f:ident ($a:trm $[, $as:trm]*)) => do
131+
let g ← mkAppM ``Global.mk #[toExpr f.getId]
132+
mkAppM ``Term.app #[g, ← elabList a as elabTrm ``Term]
133+
| `(trm| add($a:trm, $b:trm)) => do
134+
mkAppM ``Term.add #[← elabTrm a, ← elabTrm b]
135+
| `(trm| sub($a:trm, $b:trm)) => do
136+
mkAppM ``Term.sub #[← elabTrm a, ← elabTrm b]
137+
| `(trm| mul($a:trm, $b:trm)) => do
138+
mkAppM ``Term.mul #[← elabTrm a, ← elabTrm b]
139+
| `(trm| get($a:trm, $i:num)) => do
140+
mkAppM ``Term.get #[← elabTrm a, toExpr i.getNat]
141+
| `(trm| slice($a:trm, $i:num, $j:num)) => do
142+
mkAppM ``Term.slice #[← elabTrm a, toExpr i.getNat, toExpr j.getNat]
143+
| `(trm| store($a:trm)) => do
144+
mkAppM ``Term.store #[← elabTrm a]
145+
| `(trm| load($a:trm)) => do
146+
mkAppM ``Term.load #[← elabTrm a]
147+
| `(trm| ptr_val($a:trm)) => do
148+
mkAppM ``Term.ptrVal #[← elabTrm a]
149+
| `(trm| $v:trm : $t:typ) => do
150+
mkAppM ``Term.ann #[← elabTyp t, ← elabTrm v]
151+
| stx => throw $ .error stx "Invalid syntax for term"
152+
153+
declare_syntax_cat constructor
154+
syntax ident : constructor
155+
syntax ident "(" typ (", " typ)* ")" : constructor
156+
157+
def elabConstructor : ElabStxCat `constructor
158+
| `(constructor| $i:ident) => match i.getId with
159+
| .str .anonymous name => do
160+
mkAppM ``Constructor.mk #[toExpr name, ← elabEmptyList ``Typ]
161+
| _ => throw $ .error i "Illegal constructor name"
162+
| `(constructor| $i:ident($t:typ$[, $ts:typ]*)) => match i.getId with
163+
| .str .anonymous name => do
164+
mkAppM ``Constructor.mk #[toExpr name, ← elabList t ts elabTyp ``Typ]
165+
| _ => throw $ .error i "Illegal constructor name"
166+
| stx => throw $ .error stx "Invalid syntax for constructor"
167+
168+
declare_syntax_cat data_type
169+
syntax "enum " ident : data_type
170+
syntax "enum " ident "{" constructor (", " constructor)* "}" : data_type
171+
172+
def elabDataType : ElabStxCat `data_type
173+
| `(data_type| enum $n:ident) => do
174+
let g ← mkAppM ``Global.mk #[toExpr n.getId]
175+
mkAppM ``DataType.mk #[g, ← elabEmptyList ``Constructor]
176+
| `(data_type| enum $n:ident {$c:constructor $[, $cs:constructor]*}) => do
177+
let g ← mkAppM ``Global.mk #[toExpr n.getId]
178+
mkAppM ``DataType.mk #[g, ← elabList c cs elabConstructor ``Constructor]
179+
| stx => throw $ .error stx "Invalid syntax for data type"
180+
181+
declare_syntax_cat bind
182+
syntax ident ": " typ : bind
183+
184+
def elabBind : ElabStxCat `bind
185+
| `(bind| $i:ident: $t:typ) => match i.getId with
186+
| .str .anonymous name => do
187+
mkAppM ``Prod.mk #[← mkAppM ``Local.str #[toExpr name], ← elabTyp t]
188+
| _ => throw $ .error i "Illegal variable name"
189+
| stx => throw $ .error stx "Invalid syntax for binding"
190+
191+
declare_syntax_cat function
192+
syntax "fn " ident "(" ")" " -> " typ "{" trm "}" : function
193+
syntax "fn " ident "(" bind (", " bind)* ")" " -> " typ "{" trm "}" : function
194+
195+
def elabFunction : ElabStxCat `function
196+
| `(function| fn $i:ident() -> $ty:typ {$t:trm}) => do
197+
let g ← mkAppM ``Global.mk #[toExpr i.getId]
198+
let bindType ← mkAppM ``Prod #[mkConst ``Local, mkConst ``Typ]
199+
mkAppM ``Function.mk #[g, ← mkListLit bindType [], ← elabTyp ty, ← elabTrm t]
200+
| `(function| fn $i:ident($b:bind $[, $bs:bind]*) -> $ty:typ {$t:trm}) => do
201+
let g ← mkAppM ``Global.mk #[toExpr i.getId]
202+
let bindType ← mkAppM ``Prod #[mkConst ``Local, mkConst ``Typ]
203+
mkAppM ``Function.mk
204+
#[g, ← elabListCore b bs elabBind bindType, ← elabTyp ty, ← elabTrm t]
205+
| stx => throw $ .error stx "Invalid syntax for function"
206+
207+
declare_syntax_cat declaration
208+
syntax function : declaration
209+
syntax data_type : declaration
210+
211+
def accElabDeclarations (declarations : (Array Expr × Array Expr))
212+
(stx : TSyntax `declaration) : TermElabM (Array Expr × Array Expr) :=
213+
let (dataTypes, functions) := declarations
214+
match stx with
215+
| `(declaration| $f:function) => do
216+
pure (dataTypes, functions.push $ ← elabFunction f)
217+
| `(declaration| $d:data_type) => do
218+
pure (dataTypes.push $ ← elabDataType d, functions)
219+
| stx => throw $ .error stx "Invalid syntax for declaration"
220+
221+
declare_syntax_cat toplevel
222+
syntax declaration* : toplevel
223+
224+
def elabToplevel : ElabStxCat `toplevel
225+
| `(toplevel| $[$ds:declaration]*) => do
226+
let (dataTypes, functions) ← ds.foldlM (init := default) accElabDeclarations
227+
mkAppM ``Toplevel.mk #[
228+
← mkListLit (mkConst ``DataType) dataTypes.toList,
229+
← mkListLit (mkConst ``Function) functions.toList,
230+
]
231+
| stx => throw $ .error stx "Invalid syntax for toplevel"
232+
233+
elab "⟦" t:toplevel "⟧" : term => elabToplevel t
234+
235+
end Aiur

0 commit comments

Comments
 (0)