{-# LANGUAGE OverloadedStrings  #-}

-- | 
-- This module provides the types and the functions necessary for defining funcons.
-- The package provides a large collection of predefined funcons in "Funcons.Core".
-- Module "Funcons.Tools" provides functions for creating executables.
module Funcons.EDSL (
    -- * Funcon representation
        Funcons(..), Values(..), Types(..), ComputationTypes(..),SeqSortOp(..),
            applyFuncon,
    -- ** Smart construction of funcon terms
        app0_, app1_, app2_, app3_,
    -- *** Funcon terms
        set_, vec_, env_fromlist_, null__,
    -- *** Values
        int_, bool_, bool__, list__, vector__, tuple__, char_, char__, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_,
    -- *** Types
        values_, integers_, vectors_, type_, ty_star, ty_plus, ty_opt, ty_union, ty_neg, ty_inter, ty_power,
    -- ** Pretty-print funcon terms
        showValues, showValuesSeq, showFuncons, showFunconsSeq, showTypes, showTerms, showOp,
    -- ** Is a funcon term a certain value?
        isVal, isInt, isNat, isList, isMap, isType,
        isVec, isChar, isTup, isString, isString_, unString, 
    -- ** Up and downcasting between funcon terms 
        downcastValue, downcastType, downcastValueType,
        upcastNaturals, upcastIntegers, upcastRationals,upcastCharacter, 
    -- ** Evaluation functions
         EvalFunction(..), Strictness(..), StrictFuncon, PartiallyStrictFuncon, 
              NonStrictFuncon, ValueOp, NullaryFuncon,

    -- *** Funcon libraries
    FunconLibrary, libEmpty, libUnion, libOverride, libUnions, libOverrides, libFromList, Funcons.EDSL.library, fromNullaryValOp, fromValOp, fromSeqValOp,
    -- ** Implicit & modular propagation of entities
    MSOS, Rewrite, Rewritten, 
    -- *** Helpers to create rewrites & step rules
            rewriteTo, rewriteSeqTo, stepTo, stepSeqTo, 
              compstep, rewritten, premiseStep, premiseEval,
                norule, sortErr, partialOp,
    -- *** Entities and entity access
        Inherited, getInh, withInh,
        Mutable, getMut, putMut,
        Output, writeOut, readOut, 
        Control, raiseSignal, receiveSignals, 
        Input, withExtraInput, withExactInput,  
            
    -- * CBS compilation

    -- $cbsintro

    -- ** Funcon representation with meta-variables
        FTerm(..), Env, emptyEnv, fvalues,
    -- *** Defining rules 
        rewriteTermTo,stepTermTo,premise,
    -- *** Entity access
        withInhTerm, getInhPatt, putMutTerm, getMutPatt, writeOutTerm, readOutPatt, 
        receiveSignalPatt, raiseTerm, matchInput, withExtraInputTerms, withExactInputTerms,
        withControlTerm, getControlPatt,
    -- ** Backtracking
        evalRules, stepRules, rewriteRules,
           SideCondition(..), sideCondition,  lifted_sideCondition,
    -- ** Pattern Matching
        VPattern(..), FPattern(..), TPattern(..), 
            vsMatch, fsMatch, f2vPattern,
            lifted_vsMatch, lifted_fsMatch, pat2term, vpat2term, typat2term,
    -- ** Meta-environment
        envRewrite, envStore, lifted_envRewrite, lifted_envStore,
      
    -- * Type substitution
    TypeEnv, TyAssoc(..), HasTypeVar(..), limitedSubsTypeVar, limitedSubsTypeVarWildcard, 
 
    -- * Tools for creating interpreters
  
    -- For more explanation see "Funcons.Tools"
    -- ** Helpers for defining evaluation functions.
        rewriteType,
    -- ** Default entity values
        EntityDefaults, EntityDefault(..),
    -- ** Type environments
        TypeRelation, TypeParam(..), DataTypeMembers(..), DataTypeAltt(..), 
            typeLookup, typeEnvUnion, typeEnvUnions, typeEnvFromList, emptyTypeRelation,
    )where

import Funcons.MSOS
import Funcons.Types
import qualified Funcons.Operations as VAL
import Funcons.Entities
import Funcons.Patterns
import Funcons.Substitution
import Funcons.Printer
import Funcons.TypeSubstitution

import Control.Arrow ((***))

congruence1_1 :: Name -> Funcons -> Rewrite Rewritten
congruence1_1 :: Name -> Funcons -> Rewrite Rewritten
congruence1_1 Name
fnm = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> (Funcons -> MSOS StepRes) -> Funcons -> Rewrite Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp (([Funcons] -> Funcons) -> StepRes -> StepRes
flattenApp [Funcons] -> Funcons
app) 
    where app :: [Funcons] -> Funcons
app = Name -> [Funcons] -> Funcons
applyFuncon Name
fnm

congruence1_2 :: Name -> Funcons -> Funcons -> Rewrite Rewritten
congruence1_2 :: Name -> Funcons -> Funcons -> Rewrite Rewritten
congruence1_2 Name
fnm Funcons
arg1 Funcons
arg2 = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> MSOS StepRes -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp (([Funcons] -> Funcons) -> StepRes -> StepRes
flattenApp [Funcons] -> Funcons
app) Funcons
arg1 
    where app :: [Funcons] -> Funcons
app [Funcons]
fs = Name -> [Funcons] -> Funcons
applyFuncon Name
fnm ([Funcons]
fs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++[Funcons
arg2])

congruence2_2 :: Name -> Funcons -> Funcons -> Rewrite Rewritten
congruence2_2 :: Name -> Funcons -> Funcons -> Rewrite Rewritten
congruence2_2 Name
fnm Funcons
arg1 Funcons
arg2 = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> MSOS StepRes -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp (([Funcons] -> Funcons) -> StepRes -> StepRes
flattenApp [Funcons] -> Funcons
app) Funcons
arg2
    where app :: [Funcons] -> Funcons
app [Funcons]
fs = Name -> [Funcons] -> Funcons
applyFuncon Name
fnm (Funcons
arg1Funcons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:[Funcons]
fs)

congruence1_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence1_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence1_3 Name
fnm Funcons
arg1 Funcons
arg2 Funcons
arg3 = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> MSOS StepRes -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp (([Funcons] -> Funcons) -> StepRes -> StepRes
flattenApp [Funcons] -> Funcons
app) Funcons
arg1 
    where app :: [Funcons] -> Funcons
app [Funcons]
fs = Name -> [Funcons] -> Funcons
applyFuncon Name
fnm ([Funcons]
fs [Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++ [Funcons
arg2, Funcons
arg3])

congruence2_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence2_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence2_3 Name
fnm Funcons
arg1 Funcons
arg2 Funcons
arg3 = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> MSOS StepRes -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp (([Funcons] -> Funcons) -> StepRes -> StepRes
flattenApp [Funcons] -> Funcons
app) Funcons
arg2 
    where app :: [Funcons] -> Funcons
app [Funcons]
fs = Name -> [Funcons] -> Funcons
applyFuncon Name
fnm (Funcons
arg1 Funcons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
: [Funcons]
fs [Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++ [Funcons
arg3])

congruence3_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence3_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence3_3 Name
fnm Funcons
arg1 Funcons
arg2 Funcons
arg3 = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> MSOS StepRes -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp (([Funcons] -> Funcons) -> StepRes -> StepRes
flattenApp [Funcons] -> Funcons
app) Funcons
arg3 
    where app :: [Funcons] -> Funcons
app [Funcons]
fs = Name -> [Funcons] -> Funcons
applyFuncon Name
fnm ([Funcons
arg1, Funcons
arg2] [Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++ [Funcons]
fs)

flattenApp :: ([Funcons] -> Funcons) -> (StepRes -> StepRes) 
flattenApp :: ([Funcons] -> Funcons) -> StepRes -> StepRes
flattenApp [Funcons] -> Funcons
app StepRes
res = case StepRes
res of 
  Left Funcons
f    -> Funcons -> StepRes
toStepRes ([Funcons] -> Funcons
app [Funcons
f])
  Right [Values]
vs  -> Funcons -> StepRes
toStepRes ([Funcons] -> Funcons
app ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs))

-- | Create an environment from a list of bindings (String to Values)
-- This function has been introduced for easy expression of the
-- semantics of builtin identifiers 
env_fromlist_ :: [(String, Funcons)] -> Funcons
env_fromlist_ :: [(String, Funcons)] -> Funcons
env_fromlist_ = [Funcons] -> Funcons
FMap ([Funcons] -> Funcons)
-> ([(String, Funcons)] -> [Funcons])
-> [(String, Funcons)]
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Funcons) -> Funcons) -> [(String, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
k,Funcons
v) -> [Funcons] -> Funcons
tuple_ [String -> Funcons
string_ String
k, Funcons
v])


-- | A funcon library with funcons for builtin types.
library :: FunconLibrary
library :: FunconLibrary
library = [FunconLibrary] -> FunconLibrary
libUnions [FunconLibrary
unLib, FunconLibrary
nullLib, FunconLibrary
binLib, FunconLibrary
floatsLib,FunconLibrary
boundedLib]
 where
        nullLib :: FunconLibrary
nullLib = [(Name, EvalFunction)] -> FunconLibrary
libFromList (((Name, Types) -> (Name, EvalFunction))
-> [(Name, Types)] -> [(Name, EvalFunction)]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
forall a. a -> a
id (Name -> Name)
-> (Types -> EvalFunction) -> (Name, Types) -> (Name, EvalFunction)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Types -> EvalFunction
mkNullary) [(Name, Types)]
nullaryTypes)
        unLib :: FunconLibrary
