• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
        • Aleovm
        • Leo
          • Grammar
          • Early-version
            • Json2ast
            • Testing
            • Definition
              • Flattening
              • Abstract-syntax
              • Dynamic-semantics
                • Execution
                • Values
                • Dynamic-environments
                  • Call-dinfo
                  • Denv
                  • Update-var/const-dinfo-in-scope-list
                  • Update-var/const-dinfo-in-scope
                  • Var/const-dinfo
                  • Update-var/const-dinfo
                  • Add-var/const-dinfo-to-scope
                  • Add-var/const-dinfo
                  • Var/const-dinfo-option
                  • Get-var/const-dinfo-from-scope-list
                  • Denv-option
                  • Get-var/const-dinfo-from-scope
                  • Vcscope-dinfo-option
                  • Vcscope-dinfo-list-option
                  • Vcscope-dinfo
                  • Screens
                  • Get-var/const-dinfo
                  • Vcscope-dinfo-option-result
                  • Vcscope-dinfo-list-result
                  • Vcscope-dinfo-result
                  • Dynamic-struct-environments
                  • Dynamic-function-environments
                    • Function-dinfo
                      • Function-dinfo-fix
                      • Function-dinfo-equiv
                      • Make-function-dinfo
                      • Function-dinfo->inputs
                      • Function-dinfo->output
                      • Function-dinfo->body
                      • Change-function-dinfo
                      • Function-dinfop
                    • Function-dinfo-option
                    • Add-function-dinfo
                    • Function-denv-option
                    • Get-function-dinfo
                    • Function-denv
                    • Init-function-denv
                  • Denv-result
                  • Init-denv
                  • Vcscope-dinfo-list
                  • Call-dinfo-list
                • Arithmetic-operations
                • Curve-parameterization
                • Shift-operations
                • Errors
                • Value-expressions
                • Locations
                • Input-execution
                • Edwards-bls12-generator
                • Equality-operations
                • Logical-operations
                • Program-execution
                • Ordering-operations
                • Bitwise-operations
                • Literal-evaluation
                • Type-maps-for-struct-components
                • Output-execution
                • Tuple-operations
                • Struct-operations
              • Compilation
              • Static-semantics
              • Concrete-syntax
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Dynamic-function-environments

Function-dinfo

Fixtype of dynamic information for functions.

This is a product type introduced by fty::defprod.

Fields
inputs — funparam-list
output — type
body — statement-list

This captures the information associated to a function in a dynamic environment for functions. The information consists of the inputs of the function (well captured by function parameters in the abstract syntax), the output type of the function, and the body of the function. The name of the function is outside this function information, so that we can define finite maps: see function-denv.

This function information is the same as in function definitions in the abstract syntax (see fundecl).

Subtopics

Function-dinfo-fix
Fixing function for function-dinfo structures.
Function-dinfo-equiv
Basic equivalence relation for function-dinfo structures.
Make-function-dinfo
Basic constructor macro for function-dinfo structures.
Function-dinfo->inputs
Get the inputs field from a function-dinfo.
Function-dinfo->output
Get the output field from a function-dinfo.
Function-dinfo->body
Get the body field from a function-dinfo.
Change-function-dinfo
Modifying constructor for function-dinfo structures.
Function-dinfop
Recognizer for function-dinfo structures.