@[reducible, inline]

abbrev Strata.translateLoc : ExprSourceLoc

Location of expressions this file builds itself.

Equations

• Strata.translateLoc = ExprSourceLoc.synthesized "translate"

structure Strata.TransState : Type

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

def Strata.TransM (α : Type) : Type

Equations

• Strata.TransM = StateM Strata.TransState

@[instance_reducible]

instance Strata.instMonadTransM : Monad TransM

Equations

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

def Strata.TransM.run {α : Type} (ictx : Lean.Parser.InputContext) (m : TransM α) (gctx : StrataDDM.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.TransM.recordError {α : Type} (msg : String) (fallback : α) : TransM α

Record a translation error without panicking, then continue with fallback. Use for malformed user input (as opposed to internal invariant violations, which use TransM.error).

Equations

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

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

Equations

• Strata.SourceRange.toMetaData ictx sr = Imperative.MetaData.ofSourceRange (Strata.Uri.file ictx.fileName) sr

def Strata.getOpMetaData (op : StrataDDM.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 : StrataDDM.Arg) : TransM (Imperative.MetaData Core.Expression)

Equations

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

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

Equations

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

def Strata.checkOpArg (arg : StrataDDM.Arg) (name : StrataDDM.QualifiedIdent) (argc : Nat) : TransM (Array StrataDDM.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 : StrataDDM.Arg → TransM α) (arg : StrataDDM.Arg) : TransM (Array α)

Equations

• Strata.translateCommaSep f (StrataDDM.ArgF.seq ann StrataDDM.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 StrataDDM.Arg → TransM α) (arg : StrataDDM.Arg) : TransM α

Equations

• Strata.translateOption f (StrataDDM.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 : StrataDDM.Arg) : TransM Identifier

Equations

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

def Strata.translateOptionLabel? (arg : StrataDDM.Arg) : TransM (Option String)

Translate an optional Core.label argument, returning the user-supplied label name if one was written, or none otherwise.

Equations

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

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

Equations

• Strata.translateOptionLabel default arg = do let __do_lift ← Strata.translateOptionLabel? arg pure (__do_lift.getD default)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Strata.translateMetadataAnnKey (arg : StrataDDM.Arg) : TransM String

Translate a MetadataAnnKey to a string (bare or dialect-prefixed).

Equations

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

def Strata.translateMetadataAnnEntry (arg : StrataDDM.Arg) : TransM (Imperative.MetaDataElem Core.Expression)

Translate a MetadataAnnEntry to a MetaDataElem (flags and string values only; expression values are not yet supported).

Equations

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

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

Translate an Option MetadataAnn argument into MetaData. Returns empty metadata if the annotation is absent.

Equations

• One or more equations did not get rendered due to their size.
• Strata.translateOptMetadataAnn (StrataDDM.ArgF.option ann none) = pure Imperative.MetaData.empty
• Strata.translateOptMetadataAnn (StrataDDM.ArgF.option ann (some annArg)) = Strata.TransM.error (toString "translateOptMetadataAnn expected op " ++ toString (repr annArg))
• Strata.translateOptMetadataAnn arg = Strata.TransM.error (toString "translateOptMetadataAnn unexpected " ++ toString (repr arg))

def Strata.mergeAnnMetaData (md annMd : Imperative.MetaData Core.Expression) : Imperative.MetaData Core.Expression

Merge explicit annotation metadata (annMd) into source-position metadata (md).

getOpMetaData derives a provenance element from the op's DDM source position. There is only ever one provenance, so an explicit @[provenance = …] replaces that derived one instead of being appended and ignored. Other keys stay additive. A future metadata validator can reject bad input like duplicate provenance; for now the last one wins.

Equations

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

def Strata.getMetaDataWithAnn (op : StrataDDM.Operation) (annotsArg : StrataDDM.Arg) : TransM (Imperative.MetaData Core.Expression)

Merge explicit annotation metadata into source-position metadata from an op. Combines getOpMetaData (source positions) with translateOptMetadataAnn (user-supplied annotations).

Equations

• Strata.getMetaDataWithAnn op annotsArg = do let annMd ← Strata.translateOptMetadataAnn annotsArg let md ← Strata.getOpMetaData op pure (Strata.mergeAnnMetaData md annMd)

inductive Strata.GenKind : Type

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

@[instance_reducible]

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_reducible]

instance Strata.instReprGenNum : Repr GenNum

Equations

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

structure Strata.TransBindings : Type

A scoped frame of the translator. :)

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

def Strata.getGenCount (gen_kind : GenKind) (g : GenNum) : Nat

Equations

• Strata.getGenCount Strata.GenKind.var_def g = g.var_def
• Strata.getGenCount Strata.GenKind.axiom_def g = g.axiom_def
• Strata.getGenCount Strata.GenKind.assume_def g = g.assume_def
• Strata.getGenCount Strata.GenKind.assert_def g = g.assert_def
• Strata.getGenCount Strata.GenKind.cover_def g = g.cover_def

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

Equations

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

