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)

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

instance Strata.instReprGenNum : Repr GenNum

Equations

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

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

Equations

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

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)

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.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

def Strata.resolveRecFunc (funcs : List Core.Function) (idx : Nat) : TransM Core.Function

Resolve a function from a recFuncBlock by its global-context index.

Equations

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

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 (List Core.Expression.Expr)

Equations

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

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

def Strata.translateMeasure (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.translateMeasure p bindings arg = pure none

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

Equations

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

def Strata.translateVarStatement (bindings : TransBindings) (decls : Array Arg) (md : Imperative.MetaData Core.Expression) : 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) (md : Imperative.MetaData Core.Expression) : TransM (List Core.Statement × TransBindings)

Equations

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

def Strata.translateOptionReachCheck (arg : Arg) : TransM Bool

Equations

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

def Strata.translateFnPreconds (p : Program) (name : Core.CoreIdent) (bindings : TransBindings) (arg : Arg) : TransM (List (DL.Util.FuncPrecondition Core.Expression.Expr Core.Expression.ExprMetadata))

Equations

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

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 × Bool)

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 × Bool))

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.translateBindingsWithCases (bindings : TransBindings) (op : Arg) : TransM (ListMap Core.CoreIdent Lambda.LMonoTy × Option Nat)

Like translateBindings but also returns the index of the @[cases] parameter, if any.

Equations

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

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

Equations

• Strata.translateModifies arg = do let args ← Strata.checkOpArg arg { dialect := "Core", name := "modifies_spec" } 1 Strata.translateCommaSep (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.

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

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✝

instance Strata.instReprFnInterp : Repr FnInterp

Equations

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

def Strata.translateOptionInline (arg : Arg) : TransM (Array DL.Util.FuncAttr)

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.

def Strata.translateRecFnDecl (p : Program) (preBindings : TransBindings) (fnOp : Operation) (siblingExprs : Array Core.Expression.Expr) : TransM Core.Function

Translate a single function within a mutual recursive block. fnOp is a recfn_decl operation. preBindings has placeholder fvars for all functions in the block. siblingExprs contains the opExpr for each preceding sibling (for bvar resolution).

Equations

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

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

Translate a command_recfndefs block (one or more mutually recursive functions).

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

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

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 Unit

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 Unit) (funcDecls : List Core.Decl) : 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 Unit)

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 Unit)) : 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.translateDatatypes (p : Program) (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings)

Translate a datatype block (one or more datatype declarations). The @[preRegisterTypes] metadata on command_datatypes ensures that type names are pre-registered in the DDM GlobalContext before processing.

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

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

Equations

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