{-# LANGUAGE OverloadedStrings #-}
module Funcons.EDSL (
Funcons(..), Values(..), Types(..), ComputationTypes(..),SeqSortOp(..),
applyFuncon,
app0_, app1_, app2_, app3_,
set_, vec_, env_fromlist_, null__,
int_, bool_, bool__, list__, vector__, tuple__, char_, char__, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_,
values_, integers_, vectors_, type_, ty_star, ty_plus, ty_opt, ty_union, ty_neg, ty_inter, ty_power,
showValues, showValuesSeq, showFuncons, showFunconsSeq, showTypes, showTerms, showOp,
isVal, isInt, isNat, isList, isMap, isType,
isVec, isChar, isTup, isString, isString_, unString,
downcastValue, downcastType, downcastValueType,
upcastNaturals, upcastIntegers, upcastRationals,upcastCharacter,
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 . map (\(k,v) -> tuple_ [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 (injectT x) (injectT 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]
ty_star,ty_opt,ty_plus,ty_neg :: Funcons -> Funcons
ty_star = flip FSortSeq StarOp
ty_opt = flip FSortSeq QuestionMarkOp
ty_plus = flip FSortSeq PlusOp
ty_neg = FSortComplement
ty_inter,ty_union,ty_power :: Funcons -> Funcons -> Funcons
ty_inter = FSortInter
ty_union = FSortUnion
ty_power = FSortPower