lean2js

Lean2Js.Step

source

Imports 2

The small-step semantics, as an abstract machine with explicit continuations #

The small-step semantics of the subset, written as an abstract machine with explicit continuations.

Where the big-step eval only says "what it returns", this one holds the states along the way. Rules where the question is "when is it not evaluated" — short-circuiting, evaluation order — cannot be stated without those intermediate states.

Agreement with eval is proved in StepAgree: given enough steps, the machine answers every call the way eval does.

inductive

Lean2Js.Frame

source
:
Type

A continuation waiting to be evaluated. andK / orK stand on their own because JS's && and || short-circuit; waiting on both sides with binL would always evaluate the right one.

Instances For
    Used by
      instance

      Lean2Js.instInhabitedFrame

      source
      @[instance_reducible]
      :
      Inhabited Frame
      Equations
      Used by
        inductive

        Lean2Js.State

        source
        :
        Type
        Instances For
          Used by
            instance

            Lean2Js.instInhabitedState

            source
            @[instance_reducible]
            :
            Inhabited State
            Equations
            Used by
              def

              Lean2Js.State.fail

              source
              (e : Err) :
              State
              Equations
              Instances For
                Used by
                  def

                  Lean2Js.State.finish

                  source
                  (v : Value) :
                  List Frame → State
                  Equations
                  Instances For
                    Used by
                      def

                      Lean2Js.continueArgs

                      source
                      (build : List Value → State) (done : List Value) (rest : List Core.Expr) (env : Env) (k : List Frame) (frame : List Value → List Core.Expr → Frame) :
                      State

                      Evaluates the argument list left to right, building the constructor or call once nothing is left.

                      Equations
                      Instances For
                        Used by
                          def

                          Lean2Js.continueMap

                          source
                          (binder : String) (body : Core.Expr) (env : Env) (done rest : List Value) (k : List Frame) :
                          State

                          Walks the elements left to right, one lambda body per element. The three combinators differ only in what they carry between elements: the results so far, the elements kept so far, or the accumulator.

                          Equations
                          Instances For
                            Used by
                              def

                              Lean2Js.sortDone

                              source
                              (ps : List (Value × Value)) (k : List Frame) :
                              State
                              Equations
                              Instances For
                                Used by
                                  def

                                  Lean2Js.continueSort

                                  source
                                  (binder : String) (body : Core.Expr) (env : Env) (done : List (Value × Value)) (rest : List Value) (k : List Frame) :
                                  State

                                  The key of each element is worked out on the way past, and the order is settled once, at the end, on the pairs the walk collected.

                                  Equations
                                  Instances For
                                    Used by
                                      def

                                      Lean2Js.continueFilter

                                      source
                                      (binder : String) (body : Core.Expr) (env : Env) (done rest : List Value) (k : List Frame) :
                                      State
                                      Equations
                                      Instances For
                                        Used by
                                          def

                                          Lean2Js.continueFind

                                          source
                                          (binder : String) (body : Core.Expr) (env : Env) (rest : List Value) (k : List Frame) :
                                          State
                                          Equations
                                          Instances For
                                            Used by
                                              def

                                              Lean2Js.continueQuant

                                              source
                                              (op : Core.QuantOp) (binder : String) (body : Core.Expr) (env : Env) (rest : List Value) (k : List Frame) :
                                              State
                                              Equations
                                              Instances For
                                                Used by
                                                  def

                                                  Lean2Js.continueReduce

                                                  source
                                                  (accName elemName : String) (body : Core.Expr) (env : Env) (acc : Value) (rest : List Value) (k : List Frame) :
                                                  State
                                                  Equations
                                                  Instances For
                                                    Used by

                                                      The walk a fold takes #

                                                      A node is walked one declared field at a time. A field that came round is handed back to the machine as a value to walk rather than walked here, so these two recur on the field list and on the element list alone and the descent into the value is a transition — which is what keeps step a structural match.

                                                      def

                                                      Lean2Js.continueFoldFields

                                                      source
                                                      @[irreducible]
                                                      (typeName : String) (tyArgs : List Core.Ty) (alts : List Core.Alt) (env : Env) (ctor : String) (fields done : List (String × Value)) (rest : List Core.Field) (k : List Frame) :
                                                      State
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Used by
                                                          def

                                                          Lean2Js.continueFoldElems

                                                          source
                                                          @[irreducible]
                                                          (typeName : String) (tyArgs : List Core.Ty) (alts : List Core.Alt) (env : Env) (ctor : String) (fields done : List (String × Value)) (name : String) (doneXs restXs : List Value) (rest : List Core.Field) (k : List Frame) :
                                                          State
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Used by
                                                              def

                                                              Lean2Js.beginFold

                                                              source
                                                              (p : Core.Program) (typeName : String) (tyArgs : List Core.Ty) (alts : List Core.Alt) (env : Env) (v : Value) (k : List Frame) :
                                                              State

                                                              Opens one node of the walk: the constructor the value carries decides which fields come round.

                                                              Equations
                                                              Instances For
                                                                Used by
                                                                  def

                                                                  Lean2Js.step

                                                                  source
                                                                  (p : Core.Program) :
                                                                  State → State
                                                                  Equations
                                                                  Instances For
                                                                    Used by
                                                                      def

                                                                      Lean2Js.step.buildCall

                                                                      source
                                                                      (p : Core.Program) (fn : String) (args : List Value) (k : List Frame) :
                                                                      State
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        Used by
                                                                          def

                                                                          Lean2Js.step.buildCtor

                                                                          source
                                                                          (p : Core.Program) (typeName ctorName : String) (args : List Value) (k : List Frame) :
                                                                          State
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            Used by
                                                                              def

                                                                              Lean2Js.step.buildDictGet

                                                                              source
                                                                              (args : List Value) (k : List Frame) :
                                                                              State
                                                                              Equations
                                                                              Instances For
                                                                                Used by
                                                                                  def

                                                                                  Lean2Js.step.buildDictHas

                                                                                  source
                                                                                  (args : List Value) (k : List Frame) :
                                                                                  State
                                                                                  Equations
                                                                                  Instances For
                                                                                    Used by
                                                                                      def

                                                                                      Lean2Js.step.buildDictSet

                                                                                      source
                                                                                      (args : List Value) (k : List Frame) :
                                                                                      State
                                                                                      Equations
                                                                                      Instances For
                                                                                        Used by
                                                                                          def

                                                                                          Lean2Js.step.buildDictDelete

                                                                                          source
                                                                                          (args : List Value) (k : List Frame) :
                                                                                          State
                                                                                          Equations
                                                                                          Instances For
                                                                                            Used by
                                                                                              def

                                                                                              Lean2Js.step.buildArraySlice

                                                                                              source
                                                                                              (args : List Value) (k : List Frame) :
                                                                                              State
                                                                                              Equations
                                                                                              Instances For
                                                                                                Used by
                                                                                                  def

                                                                                                  Lean2Js.step.buildSlice

                                                                                                  source
                                                                                                  (args : List Value) (k : List Frame) :
                                                                                                  State
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    Used by
                                                                                                      def

                                                                                                      Lean2Js.run

                                                                                                      source
                                                                                                      (p : Core.Program) :
                                                                                                      Nat → State → Except Err Value
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        Used by
                                                                                                          def

                                                                                                          Lean2Js.stepCall

                                                                                                          source
                                                                                                          (p : Core.Program) (bound : Nat) (fn : String) (args : List Value) :
                                                                                                          Except Err Value

                                                                                                          Calls one exported function on the abstract machine, letting it take at most bound steps. The type check at the entry is the same as evalCall's.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            Used by