Skip to content

Commit 652fff1

Browse files
kustoszkustosz
committed
clean
1 parent 1fd55b7 commit 652fff1

14 files changed

Lines changed: 58 additions & 93 deletions

File tree

‎Freigen.lean‎

Lines changed: 43 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,45 @@
1-
-- This module serves as the root of the `Freigen` library.
21
import Freigen.Free
3-
import Freigen.ITree
4-
import Freigen.Ast
5-
import Freigen.Reflect
2+
import Freigen.ITree.Effect
3+
import Freigen.ITree.Basic
4+
import Freigen.ITree.Eutt
5+
import Freigen.Ast.Tp
6+
import Freigen.Ast.Basic
7+
import Freigen.Ast.Sexp
8+
import Freigen.Reflect.Sound
9+
import Freigen.Reflect.Basic
10+
import Freigen.Reflect.Recursion
611
import Freigen.Compile
7-
import Freigen.Examples
12+
import Freigen.Examples.Circuit.Basic
13+
import Freigen.Examples.Storage
14+
import Freigen.Examples.Recursion
15+
16+
/-!
17+
# Freigen — the root module
18+
19+
`import Freigen` brings in the whole library. Directories are pure namespaces (mathlib-style:
20+
no per-directory umbrella modules); this file lists every module, and the lakefile's
21+
`.andSubmodules` glob makes CI build any module even if it goes missing from this list.
22+
23+
Module map (details in each module's own docstring; the full story is in the README):
24+
25+
- `Freigen.Free` — the free monad `Free Op SOp` (`pure`/`op`/`hop`) and the generic interpreter
26+
`run`.
27+
- `Freigen.ITree.Basic`/`.Effect`/`.Eutt` — the coinductive denotation domain `Comp Op`
28+
(`ret`/`tau`/`vis`/`fail`), `bind` + its laws, the general-recursion combinator `mrec` (with
29+
`interp` and the call-extended signature `CallOp`), and weak bisimulation `≈` with its
30+
congruence algebra.
31+
- `Freigen.Ast.Tp`/`.Basic`/`.Sexp` — the object-type universe and reified primitives, the dumb
32+
typed AST `Code`/`Prog` with its uniform denotation `denoteProg` into `Comp`, and the
33+
S-expression serialization (**the** printer; grammar pinned in `Ast.Sexp`).
34+
- `Freigen.Reflect.Sound`/`.Basic`/`.Recursion` — `reflect%` compiles a `Free` program (a value,
35+
a function of its inputs, or a structural recursion) into a `Prog` bundled with its
36+
`≈`-soundness against `ofFree`: per-node congruence lemmas, the mode-parametric walk, and the
37+
recursion arm with the `reflect%`/`reflect_def` elaborators.
38+
- `Freigen.Compile` — the `DSL` class, `serialize`, and the `#compile prog => "path"` command
39+
behind the `lake build <lib>:prog` facet.
40+
- `Freigen.Examples.Circuit.Basic`/`.Storage`/`.Recursion` — the Lean-side unit-test suite
41+
(`CircOp` + scoped `hint`, the hint-less `StoreOp`, and `rec_` programs), each example pinning
42+
its runtime result, soundness statement, and serialized AST with `#guard_msgs`. The end-to-end
43+
path — `#compile` → `.prog` artifact → parsed and executed by the Rust SDK — is exercised by
44+
the separate goldens project (`examples/client/`) on CI.
45+
-/

‎Freigen/Ast.lean‎

Lines changed: 0 additions & 13 deletions
This file was deleted.

‎Freigen/Ast/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
import Freigen.Free
22
import Freigen.Ast.Tp
3-
import Freigen.ITree
3+
import Freigen.ITree.Basic
44

55
/-!
66
# The AST: syntax and denotation

‎Freigen/AxCheck.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import Freigen.Examples.Circuit
1+
import Freigen.Examples.Circuit.Basic
22
import Freigen.Examples.Storage
33
import Freigen.Examples.Recursion
44

‎Freigen/Compile.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
import Freigen.Ast
2-
import Freigen.Reflect
1+
import Freigen.Ast.Sexp
2+
import Freigen.Reflect.Recursion
33
import Lean.Elab.Command
44
import Lean.Elab.SyntheticMVars
55

‎Freigen/Examples.lean‎

Lines changed: 0 additions & 24 deletions
This file was deleted.

‎Freigen/Examples/Circuit.lean‎

Lines changed: 0 additions & 13 deletions
This file was deleted.

‎Freigen/Examples/Circuit/Basic.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import Freigen.Free
2-
import Freigen.Reflect
2+
import Freigen.Reflect.Recursion
33
import Freigen.Compile
44

55
/-!
@@ -14,6 +14,10 @@ predicate transformer, blocks erased to fresh existentials). `reflect%` compile
1414
Every example is reflected with `reflect_def C := src` (named `C` / `C_sound`), and pins its
1515
`runCirc` result, its **soundness statement** (`#check C_sound`), and its serialized AST via
1616
`#guard_msgs`, so the comments can't drift from what the code actually produces.
17+
18+
A *real* circuit built on this DSL — the Poseidon hash over BN254 `Fr` — lives in the downstream
19+
goldens project (`examples/client/Client/Poseidon.lean`), where it doubles as the `#compile`
20+
golden test.
1721
-/
1822

1923
namespace Freigen

‎Freigen/Examples/Recursion.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import Freigen.Reflect
1+
import Freigen.Reflect.Recursion
22
import Freigen.Free
33
import Freigen.Compile
44
import Freigen.Examples.Circuit.Basic

‎Freigen/Examples/Storage.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import Freigen.Free
2-
import Freigen.Reflect
2+
import Freigen.Reflect.Recursion
33
import Freigen.Compile
44

55
/-!

0 commit comments

Comments
 (0)