www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | LICENSE

envlang.rkt (26525B)


      1 #lang racket
      2 (define-syntax-rule (matches? pat ...) (match-lambda [pat #t] ... [else #f]))
      3 (define ((procedure/arity? a) p) (and (procedure? p) (procedure-arity-includes? p a)))
      4 (define v?       (matches? `(\\ env χ ,_) (? hash?) (? string?) (? number?) `(ffi ,(? (procedure/arity? 3)))))
      5 (define e-not-v? (matches? `(@ ,e-f ,e-env ,e-arg) `(thunk ,e) 'env 'χ (? symbol?)))
      6 
      7 (define (eval debug? env+χ+redex+k-frames)
      8   (when debug? (println (third env+χ+redex+k-frames)))
      9   (define (r debug env+χ+redex+k-frames) (when debug? (displayln debug)) (eval debug? env+χ+redex+k-frames))
     10   (match env+χ+redex+k-frames
     11     [`{,E ,X ,(? v? v) ()}
     12      v]
     13     ;; Primitive application
     14     [           `{,E     ,X                (@ (\\ env χ ,e) ,(? v? v-env) (\\ env χ ,e-arg))                                      ,… }
     15      (r "APP"   `{,v-env (\\ env χ ,e-arg)              ,e                                                                        ,… })]
     16     [           `{,E     ,X                (@ (ffi ,f)      ,(? v? v-env) (\\ env χ ,e-arg))                                      ,… }
     17      (r "FFI"   `{,E     ,X                ,(f r v-env `(\\ env χ ,e-arg))                                                        ,… })]
     18     ;;---------------------------------------------------------------------------------------------------------------------------
     19     ;; Evaluation of sub-parts of an application    
     20     [           `{,E     ,X                (@  ,(? e-not-v? e-f)              ,e-env ,e-arg)                                      ,… }
     21      (r "@-F"   `{,E     ,X                                ,e-f                               ((,E  ,X  (@ _    ,e-env ,e-arg)) . ,…)})]
     22     [           `{,E     ,X                (@  ,(? v? v-f)       ,(? e-not-v? e-env) ,e-arg)                                      ,… }
     23      (r "@-ENV" `{,E     ,X                                                  ,e-env           ((,E  ,X  (@ ,v-f _      ,e-arg)) . ,…)})]
     24     [           `{,E     ,X                (@  ,(? v? v-f) ,(? v? v-env) ,(? e-not-v? e-arg))                                     ,… }
     25      (r "@-ARG" `{,E     ,X                                                          ,e-arg   ((,E  ,X  (@ ,v-f ,v-env _     )) . ,…)})]
     26     
     27     [           `{,E     ,X                   ,(? v? v-f)                                     ((,E′ ,X′ (@ _ ,e-env ,e-arg))    . ,…)}
     28      (r "K-F"   `{,E′    ,X′                     (@ ,v-f ,e-env ,e-arg)                                                           ,… })]
     29     [           `{,E     ,X                        ,(? v? v-env)                              ((,E′ ,X′ (@ ,v-f _   ,e-arg))    . ,…)}
     30      (r "K-ENV" `{,E′    ,X′                     (@ ,v-f ,v-env ,e-arg)                                                           ,… })]
     31     [           `{,E     ,X                               ,(? v? v-arg)                       ((,E′ ,X′ (@ ,v-f ,v-env _  ))    . ,…)}
     32      (r "K-ARG" `{,E′    ,X′                     (@ ,v-f ,v-env ,v-arg)                                                           ,… })]
     33     ;;---------------------------------------------------------------------------------------------------------------------------
     34     ;; Syntactic sugar
     35     ;; insertion of #%app at the front of all parentheses that don't start with an @ or \ or ffi or thunk or #%app
     36     [           `{,E     ,X                (,(and (not '@ '\\ 'ffi 'thunk '#%app) e-f) ,e-arg)                                    ,… }
     37      (r "#%app" `{,E     ,X                (#%app                         ,e-f  ,e-arg)                                           ,… })]
     38     [           `{,E     ,X                (#%app                         ,e-f  ,e-arg)                                           ,… }
     39      (r "@%app" `{,E     ,X                (@ (@ (@ #%get env (\\ env χ "#%app"))
     40                                                  env (\\ env χ ,e-f))
     41                                               env (\\ env χ ,e-arg))                                                              ,… })]
     42     [           `{,E     ,X                (λ ,var-name ,e)                                                                       ,… }
     43      (r "LAM"   `{,E     ,X                (#%app (#%app λ ,var-name) ,e)                                                         ,… })]
     44     [           `{,E     ,X                (thunk ,e)                                                                             ,… }
     45      (r "THUNK" `{,E     ,X                (\\ env χ (@ (\\ env χ ,e) env ,X))                                                    ,… })]
     46     ;;---------------------------------------------------------------------------------------------------------------------------
     47     ;; Built-ins and variables
     48     [           `{,E     ,X                env                                                                                    ,… }
     49      (r "VAR"   `{,E     ,X                ,E                                                                                     ,… })]
     50     [           `{,E     ,X                χ                                                                                      ,… }
     51      (r "VAR"   `{,E     ,X                ,X                                                                                     ,… })]
     52     [           `{,E     ,X                #%get                                                                                  ,… }
     53      (r "VAR"   `{,E     ,X                ,(car (hash-ref E "#%get"))                                                            ,… })]
     54     [           `{,E     ,X                ,(? symbol? var-name)                                                                  ,… }
     55      (r "VAR"   `{,E     ,X                (@ #%get env (\\ env χ ,(symbol->string var-name)))                                    ,… })]
     56     ;;---------------------------------------------------------------------------------------------------------------------------
     57     [other
     58      `(stuck . ,other)]))
     59 
     60 (define unit '(\\ env χ χ))
     61 (define (#%force eval env t)                        (eval "FFI:FORCE" `{,env ,unit (@ ,t ,env ,unit) ()}))
     62 (define (#%get   eval env χ)                        (car (hash-ref env (#%force eval env χ))))
     63 (define (#%push  ev1 env1 χ) `(ffi ,(λ (ev2 env2 v) (hash-update env1 (#%force ev1 env1 χ) (λ (vs) (cons (#%force ev2 env2 v) vs)) '()))))
     64 (define (#%drop  eval env χ)                        (hash-update env (#%force eval env χ) (λ (vs) (cdr vs))))
     65 (define (-#%app  ev1 env1 f) `(ffi ,(λ (ev2 env2 a) `(@ ,(#%force ev1 env1 f) env (\\ env χ ,(#%force ev2 env2 a))))))
     66 (define (#%lam   ev1 env1 a) `(ffi ,(λ (ev2 env2 e)
     67                                       (let ([astr (match ([`(\\ env χ (? symbol? a)) (symbol->string a)]))])
     68                                         `(@ capture
     69                                             env
     70                                             (\ env χ (@ (\ env χ ,e)
     71                                                         (@ (@ #%push env ,astr) env χ)
     72                                                         χ)))))))
     73 (define (#%capture eval E f) `(\ env χ (@ ,f ,E χ)))
     74 (define-syntax-rule (ffis f ...) (make-hash (list (cons (symbol->string 'f) `((ffi ,f))) ...)))
     75 (define initial-env
     76   (let ([#%app -#%app]) (ffis #%force #%get #%push #%drop #%app)))
     77 
     78 
     79 
     80 (define e-or-v? (or? e-not-v? v?))
     81 
     82 
     83 (require rackunit predicates)
     84 (define (ev e [debug? #f]) (eval debug? `(,initial-env (\\ env χ "argv") ,e ())))
     85 
     86 (check-pred v? '(\\ env χ 1))
     87 (check-pred v? '(\\ env χ (\\ env χ 1)))
     88 (check-pred v? #hash())
     89 (check-pred v? initial-env)
     90 (check-pred v? "foo")
     91 (check-pred v? 1)
     92 (check-pred v? `(ffi ,(lambda (eval env χ) 42)))
     93 (check-pred v? `(ffi ,#%get))
     94 (check-pred v? `(ffi ,#%push))
     95 (check-pred v? `(ffi ,#%drop))
     96 (check-pred e-not-v? '(@ (\\ env χ 1) #hash() 2))
     97 (check-pred (not? v?) '(@ (\\ env χ 1) #hash() 2))
     98 (check-pred (not? e-not-v?) '(\\ env χ 1))
     99 (check-pred (not? e-not-v?) '(\\ env χ (\\ env χ 1)))
    100 (check-pred (not? e-not-v?) #hash())
    101 (check-pred (not? e-not-v?) "foo")
    102 (check-pred (not? e-not-v?) 1)
    103 (check-pred (not? e-not-v?) `(ffi ,(lambda (env χ) 42)))
    104 (check-pred e-or-v? '(\\ env χ 1))
    105 (check-pred e-or-v? '(\\ env χ (\\ env χ 1)))
    106 (check-pred e-or-v? #hash())
    107 (check-pred e-or-v? "foo")
    108 (check-pred e-or-v? 1)
    109 (check-pred e-or-v? `(ffi ,(lambda (eval env χ) 42)))
    110 (check-pred e-or-v? '(@ (\\ env χ 1) #hash() 2))
    111 
    112 (check-equal? (ev '(\\ env χ 1)) '(\\ env χ 1))
    113 (check-equal? (ev #hash()) #hash())
    114 (check-equal? (ev "foo") "foo")
    115 (check-equal? (ev 1) 1)
    116 (let ([example-ffi `(ffi ,(lambda (eval env χ) 42))])
    117   (check-equal? (ev example-ffi) example-ffi))
    118 (check-equal? (ev `(ffi ,#%get)) `(ffi ,#%get))
    119 (check-equal? (ev `(ffi ,#%push)) `(ffi ,#%push))
    120 (check-equal? (ev `(ffi ,#%drop)) `(ffi ,#%drop))
    121 (check-equal? (ev '#%get) `(ffi ,#%get))
    122 (check-equal? (ev '#%push) `(ffi ,#%push))
    123 (check-equal? (ev '#%drop) `(ffi ,#%drop))
    124 ;; TODO: test #%get, #%push, pop, FFI
    125 (check-equal? (ev '(@ (\\ env χ 1) #hash() (\\ env χ 2))) 1)
    126 (check-equal? (ev '(@ (\\ env χ 1) env (\\ env χ 2))) 1)
    127 (check-equal? (ev 'env) initial-env)
    128 (check-equal? (ev 'χ) '(\\ env χ "argv"))
    129 (check-equal? (ev '(@ #%force env χ)) '"argv")
    130 (check-equal? (ev '(@ (\\ env χ 1) env (\\ env χ 2))) 1)
    131 (check-equal? (ev '(@ (\\ env χ #%get) env (\\ env χ χ))) `(ffi ,#%get))
    132 (check-equal? (ev '(@ (\\ env χ #%push) env (\\ env χ χ))) `(ffi ,#%push))
    133 (check-equal? (ev '(@ (\\ env χ #%drop) env (\\ env χ χ))) `(ffi ,#%drop))
    134 (check-equal? (ev '(@ #%force env (\\ env χ χ))) unit)
    135 (check-equal? (ev '(@ #%force env (\\ env χ 42))) 42)
    136 (check-equal? (ev '(@ #%force env (\\ env χ (\\ env χ χ)))) '(\\ env χ χ))
    137 (check-equal? (ev '(thunk χ)) '(\\ env χ (@ (\\ env χ χ) env (\\ env χ "argv"))))
    138 (check-equal? (ev '(@ #%force env (thunk (@ #%force env χ)))) "argv")
    139 (check-equal? (ev '(@ #%force env (thunk 3))) 3)
    140 (check-equal? (ev '(#%force 3)) 3)
    141 
    142 
    143 
    144 
    145 #;(
    146 ;; Primitive application
    147 ;; defaults to:
    148  =>            env=[E],    χ=X               (@     e-f env (\ env χ e-arg))                      …
    149 
    150 ;; In particular, the sugared λ is just a function
    151 ;; defaults to:
    152  =>            env=[E],    χ=X               (@ capture
    153                                                 env
    154                                                 (\ env χ (@ (\ env χ e)
    155                                                             (@ (@ #%push env "var-name") env χ)
    156                                                            χ)))
    157 
    158  CAPTURE       env=[E],    χ=X               (@ capture v-env (\ env χ e))                        …
    159  =>            env=[E],    χ=X               (\ env χ (@ (λ env χ e) v-env χ))                    …
    160 
    161  FORCE         env=[E],    χ=(\ env χ e-arg) (@ #%force v-env (\ env χ e))                          …
    162  =>            env=[E],    χ=()              (@ (\ env χ e) v-env dummy)                          …
    163 )
    164 
    165 
    166 
    167 
    168 
    169 
    170 
    171 
    172 
    173 
    174 
    175 
    176 #|
    177 ;; Syntax of the language:
    178 ;;
    179 ;; Plain λ-calculus:
    180 ;; x,y,z ::= variable name   Variable
    181 ;; e ::= (λ x e)             Abstraction (lambda)
    182 ;;    |  (e₁ e₂)             Application
    183 ;;    |  x                   variable reference
    184 ;;
    185 ;; Plain λ-calculus + laziness:
    186 ;; e ::= …
    187 ;;    |  (#%app e₁ e₂)       Sugar application
    188 ;;
    189 ;; Translation to λ-calculus
    190 ;; (#%app e₁ e₂)          => ((e₁ env) (λ _ e₂))
    191 ;;
    192 ;; Plain λ-calculus + continuations:
    193 ;; e ::= (λ k x e)                                             Abstraction (lambda)
    194 ;;    |  (call/prompt stack-frame-name e₁ continuation e₂)     Primitive application
    195 ;;    |  x                                                     variable reference
    196 ;;    |  (#%app e₁ e₂)                                         Sugar application
    197 ;;    |  (#%lam x e)                                           Sugar lambda
    198 ;;
    199 ;; (#%app e₁ e₂)          => (call/cc (λ (k) (call/prompt "stack frame" e₁ k e₂))
    200 
    201 (f e) => (λ kont . (eval-f k=(λ res-f (eval-e k=(λ res-e (res-f res-e k=kont))))))
    202 
    203 
    204 
    205 
    206 
    207 
    208 
    209 
    210 
    211 
    212 
    213 
    214 
    215 
    216 
    217 
    218 
    219 
    220 
    221 
    222 
    223 
    224 ;; translation rules
    225 x       => (λ k . k x)
    226 (λ x e) => (λ k . k (λ (k' x) . [[e]] k' ))
    227 (f arg) => (λ k . k ( [[f]] (λ fval . [[arg]] (λ argval . fval k argval) )))
    228 
    229 eval k x => k x
    230 eval k (λ x e) => can't reduce further
    231 eval k (f arg) => (eval f) then (eval arg) then (eval k (fval argval))
    232 
    233 
    234 ;; Plain λ-calculus + continuations:
    235 ;; e ::= (λ k x e)           Abstraction (lambda)
    236 ;;    |  (e₁ k e₂)           Primitive application
    237 ;;    |  x                   variable reference
    238 ;;    |  (#%app e₁ e₂)       Sugar application is call/cc
    239 
    240 eval ((λ k x e) kont param) => e[x := param, k := kont]
    241 eval (#%app f param) => (call/cc f param) => (f current-continuation param)
    242 
    243 location of expr    current-continuation
    244 (λ k x _)           k
    245 
    246 (_  k e₂)           (λ outer-continuation evaled-f (f k e₂))
    247 (e₁ _ e₂)           ??
    248 (e₁ k  _)           (λ outer-continuation result (e₁ k result))
    249 
    250 
    251 (#%app _ e₂)       Sugar application is call/cc
    252 (#%app e₁ _)       Sugar application is call/cc
    253 
    254 
    255 
    256 
    257 
    258 
    259 
    260 
    261 
    262 
    263 
    264 
    265 
    266 
    267 
    268 
    269 
    270 ;; Plain λ-calculus + continuations:
    271 ;; e ::= (λ k=x₁ x₂ e)       Abstraction (lambda), takes a continuation
    272 ;;    |  (e₁ k=e₂ e₃)        Raw aplication
    273 ;;    |  x                   variable reference
    274 ;;    |  (#%app e₁ e₂)       Sugar application
    275 ;;
    276 ;; Evaluation rules:
    277 ;; eval env ((λ k=x₂ x₃ e₁) k=e₂ e₃) => eval env[x₂↦e₂][x₃↦e₃] e₁
    278 ;; x                                 => env[x]
    279 ;; ((#%app e₁ e₂) k=e' e'') =>
    280 ;; (e' k=(#%app e₁ e₂) e'') =>
    281 ;; (e' k=e'' (#%app e₁ e₂)) => (e₁ k=(λ arg k=? (e' k=e'' arg)) e₂)
    282 ;;
    283 ;; (#%app f (#%app g x))  => (g k=f x)
    284 ;; (f (g (h x)))    => ((g f) (h x)) => (h (g f) x)
    285 
    286 ;; λk.x => k x
    287 ;; λk.λx.e => k (λk λk' (#%app e k))
    288 ;;
    289 ;; Plain lambda-calculus + first-class environments:
    290 ;; "x" ::= "x","y","z"…   String
    291 ;; e ::= (λ env arg e)      Abstraction (lambda) which
    292 ;;                          * an environment (map from strings to values)
    293 ;;                          * takes an argument always named arg which is not added to the env
    294 ;;    |  (e env e)          Application
    295 ;;    |  env                the env of the innermost lambda containing this expression
    296 ;;    |  arg                the arg of the innermost lambda containing this expression
    297 ;; prim ::=
    298 ;;    |  get                Get variable from environment, type is (→ Environment → String Any)
    299 ;;    |  add                Extend environment with new binding, type is (→ Environment String (→ _Environment Any Environment)))
    300 ;;
    301 ;; Translation to plain lambda-calculus:
    302 ;; (λ env arg e)    => (λ arg (λ env e))
    303 ;; (e₁ env e₂)      => ((e₁ env) e₂)
    304 ;; env              => env
    305 ;; arg              => arg
    306 ;; get              => primitive "get" from an immutable name↦val mapping (could be implemented in plain lambda-calculus)
    307 ;; add              => primitive "add" to an immutable name↦val mapping (could be implemented in plain lambda-calculus)
    308 ;;
    309 ;; With laziness:
    310 ;; (e₁ env e₂)      => ((e₁ env) (λ env (λ _ e₂)))
    311 ;;
    312 ;; With continuations
    313 ;; (e₁ env e₂)      => ((e₁ env) (λ env (λ _ e₂)))
    314 ;; (f (g x)) => (g k=f x)
    315 ;;
    316 ;; With #%app
    317 ;; 
    318 |#
    319 
    320 
    321 
    322 
    323 
    324 
    325 
    326 
    327 
    328 
    329 
    330 
    331 
    332 
    333 
    334 
    335 
    336 
    337 
    338 
    339 
    340 ;; "x" ::= "x","y","z"…   String
    341 ;; e ::= (-λ -env -arg -k e)      Abstraction (lambda) which takes
    342 ;;                                  * an environment            always named -env (not in the -env)
    343 ;;                                  * a promise for an argument always named -arg (not in the -env)
    344 ;;                                  * a continuation            always named -k   (not in the -env)
    345 ;;    |  (v e-env e-arg e-k)      Tail call
    346 ;;    |  (v e-env ()    e-k)      Forcing a promise
    347 ;;    |  (v ()    e-ret  ())      Calling a continuation
    348 ;;    |  -env                     the -env
    349 ;;    |  -arg                     the -arg of the innermost lambda
    350 ;;    |  -k                       the continuation of the innermost lambda
    351 ;;    |  (-get e-env e-str)       Get variable from environment
    352 ;;    |  (-add e-env e-str e-val) Extend environment with new binding
    353 
    354 
    355 #|
    356 (λ -env -arg -k
    357   ((get -env "1+") (-add -env "foo" 42) -arg -k))
    358 
    359 (λ -env -arg -k
    360   (let (["env2" (-add -env "foo" 42)])
    361     ((get -env "1+") (get -env "env2") -arg -k)))
    362 
    363 (define -lambda '…)
    364 |#
    365 
    366 
    367 
    368 
    369 
    370 
    371 
    372 
    373 
    374 
    375 
    376 
    377 
    378 
    379 
    380 
    381 
    382 
    383 
    384 #;(
    385  ;; lambda calculus:
    386  v ::= (λ x e)
    387     || "str"
    388     || 0
    389  e ::= v
    390     || x
    391     || (e e)
    392 
    393  ;; reduction:
    394     redex                         continuation frames
    395     (((λ x (λ y x)) 1) (inc 1))   _
    396  =>  ((λ x (λ y x)) 1)            _  (_                 (inc 1))
    397  =>        (λ y 1)                _  (_                 (inc 1))
    398  => (      (λ y 1)     (inc 1))   _
    399  =>                    (inc 1)    _  ((λ y 1)           _      )
    400  =>                    2          _  ((λ y 1)           _      )
    401  => (      (λ y 1)     2      )   _
    402  =>             1                 _
    403 
    404  ;; state of evaluation:
    405           redex = (v1 v2)
    406    continuation = (λ result e)
    407 )
    408 
    409 
    410 #;(
    411  ;; Using explicit closures:
    412  v ::= (λ […] x e)
    413     || "str"
    414     || 0
    415  e ::= v
    416     || (λ ?? x e)
    417     || x
    418     || (e e)
    419 
    420     
    421  ;; Rules:
    422  rule name     environment   redex              continuation frames
    423  =>            environment′  redex′             continuation frames′
    424 
    425  APP           [E]           ((λ [E′] x e) v)   …
    426  =>            [E′,x=v]                 e       …
    427 
    428  CAPTURE       [E]           (λ ??  x e)        …
    429  =>            [E]           (λ [E] x e)        …
    430 
    431  APP-F         [E]           (e-f e-arg)        …
    432  =>            [E]            e-f               … E,(_ e-arg)
    433 
    434  APP-ARG       [E]           (v-f e-arg)        …
    435  =>            [E]                e-arg         … E,(v-f _)
    436 
    437  CONTINUE-F    [E]            v-f               … E′,(_ e-arg)
    438  =>            [E′]          (v-f e-arg)        …
    439 
    440  CONTINUE-ARG  [E]                v-arg         … E′,(v-f _)       Optimization: [],(v-f _)
    441  =>            [E′]          (v-f v-arg)        …
    442 
    443  DEREFERENCE   [E,x=v,E′]    x                  …
    444  =>            [E,x=v,E′]    v                  …
    445  
    446  ;; Reduction example:
    447     env             redex                                 continuation frames                                           rule to use
    448     [inc=…]         (((λ ?? x (λ ??    y x)) 1) (inc 1))  … […],_                                                       APP-F
    449  => [inc=…]          ((λ ?? x (λ ??    y x)) 1)           … […],_  [inc=…],(_ (inc 1))                                  APP-F
    450  => [inc=…]           (λ ?? x (λ ??    y x))              … […],_  [inc=…],(_ (inc 1))  [inc=…],(_ 1)                   CAPTURE
    451  => [inc=…]           (λ [] x (λ ??    y x))              … […],_  [inc=…],(_ (inc 1))  [inc=…],(_ 1)                   CONTINUE-F
    452  => [inc=…]          ((λ [] x (λ ??    y x)) 1)           … […],_  [inc=…],(_ (inc 1))                                  APP-ARG
    453  => [inc=…]                                  1            … […],_  [inc=…],(_ (inc 1))  [inc=…],((λ [] x (λ ?? y x)) _) CONTINUE-ARG
    454  => [inc=…]          ((λ [] x (λ ??    y x)) 1)           … […],_  [inc=…],(_ (inc 1))                                  APP
    455  => [inc=…,x=1]               (λ ??    y x)               … […],_  [inc=…],(_ (inc 1))                                  CAPTURE
    456  => [inc=…,x=1]               (λ [x=1] y x)               … […],_  [inc=…],(_ (inc 1))                                  CONTINUE-F
    457  => [inc=…]         (         (λ [x=1] y x)     (inc 1))  … […],_                                                       APP-ARG
    458  => [inc=…]                                     (inc 1)   … […],_  [inc=…],((λ [x=1] y x) _)                            APP-F
    459  => [inc=…]                                      inc      … […],_  [inc=…],((λ [x=1] y x) _)  [inc=…],(_ 1)             GETVAR
    460  => [inc=…]                                      …        … […],_  [inc=…],((λ [x=1] y x) _)  [inc=…],(_ 1)             CONTINUE-F
    461  => [inc=…]                                     (…   1)   … […],_  [inc=…],((λ [x=1] y x) _)                            APP-ARG
    462  => [inc=…]                                          1    … […],_  [inc=…],((λ [x=1] y x) _)  [inc=…],(… _)             CONTINUE-ARG
    463  => [inc=…]                                     (…   1)   … […],_  [inc=…],((λ [x=1] y x) _)                            APP
    464    465  => [inc=…]                                     2         … […],_  [inc=…],((λ [x=1] y x) _)                            CONTINUE-ARG
    466  => [inc=…]         (         (λ [x=1] y x)     2      )  … […],_                                                       APP
    467  => [inc=…,x=1,y=2]                      x                … […],_                                                       GETVAR
    468  => [inc=…,x=1,y=2]                      2                … […],_                                                       CONTINUE-?
    469  => […]                                  2                …                                                             …
    470 
    471 )
    472 
    473 
    474 #;(
    475  ;; Using first-class environments and lazy evaluations:
    476  ;; λ, env, χ, get, push, #%drop are keywords
    477  ;; v-env
    478  v ::= (\ env χ e) ;; open term, expects an env to close the term
    479     || […]         ;; mapping from names to values
    480     || "str"
    481     || 0
    482     || get
    483     || push
    484     || pop
    485  e ::= v
    486     || (@ e-f e-env e-arg)
    487 
    488 
    489 TODO: instead of ad-hoc var-to-string conversion, use a functional env
    490     
    491  ;; Rules:
    492  rule name     environment                   redex                                                continuation frames
    493  =>            environment′                  redex′                                               continuation frames′
    494 
    495 ;; Primitive application
    496  APP           env=[E],    χ=X               (@ (\ env χ e) v-env (\ env χ e-arg))                …
    497  =>            env=v-env,χ=(\ env χ e-arg)               e                                        …
    498 ;;---------------------------------------------------------------------------------------------------------------------------
    499 ;; Evaluation of sub-parts of an application
    500  APP-F         env=[E],    χ=X               (@  e-f e-env e-arg)                                 …
    501  =>            env=[E],    χ=X                   e-f                                              … env=[E],χ=X,(@ _   e-env e-arg)
    502 
    503  APP-ENV       env=[E],    χ=X               (@ v-f e-env e-arg)                                  …
    504  =>            env=[E],    χ=X                      e-env                                         … env=[E],χ=X,(@ v-f _     e-arg)
    505 
    506  APP-ARG       env=[E],    χ=X               (@ v-f v-env e-arg)                                  …
    507  =>            env=[E],    χ=X                            e-arg                                   … env=[E],χ=X,(@ v-f v-env _    )
    508 
    509  CONTINUE-F    env=[E],    χ=X                v-f                                                 … E′,χ=X′,(_   e-env e-arg)
    510  =>            env=[E′],   χ=X′              (@ v-f e-env e-arg)                                  …
    511 
    512  CONTINUE-ENV  env=[E],    χ=X                    v-env                                           … E′,χ=X′,(v-f _     e-arg)
    513  =>            env=[E′],   χ=X′              (@ v-f v-env e-arg)                                  …
    514 
    515  CONTINUE-ARG  env=[E],    χ=X                          v-arg                                     … E′,χ=X′,(v-f v-env _    )
    516  =>            env=[E′],   χ=X′              (@ v-f v-env v-arg)                                  … 
    517 
    518 ;;---------------------------------------------------------------------------------------------------------------------------
    519 ;; Syntactic sugar
    520 
    521 ;; insertion of #%app at the front of all parentheses that don't start with an @ or \ or #%app
    522  SUGAR-APP     env=[E],    χ=X               (                         e-f             e-arg )    …
    523  =>            env=[E],    χ=X               (#%app                    e-f             e-arg )    …
    524  =>            env=[E],    χ=X                 (@ (@ (@ get env (\ env χ "#%app"))
    525                                                    env
    526                                                    (\ env χ e-f))
    527                                                 env
    528                                                 (\ env χ e-arg))                                  …
    529 ;; defaults to:
    530  =>            env=[E],    χ=X               (@     e-f env (\ env χ e-arg))                      …
    531 
    532 ;; In particular, the sugared λ is just a function
    533  SUGAR-LAM     env=[E],    χ=X               (λ var-name e)                                       …
    534  =>            env=[E],    χ=X               (#%app (#%app λ var-name) e)                         …
    535 ;; defaults to:
    536  =>            env=[E],    χ=X               (@ capture
    537                                                 env
    538                                                 (\ env χ (@ (\ env χ e)
    539                                                             (@ (@ push env "var-name") env χ)
    540                                                             χ)))
    541 
    542  SUGAR-STR     env=[E],    χ=X                        "str"                                       …
    543  =>            env=[E],    χ=X               (#%datum "str")                                      …
    544 
    545  SUGAR-NUM     env=[E],    χ=X                        0                                           …
    546  =>            env=[E],    χ=X               (#%datum 0)                                          …
    547 
    548  SUGAR-VAR     env=[E],    χ=X                        var-name                                    …
    549  =>            env=[E],    χ=X               (get env var-name)                                   …
    550 ;;---------------------------------------------------------------------------------------------------------------------------
    551  CAPTURE       env=[E],    χ=X               (@ capture v-env (\ env χ e))                        …
    552  =>            env=[E],    χ=X               (\ env χ (@ (λ env χ e) v-env χ))                    …
    553 
    554  FORCE         env=[E],    χ=(\ env χ e-arg) (@ #%force v-env (\ env χ e))                          …
    555  =>            env=[E],    χ=()              (@ (\ env χ e) v-env dummy)                          …
    556 )
    557 
    558 
    559 
    560 
    561