{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

module Kanren.Data.Scheme (
  Symbol,
  Env,
  SExpr (..),
  LogicSExpr (..),
  Value (..),
  LogicValue (..),
  evalo,
) where

import Control.Lens.TH (makePrisms)
import GHC.Exts (IsList, IsString (..))
import GHC.Generics (Generic)
import GHC.IsList (IsList (..))

import Control.DeepSeq
import Kanren.Core
import Kanren.Goal
import Kanren.LogicalBase
import Kanren.TH

type Symbol = Atomic String
type Env = [(Symbol, Value)]

data SExpr
  = SSymbol Symbol
  | SNil
  | SCons SExpr SExpr
  deriving (SExpr -> SExpr -> Bool
(SExpr -> SExpr -> Bool) -> (SExpr -> SExpr -> Bool) -> Eq SExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SExpr -> SExpr -> Bool
== :: SExpr -> SExpr -> Bool
$c/= :: SExpr -> SExpr -> Bool
/= :: SExpr -> SExpr -> Bool
Eq, (forall x. SExpr -> Rep SExpr x)
-> (forall x. Rep SExpr x -> SExpr) -> Generic SExpr
forall x. Rep SExpr x -> SExpr
forall x. SExpr -> Rep SExpr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SExpr -> Rep SExpr x
from :: forall x. SExpr -> Rep SExpr x
$cto :: forall x. Rep SExpr x -> SExpr
to :: forall x. Rep SExpr x -> SExpr
Generic, SExpr -> ()
(SExpr -> ()) -> NFData SExpr
forall a. (a -> ()) -> NFData a
$crnf :: SExpr -> ()
rnf :: SExpr -> ()
NFData)

data Value
  = SExpr SExpr
  | Closure Symbol SExpr Env
  deriving (Value -> Value -> Bool
(Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
/= :: Value -> Value -> Bool
Eq, (forall x. Value -> Rep Value x)
-> (forall x. Rep Value x -> Value) -> Generic Value
forall x. Rep Value x -> Value
forall x. Value -> Rep Value x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Value -> Rep Value x
from :: forall x. Value -> Rep Value x
$cto :: forall x. Rep Value x -> Value
to :: forall x. Rep Value x -> Value
Generic, Value -> ()
(Value -> ()) -> NFData Value
forall a. (a -> ()) -> NFData a
$crnf :: Value -> ()
rnf :: Value -> ()
NFData)

instance Show SExpr where
  show :: SExpr -> [Char]
show (SSymbol (Atomic [Char]
symbol)) = [Char]
symbol
  show SExpr
SNil = [Char]
"()"
  show (SCons SExpr
car SExpr
cdr) = [Char]
"(" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> [Char]
forall a. Show a => a -> [Char]
show SExpr
car [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> [Char]
showSList SExpr
cdr

showSList :: SExpr -> [Char]
showSList :: SExpr -> [Char]
showSList SExpr
SNil = [Char]
")"
showSList (SCons SExpr
car SExpr
cdr) = [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> [Char]
forall a. Show a => a -> [Char]
show SExpr
car [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> [Char]
showSList SExpr
cdr
showSList SExpr
other = [Char]
" . " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> [Char]
forall a. Show a => a -> [Char]
show SExpr
other [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance Show Value where
  show :: Value -> [Char]
show (SExpr SExpr
expr) = SExpr -> [Char]
forall a. Show a => a -> [Char]
show SExpr
expr
  show (Closure (Atomic [Char]
var) SExpr
body [(Symbol, Value)]
env) =
    [Char]
"#(lambda (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
var [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> [Char]
forall a. Show a => a -> [Char]
show SExpr
body [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Symbol, Value)] -> [Char]
forall a. Show a => a -> [Char]
show [(Symbol, Value)]
env [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance IsList SExpr where
  type Item SExpr = SExpr
  fromList :: [Item SExpr] -> SExpr
fromList [] = SExpr
SNil
  fromList (Item SExpr
x : [Item SExpr]
xs) = SExpr -> SExpr -> SExpr
SCons Item SExpr
SExpr
x ([Item SExpr] -> SExpr
forall l. IsList l => [Item l] -> l
fromList [Item SExpr]
xs)
  toList :: SExpr -> [Item SExpr]
toList = SExpr -> [Item SExpr]
SExpr -> [SExpr]
forall a. HasCallStack => a
undefined

instance IsString SExpr where
  fromString :: [Char] -> SExpr
fromString = Symbol -> SExpr
SSymbol (Symbol -> SExpr) -> ([Char] -> Symbol) -> [Char] -> SExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Symbol
forall a. a -> Atomic a
Atomic

makeLogical ''SExpr
makeLogical ''Value
makePrisms ''LogicSExpr
makePrisms ''LogicValue
makeExhaustivePrisms ''LogicSExpr
makeExhaustivePrisms ''LogicValue

instance Normalizable SExpr where
  normalize :: (forall i. VarId i -> Normalizer (VarId i))
-> Logic SExpr -> Normalizer (Logic SExpr)
normalize forall i. VarId i -> Normalizer (VarId i)
f (LogicSSymbol Term Symbol
x) = Term Symbol -> LogicSExpr
LogicSSymbol (Term Symbol -> LogicSExpr)
-> Normalizer (Term Symbol) -> Normalizer LogicSExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall i. VarId i -> Normalizer (VarId i))
-> Term Symbol -> Normalizer (Term Symbol)
forall a.
Normalizable a =>
(forall i. VarId i -> Normalizer (VarId i))
-> Term a -> Normalizer (Term a)
normalize' VarId i -> Normalizer (VarId i)
forall i. VarId i -> Normalizer (VarId i)
f Term Symbol
x
  normalize forall i. VarId i -> Normalizer (VarId i)
_ Logic SExpr
LogicSExpr
LogicSNil = LogicSExpr -> Normalizer LogicSExpr
forall a. a -> Normalizer a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LogicSExpr
LogicSNil
  normalize forall i. VarId i -> Normalizer (VarId i)
f (LogicSCons Term SExpr
car Term SExpr
cdr) = Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons (Term SExpr -> Term SExpr -> LogicSExpr)
-> Normalizer (Term SExpr) -> Normalizer (Term SExpr -> LogicSExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall i. VarId i -> Normalizer (VarId i))
-> Term SExpr -> Normalizer (Term SExpr)
forall a.
Normalizable a =>
(forall i. VarId i -> Normalizer (VarId i))
-> Term a -> Normalizer (Term a)
normalize' VarId i -> Normalizer (VarId i)
forall i. VarId i -> Normalizer (VarId i)
f Term SExpr
car Normalizer (Term SExpr -> LogicSExpr)
-> Normalizer (Term SExpr) -> Normalizer LogicSExpr
forall a b. Normalizer (a -> b) -> Normalizer a -> Normalizer b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall i. VarId i -> Normalizer (VarId i))
-> Term SExpr -> Normalizer (Term SExpr)
forall a.
Normalizable a =>
(forall i. VarId i -> Normalizer (VarId i))
-> Term a -> Normalizer (Term a)
normalize' VarId i -> Normalizer (VarId i)
forall i. VarId i -> Normalizer (VarId i)
f Term SExpr
cdr

deriving instance NFData LogicSExpr

instance Show LogicSExpr where
  show :: LogicSExpr -> [Char]
show (LogicSSymbol (Value (Atomic [Char]
symbol))) = [Char]
symbol
  show (LogicSSymbol Term Symbol
var) = Term Symbol -> [Char]
forall a. Show a => a -> [Char]
show Term Symbol
var
  show LogicSExpr
LogicSNil = [Char]
"()"
  show (LogicSCons Term SExpr
car Term SExpr
cdr) = [Char]
"(" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term SExpr -> [Char]
forall a. Show a => a -> [Char]
show Term SExpr
car [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term SExpr -> [Char]
showLogicSList Term SExpr
cdr

instance Show LogicValue where
  show :: LogicValue -> [Char]
show (LogicSExpr Term SExpr
expr) = Term SExpr -> [Char]
forall a. Show a => a -> [Char]
show Term SExpr
expr
  show (LogicClosure Term Symbol
var Term SExpr
body Term [(Symbol, Value)]
env) =
    [Char]
"#(lambda (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term Symbol -> [Char]
forall a. Show a => a -> [Char]
show Term Symbol
var [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term SExpr -> [Char]
forall a. Show a => a -> [Char]
show Term SExpr
body [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term [(Symbol, Value)] -> [Char]
forall a. Show a => a -> [Char]
show Term [(Symbol, Value)]
env [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"

showLogicSList :: Term SExpr -> [Char]
showLogicSList :: Term SExpr -> [Char]
showLogicSList (Value Logic SExpr
LogicSExpr
LogicSNil) = [Char]
")"
showLogicSList (Value (LogicSCons Term SExpr
car Term SExpr
cdr)) = [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term SExpr -> [Char]
forall a. Show a => a -> [Char]
show Term SExpr
car [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term SExpr -> [Char]
showLogicSList Term SExpr
cdr
showLogicSList Term SExpr
other = [Char]
" . " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term SExpr -> [Char]
forall a. Show a => a -> [Char]
show Term SExpr
other [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"

applyo :: Term SExpr -> Term SExpr -> Term SExpr -> Goal ()
applyo :: Term SExpr -> Term SExpr -> Term SExpr -> Goal ()
applyo Term SExpr
f Term SExpr
x Term SExpr
expr = Term SExpr
expr Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons Term SExpr
f (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons Term SExpr
x (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value Logic SExpr
LogicSExpr
LogicSNil))))

lambda :: Term Symbol
lambda :: Term Symbol
lambda = Symbol -> Term Symbol
forall a. Logical a => a -> Term a
inject' ([Char] -> Symbol
forall a. a -> Atomic a
Atomic [Char]
"lambda")

quote :: Term Symbol
quote :: Term Symbol
quote = Symbol -> Term Symbol
forall a. Logical a => a -> Term a
inject' ([Char] -> Symbol
forall a. a -> Atomic a
Atomic [Char]
"quote")

list :: Term Symbol
list :: Term Symbol
list = Symbol -> Term Symbol
forall a. Logical a => a -> Term a
inject' ([Char] -> Symbol
forall a. a -> Atomic a
Atomic [Char]
"list")

lambdao :: Term Symbol -> Term SExpr -> Term SExpr -> Goal ()
lambdao :: Term Symbol -> Term SExpr -> Term SExpr -> Goal ()
lambdao Term Symbol
x Term SExpr
body Term SExpr
expr =
  Term SExpr
expr
    Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value
      ( Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons
          (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term Symbol -> LogicSExpr
LogicSSymbol Term Symbol
lambda))
          ( Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value
              ( Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons
                  Term SExpr
parameter
                  (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons Term SExpr
body (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value Logic SExpr
LogicSExpr
LogicSNil)))
              )
          )
      )
 where
  parameter :: Term SExpr
parameter = Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term Symbol -> LogicSExpr
LogicSSymbol Term Symbol
x)) (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value Logic SExpr
LogicSExpr
LogicSNil))

quoteo :: Term SExpr -> Term SExpr -> Goal ()
quoteo :: Term SExpr -> Term SExpr -> Goal ()
quoteo Term SExpr
value Term SExpr
expr =
  Term SExpr
expr
    Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value
      ( Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons
          (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term Symbol -> LogicSExpr
LogicSSymbol Term Symbol
quote))
          (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons Term SExpr
value (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value Logic SExpr
LogicSExpr
LogicSNil)))
      )