def Strata.nextLabel (namePrefix : String) (kind : GenKind) (labelArg : StrataDDM.Arg) (bindings : TransBindings) : TransM (String × TransBindings)

Generate a default label and increment the counter for the given kind.

Equations

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

@[instance_reducible]

instance Strata.instToFormatTransBindings : Std.ToFormat TransBindings

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Strata.instInhabitedDecl : Inhabited Core.Decl

Equations

• Strata.instInhabitedDecl = { default := Core.Decl.type (Core.TypeDecl.con { name := "badguy", params := [] }) Imperative.MetaData.empty }

@[instance_reducible]

instance Strata.instInhabitedCheckAttr : Inhabited Core.Procedure.CheckAttr

Equations

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

@[instance_reducible]

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

Equations

• Strata.instInhabitedProdDeclTransBindings = { default := (Core.Decl.type (Core.TypeDecl.con { name := "badguy", params := [] }) Imperative.MetaData.empty, { }) }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

def Strata.translateTypeBinding (bindings : TransBindings) (op : StrataDDM.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 StrataDDM.Arg) : TransM (Array Lambda.TyIdentifier × TransBindings)

Equations

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

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

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

def Strata.translateTypeVar (op : StrataDDM.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 : StrataDDM.Arg) : TransM (Array Lambda.TyIdentifier)

Equations

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

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

Equations

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

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

Equations

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

def Strata.translateBindMk (bindings : TransBindings) (arg : StrataDDM.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 : StrataDDM.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 : StrataDDM.Arg) : TransM (ListMap Core.Expression.Ident Lambda.LTy)

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

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

Equations

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

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

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

partial def Strata.withScopedBindings (p : StrataDDM.Program) (bindings : TransBindings) (xsa bodya : StrataDDM.Arg) : TransM (ListMap Core.Expression.Ident Core.Expression.Ty × TransBindings × Core.Expression.Expr)

Shared binding setup for lambdas and quantifiers: translates the declaration list, creates scoped bound variables, and translates the body in the extended scope.

partial def Strata.translateLambda (p : StrataDDM.Program) (bindings : TransBindings) (xsa bodya : StrataDDM.Arg) : TransM Core.Expression.Expr

partial def Strata.translateHave (p : StrataDDM.Program) (bindings : TransBindings) (xsa vala bodya : StrataDDM.Arg) : TransM Core.Expression.Expr

Translate a have x : T = value in body binding. body is translated with x in scope (reusing withScopedBindings, as lambda does); value is translated in the outer scope. Desugars to (λ x : T. body) value via LExpr.mkHave.

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

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