unLib   = [(Name, EvalFunction)] -> FunconLibrary
libFromList (((Name, Types -> Types) -> (Name, EvalFunction))
-> [(Name, Types -> Types)] -> [(Name, EvalFunction)]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
forall a. a -> a
id (Name -> Name)
-> ((Types -> Types) -> EvalFunction)
-> (Name, Types -> Types)
-> (Name, EvalFunction)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (Types -> Types) -> EvalFunction
mkUnary) [(Name, Types -> Types)]
unaryTypes)
        binLib :: FunconLibrary
binLib  = [(Name, EvalFunction)] -> FunconLibrary
libFromList (((Name, Types -> Types -> Types) -> (Name, EvalFunction))
-> [(Name, Types -> Types -> Types)] -> [(Name, EvalFunction)]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
forall a. a -> a
id (Name -> Name)
-> ((Types -> Types -> Types) -> EvalFunction)
-> (Name, Types -> Types -> Types)
-> (Name, EvalFunction)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (Types -> Types -> Types) -> EvalFunction
mkBinary) [(Name, Types -> Types -> Types)]
binaryTypes)
        floatsLib :: FunconLibrary
floatsLib = [(Name, EvalFunction)] -> FunconLibrary
libFromList (((Name, IEEEFormats -> Types) -> (Name, EvalFunction))
-> [(Name, IEEEFormats -> Types)] -> [(Name, EvalFunction)]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
forall a. a -> a
id (Name -> Name)
-> ((IEEEFormats -> Types) -> EvalFunction)
-> (Name, IEEEFormats -> Types)
-> (Name, EvalFunction)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (IEEEFormats -> Types) -> EvalFunction
mkFloats) [(Name, IEEEFormats -> Types)]
floatTypes)
        boundedLib :: FunconLibrary