listo :: Term SExpr -> Term SExpr -> Goal ()
listo :: Term SExpr -> Term SExpr -> Goal ()
listo Term SExpr
exprs Term SExpr
expr =
  Term SExpr
expr Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons (Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term Symbol -> LogicSExpr
LogicSSymbol Term Symbol
list)) Term SExpr
exprs)

lookupo :: Term Symbol -> Term Env -> Term Value -> Goal ()
lookupo :: Term Symbol -> Term [(Symbol, Value)] -> Term Value -> Goal ()
lookupo Term Symbol
expectedVar Term [(Symbol, Value)]
env Term Value
returnValue = do
  (Term Symbol
var, Term Value
value, Term [(Symbol, Value)]
rest) <- Goal (Term Symbol, Term Value, Term [(Symbol, Value)])
forall v. Fresh v => Goal v
fresh
  Term [(Symbol, Value)]
env Term [(Symbol, Value)] -> Term [(Symbol, Value)] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [(Symbol, Value)] -> Term [(Symbol, Value)]
forall a. Logic a -> Term a
Value (Term (Symbol, Value)
-> Term [(Symbol, Value)] -> LogicList (Symbol, Value)
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic (Symbol, Value) -> Term (Symbol, Value)
forall a. Logic a -> Term a
Value (Term Symbol
var, Term Value
value)) Term [(Symbol, Value)]
rest)
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term Symbol
var Term Symbol -> Term Symbol -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Symbol
expectedVar
        Term Value
