{-# 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                        -> 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] | forall t. HasValues t => Values t -> Bool
isString_ Values
nm -> do 
    Values
v <- Funcons -> MSOS Values
evalRel 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 -> forall t. ValueMaps (Values t) -> Values t
Map (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Values
nm [Values
v] ValueMaps Values
env)
                Values
_       -> forall t. ValueMaps (Values t) -> Values t
Map (forall k a. k -> a -> Map k a
M.singleton Values
nm [Values
v])
    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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Name -> [t] -> Values t
ADTVal Name
nm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. ComputationTypes t -> Values t
ComputationType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Types t -> ComputationTypes t
Type forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Name -> [t] -> Types t
ADT Name
nm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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                        -> forall (m :: * -> *) a. Monad m => a -> m a
return (Values -> Funcons
FValue Values
v)
  Funcons
_                               -> forall a. Rewrite a -> MSOS a
liftRewrite (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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Funcons -> MSOS Values
evalRel forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Rewrite a -> MSOS a
liftRewrite 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              -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Funcons
string_ (Name -> String
unpack Name
nm)forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Funcons
string_ String
"set"forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Funcons
string_ String
"map"forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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              -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Funcons] -> Funcons
ast_value [Types Funcons -> Funcons
type_ (forall t. HasValues t => Values t -> Types t
tyOf Values
v), Values -> Funcons
FValue Values
v]
  -- What TODO with type annotations? 
  Funcons
_                     -> forall a. Rewrite a -> MSOS a
liftRewrite (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
_) <- forall t. HasValues t => t -> Maybe (Values t)
project Funcons
t -> forall (m :: * -> *) a. Monad m => a -> m a
return Funcons
v
  ADTVal Name
"ast-term" [Funcons
nm] | Funcons -> Bool
isString Funcons
nm -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Funcons
FName (String -> Name
pack (forall t. HasValues t => Values t -> String
unString (forall a. HasCallStack => Maybe a -> a
fromJust (forall t. HasValues t => t -> Maybe (Values t)
project Funcons
nm)))))
  ADTVal Name
"ast-term" (Funcons
s:[Funcons]
vs')
    | Just [Values]
vs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
vs' 
    , Funcons -> Bool
isString Funcons
s, String
"set" <- forall t. HasValues t => Values t -> String
unString (forall a. HasCallStack => Maybe a -> a
fromJust (forall t. HasValues t => t -> Maybe (Values t)
project Funcons
s)) -> [Funcons] -> Funcons
FSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
vs' 
    , Funcons -> Bool
isString Funcons
m, String
"map" <- forall t. HasValues t => Values t -> String
unString (forall a. HasCallStack => Maybe a -> a
fromJust (forall t. HasValues t => t -> Maybe (Values t)
project Funcons
m)) -> [Funcons] -> Funcons
FMap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
vs' 
    , Funcons -> Bool
isString Funcons
nm -> Name -> [Funcons] -> Funcons
FApp (String -> Name
pack (forall t. HasValues t => Values t -> String
unString (forall a. HasCallStack => Maybe a -> a
fromJust (forall t. HasValues t => t -> Maybe (Values t)
project Funcons
nm)))) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 
                      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
_ -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
  Right [Values
v]   -> forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
  Right [Values]
vs    -> forall a. Rewrite a -> MSOS a
liftRewrite forall a b. (a -> b) -> a -> b
$ 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 = (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 forall a. SimIO a -> InputValues -> (a, InputValues)
runSimIO (forall a.
MSOS a
-> forall (m :: * -> *).
   Interactive m =>
   MSOSReader m
   -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS MSOS Funcons
process (forall {m :: * -> *}.
Interactive m =>
FunconLibrary -> TypeRelation -> Funcons -> MSOSReader m
cmp_MSOSReader FunconLibrary
lib TypeRelation
tyenv Funcons
f) forall {m :: * -> *}. MSOSState m
cmp_MSOSState) forall k a. Map k a
M.empty of
    ((Left IException
ie , MSOSState (StateT InputValues Identity)
_,MSOSWriter
_), InputValues
_) -> forall a. HasCallStack => String -> a
error (String
"failed to compile\n" 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 [forall t. ValueSets (Values t) -> Values t
Set forall a. Set a
S.empty]
          Name -> [Values] -> MSOS ()
putMut Name
store_entity [forall t. ValueMaps (Values t) -> Values t
Map forall k a. Map k a
M.empty]
          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 forall a b. (a -> b) -> a -> b
$ do  [Funcons]
fs <- forall a. Rewrite a -> MSOS a
liftRewrite (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values -> Rewrite Funcons
dlRel [Values]
vs)
                                      forall a b. a -> Either a b
Left 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 = forall (m :: * -> *).
RewriteReader
-> InputValues
-> DownControl
-> (Name -> m Funcons)
-> MSOSReader m
MSOSReader RewriteReader
cmp_RewriteReader forall k a. Map k a
M.empty forall k a. Map k a
M.empty (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 = forall (m :: * -> *).
Input m -> InputValues -> RewriteState -> MSOSState m
MSOSState forall k a. Map k a
M.empty forall k a. Map k a
M.empty RewriteState
emptyRewriteState

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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Funcons -> Rewrite Rewritten
rewriteTo
step_meta_eval [Values]
fs = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Funcons -> MSOS Funcons
ulRel Funcons
f)
step_code [Funcons]
fs = 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 forall a b. (a -> b) -> a -> b
$ Types Funcons -> Funcons
type_ forall a b. (a -> b) -> a -> b
$ forall t. HasValues t => Values t -> Types t
tyOf Values
v
step_ty_of [Values]
vs = 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