{-# LANGUAGE OverloadedStrings, LambdaCase #-}

-- |
-- This module implements HGMPification of funcons based on Berger et al. (2017)
-- (First-order.)
module Funcons.MetaProgramming where

import Funcons.MSOS
import Funcons.EDSL
import Funcons.Types
import Funcons.Patterns
import Funcons.RunOptions
import Funcons.Simulation

import Data.Maybe (fromJust)
import Data.Text (pack, unpack)
import qualified Data.Map as M
import qualified Data.Set as S

-- | This function implements the ==CT=> relation.
-- Compiling programs to executable funcons terms,
-- removing occurrences of `meta-up`, `meta-down` and `meta-let` and `meta-bound`.
ctRel :: Funcons -> MSOS Funcons
ctRel :: Funcons -> MSOS Funcons
ctRel Funcons
f = case Funcons
f of
  FName Name
nm                        -> Funcons -> MSOS Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return Funcons
f 
  FApp Name
"meta-up" [Funcons
m]              -> Funcons -> MSOS Funcons
ulRel Funcons
m
  FApp Name
"meta-down" [Funcons
m]            -> Funcons -> MSOS Funcons
staticEval Funcons
m
  FApp Name
"meta-let" [FValue Values
nm,Funcons
m,Funcons
n] | Values -> Bool
forall t. HasValues t => Values t -> Bool
isString_ Values
nm -> do 
    Values
v <- Funcons -> MSOS Values
evalRel (Funcons -> MSOS Values) -> MSOS Funcons -> MSOS Values
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Funcons -> MSOS Funcons
ctRel Funcons
m
    [Values
menv] <- Name -> MSOS [Values]
getInh Name
env_entity 
    let env' :: Values
env' = case Values
menv of 
                Map ValueMaps Values
env -> ValueMaps Values -> Values
forall t. ValueMaps (Values t) -> Values t
Map (Values -> [Values] -> ValueMaps Values -> ValueMaps Values
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Values
nm [Values
v] ValueMaps Values
env)
                Values
_       -> ValueMaps Values -> Values
forall t. ValueMaps (Values t) -> Values t
Map (Values -> [Values] -> ValueMaps Values
forall k a. k -> a -> Map k a
M.singleton Values
nm [Values
v])
    Name -> [Values] -> MSOS Funcons -> MSOS Funcons
forall a. Name -> [Values] -> MSOS a -> MSOS a
withInh Name
env_entity [Values
env'] (Funcons -> MSOS Funcons
ctRel Funcons
n)
  FApp Name
nm [Funcons]
arg                     -> Name -> [Funcons] -> Funcons
FApp Name
nm ([Funcons] -> Funcons) -> MSOS [Funcons] -> MSOS Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> MSOS Funcons) -> [Funcons] -> MSOS [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> MSOS Funcons
ctRel [Funcons]
arg
--  FList fs                        -> FList <$> mapM ctRel fs
  FSet [Funcons]
fs                         -> [Funcons] -> Funcons
FSet ([Funcons] -> Funcons) -> MSOS [Funcons] -> MSOS Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> MSOS Funcons) -> [Funcons] -> MSOS [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> MSOS Funcons
ctRel [Funcons]
fs
  FMap [Funcons]
fs                         -> [Funcons] -> Funcons
FMap ([Funcons] -> Funcons) -> MSOS [Funcons] -> MSOS Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> MSOS Funcons) -> [Funcons] -> MSOS [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> MSOS Funcons
ctRel [Funcons]
fs
  FValue (ADTVal Name
nm [Funcons]
fs)           -> Values -> Funcons
FValue (Values -> Funcons)
-> ([Funcons] -> Values) -> [Funcons] -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
nm ([Funcons] -> Funcons) -> MSOS [Funcons] -> MSOS Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> MSOS Funcons) -> [Funcons] -> MSOS [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> MSOS Funcons
ctRel [Funcons]
fs
  FValue (ComputationType (Type (ADT Name
nm [Funcons]
fs)))
                                  -> Values -> Funcons
FValue (Values -> Funcons)
-> ([Funcons] -> Values) -> [Funcons] -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComputationTypes Funcons -> Values
forall t. ComputationTypes t -> Values t
ComputationType (ComputationTypes Funcons -> Values)
-> ([Funcons] -> ComputationTypes Funcons) -> [Funcons] -> Values
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Types Funcons -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
Type (Types Funcons -> ComputationTypes Funcons)
-> ([Funcons] -> Types Funcons)
-> [Funcons]
-> ComputationTypes Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Funcons] -> Types Funcons
forall t. Name -> [t] -> Types t
ADT Name
nm ([Funcons] -> Funcons) -> MSOS [Funcons] -> MSOS Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> MSOS Funcons) -> [Funcons] -> MSOS [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> MSOS Funcons
ctRel [Funcons]
fs
  FValue Values
v                        -> Funcons -> MSOS Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (Values -> Funcons
FValue Values
v)
  Funcons
_                               -> Rewrite Funcons -> MSOS Funcons
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> String -> Rewrite Funcons
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f (String
"ctRel not defined"))
  where staticEval :: Funcons -> MSOS Funcons