value Term Value -> Term Value -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Value
returnValue
    , do
        Term Symbol
var Term Symbol -> Term Symbol -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=/= Term Symbol
expectedVar
        Term Symbol -> Term [(Symbol, Value)] -> Term Value -> Goal ()
lookupo Term Symbol
expectedVar Term [(Symbol, Value)]
rest Term Value
returnValue
    ]

notInEnvo :: Term Symbol -> Term Env -> Goal ()
notInEnvo :: Term Symbol -> Term [(Symbol, Value)] -> Goal ()
notInEnvo Term Symbol
var Term [(Symbol, Value)]
env =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        (Term Symbol
entryVar, Term Value
value, Term [(Symbol, Value)]
rest) <- Goal (Term Symbol, Term Value, Term [(Symbol, Value)])
forall v. Fresh v => Goal v
fresh
        Term [(Symbol, Value)]
env Term [(Symbol, Value)] -> Term [(Symbol, Value)] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [(Symbol, Value)] -> Term [(Symbol, Value)]
forall a. Logic a -> Term a
Value (Term (Symbol, Value)
-> Term [(Symbol, Value)] -> LogicList (Symbol, Value)
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic (Symbol, Value) -> Term (Symbol, Value)
forall a. Logic a -> Term a
Value (Term Symbol
entryVar, Term Value
value)) Term [(Symbol, Value)]
rest)
        Term Symbol
