Datatype Support for DDM

This module provides datatype-related types and functions for the DDM, including function templates and name pattern expansion. This module is imported by Strata.DDM.AST and its types are re-exported there. Most users should import Strata.DDM.AST rather than this module directly.

Function Template System

Function templates specify patterns for generating auxiliary functions from datatype declarations. Each template has:

• An iteration scope (perConstructor or perField)
• A name pattern for generating function names
• Parameter and return type specifications

Function Template Types

inductive StrataDDM.FunctionIterScope : Type

Iteration scope for function template expansion.

• perConstructor : FunctionIterScope

  One function per constructor

• perField : FunctionIterScope

  One function per field (across all constructors)

def StrataDDM.instBEqFunctionIterScope.beq : FunctionIterScope → FunctionIterScope → Bool

Equations

• StrataDDM.instBEqFunctionIterScope.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance StrataDDM.instBEqFunctionIterScope : BEq FunctionIterScope

Equations

• StrataDDM.instBEqFunctionIterScope = { beq := StrataDDM.instBEqFunctionIterScope.beq }

def StrataDDM.instReprFunctionIterScope.repr : FunctionIterScope → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprFunctionIterScope : Repr FunctionIterScope

Equations

• StrataDDM.instReprFunctionIterScope = { reprPrec := StrataDDM.instReprFunctionIterScope.repr }

@[implicit_reducible]

instance StrataDDM.instDecidableEqFunctionIterScope : DecidableEq FunctionIterScope

Equations

• StrataDDM.instDecidableEqFunctionIterScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instInhabitedFunctionIterScope : Inhabited FunctionIterScope

Equations

• StrataDDM.instInhabitedFunctionIterScope = { default := StrataDDM.instInhabitedFunctionIterScope.default }

def StrataDDM.instInhabitedFunctionIterScope.default : FunctionIterScope

Equations

• StrataDDM.instInhabitedFunctionIterScope.default = StrataDDM.FunctionIterScope.perConstructor

inductive StrataDDM.TypeRef : Type

Type reference in a function specification, used to specify parameter and return types in function templates.

• datatype : TypeRef

  The datatype being declared

• fieldType : TypeRef

  The type of the current field

• builtin (name : String) : TypeRef

  A built-in type like "bool", "int"

def StrataDDM.instBEqTypeRef.beq : TypeRef → TypeRef → Bool

Equations

• StrataDDM.instBEqTypeRef.beq StrataDDM.TypeRef.datatype StrataDDM.TypeRef.datatype = true
• StrataDDM.instBEqTypeRef.beq StrataDDM.TypeRef.fieldType StrataDDM.TypeRef.fieldType = true
• StrataDDM.instBEqTypeRef.beq (StrataDDM.TypeRef.builtin a) (StrataDDM.TypeRef.builtin b) = (a == b)
• StrataDDM.instBEqTypeRef.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqTypeRef : BEq TypeRef

Equations

• StrataDDM.instBEqTypeRef = { beq := StrataDDM.instBEqTypeRef.beq }

def StrataDDM.instReprTypeRef.repr : TypeRef → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.instReprTypeRef.repr StrataDDM.TypeRef.datatype prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StrataDDM.TypeRef.datatype")).group prec✝
• StrataDDM.instReprTypeRef.repr StrataDDM.TypeRef.fieldType prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StrataDDM.TypeRef.fieldType")).group prec✝

@[implicit_reducible]

instance StrataDDM.instReprTypeRef : Repr TypeRef

Equations

• StrataDDM.instReprTypeRef = { reprPrec := StrataDDM.instReprTypeRef.repr }

