Add code generation for extracting annotations

Author: joehendrix

Strata/DDM/Format.lean

@@ -111,7 +111,7 @@ 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
@@ -441,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 := e.mformatM #[] c s |>.fst
 
-instance Arg.instToStrataFormat : ToStrataFormat Arg where
+instance Arg.instToStrataFormat : ToStrataFormat (ArgF α) where
   mformat a c s := a.mformatM c s |>.fst
 
-instance Operation.instToStrataFormat : ToStrataFormat Operation where
+instance Operation.instToStrataFormat : ToStrataFormat (OperationF α) where
   mformat o c s := o.mformatM c s |>.fst
 
 namespace MetadataArg

Strata/DDM/Integration/Lean/BoolConv.lean

@@ -8,27 +8,29 @@ import Strata.DDM.Integration.Lean.OfAstM
 
 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