entryVar Term Symbol -> Term Symbol -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=/= Term Symbol
var
        Term Symbol -> Term [(Symbol, Value)] -> Goal ()
notInEnvo Term Symbol
var Term [(Symbol, Value)]
rest
    , do
        Term [(Symbol, Value)]
env Term [(Symbol, Value)] -> Term [(Symbol, Value)] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [(Symbol, Value)] -> Term [(Symbol, Value)]
forall a. Logical a => a -> Term a
inject' []
    ]

properListo :: Term SExpr -> Term Env -> Term SExpr -> Goal ()
properListo :: Term SExpr -> Term [(Symbol, Value)] -> Term SExpr -> Goal ()
properListo Term SExpr
exprs Term [(Symbol, Value)]
env Term SExpr
value =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term SExpr
exprs Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== SExpr -> Term SExpr
forall a. Logical a => a -> Term a
inject' []
        Term SExpr
value Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== SExpr -> Term SExpr
forall a. Logical a => a -> Term a
inject' []
    , do
        (Term SExpr
car, Term SExpr
cdr, Term SExpr
car', Term SExpr
cdr') <- Goal (Term SExpr, Term SExpr, Term SExpr, Term SExpr)
forall v. Fresh v => Goal v
fresh
        Term SExpr
exprs Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons Term SExpr
car Term SExpr
cdr)
        Term SExpr
value Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term SExpr -> Term SExpr -> LogicSExpr
LogicSCons Term SExpr
car' Term SExpr
cdr')
        Term SExpr -> Term [(Symbol, Value)] -> Term Value -> Goal ()
