Skip to content

Instantly share code, notes, and snippets.

@edwinb

edwinb/Eval.idr Secret

Last active Aug 28, 2021
Embed
What would you like to do?
module Eval
import ToyLang
import Scheme
import System
data NS : Type where
nextName : Ref NS Integer => IO Integer
nextName
= do n <- get NS
put NS (n + 1)
pure n
data SVar = Bound String | Free String
Show SVar where
show (Bound x) = x
show (Free x) = "'" ++ x
getName : SVar -> String
getName (Bound x) = x
getName (Free x) = x
data SchVars : List Name -> Type where
Nil : SchVars []
(::) : SVar -> SchVars ns -> SchVars (n :: ns)
Show (SchVars ns) where
show xs = show (toList xs)
where
toList : forall ns . SchVars ns -> List String
toList [] = []
toList (Bound x :: xs) = x :: toList xs
toList (Free x :: xs) = "'x" :: toList xs
getSchVar : {idx : _} -> (0 _ : IsVar n idx vars) -> SchVars vars -> String
getSchVar First (Bound x :: xs) = x
getSchVar First (Free x :: xs) = "'" ++ x
getSchVar (Later p) (x :: xs) = getSchVar p xs
-- Convert a term to a scheme string. There is probably a neater way than
-- building the string then passing it to scheme, but I don't yet know what
-- it is.
toScheme : Ref NS Integer =>
SchVars vars -> Term vars -> IO String
toScheme vs (Local idx p) = pure (getSchVar p vs)
toScheme vs (Global n) = pure n
toScheme vs (Bind x Lam sc)
= do i <- nextName
let x' = x ++ "-" ++ show i
pure $ "(lambda (" ++ x' ++ ") "
++ !(toScheme (Bound x' :: vs) sc) ++ ")"
toScheme vs (Bind x (Let y) sc)
= do i <- nextName
let x' = x ++ "-" ++ show i
pure $ "(let [(" ++ x' ++ " " ++ !(toScheme vs y) ++ ")] " ++
!(toScheme (Bound x' :: vs) sc) ++ ")"
toScheme vs (App f a)
= pure $ "(" ++ !(toScheme vs f) ++ " " ++
!(toScheme vs a) ++ ")"
toScheme vs (Pair x y)
= pure $ "(cons " ++ !(toScheme vs x) ++ " " ++
!(toScheme vs y) ++ ")"
toScheme vs Null = pure "'()"
toScheme vs (Val x) = pure (show x)
toScheme vs (Op f x y)
= pure $ "(" ++ schOp f ++ " " ++
!(toScheme vs x) ++ " " ++
!(toScheme vs y) ++ ")"
where
schOp : PrimOp -> String
schOp Plus = "fx+"
schOp Minus = "fx-"
schOp Times = "fx*"
schOp Divide = "fx/"
-- Convert a top level case tree to a scheme definition, with the scheme
-- expression to return if evaluating the case tree is blocked.
toSchemeCase : Ref NS Integer =>
String -> SchVars vars -> CaseTree vars -> IO String
toSchemeCase blocked vs (IfNull p t e)
= do i <- nextName
let enm = "arg-" ++ show i
pure $
"(if (null? " ++ (getSchVar p vs) ++ ") " ++
!(toSchemeCase blocked vs t) ++ " " ++
"(if (pair? " ++ (getSchVar p vs) ++ ") " ++
"(let [(" ++ enm ++ " (cdr " ++ getSchVar p vs ++ "))] " ++
!(toSchemeCase blocked (Bound enm :: vs) e) ++ ") " ++
blocked ++ "))"
toSchemeCase blocked vs (IfZero p t e)
= pure $ "(if (number? " ++ (getSchVar p vs) ++ ") " ++
"(if (eq? 0 " ++ (getSchVar p vs) ++ ") " ++
!(toSchemeCase blocked vs t) ++ " " ++
!(toSchemeCase blocked vs e) ++ ")" ++
blocked ++ ")"
toSchemeCase blocked vs (STerm t) = toScheme vs t
compileDef : Name -> (args : _) -> CaseTree args -> IO ()
compileDef n args tree
= do i <- newRef NS 0
argvs <- mkArgs args
body <- toSchemeCase (mkBlocked argvs) argvs tree
let def = "(define " ++ n ++ " " ++ bindArgs argvs body ++ ")"
let Just _ = evalScheme def
| Nothing => putStrLn "Oops"
putStrLn def
let Just res = evalScheme n
| Nothing => putStrLn "Oops"
debugScheme res
where
bindArgs : SchVars ns -> String -> String
bindArgs [] body = body
bindArgs (x :: xs) body
= "(lambda (" ++ show x ++ ") " ++ bindArgs xs body ++ ")"
showVars : SchVars ns -> String
showVars [] = ""
showVars [x] = show x
showVars (x :: xs) = show x ++ " " ++ showVars xs
mkBlocked : SchVars ns -> String
mkBlocked argvs
= "(vector " ++ show n ++ " " ++
show (length args) ++ " " ++
showVars argvs ++ ")"
mkArgs : Ref NS Integer =>
(ns : List Name) -> IO (SchVars ns)
mkArgs [] = pure []
mkArgs (x :: xs)
= do i <- nextName
pure $ Bound (x ++ "-" ++ show i) :: !(mkArgs xs)
-- A value is a pair of the result of running the scheme, and the scheme
-- variable names. We use the scheme variable names to turn symbols (which
-- stand for free variables) into Locals again
data Value : List Name -> Type where
MkValue : ForeignObj -> SchVars vars -> Value vars
eval : Env Term vars -> Term vars -> IO (Value vars)
eval env tm
= do i <- newRef NS 0
(bind, schEnv) <- mkEnv env id
tm' <- toScheme schEnv tm
let Just res = evalScheme (bind tm')
| Nothing => believe_me {a=IO ()} $ do putStrLn "Oops"
exitWith (ExitFailure 1)
-- ^ if everything worked out, this can't happen!
-- Place your bets...
pure (MkValue res schEnv)
where
mkEnv : forall vars . Ref NS Integer =>
Env Term vars ->
(String -> String) ->
IO (String -> String, SchVars vars)
mkEnv [] k = pure (k, [])
mkEnv (Lam :: es) k
= do i <- nextName
(bind, vs) <- mkEnv es k
pure (bind, Free ("free-" ++ show i) :: vs)
mkEnv (Let v :: es) k
= do i <- nextName
(bind, vs) <- mkEnv es k
v' <- toScheme vs v
let n = "let-var-" ++ show i
pure (\x => "(let [(" ++ n ++ " " ++ v' ++ ")] " ++
bind x ++ ")",
Bound n :: vs)
cond : List (Bool, Lazy a) -> Lazy a -> a
cond [] def = def
cond ((x, y) :: xs) def = if x then y else cond xs def
quote' : Ref NS Integer =>
SchVars (outer ++ vars) -> ForeignObj -> IO (Term (outer ++ vars))
quote' vs val
= case decodeObj val of
Null => pure Null
Cons x y => pure (Pair !(quote' vs x) !(quote' vs y))
IntegerVal x => pure (Val x)
Symbol x => pure (findName vs x)
Procedure x =>
do i <- nextName
let n = "ref-" ++ show i
let sc = unsafeApply val (makeSymbol n)
sc' <- quote' {outer = n :: outer} (Bound n :: vs) sc
pure (Bind n Lam sc')
Vector (fn_in :: arity_in :: args) =>
do let StringVal fn = decodeObj fn_in
| _ => pure Null
let IntegerVal arity = decodeObj arity_in
| _ => pure Null
args' <- traverse (quote' vs) args
pure (apply (Global fn) args')
_ => pure Null
where
findName : forall vars . SchVars vars -> Name -> Term vars
findName [] n = Global n
findName (x :: xs) n
= if getName x == n
then Local _ First
else let Local _ p = findName xs n
| _ => Global n in
Local _ (Later p)
quote : Value vars -> IO (Term vars)
quote (MkValue val schEnv)
= do i <- newRef NS 0
quote' {outer = []} schEnv val
debugVal : Value vars -> IO ()
debugVal (MkValue val sch) = debugScheme val
test : IO ()
test = do -- Make a scheme function called 'plus' that implements the one
-- in our little language
compileDef "plus" _ plusfn
-- and a couple of others
compileDef "natToInt" _ natToIntfn
compileDef "intToNat" _ intToNatfn
-- Now lets' try evaluating it.
-- First just dump the scheme values
debugVal !(eval [] (suc (suc zero)))
debugVal !(eval [] (apply (Global "plus") [suc (suc zero), suc (suc zero)]))
debugVal !(eval {vars = ["var"]}
[Lam] (apply (Global "plus")
[suc (suc zero),
suc (suc (Local _ First))]))
debugVal !(eval {vars = ["var"]}
[Let (suc zero)] (apply (Global "plus")
[suc (suc zero),
suc (suc (Local _ First))]))
-- Now try quoting the scheme values with free variables back as
-- terms
putStrLn "Quoting:\n--------"
val <- eval [] (apply (Global "plus") [suc (suc zero), suc (suc zero)])
printLn !(quote val)
-- Try 'plus' but blocked on the second argument
lamval <- eval [] (Bind "var" Lam
(apply (Global "plus")
[suc (suc zero),
suc (suc (Local _ First))]))
printLn !(quote lamval)
-- Try 'plus' but blocked on the first argument
lamval <- eval [] (Bind "var" Lam
(apply (Global "plus")
[suc (suc (Local _ First)),
suc (suc zero)]))
printLn !(quote lamval)
-- And blocked on both
lamsval <- eval [] (Bind "x" Lam
(Bind "y" Lam
(apply (Global "plus")
[suc (suc (Local _ First)),
suc (suc (Local _ (Later First)))])))
printLn !(quote lamsval)
-- Try it in an environment, rather than under lambdas
envval <- eval {vars = ["x", "y"]}
[Let (suc zero), Lam]
(apply (Global "plus")
[suc (suc (Local _ First)),
suc (suc (Local _ (Later First)))])
printLn !(quote envval)
-- And some nat/int conversions to try something bigger
val <- eval [] (apply (Global "natToInt")
[apply (Global "plus")
[apply (Global "intToNat") [Val 400000],
apply (Global "intToNat") [Val 540000]]])
printLn !(quote val)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment