Make `callcc` into a proper primitive rather than a hardcoded "variable".
parent
a543981b67
commit
74d2e26646
|
@ -44,8 +44,6 @@ This interpreter has preliminary support for
|
||||||
However, it has not been thoroughly tested.
|
However, it has not been thoroughly tested.
|
||||||
|
|
||||||
To use it, simply apply the variable `callcc` like you would a function, e.g. `(callcc (\k. ...))`.
|
To use it, simply apply the variable `callcc` like you would a function, e.g. `(callcc (\k. ...))`.
|
||||||
`callcc` is not a normal variable and cannot be shadowed;
|
|
||||||
`\callcc. callcc` is *not* the identity function, it *ignores* its argument and then returns the *operator* `callcc`.
|
|
||||||
|
|
||||||
Continuations are printed as `λ!. ... ! ...`, like a lambda abstraction
|
Continuations are printed as `λ!. ... ! ...`, like a lambda abstraction
|
||||||
with an argument named `!` which is used exactly once;
|
with an argument named `!` which is used exactly once;
|
||||||
|
|
|
@ -56,8 +56,6 @@ library:
|
||||||
# Less stupid warnings, but I still don't care
|
# Less stupid warnings, but I still don't care
|
||||||
- -Wno-all-missed-specialisations
|
- -Wno-all-missed-specialisations
|
||||||
- -Wno-missing-local-signatures
|
- -Wno-missing-local-signatures
|
||||||
# This is a good warning, but often polymorphism isn't actually needed.
|
|
||||||
- -Wno-monomorphism-restriction
|
|
||||||
# Explicit import lists are generally a good thing, but I don't want them
|
# Explicit import lists are generally a good thing, but I don't want them
|
||||||
# in certain cases (e.g. importing my own modules, task-specific modules like the parser).
|
# in certain cases (e.g. importing my own modules, task-specific modules like the parser).
|
||||||
- -Wno-missing-import-lists
|
- -Wno-missing-import-lists
|
||||||
|
|
|
@ -1,8 +1,8 @@
|
||||||
module LambdaCalculus.Evaluator
|
module LambdaCalculus.Evaluator
|
||||||
( Expr (..), ExprF (..), VoidF, Text
|
( Expr (..), ExprF (..), VoidF, Text
|
||||||
, Eval, EvalExpr, EvalX, EvalXF (..)
|
, Eval, EvalExpr, EvalX, EvalXF (..)
|
||||||
, pattern AppFE, pattern Cont, pattern ContF
|
, pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
|
||||||
, eval, traceEval
|
, eval, traceEval, substitute, alphaConvert
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import LambdaCalculus.Evaluator.Base
|
import LambdaCalculus.Evaluator.Base
|
||||||
|
@ -21,18 +21,17 @@ import Data.Void (Void, absurd)
|
||||||
-- | Free variables are variables which are present in an expression but not bound by any abstraction.
|
-- | Free variables are variables which are present in an expression but not bound by any abstraction.
|
||||||
freeVars :: EvalExpr -> HashSet Text
|
freeVars :: EvalExpr -> HashSet Text
|
||||||
freeVars = cata \case
|
freeVars = cata \case
|
||||||
VarF name -> HS.singleton name
|
AbsF n e -> HS.delete n e
|
||||||
AppFE e1 e2 -> HS.union e1 e2
|
ContF e -> HS.delete "!" e
|
||||||
AbsF n e -> HS.delete n e
|
VarF n -> HS.singleton n
|
||||||
ContF e -> HS.delete "!" e
|
e -> foldr HS.union HS.empty e
|
||||||
|
|
||||||
-- | Bound variables are variables which are bound by any form of abstraction in an expression.
|
-- | Bound variables are variables which are bound by any form of abstraction in an expression.
|
||||||
boundVars :: EvalExpr -> HashSet Text
|
boundVars :: EvalExpr -> HashSet Text
|
||||||
boundVars = cata \case
|
boundVars = cata \case
|
||||||
VarF _ -> HS.empty
|
AbsF n e -> HS.insert n e
|
||||||
AppFE e1 e2 -> HS.union e1 e2
|
ContF e -> HS.insert "!" e
|
||||||
AbsF n e -> HS.insert n e
|
e -> foldr HS.union HS.empty e
|
||||||
ContF e -> HS.insert "!" e
|
|
||||||
|
|
||||||
-- | Vars that occur anywhere in an experession, bound or free.
|
-- | Vars that occur anywhere in an experession, bound or free.
|
||||||
usedVars :: EvalExpr -> HashSet Text
|
usedVars :: EvalExpr -> HashSet Text
|
||||||
|
@ -88,16 +87,17 @@ unsafeSubstitute var val = para \case
|
||||||
| ContF _ <- e', var == "!" -> unmodified e'
|
| ContF _ <- e', var == "!" -> unmodified e'
|
||||||
| otherwise -> substituted e'
|
| otherwise -> substituted e'
|
||||||
where
|
where
|
||||||
|
substituted, unmodified :: EvalExprF (EvalExpr, EvalExpr) -> EvalExpr
|
||||||
substituted = embed . fmap snd
|
substituted = embed . fmap snd
|
||||||
unmodified = embed . fmap fst
|
unmodified = embed . fmap fst
|
||||||
|
|
||||||
isReducible :: EvalExpr -> Bool
|
isReducible :: EvalExpr -> Bool
|
||||||
isReducible = snd . cata \case
|
isReducible = snd . cata \case
|
||||||
AppF ctr (Identity args) -> eliminator ctr [args]
|
AppFE ctr args -> eliminator ctr [args]
|
||||||
VarF "callcc" -> constructor
|
CallCCF -> constructor
|
||||||
AbsF _ _ -> constructor
|
AbsF _ _ -> constructor
|
||||||
ContF _ -> constructor
|
ContF _ -> constructor
|
||||||
VarF _ -> constant
|
VarF _ -> constant
|
||||||
where
|
where
|
||||||
-- | Constants are irreducible in any context.
|
-- | Constants are irreducible in any context.
|
||||||
constant = (False, False)
|
constant = (False, False)
|
||||||
|
@ -150,8 +150,7 @@ evaluatorStep = \case
|
||||||
put []
|
put []
|
||||||
pure $ substitute "!" ex body
|
pure $ substitute "!" ex body
|
||||||
-- capture the current continuation if requested...
|
-- capture the current continuation if requested...
|
||||||
Var "callcc" -> do
|
CallCC -> do
|
||||||
-- Don't worry about variable capture here for now.
|
|
||||||
k <- gets $ continue (Var "!")
|
k <- gets $ continue (Var "!")
|
||||||
pure $ App ex (Cont k)
|
pure $ App ex (Cont k)
|
||||||
-- otherwise the value is irreducible and we can continue evaluation.
|
-- otherwise the value is irreducible and we can continue evaluation.
|
||||||
|
|
|
@ -2,7 +2,7 @@ module LambdaCalculus.Evaluator.Base
|
||||||
( Identity (..)
|
( Identity (..)
|
||||||
, Expr (..), ExprF (..), VoidF, Text
|
, Expr (..), ExprF (..), VoidF, Text
|
||||||
, Eval, EvalExpr, EvalExprF, EvalX, EvalXF (..)
|
, Eval, EvalExpr, EvalExprF, EvalX, EvalXF (..)
|
||||||
, pattern AppFE, pattern Cont, pattern ContF
|
, pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import LambdaCalculus.Expression.Base
|
import LambdaCalculus.Expression.Base
|
||||||
|
@ -23,14 +23,16 @@ type instance AppArgsF Eval = Identity
|
||||||
type instance LetArgsF Eval = VoidF
|
type instance LetArgsF Eval = VoidF
|
||||||
type instance XExprF Eval = EvalXF
|
type instance XExprF Eval = EvalXF
|
||||||
|
|
||||||
newtype EvalXF r
|
data EvalXF r
|
||||||
-- | A continuation. This is identical to a lambda abstraction,
|
-- | A continuation. This is identical to a lambda abstraction,
|
||||||
-- with the exception that it performs the side-effect of
|
-- with the exception that it performs the side-effect of
|
||||||
-- deleting the current continuation.
|
-- deleting the current continuation.
|
||||||
--
|
--
|
||||||
-- Continuations do not have any corresponding surface-level syntax,
|
-- Continuations do not have any corresponding surface-level syntax,
|
||||||
-- but may be printed like a lambda with the illegal variable `!`.
|
-- but may be printed like a lambda with the illegal variable `!`.
|
||||||
= Cont_ r
|
= Cont_ !r
|
||||||
|
-- | Call-with-current-continuation, an evaluator built-in function.
|
||||||
|
| CallCC_
|
||||||
deriving (Eq, Functor, Foldable, Traversable, Show)
|
deriving (Eq, Functor, Foldable, Traversable, Show)
|
||||||
|
|
||||||
instance RecursivePhase Eval where
|
instance RecursivePhase Eval where
|
||||||
|
@ -40,13 +42,19 @@ instance RecursivePhase Eval where
|
||||||
pattern Cont :: EvalExpr -> EvalExpr
|
pattern Cont :: EvalExpr -> EvalExpr
|
||||||
pattern Cont e = ExprX (Cont_ e)
|
pattern Cont e = ExprX (Cont_ e)
|
||||||
|
|
||||||
|
pattern CallCC :: EvalExpr
|
||||||
|
pattern CallCC = ExprX CallCC_
|
||||||
|
|
||||||
pattern ContF :: r -> EvalExprF r
|
pattern ContF :: r -> EvalExprF r
|
||||||
pattern ContF e = ExprXF (Cont_ e)
|
pattern ContF e = ExprXF (Cont_ e)
|
||||||
|
|
||||||
|
pattern CallCCF :: EvalExprF r
|
||||||
|
pattern CallCCF = ExprXF CallCC_
|
||||||
|
|
||||||
pattern AppFE :: r -> r -> EvalExprF r
|
pattern AppFE :: r -> r -> EvalExprF r
|
||||||
pattern AppFE ef ex = AppF ef (Identity ex)
|
pattern AppFE ef ex = AppF ef (Identity ex)
|
||||||
|
|
||||||
{-# COMPLETE Var, App, Abs, Let, Cont #-}
|
{-# COMPLETE Var, App, Abs, Let, Cont, CallCC #-}
|
||||||
{-# COMPLETE VarF, AppF, AbsF, LetF, ContF #-}
|
{-# COMPLETE VarF, AppF, AbsF, LetF, ContF, CallCCF #-}
|
||||||
{-# COMPLETE VarF, AppFE, AbsF, LetF, ExprXF #-}
|
{-# COMPLETE VarF, AppFE, AbsF, LetF, ExprXF #-}
|
||||||
{-# COMPLETE VarF, AppFE, AbsF, LetF, ContF #-}
|
{-# COMPLETE VarF, AppFE, AbsF, LetF, ContF, CallCCF #-}
|
||||||
|
|
|
@ -1,22 +1,24 @@
|
||||||
module LambdaCalculus.Expression
|
module LambdaCalculus.Expression
|
||||||
( Expr (..), ExprF (..), DefF (..), VoidF, Text
|
( Expr (..), ExprF (..), DefF (..), VoidF, Text
|
||||||
, Eval, EvalExpr, EvalX, EvalXF (..), Identity (..)
|
, Eval, EvalExpr, EvalX, EvalXF (..), Identity (..)
|
||||||
, pattern AppFE, pattern Cont, pattern ContF
|
, pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
|
||||||
, Parse, AST, ASTF, NonEmptyDefFs (..), NonEmpty (..), simplify
|
, Parse, AST, ASTF, NonEmptyDefFs (..), NonEmpty (..), simplify
|
||||||
, pattern LetFP
|
, pattern LetFP
|
||||||
, ast2eval, eval2ast
|
, ast2eval, eval2ast
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import LambdaCalculus.Evaluator.Base
|
import LambdaCalculus.Evaluator.Base
|
||||||
|
import LambdaCalculus.Evaluator
|
||||||
import LambdaCalculus.Syntax.Base
|
import LambdaCalculus.Syntax.Base
|
||||||
|
|
||||||
import Data.Functor.Foldable (cata, hoist)
|
import Data.Functor.Foldable (cata, hoist)
|
||||||
|
import Data.HashSet qualified as HS
|
||||||
import Data.List (foldl')
|
import Data.List (foldl')
|
||||||
import Data.List.NonEmpty (toList)
|
import Data.List.NonEmpty (toList)
|
||||||
|
|
||||||
-- | Convert from an abstract syntax tree to an evaluator expression.
|
-- | Convert from an abstract syntax tree to an evaluator expression.
|
||||||
ast2eval :: AST -> EvalExpr
|
ast2eval :: AST -> EvalExpr
|
||||||
ast2eval = cata \case
|
ast2eval = substitute "callcc" CallCC . cata \case
|
||||||
VarF name -> Var name
|
VarF name -> Var name
|
||||||
AppF ef exs -> foldl' App ef $ toList exs
|
AppF ef exs -> foldl' App ef $ toList exs
|
||||||
AbsF ns e -> foldr Abs e $ toList ns
|
AbsF ns e -> foldr Abs e $ toList ns
|
||||||
|
@ -26,8 +28,16 @@ ast2eval = cata \case
|
||||||
|
|
||||||
-- | Convert from an evaluator expression to an abstract syntax tree.
|
-- | Convert from an evaluator expression to an abstract syntax tree.
|
||||||
eval2ast :: EvalExpr -> AST
|
eval2ast :: EvalExpr -> AST
|
||||||
eval2ast = hoist \case
|
-- Because all `ast2eval` replaces all free instances of `callcc`,
|
||||||
VarF name -> VarF name
|
-- all instances of `callcc` must be bound;
|
||||||
AppFE ef ex -> AppF ef (ex :| [])
|
-- therefore, we are free to alpha convert them,
|
||||||
AbsF n e -> AbsF (n :| []) e
|
-- freeing the name `callcc` for us to use for the built-in again.
|
||||||
ContF e -> AbsF ("!" :| []) e
|
eval2ast = hoist go . alphaConvert (HS.singleton "callcc")
|
||||||
|
where
|
||||||
|
go :: EvalExprF r -> ASTF r
|
||||||
|
go = \case
|
||||||
|
VarF name -> VarF name
|
||||||
|
CallCCF -> VarF "callcc"
|
||||||
|
AppFE ef ex -> AppF ef (ex :| [])
|
||||||
|
AbsF n e -> AbsF (n :| []) e
|
||||||
|
ContF e -> AbsF ("!" :| []) e
|
||||||
|
|
|
@ -39,10 +39,10 @@ omega = App x x
|
||||||
where x = Abs "x" (App (Var "x") (Var "x"))
|
where x = Abs "x" (App (Var "x") (Var "x"))
|
||||||
|
|
||||||
cc1 :: EvalExpr
|
cc1 :: EvalExpr
|
||||||
cc1 = App (Var "callcc") (Abs "k" (App omega (App (Var "k") (Var "z"))))
|
cc1 = App CallCC (Abs "k" (App omega (App (Var "k") (Var "z"))))
|
||||||
|
|
||||||
cc2 :: EvalExpr
|
cc2 :: EvalExpr
|
||||||
cc2 = App (Var "y") (App (Var "callcc") (Abs "k" (App (Var "z") (App (Var "k") (Var "x")))))
|
cc2 = App (Var "y") (App CallCC (Abs "k" (App (Var "z") (App (Var "k") (Var "x")))))
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = defaultMain $
|
main = defaultMain $
|
||||||
|
|
Loading…
Reference in New Issue