evalo Term SExpr
car Term [(Symbol, Value)]
env (Logic Value -> Term Value
forall a. Logic a -> Term a
Value (Term SExpr -> LogicValue
LogicSExpr Term SExpr
car'))
        Term SExpr -> Term [(Symbol, Value)] -> Term SExpr -> Goal ()
properListo Term SExpr
cdr Term [(Symbol, Value)]
env Term SExpr
cdr'
    ]

evalo :: Term SExpr -> Term Env -> Term Value -> Goal ()
evalo :: Term SExpr -> Term [(Symbol, Value)] -> Term Value -> Goal ()
evalo Term SExpr
expr Term [(Symbol, Value)]
env Term Value
value =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term SExpr
arg <- Goal (Term SExpr)
forall v. Fresh v => Goal v
fresh
        Term SExpr -> Term SExpr -> Goal ()
quoteo Term SExpr
arg Term SExpr
expr
        Term Symbol -> Term [(Symbol, Value)] -> Goal ()
notInEnvo Term Symbol
quote Term [(Symbol, Value)]
env
        Term Value
value Term Value -> Term Value -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Value -> Term Value
forall a. Logic a -> Term a
Value (Term SExpr -> LogicValue
LogicSExpr Term SExpr
arg)
    , do
        (Term SExpr
exprs, Term SExpr
value') <- Goal (Term SExpr, Term SExpr)
forall v. Fresh v => Goal v
fresh
        Term SExpr -> Term SExpr -> Goal ()
listo Term SExpr
exprs Term SExpr
expr
        Term Value
value Term Value -> Term Value -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Value -> Term Value
forall a. Logic a -> Term a
Value (Term SExpr -> LogicValue
LogicSExpr Term SExpr
value')
        Term SExpr -> Term [(Symbol, Value)] -> Term SExpr -> Goal ()
properListo Term SExpr
exprs Term [(Symbol, Value)]
env Term SExpr
value'
    , do
        Term Symbol
x <- Goal (Term Symbol)
forall v. Fresh v => Goal v
fresh
        Term SExpr
expr Term SExpr -> Term SExpr -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic SExpr -> Term SExpr
forall a. Logic a -> Term a
Value (Term Symbol -> LogicSExpr
LogicSSymbol Term Symbol
x)
        Term Symbol -> Term [(Symbol, Value)] -> Term Value -> Goal ()
lookupo Term Symbol
x Term [(Symbol, Value)]
env Term Value
value
    , do
        (Term SExpr
rator, Term SExpr
rand, Term Symbol
x, Term SExpr
body, Term [(Symbol, Value)]
ratorEnv, Term Value
rand') <- Goal
  (Term SExpr, Term SExpr, Term Symbol, Term SExpr,
   Term [(Symbol, Value)], Term Value)
forall v. Fresh v => Goal v
fresh
        Term SExpr -> Term SExpr -> Term SExpr -> Goal ()
applyo Term SExpr
rator Term SExpr
rand Term SExpr
expr
        Term SExpr -> Term [(Symbol, Value)] -> Term Value -> Goal ()
evalo Term SExpr
rator Term [(Symbol, Value)]
env (Logic Value -> Term Value
forall a. Logic a -> Term a
Value (Term Symbol -> Term SExpr -> Term [(Symbol, Value)] -> LogicValue
LogicClosure Term Symbol
x Term SExpr
body Term [(Symbol, Value)]
ratorEnv))
        Term SExpr -> Term [(Symbol, Value)] -> Term Value -> Goal ()
evalo Term SExpr
rand Term [(Symbol, Value)]
env Term Value
rand'
        Term SExpr -> Term [(Symbol, Value)] -> Term Value -> Goal ()
evalo Term SExpr
body (Logic [(Symbol, Value)] -> Term [(Symbol, Value)]
forall a. Logic a -> Term a
Value (Term (Symbol, Value)
-> Term [(Symbol, Value)] -> LogicList (Symbol, Value)
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic (Symbol, Value) -> Term (Symbol, Value)
forall a. Logic a -> Term a
Value (Term Symbol
x, Term Value
rand')) Term [(Symbol, Value)]
ratorEnv)) Term Value
value
    , do
        (Term Symbol
x, Term SExpr
body) <- Goal (Term Symbol, Term SExpr)
forall v. Fresh v => Goal v
fresh
        Term Symbol -> Term SExpr -> Term SExpr -> Goal ()
lambdao Term Symbol
x Term SExpr
body Term SExpr
expr
        Term Value
value Term Value -> Term Value -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Value -> Term Value
forall a. Logic a -> Term a
Value (Term Symbol -> Term SExpr -> Term [(Symbol, Value)] -> LogicValue
LogicClosure Term Symbol
x Term SExpr
body Term [(Symbol, Value)]
env)
        Term Symbol -> Term [(Symbol, Value)] -> Goal ()
notInEnvo Term Symbol
lambda Term [(Symbol, Value)]
env
    ]