tempus (empty) → 0.1.0
raw patch · 13 files changed
+2083/−0 lines, 13 filesdep +arraydep +basedep +directorysetup-changed
Dependencies added: array, base, directory, executable-path, filepath, haskeline, mtl, uniplate, utf8-string
Files
- LICENSE +25/−0
- Prelude.tp +89/−0
- Setup.hs +6/−0
- Tempus/Evaluation.hs +306/−0
- Tempus/Examples/lightbulb.tp +65/−0
- Tempus/Interpreter.hs +293/−0
- Tempus/Lexer.hs +326/−0
- Tempus/Loc.hs +23/−0
- Tempus/Main.hs +20/−0
- Tempus/Parser.y +226/−0
- Tempus/Syntax.hs +186/−0
- Tempus/TypeCheck.hs +468/−0
- tempus.cabal +50/−0
+ LICENSE view
@@ -0,0 +1,25 @@+Copyright (C) 2010, Matthias Reisner+All rights reserved.++Redistribution and use in source and binary forms, with or without modification, are permitted+provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright notice, this list of conditions+ and the following disclaimer.++ * Redistributions in binary form must reproduce the above copyright notice, this list of+ conditions and the following disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of the copyright holders nor the names of the contributors may be used to+ endorse or promote products derived from this software without specific prior written+ permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS “AS IS” AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND+FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER+IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF+THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Prelude.tp view
@@ -0,0 +1,89 @@+-- ------------------------+-- The Tempus Prelude+-- ------------------------+++-- * Functions++-- id : a -> a+value id = \ x . x++-- curry : (a * b -> c) -> a -> b -> c+value curry = \ f . \ x . \ y . f (x, y)++-- uncurry : (a -> b -> c) -> a * b -> c+value uncurry = \ f . \ p . f (first p) (second p)+++-- * Tuples++-- pair : a -> b -> a * b+value pair = \ x . \ y . (x, y)++-- normalize : (a * b) * c -> a * b * c+value normalize = \ p . (first (first p), second (first p), second p)++-- onFirst : (a -> b) -> (a * c) -> (b * c)+value onFirst = \ f . \ p . (f (first p), second p)++-- onSecond : (a -> b) -> (c * a) -> (c * b)+value onSecond = \ f . \ p . (first p, f (second p))+++-- * Booleans++type Bool = 1 + 1++-- false : Bool+value false = left ()++-- true : Bool+value true = right ()++-- branch : a -> a -> Bool -> a+value branch = \ x . \ y . case (\ _ . x) (\ _ . y)++-- not : Bool -> Bool+value not = branch true false++-- and : Bool -> Bool -> Bool+value and = branch (\ _ . false) id++-- or : Bool -> Bool -> Bool+value or = branch id (\ _ . true)++-- xor : Bool -> Bool -> Bool+value xor = branch id not+++-- * Extended behaviors++type Behavior a = a * behavior a++-- Behavior : a -> behavior a -> Behavior a+value Behavior = pair++-- head : Behavior a -> a+value head = first++-- tail : Behavior a -> behavior a+value tail = second++-- cut : Behavior a -> event b -> event (Behavior a * b)+value cut = \ b . \ e . const pair <*> expand (tail b) <.> e+++-- * Extended events++type Event a = a + event a++-- now : a -> Event a+value now = left++-- later : event a -> Event a+value later = right+++-- * Event streams++type EventStream a = nu s . event (a * s)
+ Setup.hs view
@@ -0,0 +1,6 @@+module Main (main) where++import Distribution.Simple++main :: IO ()+main = defaultMain
+ Tempus/Evaluation.hs view
@@ -0,0 +1,306 @@+-- | Evaluation of Tempus expressions.+module Tempus.Evaluation (+ EvalEnv,+ Value (..),++ evalExpr+) where+++import Tempus.Syntax+import Tempus.TypeCheck++import Data.List++-- | Representation of evaluation environments as a list of pairs of a variable with its expression.+type EvalEnv = [(Var, Expr)]++-- | Internal format for the value of an expression.+data Value = Natural Integer+ | Unit+ | Function (Value -> Value)+ | Pair Value Value+ | ChoiceLeft Value+ | ChoiceRight Value+ | Behavior (RelTime -> Value)+ | Event RelTime Value++-- | Number of time steps with corresponding values to include when showing a bahavior.+behaviorShowFuture :: Integer+behaviorShowFuture = 7++-- | Number of time steps to look ahead when deciding if to show an event as never occuring or not.+eventShowLookAhead :: Integer+eventShowLookAhead = 100++-- TODO: make length of behavior future scalable+-- TODO: make mu/nu expression depth scalable+instance Show Value where+ showsPrec _ (Natural i) = shows i+ showsPrec _ (Unit) = showString "()"+ showsPrec _ (Function _) = showString "<function>"+ showsPrec p (Pair e1 e2) = showParen (p > 0) $+ showsPrec 1 e1 . showString " , " . showsPrec 0 e2+ showsPrec p (ChoiceLeft e) = showParen (p > 3) $+ showString "left " . showsPrec 4 e+ showsPrec p (ChoiceRight e) = showParen (p > 3) $+ showString "right " . showsPrec 4 e+ showsPrec p (Behavior f) = showParen (True) $ showString $ (+ concat . intersperse "; "+ . map (\ps -> case ps of+ [(v, t)] -> "@" ++ show (fromTime t) ++ ": " ++ v+ ps -> "@" ++ (let ps' = map snd ps in+ show (head ps') ++ ".." ++ show (last ps')) ++ ": " ++ fst (head ps))+ . groupBy (\x y -> fst x == fst y) . map (\t -> (show $ f t, t)) $+ map fromInteger [1..behaviorShowFuture]) ++ "; ..."+ showsPrec p (Event t e) = showParen (p > 3) $+ if t > fromInteger eventShowLookAhead+ then showString "?"+ else showString "@" . shows t . showString ": " . shows e++-- | Time representation for events and behaviors+data RelTime = One+ | Succ RelTime+ deriving (Eq)++-- | A 'RelTime' value for an infinite number of time steps.+infinite :: RelTime+infinite = Succ infinite++instance Show RelTime where+ show t = show $ fromTime t++-- | Conversion from 'RelTime' values to 'Integer' values+fromTime :: RelTime -> Integer+fromTime One = 1+fromTime (Succ t) = 1 + fromTime t++instance Ord RelTime where+ compare One One = EQ+ compare One _ = LT+ compare (Succ t1) (Succ t2) = compare t1 t2+ compare (Succ _) _ = GT++ min One t' = One+ min t One = One+ min (Succ t) (Succ t') = Succ $ min t t'++instance Num RelTime where+ t + t' = Succ $ case t of+ One -> t'+ Succ t -> t + t'++ Succ t - One = t+ Succ t - Succ t' = t - t'+ _ - _ = error "undefined value for RelTime"++ fromInteger = genericIndex (iterate Succ One) . pred++ (*) = undefined+ abs = undefined+ signum = undefined++{- |+ @evalExpr sEnv tEnv eEnv e@ evaluates an expression @e@ given ++ [@sEnv@] the list of type synonyms,++ [@tEnv@] the list of global variables with their types, and++ [@eEnv@] the list of global variables with their expressions.+-}+evalExpr :: TypeSynEnv -> TypeEnv -> EvalEnv -> Expr -> Value+evalExpr = eval []++{- |+ Helper function for 'evalExpr'. @eval lEnv sEnv tEnv eEnv e@ evaluates an expression @e@+ given++ [@lEnv@] the list of local variables with their values,++ [@sEnv@] the list of type synonyms,++ [@tEnv@] the list of global variables with their types, and++ [@eEnv@] the list of global variables with their expressions.+-}+eval :: [(Var, Value)] -> TypeSynEnv -> TypeEnv -> EvalEnv -> Expr -> Value+eval lEnv sEnv tEnv eEnv expr = let eval' = eval lEnv sEnv tEnv eEnv in case expr of+ ExPair e1 e2 -> Pair (eval' e1) (eval' e2)+ ExNatLit i -> Natural i+ ExUnit -> Unit+ ExLeft -> Function $ \v -> ChoiceLeft v+ ExRight -> Function $ \v -> ChoiceRight v+ ExNull -> Function $ \_ -> error "eval: received value of type 0"+ ExFst -> Function $ \p -> case p of+ Pair l _ -> l+ _ -> error "eval: argument to ExFst not a pair"+ ExSnd -> Function $ \p -> case p of+ Pair _ r -> r+ _ -> error "eval: argument to ExSnd not a pair"+ ExCase -> Function $ \(Function l) -> Function $ \(Function r) -> Function $ \c -> case c of+ ChoiceLeft e -> l e+ ChoiceRight e -> r e+ _ -> error "third argument to case not left/right"++ ExVar (Var "add") -> withNat $ \i -> withNat $ \j -> Natural $ i + j+ ExVar (Var "mult") -> withNat $ \i -> withNat $ \j -> Natural $ i * j+ ExVar v -> case lookup v lEnv of+ Just x -> x+ Nothing -> maybe (error $ "eval: undefined var `" ++ show (SrcCode v) ++ "'")+ eval' $ lookup v eEnv++ ExLam v e -> Function (\x -> eval (replVar v x lEnv) sEnv tEnv eEnv e)+ ExApp f x -> case eval' f of+ Function fun -> fun $ eval' x+ _ -> error "eval: first argument to ExApp not a function"++ ExBehav f -> case eval' f of+ Function f -> Behavior (f . Natural . fromTime)+ _ -> error "first argument to ExBehav not a function"+ ExEvent t e -> case eval' t of+ Natural i -> Event (fromInteger i) $ eval' e+ _ -> error "first argument to ExEvent not a positive"+ ExNever -> Event infinite $ error "secret value of type 0"+ ExConst e -> Behavior $ \_ -> eval' e+ ExLiftAppB f b -> case (eval' f, eval' b) of+ (Behavior f, Behavior g) -> Behavior $ \t -> case f t of+ Function f -> f (g t)+ _ -> error "wrong argument type(s) to ExLiftAppB"+ _ -> error "wrong argument type(s) to ExLiftAppB"+ ExLiftAppE f e -> case (eval' f, eval' e) of+ (Behavior f, Event t v) -> Event t $ case f t of+ Function f -> f v+ _ -> error "wrong argument type(s) to ExLiftAppE"+ _ -> error "wrong argument type(s) to ExLiftAppE"+ ExRace -> Function $ \e1 -> case e1 of+ Event t1 v1 -> Function $ \e2 -> case e2 of+ Event t2 v2 -> Event (min t1 t2) $ case compare t1 t2 of+ LT -> ChoiceRight $ ChoiceLeft $ Pair v1 (Event (t2 - t1) v2)+ EQ -> ChoiceLeft $ Pair v1 v2+ GT -> ChoiceRight $ ChoiceRight $ Pair v2 (Event (t1 - t2) v1)+ _ -> error "second argument to ExRace not an event"+ _ -> error "first argument to ExRace not an event"+ ExExpand -> Function $ \e -> case e of+ Behavior f -> Behavior $ \t -> Pair (f t) (Behavior $ \t' -> f $ t + t')+ _ -> error "first argument to ExExpand not a behavior"+ ExPack _ -> Function id+ ExUnpack _ -> Function id+ ExReflect -> Function $ \v -> let nat 1 = ChoiceLeft Unit+ nat n = ChoiceRight $ nat (n-1)+ in case v of+ Natural n -> nat n+ _ -> error "eval: argument to ExReflect not a positive"++ -- fold :: (Functor shape) => (shape accu -> accu) -> Fix shape -> accu+ -- fold fun = fun . fmap (fold fun) . unFix+ ExFold mu f ->+ let Right (MuType var t) = expandMuType sEnv mu+ fold fun = fun . genmap CoVariant sEnv var t (fold fun)+ in case eval' f of+ Function fun -> Function $ fold fun+ _ -> error "eval: first argument to ExFold not a function"++ -- unfold :: (Functor shape) => (accu -> shape accu) -> accu -> Fix shape+ -- unfold fun = Fix . fmap (unfold fun) . fun+ ExUnfold nu f ->+ let Right (NuType var t) = expandNuType sEnv nu+ unfold fun = genmap CoVariant sEnv var t (unfold fun) . fun+ in case eval' f of+ Function fun -> Function $ unfold fun+ _ -> error "eval: first argument to ExUnfold not a function"++ ExUJump ->+ let jump e = case e of+ Event t v ->+ let (t', v') = case v of+ ChoiceLeft v' -> (One, v')+ ChoiceRight e' -> jump e'+ _ -> error "eval: inner argument to ExUJump not a choice"+ in (t + t', v')+ _ -> error "eval: argument to ExUJump not an event"+ in Function $ \e -> let (Succ t, v) = jump e in Event t v++ ExUSwitch ->+ let switch p = case p of+ Pair (Behavior f) (Event t ~(Pair v p')) -> \t' -> case compare t' t of+ LT -> f t'+ EQ -> v+ GT -> switch p' (t' - t)+ _ -> error "wrong argument type(s) to ExUSwitch"+ in Function $ \p -> let f = switch p in Behavior f+++{- |+ @genmap var sEnv v t f@ generates a generic comap\/contramap function for a type @t@ that+ applies a function @f@ to values of a type @t@. If @var == CoVariant@ a comap function will be+ produced, a contramap function for @var == ContraVariant@, where @v@ is the type variable the+ map is generated for and @sEnv@ the list of type synonyms.+-}+genmap :: Variance -> TypeSynEnv -> Var -> Type -> (Value -> Value) -> Value -> Value+genmap var sEnv v t f = case t of+ TyZero -> id+ TyUnit -> id+ TyNat -> id++ TyBehav t -> \e -> case e of+ Behavior g -> Behavior $ genmap var sEnv v t f . g+ _ -> error "genmap: value of type TyBehav is not a behavior"+ + TyEvent t -> \e -> case e of+ Event n e' -> Event n $ genmap var sEnv v t f e'+ _ -> error "genmap: value of type TyBehav is not a behavior"++ TyPair t1 t2 -> \e -> case e of+ Pair e1 e2 -> Pair (genmap var sEnv v t1 f e1) (genmap var sEnv v t2 f e2)+ _ -> error "genmap: value of type TyPair is not a pair"++ TyPlus t1 t2 -> \e -> case e of+ ChoiceLeft e' -> ChoiceLeft $ genmap var sEnv v t1 f e'+ ChoiceRight e' -> ChoiceRight $ genmap var sEnv v t2 f e'+ _ -> error "genmap: value of type TyPlus is not a choice"++ TyFun t1 t2 -> \e -> case e of+{-+ -- comap f function = comap f . function . contramap f+ (Function g, CoVariant) -> Function $+ genmap CoVariant sEnv rEnv t2 . g . genmap ContraVariant sEnv rEnv t1+ -- contramap f function = contramap f . function . comap f+ (Function g, ContraVariant) -> Function $+ genmap ContraVariant sEnv rEnv t2 . g . genmap CoVariant sEnv rEnv t1+-}+ Function g -> Function $ genmap var sEnv v t2 f+ . g . genmap (invertVariance var) sEnv v t1 f+ _ -> error "genmap: value of type TyFun not a function"++ TyApp v' [] | v' == v -> f+ TyApp v' ts -> case expandTypeSyn sEnv v' ts of+ Left _ -> id+ Right t -> genmap var sEnv v t f++ TyMu (MuType v' t') ->+ -- TODO: TyUnit here assures we get the subtrees as they are. That is a type error but + -- shouldn't be a problem for evaluation (only if v is mapped to a type including v+ -- itself, which shouldn't happen). Should be thoroughly thought through, though :-)+ let temp = TyUnit+ in genmap var sEnv v (substVar v' temp t') f+ . genmap var sEnv v' t' (genmap var sEnv v t f)++ TyNu (NuType v' t') ->+ -- TODO: see above+ let temp = TyUnit+ in genmap var sEnv v (substVar v' temp t') f+ . genmap var sEnv v' t' (genmap var sEnv v t f)++ TyVar _ -> error "genmap: called with TyVar"+ TyCon _ -> error "genmap: called with TyCon"+++withNat :: (Integer -> Value) -> Value+withNat f = Function $ \x -> case x of+ Natural n -> f n+ _ -> error "eval: function argument type mismatches expected type positive"++-- | @replVar v val@ adds a new variable @v@ with a value @var@ to a list of variable-value-pairs,+-- replacing the old value of @v@ if @v@ is already present.+replVar v v' = ((v, v') :) . filter ((/= v) . fst)
+ Tempus/Examples/lightbulb.tp view
@@ -0,0 +1,65 @@++-- * Preparation++ -- allNot : Behavior Bool → Behavior Bool+ value allNot = λ b . Behavior (not (head b)) (const not ⊛ tail b)++ -- allXor : Behavior Bool → Behavior Bool+ value allXor = λ b₁ . λ b₂ . Behavior (xor (head b₁) (head b₂)) (const xor ⊛ tail b₁ ⊛ tail b₂)++ type Ticks = ν σ . event σ++ -- dropDummies : EventStream 1 → Ticks+ value dropDummies = unfold [Ticks] (λ s . (const second) ⊙ (unpack [EventStream 1] s))++ type Segments = ν σ . Behavior Bool × event σ++ -- flip : Behavior Bool × event α → event (Behavior Bool × α)+ value flip = λ p . const (onFirst allNot) ⊙ cut (first p) (second p)++ -- step : Behavior Bool × Ticks → Behavior Bool × event (Behavior Bool × Ticks)+ value step = λ p . (first p, flip (onSecond (unpack [Ticks]) p))++ -- alternate : Behavior Bool → Ticks → Segments+ value alternate = curry (unfold [Segments] step)++ type UltraswitchArg = ν σ . behavior Bool × event (Bool × σ)++ -- shiftRecPoints : behavior Bool × event Segments → UltraswitchArg+ value shiftRecPoints = unfold [UltraswitchArg]+ (onSecond (λ e . const (λ s . normalize (unpack [Segments] s)) ⊙ e))++ -- ultraswitchArg : Segments → UltraswitchArg+ value ultraswitchArg = λ s . shiftRecPoints (tail (first (unpack [Segments] s)),+ second (unpack [Segments] s))++ -- prepareUltraswitch : Behavior Bool → EventStream 1 → nu s . behavior Bool × event (Bool × s)+ value prepareUltraswitch = λ b . λ s . ultraswitchArg (alternate b (dropDummies s))++-- * Actual example++ -- control : Behavior Bool → EventStream 1 → Behavior Bool+ value control = λ b . λ s . Behavior (head b) (ultraswitch (prepareUltraswitch b s))++ -- init : Bool+ value init = false++ -- one : EventStream 1 → Behavior Bool+ value one = control (Behavior init (const init))++ -- two : EventStream 1 → EventStream 1 → Behavior Bool+ value two = λ s₁ . λ s₂ . allXor (one s₁) (one s₂)++-- * Test cases++ -- s₁ : EventStream 1+ value s₁ = pack [EventStream 1] (event 2 ((),+ pack [EventStream 1] (const ? ⊙ never)))++ -- s₂ : EventStream 1+ value s₂ = pack [EventStream 1] (event 4 ((),+ pack [EventStream 1] (event 1 ((),+ pack [EventStream 1] (const ? ⊙ never)))))++ -- test : Behavior Bool+ value test = two s₁ s₂
+ Tempus/Interpreter.hs view
@@ -0,0 +1,293 @@+-- | The interpreter REPL.+module Tempus.Interpreter (+ repl+) where+++import Control.Arrow+import Control.Monad+import Control.Monad.Trans++import Data.Char+import Data.List+import Data.Maybe++import System.Console.Haskeline+import System.Directory+import System.FilePath+import qualified System.IO.UTF8 as BU++import Tempus.Loc+import Tempus.Syntax+import Tempus.Parser+import Tempus.TypeCheck+import Tempus.Evaluation+++version :: String+version = "0.1.0"++executableName :: String+executableName = "tempus"++-- | The state of the interpreter.+data IState = IState {+ -- | The path of the file the current module was loaded from, or @Nothing@ if no+ -- one is loaded.+ modulePath :: Maybe FilePath,++ -- TODO: merge typeEnv and evalEnv+ -- | A list of all global variables from the currently loaded module and added+ -- interactively with their corresponding inferred type.+ typeEnv :: TypeEnv,++ -- | A list of all type synonyms from the currently loaded module and added+ -- interactively.+ synEnv :: TypeSynEnv,++ -- | Like @typeEnv@ but with the expressions of the variables.+ evalEnv :: EvalEnv,++ -- | A triple with the same lists as @typeEnv@, @synEnv@, and @evalEnv@ but only+ -- including variables and types from the Prelude module.+ preludeEnvs :: (TypeEnv, TypeSynEnv, EvalEnv)+ }++-- | Initial interpreter state with empty lists and no module path.+initIState :: IState+initIState = IState {+ modulePath = Nothing,+ typeEnv = [],+ synEnv = [],+ evalEnv = [],+ preludeEnvs = ([], [], [])+ }++mergedTypeEnv st@IState { preludeEnvs = (vs, _, _) } = vs ++ typeEnv st+mergedSynEnv st@IState { preludeEnvs = (_, ts, _) } = ts ++ synEnv st+mergedEvalEnv st@IState { preludeEnvs = (_, _, es) } = es ++ evalEnv st+++-- TODO: Allow redeclaration of values/types+-- TODO: Catch Ctrl-C+-- | The main interpreter REPL loop with an optional path to a Prelude file that is loaded at+-- the start.+repl :: Maybe FilePath -> IO ()+repl preludePath = runInputT defaultSettings $ do+ outputStrLn $ "This is " ++ executableName ++ " version " ++ version++ mbInitSt <- maybe (return Nothing) (loadModule [] [] False) preludePath+ case mbInitSt of+ Nothing -> do+ outputStrLn "Warning: Loading the Prelude module failed!"+ loop initIState+ Just (vs, ts, es) -> do+ outputStrLn $ "Loaded Prelude module from file `" ++ fromJust preludePath ++ "'."+ loop $ initIState { preludeEnvs = (vs, ts, es) }++ where+ loop st = do+ let moduleName = maybe "" takeBaseName $ modulePath st+ input <- getInputLine $ moduleName ++ "> "+ case input >>= parseAction of+ Just (Command "?" _) -> do+ mapM_ outputStrLn helpLines+ loop st++ Just (Command "q" _) -> do+ outputStrLn $ "Leaving " ++ executableName ++ "."++ Just (Command "l" []) -> do+ outputStrLn $ "Unloading module."+ loop st { modulePath = Nothing, typeEnv = [], synEnv = [], evalEnv = [] }++ Just (Command "l" [path]) -> do+ let (tEnv, sEnv, _) = preludeEnvs st+ mbSt <- loadModule tEnv sEnv True path+ case mbSt of+ Nothing -> loop st+ Just (vs, ts, es) -> loop st { modulePath = Just path,+ typeEnv = vs,+ synEnv = ts,+ evalEnv = es }++ Just (Command "v" []) -> do+ showEnvironments (typeEnv st, synEnv st, evalEnv st)+ loop st++ Just (Command "p" []) -> do+ showEnvironments $ preludeEnvs st+ loop st++ Just (Command "t" [s]) -> do+ case parseExpr s of+ Left (Loc loc err) -> do+ outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err+ Right expr -> do+ case getType (mergedTypeEnv st) (mergedSynEnv st) (Loc (0,0) expr) of+ Left (Loc _ err) -> outputStrLn $ "*** type error: " ++ showTypeErr err+ Right t -> do+ outputStrLn $ " " ++ show (SrcCode expr)+ outputStrLn $ " : " ++ show (SrcCode t)+ loop st++ Just (Expression s) -> do+ case parseExpr s of+ Left (Loc loc err) -> do+ outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err+ Right expr -> do+ case getType (mergedTypeEnv st) (mergedSynEnv st) (Loc (0,0) expr) of+ Left (Loc _ err) -> outputStrLn $ "*** type error: " ++ showTypeErr err+ Right t -> liftIO $ putStrLn $ show $+ evalExpr (mergedSynEnv st) (mergedTypeEnv st) (mergedEvalEnv st) expr+ loop st++ Just (Declaration s) -> do+ case parseDecl s of+ Left (Loc loc err) -> do+ outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err+ loop st+ Right decl -> do+ let tEnv = mergedTypeEnv st+ sEnv = mergedSynEnv st+ case checkProgram tEnv sEnv [decl] of+ Left (Loc loc err) -> do+ outputStrLn $+ "*** type error: " ++ show loc ++ ": " ++ showTypeErr err+ loop st+ -- DeclVal+ Right (vs@[(v, (_,t))], []) -> do+ outputStrLn $ " " ++ show (SrcCode v) ++ " : " ++ show (SrcCode t)+ loop st { typeEnv = typeEnv st ++ vs,+ evalEnv = evalEnv st +++ [(v, let DeclVal _ _ e = decl in e )] }+ -- DeclType+ Right ([], ts@[_]) -> do+ outputStrLn $ " " ++ show (SrcCode decl)+ loop st { synEnv = synEnv st ++ ts }++ _ -> do+ outputStrLn $ "Unknown command, try :? for help."+ loop st+++-- | The list of lines to be displayed on @:?@.+helpLines :: [String]+helpLines = [+ -- "| |"+ " Available commands:", + " :? Show this help",+ " :q Quit",+ " :l Unload the current loaded module",+ " :l <file> Load the module in file <file>",+ " :v Show types of all currently loaded module variables",+ " :p Show types of all Prelude variables",+ " :t <expr> Show the type of expression <expr>",+ " <decl> Depending on the declaration <decl>, bring a new value",+ " or type synonym into scope",+ " <expr> Evaluate the expression <expr>"+ ]++-- | Produces an error message string for the given context error.+showTypeErr :: ContextError -> String+showTypeErr err = case err of+ UndefinedVariable v -> "undefined variable `" ++ show (SrcCode v) ++ "'"+ DuplicateVariable v -> "variable `" ++ show (SrcCode v) ++ "' already defined"+ DuplicateType v -> "type `" ++ show (SrcCode v) ++ "' already defined"+ OccursCheck t1 t2 -> "cannot construct the infinite type " ++ show (SrcCode t1)+ ++ " = " ++ show (SrcCode t2)+ SymbolClash t1 t2 -> "cannot match type " ++ show (SrcCode t1) ++ " with " ++ show (SrcCode t2)+ IncorrectVariances t -> "incorrect variances in type " ++ show (SrcCode t)+ UndefinedType v -> "undefiend type variable `" ++ show (SrcCode v) ++ "'"+ TypeArgsMismatch v -> "wrong number of arguments to type synonym `" ++ show (SrcCode v) ++ "'"+ NoMuType t -> "type " ++ show (SrcCode t) ++ " is not a mu type"+ NoNuType t -> "type " ++ show (SrcCode t) ++ " is not a nu type"+ NoRecType t -> "type " ++ show (SrcCode t) ++ " is neither a mu nor a nu type"+++{- |+ Reads an UTF8 encoded file and returns the file content. This function prevents that a file+ is read lazily and is so being kept in a locked state if a parser error occurs before the+ complete file was processed.+-}+seqReadFile :: FilePath -> IO String+seqReadFile = fmap (\s -> length s `seq` s) . BU.readFile+++{- |+ @loadModule tEnv sEnv verbose path@ reads a Tempus module from @path@ and parses and typechecks+ all definitions where the types from @tEnv@ and @tSyn@ can be used. The result are the lists+ of all variables with types, type synonyms and variables with expression from that module.+ If @verbose == True@ all type synonyms and variables with the inferred types are printed.+-}+loadModule :: TypeEnv -> TypeSynEnv -> Bool -> FilePath+ -> InputT IO (Maybe (TypeEnv, TypeSynEnv, EvalEnv))+loadModule tEnv sEnv verbose path = do+ exists <- liftIO $ doesFileExist path+ if exists+ then do+ s <- liftIO $ seqReadFile path+ case parseProgram s of+ Left (Loc loc err) -> do+ outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err+ return Nothing++ Right prog -> case checkProgram tEnv sEnv prog of+ Left (Loc loc err) -> do+ outputStrLn $ "*** type error: " ++ show loc ++ ": " ++ showTypeErr err+ return Nothing++ Right (vs, ts) -> do+ when verbose $ do+ forM_ ts $ \(v, (vs, t)) ->+ outputStrLn $ " " ++ show (SrcCode $ DeclType (0,0) v vs t)+ forM_ vs $ \(v, (_, t)) ->+ outputStrLn $ " " ++ show (SrcCode v) ++ " : " ++ show (SrcCode t)+ return $ Just (vs, ts, zip (map fst vs) [e | DeclVal _ _ e <- prog])+ else do+ outputStrLn $ "File not found: " ++ path+ return Nothing++-- | Prints a list of type synonyms and variables with their types.+showEnvironments :: (TypeEnv, TypeSynEnv, EvalEnv) -> InputT IO ()+showEnvironments (tEnv, sEnv, eEnv) = do+ case zipWith (\(v, (_, t)) (_, e) -> (v, e, t)) tEnv eEnv of+ [] -> outputStrLn $ "No variables loaded."+ env -> do+ outputStrLn $ "Loaded variables: "+ forM_ env $ \(v, e, t) -> outputStrLn $+ " " ++ show (SrcCode v) +++ -- " = " ++ show (SrcCode e) +++ " : " ++ show (SrcCode t)++ case sEnv of+ [] -> outputStrLn $ "No type synonyms loaded."+ env -> do+ outputStrLn $ "Loaded type synonyms: "+ forM_ env $ \(v, (vs, t)) -> outputStrLn $+ " " ++ show (SrcCode $ DeclType (0,0) v vs t)+ +-- | An interpreter action.+data Action = Command String [String]+ -- ^ A generic command with the list of parameters.+ | Expression String+ -- ^ An expression.+ | Declaration String+ -- ^ A type or value definition.++-- TODO: parse filenames with spaces correctly+-- TODO: better type/value parsing+-- | Parses a string command to an interpreter action or returns @Nothing@ if the parsing failed.+parseAction :: String -> Maybe Action+parseAction (':':'t':c:cs)+ | isSpace c = Just $ Command "t" [cs]+parseAction (':':cmd) = case words cmd of+ [] -> Nothing+ (c:cs) -> Just $ Command c cs+parseAction s+ | "value " `isPrefixOf` s = Just $ Declaration s+ | "type " `isPrefixOf` s = Just $ Declaration s+parseAction s@(c:cs)+ | isSpace c = parseAction $ dropWhile isSpace cs+ | otherwise = Just $ Expression s+parseAction _ = Nothing
+ Tempus/Lexer.hs view
@@ -0,0 +1,326 @@+-- | Tokenizing of Tempus source code.+module Tempus.Lexer (+ Token (..),+ showToken,+ lex,+ tokenize,++ Parser (..),+ ParseResult,+ initParser+) where+++import Prelude hiding (lex)++import Control.Applicative+import Control.Monad.State++import Data.Char+import Data.List (unfoldr)+import Data.Maybe (fromMaybe)++import Tempus.Loc+++-- * Tokens++-- | The input tokens for a Tempus parser.+data Token = EOF+ | Variable String+ | NatLit Integer+ | Equals+ | ArrowRight+ | Plus+ | Times+ | ParenOpen+ | ParenClose+ | Zero+ | One+ | Mu+ | Nu+ | Dot+ | Comma+ | Lambda+ | SquareOpen+ | SquareClose+ | AngleOpen+ | AngleClose+ | CircledAsterisk+ | CircledDot+ | QuestionMark++ | KWBehavior+ | KWCase+ | KWConst+ | KWEvent+ | KWExpand+ | KWFirst+ | KWFold+ | KWLeft+ | KWNever+ | KWPack+ | KWPositive+ | KWRace+ | KWReflect+ | KWRight+ | KWSecond+ | KWUltraswitch+ | KWType+ | KWUltrajump+ | KWUnfold+ | KWUnpack+ | KWValue+ deriving (Show, Eq)+++-- TODO: support unicode output+-- | Return the ASCII symbol or keyword, or a descriptive text for a token.+showToken :: Token -> String+showToken tok = case tok of+ EOF -> "end of file"+ Variable v -> v+ NatLit i -> show i+ Equals -> "="+ ArrowRight -> "->"+ Plus -> "+"+ Times -> "*"+ ParenOpen -> "("+ ParenClose -> ")"+ Zero -> "0"+ One -> "1"+ Mu -> "mu"+ Nu -> "nu"+ Dot -> "."+ Comma -> ","+ Lambda -> "\\"+ SquareOpen -> "["+ SquareClose -> "]"+ AngleOpen -> "opening angle bracket"+ AngleClose -> "closing angle bracket"+ CircledAsterisk -> "<*>"+ CircledDot -> "<.>"+ QuestionMark -> "?"+ KWBehavior -> "behavior"+ KWCase -> "case"+ KWConst -> "const"+ KWEvent -> "event"+ KWExpand -> "expand"+ KWFirst -> "first"+ KWFold -> "fold"+ KWLeft -> "left"+ KWNever -> "never"+ KWPack -> "pack"+ KWPositive -> "positive"+ KWRace -> "race"+ KWReflect -> "reflect"+ KWRight -> "right"+ KWSecond -> "second"+ KWUltraswitch -> "ultraswitch"+ KWType -> "type"+ KWUltrajump -> "ultrajump"+ KWUnfold -> "unfold"+ KWUnpack -> "unpack"+ KWValue -> "value"+++-- | The list of keyword and symbol strings with their corresponding token.+reserved :: [(String, Token)]+reserved = [+ -- keywords+ ("type", KWType),+ ("value", KWValue),+ ("behavior", KWBehavior),+ ("event", KWEvent),+ ("expand", KWExpand),+ ("positive", KWPositive),+ ("\x2115\x208A", KWPositive),+ ("fold", KWFold),+ ("unfold", KWUnfold),+ ("const", KWConst),+ ("left", KWLeft),+ ("right", KWRight),+ ("case", KWCase),+ ("first", KWFirst),+ ("second", KWSecond),+ ("never", KWNever),+ ("race", KWRace),+ ("reflect", KWReflect),+ ("pack", KWPack),+ ("unpack", KWUnpack),+ ("ultraswitch", KWUltraswitch),+ ("ultrajump", KWUltrajump),++ -- symbols+ ("\x03BC", Mu),+ ("mu", Mu),+ ("\x03BD", Nu),+ ("nu", Nu),+ ("\x2192", ArrowRight),+ ("->", ArrowRight),+ ("+", Plus),+ ("\xD7", Times),+ ("*", Times),+ ("\x03BB", Lambda),+ ("\\", Lambda),+ ("\x229B", CircledAsterisk),+ ("<*>", CircledAsterisk),+ ("\x2299", CircledDot),+ ("<.>", CircledDot),+ ("=", Equals),+ (".", Dot),+ ("?", QuestionMark)+ ]++-- | The list of brackets with a special meaning and their corresponding token.+brackets :: [(Char, Token)]+brackets = [+ ('(', ParenOpen),+ (')', ParenClose),+ ('[', SquareOpen),+ (']', SquareClose),+ ('\x27E8', AngleOpen),+ ('\x27E9', AngleClose)+ ]++++-- * Lexer++-- | The lexer monad.+type Lexer a = State LexerState a++-- | The lexer state.+data LexerState = LexerState {+ input :: String,+ -- ^ The residual input string.+ loc :: SrcLoc+ -- ^ The current location in the original input string.+ }+ deriving (Show, Eq)+++-- ** Primitive lexers++-- | Modify the input string of the current lexer state by the function.+modifyInput :: (String -> String) -> Lexer ()+modifyInput f = modify (\st -> st { input = f $ input st })++-- | Modify the location of the current lexer state.+modifyLoc :: (Int -> Int, Int -> Int) -> Lexer ()+modifyLoc (fl, fc) = modify (\st -> st { loc = let (l, c) = loc st in (fl l, fc c) })++-- | Discard the first @n@ characters of the current input string.+discard :: Int -> Lexer ()+discard n = modifyInput (drop n) >> modifyLoc (id, (+ n))+++-- | Read all subsequent characters satisfying a certain predicate from the input string and+-- return the read characters.+lexWhile :: (Char -> Bool) -> Lexer String+lexWhile p = do+ s <- gets input+ let (s', rest) = span p s+ modifyInput (const rest)+ modifyLoc (id, (+ length s'))+ return s'+++-- ** Tempus token lexers++-- | Lexes a single token discarding all whitespace before that token.+lexInput :: Lexer (Maybe Token)+lexInput = do+ s <- gets input+ case s of+ [] -> return $ Just EOF+ _ -> Just <$> lexToken >>= \t -> lexWhitespace >> return t++-- | Lexes all whitespace, including single line comments.+lexWhitespace :: Lexer ()+lexWhitespace = do+ s <- gets input+ case s of+ '-':'-':c:_ | isSpace c -> lexWhile (/= '\n') >> lexWhitespace+ '\n':_ -> discard 1 >> modifyLoc (succ, const 1) >> lexWhitespace+ c:_ | isSpace c -> discard 1 >> lexWhitespace+ _ -> return ()++-- | Returns true iff the symbol is a bracket, i.e. has the general Unicode category+-- @OpenPunctuation@ or @ClosePunctuation@.+isBracket :: Char -> Bool+isBracket c = generalCategory c `elem` [OpenPunctuation, ClosePunctuation]++-- | Converts the string representation of a decimal number to an @Integer@.+stringToNat :: String -> Integer+stringToNat = foldl (\a -> (10*a +) . toInteger . digitToInt) 0++-- | Lexes a single token.+lexToken :: Lexer Token+lexToken = do+ s <- gets input+ case s of+ -- make whitespace around commas optional+ ',':_ -> discard 1 >> return Comma++ -- brackets+ c:_ | isBracket c -> do+ discard 1+ return $ fromMaybe (Variable [c]) $ lookup c brackets++ -- all other identifiers+ | otherwise -> do+ ids <- lexWhile (\c -> not $ isSpace c || isBracket c || c == ',')+ case ids of+ "0" -> return Zero+ "1" -> return One+ _ | all isDigit ids -> let n = stringToNat ids+ in return $ if n == 0 then Variable ids+ else NatLit n+ _ -> return $ fromMaybe (Variable ids) $ lookup ids reserved++ _ -> fail $ "lexToken: interal error"+++{- |+ Runs a lexer inside the parser monad. A new parser is constructed that runs the lexer,+ applies the read token to the passed continuation and runs the resulting parser of the+ continuation with the new input string and location.+-}+lex :: (Loc Token -> Parser a) -> Parser a+lex cont = Parser $ \s loc ->+ case runState lexInput $ LexerState s loc of+ (Nothing, _) -> Left $ Loc loc $ "lexer error at " ++ showSrcLoc loc+ (Just t, LexerState s' loc') -> runParser (cont (Loc loc t)) s' loc'++-- | Tokenizes a string to a list of @Token@ values with their corresponding locations. This+-- function can be used for testing purposes.+tokenize :: String -> [Loc Token]+tokenize s = run . snd . runState lexWhitespace $ LexerState s (1,1)+ where+ run st = case runState lexInput st of+ (Nothing, _) -> []+ (Just EOF, _) -> []+ (Just tok, st') -> Loc (loc st) tok : run st'+++-- * Parser monad++-- | Parser result which is either an error message with the location the error occured or a value.+type ParseResult a = Either (Loc String) a++-- | Type for the parser monad.+newtype Parser a = Parser { runParser :: String -> SrcLoc -> ParseResult a }++instance Monad Parser where+ return a = Parser $ \_ _ -> Right a+ p >>= f = Parser $ \s loc -> case runParser p s loc of+ Left e -> Left e+ Right a -> runParser (f a) s loc+ fail s = Parser $ \_ loc -> Left $ Loc loc s+++-- | Initializes a parser by lexing all whitespace before the first token.+initParser :: Parser a -> String -> ParseResult a+initParser p s = let (_, LexerState s' loc') = runState lexWhitespace $ LexerState s (1,1)+ in runParser p s' loc'
+ Tempus/Loc.hs view
@@ -0,0 +1,23 @@+-- | Support for source locations.+module Tempus.Loc (+ SrcLoc,+ showSrcLoc,++ Loc (..),+ unLoc+) where+++-- | A source location, where the first value indicates the line and the second the column number+type SrcLoc = (Int, Int)++-- | Converts a source location to a string.+showSrcLoc :: SrcLoc -> String+showSrcLoc (l, c) = concat [show l, ":", show c]++-- | A value together with a source location.+data Loc a = Loc SrcLoc a deriving (Show, Eq)++-- | Unwraps the value and discards the location.+unLoc :: Loc a -> a+unLoc (Loc _ a) = a
+ Tempus/Main.hs view
@@ -0,0 +1,20 @@+module Main (main) where++import Paths_tempus++import Control.Monad++import System.Environment.Executable+import System.Directory+import System.FilePath++import Tempus.Interpreter+++main :: IO ()+main = do+ (path1, _) <- splitExecutablePath+ path2 <- getDataDir+ files <- filterM doesFileExist . map (</> "Prelude.tp") $ [".", path1, path2]++ repl $ head $ take 1 (map Just files) ++ [Nothing]
+ Tempus/Parser.y view
@@ -0,0 +1,226 @@+{+{-# OPTIONS_GHC -w #-}+module Tempus.Parser (+ parseProgram,+ parseDecl,+ parseType,+ parseExpr+) where++import Prelude hiding (lex)++import Tempus.Loc+import Tempus.Lexer+import Tempus.Syntax++}++%name pparseProgram prog+%name pparseDecl decl+%name pparseType type+%name pparseExpr expr++%tokentype { Loc Token }+%monad { Parser }+%lexer { lex } { Loc _ EOF }++%error { parseError }+%token+ var { Loc _ (Variable _) }+ natlit { Loc _ (NatLit _) }+ '=' { Loc $$ Equals }+ '->' { Loc $$ ArrowRight }+ '+' { Loc $$ Plus }+ '*' { Loc $$ Times }+ '(' { Loc $$ ParenOpen }+ ')' { Loc $$ ParenClose }+ '0' { Loc $$ Zero }+ '1' { Loc $$ One }+ mu { Loc $$ Mu }+ nu { Loc $$ Nu }+ '.' { Loc $$ Dot }+ ',' { Loc $$ Comma }+ lam { Loc $$ Lambda }+ '[' { Loc $$ SquareOpen }+ ']' { Loc $$ SquareClose }+ langle { Loc $$ AngleOpen }+ rangle { Loc $$ AngleClose }+ '<*>' { Loc $$ CircledAsterisk }+ '<.>' { Loc $$ CircledDot }+ '?' { Loc $$ QuestionMark }+ 'behavior' { Loc $$ KWBehavior }+ 'case' { Loc $$ KWCase }+ 'const' { Loc $$ KWConst }+ 'event' { Loc $$ KWEvent }+ 'expand' { Loc $$ KWExpand }+ 'first' { Loc $$ KWFirst }+ 'fold' { Loc $$ KWFold }+ 'left' { Loc $$ KWLeft }+ 'positive' { Loc $$ KWPositive }+ 'never' { Loc $$ KWNever }+ 'pack' { Loc $$ KWPack }+ 'race' { Loc $$ KWRace }+ 'reflect' { Loc $$ KWReflect }+ 'right' { Loc $$ KWRight }+ 'second' { Loc $$ KWSecond }+ 'ultraswitch' { Loc $$ KWUltraswitch }+ 'type' { Loc $$ KWType }+ 'ultrajump' { Loc $$ KWUltrajump }+ 'unfold' { Loc $$ KWUnfold }+ 'unpack' { Loc $$ KWUnpack }+ 'value' { Loc $$ KWValue }++%%++prog :: { Program }+prog : decls { reverse $1 }++decls :: { [Decl] }+decls : { [] }+ | decls decl { $2 : $1 }++decl :: { Decl }+decl : typedecl { $1 }+ | valdecl { $1 }++typedecl :: { Decl }+typedecl : 'type' var formalargs '=' type { DeclType $1 (var $2) (reverse $3) $5 }++formalargs :: { [Var] }+formalargs : { [] }+ | formalargs var { var $2 : $1 }++valdecl :: { Decl }+valdecl : 'value' var '=' expr { DeclVal $1 (var $2) $4 }++type :: { Type }+type : type0 { $1 }++type0 :: { Type }+type0 : mutype { TyMu $1 }+ | nutype { TyNu $1 }+ | type1 { $1 }++type1 :: { Type }+type1 : type2 '->' type1 { TyFun $1 $3 }+ | type2 { $1 }++type2 :: { Type }+type2 : type3 '+' type2 { TyPlus $1 $3 }+ | type3 { $1 }++type3 :: { Type }+type3 : type4 '*' type3 { TyPair $1 $3 }+ | type4 { $1 }++type4 :: { Type }+type4 : var typeargs { TyApp (var $1) $2 }+ | 'behavior' type5 { TyBehav $2 }+ | 'event' type5 { TyEvent $2 }+ | type5 { $1 }++type5 :: { Type }+type5 : var { TyApp (var $1) [] }+ | 'positive' { TyNat }+ | '(' type0 ')' { $2 }+ | '0' { TyZero }+ | '1' { TyUnit }++typeargs :: { [Type] }+typeargs : type5 { [$1] }+ | typeargs type5 { $2 : $1 }++mutype :: { MuType }+mutype : mu var '.' type0 { MuType (var $2) $4 }++nutype :: { NuType }+nutype : nu var '.' type0 { NuType (var $2) $4 }++expr :: { Expr }+expr : expr0 { $1 }++expr0 :: { Expr }+expr0 : expr1 ',' expr0 { ExPair $1 $3 }+ | expr1 { $1 }++expr1 :: { Expr }+expr1 : lam var '.' expr1 { ExLam (var $2) $4 }+ | expr2 { $1 }++expr2 :: { Expr }+expr2 : expr2 '<*>' expr3 { ExLiftAppB $1 $3 }+ | expr2 '<.>' expr3 { ExLiftAppE $1 $3 }+ | expr3 { $1 }++expr3 :: { Expr }+expr3 : expr3 expr4 { ExApp $1 $2 }+ | 'const' expr4 { ExConst $2 }+ | 'behavior' expr4 { ExBehav $2 }+ | 'event' expr4 expr4 { ExEvent $2 $3 }+ | foldvals '[' type ']' expr4 { $1 $3 $5 }+ | expr4 { $1 }++expr4 :: { Expr }+expr4 : var { ExVar $ var $1 }+ | '1' { ExNatLit 1 }+ | natlit { ExNatLit $ nat $1 }+ | '(' expr0 ')' { $2 }+ | '?' { ExNull }+ | langle rangle { ExUnit }+ | '(' ')' { ExUnit }+ | packvals '[' type ']' { $1 $3 }+ | baseval { $1 }++foldvals :: { Type -> Expr -> Expr }+foldvals : 'fold' { ExFold }+ | 'unfold' { ExUnfold }++packvals :: { Type -> Expr }+packvals : 'pack' { ExPack }+ | 'unpack' { ExUnpack }++baseval :: { Expr }+baseval : 'left' { ExLeft }+ | 'right' { ExRight }+ | 'case' { ExCase }+ | 'first' { ExFst }+ | 'second' { ExSnd }+ | 'expand' { ExExpand }+ | 'never' { ExNever }+ | 'race' { ExRace }+ | 'reflect' { ExReflect }+ | 'ultraswitch' { ExUSwitch }+ | 'ultrajump' { ExUJump }+++{++-- | Parses a complete Tempus program.+parseProgram :: String -> ParseResult Program+parseProgram = initParser pparseProgram++-- | Parses a single Tempus type or value declaration.+parseDecl :: String -> ParseResult Decl+parseDecl = initParser pparseDecl++-- | Parses a Tempus type expression.+parseType :: String -> ParseResult Type+parseType = initParser pparseType++-- | Parses a Tempus expression.+parseExpr :: String -> ParseResult Expr+parseExpr = initParser pparseExpr+++var :: Loc Token -> Var+var (Loc _ (Variable v)) = Var v+var _ = error "internal parser error: unexpected token in var"++nat :: Loc Token -> Integer+nat (Loc _ (NatLit i)) = i+nat _ = error "internal parser error: unexpected token in nat"++parseError :: Loc Token -> Parser a+parseError (Loc loc tok) = fail $ "error parsing token `" ++ showToken tok ++ "' at " ++ show loc++}
+ Tempus/Syntax.hs view
@@ -0,0 +1,186 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleInstances #-}++-- | Tempus abstract syntax tree types.+module Tempus.Syntax (+ Program,+ Decl (..),+ Type (..),+ MuType (..),+ NuType (..),+ Expr (..),+ Var (..),++ SrcCode (..)+) where++import Data.Data+import Data.Generics.Uniplate.Data ()+import Data.List++import Tempus.Loc+++-- | A Tempus program as a list of definitions.+type Program = [Decl]++-- | A Tempus type or value definition.+data Decl = DeclType SrcLoc Var [Var] Type+ | DeclVal SrcLoc Var Expr+ deriving (Eq, Show)+++-- | A Tempus type.+data Type = TyMu MuType+ | TyNu NuType+ | TyFun Type Type+ | TyPlus Type Type+ | TyPair Type Type+ | TyApp Var [Type]+ | TyBehav Type+ | TyEvent Type+ | TyNat+ | TyZero+ | TyUnit++ -- only used for type checking+ | TyVar Integer+ | TyCon Integer+ deriving (Eq, Show, Data, Typeable)+++-- | A mu type.+data MuType = MuType Var Type+ deriving (Eq, Show, Data, Typeable)+++-- | A nu type.+data NuType = NuType Var Type+ deriving (Eq, Show, Data, Typeable)+++-- | A Tempus expression.+data Expr = ExPair Expr Expr+ | ExLam Var Expr+ | ExLiftAppB Expr Expr+ | ExLiftAppE Expr Expr+ | ExApp Expr Expr+ | ExConst Expr+ | ExVar Var+ | ExNatLit Integer+ | ExBehav Expr+ | ExEvent Expr Expr+ | ExNull+ | ExUnit+ | ExLeft+ | ExRight+ | ExCase+ | ExExpand+ | ExFst+ | ExSnd+ | ExNever+ | ExRace+ | ExReflect+ | ExFold Type Expr+ | ExUnfold Type Expr+ | ExPack Type+ | ExUnpack Type+ | ExUJump+ | ExUSwitch+ deriving (Eq, Show, Data, Typeable)+++-- | A variable.+newtype Var = Var String deriving (Eq, Show, Data, Typeable)+++-- | Wrapper for displaying values as source code.+newtype SrcCode a = SrcCode a++instance Show (SrcCode Decl) where+ showsPrec _ (SrcCode (DeclType _ v vs t)) = + showString "type " . showsVars (map SrcCode (v:vs)) . showString " = " . shows (SrcCode t)+ showsPrec _ (SrcCode (DeclVal _ v e)) = + showString "value " . shows (SrcCode v) . showString " = " . shows (SrcCode e)++showsVars :: [SrcCode Var] -> ShowS+showsVars [] = id+showsVars [v] = shows v+showsVars (v:vs) = shows v . showChar ' ' . showsVars vs++instance Show (SrcCode Expr) where+ showsPrec p (SrcCode (ExPair e1 e2)) = showParen (p > 0) $+ showsPrec 1 (SrcCode e1) . showString " , " . showsPrec 0 (SrcCode e2)+ showsPrec p (SrcCode (ExLam v e)) = showParen (p > 1) $+ showString "\\ " . shows (SrcCode v) . showString " . " . showsPrec 1 (SrcCode e)+ showsPrec p (SrcCode (ExLiftAppB e1 e2)) = showParen (p > 2) $+ showsPrec 2 (SrcCode e1) . showString " <*> " . showsPrec 3 (SrcCode e2)+ showsPrec p (SrcCode (ExLiftAppE e1 e2)) = showParen (p > 2) $+ showsPrec 2 (SrcCode e1) . showString " <.> " . showsPrec 3 (SrcCode e2)+ showsPrec p (SrcCode (ExApp e1 e2)) = showParen (p > 3) $+ showsPrec 3 (SrcCode e1) . showChar ' ' . showsPrec 4 (SrcCode e2)+ showsPrec p (SrcCode (ExConst e)) = showParen (p > 3) $+ showString "const " . showsPrec 4 (SrcCode e)+ showsPrec p (SrcCode (ExBehav f)) = showParen (p > 3) $+ showString "behavior " . showsPrec 4 (SrcCode f)+ showsPrec p (SrcCode (ExEvent t e)) = showParen (p > 3) $+ showString "event " . showsPrec 4 (SrcCode t) . showChar ' ' . showsPrec 4 (SrcCode e)+ showsPrec p (SrcCode (ExFold t f)) = showParen (p > 3) $+ showString "fold [" . shows (SrcCode t) . showString "] " . showsPrec 4 (SrcCode f)+ showsPrec p (SrcCode (ExUnfold t f)) = showParen (p > 3) $+ showString "unfold [" . shows (SrcCode t) . showString "] " . showsPrec 4 (SrcCode f)+ showsPrec _ (SrcCode (ExVar v)) = shows (SrcCode v)+ showsPrec _ (SrcCode (ExNatLit i)) = shows i+ showsPrec _ (SrcCode ExNull) = showChar '?'+ showsPrec _ (SrcCode ExUnit) = showString "()"+ showsPrec _ (SrcCode ExLeft) = showString "left"+ showsPrec _ (SrcCode ExRight) = showString "right"+ showsPrec _ (SrcCode ExCase) = showString "case"+ showsPrec _ (SrcCode ExFst) = showString "first"+ showsPrec _ (SrcCode ExSnd) = showString "second"+ showsPrec _ (SrcCode ExExpand) = showString "expand"+ showsPrec _ (SrcCode ExNever) = showString "never"+ showsPrec _ (SrcCode ExRace) = showString "race"+ showsPrec _ (SrcCode ExReflect) = showString "reflect"+ showsPrec _ (SrcCode ExUSwitch) = showString "ultraswitch"+ showsPrec _ (SrcCode (ExPack t)) = showString "pack [" . shows (SrcCode t) . showChar ']'+ showsPrec _ (SrcCode (ExUnpack t)) = showString "unpack [" . shows (SrcCode t) . showChar ']'+ showsPrec _ (SrcCode ExUJump) = showString "ultrajump"++instance Show (SrcCode Type) where+ showsPrec p (SrcCode (TyMu mu)) = showParen (p > 0) $ shows (SrcCode mu)+ showsPrec p (SrcCode (TyNu nu)) = showParen (p > 0) $ shows (SrcCode nu)+ showsPrec p (SrcCode (TyFun t1 t2)) = showParen (p > 1) $+ showsPrec 2 (SrcCode t1) . showString " -> " . showsPrec 1 (SrcCode t2)+ showsPrec p (SrcCode (TyPlus t1 t2)) = showParen (p > 2) $+ showsPrec 3 (SrcCode t1) . showString " + " . showsPrec 2 (SrcCode t2)+ showsPrec p (SrcCode (TyPair t1 t2)) = showParen (p > 3) $+ showsPrec 4 (SrcCode t1) . showString " * " . showsPrec 3 (SrcCode t2)+ showsPrec p (SrcCode (TyApp v [])) = shows (SrcCode v)+ showsPrec p (SrcCode (TyApp v vs)) = showParen (p > 4) $+ foldl (\f t -> f . showChar ' ' . (showsPrec 5 . SrcCode $ t)) (shows . SrcCode $ v) vs+ showsPrec p (SrcCode (TyBehav t)) = showParen (p > 4) $+ showString "behavior " . showsPrec 5 (SrcCode t)+ showsPrec p (SrcCode (TyEvent t)) = showParen (p > 4) $+ showString "event " . showsPrec 5 (SrcCode t)+ showsPrec _ (SrcCode TyNat) = showString "positive"+ showsPrec _ (SrcCode TyZero) = showChar '0'+ showsPrec _ (SrcCode TyUnit) = showChar '1'+ showsPrec _ (SrcCode (TyVar i)) = showChar '_' . showShortVar ['a'..'z'] 'v' i+ showsPrec _ (SrcCode (TyCon i)) = showChar '_' . showShortVar ['A'..'Z'] 'T' i++showShortVar :: [Char] -> Char -> Integer -> ShowS+showShortVar ls c i = if i<26 then showChar $ ls !! (fromInteger i)+ else showChar c . shows (i-26)++instance Show (SrcCode MuType) where+ showsPrec _ (SrcCode (MuType x t)) =+ showString "mu " . shows (SrcCode x) . showString " . " . showsPrec 1 (SrcCode t)+++instance Show (SrcCode NuType) where+ showsPrec _ (SrcCode (NuType x t)) =+ showString "nu " . shows (SrcCode x) . showString " . " . showsPrec 1 (SrcCode t)+++instance Show (SrcCode Var) where+ showsPrec _ (SrcCode (Var s)) = showString s
+ Tempus/TypeCheck.hs view
@@ -0,0 +1,468 @@+-- | Semantical analysis (i.e. type check and variances test) for Tempus expressions.+module Tempus.TypeCheck (+ TypeEnv,+ TypeSynEnv,+ ContextError (..),++ checkProgram,+ getType,+ substVar,+ expandTypeSyn,+ expandMuType,+ expandNuType,++ Variance (..),+ invertVariance+) where+++import Control.Applicative+import Control.Arrow+import Control.Monad.Error+import Control.Monad.State++import Data.Generics.Uniplate.Operations+import Data.Function+import Data.List+import Data.Maybe++import Tempus.Loc+import Tempus.Syntax+++-- | Type check monad.+type T a = ErrorT ContextError (State TState) a++-- | A general context check error.+data ContextError = UndefinedVariable Var -- ^ Undefined global variable+ | DuplicateVariable Var -- ^ Variable defined twice+ | DuplicateType Var -- ^ Type defined twice+ | OccursCheck Type Type -- ^ Occurs check failed when trying to unify the types+ | SymbolClash Type Type -- ^ The types cannot be unified due to different+ -- outer-most constructors+ | IncorrectVariances Type -- ^ Incorrect variances+ | UndefinedType Var -- ^ Undefined type synonym or free type variable used+ | TypeArgsMismatch Var -- ^ Wrong number of arguments for the type synonym+ | NoMuType Type -- ^ Type has to be a mu type but isn't+ | NoNuType Type -- ^ Type has to be a nu type but isn't+ | NoRecType Type -- ^ Type has to be a recursive type but isn't+ deriving (Show)+++instance Error ContextError where+ noMsg = error "noMsg not implemented for Error ContextError"+ strMsg msg = error "strMsg not implemented for Error ContextError"++instance Error e => Error (Loc e) where+ noMsg = error "noMsg not implemented for Error (Loc e)"+ strMsg msg = error "stdMsg not implemented for Error (Loc e)"+++-- | Type check state.+data TState = TState {+ -- | The ID to use for the next fresh type variable.+ varID :: Integer,+ -- | The ID to use for the next fresh type constructor variable.+ conID :: Integer+ } deriving (Eq, Show)+++-- | Initial type check state.+initTState :: TState+initTState = TState { varID = 0, conID = 0 }+++{- |+ Performs a semantical analysis for a module using the given global variables with types and+ type synonyms. Either a context error with source location or lists with the global variables+ and their inferred types and type synonyms is returned.+-}+checkProgram :: TypeEnv -> TypeSynEnv -> Program+ -> Either (Loc ContextError) (TypeEnv, TypeSynEnv)+checkProgram tEnv sEnv prog =+ fst $ runState (runErrorT $ checkDecls tEnv [] sEnv [] prog) initTState++-- | Helper function for 'checkProgram'.+checkDecls :: TypeEnv -> TypeEnv -> TypeSynEnv -> TypeSynEnv -> [Decl]+ -> ErrorT (Loc ContextError) (State TState) (TypeEnv, TypeSynEnv)+checkDecls _ tEnv' _ sEnv'[] = return (reverse tEnv', reverse sEnv')+checkDecls tEnv tEnv' sEnv sEnv' (DeclType loc v vs t : ds) = do+ when (not . null $ filter ((== v) . fst) $ sEnv ++ sEnv') $+ throwError $ Loc loc $ DuplicateType v+ checkDecls tEnv tEnv' sEnv ((v, (vs, t)) : sEnv') ds+checkDecls tEnv tEnv' sEnv sEnv' (DeclVal loc v e : ds) = do+ let env = tEnv ++ tEnv'+ builtIns = map (\v -> (Var v, undefined)) ["add", "mult"]+ when (not . null $ filter ((== v) . fst) (env ++ builtIns)) $+ throwError $ Loc loc $ DuplicateVariable v+ t <- addErrorLoc loc $ checkedTypeExpr env (sEnv ++ sEnv') e+ checkDecls tEnv ((v, generalize t) : tEnv') sEnv sEnv' ds+++-- | Infer the most general type for an expression using the types from a list of global variables+-- and a list of type synonyms.+getType :: TypeEnv -> TypeSynEnv -> Loc Expr -> Either (Loc ContextError) Type+getType tEnv sEnv (Loc loc e) =+ fst $ runState (runErrorT $ addErrorLoc loc $ checkedTypeExpr tEnv sEnv e) initTState+++-- TODO: Remove type schemes?+-- | Type schemes.+type TypeScheme = ([Integer], Type)++-- | A type environment as a list of variables with their types.+type TypeEnv = [(Var, TypeScheme)]++-- | A substitution as a list of pairs of type variable IDs and the types of the corresponding+-- type variables.+type Subst = [(Integer, Type)]++-- | A type synonym environment as a list of pairs of a type synonym name with its parameter+-- names and type.+type TypeSynEnv = [(Var, ([Var], Type))]+++-- | Transforms an error monad by adding a location information to the error type.+addErrorLoc :: (Error e, Functor m) => SrcLoc -> ErrorT e m a -> ErrorT (Loc e) m a+addErrorLoc loc = mapErrorT (fmap . left $ Loc loc)+++-- | Perform a type inference with variance test within the @T@ monad for an expression, using the+-- given global variables with types and type synonyms.+checkedTypeExpr :: TypeEnv -> TypeSynEnv -> Expr -> T Type+checkedTypeExpr tEnv sEnv e = do+ t <- snd <$> typeExpr tEnv [] sEnv e+ var <- correctVariances sEnv t+ when (not $ var) $+ throwError $ IncorrectVariances t+ return t++-- | Performs a type inference for an expression. Returns the inferred type with a substitution+-- for the used type variables.+typeExpr :: TypeEnv -- ^ Global type environment+ -> TypeEnv -- ^ Local type environment+ -> TypeSynEnv -- ^ Type synonym environment+ -> Expr -- ^ Expression+ -> T (Subst, Type)+typeExpr gamma lambda sEnv e =+ case e of+ -- TODO: Put somewhere else+ ExVar (Var v)+ | v `elem` ["add", "mult"]+ -> return ([], TyFun TyNat $ TyFun TyNat TyNat)+ ExVar v -> case lookup v (lambda ++ gamma) of+ Just s -> (\t -> ([], t)) <$> instantiate s+ Nothing -> throwError $ UndefinedVariable v+ ExLam x e -> do+ b <- freshVar+ (s, t) <- typeExpr (deleteBy ((==) `on` fst) (x, undefined) gamma)+ (replVar (x, b) lambda) sEnv e+ return (s, TyFun (substType s b) t)+ ExApp e1 e2 -> do+ b <- freshVar+ (s1, t1) <- typeExpr gamma lambda sEnv e1+ (s2, t2) <- typeExpr gamma (substEnv s1 lambda) sEnv e2+ s3 <- mgu sEnv (substType s2 t1) (TyFun t2 b) []+ return (compSubst s3 $ compSubst s2 s1, substType s3 b)+ ExPair e1 e2 -> do+ (s1, t1) <- typeExpr gamma lambda sEnv e1+ (s2, t2) <- typeExpr gamma (substEnv s1 lambda) sEnv e2+ return (compSubst s2 s1, TyPair (substType s2 t1) t2)+{-+ ExLiftApp e1 e2 -> do+ (s1, t1) <- typeExpr gamma lambda e1+ [c, d] <- replicateM 2 freshVar+ s2 <- mgu (TyBehav $ TyFun c d) t1 []+ (s3, t2) <- typeExpr gamma (substEnv (compSubst s2 s1) lambda) e2+ s4 <- mgu (substType (compSubst s2 s1) $ TyBehav c) t2 []+ return (compSubst s4 $ compSubst s3 $ compSubst s2 s1, substType s4 $ TyBehav d)+-}+ -- TODO: rewrite+ ExLiftAppB e1 e2 -> do+ (s2', t1) <- typeExpr gamma lambda sEnv e1+ [a, b, c, d] <- replicateM 4 freshVar+ s3' <- mgu sEnv (TyFun (TyBehav $ TyFun c d)+ (TyFun (TyBehav c) (TyBehav d))) (TyFun t1 a) []+ (s2, t2) <- typeExpr gamma (substEnv (compSubst s3' s2') lambda) sEnv e2+ s3 <- mgu sEnv (substType (compSubst s2 s3') a) (TyFun t2 b) []+ return (compSubst s3 $ compSubst s2 $ compSubst s3' s2', substType s3 b)+ -- TODO: rewrite+ ExLiftAppE e1 e2 -> do+ (s2', t1) <- typeExpr gamma lambda sEnv e1+ [a, b, c, d] <- replicateM 4 freshVar+ s3' <- mgu sEnv (TyFun (TyBehav $ TyFun c d)+ (TyFun (TyEvent c) (TyEvent d))) (TyFun t1 a) []+ (s2, t2) <- typeExpr gamma (substEnv (compSubst s3' s2') lambda) sEnv e2+ s3 <- mgu sEnv (substType (compSubst s2 s3') a) (TyFun t2 b) []+ return (compSubst s3 $ compSubst s2 $ compSubst s3' s2', substType s3 b)+ ExConst e -> do+ (_, t) <- typeExpr gamma [] sEnv e+ return ([], TyBehav t)+ ExBehav f -> do+ (_, t) <- typeExpr gamma [] sEnv f+ a <- freshVar+ s <- mgu sEnv (TyFun TyNat a) t []+ return (s, substType s (TyBehav a))+ ExEvent t e -> do+ (s1, t1) <- typeExpr gamma lambda sEnv t+ s2 <- mgu sEnv TyNat t1 []+ (_, t2) <- typeExpr gamma [] sEnv e+ return (compSubst s2 s1, TyEvent t2)+ ExFold t f -> do+ mu@(MuType a t1) <- either throwError return $ expandMuType sEnv t+ (_, t2) <- typeExpr gamma [] sEnv f+ b <- freshVar+ s <- mgu sEnv (TyFun (substVar a b t1) b) t2 []+ return (s, substType s $ TyFun (TyMu mu) b)+ ExUnfold t f -> do+ nu@(NuType a t1) <- either throwError return $ expandNuType sEnv t+ (_, t2) <- typeExpr gamma [] sEnv f+ b <- freshVar+ s <- mgu sEnv (TyFun b (substVar a b t1)) t2 []+ return (s, substType s $ TyFun b (TyNu nu))+ -- TODO: throw returned error, not NoRecType+ ExPack t -> case (expandMuType sEnv t, expandNuType sEnv t) of+ (Right s@(MuType x t), Left _) -> return ([], TyFun (substVar x (TyMu s) t) (TyMu s))+ (Left _, Right s@(NuType x t)) -> return ([], TyFun (substVar x (TyNu s) t) (TyNu s))+ (Left _, Left _) -> throwError $ NoRecType t+ ExUnpack t -> case (expandMuType sEnv t, expandNuType sEnv t) of+ (Right s@(MuType x t), Left _) -> return ([], TyFun (TyMu s) (substVar x (TyMu s) t))+ (Left _, Right s@(NuType x t)) -> return ([], TyFun (TyNu s) (substVar x (TyNu s) t))+ (Left _, Left _) -> throwError $ NoRecType t+ _ -> (\t -> ([], t)) <$> typeSimple e+++-- | Looks up a variable name in the type synonym list and applies the type synonym to the list of+-- argument types. Either a context error or the expanded type is returned.+expandTypeSyn :: TypeSynEnv -> Var -> [Type] -> Either ContextError Type+expandTypeSyn env v ts = case lookup v env of+ Nothing -> Left $ UndefinedType v+ Just (vs, t)+ | length vs == length ts -> Right $ foldr (uncurry substVar) t $ zip vs ts+ | otherwise -> Left $ TypeArgsMismatch v++-- | Tries to expand a type to a mu type. If the resulting type isn't a mu type, an error is+-- returned, otherwise, the mu type is returned.+expandMuType :: TypeSynEnv -> Type -> Either ContextError MuType+expandMuType sEnv (TyMu mu) = Right mu+expandMuType sEnv (TyApp v ts) = expandTypeSyn sEnv v ts >>= expandMuType sEnv+expandMuType sEnv t = Left $ NoMuType t++-- | Tries to expand a type to a nu type. If the resulting type isn't a nu type, an error is+-- returned, otherwise, the nu type is returned.+expandNuType :: TypeSynEnv -> Type -> Either ContextError NuType+expandNuType sEnv (TyNu nu) = Right nu+expandNuType sEnv (TyApp v ts) = expandTypeSyn sEnv v ts >>= expandNuType sEnv+expandNuType sEnv t = Left $ NoNuType t++-- | Instantiates a type scheme to a type.+instantiate :: TypeScheme -> T Type+instantiate (vs, t) = do+ bs <- replicateM (length vs) freshVar+ return $ substType (zip vs bs) t++-- TODO: condense type vars+-- | Generalizes a type to a type scheme.+generalize :: Type -> TypeScheme+generalize t = (ftv t, t)++-- | Returns the free type variables of a type as a list of type variable IDs.+ftv :: Type -> [Integer]+ftv = nub . ftv'+ where+ ftv' (TyVar i) = [i]+ ftv' t = concatMap ftv' $ children t+++-- | Compose two substitutions to a new one.+compSubst :: Subst -> Subst -> Subst+compSubst sigma theta = let theta' = map (second $ substType sigma) theta+ sigma' = let domTheta = map fst theta+ in [ (x,t) | (x,t) <- sigma, x `notElem` domTheta ]+ theta'' = [ (x,t) | (x,t) <- theta', t /= TyVar x ]+ in nub $ theta'' ++ sigma'++{-+-- defined in Baader+compSubst :: Subst' -> Subst' -> Subst'+compSubst sigma theta = let sigma' = map (second $ substType theta) sigma+ theta' = let domSigma = map fst sigma+ in [ (x,t) | (x,t) <- theta, x `notElem` domSigma ]+ sigma'' = [ (x,t) | (x,t) <- sigma', t /= TyVar x ]+ in nub $ sigma'' ++ theta'+-}++-- | Apply a substitution to each type in the type environment.+substEnv :: Subst -> TypeEnv -> TypeEnv+substEnv s = map (second $ second $ substType s)++-- | Apply a substitution to a type.+substType :: Subst -> Type -> Type+substType s t = transform f t+ where+ f (TyVar i) = fromMaybe (TyVar i) $ lookup i s+ f t = t++-- | Add, or replace if already present, a variable with a type in a list of variables with types.+replVar :: (Var, Type) -> TypeEnv -> TypeEnv+replVar (v,t) = ((v, ([], t)):) . filter ((/= v) . fst)+++-- version Baader, Unification Theory; see also Heeren, Top Quality Type Error Messages+-- | Try to unify two types using a type synonym list and an initial substitution.+mgu :: TypeSynEnv -> Type -> Type -> Subst -> T Subst+mgu sEnv t1 t2 s =+ case (condSubst t1, condSubst t2) of+ (TyVar x, TyVar y)+ | x == y -> return []+ (TyVar x, t)+ | x `occursIn` t -> throwError $ OccursCheck (TyVar x) t+ | otherwise -> return $ compSubst [(x, t)] s+ (t1, t2@(TyVar _)) -> mgu sEnv t2 t1 s+ (TyMu (MuType x1 t1), TyMu (MuType x2 t2)) -> do+ c <- freshCon+ mgu sEnv (substVar x1 c t1) (substVar x2 c t2) []+ (TyNu (NuType x1 t1), TyNu (NuType x2 t2)) -> do+ c <- freshCon+ mgu sEnv (substVar x1 c t1) (substVar x2 c t2) []+ (TyApp v ts, t) -> either throwError (\t' -> mgu sEnv t' t s) $ expandTypeSyn sEnv v ts+ (t, TyApp v ts) -> either throwError (\t' -> mgu sEnv t t' s) $ expandTypeSyn sEnv v ts+ (t1, t2)+ | equalSymbols t1 t2 -> unifySubterms (children t1) (children t2) s+ | otherwise -> throwError $ SymbolClash t1 t2+ where+ condSubst t@(TyVar _) = substType s t+ condSubst t = t++ equalSymbols t1 t2 = case (t1, t2) of+ (TyFun _ _, TyFun _ _) -> True+ (TyPlus _ _, TyPlus _ _) -> True+ (TyPair _ _, TyPair _ _) -> True+ (TyBehav _, TyBehav _) -> True+ (TyEvent _, TyEvent _) -> True+ (TyNat, TyNat) -> True+ (TyZero, TyZero) -> True+ (TyUnit, TyUnit) -> True+ (TyCon x, TyCon y) -> x == y+ _ -> False++ -- TODO: use foldM+ unifySubterms [] [] sigma = return sigma+ unifySubterms (s:ss) (t:ts) sigma = do+ sigma' <- mgu sEnv s t sigma+ unifySubterms ss ts $ compSubst sigma sigma'+ unifySubterms _ _ _ = error "unifySubterms: same symbols with different arities"++-- | Check if a type variable with the given ID occurs in the type.+occursIn :: Integer -> Type -> Bool+occursIn x t = x `elem` [ y | TyVar y <- universe t]++-- | @substVar v s t@ replaces all occurrences of @v@ in @t@ by @s@. @v@ is not replaced if it is+-- bound locally by a mu type.+substVar :: Var -> Type -> Type -> Type+substVar x s t@(TyMu (MuType y t'))+ | x == y = t+ | otherwise = TyMu (MuType y $ substVar x s t')+substVar x s t@(TyNu (NuType y t'))+ | x == y = t+ | otherwise = TyNu (NuType y $ substVar x s t')+substVar x s t@(TyApp y [])+ | x == y = s+ | otherwise = t+substVar x s t = descend (substVar x s) t++-- | Returns the type of a Tempus primitive expression.+typeSimple :: Expr -> T Type+typeSimple e =+ case e of+ ExNatLit _ -> return $ TyNat+ ExNull -> TyFun TyZero <$> freshVar+ ExUnit -> return $ TyUnit+ ExLeft -> fresh2 $ \t1 t2 -> TyFun t1 (TyPlus t1 t2)+ ExRight -> fresh2 $ \t1 t2 -> TyFun t2 (TyPlus t1 t2)+ ExCase -> fresh3 $ \t1 t2 s -> TyFun (TyFun t1 s) $+ TyFun (TyFun t2 s) $ TyFun (TyPlus t1 t2) s+ ExFst -> fresh2 $ \t1 t2 -> TyFun (TyPair t1 t2) t1+ ExSnd -> fresh2 $ \t1 t2 -> TyFun (TyPair t1 t2) t2+ ExExpand -> fresh1 $ \t -> TyFun (TyBehav t) (TyBehav $ TyPair t (TyBehav t))+ ExNever -> return $ TyEvent TyZero+ ExRace -> fresh2 $ \t1 t2 -> TyFun (TyEvent t1) $+ TyFun (TyEvent t2) $+ TyEvent $ TyPlus (TyPair t1 t2) $+ TyPlus (TyPair t1 $ TyEvent t2)+ (TyPair t2 $ TyEvent t1)+ -- TODO: Replace n, s by new var+ ExReflect -> return $ TyFun TyNat $ TyMu $+ MuType (Var "n") (TyPlus TyUnit (TyApp (Var "n") []))+ ExUJump -> fresh1 $ \t -> TyFun (TyNu $ NuType (Var "s") $ TyEvent $+ TyPlus t (TyApp (Var "s") []))+ (TyEvent t)+ ExUSwitch -> fresh1 $ \t -> TyFun (TyNu $ NuType (Var "s") $+ TyPair (TyBehav t) $ TyEvent $ TyPair t $+ TyApp (Var "s") [])+ (TyBehav t)+ _ -> error "typeSimple: expression is not simple"++-- | Generate a new unused type variable as a type expression.+freshVar :: T Type+freshVar = do+ i <- gets varID+ modify (\st -> st { varID = varID st + 1 })+ return $ TyVar i++-- | Generate a new unused type variable as a type expression and apply the given function to that+-- type.+fresh1 :: (Type -> Type) -> T Type+fresh1 f = liftM f freshVar++-- | Like 'fresh1' but for two variables.+fresh2 :: (Type -> Type -> Type) -> T Type+fresh2 f = liftM2 f freshVar freshVar++-- | Like 'fresh1' but for three variables.+fresh3 :: (Type -> Type -> Type -> Type) -> T Type+fresh3 f = liftM3 f freshVar freshVar freshVar++-- | Generate a new unused type constructor variable as a type expression.+freshCon :: T Type+freshCon = do+ i <- gets conID+ modify (\st -> st { conID = conID st + 1 })+ return $ TyCon i+++-- | A variance.+data Variance = CoVariant | ContraVariant deriving (Eq, Show)++-- | Inverts a variance.+invertVariance :: Variance -> Variance+invertVariance CoVariant = ContraVariant+invertVariance ContraVariant = CoVariant++-- TODO: Distinguish between bound variables with wrong variances and unbound variables+-- | Perform a variances check for the type using a type synonym environment, and return @true@+-- iff the test was successful.+correctVariances :: TypeSynEnv -> Type -> T Bool+correctVariances = var []+ where+ var delta sEnv (TyApp x ts)+ | (x, CoVariant) `elem` delta = return True+ | (x, ContraVariant) `elem` delta = return False+ | otherwise = either throwError (var delta sEnv) $+ expandTypeSyn sEnv x ts+ var delta _ (TyVar x) = return True+ var _ _ TyNat = return True+ var _ _ TyZero = return True+ var _ _ TyUnit = return True+ var delta sEnv (TyBehav t) = var delta sEnv t+ var delta sEnv (TyEvent t) = var delta sEnv t+ var delta sEnv (TyPair t1 t2) = liftM2 (&&) (var delta sEnv t1) (var delta sEnv t2)+ var delta sEnv (TyPlus t1 t2) = liftM2 (&&) (var delta sEnv t1) (var delta sEnv t2)+ var delta sEnv (TyFun t1 t2) = liftM2 (&&)+ (var (map (second invertVariance) delta) sEnv t1)+ (var delta sEnv t2)+ var delta sEnv (TyMu (MuType v t)) = var (replVar (v, CoVariant) delta) sEnv t+ var delta sEnv (TyNu (NuType v t)) = var (replVar (v, CoVariant) delta) sEnv t++ replVar :: (Var, Variance) -> [(Var, Variance)] -> [(Var, Variance)]+ replVar (v,t) = ((v, t):) . filter ((/= v) . fst)
+ tempus.cabal view
@@ -0,0 +1,50 @@+Name: tempus+Version: 0.1.0+Cabal-Version: >= 1.6+Build-Type: Simple+License: BSD3+License-File: LICENSE+Copyright: (C) 2010, Matthias Reisner+Author: Matthias Reisner+Maintainer: Matthias Reisner <matthias.reisner@googlemail.com>+Stability: experimental+Synopsis: Interpreter for the FRP language Tempus+Description: This package provides an interactive console application for loading of modules,+ definition of types and values, as well as type checking and evaluation of+ expressions in the functional reactive language Tempus.+Category: FRP, Language, Compilers/Interpreters+Tested-With: GHC == 6.10.4, GHC == 6.12.1++Data-Files: Prelude.tp+Extra-Source-Files: Tempus/Examples/lightbulb.tp++Flag base4+ Description: base >= 4.0+ Default: True++Executable tempus+ Build-Tools: happy >= 1.18++ if flag(base4)+ Build-Depends: base >= 4 && < 5+ else+ Build-Depends: base >= 3.0.3 && < 4+ Build-Depends: mtl >= 1.1.0.2 && < 1.2,+ uniplate >= 1.5.1,+ array >= 0.2 && < 3,+ utf8-string >= 0.3.6,+ filepath >= 1.1.0.2,+ directory >= 1.0.0.3,+ haskeline >= 0.6.3.2,+ executable-path >= 0.0.2+ Extensions: DeriveDataTypeable,+ FlexibleInstances++ Main-Is: Tempus/Main.hs+ Other-Modules: Tempus.Loc,+ Tempus.Lexer,+ Tempus.Syntax,+ Tempus.Parser,+ Tempus.TypeCheck,+ Tempus.Evaluation,+ Tempus.Interpreter