staticEval Funcons
m = Funcons -> MSOS Funcons
ctRel Funcons
m MSOS Funcons -> (Funcons -> MSOS Values) -> MSOS Values
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Funcons -> MSOS Values
evalRel MSOS Values -> (Values -> MSOS Funcons) -> MSOS Funcons
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rewrite Funcons -> MSOS Funcons
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Funcons -> MSOS Funcons)
-> (Values -> Rewrite Funcons) -> Values -> MSOS Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Values -> Rewrite Funcons
dlRel  

-- | This function implements the ==UL=> relation.
-- Translating a funcon into its meta-representation
ulRel :: Funcons -> MSOS Funcons
ulRel :: Funcons -> MSOS Funcons
ulRel Funcons
f = case Funcons
f of
  FName Name
nm              -> Funcons -> MSOS Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (Funcons -> MSOS Funcons) -> Funcons -> MSOS Funcons
forall a b. (a -> b) -> a -> b
$ [Funcons] -> Funcons
ast_term [String -> Funcons
string_ (Name -> String
unpack Name
nm)]
  FApp Name
"meta-down" [Funcons
f]  -> Funcons -> MSOS Funcons
ctRel Funcons
f
  FApp Name
"meta-up" [Funcons
m]    -> Funcons -> MSOS Funcons
ulRel Funcons
m MSOS Funcons -> (Funcons -> MSOS Funcons) -> MSOS Funcons
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Funcons -> MSOS Funcons
ulRel
  FApp Name
nm [Funcons]
fs            -> [Funcons] -> Funcons
ast_term ([Funcons] -> Funcons)
-> ([Funcons] -> [Funcons]) -> [Funcons] -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Funcons
string_ (Name -> String
unpack Name
nm)Funcons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:) ([Funcons] -> Funcons) -> MSOS [Funcons] -> MSOS Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> MSOS Funcons) -> [Funcons] -> MSOS [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> MSOS Funcons
ulRel [Funcons]
fs
--  FList fs              -> ast_term . (string_ "list":) <$> mapM ulRel fs
  FSet [Funcons]
fs               -> [Funcons] -> Funcons
ast_term ([Funcons] -> Funcons)
-> ([Funcons] -> [Funcons]) -> [Funcons] -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Funcons
string_ String
"set"Funcons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:) ([Funcons] -> Funcons) -> MSOS [Funcons] -> MSOS Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> MSOS Funcons) -> [Funcons] -> MSOS [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> MSOS Funcons
ulRel [Funcons]
fs
  FMap [Funcons]
fs               -> [Funcons] -> Funcons
ast_term ([Funcons] -> Funcons)
-> ([Funcons] -> [Funcons]) -> [Funcons] -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Funcons
string_ String
"map"Funcons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:) ([Funcons] -> Funcons) -> MSOS [Funcons] -> MSOS Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> MSOS Funcons) -> [Funcons] -> MSOS [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> MSOS Funcons
ulRel [Funcons]
fs
  FValue Values
v              -> Funcons -> MSOS Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (Funcons -> MSOS Funcons) -> Funcons -> MSOS Funcons
forall a b. (a -> b) -> a -> b
$ [Funcons] -> Funcons
ast_value [Types Funcons -> Funcons
type_ (Values -> Types Funcons
forall t. HasValues t => Values t -> Types t
tyOf Values
v), Values -> Funcons
FValue Values
v]
  -- What TODO with type annotations? 
  Funcons
_                     -> Rewrite Funcons -> MSOS Funcons
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> String -> Rewrite Funcons
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f (String
"ulRel not defined"))

