structure Strata.TransState : Type

• inputCtx : Parser.InputContext
• errors : Array String
• globalContext : GlobalContext

def Strata.TransM (α : Type) : Type

Equations

• Strata.TransM = StateM Strata.TransState

instance Strata.instMonadTransM : Monad TransM

Equations

• Strata.instMonadTransM = StateT.instMonad

def Strata.TransM.run {α : Type} (ictx : Parser.InputContext) (m : TransM α) (gctx : GlobalContext := ∅) : α × Array String

Equations

• Strata.TransM.run ictx m gctx = match StateT.run m { inputCtx := ictx, errors := #[], globalContext := gctx } with | (v, s) => (v, s.errors)

instance Strata.instToStringProdProgramArrayString : ToString (Core.Program × Array String)

Equations

• Strata.instToStringProdProgramArrayString = { toString := fun (p : Core.Program × Array String) => toString (Std.format p.fst) ++ "\n" ++ "Errors: " ++ toString p.snd }

def Strata.TransM.error {α : Type} [Inhabited α] (msg : String) : TransM α

Equations

• Strata.TransM.error msg = do fun (s : Strata.TransState) => ((), { inputCtx := s.inputCtx, errors := s.errors.push msg, globalContext := s.globalContext }) pure (panic msg)

def Strata.SourceRange.toMetaData (ictx : Parser.InputContext) (sr : SourceRange) : Imperative.MetaData Core.Expression

Equations

• Strata.SourceRange.toMetaData ictx sr = #[{ fld := Imperative.MetaData.fileRange, value := Imperative.MetaDataElem.Value.fileRange { file := Strata.Uri.file ictx.fileName, range := sr } }]

def Strata.getOpMetaData (op : Operation) : TransM (Imperative.MetaData Core.Expression)

Equations

• Strata.getOpMetaData op = do let __do_lift ← StateT.get pure (Strata.SourceRange.toMetaData __do_lift.inputCtx op.ann)

def Strata.getArgMetaData (arg : Arg) : TransM (Imperative.MetaData Core.Expression)

Equations

• Strata.getArgMetaData arg = do let __do_lift ← StateT.get pure (Strata.SourceRange.toMetaData __do_lift.inputCtx (Strata.ArgF.ann arg))

def Strata.checkOp {α : Type} (op : Operation) (name : QualifiedIdent) (argc : Nat) : TransM (Option α)

Equations

• One or more equations did not get rendered due to their size.

def Strata.checkOpArg (arg : Arg) (name : QualifiedIdent) (argc : Nat) : TransM (Array Arg)

Equations

• One or more equations did not get rendered due to their size.
• Strata.checkOpArg arg name argc = pure (Array.ofFn fun (x : Fin argc) => default)

def Strata.translateCommaSep {α : Type} [Inhabited α] (f : Arg → TransM α) (arg : Arg) : TransM (Array α)

Equations

• Strata.translateCommaSep f (Strata.ArgF.seq ann Strata.SepFormat.comma args) = Array.mapM f args
• Strata.translateCommaSep f arg = Strata.TransM.error (toString "Expected commaSepList: " ++ toString (repr arg))

def Strata.translateOption {α : Type} [Inhabited α] (f : Option Arg → TransM α) (arg : Arg) : TransM α

Equations

• Strata.translateOption f (Strata.ArgF.option ann maybe_arg) = f maybe_arg
• Strata.translateOption f arg = Strata.TransM.error (toString "Expected Option: " ++ toString (repr arg))

def Strata.translateIdent (Identifier : Type) [Coe String Identifier] [Inhabited Identifier] (arg : Arg) : TransM Identifier

Equations

• Strata.translateIdent Identifier (Strata.ArgF.ident ann name) = pure (Coe.coe name)
• Strata.translateIdent Identifier arg = Strata.TransM.error (toString "Expected ident: " ++ toString (repr arg))

def Strata.translateOptionLabel (default : String) (arg : Arg) : TransM String

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateNat (arg : Arg) : TransM Nat

Equations

• Strata.translateNat (Strata.ArgF.num ann n) = pure n
• Strata.translateNat arg = Strata.TransM.error (toString "translateNat expects num lit")

def Strata.translateBitVec (width : Nat) (arg : Arg) : TransM Nat

Equations

• Strata.translateBitVec width (Strata.ArgF.num ann n) = pure (n % 2 ^ width)
• Strata.translateBitVec width arg = Strata.TransM.error (toString "translateBitVec expects num lit")

def Strata.translateStr (arg : Arg) : TransM String

Equations

• Strata.translateStr (Strata.ArgF.strlit ann s) = pure s
• Strata.translateStr arg = Strata.TransM.error (toString "translateStr expects string lit")

def Strata.translateReal (arg : Arg) : TransM Decimal

Equations

• Strata.translateReal (Strata.ArgF.decimal ann d) = pure d
• Strata.translateReal arg = Strata.TransM.error (toString "translateReal expects decimal lit")

inductive Strata.GenKind : Type

• var_def : GenKind
• axiom_def : GenKind
• assume_def : GenKind
• assert_def : GenKind
• cover_def : GenKind

instance Strata.instDecidableEqGenKind : DecidableEq GenKind

Equations

• Strata.instDecidableEqGenKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Strata.GenNum : Type

Counters for assigning default names for various definitions.

• var_def : Nat
• axiom_def : Nat
• assume_def : Nat
• assert_def : Nat
• cover_def : Nat

def Strata.instReprGenNum.repr : GenNum → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Strata.instReprGenNum : Repr GenNum

Equations

• Strata.instReprGenNum = { reprPrec := Strata.instReprGenNum.repr }

structure Strata.TransBindings : Type

• boundTypeVars : Array Lambda.TyIdentifier
• boundVars : Array (Lambda.LExpr Core.CoreLParams.mono)
• freeVars : Array Core.Decl
• gen : GenNum

def Strata.incrNum (gen_kind : GenKind) (b : TransBindings) : TransBindings

Equations

• One or more equations did not get rendered due to their size.

instance Strata.instToFormatTransBindings : Std.ToFormat TransBindings

Equations

• One or more equations did not get rendered due to their size.

instance Strata.instInhabitedProdListStatementTransBindings : Inhabited (List Core.Statement × TransBindings)

Equations

• Strata.instInhabitedProdListStatementTransBindings = { default := ([], { }) }

instance Strata.instInhabitedDecl_1 : Inhabited Core.Decl

Equations

• One or more equations did not get rendered due to their size.

instance Strata.instInhabitedCheckAttr : Inhabited Core.Procedure.CheckAttr

Equations

• Strata.instInhabitedCheckAttr = { default := Core.Procedure.CheckAttr.Default }

instance Strata.instInhabitedProdDeclTransBindings : Inhabited (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

instance Strata.instInhabitedProdDeclsTransBindings : Inhabited (Core.Decls × TransBindings)

Equations

• Strata.instInhabitedProdDeclsTransBindings = { default := ([], { }) }

instance Strata.instInhabitedProdListCoreIdentTransBindings : Inhabited (List Core.CoreIdent × TransBindings)

Equations

• Strata.instInhabitedProdListCoreIdentTransBindings = { default := ([], { }) }

instance Strata.instInhabitedProdListTyIdentifierTransBindings : Inhabited (List Lambda.TyIdentifier × TransBindings)

Equations

• Strata.instInhabitedProdListTyIdentifierTransBindings = { default := ([], { }) }

def Strata.translateTypeBinding (bindings : TransBindings) (op : Arg) : TransM (Lambda.TyIdentifier × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateTypeBindings (bindings : TransBindings) (ops : Array Arg) : TransM (Array Lambda.TyIdentifier × TransBindings)

Equations

• Strata.translateTypeBindings bindings ops = do let __discr ← Strata.translateTypeBindings.go bindings ops.toList match __discr with | (ans, bindings) => pure (ans.toArray, bindings)

def Strata.translateTypeBindings.go (bindings : TransBindings) (ops : List Arg) : TransM (List Lambda.TyIdentifier × TransBindings)

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateTypeBindings.go bindings [] = pure ([], bindings)

partial def Strata.translateLMonoTy (bindings : TransBindings) (arg : Arg) : TransM Lambda.LMonoTy

partial def Strata.translateLMonoTys (bindings : TransBindings) (args : Array Arg) : TransM (Array Lambda.LMonoTy)

def Strata.translateTypeVar (op : Arg) : TransM Lambda.TyIdentifier

Equations

• Strata.translateTypeVar op = do let args ← Strata.checkOpArg op { dialect := "Core", name := "type_var" } 1 Strata.translateIdent Lambda.TyIdentifier args[0]!

def Strata.translateTypeArgs (op : Arg) : TransM (Array Lambda.TyIdentifier)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateTypeSynonym (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateTypeDecl (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateForwardTypeDecl (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Translate a forward type declaration. This creates a placeholder entry that will be replaced when the actual datatype definition is encountered in a mutual block.

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateLhs (arg : Arg) : TransM Core.CoreIdent

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateLhs arg = Strata.TransM.error (toString "translateLhs expected op " ++ toString (repr arg))

def Strata.translateBindMk (bindings : TransBindings) (arg : Arg) : TransM (Core.CoreIdent × List Lambda.TyIdentifier × Lambda.LMonoTy)

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateBindMk bindings arg = Strata.TransM.error (toString "translateBindMk expected op " ++ toString (repr arg))

def Strata.translateMonoBindMk (bindings : TransBindings) (arg : Arg) : TransM (Core.CoreIdent × Lambda.LMonoTy)

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateMonoBindMk bindings arg = Strata.TransM.error (toString "translateMonoBindMk expected op " ++ toString (repr arg))

partial def Strata.translateDeclList (bindings : TransBindings) (arg : Arg) : TransM (ListMap Core.Expression.Ident Lambda.LTy)

partial def Strata.translateMonoDeclList (bindings : TransBindings) (arg : Arg) : TransM (ListMap Core.Expression.Ident Lambda.LMonoTy)

def Strata.translateOptionMonoDeclList (bindings : TransBindings) (arg : Arg) : TransM (ListMap Core.Expression.Ident Lambda.LMonoTy)

Equations

• One or more equations did not get rendered due to their size.

def Strata.dealiasTypeExpr (p : Program) (te : TypeExpr) : TypeExpr

Equations

• One or more equations did not get rendered due to their size.

def Strata.dealiasTypeArg (p : Program) (a : Arg) : Arg

Equations

• Strata.dealiasTypeArg p (Strata.ArgF.type tp) = Strata.ArgF.type (Strata.dealiasTypeExpr p tp)
• Strata.dealiasTypeArg p a = a

def Strata.isArithTy : Lambda.LMonoTy → Bool

Equations

• Strata.isArithTy (Lambda.LMonoTy.tcons "int" []) = true
• Strata.isArithTy (Lambda.LMonoTy.tcons "real" []) = true
• Strata.isArithTy (Lambda.LMonoTy.bitvec size) = true
• Strata.isArithTy x✝ = false

def Strata.translateFn (ty? : Option Lambda.LMonoTy) (q : QualifiedIdent) : TransM Core.Expression.Expr

partial def Strata.translateQuantifier (qk : Lambda.QuantifierKind) (p : Program) (bindings : TransBindings) (xsa : Arg) (triggersa : Option Arg) (bodya : Arg) : TransM Core.Expression.Expr

partial def Strata.translateTriggerGroup (p : Program) (bindings : TransBindings) (arg : Arg) : TransM Core.Expression.Expr

partial def Strata.translateTriggers (p : Program) (bindings : TransBindings) (arg : Arg) : TransM Core.Expression.Expr

partial def Strata.translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : TransM Core.Expression.Expr

partial def Strata.translateExprs (p : Program) (bindings : TransBindings) (args : Array Arg) : TransM (Array Core.Expression.Expr)

def Strata.translateInvariant (p : Program) (bindings : TransBindings) (arg : Arg) : TransM (Option Core.Expression.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateInvariant p bindings arg = pure none

partial def Strata.translateInvariants (p : Program) (bindings : TransBindings) (arg : Arg) : TransM (List Core.Expression.Expr)

def Strata.initVarStmts (tpids : ListMap Core.Expression.Ident Lambda.LTy) (bindings : TransBindings) : TransM (List Core.Statement × TransBindings)

Equations

• One or more equations did not get rendered due to their size.
• Strata.initVarStmts [] bindings = pure ([], bindings)

def Strata.translateVarStatement (bindings : TransBindings) (decls : Array Arg) : TransM (List Core.Statement × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateInitStatement (p : Program) (bindings : TransBindings) (args : Array Arg) : TransM (List Core.Statement × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

partial def Strata.translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) : TransM (List Core.Statement × TransBindings)

partial def Strata.translateBlock (p : Program) (bindings : TransBindings) (arg : Arg) : TransM (List Core.Statement × TransBindings)

partial def Strata.translateElse (p : Program) (bindings : TransBindings) (arg : Arg) : TransM (List Core.Statement × TransBindings)

def Strata.translateInitMkBinding (bindings : TransBindings) (op : Arg) : TransM (Core.CoreIdent × Lambda.LMonoTy)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateInitMkBindings (bindings : TransBindings) (ops : Array Arg) : TransM (Array (Core.CoreIdent × Lambda.LMonoTy))

Equations

• Strata.translateInitMkBindings bindings ops = Array.mapM (fun (op : Strata.Arg) => Strata.translateInitMkBinding bindings op) ops

def Strata.translateBindings (bindings : TransBindings) (op : Arg) : TransM (ListMap Core.CoreIdent Lambda.LMonoTy)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateModifies (arg : Arg) : TransM Core.CoreIdent

Equations

• Strata.translateModifies arg = do let args ← Strata.checkOpArg arg { dialect := "Core", name := "modifies_spec" } 1 Strata.translateIdent Core.CoreIdent args[0]!

def Strata.translateOptionFree (arg : Arg) : TransM Core.Procedure.CheckAttr

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateOptionFree (Strata.ArgF.option ann none) = pure Core.Procedure.CheckAttr.Default
• Strata.translateOptionFree arg = Strata.TransM.error (toString "translateOptionFree unexpected " ++ toString (repr arg))

def Strata.translateRequires (p : Program) (name : Core.CoreIdent) (count : Nat) (bindings : TransBindings) (arg : Arg) : TransM (ListMap Core.CoreLabel Core.Procedure.Check)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateEnsures (p : Program) (name : Core.CoreIdent) (count : Nat) (bindings : TransBindings) (arg : Arg) : TransM (ListMap Core.CoreLabel Core.Procedure.Check)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateSpecElem (p : Program) (name : Core.CoreIdent) (count : Nat) (bindings : TransBindings) (arg : Arg) : TransM (List Core.CoreIdent × ListMap Core.CoreLabel Core.Procedure.Check × ListMap Core.CoreLabel Core.Procedure.Check)

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateSpecElem p name count bindings arg = Strata.TransM.error (toString "translateSpecElem expects an op " ++ toString (repr arg))

def Strata.translateSpec (p : Program) (name : Core.CoreIdent) (bindings : TransBindings) (arg : Arg) : TransM (List Core.CoreIdent × ListMap Core.CoreLabel Core.Procedure.Check × ListMap Core.CoreLabel Core.Procedure.Check)

Equations

• One or more equations did not get rendered due to their size.

partial def Strata.translateSpec.go (p : Program) (name : Core.CoreIdent) (bindings : TransBindings) (count max : Nat) (args : Array Arg) : TransM (List Core.CoreIdent × ListMap Core.CoreLabel Core.Procedure.Check × ListMap Core.CoreLabel Core.Procedure.Check)

def Strata.translateProcedure (p : Program) (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateBlockCommand (p : Program) (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Translate a top-level block command as a nameless parameterless procedure

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateConstant (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateAxiom (p : Program) (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateDistinct (p : Program) (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

inductive Strata.FnInterp : Type

• Definition : FnInterp
• Declaration : FnInterp

instance Strata.instReprFnInterp : Repr FnInterp

Equations

• Strata.instReprFnInterp = { reprPrec := Strata.instReprFnInterp.repr }

def Strata.instReprFnInterp.repr : FnInterp → Nat → Std.Format

Equations

• Strata.instReprFnInterp.repr Strata.FnInterp.Definition prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.FnInterp.Definition")).group prec✝
• Strata.instReprFnInterp.repr Strata.FnInterp.Declaration prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.FnInterp.Declaration")).group prec✝

def Strata.translateOptionInline (arg : Arg) : TransM (Array String)

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateOptionInline (Strata.ArgF.option ann none) = pure #[]
• Strata.translateOptionInline arg = Strata.TransM.error (toString "translateOptionInline unexpected " ++ toString (repr arg))

def Strata.translateFunction (status : FnInterp) (p : Program) (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

structure Strata.TransConstructorInfo : Type

Information about a single constructor extracted during translation. This is the Strata Core-specific version of ConstructorInfo from AST.lean, with types translated from TypeExpr to LMonoTy.

• name : Core.CoreIdent

  Constructor name

• fields : Array (Core.CoreIdent × Lambda.LMonoTy)

  Fields as (fieldName, fieldType) pairs with translated types

instance Strata.instReprTransConstructorInfo : Repr TransConstructorInfo

Equations

• Strata.instReprTransConstructorInfo = { reprPrec := Strata.instReprTransConstructorInfo.repr }

def Strata.instReprTransConstructorInfo.repr : TransConstructorInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateConstructorList (p : Program) (bindings : TransBindings) (arg : Arg) : TransM (Array TransConstructorInfo)

Extract and translate constructor information from a constructor list argument.

Parameters:

• p: The DDM Program (provides dialect map for annotation lookup)
• bindings: Current translation bindings (for type variable resolution)
• arg: The constructor list argument from the parsed datatype command

Equations

• Strata.translateConstructorList p bindings arg = Array.mapM (Strata.translateConstructorInfo✝ bindings) (Strata.GlobalContext.extractConstructorInfo p.dialects arg)

def Strata.translateDatatypeTypeArgs (bindings : TransBindings) (arg : Arg) (errorContext : String) : TransM (List Lambda.TyIdentifier × TransBindings)

Extract type arguments from a datatype's optional bindings argument.

Equations

• One or more equations did not get rendered due to their size.

def Strata.mkPlaceholderLDatatype (name : String) (typeArgs : List Lambda.TyIdentifier) : Lambda.LDatatype Core.Visibility

Create a placeholder LDatatype for recursive type references.

Equations

• One or more equations did not get rendered due to their size.

def Strata.filterDatatypeDecls (ldatatype : Lambda.LDatatype Core.Visibility) (funcDecls : List Core.Decl) : List Core.Decl × List Core.Decl × List Core.Decl

Filter factory function declarations to extract constructor, tester, and field accessor decls for a single datatype.

Equations

• One or more equations did not get rendered due to their size.

def Strata.buildLConstrs (datatypeName : String) (constructors : Array TransConstructorInfo) : List (Lambda.LConstr Core.Visibility)

Build LConstr list from TransConstructorInfo array.

Equations

• One or more equations did not get rendered due to their size.

def Strata.genDatatypeFactory (ldatatypes : List (Lambda.LDatatype Core.Visibility)) : TransM (List Core.Decl)

Generate factory function declarations from a list of LDatatypes.

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateDatatype (p : Program) (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Translate a datatype declaration to Boogie declarations, updating bindings appropriately.

Important: The returned Core.Decls only contains the type declaration itself. Factory functions (constructors, testers, destructors) are generated automatically by Env.addDatatypes during program evaluation to avoid duplicates.

Parameters:

• p: The DDM Program (provides dialect map)
• bindings: Current translation bindings
• op: The command_datatype operation to translate

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Translate a mutual block containing mutually recursive datatype definitions. This collects all datatypes, creates a single TypeDecl.data with all of them, and updates the forward-declared entries in bindings.freeVars.

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateGlobalVar (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Equations

• One or more equations did not get rendered due to their size.

def Strata.translateCoreDecls (p : Program) (bindings : TransBindings) : TransM Core.Decls

Equations

• Strata.translateCoreDecls p bindings = do let __discr ← Strata.translateCoreDecls.go p 0 p.commands.size bindings p.commands match __discr with | (decls, snd) => pure decls

partial def Strata.translateCoreDecls.go (p : Program) (count max : Nat) (bindings : TransBindings) (ops : Array Operation) : TransM (Core.Decls × TransBindings)

def Strata.translateProgram (p : Program) : TransM Core.Program

Equations

• One or more equations did not get rendered due to their size.