{-# 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
    -- *** Funcon terms
        list_, tuple_, set_, map_empty_, empty_tuple_,
    -- *** Values
        int_, nat_, string_,
    -- *** Types
        values_, integers_, strings_, unicode_characters_,
    -- ** Pretty-print funcon terms
        showValues, showFuncons, showTypes,
    -- ** Is a funcon term a certain value?
        isVal, isString, isInt, isNat, isList, isMap, isType,
        isVec, isAscii, isChar, isTup, isId, isThunk, 
    -- ** Up and downcasting between funcon terms 
        downcastValue, downcastType, downcastValueType,
        upcastNaturals, upcastIntegers, upcastRationals, upcastUnicode,
    -- ** Evaluation functions
         EvalFunction(..), Strictness(..), StrictFuncon, PartiallyStrictFuncon, 
              NonStrictFuncon, ValueOp, NullaryFuncon,

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

    -- $cbsintro

    -- ** Funcon representation with meta-variables
        FTerm(..), Env, emptyEnv, 
    -- *** Defining rules 
        rewriteTermTo,stepTermTo,premise,
    -- *** Entity access
        withInhTerm, getInhPatt, putMutTerm, getMutPatt, writeOutTerm, readOutPatt, 
        receiveSignalPatt, raiseTerm, assignInput, withExtraInputTerms, withExactInputTerms, 
    -- ** Backtracking
        evalRules, SideCondition(..), sideCondition,  lifted_sideCondition,

    -- ** Pattern Matching
        VPattern(..), FPattern(..), 
            vsMatch, fsMatch,
            lifted_vsMatch, lifted_fsMatch,
       
    -- * Tools for creating interpreters
  
    -- For more explanation see "Funcons.Tools"
    -- ** Helpers for defining evaluation functions.
        rewriteType,
    -- ** Default entity values
        EntityDefaults, EntityDefault(..),
    -- ** Type environments
        TypeEnv, DataTypeMembers(..), DataTypeAlt(..),  
            typeLookup, typeEnvUnion, typeEnvUnions, typeEnvFromList, emptyTypeEnv,
    )where

import Funcons.MSOS
import Funcons.Types
import Funcons.Entities
import Funcons.Patterns
import Funcons.Substitution
import Funcons.Printer

import Control.Arrow ((***))

congruence1_1 :: Name -> Funcons -> Rewrite Rewritten
congruence1_1 fnm = compstep . premiseStepApp app 
    where app f = applyFuncon fnm [f] 

congruence1_2 :: Name -> Funcons -> Funcons -> Rewrite Rewritten
congruence1_2 fnm arg1 arg2 = compstep $ premiseStepApp app arg1 
    where app f = applyFuncon fnm [f, arg2]

congruence2_2 :: Name -> Funcons -> Funcons -> Rewrite Rewritten
congruence2_2 fnm arg1 arg2 = compstep $ premiseStepApp app arg2
    where app f = applyFuncon fnm [arg1, f]

congruence1_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence1_3 fnm arg1 arg2 arg3 = compstep $ premiseStepApp app arg1 
    where app f = applyFuncon fnm [f, arg2, arg3]

congruence2_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence2_3 fnm arg1 arg2 arg3 = compstep $ premiseStepApp app arg2 
    where app f = applyFuncon fnm [arg1, f, arg3]

congruence3_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence3_3 fnm arg1 arg2 arg3 = compstep $ premiseStepApp app arg3 
    where app f = applyFuncon fnm [arg1, arg2, f]

-- | A funcon library with funcons for builtin types.
library :: FunconLibrary
library = libUnions [unLib, nullLib, binLib, floatsLib, bitsLib
                    ,boundedLib]
 where
        nullLib = libFromList (map (id *** mkNullary) nullaryTypes)
        unLib   = libFromList (map (id *** mkUnary) unaryTypes)
        binLib  = libFromList (map (id *** mkBinary) binaryTypes)
        floatsLib = libFromList (map (id *** mkFloats) floatTypes)
        bitsLib = libFromList (map (id *** mkBits) bitsTypes)
        boundedLib = libFromList (map (id *** mkBounded) boundedIntegerTypes)

        mkNullary :: Types -> EvalFunction 
        mkNullary = NullaryFuncon . rewritten . typeVal

        mkFloats :: (IEEEFormats -> Types) -> EvalFunction
        mkFloats cons = StrictFuncon sfuncon
            where   sfuncon [ADTVal "binary32" _] = rewritten $ typeVal $ cons Binary32
                    sfuncon [ADTVal "binary64" _] = rewritten $ typeVal $ cons Binary64
                    sfuncon vs = sortErr (tuple_val_ vs) "ieee-float not applied to ieee-format"

        mkBits :: (Int -> Types) -> EvalFunction
        mkBits cons = StrictFuncon sfuncon
            where   sfuncon [v] | Nat n <- upcastNaturals v = 
                                        rewritten $ typeVal $ cons (fromInteger n)
                    sfuncon vs = sortErr (tuple_val_ vs) "bits not applied to naturals" 

        mkBounded :: (Integer -> Integer -> Types) -> EvalFunction
        mkBounded cons = StrictFuncon sfuncon
            where   sfuncon [v1,v2] 
                        | Int i1 <- upcastIntegers v1, Int i2 <- upcastIntegers v2 = 
                                    rewritten $ typeVal $ cons i1 i2
                    sfuncon v = sortErr (tuple_val_ v) "bounded-integers not applied to two integers" 

        mkUnary :: (Types -> Types) -> EvalFunction
        mkUnary cons = StrictFuncon sfuncon
            where sfuncon [ComputationType (Type x)]  = rewritten $ typeVal $ cons x
                  sfuncon  _                          = rewritten $ typeVal $ cons Values

        mkBinary :: (Types -> Types -> Types) -> EvalFunction
        mkBinary cons = StrictFuncon sfuncon
            where sfuncon [ComputationType (Type x), ComputationType (Type y)] = 
                    rewritten $ typeVal $ Maps x y
                  sfuncon _ = rewritten $ typeVal $ cons Values Values

-- $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/taosd2015/ TAOSD2015>The functions can be 
-- used for manual development of funcons, although this is not recommended.