boundedLib = [(Name, EvalFunction)] -> FunconLibrary
libFromList (((Name, Integer -> Types) -> (Name, EvalFunction))
-> [(Name, Integer -> Types)] -> [(Name, EvalFunction)]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
forall a. a -> a
id (Name -> Name)
-> ((Integer -> Types) -> EvalFunction)
-> (Name, Integer -> Types)
-> (Name, EvalFunction)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (Integer -> Types) -> EvalFunction
mkBounded) [(Name, Integer -> Types)]
boundedIntegerTypes)

        mkNullary :: Types -> EvalFunction 
        mkNullary :: Types -> EvalFunction
mkNullary = Rewrite Rewritten -> EvalFunction
NullaryFuncon (Rewrite Rewritten -> EvalFunction)
-> (Types -> Rewrite Rewritten) -> Types -> EvalFunction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten)
-> (Types -> Values) -> Types -> Rewrite Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Types -> Values
typeVal

        mkFloats :: (IEEEFormats -> Types) -> EvalFunction
        mkFloats :: (IEEEFormats -> Types) -> EvalFunction
mkFloats IEEEFormats -> Types
cons = StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
sfuncon
            where   sfuncon :: StrictFuncon
sfuncon [ADTVal Name
"binary32" [Funcons]
_] = Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
forall a b. (a -> b) -> a -> b
$ IEEEFormats -> Types
cons IEEEFormats
Binary32
                    sfuncon [ADTVal Name
"binary64" [Funcons]
_] = Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
forall a b. (a -> b) -> a -> b
$ IEEEFormats -> Types
cons IEEEFormats
Binary64
                    sfuncon [Values]
vs = Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr ([Values] -> Funcons
tuple_val_ [Values]
vs) String
"ieee-float not applied to ieee-format"
        mkBounded :: (Integer -> Types) -> EvalFunction
        mkBounded :: (Integer -> Types) -> EvalFunction