-- | This function implements the ==DL=> relation.
-- Translating a meta-representation of a program into the actual program
dlRel :: Values -> Rewrite Funcons
dlRel :: Values -> Rewrite Funcons
dlRel Values
v = case Values
v of 
  ADTVal Name
"ast-value" [Funcons
t,Funcons
v] | Just (ComputationType ComputationTypes Funcons
_) <- Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project Funcons
t -> Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return Funcons
v
  ADTVal Name
"ast-term" [Funcons
nm] | Funcons -> Bool
isString Funcons
nm -> Funcons -> Rewrite Funcons
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Funcons
FName (String -> Name
pack (Values -> String
forall t. HasValues t => Values t -> String
unString (Maybe Values -> Values
forall a. HasCallStack => Maybe a -> a
fromJust (Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project Funcons
nm)))))
  ADTVal Name
"ast-term" (Funcons
s:[Funcons]
vs')
    | Just [Values]
vs <- (Funcons -> Maybe Values) -> [Funcons] -> Maybe [Values]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
vs' 
    , Funcons -> Bool
isString Funcons
s, String
"set" <- Values -> String
forall t. HasValues t => Values t -> String
unString (Maybe Values -> Values
forall a. HasCallStack => Maybe a -> a
fromJust (Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project Funcons
s)) -> [Funcons] -> Funcons
FSet ([Funcons] -> Funcons) -> Rewrite [Funcons] -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Values -> Rewrite Funcons) -> [Values] -> Rewrite [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values -> Rewrite Funcons
dlRel [Values]
vs
  ADTVal Name
"ast-term" (Funcons
m:[Funcons]
vs')
    | Just [Values]
vs <- (Funcons -> Maybe Values) -> [Funcons] -> Maybe [Values]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
vs' 
    , Funcons -> Bool
isString Funcons
m, String
"map" <- Values -> String
forall t. HasValues t => Values t -> String
unString (Maybe Values -> Values
forall a. HasCallStack => Maybe a -> a
fromJust (Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project Funcons
m)) -> [Funcons] -> Funcons
FMap ([Funcons] -> Funcons) -> Rewrite [Funcons] -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Values -> Rewrite Funcons) -> [Values] -> Rewrite [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values -> Rewrite Funcons
dlRel [Values]
vs
  ADTVal Name
"ast-term" (Funcons
nm:[Funcons]
vs')       
    | Just [Values]
vs <- (Funcons -> Maybe Values) -> [Funcons] -> Maybe [Values]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
vs' 
    , Funcons -> Bool
isString Funcons
nm -> Name -> [Funcons] -> Funcons
FApp (String -> Name
pack (Values -> String
forall t. HasValues t => Values t -> String
unString (Maybe Values -> Values
forall a. HasCallStack => Maybe a -> a
fromJust (Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project Funcons
nm)))) ([Funcons] -> Funcons) -> Rewrite [Funcons] -> Rewrite Funcons
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 
                      (Values -> Rewrite Funcons) -> [Values] -> Rewrite [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values -> Rewrite Funcons
dlRel [Values]
vs
  Values
_ -> Funcons -> String -> Rewrite Funcons
forall a. Funcons -> String -> Rewrite a
sortErr ([Funcons] -> Funcons
meta_down_ ([Values] -> [Funcons]
fvalues [Values
v])) String
"meta-down not applied to a meta-representation"

evalRel :: Funcons -> MSOS Values
evalRel :: Funcons -> MSOS Values
evalRel Funcons
f = Funcons -> MSOS StepRes
evalFuncons Funcons
f MSOS StepRes -> (StepRes -> MSOS Values) -> MSOS Values
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
  Right [Values
v]   -> Values -> MSOS Values
forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
  Right [Values]
vs    -> Rewrite Values -> MSOS Values
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Values -> MSOS Values) -> Rewrite Values -> MSOS Values
forall a b. (a -> b) -> a -> b
$ String -> Rewrite Values
forall a. String -> Rewrite a
internal String
"meta evaluation yields a sequence of values"
  Left Funcons
f'     -> Funcons -> MSOS Values
evalRel Funcons
f'
  where setGlobal :: Funcons -> MSOSReader m -> MSOSReader m
setGlobal Funcons
f MSOSReader m
ctxt = MSOSReader m
ctxt { ereader :: RewriteReader
ereader = (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) { global_fct :: Funcons
global_fct = Funcons
f } }

compile :: FunconLibrary -> TypeRelation -> Funcons -> Funcons -> Funcons
compile :: FunconLibrary -> TypeRelation -> Funcons -> Funcons -> Funcons
compile FunconLibrary
lib TypeRelation
tyenv Funcons
fenv Funcons
f = 
  case SimIO
  (Either IException Funcons,
   MSOSState (StateT InputValues Identity), MSOSWriter)
-> InputValues
-> ((Either IException Funcons,
     MSOSState (StateT InputValues Identity), MSOSWriter),
    InputValues)
forall a. SimIO a -> InputValues -> (a, InputValues)
runSimIO (MSOS Funcons
-> MSOSReader (StateT InputValues Identity)
-> MSOSState (StateT InputValues Identity)
-> SimIO
     (Either IException Funcons,
      MSOSState (StateT InputValues Identity), MSOSWriter)
forall a.
MSOS a
-> forall (m :: * -> *).
   Interactive m =>
   MSOSReader m
   -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS MSOS Funcons
process (FunconLibrary
-> TypeRelation
-> Funcons
-> MSOSReader (StateT InputValues Identity)
forall (m :: * -> *).
Interactive m =>
FunconLibrary -> TypeRelation -> Funcons -> MSOSReader m
cmp_MSOSReader FunconLibrary
lib TypeRelation
tyenv Funcons
f) MSOSState (StateT InputValues Identity)
forall (m :: * -> *). MSOSState m
cmp_MSOSState) InputValues
forall k a. Map k a
M.empty of
    ((Left IException
ie , MSOSState (StateT InputValues Identity)
_,MSOSWriter
_), InputValues
_) -> String -> Funcons
forall a. HasCallStack => String -> a
error (String
"failed to compile\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ IException -> String
showIException IException
ie)
    ((Right Funcons
f, MSOSState (StateT InputValues Identity)
_, MSOSWriter
_), InputValues
_) -> Funcons
f  
  where process :: MSOS Funcons
process = do  
          Values
env <- Funcons -> MSOS Values
evalRel Funcons
fenv
          Name -> Values -> MSOS ()
putMut Name
atom_gen_entity (ValueSets Values -> Values
forall t. ValueSets (Values t) -> Values t
Set ValueSets Values
forall a. Set a
S.empty)
          Name -> Values -> MSOS ()
putMut Name
store_entity (ValueMaps Values -> Values
forall t. ValueMaps (Values t) -> Values t
Map ValueMaps Values
forall k a. Map k a
M.empty)
          Name -> [Values] -> MSOS Funcons -> MSOS Funcons
forall a. Name -> [Values] -> MSOS a -> MSOS a
withInh Name
env_entity [Values
env] (Funcons -> MSOS Funcons
ctRel Funcons
f)

env_entity :: Name
env_entity = Name
"environment"
store_entity :: Name
store_entity = Name
"store"
atom_gen_entity :: Name
atom_gen_entity = Name
"used-atom-set"
 
translationStep :: ([Funcons] -> Funcons) -> StrictFuncon
translationStep :: ([Funcons] -> Funcons) -> StrictFuncon
translationStep [Funcons] -> Funcons
f [Values]
vs = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> MSOS StepRes -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ do  [Funcons]
fs <- Rewrite [Funcons] -> MSOS [Funcons]
forall a. Rewrite a -> MSOS a
liftRewrite ((Values -> Rewrite Funcons) -> [Values] -> Rewrite [Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values -> Rewrite Funcons
dlRel [Values]
vs)
                                      Funcons -> StepRes
forall a b. a -> Either a b
Left (Funcons -> StepRes) -> MSOS Funcons -> MSOS StepRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Funcons -> MSOS Funcons
ulRel ([Funcons] -> Funcons
f [Funcons]
fs)

cmp_MSOSReader :: FunconLibrary -> TypeRelation -> Funcons -> MSOSReader m
cmp_MSOSReader FunconLibrary
lib TypeRelation
env Funcons
f = RewriteReader
-> InputValues
-> DownControl
-> (Name -> m Funcons)
-> MSOSReader m
forall (m :: * -> *).
RewriteReader
-> InputValues
-> DownControl
-> (Name -> m Funcons)
-> MSOSReader m
MSOSReader RewriteReader
cmp_RewriteReader InputValues
forall k a. Map k a
M.empty DownControl
forall k a. Map k a
M.empty (Bool -> Name -> m Funcons
forall (m :: * -> *). Interactive m => Bool -> Name -> m Funcons
fread Bool
True)
  where cmp_RewriteReader :: RewriteReader
cmp_RewriteReader = FunconLibrary
-> TypeRelation
-> RunOptions
-> Funcons
-> Funcons
-> RewriteReader
RewriteReader FunconLibrary
lib TypeRelation
env RunOptions
defaultRunOptions Funcons
f Funcons
f  
--cmp_MSOSWriter = MSOSWriter mempty mempty mempty
cmp_MSOSState :: MSOSState m
cmp_MSOSState = Input m -> Mutable -> RewriteState -> MSOSState m
forall (m :: * -> *).
Input m -> Mutable -> RewriteState -> MSOSState m
MSOSState Input m
forall k a. Map k a
M.empty Mutable
forall k a. Map k a
M.empty (RewriteState
RewriteState)

library :: FunconLibrary
library :: FunconLibrary
library = [(Name, EvalFunction)] -> FunconLibrary
libFromList [
--    ("meta-up", NonStrictFuncon step_meta_up)  -- static funcon
--  , ("meta-down", StrictFuncon step_meta_down) -- static funcon
    (Name
"eval", StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
step_meta_eval)
  , (Name
"code", NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
step_code)
  , (Name
"type-of", StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
step_ty_of)
  ]

meta_up_ :: [Funcons] -> Funcons
meta_up_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"meta-up"
meta_down_ :: [Funcons] -> Funcons
meta_down_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"meta-down"
meta_let_ :: [Funcons] -> Funcons
meta_let_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"meta-let"

eval_ :: [Funcons] -> Funcons
eval_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"eval"
code_ :: [Funcons] -> Funcons
code_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"code"
step_meta_eval :: [Values] -> Rewrite Rewritten
step_meta_eval :: StrictFuncon
step_meta_eval [Values
v] = Values -> Rewrite Funcons
dlRel Values
v Rewrite Funcons
-> (Funcons -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Funcons -> Rewrite Rewritten
rewriteTo
step_meta_eval [Values]
fs = Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr ([Funcons] -> Funcons
eval_ ([Values] -> [Funcons]
fvalues [Values]
fs)) String
"eval not applied to one argument"

step_code :: [Funcons] -> Rewrite Rewritten
step_code :: NonStrictFuncon
step_code [Funcons
f] = MSOS StepRes -> Rewrite Rewritten
compstep (Funcons -> StepRes
toStepRes (Funcons -> StepRes) -> MSOS Funcons -> MSOS StepRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Funcons -> MSOS Funcons
ulRel Funcons
f)
step_code [Funcons]
fs = Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr ([Funcons] -> Funcons
code_ [Funcons]
fs) String
"code not applied to a single term"

ast_term :: [Funcons] -> Funcons
ast_term = Name -> [Funcons] -> Funcons
applyFuncon Name
"ast-term"
ast_value :: [Funcons] -> Funcons
ast_value = Name -> [Funcons] -> Funcons
applyFuncon Name
"ast-value"

type_of_ :: [Funcons] -> Funcons
type_of_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"type-of"
step_ty_of :: [Values] -> Rewrite Rewritten
step_ty_of :: StrictFuncon
step_ty_of [Values
v] = Funcons -> Rewrite Rewritten
rewriteTo (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types Funcons -> Funcons
type_ (Types Funcons -> Funcons) -> Types Funcons -> Funcons
forall a b. (a -> b) -> a -> b
$ Values -> Types Funcons
forall t. HasValues t => Values t -> Types t
tyOf Values
v
step_ty_of [Values]
vs = Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr ([Funcons] -> Funcons
type_of_ ([Values] -> [Funcons]
fvalues [Values]
vs)) String
"type-of not applied to a single value"

--TODO perhaps the parser should be extended to recognise "ast-" prefixes
-- which are translated into applications of VMeta