dino (empty) → 0.1
raw patch · 17 files changed
+3538/−0 lines, 17 filesdep +ansi-wl-pprintdep +basedep +containerssetup-changed
Dependencies added: ansi-wl-pprint, base, containers, dino, errors, exceptions, hashable, monad-loops, mtl, tasty, tasty-quickcheck, tasty-th, text, transformers, tree-view, unordered-containers
Files
- LICENSE +30/−0
- README.md +169/−0
- Setup.hs +2/−0
- dino.cabal +105/−0
- examples/Examples.hs +22/−0
- examples/README.hs +110/−0
- src/Dino.hs +14/−0
- src/Dino/AST.hs +337/−0
- src/Dino/AST/Diff.hs +369/−0
- src/Dino/Expression.hs +847/−0
- src/Dino/Interpretation.hs +1033/−0
- src/Dino/Prelude.hs +64/−0
- src/Dino/Pretty.hs +93/−0
- src/Dino/Types.hs +90/−0
- src/Dino/Verification.hs +52/−0
- test/DiffTest.hs +194/−0
- test/Tests.hs +7/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2019, Mpowered Business Solutions++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 Emil Axelsson nor the names of other+ 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+OWNER 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.
+ README.md view
@@ -0,0 +1,169 @@+# Dino++Dino is a [tagless EDSL](http://okmij.org/ftp/tagless-final) supporting numeric and logic expressions, conditionals, explicit sharing, etc.++++Syntactic conveniences+--------------------------------------------------------------------------------++The module [`Dino.Expression`](https://hackage.haskell.org/package/dino/docs/Dino-Expression.html) redefines many identifiers from the prelude, so users are advised to hide the prelude when importing it. This can be done, for example, using the `NoImplicitPrelude` language extension. The main module, [`Dino`](https://hackage.haskell.org/package/dino/docs/Dino.html), exports both `Dino.Expression` and `Dino.Prelude`, where the latter is a subset of the standard prelude plus a few extra definitions.++Dino provides a newtype wrapper, `Exp`, which allows EDSL terms to be used directly as numbers and strings; for example:++```haskell+ex1 ::+ (ConstExp e, NumExp e, FracExp e, CompareExp e, CondExp e)+ => Exp e Double+ -> Exp e Text+ex1 a =+ if a > 4.5+ then "greater"+ else "smaller or equal"+```++This example also shows the use of `RebindableSyntax` to allow Haskell's `if` syntax in EDSL expressions.++Multi-way conditionals can be expressed using `cases`; for example:++```haskell+beaufortScale ::+ (ConstExp e, NumExp e, FracExp e, CompareExp e, CondExp e)+ => Exp e Double+ -> Exp e Text+beaufortScale v = cases+ [ (v < 0.5) --> "calm"+ , (v < 13.8) --> "breeze"+ , (v < 24.5) --> "gale" ]+ ( Otherwise --> "storm" )+```++Browse the [`Dino.Expression`](https://hackage.haskell.org/package/dino/docs/Dino-Expression.html) documentation to find different variations on `cases`, including a version for matching on enumerations without a fall-through case.++### A `Maybe`-like monad++Similar to the function `maybe` in the standard prelude, Dino provides the following function to deconstruct `Maybe` values:++```haskell+maybe ::+ (...)+ => e b -- ^ Result when 'nothing'+ -> (e a -> e b) -- ^ Result when 'just'+ -> e (Maybe a) -- ^ Value to deconstruct+ -> e b+```++However, it is not very convenient to use `maybe` in a nested way (i.e. when another `maybe` is needed inside the function that handles `just`). In such cases, it is much preferred to use a monadic interface. Indeed, Dino provides the type `Optional` which has a `Monad` instance and the following functions to convert to and from `e (Maybe a)`:++```haskell+suppose :: (...) => e (Maybe a) -> Optional e (e a)+runOptional :: (...) => Optional e (e a) -> e (Maybe a)+```++++Semantic conveniences+--------------------------------------------------------------------------------++On the interpretation side, most Dino constructs provide default implementations for monads (many just requiring `Applicative`), making it easy to derive interpretations for custom monads. There is also special support for intensional analysis of higher-order constructs (i.e. constructs that introduce local variables).++### Standard interpretation with special cases++For example, say that we want standard evaluation of expressions but with the ability to catch division by 0. For this, we can use a newtype around `Maybe`:++```haskell+newtype SafeDiv a = SafeDiv {fromSafeDiv :: Maybe a}+ deriving (Functor, Applicative, Monad)+```++Since `SafeDiv` is an applicative functor, we can derive a standard interpretation of syntactic classes by just declaring instances:++```haskell+instance ConstExp SafeDiv+instance NumExp SafeDiv+instance LogicExp SafeDiv+instance CompareExp SafeDiv+```++(In this particular case, we could also have used `GeneralizedNewtypeDeriving`, since there are already instances of those classes for `Maybe`.)++In order to get special semantics for division, we have to give a manual definition of `fdiv`:++```haskell+instance FracExp SafeDiv where+ fdiv _ (SafeDiv (Just 0)) = SafeDiv Nothing+ fdiv (SafeDiv a) (SafeDiv b) = SafeDiv (liftA2 (/) a b)+```++### Intensional analysis++Dino has special support for intensional interpretation of higher-order constructs (i.e. interpretations that inspect the syntax).++Consider the following two classes:++```haskell+class LetExp e where+ letE :: DinoType a+ => Text -- ^ Variable base name+ -> e a -- ^ Value to share+ -> (e a -> e b) -- ^ Body+ -> e b++class LetIntensional e where+ letI :: DinoType a+ => Text -- ^ Variable name+ -> e a+ -> e b -- ^ Body (open term)+ -> e b+```++The former is the class that is exposed to the EDSL user. It provides a convenient higher-order construct for sharing values. Here is an example of its use:++```haskell+ex2 :: Exp e Double -> Exp e Double+ex2 a = letE "x" expensive $ \x ->+ if a > 10+ then x*2+ else x*3+ where+ expensive = a*a*a*a*a*a*a*a+```++But the higher-order interface is problematic for intensional interpretations (e.g. AST extraction). The main problem is to come up with a representation of the variable to which the body can be applied. One must make sure that the chosen variable does not lead to capturing. For such interpretations, the first-order function `letI` is more suitable.++`letI` is similar to `letE`, but with some important differences:++ * The "body" argument passed to `letE` is a function while the `letI` has an open expression as body.+ * The name passed to `letE` is just a suggested *base* of the variable name. The user does not need to worry about potential name clashing.+ * The name passed to `letI` is the *actual* variable name. The caller must guarantee that this name does not clash with other variables.++The thing to note is this:++ * `letE` is *easy* to call, but *hard* to implement.+ * `letI` is *hard* to call, but *easy* to implement.++`letI` is hard to call, because it must be given a name that does not lead to capturing. But for an implementor, `letI` is very nice. Why? Because it gets a variable name from someone else, and it can directly inspect the body without first applying it to an argument.++The good news is that Dino provides the means to bridge the gap between `letE` and `letI`: the `Intensional` newtype wrapper. Given a `LetIntensional` instance for an interpretation, we can automatically derive `LetExp` by just wrapping it in `Intensional`, due to the following instance:++```haskell+instance (VarExp e, LetIntensional e) => LetExp (Intensional e)+```++In other words, you get to *define your semantics using first-order constructs and automatically derive a higher-order interface*.++As an example, the `Reified` interpretation (for AST extraction; see [Dino.Interpretation](https://hackage.haskell.org/package/dino/docs/Dino-Interpretation.html)) is an example of one that only instantiates first-order classes (`LetIntensional` and friends). But the combined type `Intensional Reified` supports a higher-order interface (`LetExp` and friends).++But what about adding new higher-order constructs? Then one must go through the work of defining an instance such as the one for `LetExp (Intensional e)` above. Fortunately, defining such instances is made very easy by the following function:++```haskell+unbind+ :: (VarExp e, DinoType a)+ => Text -- ^ Variable base name+ -> (Intensional e a -> Intensional e b) -- ^ Body parameterized by its free variable+ -> (Text, Intensional e b) -- ^ Generated variable and function body+```++It takes a body represented as a function, and returns a body as an open expression along with the generated variable name. This name is guaranteed not to lead to capturing, as long all binders are generated using the same method. There is also `unbind2`, for constructs that introduce two local variables.++For the curious reader, `unbind` is implemented using the technique in [Using Circular Programming for Higher-Order Syntax](https://emilaxelsson.github.io/documents/axelsson2013using.pdf).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ dino.cabal view
@@ -0,0 +1,105 @@+name: dino+version: 0.1+synopsis: A convenient tagless EDSL+description: For more information, see the+ <https://github.com/emilaxelsson/trackit/blob/master/README.md README>.+license: BSD3+license-file: LICENSE+author: Emil Axelsson+maintainer: 78emil@gmail.com+copyright: 2019 Mpowered Business Solutions+homepage: https://github.com/emilaxelsson/dino+bug-reports: https://github.com/emilaxelsson/dino/issues+category: Language+build-type: Simple+cabal-version: >=1.10++extra-source-files: README.md++source-repository head+ type: git+ location: https://github.com/emilaxelsson/dino.git++library+ exposed-modules: Dino.Pretty+ Dino.AST+ Dino.AST.Diff+ Dino.Prelude+ Dino.Types+ Dino.Expression+ Dino.Interpretation+ Dino.Verification+ Dino+ build-depends: base < 5,+ ansi-wl-pprint < 0.7,+ containers < 0.7,+ exceptions < 0.11,+ errors < 2.4,+ hashable < 1.3,+ monad-loops < 0.5,+ mtl < 2.3,+ text < 1.3,+ transformers < 0.6,+ tree-view < 0.6,+ unordered-containers < 0.3+ hs-source-dirs: src+ default-language: Haskell2010+ default-extensions: ConstraintKinds+ DataKinds+ DefaultSignatures+ DeriveFoldable+ DeriveFunctor+ DeriveGeneric+ DeriveTraversable+ FlexibleContexts+ FlexibleInstances+ FunctionalDependencies+ GADTs+ InstanceSigs+ MultiParamTypeClasses+ NamedFieldPuns+ NoImplicitPrelude+ OverloadedStrings+ Rank2Types+ ScopedTypeVariables+ StandaloneDeriving+ TupleSections+ TypeApplications+ TypeFamilies+ TypeOperators+ other-extensions: GeneralizedNewtypeDeriving+ PolyKinds+ ghc-options: -Wall++test-suite tests+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Tests.hs+ other-modules: DiffTest+ build-depends: base+ , dino+ , tasty < 1.3+ , tasty-quickcheck < 0.11+ , tasty-th < 0.2+ , text+ , unordered-containers+ ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N+ default-language: Haskell2010+ default-extensions: DefaultSignatures+ FlexibleInstances+ OverloadedStrings+ ScopedTypeVariables+ TupleSections++test-suite examples+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: Examples.hs+ other-modules: README+ build-depends: base >= 4.10 && < 5+ , dino+ ghc-options: -Wall+ default-language: Haskell2010+ default-extensions: NoImplicitPrelude+ OverloadedStrings+ Rank2Types
+ examples/Examples.hs view
@@ -0,0 +1,22 @@+{-# OPTIONS_GHC -Wno-missing-signatures #-}++import Dino+import Dino.Verification++import qualified README++exp1 :: (ConstExp e, NumExp e, LetExp e, AssertExp e) => Exp e Int+exp1 =+ ( share (a + b) $ \c ->+ assertEq "should_succeed" ((a + 3) * c) (b * c)+ -- Note: `c` is a free variable in the assertion+ ) + b+ where+ a = assertEq "should_fail" (1+1) (1+2)+ b = a + 3++test1 = presentStructuralVerification $ verifyAssertEqStructurally $ unExp exp1++main = do+ README.tests+ test1
+ examples/README.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RebindableSyntax #-}++{-# OPTIONS_GHC -Wno-missing-signatures #-}+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- Code from README.md++module README where++import qualified Prelude++import Control.Applicative (liftA2)++import Dino+import Dino.AST (drawTree)+import Dino.Interpretation++++--------------------------------------------------------------------------------+-- * Syntax+--------------------------------------------------------------------------------++ex1 ::+ (ConstExp e, NumExp e, FracExp e, CompareExp e, CondExp e)+ => Exp e Double+ -> Exp e Text+ex1 a =+ if a > 4.5+ then "greater"+ else "smaller or equal"++beaufortScale ::+ (ConstExp e, NumExp e, FracExp e, CompareExp e, CondExp e)+ => Exp e Double+ -> Exp e Text+beaufortScale v = cases+ [ (v < 0.5) --> "calm"+ , (v < 13.8) --> "breeze"+ , (v < 24.5) --> "gale" ]+ ( Otherwise --> "storm" )++safeDiv ::+ (ConstExp e, FracExp e, CompareExp e, CondExp e, DinoType a, Fractional a)+ => e a+ -> e a+ -> Optional e (e a)+safeDiv a b = suppose $ if (b /= lit 0)+ then just (fdiv a b)+ else nothing++foo ::+ (ConstExp e, NumExp e, FracExp e, CompareExp e, CondExp e, LetExp e)+ => Exp e Double+ -> Exp e Double+ -> Exp e Double+foo a b = fromOptional 0 $ do+ x <- safeDiv a b+ y <- safeDiv b x+ safeDiv x y++-- Let's have look at the expression generated by `foo`:++fooExp = drawTree $ unReified $ prodSnd $ unIntensional $ unExp $ foo 111 222+ -- The type of `foo` here is `Exp (Intensional Reified) Double`++++--------------------------------------------------------------------------------+-- * Semantics+--------------------------------------------------------------------------------++newtype SafeDiv a = SafeDiv {fromSafeDiv :: Maybe a}+ deriving (Functor, Applicative, Monad)++instance ConstExp SafeDiv+instance NumExp SafeDiv+instance LogicExp SafeDiv+instance CompareExp SafeDiv++instance FracExp SafeDiv where+ fdiv _ (SafeDiv (Just b))+ | b Prelude.== 0 = SafeDiv Nothing+ fdiv (SafeDiv a) (SafeDiv b) = SafeDiv (liftA2 (/) a b)++evalSafeDiv+ :: (forall e. (ConstExp e, NumExp e, FracExp e, LogicExp e, CompareExp e) => Exp e a)+ -> Maybe a+evalSafeDiv = fromSafeDiv . unExp++ex2 :: (ConstExp e, NumExp e, FracExp e, LogicExp e, CompareExp e) => Exp e Double+ex2 = 1+2/3++ex3 :: (ConstExp e, NumExp e, FracExp e, LogicExp e, CompareExp e) => Exp e Double+ex3 = 1+2/0++++--------------------------------------------------------------------------------++tests = do+ print $ eval $ ex1 2+ print $ eval $ ex1 5+ print $ eval $ beaufortScale 8+ print $ eval $ foo 11 12+ print $ eval $ foo 11 0+ fooExp+ print $ evalSafeDiv ex2+ print $ evalSafeDiv ex3
+ src/Dino.hs view
@@ -0,0 +1,14 @@+-- | The Dino language+--+-- Dino is a tagless embedded DSL for numeric simple calculations.++module Dino+ ( module Dino.Prelude+ , module Dino.Types+ , module Dino.Expression+ ) where++import Dino.Prelude+import Dino.Types+import Dino.Expression+import Dino.Interpretation ()
+ src/Dino/AST.hs view
@@ -0,0 +1,337 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Untyped representation of abstract syntax trees+module Dino.AST+ ( -- * Representation+ Field (..)+ , Mapping (..)+ , NameType (..)+ , Constr (..)+ , Importance (..)+ , AST (..)+ , record+ , prettyNamed++ -- * Generic inspection+ , GInspectableArgs (..)+ , GInspectableFields (..)+ , GInspectable (..)+ , Inspectable (..)+ , inspectListAsRec++ -- * Conversion to Tree+ , toTree+ , showTree+ , drawTree+ , htmlTree+ ) where++import Prelude++import Data.Hashable (Hashable (..))+import Data.HashMap.Strict (HashMap)+import qualified Data.HashMap.Strict as HM+import Data.Proxy (Proxy (..))+import Data.String (IsString(..))+import Data.Text (Text)+import qualified Data.Text as Text+import Data.Tree (Tree(..))+import Data.Tree.View (Behavior(..), NodeInfo(..))+import qualified Data.Tree.View as View+import GHC.Generics+ ( (:+:)(..)+ , (:*:)(..)+ , C1+ , D1+ , Generic(..)+ , K1(..)+ , M1(..)+ , Meta(..)+ , Rec0+ , Rep+ , S1+ , U1+ )+import GHC.Stack (HasCallStack)+import GHC.TypeLits (KnownSymbol, symbolVal)+import Text.PrettyPrint.ANSI.Leijen (Doc, Pretty (..))+import qualified Text.PrettyPrint.ANSI.Leijen as PP++import Dino.Pretty++++--------------------------------------------------------------------------------+-- * Representation+--------------------------------------------------------------------------------++-- A key-value mapping, used to represent records+--+-- The 'Importance' argument to 'Mapping' is used to distinguish between records+-- whose fields are essentially named parameters and records whose fields carry+-- information.+--+-- For example, a collection of people could be represented as a nested record+-- like this:+--+-- > { Harry = {age = 45, speed = 46}+-- > , Harriet = {age = 47, speed = 48}+-- > , ...+-- > }+--+-- In this case, the outer record can be considered to have 'Important' fields,+-- while the fields in the inner records are just there to give meaning to the+-- numbers.+--+-- But why not just add a @name@ field to the inner records and represent the+-- above collection as a list? The reason why a nested record may be preferred+-- is that it puts the name on the path from the root, which means that it will+-- show up in diffs.+data Mapping k v = Mapping Importance !(HashMap k v)+ deriving (Eq, Show, Foldable, Functor, Traversable, Generic)++instance (Hashable k, Hashable v) => Hashable (Mapping k v) where+ hashWithSalt s (Mapping i m) = hashWithSalt s (i, m)++data NameType+ = Constructor -- ^ Global constructor or variable+ | LocalVar -- ^ Local variable+ | Annotation -- ^ User annotation+ deriving (Eq, Show, Generic, Enum, Bounded)++instance Hashable NameType++-- | Description of a constructor or variable+data Constr+ = Tuple+ | List+ | Named NameType Text+ deriving (Eq, Show, Generic)++-- | Creates a 'Named' constructor/variable+instance IsString Constr where+ fromString = Named Constructor . Text.pack++instance Hashable Constr++-- | Representation of abstract syntax and values+--+-- 'AST' is parameterized by the representation of numbers. This makes it+-- possible to affect the exactness of comparisons. For example a newtype with+-- approximate equality can be used instead of e.g. 'Double'.+data AST n+ = Number n -- ^ Numeric literal+ | Text Text -- ^ Text literal+ | App Constr [AST n] -- ^ Application of constructor or variable+ | Let Text (AST n) (AST n) -- ^ @`Let` v a body@ binds @v@ to @a@ in @body@+ | Record (Mapping Field (AST n))+ deriving (Eq, Show, Foldable, Functor, Traversable, Generic)++instance Hashable n => Hashable (AST n)++record :: HasCallStack => Importance -> [(Field, AST n)] -> AST n+record imp = Record . Mapping imp . HM.fromList++prettyNamed :: NameType -> Text -> Doc+prettyNamed Constructor c = PP.string $ Text.unpack c+prettyNamed LocalVar v = PP.string $ Text.unpack v+prettyNamed Annotation a = PP.string $ Text.unpack $ "ANN: " <> a++-- | If @k@ is a 'String'-like type, it will be shown with quotes. Use 'Field'+-- to prevent this.+instance {-# OVERLAPPABLE #-}+ (Pretty a, Show k, Ord k) => Pretty (Mapping k a) where+ pretty (Mapping imp m) = prettyRecord imp $ pretty <$> m++instance Show a => Pretty (AST a) where+ pretty (Number a) = PP.string $ show a+ pretty (Text a) = PP.string $ show a+ pretty (App Tuple []) = PP.parens PP.empty+ pretty (App Tuple vs) =+ verticalList PP.lparen PP.comma PP.rparen $ map pretty vs+ pretty (App List []) = PP.brackets PP.empty+ pretty (App List vs) =+ verticalList PP.lbracket PP.comma PP.rbracket $ map pretty vs+ pretty (App (Named t c) []) = prettyNamed t c+ pretty (App (Named t c) vs) =+ underHeader (prettyNamed t c) $ foldr1 (PP.<$>) $ map pretty vs+ pretty (Let v a b) =+ underHeader (PP.string "let" PP.<+> var PP.<+> "=") (pretty a)+ PP.<$>+ underHeader (PP.string " in") (pretty b)+ where+ var = PP.string $ Text.unpack v+ pretty (Record rec) = pretty rec++++--------------------------------------------------------------------------------+-- * Generic inspection+--------------------------------------------------------------------------------++showSym :: forall sym str. (KnownSymbol sym, IsString str) => str+showSym = fromString $ symbolVal (Proxy @sym)++class GInspectableArgs rep where+ gInspectArgs :: rep x -> [AST Rational]++instance GInspectableArgs U1 where+ gInspectArgs _ = []++instance Inspectable a =>+ GInspectableArgs (S1 ('MetaSel 'Nothing x y z) (Rec0 a)) where+ gInspectArgs = pure . inspect . unK1 . unM1++instance (GInspectableArgs rep1, GInspectableArgs rep2) =>+ GInspectableArgs (rep1 :*: rep2) where+ gInspectArgs (rep1 :*: rep2) = gInspectArgs rep1 ++ gInspectArgs rep2++class GInspectableFields rep where+ gInspectFields :: rep x -> [(Field, AST Rational)]++instance GInspectableFields U1 where+ gInspectFields _ = []++instance (Inspectable a, KnownSymbol fld) =>+ GInspectableFields (S1 ('MetaSel ('Just fld) x y z) (Rec0 a)) where+ gInspectFields = pure . (showSym @fld, ) . inspect . unK1 . unM1++instance (GInspectableFields rep1, GInspectableFields rep2) =>+ GInspectableFields (rep1 :*: rep2) where+ gInspectFields (rep1 :*: rep2) = gInspectFields rep1 ++ gInspectFields rep2++class GInspectable rep where+ gInspect :: rep x -> AST Rational++instance (GInspectable rep1, GInspectable rep2) =>+ GInspectable (rep1 :+: rep2) where+ gInspect (L1 rep) = gInspect rep+ gInspect (R1 rep) = gInspect rep++instance GInspectable rep => GInspectable (D1 meta rep) where+ gInspect = gInspect . unM1++instance (GInspectableArgs rep, KnownSymbol con) =>+ GInspectable (C1 ('MetaCons con x 'False) rep) where+ gInspect = App (showSym @con) . gInspectArgs . unM1++instance (GInspectableFields rep, KnownSymbol con) =>+ GInspectable (C1 ('MetaCons con x 'True) rep) where+ gInspect =+ App (showSym @con) .+ pure . Record . Mapping Unimportant . HM.fromList . gInspectFields . unM1++class Inspectable a where+ inspect :: a -> AST Rational++ default inspect :: (Generic a, GInspectable (Rep a)) => a -> AST Rational+ inspect = gInspect . from++instance Inspectable Rational where inspect = Number+instance Inspectable Int where inspect = Number . toRational+instance Inspectable Integer where inspect = Number . toRational+instance Inspectable Float where inspect = Number . toRational+instance Inspectable Double where inspect = Number . toRational++instance Real n => Inspectable (AST n) where+ inspect = fmap toRational++instance Inspectable () where+ inspect () = App "()" []++instance Inspectable Bool where+ inspect b = App (fromString $ show b) []++instance {-# OVERLAPS #-} Inspectable String where+ inspect = Text . Text.pack++instance Inspectable Text where+ inspect = Text++instance Inspectable a => Inspectable (Maybe a) where+ inspect Nothing = App "Nothing" []+ inspect (Just a) = App "Just" [inspect a]++instance {-# OVERLAPPABLE #-} Inspectable a => Inspectable [a] where+ inspect = App List . map inspect++instance Inspectable a => Inspectable (Mapping Field a) where+ inspect (Mapping i m) = Record $ Mapping i $ fmap inspect m++instance (Inspectable a, Inspectable b) => Inspectable (a, b) where+ inspect (a, b) = App Tuple [inspect a, inspect b]++instance (Inspectable a, Inspectable b, Inspectable c) =>+ Inspectable (a, b, c) where+ inspect (a, b, c) = App Tuple [inspect a, inspect b, inspect c]++instance (Inspectable a, Inspectable b, Inspectable c, Inspectable d) =>+ Inspectable (a, b, c, d) where+ inspect (a, b, c, d) = App Tuple [inspect a, inspect b, inspect c, inspect d]++-- | Represent a list as a record, if the elements contain a value that can be+-- used as key+inspectListAsRec ::+ Inspectable a+ => Importance+ -> (a -> Field) -- ^ Extract the key+ -> [a]+ -> AST Rational+inspectListAsRec imp getKey as =+ Record $ Mapping imp $ HM.fromList [(getKey a, inspect a) | a <- as]++++--------------------------------------------------------------------------------+-- * Conversion to Tree+--------------------------------------------------------------------------------++renderCon :: Constr -> Text+renderCon Tuple = "#Tuple"+renderCon List = "#List"+renderCon (Named t n) = case t of+ Constructor -> n+ LocalVar -> "*" <> n+ Annotation -> "ANN: " <> n++tagTree :: Text -> Tree Text -> Tree Text+tagTree tag (Node n ts) = Node (tag <> n) ts++toTreeRec :: Show n => Mapping Field (AST n) -> [Tree Text]+toTreeRec (Mapping _ fs) =+ [tagTree (Text.pack (unField f) <> ": ") $ toTree a | (f, a) <- HM.toList fs]++-- | Conversion from 'AST' to 'Tree'+--+-- * Built-in consturctors (tuples and lists) are shown prepended with @#@.+--+-- * Record fields are shown as @fieldName:@.+--+-- * Local variables are shown as @*varName@ (both at binding and use site).+--+-- * Annotations are shown as "ANN: annotation ".+toTree :: Show n => AST n -> Tree Text+toTree (App c [Record rec]) = Node (renderCon c) $ toTreeRec rec+toTree (Number n) = Node (Text.pack $ show n) []+toTree (Text t) = Node (Text.pack $ show t) []+toTree (App c as) = Node (renderCon c) $ map toTree as+toTree (Let v a body) = Node ("Let *" <> v) [toTree a, toTree body]+toTree (Record fs) = Node "Record" $ toTreeRec fs++-- | Show an 'AST' using Unicode art+showTree :: Show n => AST n -> String+showTree = View.showTree . fmap Text.unpack . toTree+ -- TODO Convert `tree-view` to `Text`++-- | Draw an 'AST' on the terminal using Unicode art+drawTree :: Show n => AST n -> IO ()+drawTree = View.drawTree . fmap Text.unpack . toTree++-- | Convert an 'AST' to an HTML file with foldable nodes+htmlTree :: Show n => FilePath -> AST n -> IO ()+htmlTree file =+ View.writeHtmlTree Nothing file . fmap mkInfo . fmap Text.unpack . toTree+ where+ mkInfo n = NodeInfo InitiallyExpanded n ""
+ src/Dino/AST/Diff.hs view
@@ -0,0 +1,369 @@+{-# LANGUAGE UndecidableInstances #-}++module Dino.AST.Diff where++import Prelude++import Control.Monad (guard, zipWithM)+import Data.Coerce (coerce)+import Data.Foldable (asum)+import Data.Hashable (Hashable)+import qualified Data.HashMap.Strict as HM+import Data.List (sortOn)+import Data.Text (Text)+import qualified Data.Text as Text+import Text.PrettyPrint.ANSI.Leijen (Doc, Pretty (..), (<+>))+import qualified Text.PrettyPrint.ANSI.Leijen as PP++import Dino.Pretty+import Dino.AST++-- | Drop elements at the end of a list+dropEnd :: Int -> [a] -> [a]+dropEnd n as = take (length as - n) as++++--------------------------------------------------------------------------------+-- * Types+--------------------------------------------------------------------------------++data Replace a = Replace+ { original :: a+ , new :: a+ } deriving (Eq, Show, Functor)++-- | Edit operations on an optional element+data ElemOp a+ = AddElem a+ | RemoveElem a+ | EditElem (Diff a)++deriving instance (Eq a, Eq (Diff a)) => Eq (ElemOp a)+deriving instance (Show a, Show (Diff a)) => Show (ElemOp a)++-- | Edit operations at the end of a list+data EndOp a+ = Append [a]+ | DropEnd [a]+ deriving (Eq, Show, Functor)++-- | Edit operations on lists+data ListOp a =+ ListOp+ [Maybe (Diff a)]+ -- Edits for elements that are common in both lists (drawn from start)+ (Maybe (EndOp a))+ -- Elements that are added or removed at the end++deriving instance (Eq a, Eq (Diff a)) => Eq (ListOp a)+deriving instance (Show a, Show (Diff a)) => Show (ListOp a)++-- | Edit operation on a 'AST'+data Edit a+ = Replacement (Replace (AST a))+ | EditApp Constr [Maybe (Edit a)]+ | EditList (Diff [AST a])+ | EditLet (Diff (Text, AST a, AST a))+ | EditRecord (Diff (Mapping Field (AST a)))+ deriving (Eq, Show)++-- | Wrapper for values that should be regarded as monolithic when diffing+newtype Monolithic a = Monolithic {unMonolithic :: a}++++--------------------------------------------------------------------------------+-- * Diffing+--------------------------------------------------------------------------------++class Diffable a where+ -- | Representation of the difference between two values+ type Diff a+ type instance Diff a = Replace a++ -- | Calculate the difference between two values+ --+ -- The result is 'Nothing' iff. the two values are equal.+ --+ -- The following property holds:+ --+ -- @+ -- If Just d = diff a b+ -- Then Just b = `applyDiff` d a+ -- @+ diff ::+ a -- ^ Original+ -> a -- ^ New+ -> Maybe (Diff a)++ default diff :: (Eq a, Diff a ~ Replace a) => a -> a -> Maybe (Diff a)+ diff original new = do+ guard (original /= new)+ return $ Replace {original, new}++ -- | Apply an 'Edit' to a 'Value'+ --+ -- This function is mostly intended for testing. It succeeds iff. the edit+ -- makes sense.+ applyDiff :: Diff a -> a -> Maybe a++ default applyDiff :: (Eq a, Diff a ~ Replace a) => Diff a -> a -> Maybe a+ applyDiff (Replace {original, new}) a+ | a == original = Just new+ | otherwise = Nothing++applyDiffWhen :: Diffable a => Maybe (Diff a) -> a -> Maybe a+applyDiffWhen Nothing a = Just a+applyDiffWhen (Just d) a = applyDiff d a++instance Diffable ()+instance Diffable Bool+instance Diffable Text+instance Diffable Int+instance Diffable Integer+instance Diffable Float+instance Diffable Double+instance Diffable Rational++instance Eq a => Diffable (Monolithic a) where+ type Diff (Monolithic a) = Replace a+ diff (Monolithic original) (Monolithic new) = do+ guard (original /= new)+ return $ Replace {original, new}++ applyDiff (Replace {original, new}) a+ | unMonolithic a == original = Just $ Monolithic new+ | otherwise = Nothing++instance Diffable a => Diffable (Maybe a) where+ type Diff (Maybe a) = ElemOp a+ diff Nothing Nothing = Nothing+ diff (Just a') Nothing = Just $ RemoveElem a'+ diff Nothing (Just b') = Just $ AddElem b'+ diff (Just a') (Just b') = EditElem <$> diff a' b'++ applyDiff (RemoveElem _) Nothing = Nothing+ applyDiff (RemoveElem _) (Just _) = Just Nothing+ applyDiff (AddElem a) Nothing = Just (Just a)+ applyDiff (AddElem _) (Just _) = Nothing+ applyDiff (EditElem d) (Just a) = Just <$> applyDiff d a+ applyDiff (EditElem _) Nothing = Nothing++-- | Matches element-wise from the start of the lists, and detects+-- additions/removals at the end.+instance Diffable a => Diffable [a] where+ type Diff [a] = ListOp a+ diff o n+ | Nothing <- asum es, Nothing <- endOp = Nothing+ | otherwise = Just $ ListOp es endOp+ where+ es = zipWith diff o n+ lo = length o+ ln = length n+ endOp+ | lo < ln = Just $ Append (drop lo n)+ | ln < lo = Just $ DropEnd (dropEnd ln o)+ | otherwise = Nothing++ applyDiff (ListOp es endOp) as+ | le < la, maybe False isAppend endOp = Nothing+ | le <= la = applyEndOp <$> zipWithM applyDiffWhen es as+ | otherwise = Nothing+ where+ le = length es+ la = length as+ isAppend (Append _) = True+ isAppend _ = False+ applyEndOp = case endOp of+ Just (Append bs) -> (++ bs)+ _ -> id -- Dropping is handled by `zipWithM` above++instance (Diffable a, Diffable b) => Diffable (a, b) where+ type Diff (a, b) = (Maybe (Diff a), Maybe (Diff b))+ diff (oa, ob) (na, nb)+ | Nothing <- da, Nothing <- db = Nothing+ | otherwise = Just (da, db)+ where+ da = diff oa na+ db = diff ob nb++ applyDiff (da, db) (a, b) = (,) <$> applyDiffWhen da a <*> applyDiffWhen db b++instance (Diffable a, Diffable b, Diffable c) => Diffable (a, b, c) where+ type Diff (a, b, c) = (Maybe (Diff a), Maybe (Diff b), Maybe (Diff c))+ diff (oa, ob, oc) (na, nb, nc)+ | Nothing <- da, Nothing <- db, Nothing <- dc = Nothing+ | otherwise = Just (da, db, dc)+ where+ da = diff oa na+ db = diff ob nb+ dc = diff oc nc++ applyDiff (da, db, dc) (a, b, c) =+ (,,) <$> applyDiffWhen da a <*> applyDiffWhen db b <*> applyDiffWhen dc c++instance (Eq k, Hashable k, Diffable a) => Diffable (Mapping k a) where+ type Diff (Mapping k a) = Mapping k (ElemOp a)++ diff (Mapping oi o) (Mapping ni n)+ | null e = Nothing+ | otherwise = Just $ Mapping (oi <> ni) e+ where+ e = flip HM.mapMaybeWithKey (HM.union o n) $ \k _ ->+ diff (HM.lookup k o) (HM.lookup k n)++ applyDiff (Mapping imp e) (Mapping _ m) =+ fmap (Mapping imp . HM.union additions . HM.mapMaybe id) $+ HM.traverseWithKey applyElem m+ where+ applyElem k v =+ case HM.lookup k e of+ Nothing -> Just $ Just v+ Just (AddElem _) -> Nothing -- Cannot add an existing element+ Just (RemoveElem _) -> Just Nothing+ Just (EditElem d) -> Just <$> applyDiff d v+ additions =+ flip HM.mapMaybe e $ \d ->+ case d of+ AddElem v -> Just v+ _ -> Nothing++instance Eq a => Diffable (AST a) where+ type Diff (AST a) = Edit a++ diff (App List o) (App List n) = EditList <$> diff o n+ diff (App co os) (App cn ns)+ | co == cn && length os == length ns =+ (\(ListOp es _) -> EditApp co es) <$> diff os ns+ -- We know that `os` and `ns` have the same length, so if `diffList`+ -- returns `Just`, it must mean that at least one element in `es` is+ -- `Just`.+ diff (Let vo o bo) (Let vn n bn) = EditLet <$> diff (vo, o, bo) (vn, n, bn)+ diff (Record o) (Record n) = EditRecord <$> diff o n+ diff o n = Replacement <$> diff (Monolithic o) (Monolithic n)++ applyDiff (Replacement d) a = coerce $ applyDiff d (Monolithic a)+ applyDiff (EditList e) (App List as) = App List <$> applyDiff e as+ applyDiff (EditApp c es) (App c' as)+ | c == c' = App c <$> applyDiff (ListOp es Nothing) as+ applyDiff (EditLet e) (Let v a b) =+ (\(v', a', b') -> Let v' a' b') <$> applyDiff e (v, a, b)+ applyDiff (EditRecord e) (Record rec) = Record <$> applyDiff e rec+ applyDiff _ _ = Nothing++++--------------------------------------------------------------------------------+-- * Rendering+--------------------------------------------------------------------------------++-- | If @k@ is a 'String'-like type, it will be shown with quotes. Use 'Field'+-- to prevent this.+instance {-# OVERLAPPING #-}+ (Pretty a, Pretty (Diff a), Show k, Ord k) =>+ Pretty (Mapping k (ElemOp a)) where+ pretty (Mapping imp m) =+ verticalList PP.lbrace PP.comma PP.rbrace $+ map prettyField $ sortOn fst $ HM.toList m+ where+ prettyField (f, AddElem v) =+ PP.green $+ (PP.text "+" <+>+ emphasize imp (PP.string (show f)) <+> PP.text "=") PP.<$>+ PP.text " " <>+ PP.align (pretty v)+ prettyField (f, RemoveElem v) =+ PP.red $+ (PP.text "-" <+>+ emphasize imp (PP.string (show f)) <+> PP.text "=") PP.<$>+ PP.text " " <>+ PP.align (pretty v)+ prettyField (f, EditElem e) =+ underHeader (emphasize imp (PP.string (show f)) <+> PP.text "=") $+ pretty e++instance Pretty a => Pretty (Replace a) where+ pretty Replace {original, new} =+ PP.red (PP.char '-' <+> PP.align (pretty original)) PP.<$>+ PP.green (PP.char '+' <+> PP.align (pretty new))++-- | Pretty print for edits on tuple-like collections (where elements are+-- identified by position)+prettyEditTuple :: Pretty a => Doc -> Doc -> Doc -> [Maybe a] -> Doc+prettyEditTuple l sep r = verticalList l sep r . map (maybe unchanged pretty)++-- | Pretty print 'EditApp' for \"named\" constructors+prettyEditApp :: Pretty a => NameType -> Text -> [Maybe a] -> Doc+prettyEditApp t c [] = prettyNamed t c+prettyEditApp t c as =+ underHeader (prettyNamed t c) $ PP.vcat $ map (maybe unchanged pretty) as++instance (Pretty a, Pretty (Diff a)) => Pretty (ListOp a) where+ pretty (ListOp es endOp) =+ verticalList PP.lbracket PP.comma PP.rbracket (es' ++ os)+ where+ es' =+ [ underHeader (PP.magenta $ PP.text ("edit @" <> show i)) (pretty e)+ | (i :: Int, Just e) <- zip [0 ..] es+ ]+ os = case endOp of+ Nothing -> []+ Just (Append vs) ->+ [ underHeader (PP.magenta $ PP.text "append") $+ PP.green (PP.char '+' <+> PP.align (pretty v))+ | v <- vs+ ]+ Just (DropEnd vs) ->+ [ underHeader (PP.magenta $ PP.text "drop from end") $+ PP.red (PP.char '-' <+> PP.align (pretty v))+ | v <- vs+ ]++instance Show a => Pretty (Edit a) where+ pretty (EditApp Tuple es) =+ verticalList PP.lparen PP.comma PP.rparen $ map (maybe unchanged pretty) es+ pretty (Replacement e) = pretty e+ pretty (EditApp List es) = pretty $ EditList (ListOp es Nothing)+ pretty (EditApp (Named t c) es) = prettyEditApp t c es+ pretty (EditList e) = pretty e+ pretty (EditLet (v, a, b)) =+ underHeader (PP.string "let" PP.<+> PP.align var PP.<+> "=") (maybe unchanged pretty a)+ PP.<$>+ underHeader (PP.string " in") (maybe unchanged pretty b)+ where+ var = maybe unchanged (pretty . fmap (PP.string . Text.unpack)) v+ -- TODO Would maybe be good to show the variable name even if it hasn't+ -- changed...+ pretty (EditRecord (Mapping imp erec)) =+ verticalList PP.lbrace PP.comma PP.rbrace $+ map prettyField $ sortOn fst $ HM.toList erec+ where+ prettyField (f, AddElem v) =+ PP.green $+ (PP.text "+" <+>+ emphasize imp (PP.string (unField f)) <+> PP.text "=") PP.<$>+ PP.text " " <>+ PP.align (pretty v)+ prettyField (f, RemoveElem v) =+ PP.red $+ (PP.text "-" <+>+ emphasize imp (PP.string (unField f)) <+> PP.text "=") PP.<$>+ PP.text " " <>+ PP.align (pretty v)+ prettyField (f, EditElem e) =+ underHeader (emphasize imp (PP.string (unField f)) <+> PP.text "=") $+ pretty e++-- | Print an 'Edit' value to the terminal using ANSI colors+printEdit :: Show a => Edit a -> IO ()+printEdit e = PP.putDoc (pretty e) >> putStrLn ""++-- | Print a diff as a test result+--+-- 'Nothing' is shown as a green \"OK\".+--+-- @`Just` d@ is shown as a red \"Fail\", followed by a rendering of the diff.+diffAsTestResult :: Show a => Maybe (Edit a) -> Doc+diffAsTestResult Nothing = PP.green $ PP.string "OK"+diffAsTestResult (Just e) = underHeader (PP.red (PP.string "Fail")) (PP.pretty e)
+ src/Dino/Expression.hs view
@@ -0,0 +1,847 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PolyKinds #-}++-- | General tagless expressions++module Dino.Expression where++import Dino.Prelude+import qualified Prelude++import Control.Applicative (liftA, liftA2)+import Control.Error (headMay)+import Control.Monad ((>=>), ap, foldM)+import Control.Monad.Loops (dropWhileM, firstM)+import Data.Bifunctor (Bifunctor (..))+import Data.List ((\\))+import Data.String (IsString (..))+import Data.Text (Text)+import GHC.TypeLits (KnownSymbol, Symbol)+import qualified GHC.Records as GHC+import GHC.Stack++import Dino.Types++++--------------------------------------------------------------------------------+-- * Expression classes and constructs+--------------------------------------------------------------------------------++----------------------------------------+-- ** Constants+----------------------------------------++-- | Constant expressions+--+-- The default implementation is for 'Applicative' interpretations.+class ConstExp e where+ -- | Make a Dino literal from a Haskell value+ lit :: DinoType a => a -> e a++ default lit :: Applicative e => a -> e a+ lit = pure++true, false :: ConstExp e => e Bool+true = lit True+false = lit False++-- | Constant text expression+--+-- With @OverloadedStrings@ enabled, text literals can be written simply as+-- @"..."@.+text :: ConstExp e => Text -> e Text+text = lit++++----------------------------------------+-- ** Numeric expressions+----------------------------------------++-- | Numeric expressions+--+-- The default implementations are for 'Applicative' interpretations.+class NumExp e where+ add :: Num a => e a -> e a -> e a+ sub :: Num a => e a -> e a -> e a+ mul :: Num a => e a -> e a -> e a+ absE :: Num a => e a -> e a+ signE :: Num a => e a -> e a++ -- | Convert an integer to any numeric type+ fromIntegral :: (Integral a, DinoType b, Num b) => e a -> e b++ -- | @`floor` x@ returns the greatest integer not greater than @x@+ floor :: (RealFrac a, DinoType b, Integral b) => e a -> e b++ -- | @`truncate` x@ returns the integer nearest @x@ between zero and @x@+ truncate :: (RealFrac a, DinoType b, Integral b) => e a -> e b++ -- | Round to the specified number of decimals+ roundN :: RealFrac a => Int -> e a -> e a+ -- TODO This function doesn't make much sense for non-decimal+ -- representations. Use a decimal representation.++ default add :: (Applicative e, Num a) => e a -> e a -> e a+ default sub :: (Applicative e, Num a) => e a -> e a -> e a+ default mul :: (Applicative e, Num a) => e a -> e a -> e a+ default absE :: (Applicative e, Num a) => e a -> e a+ default signE :: (Applicative e, Num a) => e a -> e a+ default fromIntegral :: (Applicative e, Integral a, Num b) => e a -> e b+ default floor :: (Applicative e, RealFrac a, Integral b) => e a -> e b+ default truncate :: (Applicative e, RealFrac a, Integral b) => e a -> e b+ default roundN :: (Applicative e, RealFrac a) => Int -> e a -> e a++ add = liftA2 (+)+ sub = liftA2 (-)+ mul = liftA2 (*)+ absE = liftA abs+ signE = liftA signum+ fromIntegral = liftA Prelude.fromIntegral+ floor = liftA (Prelude.fromInteger . Prelude.floor)+ truncate = liftA (Prelude.fromInteger . Prelude.truncate)+ roundN n = liftA roundN'+ where+ roundN' a = (fromInteger $ Prelude.round $ a * (10^n)) / (10.0^^n)+ -- https://stackoverflow.com/questions/12450501/round-number-to-specified-number-of-digits#12450771++-- | Convert an 'Integer' to any numeric type+fromInt :: (NumExp e, DinoType a, Num a) => e Integer -> e a+fromInt = fromIntegral+ -- We cannot override the name `fromInteger`, since that's used for desugaring+ -- numeric literals.++-- | Fractional expressions+--+-- The default implementation is for 'Applicative' interpretations.+class FracExp e where+ -- | Division+ fdiv :: (Fractional a, Eq a) => e a -> e a -> e a+ -- `Eq` is useful for catching division by zero.++ default fdiv :: (Applicative e, Fractional a) => e a -> e a -> e a+ fdiv = liftA2 (/)++-- | Division that returns 0 when the denominator is 0+(./) ::+ ( ConstExp e+ , FracExp e+ , CompareExp e+ , CondExpFO e+ , DinoType a+ , Fractional a+ )+ => e a+ -> e a+ -> e a+a ./ b = ifThenElse (b == lit 0) (lit 0) (fdiv a b)++++----------------------------------------+-- ** Logic expressions+----------------------------------------++-- | Logic expressions+--+-- The default implementations are for 'Applicative' interpretations.+class LogicExp e where+ not :: e Bool -> e Bool+ conj :: e Bool -> e Bool -> e Bool+ disj :: e Bool -> e Bool -> e Bool+ xor :: e Bool -> e Bool -> e Bool++ default not :: Applicative e => e Bool -> e Bool+ default conj :: Applicative e => e Bool -> e Bool -> e Bool+ default disj :: Applicative e => e Bool -> e Bool -> e Bool+ default xor :: Applicative e => e Bool -> e Bool -> e Bool++ not = liftA Prelude.not+ conj = liftA2 (Prelude.&&)+ disj = liftA2 (Prelude.||)+ xor = liftA2 (Prelude./=)++(&&), (||) :: LogicExp e => e Bool -> e Bool -> e Bool++(&&) = conj+(||) = disj++infixr 3 &&+infixr 2 ||++++----------------------------------------+-- ** Comparisons+----------------------------------------++-- | Comparisons+--+-- The default implementations are for 'Applicative' interpretations.+class CompareExp e where+ eq :: Eq a => e a -> e a -> e Bool+ neq :: Eq a => e a -> e a -> e Bool+ lt :: Ord a => e a -> e a -> e Bool+ gt :: Ord a => e a -> e a -> e Bool+ lte :: Ord a => e a -> e a -> e Bool+ gte :: Ord a => e a -> e a -> e Bool+ min :: Ord a => e a -> e a -> e a+ max :: Ord a => e a -> e a -> e a++ default eq :: (Applicative e, Eq a) => e a -> e a -> e Bool+ default neq :: (Applicative e, Eq a) => e a -> e a -> e Bool+ default lt :: (Applicative e, Ord a) => e a -> e a -> e Bool+ default gt :: (Applicative e, Ord a) => e a -> e a -> e Bool+ default lte :: (Applicative e, Ord a) => e a -> e a -> e Bool+ default gte :: (Applicative e, Ord a) => e a -> e a -> e Bool+ default min :: (Applicative e, Ord a) => e a -> e a -> e a+ default max :: (Applicative e, Ord a) => e a -> e a -> e a++ eq = liftA2 (Prelude.==)+ neq = liftA2 (Prelude./=)+ lt = liftA2 (Prelude.<)+ gt = liftA2 (Prelude.>)+ lte = liftA2 (Prelude.<=)+ gte = liftA2 (Prelude.>=)+ min = liftA2 Prelude.min+ max = liftA2 Prelude.max++(==), (/=) :: (Eq a, CompareExp e) => e a -> e a -> e Bool+(==) = eq+(/=) = neq++(<), (>), (<=), (>=) :: (Ord a, CompareExp e) => e a -> e a -> e Bool+(<) = lt+(>) = gt+(<=) = lte+(>=) = gte++infix 4 ==, /=, <, >, <=, >=++-- | Check equality against a constant value+(==!) :: (ConstExp e, CompareExp e, DinoType a) => e a -> a -> e Bool+a ==! b = a == lit b++infix 4 ==!++++----------------------------------------+-- ** Conditionals+----------------------------------------++-- | Representation of a case in 'cases'+data a :-> b = a :-> b+ deriving (Eq, Show, Foldable, Functor, Traversable)++instance Bifunctor (:->) where+ bimap f g (a :-> b) = f a :-> g b++-- | Construct a case in 'cases', 'match', etc.+--+-- Example:+--+-- @+-- beaufortScale :: _ => `Exp` e a -> `Exp` e `Text`+-- beaufortScale v = `match` v+-- [ (`<` 0.5) `-->` "calm"+-- , (`<` 13.8) `-->` "breeze"+-- , (`<` 24.5) `-->` "gale" ]+-- ( `Otherwise` `-->` "storm" )+-- @+(-->) :: a -> b -> (a :-> b)+(-->) = (:->)++infix 1 :->, -->++-- | Marker for the default case in 'cases'+data Otherwise = Otherwise++-- | Helper class to 'CondExp' containing only first-order constructs+--+-- The reason for having this class is that there are types for which+-- 'CondExpFO' can be derived but 'CondExp' cannot.+class CondExpFO e where+ -- | Construct an optional value that is present+ just :: e a -> e (Maybe a)++ -- | Case expression+ cases ::+ [e Bool :-> e a] -- ^ Guarded expressions+ -> (Otherwise :-> e a) -- ^ Fall-through case+ -> e a++ -- | Case expression without fall-through+ --+ -- Evaluation may fail if the cases are not complete.+ partial_cases ::+ HasCallStack+ => [e Bool :-> e a] -- ^ Guarded expressions+ -> e a++ default just :: Applicative e => e a -> e (Maybe a)+ just = liftA Just++ default cases :: Monad e => [e Bool :-> e a] -> (Otherwise :-> e a) -> e a+ cases cs (_ :-> d) = do+ f <- firstM (\(c :-> _) -> c) cs+ case f of+ Nothing -> d+ Just (_ :-> a) -> a++ default partial_cases :: (Monad e, HasCallStack) => [e Bool :-> e a] -> e a+ partial_cases = default_partial_cases++-- | Expressions supporting conditionals+--+-- The default implementations are for monadic interpretations.+class CondExpFO e => CondExp e where+ -- | Deconstruct an optional value+ maybe ::+ DinoType a+ => e b -- ^ Result when 'nothing'+ -> (e a -> e b) -- ^ Result when 'just'+ -> e (Maybe a) -- ^ Value to deconstruct+ -> e b++ default maybe :: Monad e => e b -> (e a -> e b) -> e (Maybe a) -> e b+ maybe n j m = Prelude.maybe n (j . return) =<< m++default_partial_cases :: (CondExpFO e, HasCallStack) => [e Bool :-> e a] -> e a+default_partial_cases cs =+ cases cs $ (Otherwise --> error "partial_cases: no matching case")++-- | Construct an optional value that is missing+nothing :: (ConstExp e, DinoType a) => e (Maybe a)+nothing = lit Nothing++isJust :: (ConstExp e, CondExp e, DinoType a) => e (Maybe a) -> e Bool+isJust = maybe false (const true)++-- | Case expression using Boolean functions for matching+match ::+ CondExpFO e+ => a -- ^ Scrutinee+ -> [(a -> e Bool) :-> e b] -- ^ Cases+ -> (Otherwise :-> e b) -- ^ Fall-through case+ -> e b+match a = cases . map (first ($ a))++-- | Case expression matching a value against constants+--+-- Example:+--+-- @+-- operate c a = `matchConst` c+-- ['+' `-->` a + 1+-- ,'-' `-->` a - 1+-- ]+-- (`Otherwise` `-->` a)+-- @+matchConst ::+ (ConstExp e, CompareExp e, CondExpFO e, DinoType a)+ => e a -- ^ Scrutinee+ -> [a :-> e b] -- ^ Cases+ -> (Otherwise :-> e b) -- ^ Fall-through case+ -> e b+matchConst a = match a . map (first ((==) . lit))++-- | A Version of 'matchConst' for enumerations where the cases cover the whole+-- domain+--+-- An error is thrown if the cases do not cover the whole domain.+matchConstFull ::+ ( ConstExp e+ , CompareExp e+ , CondExpFO e+ , DinoType a+ , Show a+ , Enum a+ , Bounded a+ , HasCallStack+ )+ => e a -- ^ Scrutinee+ -> [a :-> e b] -- ^ Cases+ -> e b+matchConstFull a cs+ | null missing = partial_cases $ map (first (a ==!)) cs+ | otherwise = error $ "matchConstFull: missing cases " ++ show missing+ where+ domain = [minBound .. maxBound]+ missing = domain \\ [b | b :-> _ <- cs]++-- | Conditional expression+--+-- Enable @RebindableSyntax@ to use the standard syntax @if a then b else c@+-- for calling this function.+ifThenElse ::+ CondExpFO e+ => e Bool -- ^ Condition+ -> e a -- ^ True branch+ -> e a -- ^ False branch+ -> e a+ifThenElse c t f = cases [c --> t] (Otherwise --> f)++fromMaybe :: (CondExp e, DinoType a) => e a -> e (Maybe a) -> e a+fromMaybe n = maybe n id++++----------------------------------------+-- ** Lists+----------------------------------------++-- | Helper class to 'ListExp' containing only first-order constructs+--+-- The reason for having this class is that there are types for which+-- 'ListExpFO' can be derived but 'ListExp' cannot.+class ListExpFO e where+ range ::+ Enum a+ => e a -- ^ Lower bound (inclusive)+ -> e a -- ^ Upper bound (inclusive)+ -> e [a]++ list :: DinoType a => [e a] -> e [a]+ headE :: e [a] -> e (Maybe a)+ append :: e [a] -> e [a] -> e [a]++ default range :: (Applicative e, Enum a) => e a -> e a -> e [a]+ default list :: Applicative e => [e a] -> e [a]+ default headE :: Applicative e => e [a] -> e (Maybe a)+ default append :: Applicative e => e [a] -> e [a] -> e [a]++ range = liftA2 $ \l u -> [l .. u]+ list = sequenceA+ headE = liftA headMay+ append = liftA2 (++)++class ListExpFO e => ListExp e where+ mapE :: DinoType a => (e a -> e b) -> e [a] -> e [b]+ dropWhileE :: DinoType a => (e a -> e Bool) -> e [a] -> e [a]++ -- | Left fold+ foldE ::+ (DinoType a, DinoType b)+ => (e a -> e b -> e a) -- ^ Reducer function+ -> e a -- ^ Initial value+ -> e [b] -- ^ List to reduce (traversed left-to-right)+ -> e a++ default mapE :: Monad e => (e a -> e b) -> e [a] -> e [b]+ default dropWhileE :: Monad e => (e a -> e Bool) -> e [a] -> e [a]+ default foldE :: Monad e => (e a -> e b -> e a) -> e a -> e [b] -> e a++ mapE f as = mapM (f . return) =<< as+ dropWhileE p as = dropWhileM (p . return) =<< as++ foldE f a bs = do+ a' <- a+ bs' <- bs+ foldM (\aa bb -> f (return aa) (return bb)) a' bs'++++----------------------------------------+-- ** Tuples+----------------------------------------++class TupleExp e where+ pair :: e a -> e b -> e (a, b)+ fstE :: e (a, b) -> e a+ sndE :: e (a, b) -> e b++ default pair :: Applicative e => e a -> e b -> e (a, b)+ default fstE :: Applicative e => e (a, b) -> e a+ default sndE :: Applicative e => e (a, b) -> e b++ pair = liftA2 (,)+ fstE = liftA fst+ sndE = liftA snd++++----------------------------------------+-- ** Let bindings+----------------------------------------++class LetExp e where+ -- | Share a value in a calculation+ --+ -- The default implementation of 'letE' implements call-by-value.+ letE ::+ DinoType a+ => Text -- ^ Variable base name+ -> e a -- ^ Value to share+ -> (e a -> e b) -- ^ Body+ -> e b++ default letE :: Monad e => Text -> e a -> (e a -> e b) -> e b+ letE _ a body = a >>= body . return++-- | Share a value in a calculation+--+-- Like 'letE' but with the variable base name fixed to \"share\".+share ::+ (LetExp e, DinoType a)+ => e a -- ^ Value to share+ -> (e a -> e b) -- ^ Body+ -> e b+share = letE "share"++-- | Make a function with a shared argument+--+-- @+-- `shared` = `flip` `share`+-- @+--+-- Like 'letE' but with the variable base name fixed to \"share\".+shared ::+ (LetExp e, DinoType a)+ => (e a -> e b) -- ^ Body+ -> e a -- ^ Value to share+ -> e b+shared = flip share++++----------------------------------------+-- ** Records+----------------------------------------++data Field (f :: Symbol) = Field++class FieldExp e where+ getField ::+ (KnownSymbol f, HasField f r a, DinoType a) => proxy f -> e r -> e a++ default getField ::+ forall proxy f r a. (Applicative e, KnownSymbol f, HasField f r a)+ => proxy f+ -> e r+ -> e a+ getField _ = liftA (GHC.getField @f)++instance (f1 ~ f2) => IsLabel f1 (Field f2) where+ fromLabel = Field++-- | Extract a field from a record+--+-- Use as follows (with @OverloadedLabels@):+--+-- > field #name $ field #driver car+field ::+ (FieldExp e, KnownSymbol f, HasField f r a, DinoType a)+ => Field f+ -> e r+ -> e a+field = getField++-- | Extract a field from a record+--+-- Use as follows (with @OverloadedLabels@):+--+-- > #name <. #driver <. car+(<.) ::+ (FieldExp e, KnownSymbol f, HasField f r a, DinoType a)+ => Field f+ -> e r+ -> e a+(<.) = getField++infixr 9 <.++++----------------------------------------+-- ** Annotations+----------------------------------------++class AnnExp ann e where+ -- | Annotate an expression+ ann :: ann -> e a -> e a+ ann _ = id++++----------------------------------------+-- ** Assertions+----------------------------------------++class AssertExp e where+ -- | Assert that a condition is true+ --+ -- Interpretations can choose whether to ignore the assertion or to check its+ -- validity. The default implementation ignores the assertion.+ --+ -- The following must hold for any monadic interpretation:+ --+ -- @+ -- `assert` lab c a+ -- `==`+ -- (`assert` lab c (`return` ()) `>>` `return` a)+ -- @+ assert ::+ Text -- ^ Assertion label+ -> e Bool -- ^ Condition that should be true+ -> e a -- ^ Expression to attach the assertion to+ -> e a+ assert _ _ = id++ -- | Assert that an expression is semantically equivalent to a reference+ -- expression+ --+ -- Interpretations can choose whether to ignore the assertion or to check its+ -- validity. The default implementation ignores the assertion.+ --+ -- The following must hold for any monadic interpretation:+ --+ -- @+ -- `assertEq` lab ref act+ -- `==`+ -- ( do a <- act+ -- `assertEq` lab ref (`return` a)+ -- return a+ -- )+ -- @+ assertEq ::+ (Eq a, Show a) -- TODO Use `Pretty`?+ => Text -- ^ Assertion label+ -> e a -- ^ Reference expression+ -> e a -- ^ Actual expression+ -> e a+ assertEq _ _ act = act+ -- Having a separate function for equality avoids the problem of "Boolean+ -- blindness". For example, a diff of the two expressions can be shown when+ -- they are not equal.++++----------------------------------------+-- ** Concrete expression wrapper+----------------------------------------++-- | Useful wrapper to get a concrete type for tagless DSL expressions+--+-- The problem solved by this type can be explained as follows:+--+-- Suppose you write a numeric expression with the most general type:+--+-- > myExp1 :: Num e => e+-- > myExp1 = 1+2+--+-- And suppose you define an evaluation function as follows:+--+--+-- > eval1 :: (forall e . (ConstExp e, NumExp e) => e a) -> a+-- > eval1 = runIdentity+--+-- The problem is that we cannot pass @myExp1@ to @eval1@:+--+-- > test1 :: Int+-- > test1 = eval1 myExp1+--+-- This leads to:+--+-- > • Could not deduce (Num (e Int)) ...+--+-- And we don't want to change @eval1@ to+--+-- > eval1 :: (forall e . (ConstExp e, NumExp e, Num (e a)) => e a) -> a+--+-- since this requires the expression to return a number (and not e.g. a+-- Boolean), and it also doesn't help to satisfy any internal numeric+-- expressions that may use a different type than @a@.+--+-- Instead, the solution is to use 'Exp' as follows:+--+-- > myExp2 :: (ConstExp e, NumExp e, Num a) => Exp e a+-- > myExp2 = 1+2+-- >+-- > eval2 :: (forall e . (ConstExp e, NumExp e) => Exp e a) -> a+-- > eval2 = runIdentity . unExp+-- >+-- > test2 :: Int+-- > test2 = eval2 myExp2+--+-- The trick is that there exists an instance+--+-- > instance (Num a, ConstExp e, NumExp e) => Num (Exp e a)+--+-- So it is enough for @eval2@ to supply constraints on @e@, and it will+-- automatically imply the availability of the `Num` instance.+newtype Exp e a = Exp+ { unExp :: e a+ } deriving ( Eq+ , Show+ , Functor+ , Applicative+ , Monad+ , ConstExp+ , NumExp+ , FracExp+ , LogicExp+ , CompareExp+ , CondExpFO+ , CondExp+ , ListExpFO+ , ListExp+ , LetExp+ , FieldExp+ , AnnExp ann+ , AssertExp+ )++instance (ConstExp e, IsString a, DinoType a) => IsString (Exp e a) where+ fromString = lit . fromString++instance (ConstExp e, NumExp e, DinoType a, Num a) => Num (Exp e a) where+ fromInteger = Exp . lit . fromInteger+ (+) = add+ (-) = sub+ (*) = mul+ abs = absE+ signum = signE++instance (ConstExp e, NumExp e, FracExp e, DinoType a, Fractional a) =>+ Fractional (Exp e a) where+ fromRational = Exp . lit . fromRational+ (/) = fdiv++instance (FieldExp e1, e1 ~ e2, KnownSymbol f, HasField f r a, DinoType a) =>+ IsLabel f (Exp e1 r -> Exp e2 a) where+ fromLabel = getField (Field @f)++++--------------------------------------------------------------------------------+-- * Derived operations+--------------------------------------------------------------------------------++----------------------------------------+-- ** Operations on Dino lists+----------------------------------------++sumE :: (ConstExp e, NumExp e, ListExp e, DinoType a, Num a) => e [a] -> e a+sumE = foldE add (lit 0)++andE :: (ConstExp e, LogicExp e, ListExp e) => e [Bool] -> e Bool+andE = foldE (&&) true++orE :: (ConstExp e, LogicExp e, ListExp e) => e [Bool] -> e Bool+orE = foldE (||) false++allE ::+ (ConstExp e, LogicExp e, ListExp e, DinoType a)+ => (e a -> e Bool)+ -> e [a]+ -> e Bool+allE p = andE . mapE p++anyE ::+ (ConstExp e, LogicExp e, ListExp e, DinoType a)+ => (e a -> e Bool)+ -> e [a]+ -> e Bool+anyE p = orE . mapE p++find ::+ (LogicExp e, ListExp e, DinoType a)+ => (e a -> e Bool)+ -> e [a]+ -> e (Maybe a)+find p = headE . dropWhileE (not . p)++(<++>) :: ListExpFO e => e [a] -> e [a] -> e [a]+(<++>) = append++++----------------------------------------+-- ** Operations on Haskell lists+----------------------------------------++and :: (ConstExp e, LogicExp e) => [e Bool] -> e Bool+and = foldr (&&) true++or :: (ConstExp e, LogicExp e) => [e Bool] -> e Bool+or = foldr (||) false++all :: (ConstExp e, LogicExp e) => (a -> e Bool) -> [a] -> e Bool+all p = and . map p++any :: (ConstExp e, LogicExp e) => (a -> e Bool) -> [a] -> e Bool+any p = or . map p++++----------------------------------------+-- ** Optional monad+----------------------------------------++-- | 'Optional' expressions with a 'Monad' instance+--+-- 'Optional' is handy to avoid nested uses of 'maybe'. As an example, here is a+-- safe division function:+--+-- > safeDiv :: _ => e a -> e a -> Optional e (e a)+-- > safeDiv a b = suppose $+-- > if (b /= lit 0)+-- > then just (fdiv a b)+-- > else nothing+--+-- And here is a calculation that defaults to 0 if any of the divisions fails:+--+-- > foo :: _ => Exp e Double -> Exp e Double -> Exp e Double+-- > foo a b = fromOptional 0 $ do+-- > x <- safeDiv a b+-- > y <- safeDiv b x+-- > safeDiv x y+data Optional e a where+ Return :: a -> Optional e a+ Bind :: DinoType a => e (Maybe a) -> (e a -> Optional e b) -> Optional e b+ -- Inspired by the Operational monad++instance Functor (Optional e) where+ fmap f (Return a) = Return $ f a+ fmap f (Bind m k) = Bind m (fmap f . k)++instance Applicative (Optional e) where+ pure = Return+ (<*>) = ap++instance Monad (Optional e) where+ Return a >>= k = k a+ Bind m k >>= l = Bind m (k >=> l)++-- | Lift an optional expression to 'Optional'+suppose :: DinoType a => e (Maybe a) -> Optional e (e a)+suppose a = Bind a Return++-- | Convert from 'Optional' value to an optional expression+optional ::+ (ConstExp e, CondExp e, LetExp e, DinoType a, DinoType b)+ => e b -- ^ Result if missing+ -> (e a -> e b) -- ^ Result if present+ -> Optional e (e a) -- ^ Value to examine+ -> e b+optional n j o = share n $ \n' ->+ let go (Return a) = j a+ go (Bind m k) = maybe n' (go . k) m+ in go o++runOptional ::+ (ConstExp e, CondExp e, LetExp e, DinoType a)+ => Optional e (e a)+ -> e (Maybe a)+runOptional = optional nothing just++-- | Extract an 'Optional' value+fromOptional ::+ (ConstExp e, CondExp e, LetExp e, DinoType a)+ => e a -- ^ Default value (in case the 'Optional' value is missing)+ -> Optional e (e a)+ -> e a+fromOptional d = optional d id
+ src/Dino/Interpretation.hs view
@@ -0,0 +1,1033 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -Wno-orphans #-}++-- | Interpretation of tagless expressions++module Dino.Interpretation where++import Dino.Prelude+import qualified Prelude++import Control.Exception (Exception, throw)+import Control.Monad (foldM, unless)+import Control.Monad.Catch (MonadThrow (..))+import Control.Monad.Except (ExceptT, MonadError (..))+import Control.Monad.Identity (Identity (..))+import Control.Monad.Loops (dropWhileM)+import Control.Monad.Reader (MonadReader (..), ReaderT (..))+import Control.Monad.Writer (WriterT)+import Data.Coerce (coerce)+import Data.HashMap.Strict (HashMap)+import qualified Data.HashMap.Strict as HashMap+import qualified Data.Text as Text+import Data.Proxy (Proxy (..))+import Data.Ratio (denominator, numerator)+import GHC.TypeLits (symbolVal)++import Dino.AST+import Dino.Types+import Dino.Expression++++-- Some terminology used in this module:+--+-- We'll refer to the various `...Exp` classes as "syntax classes". (To be+-- exact, the class definitions provide syntax, while the instances provide+-- semantics.)+--+-- "First-order syntax" (FOS) refers to classes that only contain first-order+-- constructs (i.e. no negative occurrences of the `e` type).+--+-- "Higher-order syntax" (HOS) refers to classes that contain higher-order+-- constructs.+--+-- The "intensional" counterpart of a HOS class is a FOS class that uses+-- explicit named variables instead. Intensional classes are only used+-- internally to enable certain interpretations. They should not be exported to+-- the user.++++--------------------------------------------------------------------------------+-- * Type checking+--------------------------------------------------------------------------------++-- The `DinoTypeRep` interpretation serves as a proof that Dino expressions can+-- only calculate with "supported types". Or, pragmatically, it means that we+-- can make arbitrary type information available to any sub-expression via+-- `DinoTypeRep`.++instance ConstExp DinoTypeRep where+ lit _ = dinoTypeRep++instance NumExp DinoTypeRep where+ add t _ = t+ sub t _ = t+ mul t _ = t+ absE t = t+ signE t = t+ fromIntegral _ = dinoTypeRep+ floor _ = dinoTypeRep+ truncate _ = dinoTypeRep+ roundN _ t = t++instance FracExp DinoTypeRep where+ fdiv t _ = t++instance LogicExp DinoTypeRep where+ not _ = dinoTypeRep+ conj _ _ = dinoTypeRep+ disj _ _ = dinoTypeRep+ xor _ _ = dinoTypeRep++instance CompareExp DinoTypeRep where+ eq _ _ = dinoTypeRep+ neq _ _ = dinoTypeRep+ lt _ _ = dinoTypeRep+ gt _ _ = dinoTypeRep+ lte _ _ = dinoTypeRep+ gte _ _ = dinoTypeRep+ min t _ = t+ max t _ = t++instance CondExpFO DinoTypeRep where+ just t = withType t OtherType+ cases _ (_ :-> t) = t+ partial_cases = default_partial_cases++instance CondExp DinoTypeRep where+ maybe t _ _ = t++instance ListExpFO DinoTypeRep where+ range t _ = ListType t+ list _ = dinoTypeRep+ headE = (\t -> withType t OtherType) . listTypeElem+ append t _ = t++instance ListExp DinoTypeRep where+ mapE f = ListType . f . listTypeElem+ dropWhileE _ = id+ foldE _ t _ = t+ -- Note: `mapE` has to build the body before returning. This leads to+ -- quadratic complexity for nested maps.++instance TupleExp DinoTypeRep where+ pair = PairType+ fstE (PairType t _) = t+ sndE (PairType _ t) = t++instance LetExp DinoTypeRep where+ letE _ t body = body t+ -- Note: `letE` has to build the body before returning. This leads to+ -- quadratic complexity for nested maps.++instance FieldExp DinoTypeRep where+ getField _ _ = dinoTypeRep++instance AnnExp ann DinoTypeRep++instance AssertExp DinoTypeRep++++--------------------------------------------------------------------------------+-- * Monadic interpretation+--------------------------------------------------------------------------------++instance ConstExp Identity+instance NumExp Identity+instance FracExp Identity+instance LogicExp Identity+instance CompareExp Identity+instance CondExpFO Identity+instance CondExp Identity+instance ListExpFO Identity+instance ListExp Identity+instance TupleExp Identity+instance LetExp Identity+instance FieldExp Identity+instance AnnExp ann Identity+-- | Ignoring assertion for efficiency+instance AssertExp Identity++instance ConstExp Maybe+instance NumExp Maybe+instance FracExp Maybe+instance LogicExp Maybe+instance CompareExp Maybe+instance CondExpFO Maybe+instance CondExp Maybe+instance ListExpFO Maybe+instance ListExp Maybe+instance TupleExp Maybe+instance LetExp Maybe+instance FieldExp Maybe+instance AnnExp ann Maybe+-- | Ignoring assertion for efficiency+instance AssertExp Maybe++instance ConstExp (Either e)+instance NumExp (Either e)+instance FracExp (Either e)+instance LogicExp (Either e)+instance CompareExp (Either e)+instance CondExpFO (Either e)+instance CondExp (Either e)+instance ListExpFO (Either e)+instance ListExp (Either e)+instance TupleExp (Either e)+instance LetExp (Either e)+instance FieldExp (Either e)+instance AnnExp ann (Either e)+-- | Ignoring assertion for efficiency+instance AssertExp (Either e)++instance Monad m => ConstExp (ExceptT e m)+instance Monad m => NumExp (ExceptT e m)+instance Monad m => FracExp (ExceptT e m)+instance Monad m => LogicExp (ExceptT e m)+instance Monad m => CompareExp (ExceptT e m)+instance Monad m => CondExpFO (ExceptT e m)+instance Monad m => CondExp (ExceptT e m)+instance Monad m => ListExpFO (ExceptT e m)+instance Monad m => ListExp (ExceptT e m)+instance Monad m => TupleExp (ExceptT e m)+instance Monad m => LetExp (ExceptT e m)+instance Monad m => FieldExp (ExceptT e m)+instance AnnExp ann (ExceptT e m)+-- | Ignoring assertion for efficiency+instance AssertExp (ExceptT e m)++instance Applicative m => ConstExp (ReaderT env m)+instance Applicative m => NumExp (ReaderT env m)+instance Applicative m => FracExp (ReaderT env m)+instance Applicative m => LogicExp (ReaderT env m)+instance Applicative m => CompareExp (ReaderT env m)+instance Monad m => CondExpFO (ReaderT env m)+instance Monad m => CondExp (ReaderT env m)+instance Monad m => ListExpFO (ReaderT env m)+instance Monad m => ListExp (ReaderT env m)+instance Monad m => TupleExp (ReaderT env m)+instance Monad m => LetExp (ReaderT env m)+instance Monad m => FieldExp (ReaderT env m)+instance AnnExp ann (ReaderT env m)+-- | Ignoring assertion for efficiency+instance AssertExp (ReaderT env m)++instance (Monoid t, Applicative m) => ConstExp (WriterT t m)+instance (Monoid t, Applicative m) => NumExp (WriterT t m)+instance (Monoid t, Applicative m) => FracExp (WriterT t m)+instance (Monoid t, Applicative m) => LogicExp (WriterT t m)+instance (Monoid t, Applicative m) => CompareExp (WriterT t m)+instance (Monoid t, Monad m) => CondExpFO (WriterT t m)+instance (Monoid t, Monad m) => CondExp (WriterT t m)+instance (Monoid t, Monad m) => ListExpFO (WriterT t m)+instance (Monoid t, Monad m) => ListExp (WriterT t m)+instance (Monoid t, Monad m) => TupleExp (WriterT t m)+instance (Monoid t, Monad m) => LetExp (WriterT t m)+instance (Monoid t, Monad m) => FieldExp (WriterT t m)+instance AnnExp ann (WriterT t m)+-- | Ignoring assertion for efficiency+instance AssertExp (WriterT t m)++-- | Pure evaluation+eval :: Exp Identity a -> a+eval = coerce++-- | Functorial evaluation+--+-- Can, for example, have the type+--+-- @`evalF` :: `Exp` `Maybe` a -> `Maybe` a@+evalF :: Exp f a -> f a+evalF = coerce++++--------------------------------------------------------------------------------+-- * Folding+--------------------------------------------------------------------------------++-- | A folding interpretation+--+-- Instances of expression classes work by monoidal folding over @e@ (see+-- 'foldMonoid').+newtype Fold e a = Fold {fold :: e}+ deriving (Eq, Show, Functor, Semigroup, Monoid)++instance Monoid e => Applicative (Fold e) where+ pure = mempty+ f <*> a = Fold (fold f <> fold a)++-- | N-ary folding functions+class FoldN f e | f -> e where+ -- | @`foldN` e (*)@ returns an n-ary function of the following form:+ --+ -- > \(Fold a) (Fold b) ... (Fold x) -> Fold (e * a * b * ... x)+ --+ -- (here @*@ denotes any binary operator, and it's assumed to be right-+ -- associative.)+ foldN :: e -> (e -> e -> e) -> f++instance FoldN (Fold e a) e where+ foldN e0 _ = Fold e0++instance FoldN f e => FoldN (Fold e a -> f) e where+ foldN e0 conc = \(Fold e) -> foldN (conc e0 e) conc++-- | @'foldMonoid' returns an n-ary function of the following form:+--+-- > \(Fold a) (Fold b) ... (Fold x) -> Fold (mempty <> a <> b <> ... x)+--+-- where 'mempty' and '<>' are the methods of the 'Monoid' class.+foldMonoid :: (FoldN f e, Monoid e) => f+foldMonoid = foldN mempty mappend++instance Monoid e => ConstExp (Fold e)+instance Monoid e => NumExp (Fold e)+instance Monoid e => FracExp (Fold e)+instance Monoid e => LogicExp (Fold e)+instance Monoid e => CompareExp (Fold e)+instance Monoid e => ListExpFO (Fold e)+instance Monoid e => TupleExp (Fold e)+instance Monoid e => FieldExp (Fold e)+instance AnnExp ann (Fold e)++-- | Interprets all branches+instance Monoid e => CondExpFO (Fold e) where+ cases cs (Otherwise :-> d) =+ Fold $ mconcat $ concat [[fold c, fold a] | (c :-> a) <- cs] ++ [fold d]++ partial_cases cs =+ Fold $ mconcat $ concat [[fold c, fold a] | (c :-> a) <- cs]++-- | Interprets all branches+instance Monoid e => CondExp (Fold e) where+ maybe n j m = coerce m <> coerce n <> coerce (j mempty)++instance Monoid e => ListExp (Fold e) where+ mapE f as = coerce as <> coerce (f mempty)+ dropWhileE p as = coerce as <> coerce (p mempty)+ foldE f a as = coerce a <> coerce as <> coerce (f mempty mempty)++instance Monoid e => LetExp (Fold e) where+ letE _ a f = coerce a <> f mempty++-- | Ignoring assertion+instance AssertExp (Fold e)++instance Monoid e => VarExp (Fold e) where+ varE _ = mempty++instance Semigroup e => CondIntensional (Fold e) where+ maybeI _ n j m = coerce m <> coerce n <> coerce j++instance Semigroup e => ListIntensional (Fold e) where+ mapI _ b as = coerce as <> coerce b+ dropWhileI _ b as = coerce as <> coerce b+ foldI _ _ b a as = coerce a <> coerce as <> coerce b++instance Semigroup e => LetIntensional (Fold e) where+ letI _ a b = coerce a <> coerce b++++--------------------------------------------------------------------------------+-- * Product of interpretations+--------------------------------------------------------------------------------++-- | Product of two interpretations+--+-- The product is used to run two interpretations in parallel. Note that there+-- are no instances for HOS classes. Instead, use @`Intensional` (e1 :×: e2)@ in+-- order to derive an interpretation of HOS classes for products.+data (e1 :×: e2) a = (:×:)+ { prodFst :: e1 a+ , prodSnd :: e2 a+ }++mkProd ::+ (lang e1, lang e2)+ => proxy lang+ -> (forall e. lang e => e a)+ -> (e1 :×: e2) a+mkProd _ e = e :×: e++liftProd ::+ (lang e1, lang e2)+ => proxy lang+ -> (forall e. lang e => e a -> e b)+ -> (e1 :×: e2) a+ -> (e1 :×: e2) b+liftProd _ f (a1 :×: a2) = f a1 :×: f a2++liftProd2 ::+ (lang e1, lang e2)+ => proxy lang+ -> (forall e. lang e => e a -> e b -> e c)+ -> (e1 :×: e2) a+ -> (e1 :×: e2) b+ -> (e1 :×: e2) c+liftProd2 _ f (a1 :×: a2) (b1 :×: b2) = f a1 b1 :×: f a2 b2++liftProd3 ::+ (lang e1, lang e2)+ => proxy lang+ -> (forall e. lang e => e a -> e b -> e c -> e d)+ -> (e1 :×: e2) a+ -> (e1 :×: e2) b+ -> (e1 :×: e2) c+ -> (e1 :×: e2) d+liftProd3 _ f (a1 :×: a2) (b1 :×: b2) (c1 :×: c2) = f a1 b1 c1 :×: f a2 b2 c2++instance (ConstExp e1, ConstExp e2) => ConstExp (e1 :×: e2) where+ lit a = mkProd (Proxy @ConstExp) (lit a)++instance (NumExp e1, NumExp e2) => NumExp (e1 :×: e2) where+ add = liftProd2 (Proxy @NumExp) add+ sub = liftProd2 (Proxy @NumExp) sub+ mul = liftProd2 (Proxy @NumExp) mul+ absE = liftProd (Proxy @NumExp) absE+ signE = liftProd (Proxy @NumExp) signE+ fromIntegral = liftProd (Proxy @NumExp) fromIntegral+ floor = liftProd (Proxy @NumExp) floor+ truncate = liftProd (Proxy @NumExp) truncate+ roundN n = liftProd (Proxy @NumExp) (roundN n)++instance (FracExp e1, FracExp e2) => FracExp (e1 :×: e2) where+ fdiv = liftProd2 (Proxy @FracExp) fdiv++instance (LogicExp e1, LogicExp e2) => LogicExp (e1 :×: e2) where+ not = liftProd (Proxy @LogicExp) not+ conj = liftProd2 (Proxy @LogicExp) conj+ disj = liftProd2 (Proxy @LogicExp) disj+ xor = liftProd2 (Proxy @LogicExp) xor++instance (CompareExp e1, CompareExp e2) => CompareExp (e1 :×: e2) where+ eq = liftProd2 (Proxy @CompareExp) eq+ neq = liftProd2 (Proxy @CompareExp) neq+ lt = liftProd2 (Proxy @CompareExp) lt+ gt = liftProd2 (Proxy @CompareExp) gt+ lte = liftProd2 (Proxy @CompareExp) lte+ gte = liftProd2 (Proxy @CompareExp) gte+ min = liftProd2 (Proxy @CompareExp) min+ max = liftProd2 (Proxy @CompareExp) max++instance (CondExpFO e1, CondExpFO e2) => CondExpFO (e1 :×: e2) where+ just = liftProd (Proxy @CondExpFO) just++ cases cs (Otherwise :-> (d1 :×: d2)) =+ cases cs1 (Otherwise :-> d1) :×: cases cs2 (Otherwise :-> d2)+ where+ (cs1, cs2) =+ unzip [(c1 :-> a1, c2 :-> a2) | ((c1 :×: c2) :-> (a1 :×: a2)) <- cs]++ partial_cases cs = partial_cases cs1 :×: partial_cases cs2+ where+ (cs1, cs2) =+ unzip [(c1 :-> a1, c2 :-> a2) | ((c1 :×: c2) :-> (a1 :×: a2)) <- cs]++instance (ListExpFO e1, ListExpFO e2) => ListExpFO (e1 :×: e2) where+ range = liftProd2 (Proxy @ListExpFO) range+ headE = liftProd (Proxy @ListExpFO) headE+ append = liftProd2 (Proxy @ListExpFO) append++ list as = list as1 :×: list as2+ where+ (as1, as2) = unzip [(a1, a2) | (a1 :×: a2) <- as]++instance (TupleExp e1, TupleExp e2) => TupleExp (e1 :×: e2) where+ pair = liftProd2 (Proxy @TupleExp) pair+ fstE = liftProd (Proxy @TupleExp) fstE+ sndE = liftProd (Proxy @TupleExp) sndE++instance (FieldExp e1, FieldExp e2) => FieldExp (e1 :×: e2) where+ getField f = liftProd (Proxy @FieldExp) (getField f)++instance (AnnExp ann e1, AnnExp ann e2) => AnnExp ann (e1 :×: e2) where+ ann a = liftProd (Proxy @(AnnExp ann)) (ann a)++instance (AssertExp e1, AssertExp e2) => AssertExp (e1 :×: e2) where+ assert lab = liftProd2 (Proxy @AssertExp) (assert lab)+ assertEq lab = liftProd2 (Proxy @AssertExp) (assertEq lab)++instance (VarExp e1, VarExp e2) => VarExp (e1 :×: e2) where+ varE v = mkProd (Proxy @VarExp) (varE v)++instance (CondIntensional e1, CondIntensional e2) =>+ CondIntensional (e1 :×: e2) where+ maybeI v = liftProd3 (Proxy @CondIntensional) (maybeI v)++instance (ListIntensional e1, ListIntensional e2) =>+ ListIntensional (e1 :×: e2) where+ mapI v = liftProd2 (Proxy @ListIntensional) (mapI v)+ dropWhileI v = liftProd2 (Proxy @ListIntensional) (dropWhileI v)+ foldI va vb = liftProd3 (Proxy @ListIntensional) (foldI va vb)++instance (LetIntensional e1, LetIntensional e2) =>+ LetIntensional (e1 :×: e2) where+ letI v = liftProd2 (Proxy @LetIntensional) (letI v)++++--------------------------------------------------------------------------------+-- * Intensional interpretation+--------------------------------------------------------------------------------++-- Intensional interpretation essentially means to analyze the expression+-- syntactically rather than evaluating it.+--+-- <https://en.wikipedia.org/wiki/Extensional_and_intensional_definitions>++++-- | Representation of the set of variables used by bindings in an expression.+-- An entry @(v, n)@ means that the base name @v@ is used possibly appended with+-- a number that is at most @n@.+--+-- Since the keys represent variable base names, they are not allowed to end+-- with digits.+type BindSet = HashMap Text Int++-- | Return an unused variable name from the given base name+--+-- The returned 'BindSet' includes the new variable.+freshVar :: Text -> BindSet -> (Text, BindSet)+freshVar v bs = case HashMap.lookup v bs of+ Nothing -> (v, HashMap.insert v 0 bs)+ Just n -> (v <> fromString (show n), HashMap.insert v (n+1) bs)++-- | Allow intensional interpretation of higher-order constructs+--+-- 'Intensional' is used to obtain instances of HOS classes from their+-- intensional counterparts. For example, given+-- @(`CondExpFO` e, `VarExp` e, `CondIntensional` e)@, we get+-- @`CondExp` (`Intensional` e)@.+--+-- Pairing the interpretation with a 'BindSet' allows generating symbolic+-- variables to inspect higher-order constructs rather than just running them.+newtype Intensional e a = Intensional+ { unIntensional :: (Fold BindSet :×: e) a+ } deriving ( ConstExp+ , NumExp+ , FracExp+ , LogicExp+ , CompareExp+ , CondExpFO+ , ListExpFO+ , TupleExp+ , FieldExp+ , AnnExp ann+ , AssertExp+ )++liftIntensional :: (e a -> e b) -> Intensional e a -> Intensional e b+liftIntensional f (Intensional (bsa :×: ea)) = Intensional (coerce bsa :×: f ea)++liftIntensional2 ::+ (e a -> e b -> e c)+ -> Intensional e a+ -> Intensional e b+ -> Intensional e c+liftIntensional2 f (Intensional (bsa :×: ea)) (Intensional (bsb :×: eb)) =+ Intensional ((coerce bsa <> coerce bsb) :×: f ea eb)++liftIntensional3 ::+ (e a -> e b -> e c -> e d)+ -> Intensional e a+ -> Intensional e b+ -> Intensional e c+ -> Intensional e d+liftIntensional3 f+ (Intensional (bsa :×: ea))+ (Intensional (bsb :×: eb))+ (Intensional (bsc :×: ec)) =+ Intensional (Fold (fold bsa <> fold bsb <> fold bsc) :×: f ea eb ec)++-- | Named variable expressions+--+-- This class is only used to internally to create intensional interpretations.+-- It should not be exposed to the EDSL user.+class VarExp e where+ -- | Create a named variable+ varE ::+ DinoType a+ => Text -- ^ Variable name+ -> e a++instance VarExp e => VarExp (Intensional e) where+ varE v = Intensional (mempty :×: varE v)++-- | Open up a binder represented as a Haskell function+--+-- This function helps creating intensional interpretations of higher-order+-- constructs.+unbind ::+ (VarExp e, DinoType a)+ => Text -- ^ Variable base name+ -> (Intensional e a -> Intensional e b) -- ^ Body parameterized by its free variable+ -> (Text, Intensional e b) -- ^ Generated variable and function body+unbind base f = (v, Intensional (Fold bsb' :×: eb))+ where+ Intensional (Fold bsb :×: eb) = f (varE v)+ (v, bsb') = freshVar base bsb+ -- This function uses the technique described in+ -- "Using Circular Programming for Higher-Order Syntax"+ -- <https://emilaxelsson.github.io/documents/axelsson2013using.pdf>++-- | A version of 'unbind' for 2-argument functions+unbind2 ::+ (VarExp e, DinoType a, DinoType b)+ => Text -- ^ Variable base name+ -> (Intensional e a -> Intensional e b -> Intensional e c)+ -- ^ Body parameterized by its free variables+ -> (Text, Text, Intensional e c) -- ^ Generated variables and function body+unbind2 base f = (va, vb, Intensional (Fold bsc'' :×: ec))+ where+ Intensional (Fold bsc :×: ec) = f (varE va) (varE vb)+ (va, bsc') = freshVar base bsc+ (vb, bsc'') = freshVar base bsc'++-- | Intensional counterpart of 'CondExp'+class CondIntensional e where+ -- | Intensional counterpart of 'maybe'+ maybeI ::+ DinoType a+ => Text -- ^ Variable name+ -> e b+ -> e b -- ^ Result when 'just' (open term)+ -> e (Maybe a)+ -> e b++-- | Intensional counterpart of 'ListExp'+class ListIntensional e where+ -- | Intensional counterpart of 'mapE'+ mapI ::+ DinoType a+ => Text -- ^ Variable name+ -> e b -- ^ Body (open term)+ -> e [a]+ -> e [b]++ -- | Intensional counterpart of 'dropWhileE'+ dropWhileI ::+ DinoType a+ => Text -- ^ Name of element variable+ -> e Bool -- ^ Predicate body (open term)+ -> e [a]+ -> e [a]++ -- | Intensional counterpart of 'foldE'+ foldI+ :: (DinoType a, DinoType b)+ => Text -- ^ Name of state variable+ -> Text -- ^ Name of element variable+ -> e a -- ^ Body (term with two free variables)+ -> e a+ -> e [b]+ -> e a++-- | Intensional counterpart of 'LetExp'+class LetIntensional e where+ -- | Intensional counterpart of 'letE'+ letI ::+ DinoType a+ => Text -- ^ Variable name+ -> e a+ -> e b -- ^ Body (open term)+ -> e b++instance (CondExpFO e, VarExp e, CondIntensional e) =>+ CondExp (Intensional e) where+ maybe n j = liftIntensional3 (maybeI var) n body+ where+ (var, body) = unbind "elem" j++instance (ListExpFO e, VarExp e, ListIntensional e) =>+ ListExp (Intensional e) where+ mapE f = liftIntensional2 (mapI var) body+ where+ (var, body) = unbind "elem" f++ dropWhileE f = liftIntensional2 (dropWhileI var) body+ where+ (var, body) = unbind "elem" f++ foldE f = liftIntensional3 (foldI va vb) body+ where+ (va, vb, body) = unbind2 "elem" f++instance (VarExp e, LetIntensional e) => LetExp (Intensional e) where+ letE base a f = liftIntensional2 (letI var) a body+ where+ (var, body) = unbind base f++++--------------------------------------------------------------------------------+-- * AST reification+--------------------------------------------------------------------------------++-- | Generic representation of numbers using 'Rational'+newtype NumRep = NumRep {unNumRep :: Rational}+ deriving (Eq, Ord, Num, Fractional, Real, Hashable)++-- | Integers are show exactly, non-integers are shown at 'Double' precision.+instance Show NumRep where+ show (NumRep n)+ | denominator n Prelude.== 1 = show $ numerator n+ | otherwise = show $ fromRational @Double n++-- | Expression reified as an 'AST'+newtype Reified a = Reified {unReified :: AST NumRep}++instance Inspectable (Reified a) where+ inspect = coerce++appReified :: Constr -> Reified a -> Reified b+appReified con = coerce $ \a -> App @NumRep con [a]++appReified2 :: Constr -> Reified a -> Reified b -> Reified c+appReified2 con = coerce $ \a b -> App @NumRep con [a, b]++appReified3 :: Constr -> Reified a -> Reified b -> Reified c -> Reified d+appReified3 con = coerce $ \a b c -> App @NumRep con [a, b, c]++appReified4 ::+ Constr -> Reified a -> Reified b -> Reified c -> Reified d -> Reified e+appReified4 con = coerce $ \a b c d -> App @NumRep con [a, b, c, d]++appReified5 ::+ Constr+ -> Reified a+ -> Reified b+ -> Reified c+ -> Reified d+ -> Reified e+ -> Reified f+appReified5 con = coerce $ \a b c d f -> App @NumRep con [a, b, c, d, f]++instance ConstExp Reified where+ lit = coerce . inspect++instance NumExp Reified where+ add = appReified2 "add"+ sub = appReified2 "sub"+ mul = appReified2 "mul"+ absE = appReified "absE"+ signE = appReified "signE"+ fromIntegral = appReified "fromIntegral"+ floor = appReified "floor"+ truncate = appReified "truncate"+ roundN n = appReified2 "roundN" (Reified $ Number $ Prelude.fromIntegral n)++instance FracExp Reified where+ fdiv = appReified2 "fdiv"++instance LogicExp Reified where+ not = appReified "not"+ conj = appReified2 "conj"+ disj = appReified2 "disj"+ xor = appReified2 "xor"++instance CompareExp Reified where+ eq = appReified2 "eq"+ neq = appReified2 "neq"+ lt = appReified2 "lt"+ gt = appReified2 "gt"+ lte = appReified2 "lte"+ gte = appReified2 "gte"+ min = appReified2 "min"+ max = appReified2 "max"++instance CondExpFO Reified where+ just = appReified "just"++ cases cs (Otherwise :-> d) =+ partial_cases (cs ++ [Reified (App "Otherwise" []) :-> d])++ partial_cases cs = Reified $ App "cases" $ pure $ App List+ [App ":->" [unReified c, unReified a] | c :-> a <- cs]++instance ListExpFO Reified where+ range = appReified2 "range"+ list = coerce $ App @NumRep List+ headE = appReified "headE"+ append = appReified2 "append"++instance TupleExp Reified where+ pair = appReified2 "pair"+ fstE = appReified "fstE"+ sndE = appReified "sndE"++-- | Field name prepended with @#@+instance FieldExp Reified where+ getField f = appReified (fromString $ "#" ++ symbolVal f)++instance AnnExp Text Reified where+ ann = appReified . Named Annotation++-- | Ignores the assertion+instance AssertExp Reified++instance VarExp Reified where+ varE v = Reified $ App (Named LocalVar v) []++instance CondIntensional Reified where+ maybeI v = appReified3 $ Named Constructor $ "maybe *" <> v++instance ListIntensional Reified where+ mapI v = appReified2 $ Named Constructor $ "mapE *" <> v+ dropWhileI v = appReified2 $ Named Constructor $ "dropWhileE *" <> v+ foldI va vb = appReified3 $+ Named Constructor $ Text.unwords ["foldE", "*" <> va, "*" <> vb]++instance LetIntensional Reified where+ letI v a b = (coerce $ Let @NumRep v) a b++++--------------------------------------------------------------------------------+-- * Evaluation with variables+--------------------------------------------------------------------------------++-- | Interpretation wrapper that evaluates using a variable environment rather+-- than piggybacking on higher-order syntax+--+-- 'EvalEnv' lacks instances of HOS classes. Instead, it provides instances of+-- 'intensional classes. In order to regain the missing HOS instances, 'EvalEnv'+-- 'can be wrapped in 'Intensional'.+--+-- @`Intensional` (`EvalEnv` e)@ is essentially equivalent to @e@, when @e@ is a+-- 'Monad'.+--+-- The purpose of 'EvalEnv' is to be used when evaluation must be done under+-- 'Intensional'. For example, this happens when combining reification and+-- evaluation.+newtype EvalEnv e a = EvalEnv+ { unEvalEnv :: ReaderT (HashMap Text Dinamic) e a+ } deriving ( Functor+ , Applicative+ , Monad+ , MonadReader (HashMap Text Dinamic)+ , ConstExp+ , NumExp+ , FracExp+ , LogicExp+ , CompareExp+ , CondExpFO+ , ListExpFO+ , TupleExp+ , FieldExp+ , AnnExp ann+ )+ -- It would be possible to derive instances of `CondExp`, etc. However, that+ -- would be confusing, since `EvalEnv` is intended to be used exactly in+ -- situations where those instances cannot be used (e.g. inside+ -- `Intensional`).++-- | Add a local variable binding+extendEnv ::+ (Monad e, DinoType a)+ => Text -- ^ Variable name+ -> a -- ^ Value of variable+ -> EvalEnv e b -- ^ Expression to evaluate in modified environment+ -> EvalEnv e b+extendEnv var = local . HashMap.insert var . Dinamic++data EvalEnvError+ = NotInScope Text+ | TypeError Text+ deriving (Show)++instance Exception EvalEnvError++-- | Throws 'EvalEnvError' when variable is not in scope or has the wrong type+instance Monad e => VarExp (EvalEnv e) where+ varE var = do+ env <- ask+ return $+ Prelude.maybe (throw $ TypeError var) id $+ fromDinamic $+ Prelude.maybe (throw $ NotInScope var) id $ HashMap.lookup var env++instance Monad e => CondIntensional (EvalEnv e) where+ maybeI var n j m = do+ m' <- m+ case m' of+ Nothing -> n+ Just a -> extendEnv var a j++instance Monad e => ListIntensional (EvalEnv e) where+ mapI var body as = Prelude.mapM (flip (extendEnv var) body) =<< as+ dropWhileI var body as = dropWhileM (flip (extendEnv var) body) =<< as++ foldI va vb body a bs = do+ a' <- a+ bs' <- bs+ foldM (\aa bb -> extendEnv va aa $ extendEnv vb bb body) a' bs'++instance Monad e => LetIntensional (EvalEnv e) where+ letI var a b = flip (extendEnv var) b =<< a++++--------------------------------------------------------------------------------+-- * Checking assertions+--------------------------------------------------------------------------------++data InvalidAssertion+ = InvalidCondition+ { assertionLabel :: Text+ }+ | NotEqual+ { assertionLabel :: Text+ , reference :: Text+ , actual :: Text+ }+ deriving (Show)++instance Exception InvalidAssertion++-- | Interpretation wrapper whose 'AssertExp' instance uses 'MonadError'+newtype AssertViaMonadError e a = AssertViaMonadError+ { unAssertViaMonadError :: e a+ } deriving ( Functor+ , Applicative+ , Monad+ , MonadError exc+ , ConstExp+ , NumExp+ , FracExp+ , LogicExp+ , CompareExp+ , CondExpFO+ , CondExp+ , ListExpFO+ , ListExp+ , TupleExp+ , LetExp+ , FieldExp+ , AnnExp ann+ )++-- | Throws 'InvalidAssertion' in the underlying monad+instance MonadError InvalidAssertion e =>+ AssertExp (AssertViaMonadError e) where+ assert lab cond a = do+ c <- cond+ unless c $ throwError $ InvalidCondition lab+ a++ assertEq lab ref act = do+ r <- ref+ a <- act+ unless (r Prelude.== a) $+ throwError $ NotEqual lab (Text.pack $ show r) (Text.pack $ show a)+ return a++-- | Interpretation wrapper whose 'AssertExp' instance uses 'MonadThrow'+newtype AssertViaMonadThrow e a = AssertViaMonadThrow+ { unAssertViaMonadThrow :: e a+ } deriving ( Functor+ , Applicative+ , Monad+ , MonadThrow+ , ConstExp+ , NumExp+ , FracExp+ , LogicExp+ , CompareExp+ , CondExpFO+ , CondExp+ , ListExpFO+ , ListExp+ , TupleExp+ , LetExp+ , FieldExp+ , AnnExp ann+ )++-- | Throws 'InvalidAssertion' in the underlying monad+instance MonadThrow e => AssertExp (AssertViaMonadThrow e) where+ assert lab cond a = do+ c <- cond+ unless c $ throwM $ InvalidCondition lab+ a++ assertEq lab ref act = do+ r <- ref+ a <- act+ unless (r Prelude.== a) $+ throwM $ NotEqual lab (Text.pack $ show r) (Text.pack $ show a)+ return a++data Assertion e where+ Assert :: e Bool -> Assertion e+ AssertEq :: (Eq a, Show a) => e a -> e a -> Assertion e++-- | Collect all assertions in an expression+--+-- Note that the wrapped interpretation @e@ must have instances of intensional+-- classes in order for 'CollectAssertions' to derive instances of HOS classes.+-- In order for the wrapped interpretation to do monadic evaluation, use the+-- wrapper 'EvalEnv' to obtain the necessary intensional instances.+newtype CollectAssertions e a = CollectAssertions+ { unCollectAssertions :: (Intensional (e :×: Fold [(Text, Assertion e)])) a+ } deriving ( ConstExp+ , NumExp+ , FracExp+ , LogicExp+ , CompareExp+ , CondExpFO+ , CondExp+ , ListExpFO+ , ListExp+ , TupleExp+ , LetExp+ , FieldExp+ , AnnExp ann+ , VarExp+ )+ -- TODO Use `Seq` instead of list.++instance AssertExp (CollectAssertions e) where+ assert lab =+ coerce $+ liftIntensional2 @(e :×: Fold [(Text, Assertion e)]) $+ \(c :×: _) (a :×: as) -> (a :×: (as <> Fold [(lab, Assert c)]))++ assertEq lab =+ coerce $+ liftIntensional2 @(e :×: Fold [(Text, Assertion e)]) $+ \(ref :×: _) (act :×: as) ->+ (act :×: (as <> Fold [(lab, AssertEq ref act)]))++-- Here is an example of how to "run" `CollectAssertions`:+--+-- collectAssertions ::+-- (ConstExp e, NumExp e, CompareExp e, VarExp e, LetIntensional e)+-- => (forall e'. ( ConstExp e'+-- , NumExp e'+-- , CompareExp e'+-- , AssertExp e'+-- , LetExp e'+-- ) =>+-- Exp e' a+-- )+-- -> [(Text, Assertion e)]+-- collectAssertions =+-- fold . prodSnd . prodSnd . unIntensional . unCollectAssertions . unExp+--+-- Note that the interpretation type is different in the argument and the+-- result. But the two are related in the following way:+--+-- * FOS classes that appear as constraints on `e'` must also appear as+-- constraints on `e`.+-- * Each HOS class constraint on `e'` requires a corresponding intensional+-- class constraint on `e`.+--+-- Note that the `AssertExp` constraint on `e'` isn't needed on `e`.
+ src/Dino/Prelude.hs view
@@ -0,0 +1,64 @@+-- | Prelude for Dino expressions+--+-- This module mostly re-exports the standard "Prelude", but hides identifiers+-- that are overridden by Dino definitions.++module Dino.Prelude+ ( module Prelude+ , HasField+ , Hashable+ , IsLabel+ , KnownSymbol+ , Symbol+ , Text+ , Typeable++ -- Needed when `RebindableSyntax` is enabled:+ , fromLabel+ , fromString+ , join+ ) where++-- Regarding the exports:+--+-- * Dino code and ordinary application code normally live in separate+-- modules. Dino code normally doesn't need to use IO, except maybe for+-- calling a back end and printing results. Hence it only needs a simple+-- prelude.+--+-- * Dino is supposed to be used by non-developers who are maybe Haskell+-- beginners. The standard Prelude seems suitable for them.+--+-- * Prelude deficiencies such as `String` and partial functions are no+-- problem for Dino code, since Haskell's run time is Dino's compile time.++import Prelude hiding+ ( RealFrac(..)+ , (&&)+ , (||)+ , (==)+ , (/=)+ , (<)+ , (>)+ , (<=)+ , (>=)+ , all+ , and+ , any+ , fromIntegral+ , max+ , maybe+ , min+ , not+ , or+ )+import Prelude (RealFrac)++import Control.Monad (join)+import Data.Hashable (Hashable)+import Data.String (fromString)+import Data.Text (Text)+import Data.Typeable (Typeable)+import GHC.OverloadedLabels (IsLabel (..))+import GHC.TypeLits (KnownSymbol, Symbol)+import GHC.Records (HasField)
+ src/Dino/Pretty.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- | Helpers for pretty printing+module Dino.Pretty where++import Prelude++import Data.Hashable (Hashable)+import Data.HashMap.Strict (HashMap)+import qualified Data.HashMap.Strict as HM+import Data.List (sortOn)+import Data.String (IsString)+import GHC.Generics (Generic)+import Text.PrettyPrint.ANSI.Leijen (Doc, Pretty (..), (<+>))+import qualified Text.PrettyPrint.ANSI.Leijen as PP++data Importance+ = Unimportant+ | Important+ deriving (Eq, Show, Generic)++-- | Returns 'Important' iff. any argument is 'Important'.+instance Semigroup Importance where+ Unimportant <> Unimportant = Unimportant+ _ <> _ = Important++instance Hashable Importance++-- | Marks a part of a value that hasn't changed+unchanged :: Doc+unchanged = PP.magenta $ PP.text "*"++-- | Emphasize when 'Important'+emphasize :: Importance -> Doc -> Doc+emphasize Unimportant = id+emphasize Important = PP.bold . PP.blue++-- | Place a document indented under a header:+--+-- > header+-- > doc+-- > doc+-- > ...+underHeader ::+ Doc -- ^ Header+ -> Doc -- ^ Document to place under the header+ -> Doc+underHeader h d = h PP.<$> PP.space <+> PP.align d++-- | Render a list of documents as follows:+--+-- > [ a+-- > , b+-- > , ...+-- > ]+--+-- where @'['@, @','@ and @']'@ are provided as the first three parameters.+verticalList :: Doc -> Doc -> Doc -> [Doc] -> Doc+verticalList l _ r [] = l <+> r+verticalList l sep r ds =+ PP.vcat [c <+> PP.align d | (c, d) <- zip (l : repeat sep) ds] PP.<$> r++-- | A wrapper for 'String' with a 'Show' instance that omits quotes+--+-- Useful in situations where 'show' is (ab)used to provide conversion to+-- 'String' rather than for displaying values.+newtype Field = Field {unField :: String}+ deriving (Eq, Ord, IsString, Hashable)++instance Show Field where+ show = unField++instance Pretty Field where+ pretty = PP.string . unField++-- | Render a record as follows:+--+-- > { field1 =+-- > value1+-- > , field2 =+-- > value2+-- > , ...+-- > }+--+-- If @k@ is a 'String'-like type, it will be shown with quotes. Use 'Field' to+-- prevent this.+prettyRecord :: (Show k, Ord k) => Importance -> HashMap k Doc -> Doc+prettyRecord imp =+ verticalList PP.lbrace PP.comma PP.rbrace .+ map prettyField . sortOn fst . HM.toList+ where+ prettyField (f, v) =+ underHeader (emphasize imp (PP.string (show f)) <+> PP.string "=") v
+ src/Dino/Types.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Dino.Types+ ( module Dino.Types+ , Inspectable+ ) where++import Dino.Prelude++import Data.Type.Equality ((:~:) (..), TestEquality (..))+import Data.Typeable (cast)+import Type.Reflection (typeRep)++import Dino.AST (Inspectable)++-- | Built-in Dino types+--+-- Whether or not a type is built-in is mostly an implementation detail.+type family BuiltIn a :: Bool where+ BuiltIn [a] = 'True+ BuiltIn (a, b) = 'True+ BuiltIn a = 'False++data DinoTypeRep a where+ ListType :: DinoTypeRep a -> DinoTypeRep [a]+ PairType :: DinoTypeRep a -> DinoTypeRep b -> DinoTypeRep (a, b)+ OtherType :: (BuiltIn a ~ 'False, DinoType a) => DinoTypeRep a+ -- The `BuiltIn` constraint ensures that `DinoTypeRep` is a canonical+ -- representation for built-in types. This allows us to give total definitions+ -- of functions like `listElemType`.++ -- The reason for having a separate constructor for list types is solely to be+ -- able to implement functions like `listElemType`.++ -- The constraints on `OtherType` are somewhat arbitrary. We may bring in+ -- other constraints in the future if that is needed by a particular back end.+ -- However, we should avoid using type classes from a back end directly.+ -- Rather use generic ones, such as `Data`. We can also have different+ -- constructors for different types; e.g. numeric types, enumerations, etc.++withType :: DinoTypeRep a -> (DinoType a => b) -> b+withType (ListType t) b = withType t b+withType (PairType t u) b = withType t $ withType u b+withType OtherType b = b++listTypeElem :: DinoTypeRep [a] -> DinoTypeRep a+listTypeElem (ListType t) = t+ -- This function is total due to the `BuiltIn` constraint on `OtherType`.++-- | This instance is complete in the sense that if @t ~ u@, then+-- @`testEquality` (trep :: `DinoTypeRep` t) (urep :: `DinoTypeRep` u)@ returns+-- @`Just` `Refl`@.+--+-- For example, @`BoolType`@ and @`EnumType` :: `DinoTypeRep` `Bool`@ are+-- considered equal.+instance TestEquality DinoTypeRep where+ testEquality :: forall t u. DinoTypeRep t -> DinoTypeRep u -> Maybe (t :~: u)+ testEquality t u = withType t $ withType u $+ testEquality (typeRep @t) (typeRep @u)+ -- Note: Because `DinoTypeRep` is a canonical representation of Dino types,+ -- testing equality via `typeRep` should correspond to structural equality.++class (Eq a, Show a, Typeable a, Inspectable a) => DinoType a where+ dinoTypeRep :: DinoTypeRep a++ default dinoTypeRep :: (BuiltIn a ~ 'False) => DinoTypeRep a+ dinoTypeRep = OtherType++instance DinoType ()+instance DinoType Bool+instance DinoType Rational+instance DinoType Int+instance DinoType Integer+instance DinoType Float+instance DinoType Double+instance DinoType Text+instance DinoType a => DinoType (Maybe a)++instance DinoType a => DinoType [a] where+ dinoTypeRep = ListType dinoTypeRep++instance (DinoType a, DinoType b) => DinoType (a, b) where+ dinoTypeRep = PairType dinoTypeRep dinoTypeRep++-- | Dynamic type based on 'DinoType'+data Dinamic where+ Dinamic :: DinoType a => a -> Dinamic++fromDinamic :: DinoType a => Dinamic -> Maybe a+fromDinamic (Dinamic a) = cast a
+ src/Dino/Verification.hs view
@@ -0,0 +1,52 @@+module Dino.Verification where++import Prelude++import Data.Text (Text)+import qualified Data.Text as Text+import Text.PrettyPrint.ANSI.Leijen (Doc)+import qualified Text.PrettyPrint.ANSI.Leijen as PP++import Dino.AST.Diff+import Dino.Interpretation++-- | Check each 'assertEq' assertion by structurally comparing the ASTs of the+-- two expressions+--+-- This limited form of formal verification is useful two ways:+--+-- * It can be used to verify refactorings that don't affect the AST; for+-- example, introducing a meta-level helper function (i.e. a normal Haskell+-- function).+--+-- * When the ASTs do differ, the resulting 'Edit' will show only the parts of+-- the expressions where the difference occurs, which can make it easier to+-- manually verify equivalence.+verifyAssertEqStructurally ::+ CollectAssertions Reified a -> [(Text, Maybe (Edit NumRep))]+verifyAssertEqStructurally e =+ [ (lab, diff (unReified ref) (unReified act))+ | (lab, AssertEq ref act) <- as+ ]+ where+ as = fold $ prodSnd $ prodSnd $ unIntensional $ unCollectAssertions e++-- | Present the output of 'verifyAssertEqStructurally' as a list of test cases+-- that either succeed or fail with a diff+presentStructuralVerificationAsDocs :: [(Text, Maybe (Edit NumRep))] -> [Doc]+presentStructuralVerificationAsDocs as = map mkCase as+ where+ l = maximum (0 : map (Text.length . fst) as)+ l' = min l 20++ showLabel lab =+ Text.unpack lab ++ ":" ++ replicate (l' - Text.length lab) ' '++ mkCase (lab, d) =+ PP.string (showLabel lab) <> PP.space <> diffAsTestResult d <> end+ where+ end = maybe mempty (const $ mempty PP.<$> mempty) d++presentStructuralVerification :: [(Text, Maybe (Edit NumRep))] -> IO ()+presentStructuralVerification =+ PP.putDoc . PP.vsep . presentStructuralVerificationAsDocs
+ test/DiffTest.hs view
@@ -0,0 +1,194 @@+{-# LANGUAGE TemplateHaskell #-}++{-# OPTIONS_GHC -Wno-missing-signatures #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module DiffTest where++import Prelude++import Control.Monad (replicateM)+import qualified Data.HashMap.Strict as HM+import Data.Maybe (fromJust, isJust, isNothing)+import Data.Text (Text)+import qualified Data.Text as Text++import Dino.Pretty+import Dino.AST+import Dino.AST.Diff hiding (new)++import Test.Tasty.QuickCheck+import Test.Tasty.TH++instance Arbitrary NameType where+ arbitrary = oneof $ map pure [minBound .. maxBound]++-- | Generate a short text consisting of alphabetic characters+instance Arbitrary Text where+ arbitrary = do+ n <- choose (1,6)+ fmap Text.pack $ vectorOf n $ choose ('a', 'z')++ shrink "v" = []+ shrink _ = ["v"]++instance Arbitrary Field where+ arbitrary = do+ n <- choose (1,6)+ fmap Field $ vectorOf n $ choose ('a', 'z')++instance Arbitrary Constr where+ arbitrary = frequency+ [ (1, return List)+ , (1, return Tuple)+ , (3, Named <$> arbitrary <*> arbitrary)+ ]++ shrink List = []+ shrink _ = [List]++instance Arbitrary a => Arbitrary (Mapping Field a) where+ arbitrary = sized $ \s -> do+ n <- choose (0, s)+ Mapping Unimportant . HM.fromList <$>+ replicateM n ((,) <$> arbitrary <*> resize (s `div` n) arbitrary)++-- | Generate an 'AST' of bounded size+genAST :: Arbitrary a => Int -> Gen (AST a)+genAST s =+ frequency+ [ (1, Number <$> arbitrary)+ , (1, Text <$> arbitrary)+ , (s, ) $ do+ n <- choose (0, s)+ App <$> arbitrary <*> replicateM n (genAST (s `div` n))+ , (s, ) $ Let <$> arbitrary <*> genAST (s `div` 2) <*> genAST (s `div` 2)+ , (s, ) . fmap Record $ resize s arbitrary+ ]++shrinkAST :: Arbitrary a => AST a -> [AST a]+shrinkAST (Number _) = [Text ""]+shrinkAST (Text _) = []+shrinkAST (App c as) = as ++ map (uncurry App) (shrink (c, as))+shrinkAST (Let v a b) =+ [a, b] ++ [Let v' a' b' | (a', b') <- shrink (a, b), v' <- shrink v]+shrinkAST (Record (Mapping imp rec)) =+ HM.elems rec +++ [App List $ HM.elems rec] +++ map+ (Record . Mapping imp . HM.fromList)+ (shrinkList (\(f, a) -> map (f, ) $ shrink a) $ HM.toList rec)++instance Arbitrary a => Arbitrary (AST a) where+ arbitrary = sized genAST+ shrink = shrinkAST++oldOrNew :: Arbitrary a => a -> Gen a+oldOrNew a = frequency [(1, resize 3 arbitrary), (5, return a)]++class ArbitraryRelative a where+ -- | Generate a value by applying small changes to an existing value+ genRelative :: a -> Gen a++ default genRelative :: Arbitrary a => a -> Gen a+ genRelative = oldOrNew++instance (Arbitrary a, ArbitraryRelative a) => ArbitraryRelative [a] where+ genRelative as = do+ as' <- mapM (\a -> frequency [(4, return a), (1, genRelative a)]) as+ frequency+ [ (3, ) $ return as'+ , (1, ) $ do+ n <- choose (0, 2)+ return $ dropEnd n as'+ , (1, ) $ do+ n <- choose (0, 2)+ (as' ++) <$> replicateM n (resize 3 arbitrary)+ ]++instance (Arbitrary a, ArbitraryRelative a) => ArbitraryRelative (Maybe a) where+ genRelative Nothing = oldOrNew Nothing+ genRelative (Just a) = frequency+ [ (1, return Nothing)+ , (4, Just <$> genRelative a)+ ]++instance (Arbitrary a, ArbitraryRelative a) =>+ ArbitraryRelative (Mapping Field a) where+ genRelative (Mapping imp m) =+ frequency+ [ ( 4+ , do m' <-+ fmap (HM.mapMaybe id) $+ flip traverse m $ \a ->+ frequency+ [ (3, Just <$> return a)+ , (1, Just <$> genRelative a)+ , (1, return Nothing)+ ]+ Mapping _ m'' <- resize 3 arbitrary+ return $ Mapping imp $ HM.union m'' m')+ , (1, resize 5 arbitrary)+ ]++instance (ArbitraryRelative a, ArbitraryRelative b) =>+ ArbitraryRelative (a, b) where+ genRelative (a, b) = (,) <$> genRelative a <*> genRelative b++instance ArbitraryRelative Constr++instance Arbitrary a => ArbitraryRelative (AST a) where+ genRelative (Number a) = frequency+ [ (4, return $ Number a)+ , (2, Number <$> arbitrary)+ , (1, genAST 3)+ ]+ genRelative (Text a) = frequency+ [ (4, return $ Text a)+ , (2, Text <$> arbitrary)+ , (1, genAST 3)+ ]+ genRelative (App c as) = frequency+ [ (4, App <$> genRelative c <*> genRelative as)+ , (1, genAST 3)+ ]+ genRelative (Let v a b) = frequency+ [ (4, Let <$> oldOrNew v <*> genRelative a <*> genRelative b)+ , (1, genAST 3)+ ]+ genRelative (Record rec) = frequency+ [ (4, Record <$> genRelative rec)+ , (1, genAST 3)+ ]++genEdit :: Int -> Gen (Edit Int)+genEdit s = do+ ast <- genAST s+ rel <- genRelative ast+ maybe (genEdit s) return $ diff ast rel++-- | If the edit is empty, then @ast@ and @rel@ are equal+prop_diffEq1 =+ forAllShrink (genAST 8) shrinkAST $ \(a :: AST Int) ->+ forAllShrink (genRelative a) shrinkAST $ \rel ->+ isNothing (diff a rel) ==> a == rel++-- | If @ast@ and @rel@ are equal, then the edit is empty+prop_diffEq2 =+ forAllShrink (genAST 8) shrinkAST $ \(a :: AST Int) ->+ forAllShrink (genRelative a) shrinkAST $ \rel ->+ a == rel ==> isNothing (diff a rel)++-- | Applying the calculated edit to the original retrieves the new 'AST'+prop_diffApply (orig :: AST Int) =+ forAllShrink (genRelative orig) shrinkAST $ \new ->+ let e = diff orig new+ in isJust e ==> applyDiff (fromJust e) orig == Just new++-- TODO Test that the diff is "optimal". E.g. don't use `Replacement` when a+-- smaller representation of the diff exists.++-- TODO Property that tests when `applyDiff` must return `Nothing`. Probably+-- hard...++tests = $testGroupGenerator
+ test/Tests.hs view
@@ -0,0 +1,7 @@+{-# OPTIONS_GHC -Wno-missing-signatures #-}++import Test.Tasty++import qualified DiffTest++main = defaultMain DiffTest.tests