mkBounded Integer -> Types
cons = StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
sfuncon
            where   sfuncon :: StrictFuncon
sfuncon [Values
v1] 
                        | Int Integer
i1 <- Values -> Values
forall t. Values t -> Values t
upcastIntegers Values
v1 = 
                                    Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
forall a b. (a -> b) -> a -> b
$ Integer -> Types
cons Integer
i1
                    sfuncon [Values]
v = Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr ([Values] -> Funcons
tuple_val_ [Values]
v) String
"type not applied to an integer value" 

        mkUnary :: (Types -> Types) -> EvalFunction
        mkUnary :: (Types -> Types) -> EvalFunction
mkUnary Types -> Types
cons = StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
sfuncon
            where sfuncon :: StrictFuncon
sfuncon [ComputationType (Type Types
x)]  = Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
forall a b. (a -> b) -> a -> b
$ Types -> Types
cons Types
x
                  sfuncon  [Values]
_                          = Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
forall a b. (a -> b) -> a -> b
$ Types -> Types
cons Types
forall t. Types t
VAL.Values

        mkBinary :: (Types -> Types -> Types) -> EvalFunction
        mkBinary :: (Types -> Types -> Types) -> EvalFunction
mkBinary Types -> Types -> Types
cons = StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
sfuncon
            where sfuncon :: StrictFuncon
sfuncon [ComputationType (Type Types
x), ComputationType (Type Types
y)] = 
                    Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Types
forall t. HasValues t => t -> t -> Types t
maps (Types -> Funcons
forall t. HasTypes t => Types t -> t
injectT Types
x) (Types -> Funcons
forall t. HasTypes t => Types t -> t
injectT Types
y)
                  sfuncon [Values]
_ = Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
forall a b. (a -> b) -> a -> b
$ Types -> Types -> Types
cons Types
forall t. Types t
VAL.Values Types
forall t. Types t
VAL.Values

app0_ :: ([Funcons] -> Funcons) -> Funcons
app0_ :: ([Funcons] -> Funcons) -> Funcons
app0_ [Funcons] -> Funcons
cons = [Funcons] -> Funcons
cons []

app1_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons
app1_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons
app1_ [Funcons] -> Funcons
cons Funcons
x = [Funcons] -> Funcons
cons [Funcons
x]

app2_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons
app2_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons
app2_ [Funcons] -> Funcons
cons Funcons
x Funcons
y = [Funcons] -> Funcons
cons [Funcons
x,Funcons
y]

app3_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons -> Funcons
app3_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons -> Funcons
app3_ [Funcons] -> Funcons
cons Funcons
x Funcons
y Funcons
z = [Funcons] -> Funcons
cons [Funcons
x,Funcons
y,Funcons
z]


ty_star,ty_opt,ty_plus,ty_neg :: Funcons -> Funcons
ty_star :: Funcons -> Funcons
ty_star = (Funcons -> SeqSortOp -> Funcons)
-> SeqSortOp -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> SeqSortOp -> Funcons
FSortSeq SeqSortOp
StarOp
ty_opt :: Funcons -> Funcons
ty_opt = (Funcons -> SeqSortOp -> Funcons)
-> SeqSortOp -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> SeqSortOp -> Funcons
FSortSeq SeqSortOp
QuestionMarkOp
ty_plus :: Funcons -> Funcons
ty_plus = (Funcons -> SeqSortOp -> Funcons)
-> SeqSortOp -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> SeqSortOp -> Funcons
FSortSeq SeqSortOp
PlusOp
ty_neg :: Funcons -> Funcons
ty_neg = Funcons -> Funcons
FSortComplement 

ty_inter,ty_union,ty_power :: Funcons -> Funcons -> Funcons
ty_inter :: Funcons -> Funcons -> Funcons
ty_inter = Funcons -> Funcons -> Funcons
FSortInter
ty_union :: Funcons -> Funcons -> Funcons
ty_union = Funcons -> Funcons -> Funcons
FSortUnion
ty_power :: Funcons -> Funcons -> Funcons
ty_power = Funcons -> Funcons -> Funcons
FSortPower

-- $cbsintro
-- This section describes functions that extend the interpreter with
-- backtracking and pattern-matching facilities. These functions
-- are developed for compiling CBS funcon specifications to 
-- Haskell. To read about CBS we refer to 
-- <http://plancomps.dreamhosters.com/wp-content/uploads/2016/02/jlamp-16.pdf JLAMP2016>. 
-- The functions can be 
-- used for manual development of funcons, although this is not recommended.