• 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
                    • Call-dinfo-fix
                    • Call-dinfo-equiv
                    • Make-call-dinfo
                    • Call-dinfo->scopes
                    • Change-call-dinfo
                    • Call-dinfo->fun
                    • Call-dinfop
                  • 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
                  • 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-environments

Call-dinfo

Fixtype of dynamic information about function calls.

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

Fields
fun — identifier
scopes — vcscope-dinfo-list

Expressions and statements are executed in the context of executing bodies of functions; that is, the expressions and statements are from those bodies. When a function calls another function, its body is executed, and control is returned to the calling function: thus, there is a stack of function calls. The elements of the stack are frames, in compiler terminology.

The dynamic information about a function call consists of the name of the function and a stack (i.e. list) of scopes. The scope at the bottom of the stack is the one for the function body, and the scopes above it correspond to smaller scopes within the body, based on where execution goes within the body.

When a function is executed, only the variables and constants in the scopes for the function can be accessed. Variables and constants in scopes for other function calls are not accessible. This would be the case also for different calls of the same function, if Leo allowed recursion (which it does not currently, but it could in the future).

The call stack is represented as a list of values of this fixtype. The car of the list is the top of the stack, cons is push, and cdr is pop.

Looking at the call stack, the variable and constant scopes are organized in a stack of stacks: the outer stack is the call stack, while the inner stacks are the ones for the function bodies.

Subtopics

Call-dinfo-fix
Fixing function for call-dinfo structures.
Call-dinfo-equiv
Basic equivalence relation for call-dinfo structures.
Make-call-dinfo
Basic constructor macro for call-dinfo structures.
Call-dinfo->scopes
Get the scopes field from a call-dinfo.
Change-call-dinfo
Modifying constructor for call-dinfo structures.
Call-dinfo->fun
Get the fun field from a call-dinfo.
Call-dinfop
Recognizer for call-dinfo structures.