{-# LANGUAGE OverloadedStrings #-}
module Funcons.EDSL (
Funcons(..), Values(..), Types(..), ComputationTypes(..),SeqSortOp(..),TaggedSyntax(..),
applyFuncon,
app0_, app1_, app2_, app3_,
tuple_, list_, set_, map_, vec_, env_fromlist_, none__,
int_, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_,
values_, integers_, atoms_, unicode_characters_, vectors_, type_,
showValues, showValuesSeq, showFuncons, showFunconsSeq, showTypes, showTerms, showOp,
isVal, isInt, isNat, isList, isMap, isType,
isVec, isAscii, isChar, isTup, isString, isString_, unString,
downcastValue, downcastType, downcastValueType,
upcastNaturals, upcastIntegers, upcastRationals, upcastUnicode,
EvalFunction(..), Strictness(..), StrictFuncon, PartiallyStrictFuncon,
NonStrictFuncon, ValueOp, NullaryFuncon,
FunconLibrary, libEmpty, libUnion, libOverride, libUnions, libOverrides, libFromList, Funcons.EDSL.library, fromNullaryValOp, fromValOp, fromSeqValOp,
MSOS, Rewrite, Rewritten,
rewriteTo, rewriteSeqTo, stepTo, stepSeqTo,
compstep, rewritten, premiseStep, premiseEval,
norule, sortErr, partialOp,
Inherited, getInh, withInh,
Mutable, getMut, putMut,
Output, writeOut, readOut,
Control, raiseSignal, receiveSignals,
Input, withExtraInput, withExactInput,
FTerm(..), Env, emptyEnv, fvalues,
rewriteTermTo,stepTermTo,premise,
withInhTerm, getInhPatt, putMutTerm, getMutPatt, writeOutTerm, readOutPatt,
receiveSignalPatt, raiseTerm, matchInput, withExtraInputTerms, withExactInputTerms,
withControlTerm, getControlPatt,
evalRules, stepRules, rewriteRules,
SideCondition(..), sideCondition, lifted_sideCondition,
VPattern(..), FPattern(..), TPattern(..),
vsMatch, fsMatch, f2vPattern,
lifted_vsMatch, lifted_fsMatch, pat2term, vpat2term, typat2term,
envRewrite, envStore, lifted_envRewrite, lifted_envStore,
TypeEnv, TyAssoc(..), HasTypeVar(..), limitedSubsTypeVar, limitedSubsTypeVarWildcard,
rewriteType,
EntityDefaults, EntityDefault(..),
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 fnm = compstep . premiseStepApp (flattenApp app)
where app = applyFuncon fnm
congruence1_2 :: Name -> Funcons -> Funcons -> Rewrite Rewritten
congruence1_2 fnm arg1 arg2 = compstep $ premiseStepApp (flattenApp app) arg1
where app fs = applyFuncon fnm (fs++[arg2])
congruence2_2 :: Name -> Funcons -> Funcons -> Rewrite Rewritten
congruence2_2 fnm arg1 arg2 = compstep $ premiseStepApp (flattenApp app) arg2
where app fs = applyFuncon fnm (arg1:fs)
congruence1_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence1_3 fnm arg1 arg2 arg3 = compstep $ premiseStepApp (flattenApp app) arg1
where app fs = applyFuncon fnm (fs ++ [arg2, arg3])
congruence2_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence2_3 fnm arg1 arg2 arg3 = compstep $ premiseStepApp (flattenApp app) arg2
where app fs = applyFuncon fnm (arg1 : fs ++ [arg3])
congruence3_3 :: Name -> Funcons -> Funcons -> Funcons -> Rewrite Rewritten
congruence3_3 fnm arg1 arg2 arg3 = compstep $ premiseStepApp (flattenApp app) arg3
where app fs = applyFuncon fnm ([arg1, arg2] ++ fs)
flattenApp :: ([Funcons] -> Funcons) -> (StepRes -> StepRes)
flattenApp app res = case res of
Left f -> toStepRes (app [f])
Right vs -> toStepRes (app (map FValue vs))
env_fromlist_ :: [(String, Funcons)] -> Funcons
env_fromlist_ = FMap . concatMap (\(k,v) -> [string_ k, v])
library :: FunconLibrary
library = libUnions [unLib, nullLib, binLib, floatsLib,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)
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"
mkBounded :: (Integer -> Types) -> EvalFunction
mkBounded cons = StrictFuncon sfuncon
where sfuncon [v1]
| Int i1 <- upcastIntegers v1 =
rewritten $ typeVal $ cons i1
sfuncon v = sortErr (tuple_val_ v) "type not applied to an integer value"
mkUnary :: (Types -> Types) -> EvalFunction
mkUnary cons = StrictFuncon sfuncon
where sfuncon [ComputationType (Type x)] = rewritten $ typeVal $ cons x
sfuncon _ = rewritten $ typeVal $ cons VAL.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 VAL.Values VAL.Values
app0_ :: ([Funcons] -> Funcons) -> Funcons
app0_ cons = cons []
app1_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons
app1_ cons x = cons [x]
app2_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons
app2_ cons x y = cons [x,y]
app3_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons -> Funcons
app3_ cons x y z = cons [x,y,z]