Add code generation for extracting annotations

Strata/DDM/AST.lean

@@ -10,7 +10,8 @@ public import Strata.DDM.Util.ByteArray
 public import Strata.DDM.Util.Decimal
 
 import Std.Data.HashMap
-import Strata.DDM.Util.Array
+import all Strata.DDM.Util.Array
+import all Strata.DDM.Util.ByteArray
 
 set_option autoImplicit false
 
@@ -29,7 +30,7 @@ namespace QualifiedIdent
 def fullName (i : QualifiedIdent) : String := s!"{i.dialect}.{i.name}"
 
 instance : ToString QualifiedIdent where
-  toString := private fullName
+  toString := fullName
 
 section
 open _root_.Lean
@@ -554,12 +555,14 @@ structure DebruijnIndex (n : Nat) where
   isLt : val < n
 deriving Repr
 
-
 namespace DebruijnIndex
 
 def toLevel {n} : DebruijnIndex n → Fin n
 | ⟨v, lt⟩ => ⟨n - (v+1), by omega⟩
 
+protected def ofNat {n : Nat} [NeZero n] (a : Nat) : DebruijnIndex n :=
+  ⟨a % n, Nat.mod_lt _ (Nat.pos_of_neZero n)⟩
+
 end DebruijnIndex
 
 /--

Strata/DDM/Elab.lean

@@ -12,6 +12,8 @@ import Strata.DDM.BuiltinDialects
 import Strata.DDM.Util.Ion.Serialize
 import Strata.Util.IO
 
+import all Strata.DDM.Util.ByteArray
+
 open Lean (Message)
 open Strata.Parser (InputContext)
 

Strata/DDM/Elab/Core.lean

@@ -8,8 +8,8 @@ module
 public import Strata.DDM.Elab.DeclM
 public import Strata.DDM.Elab.Tree
 
-import Strata.DDM.Util.Array
-import Strata.DDM.Util.Fin
+import all Strata.DDM.Util.Array
+import all Strata.DDM.Util.Fin
 import Strata.DDM.HNF
 
 open Lean (

Strata/DDM/Elab/DialectM.lean

@@ -9,8 +9,8 @@ public import Strata.DDM.AST
 public import Strata.DDM.Elab.Core
 
 import Std.Data.HashMap
-import Strata.DDM.Util.Array
-import Strata.DDM.Util.Fin
+import all Strata.DDM.Util.Array
+import all Strata.DDM.Util.Fin
 
 set_option autoImplicit false
 

Strata/DDM/Format.lean

@@ -5,14 +5,11 @@
 -/
 module
 
+import Std.Data.HashSet
 public import Strata.DDM.AST
-
 import Strata.DDM.Util.Format
 import Strata.DDM.Util.Nat
-import Strata.DDM.Util.String
-import Std.Data.HashSet
-
-meta import Strata.DDM.AST
+import all Strata.DDM.Util.String
 
 open Std (Format format)
 
@@ -114,7 +111,7 @@ private def fvarName (ctx : FormatContext) (idx : FreeVarIndex) : String :=
   else
     s!"fvar!{idx}"
 
-protected def ofDialects (dialects : DialectMap) (globalContext : GlobalContext) (opts : FormatOptions) : FormatContext where
+protected def ofDialects (dialects : DialectMap) (globalContext : GlobalContext := {}) (opts : FormatOptions := {}) : FormatContext where
   opts := opts
   getFnDecl sym := Id.run do
     let .function f := dialects.decl! sym
@@ -444,13 +441,13 @@ private partial def OperationF.mformatM (op : OperationF α) : FormatM PrecForma
 
 end
 
-instance Expr.instToStrataFormat : ToStrataFormat Expr where
+instance Expr.instToStrataFormat {α} : ToStrataFormat (ExprF α) where
   mformat e c s := private e.mformatM #[] c s |>.fst
 
-instance Arg.instToStrataFormat : ToStrataFormat Arg where
+instance Arg.instToStrataFormat {α} : ToStrataFormat (ArgF α) where
   mformat a c s := private a.mformatM c s |>.fst
 
-instance Operation.instToStrataFormat : ToStrataFormat Operation where
+instance Operation.instToStrataFormat {α} : ToStrataFormat (OperationF α) where
   mformat o c s := private o.mformatM c s |>.fst
 
 namespace MetadataArg

Strata/DDM/HNF.lean

@@ -6,7 +6,7 @@
 
 module
 public import Strata.DDM.AST
-import Strata.DDM.Util.Array
+import all Strata.DDM.Util.Array
 
 public section
 namespace Strata

Strata/DDM/Integration/Lean.lean

@@ -3,6 +3,7 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-import Strata.DDM.Integration.Lean.Gen
-import Strata.DDM.Integration.Lean.HashCommands
+public import Strata.DDM.Integration.Lean.Gen
+public import Strata.DDM.Integration.Lean.HashCommands

Strata/DDM/Integration/Lean/BoolConv.lean

@@ -11,27 +11,28 @@ public section
 namespace Strata
 
 /-- Convert Init.Bool inductive to OperationF -/
-def Bool.toAst {α} [Inhabited α] (v : Ann Bool α) : OperationF α :=
-  if v.val then
-    ⟨v.ann, q`Init.boolTrue, #[]⟩
+def OperationF.ofBool {α} (ann : α) (b : Bool) : OperationF α :=
+  if b then
+    { ann := ann, name := q`Init.boolTrue, args := #[] }
   else
-    ⟨v.ann, q`Init.boolFalse, #[]⟩
+    { ann := ann, name := q`Init.boolFalse, args := #[] }
 
 /-- Convert OperationF to Init.Bool -/
-def Bool.ofAst {α} [Inhabited α] [Repr α] (op : OperationF α) : OfAstM (Ann Bool α) :=
-  match op.name with
-  | q`Init.boolTrue =>
-    if op.args.size = 0 then
-      pure ⟨op.ann, true⟩
-    else
-      .error s!"boolTrue expects 0 arguments, got {op.args.size}"
-  | q`Init.boolFalse =>
-    if op.args.size = 0 then
-      pure ⟨op.ann, false⟩
-    else
-      .error s!"boolFalse expects 0 arguments, got {op.args.size}"
-  | _ =>
-    .error s!"Unknown Bool operator: {op.name}"
+def Bool.ofAst {α} [Inhabited α] [Repr α] (arg : ArgF α) : OfAstM Bool := do
+  match arg with
+  | .op op =>
+    match op.name with
+    | q`Init.boolTrue =>
+      if op.args.size ≠ 0 then
+        .error s!"boolTrue expects 0 arguments, got {op.args.size}"
+      pure true
+    | q`Init.boolFalse =>
+      if op.args.size ≠ 0 then
+        .error s!"boolFalse expects 0 arguments, got {op.args.size}"
+      pure false
+    | _ =>
+      .error s!"Unknown Bool operator: {op.name}"
+  | _ => .throwExpected "boolean" arg
 
 end Strata
 end