partial def Strata.translateTriggers (p : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.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 : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM Core.Expression.Expr

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

def Strata.translateInvariant (p : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (List (String × 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 : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (List (String × Core.Expression.Expr))

def Strata.translateMeasure (p : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.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) (annotsArg : StrataDDM.Arg) (decls : Array StrataDDM.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 : StrataDDM.Program) (bindings : TransBindings) (annotsArg : StrataDDM.Arg) (args : Array StrataDDM.Arg) (md : Imperative.MetaData Core.Expression) : TransM (List Core.Statement × TransBindings)

Equations

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

partial def Strata.translateLhsParts (p : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (Core.CoreIdent × List Core.Expression.Expr)

Decompose an LHS into a base identifier and a (reversed) list of index expressions. For m[k1][k2], returns (m, [k2, k1]).

def Strata.translateFnPreconds (p : StrataDDM.Program) (name : Core.CoreIdent) (bindings : TransBindings) (arg : StrataDDM.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))

def Strata.translateLabeledCheck (p : StrataDDM.Program) (bindings : TransBindings) (op : StrataDDM.Operation) (namePrefix : String) (kind : GenKind) (annotsArg la ca : StrataDDM.Arg) (mk : String → Core.Expression.Expr → Imperative.MetaData Core.Expression → Core.Statement) (promoteLabelToSummary : Bool := false) : TransM (List Core.Statement × TransBindings)

Translate an assert/cover/assume statement with optional metadata annotations.

Equations

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

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

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

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

inductive Strata.BindingKind : Type

• input : BindingKind
• out : BindingKind
• inout : BindingKind
• cases : BindingKind

@[instance_reducible]

instance Strata.instDecidableEqBindingKind : DecidableEq BindingKind

Equations

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

@[instance_reducible]

instance Strata.instReprBindingKind : Repr BindingKind

Equations

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

def Strata.instReprBindingKind.repr : BindingKind → Nat → Std.Format

Equations

• Strata.instReprBindingKind.repr Strata.BindingKind.input prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.BindingKind.input")).group prec✝
• Strata.instReprBindingKind.repr Strata.BindingKind.out prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.BindingKind.out")).group prec✝
• Strata.instReprBindingKind.repr Strata.BindingKind.inout prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.BindingKind.inout")).group prec✝
• Strata.instReprBindingKind.repr Strata.BindingKind.cases prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.BindingKind.cases")).group prec✝

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

Equations

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

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

Equations

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

def Strata.translateBindings (bindings : TransBindings) (op : StrataDDM.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 : StrataDDM.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.translateOptionFree (arg : StrataDDM.Arg) : TransM Core.Procedure.CheckAttr

Equations

• Strata.translateOptionFree (StrataDDM.ArgF.option ann (some f)) = do let _ ← Strata.checkOpArg f { dialect := "Core", name := "free" } 0 pure Core.Procedure.CheckAttr.Free
• Strata.translateOptionFree (StrataDDM.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 : StrataDDM.Program) (name : Core.CoreIdent) (count : Nat) (bindings : TransBindings) (arg : StrataDDM.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 : StrataDDM.Program) (name : Core.CoreIdent) (count : Nat) (bindings : TransBindings) (arg : StrataDDM.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 : StrataDDM.Program) (name : Core.CoreIdent) (count : Nat) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (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 : StrataDDM.Program) (name : Core.CoreIdent) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (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.translateProcBindings (bindings : TransBindings) (bop : StrataDDM.Arg) : TransM (ListMap Core.CoreIdent Lambda.LMonoTy × ListMap Core.CoreIdent Lambda.LMonoTy × TransBindings)

Translate a procedure's parameter bindings (the mkBindings arg bop) and push the body's variable scope.

Returns the partitioned input/output signatures for the header, together with bindings extended by the parameter scope. The declaration-order invariant lives here: the body's de Bruijn indices are assigned against the original textual order, not the input/output partition, so the scope binds every parameter in declaration order.

Equations

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

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

Equations

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

def Strata.translateBlockCommand (p : StrataDDM.Program) (bindings : TransBindings) (op : StrataDDM.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.translateTransfer (p : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (List Core.Command × Imperative.DetTransferCmd String Core.Expression × TransBindings)

Equations

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

def Strata.translateCFGBlock (p : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (String × Imperative.BasicBlock (Imperative.DetTransferCmd String Core.Expression) Core.Command × TransBindings)

Translate a single CFG block

Equations

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

partial def Strata.translateCFGBlocks (p : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (List (String × Imperative.BasicBlock (Imperative.DetTransferCmd String Core.Expression) Core.Command) × TransBindings)

Translate a list of CFG blocks

def Strata.translateCFGBody (p : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.Arg) : TransM (Imperative.CFG String (Imperative.DetBlock String Core.Command Core.Expression) × TransBindings)

Translate a CFG body

Equations

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

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

Translate a procedure with CFG body

Equations

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

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

Equations

• Strata.translateOptionInline (StrataDDM.ArgF.option ann (some f)) = do let _ ← Strata.checkOpArg f { dialect := "Core", name := "inline" } 0 pure #[Strata.DL.Util.FuncAttr.inline]
• Strata.translateOptionInline (StrataDDM.ArgF.option ann none) = pure #[]
• Strata.translateOptionInline arg = Strata.TransM.error (toString "translateOptionInline unexpected " ++ toString (repr arg))

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

Translate const x : T;, a constant whose value is left unspecified.

It elaborates to a nullary function without a body, so x is constrained only by whatever axioms mention it.

Equations

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

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

Translate const x : T := v;, a constant declared together with its value.

It elaborates to a nullary function whose body is v, so the value is available to the type checker and to symbolic evaluation without an SMT-level axiom relating x to v. As for a function definition, the body is substituted at each use only when the declaration is marked inline.

Like const x : T;, this form takes no type arguments: a constant is monomorphic. Write a polymorphic nullary value with function syntax instead.

Equations

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

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

Equations

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

def Strata.translateOptionDeclLabel? (arg : StrataDDM.Arg) : TransM (Option String)

Translate an optional DeclLabel, the name in front of a parameter list.

Equations

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

def Strata.translateParamsProposition (p : StrataDDM.Program) (bindings : TransBindings) (namePrefix : String) (args : Array StrataDDM.Arg) : TransM (String × Core.Expression.Expr × TransBindings)

Translate the name and proposition of axiom or lemma written with a parameter list, [name] (x : T, ...) { triggers }: e, into the name and forall x : T, ... :: { triggers } e. args holds the label, the parameter list, the triggers and the proposition, in that order.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Strata.translateDistinct (p : StrataDDM.Program) (bindings : TransBindings) (op : StrataDDM.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_reducible]

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.translateFunction (status : FnInterp) (p : StrataDDM.Program) (bindings : TransBindings) (op : StrataDDM.Operation) : TransM (Core.Decl × TransBindings)

Equations

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

def Strata.translateRecFnDecl (p : StrataDDM.Program) (preBindings : TransBindings) (fnOp : StrataDDM.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 : StrataDDM.Program) (bindings : TransBindings) (op : StrataDDM.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_reducible]

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 : StrataDDM.Program) (bindings : TransBindings) (arg : StrataDDM.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 : StrataDDM.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 : StrataDDM.Program) (bindings : TransBindings) (op : StrataDDM.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.translateCoreDecls (p : StrataDDM.Program) (bindings : TransBindings) : TransM Core.Decls

Equations

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

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

Equations

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