def StrataDDM.instDecidableEqTypeRef.decEq (x✝ x✝¹ : TypeRef) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqTypeRef.decEq StrataDDM.TypeRef.datatype StrataDDM.TypeRef.datatype = isTrue ⋯
• StrataDDM.instDecidableEqTypeRef.decEq StrataDDM.TypeRef.datatype StrataDDM.TypeRef.fieldType = isFalse StrataDDM.instDecidableEqTypeRef.decEq._proof_1✝
• StrataDDM.instDecidableEqTypeRef.decEq StrataDDM.TypeRef.datatype (StrataDDM.TypeRef.builtin name) = isFalse ⋯
• StrataDDM.instDecidableEqTypeRef.decEq StrataDDM.TypeRef.fieldType StrataDDM.TypeRef.datatype = isFalse StrataDDM.instDecidableEqTypeRef.decEq._proof_3✝
• StrataDDM.instDecidableEqTypeRef.decEq StrataDDM.TypeRef.fieldType StrataDDM.TypeRef.fieldType = isTrue ⋯
• StrataDDM.instDecidableEqTypeRef.decEq StrataDDM.TypeRef.fieldType (StrataDDM.TypeRef.builtin name) = isFalse ⋯
• StrataDDM.instDecidableEqTypeRef.decEq (StrataDDM.TypeRef.builtin name) StrataDDM.TypeRef.datatype = isFalse ⋯
• StrataDDM.instDecidableEqTypeRef.decEq (StrataDDM.TypeRef.builtin name) StrataDDM.TypeRef.fieldType = isFalse ⋯
• StrataDDM.instDecidableEqTypeRef.decEq (StrataDDM.TypeRef.builtin a) (StrataDDM.TypeRef.builtin b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqTypeRef : DecidableEq TypeRef

Equations

• StrataDDM.instDecidableEqTypeRef = StrataDDM.instDecidableEqTypeRef.decEq

@[implicit_reducible]

instance StrataDDM.instInhabitedTypeRef : Inhabited TypeRef

Equations

• StrataDDM.instInhabitedTypeRef = { default := StrataDDM.instInhabitedTypeRef.default }

def StrataDDM.instInhabitedTypeRef.default : TypeRef

Equations

• StrataDDM.instInhabitedTypeRef.default = StrataDDM.TypeRef.datatype

inductive StrataDDM.NamePatternPart : Type

A part of a name pattern - either a literal string or a placeholder.

• literal (s : String) : NamePatternPart

  A literal string to include verbatim in the generated name

• datatype : NamePatternPart

  Placeholder for the datatype name

• constructor : NamePatternPart

  Placeholder for the constructor name

• field : NamePatternPart

  Placeholder for the field name

def StrataDDM.instBEqNamePatternPart.beq : NamePatternPart → NamePatternPart → Bool

Equations

• StrataDDM.instBEqNamePatternPart.beq (StrataDDM.NamePatternPart.literal a) (StrataDDM.NamePatternPart.literal b) = (a == b)
• StrataDDM.instBEqNamePatternPart.beq StrataDDM.NamePatternPart.datatype StrataDDM.NamePatternPart.datatype = true
• StrataDDM.instBEqNamePatternPart.beq StrataDDM.NamePatternPart.constructor StrataDDM.NamePatternPart.constructor = true
• StrataDDM.instBEqNamePatternPart.beq StrataDDM.NamePatternPart.field StrataDDM.NamePatternPart.field = true
• StrataDDM.instBEqNamePatternPart.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqNamePatternPart : BEq NamePatternPart

Equations

• StrataDDM.instBEqNamePatternPart = { beq := StrataDDM.instBEqNamePatternPart.beq }

@[implicit_reducible]

instance StrataDDM.instReprNamePatternPart : Repr NamePatternPart

Equations

• StrataDDM.instReprNamePatternPart = { reprPrec := StrataDDM.instReprNamePatternPart.repr }

def StrataDDM.instReprNamePatternPart.repr : NamePatternPart → Nat → Std.Format

Equations

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

def StrataDDM.instDecidableEqNamePatternPart.decEq (x✝ x✝¹ : NamePatternPart) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqNamePatternPart.decEq (StrataDDM.NamePatternPart.literal a) (StrataDDM.NamePatternPart.literal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq (StrataDDM.NamePatternPart.literal s) StrataDDM.NamePatternPart.datatype = isFalse ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq (StrataDDM.NamePatternPart.literal s) StrataDDM.NamePatternPart.constructor = isFalse ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq (StrataDDM.NamePatternPart.literal s) StrataDDM.NamePatternPart.field = isFalse ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.datatype (StrataDDM.NamePatternPart.literal s) = isFalse ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.datatype StrataDDM.NamePatternPart.datatype = isTrue ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.datatype StrataDDM.NamePatternPart.constructor = isFalse StrataDDM.instDecidableEqNamePatternPart.decEq._proof_7✝
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.datatype StrataDDM.NamePatternPart.field = isFalse StrataDDM.instDecidableEqNamePatternPart.decEq._proof_8✝
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.constructor (StrataDDM.NamePatternPart.literal s) = isFalse ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.constructor StrataDDM.NamePatternPart.datatype = isFalse StrataDDM.instDecidableEqNamePatternPart.decEq._proof_10✝
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.constructor StrataDDM.NamePatternPart.constructor = isTrue ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.constructor StrataDDM.NamePatternPart.field = isFalse StrataDDM.instDecidableEqNamePatternPart.decEq._proof_11✝
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.field (StrataDDM.NamePatternPart.literal s) = isFalse ⋯
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.field StrataDDM.NamePatternPart.datatype = isFalse StrataDDM.instDecidableEqNamePatternPart.decEq._proof_13✝
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.field StrataDDM.NamePatternPart.constructor = isFalse StrataDDM.instDecidableEqNamePatternPart.decEq._proof_14✝
• StrataDDM.instDecidableEqNamePatternPart.decEq StrataDDM.NamePatternPart.field StrataDDM.NamePatternPart.field = isTrue ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqNamePatternPart : DecidableEq NamePatternPart

Equations

• StrataDDM.instDecidableEqNamePatternPart = StrataDDM.instDecidableEqNamePatternPart.decEq

@[implicit_reducible]

instance StrataDDM.instInhabitedNamePatternPart : Inhabited NamePatternPart

Equations

• StrataDDM.instInhabitedNamePatternPart = { default := StrataDDM.instInhabitedNamePatternPart.default }

def StrataDDM.instInhabitedNamePatternPart.default : NamePatternPart

Equations

• StrataDDM.instInhabitedNamePatternPart.default = StrataDDM.NamePatternPart.literal default

structure StrataDDM.FunctionTemplate : Type

A function template specification. Describes how to generate additional functions based on datatype structure.

• scope : FunctionIterScope

  Iteration scope

• namePattern : Array NamePatternPart

  Name pattern as structured parts

• paramTypes : Array TypeRef

  Parameter types (list of type references)

• returnType : TypeRef

  Return type reference

def StrataDDM.instBEqFunctionTemplate.beq : FunctionTemplate → FunctionTemplate → Bool

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.instBEqFunctionTemplate.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqFunctionTemplate : BEq FunctionTemplate

Equations

• StrataDDM.instBEqFunctionTemplate = { beq := StrataDDM.instBEqFunctionTemplate.beq }

@[implicit_reducible]

instance StrataDDM.instReprFunctionTemplate : Repr FunctionTemplate

Equations

• StrataDDM.instReprFunctionTemplate = { reprPrec := StrataDDM.instReprFunctionTemplate.repr }

def StrataDDM.instReprFunctionTemplate.repr : FunctionTemplate → Nat → Std.Format

Equations

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

def StrataDDM.instDecidableEqFunctionTemplate.decEq (x✝ x✝¹ : FunctionTemplate) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance StrataDDM.instDecidableEqFunctionTemplate : DecidableEq FunctionTemplate

Equations

• StrataDDM.instDecidableEqFunctionTemplate = StrataDDM.instDecidableEqFunctionTemplate.decEq

def StrataDDM.instInhabitedFunctionTemplate.default : FunctionTemplate

Equations

• StrataDDM.instInhabitedFunctionTemplate.default = { scope := default, namePattern := default, paramTypes := default, returnType := default }

@[implicit_reducible]

instance StrataDDM.instInhabitedFunctionTemplate : Inhabited FunctionTemplate

Equations

• StrataDDM.instInhabitedFunctionTemplate = { default := StrataDDM.instInhabitedFunctionTemplate.default }

Name Pattern Functions

def StrataDDM.expandNamePattern (pattern : Array NamePatternPart) (datatypeName : String) (constructorName fieldName : Option String := none) : String

Expand a name pattern with concrete values. Each part is expanded based on its type:

• literal s → the literal string s
• datatype → the datatype name
• constructor → the constructor name (or empty string if not provided)
• field → the field name (or empty string if not provided)

Equations

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

def StrataDDM.validateNamePattern (pattern : Array NamePatternPart) (scope : FunctionIterScope) : Option String

Validate a name pattern for scope compatibility. Returns none if valid, or some errorMessage if invalid.

• perConstructor scope cannot use .field placeholder
• perField scope cannot use .constructor placeholder

Equations

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