.direnv/
.ghc.environment.*
.stack-work/
+dist/
dist-newstyle/
dump-core/
hlint.html
- name: TypeApplications
- ignore: {name: Avoid lambda}
+- ignore: {name: Collapse lambdas}
- ignore: {name: Move brackets to avoid $}
- ignore: {name: Reduce duplication}
- ignore: {name: Redundant $}
- ignore: {name: Use camelCase}
- ignore: {name: Use const}
- ignore: {name: Use fmap}
+- ignore: {name: Use guards}
- ignore: {name: Use id}
- ignore: {name: Use if}
- ignore: {name: Use import/export shortcut}
Copyright: Julien Moutinho <julm+symantic-base@sourcephile.fr>
License: CC0-1.0
-Files: src/*
+Files: src/* tests/*
Copyright: Julien Moutinho <julm+symantic-base@sourcephile.fr>
License: AGPL-3.0-or-later
cabal_builddir ?= dist-newstyle
override REPL_OPTIONS += -ignore-dot-ghci
+override TEST_OPTIONS +=
override GHCID_OPTIONS += --no-height-limit --reverse-errors --color=always --warnings --restart $(cabal)
+# Note that cabal's v1-* commands are required to use sydtest-discover from $PATH
+# instead of requiring a cabal update to build it.
+
all: build
build:
- cabal build $(CABAL_BUILD_FLAGS)
+ cabal v1-build $(CABAL_BUILD_FLAGS)
clean c:
cabal clean
repl:
- cabal repl $(CABAL_REPL_FLAGS) $(project)
+ cabal v1-repl $(CABAL_REPL_FLAGS) $(project)
ghcid:
- ghcid $(GHCID_OPTIONS) --command 'cabal repl -fno-code $(CABAL_REPL_FLAGS) $(project) $(addprefix --repl-options ,$(REPL_OPTIONS))'
+ ghcid $(GHCID_OPTIONS) --command 'cabal v1-repl $(CABAL_REPL_FLAGS) $(project) $(addprefix --repl-options ,$(REPL_OPTIONS))'
+
+.PHONY: tests
+t tests:
+ cabal v1-test $(CABAL_TEST_FLAGS) \
+ --show-details always --test-options "$(TEST_OPTIONS)"
+t/repl tests/repl:
+ cabal v1-repl $(CABAL_REPL_FLAGS) $(CABAL_TEST_FLAGS) $(project)-tests
+t/ghcid tests/ghcid:
+ ghcid $(GHCID_OPTIONS) --command 'cabal v1-repl $(CABAL_REPL_FLAGS) $(project) $(addprefix --repl-options ,$(REPL_OPTIONS))' \
+ --run=':! ghcid $(GHCID_OPTIONS) --command "cabal v1-repl $(CABAL_REPL_FLAGS) $(CABAL_TEST_FLAGS) $(project)-tests" --test ":main $(TEST_OPTIONS)"'
+
+%/accept: TEST_OPTIONS += --accept
+%/accept: %
+
+%/cover: CABAL_TEST_FLAGS += --enable-coverage
+%/cover: %
+
doc:
cabal haddock --haddock-css ocean --haddock-hyperlink-source
+++ /dev/null
-packages:.
{
"nodes": {
- "flake-utils": {
+ "flake-compat": {
+ "flake": false,
"locked": {
- "lastModified": 1667077288,
- "narHash": "sha256-bdC8sFNDpT0HK74u9fUkpbf1MEzVYJ+ka7NXCdgBoaA=",
- "owner": "numtide",
- "repo": "flake-utils",
- "rev": "6ee9ebb6b1ee695d2cacc4faa053a7b9baa76817",
+ "lastModified": 1696426674,
+ "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=",
+ "owner": "edolstra",
+ "repo": "flake-compat",
+ "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33",
"type": "github"
},
"original": {
- "owner": "numtide",
- "repo": "flake-utils",
+ "owner": "edolstra",
+ "repo": "flake-compat",
"type": "github"
}
},
- "nixpkgs": {
+ "git-hooks": {
+ "inputs": {
+ "flake-compat": "flake-compat",
+ "gitignore": "gitignore",
+ "nixpkgs": [
+ "nixpkgs"
+ ],
+ "nixpkgs-stable": "nixpkgs-stable"
+ },
"locked": {
- "lastModified": 1691328192,
- "narHash": "sha256-w59N1zyDQ7SupfMJLFvtms/SIVbdryqlw5AS4+DiH+Y=",
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "61676e4dcfeeb058f255294bcb08ea7f3bc3ce56",
+ "lastModified": 1715870890,
+ "narHash": "sha256-nacSOeXtUEM77Gn0G4bTdEOeFIrkCBXiyyFZtdGwuH0=",
+ "owner": "cachix",
+ "repo": "git-hooks.nix",
+ "rev": "fa606cccd7b0ccebe2880051208e4a0f61bfc8c1",
"type": "github"
},
"original": {
- "id": "nixpkgs",
- "type": "indirect"
+ "owner": "cachix",
+ "repo": "git-hooks.nix",
+ "type": "github"
}
},
- "pre-commit-hooks": {
+ "gitignore": {
"inputs": {
- "flake-utils": "flake-utils",
"nixpkgs": [
+ "git-hooks",
"nixpkgs"
]
},
"locked": {
- "lastModified": 1667992213,
- "narHash": "sha256-8Ens8ozllvlaFMCZBxg6S7oUyynYx2v7yleC5M0jJsE=",
- "owner": "cachix",
- "repo": "pre-commit-hooks.nix",
- "rev": "ebcbfe09d2bd6d15f68de3a0ebb1e4dcb5cd324b",
+ "lastModified": 1709087332,
+ "narHash": "sha256-HG2cCnktfHsKV0s4XW83gU3F57gaTljL9KNSuG6bnQs=",
+ "owner": "hercules-ci",
+ "repo": "gitignore.nix",
+ "rev": "637db329424fd7e46cf4185293b9cc8c88c95394",
"type": "github"
},
"original": {
- "owner": "cachix",
- "repo": "pre-commit-hooks.nix",
+ "owner": "hercules-ci",
+ "repo": "gitignore.nix",
+ "type": "github"
+ }
+ },
+ "nixpkgs": {
+ "locked": {
+ "lastModified": 1712310679,
+ "narHash": "sha256-XgC/a/giEeNkhme/AV1ToipoZ/IVm1MV2ntiK4Tm+pw=",
+ "path": "/nix/store/8mk40j3mfrvndrnh89azngcgdgr1fidi-source",
+ "rev": "72da83d9515b43550436891f538ff41d68eecc7f",
+ "type": "path"
+ },
+ "original": {
+ "id": "nixpkgs",
+ "type": "indirect"
+ }
+ },
+ "nixpkgs-stable": {
+ "locked": {
+ "lastModified": 1710695816,
+ "narHash": "sha256-3Eh7fhEID17pv9ZxrPwCLfqXnYP006RKzSs0JptsN84=",
+ "owner": "NixOS",
+ "repo": "nixpkgs",
+ "rev": "614b4613980a522ba49f0d194531beddbb7220d3",
+ "type": "github"
+ },
+ "original": {
+ "owner": "NixOS",
+ "ref": "nixos-23.11",
+ "repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
- "nixpkgs": "nixpkgs",
- "pre-commit-hooks": "pre-commit-hooks"
+ "git-hooks": "git-hooks",
+ "nixpkgs": "nixpkgs"
}
}
},
{
inputs = {
nixpkgs.url = "flake:nixpkgs";
- pre-commit-hooks.url = "github:cachix/pre-commit-hooks.nix";
- pre-commit-hooks.inputs.nixpkgs.follows = "nixpkgs";
+ git-hooks.url = "github:cachix/git-hooks.nix";
+ git-hooks.inputs.nixpkgs.follows = "nixpkgs";
};
outputs = inputs:
let
pkg = "symantic-base";
lib = inputs.nixpkgs.lib;
+ fileInputs = with lib.fileset; toSource {
+ root = ./.;
+ fileset = unions [
+ ./symantic-base.cabal
+ ./LICENSES
+ (fileFilter (file: lib.any file.hasExt [ ".hs" ]) ./src)
+ (fileFilter (file: lib.any file.hasExt [ ".hs" ]) ./tests)
+ ];
+ };
forAllSystems = f: lib.genAttrs lib.systems.flakeExposed (system: f rec {
inherit system;
pkgs = inputs.nixpkgs.legacyPackages.${system};
haskellPackages = pkgs.haskellPackages.extend (with pkgs.haskell.lib; hfinal: hsuper: {
- ${pkg} = buildFromSdist (hfinal.callCabal2nix pkg ./. { });
+ ${pkg} = buildFromSdist (hfinal.callCabal2nix pkg fileInputs { });
});
});
in
rec {
# nix -L build
- defaultPackage = forAllSystems ({ haskellPackages, ... }: haskellPackages.${pkg});
+ packages = forAllSystems ({ haskellPackages, ... }: {
+ default = haskellPackages.${pkg};
+ });
# nix -L develop or direnv allow
- devShell = forAllSystems ({ pkgs, haskellPackages, system, ... }:
- haskellPackages.shellFor {
- packages = ps: [ ps.${pkg} ];
- nativeBuildInputs = [
- haskellPackages.cabal-install
- haskellPackages.ghcid
- haskellPackages.haskell-language-server
- haskellPackages.hlint
- pkgs.git-chglog
- pkgs.reuse
- ];
- withHoogle = false;
- inherit (checks.${system}.pre-commit-check) shellHook;
- });
+ devShells = forAllSystems ({ pkgs, haskellPackages, system, ... }: {
+ default =
+ haskellPackages.shellFor {
+ packages = ps: [ ps.${pkg} ];
+ nativeBuildInputs = [
+ haskellPackages.cabal-install
+ haskellPackages.ghcid
+ haskellPackages.haskell-language-server
+ haskellPackages.hlint
+ pkgs.git-chglog
+ pkgs.reuse
+ ];
+ withHoogle = false;
+ inherit (checks.${system}.git-hooks-check) shellHook;
+ };
+ });
# nix flake check
checks = forAllSystems (args: with args; {
- pre-commit-check = inputs.pre-commit-hooks.lib.${system}.run {
+ git-hooks-check = inputs.git-hooks.lib.${system}.run {
src = ./.;
- #settings.ormolu.cabalDefaultExtensions = true;
- settings.ormolu.defaultExtensions = [
- "ImportQualifiedPost"
- "TypeApplications"
- ];
hooks = {
+ ormolu.settings.cabalDefaultExtensions = true;
+ cabal-fmt.enable = true;
+ fourmolu.enable = true;
hlint.enable = true;
nixpkgs-fmt.enable = true;
- fourmolu.enable = true;
- cabal-fmt.enable = true;
+ reuse = {
+ enable = true;
+ entry = "${pkgs.reuse}/bin/reuse lint";
+ pass_filenames = false;
+ };
};
};
});
{-# OPTIONS_GHC -fno-warn-orphans #-}
--- | This module provides the 'Identity' semantic
+
+-- | This module provides the 'Identity' and 'IdentityT' semantics
-- which interprets the combinators as a Haskell value.
-module Symantic.Semantics.Identity
- ( Identity(..)
- ) where
+module Symantic.Semantics.Identity (
+ Identity (..),
+ IdentityT (..),
+) where
import Control.Applicative qualified as App
+import Control.Monad.Trans.Identity (IdentityT (..))
import Data.Either qualified as Either
import Data.Eq qualified as Eq
import Data.Function qualified as Fun
-import Data.Functor.Identity (Identity(..))
+import Data.Functor.Identity (Identity (..))
import Data.Maybe qualified as Maybe
+import Debug.Trace (traceShow)
+import Text.Show (Show)
+
import Symantic.Syntaxes.Classes
+import Symantic.Syntaxes.Derive
--- * Type 'Identity'
+-- * Type 'IdentityT'
+type instance Derived (IdentityT sem) = sem
+instance Derivable (IdentityT sem) where
+ derive = runIdentityT
+instance LiftDerived (IdentityT sem) where
+ liftDerived = IdentityT
+instance LiftDerived1 (IdentityT sem) where
+ liftDerived1 f = IdentityT Fun.. f Fun.. runIdentityT
+instance LiftDerived2 (IdentityT sem) where
+ liftDerived2 f x y = IdentityT (f (runIdentityT x) (runIdentityT y))
+instance LiftDerived3 (IdentityT sem) where
+ liftDerived3 f x y z = IdentityT (f (runIdentityT x) (runIdentityT y) (runIdentityT z))
+instance LiftDerived4 (IdentityT sem) where
+ liftDerived4 f w x y z = IdentityT (f (runIdentityT w) (runIdentityT x) (runIdentityT y) (runIdentityT z))
+
+instance Abstractable sem => Abstractable (IdentityT sem)
+instance Abstractable1 sem => Abstractable1 (IdentityT sem)
+instance Anythingable sem => Anythingable (IdentityT sem)
+instance Constantable c sem => Constantable c (IdentityT sem)
+instance Eitherable sem => Eitherable (IdentityT sem)
+instance Equalable sem => Equalable (IdentityT sem)
+instance IfThenElseable sem => IfThenElseable (IdentityT sem)
+instance Instantiable sem => Instantiable (IdentityT sem)
+instance LetRecable idx sem => LetRecable idx (IdentityT sem)
+instance Listable sem => Listable (IdentityT sem)
+instance Maybeable sem => Maybeable (IdentityT sem)
+instance Unabstractable sem => Unabstractable (IdentityT sem)
+instance Varable sem => Varable (IdentityT sem)
+
+-- * Type 'Identity'
instance Abstractable Identity where
lam f = Identity (runIdentity Fun.. f Fun.. Identity)
instance Abstractable1 Identity where
instance Equalable Identity where
equal = Identity (Eq.==)
instance IfThenElseable Identity where
- ifThenElse test ok ko = Identity
- (if runIdentity test
- then runIdentity ok
- else runIdentity ko)
+ ifThenElse test ok ko =
+ Identity
+ ( if runIdentity test
+ then runIdentity ok
+ else runIdentity ko
+ )
instance Instantiable Identity where
Identity f .@ Identity x = Identity (f x)
instance Listable Identity where
($) = Identity (Fun.$)
instance Varable Identity where
var = Fun.id
+instance Letable Identity where
+ let_ e body = body e
+instance Show idx => LetRecable idx Identity where
+ letRec _idx f body =
+ Identity Fun.$
+ -- traceShow ["Identity", "letRec"] Fun.$
+ let self idx =
+ -- traceShow (["Identity", "letRec", "self"], ("idx", idx)) Fun.$
+ runIdentity (f (Identity Fun.. self) idx)
+ in runIdentity (body (Identity Fun.. self))
--- /dev/null
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+-- For Syn.LetRecable
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symantic.Semantics.LetInserter where
+
+import Control.Applicative (liftA2, liftA3)
+import Control.Monad (Monad (..))
+import Control.Monad.Trans.State.Strict qualified as MT
+import Data.Bool (Bool (..), not, otherwise, (&&))
+import Data.Either (Either (..))
+import Data.Eq (Eq (..))
+import Data.Foldable (foldMap)
+import Data.Function (const, id, on, ($), (.))
+import Data.Functor ((<$>))
+import Data.Int (Int)
+import Data.Kind (Type)
+import Data.List qualified as List
+import Data.Maybe (Maybe (..), isNothing, maybe)
+import Data.Ord (Ord (..))
+import Data.Semigroup (Semigroup (..))
+import Data.Set qualified as Set
+import Debug.Trace qualified as Trace
+import Numeric.Natural (Natural)
+import Symantic.Syntaxes.Classes qualified as Syn
+import Symantic.Syntaxes.Derive qualified as Syn
+import Text.Show (Show (..), showListWith, showString, shows)
+import Unsafe.Coerce (unsafeCoerce)
+import Prelude (error, pred)
+import Prelude qualified
+
+-- import Control.Monad.Trans.Class qualified as MT
+-- import Data.Functor.Identity (Identity(..))
+-- import Data.Monoid (Monoid(..))
+-- import Data.String (String)
+
+traceShow :: Show a => a -> b -> b
+-- traceShow = Trace.traceShow
+traceShow _x a = a
+
+newtype Locus = Locus Natural
+ deriving (Eq, Ord)
+ deriving newtype (Show)
+
+{-
+type Locus = [Pigit]
+data Pigit = POne | PTwo | PThree | PLoc Locus | PNote String
+ deriving (Eq, Ord)
+instance Show Pigit where
+ showsPrec _p x =
+ case x of
+ POne -> shows (1::Int)
+ PTwo -> shows (2::Int)
+ PThree -> shows (3::Int)
+ PLoc loc -> shows loc
+ PNote msg -> showString msg
+-}
+
+-- * Type 'OpenCode'
+newtype OpenCode code a = OpenCode {unOpenCode :: Env code -> code a}
+type instance Syn.Derived (OpenCode code) = code
+
+-- instance Syn.Derivable (OpenCode code) where
+-- derive oc = unOpenCode oc mempty
+instance Syn.LiftDerived (OpenCode code) where
+ liftDerived x = OpenCode (const x)
+instance Syn.LiftDerived1 (OpenCode code) where
+ liftDerived1 f x = OpenCode (\env -> f (unOpenCode x env))
+instance Syn.LiftDerived2 (OpenCode code) where
+ liftDerived2 f x y = OpenCode (\env -> f (unOpenCode x env) (unOpenCode y env))
+instance Syn.LiftDerived3 (OpenCode code) where
+ liftDerived3 f x y z = OpenCode (\env -> f (unOpenCode x env) (unOpenCode y env) (unOpenCode z env))
+
+-- instance Syn.Abstractable code => Syn.Abstractable (OpenCode code) where
+-- lam f = OpenCode (\env -> Syn.lam (\x -> unOpenCode f env (unOpenCode x env)))
+-- instance Syn.Instantiable code => Syn.Instantiable (OpenCode code)
+-- instance Syn.Constantable c code => Syn.Constantable c (OpenCode code)
+instance Syn.IfThenElseable code => Syn.IfThenElseable (OpenCode code) where
+ ifThenElse x y z = OpenCode (\env -> Syn.ifThenElse (unOpenCode x env) (unOpenCode y env) (unOpenCode z env))
+instance Syn.Equalable code => Syn.Equalable (OpenCode code) where
+ equal = OpenCode (const Syn.equal)
+instance Syn.Constantable c code => Syn.Constantable c (OpenCode code)
+
+-- ** Type Env'
+type Env code = [EnvBind code]
+
+-- *** Type 'Var'
+newtype Var a = Var {unVar :: VarName}
+ deriving (Eq)
+ deriving newtype (Show)
+type VarName = Locus
+
+-- *** Type 'EnvBind'
+data EnvBind code where
+ EnvBind :: !(Var a, code a) -> EnvBind code
+instance Show (EnvBind code) where
+ showsPrec p (EnvBind (n, _e)) = showsPrec p n
+
+lookupVar :: Var a -> OpenCode code a
+lookupVar (Var v) =
+ traceShow (["lookupVar", "OpenCode"], v) $
+ OpenCode $ \env ->
+ traceShow (["lookupVar", "OpenCode", "find"], v, ("env", env)) $
+ case List.find (\(EnvBind (Var v1, _)) -> v1 == v) env of
+ Just (EnvBind (_, x)) -> unsafeCoerce x
+ Nothing -> error ("lookupVar failure for var=(" <> show v <> ") env=" <> show ((\(EnvBind (Var n, _v)) -> n) <$> env))
+
+lookupVarLetInserter :: Var a -> LetInserter code a
+lookupVarLetInserter v =
+ LetInserter $
+ return
+ AnnotatedCode
+ { annotatedCodeOpenCode = lookupVar v
+ , annotatedCodeFloatingLets = FloatingLets []
+ , annotatedCodeFreeVars = Set.singleton (unVar v)
+ }
+
+insertVar :: Var a -> code a -> Env code -> Env code
+insertVar v e env =
+ traceShow ("insertVar", v) $
+ EnvBind (v, e) : env
+
+-- * Type 'Memo'
+type Memo = Natural
+
+-- ** Type 'MaybeMemo'
+
+-- | Like a @(Maybe Memo)@ except 'Nothing' is never equal to any other value
+-- to implement unique memoization key.
+newtype MaybeMemo = MaybeMemo (Maybe Memo)
+ deriving (Show)
+
+instance Eq MaybeMemo where
+ MaybeMemo (Just x) == MaybeMemo (Just y) = x == y
+ _ == _ = False
+
+-- * Type 'FloatingLet'
+data FloatingLet code where
+ FloatingLet ::
+ { floatingLetLocus :: !(Maybe Locus)
+ -- ^ 'FloatingLet' are either inserted at the place of an explicit 'Locus',
+ -- or at the binding ('lam' or 'let_') that dominates all free variables of the bound expression,
+ -- whichever has the narrowest scope.
+ , floatingLetMemo :: !MaybeMemo
+ -- ^ Memoization key, either internal (unique) or user-specified.
+ --
+ -- The memo key defines the equivalence classes:
+ -- expressions with the same memo key are to be shared.
+ -- Therefore, if @('genLetMemo' k l e)@ finds that there is already a let-binding
+ -- produced by an earlier 'genLetMemo' with the same locus @(l)@ and the same memo key @(k)@,
+ -- @('genLetMemo' k l e) returns the code of the earlier bound variable.
+ , floatingLetVarName :: !(Var a)
+ , floatingLetBoundCode :: !(BoundCode code a)
+ , floatingLetFreeVars :: !(Set.Set VarName)
+ } ->
+ FloatingLet code
+instance Show (FloatingLet code) where
+ showsPrec _p FloatingLet{..} =
+ showString "FloatingLet{"
+ . showString "locus="
+ . shows floatingLetLocus
+ . showString ", "
+ . showString "memo="
+ . shows floatingLetMemo
+ . showString ", "
+ . showString "var="
+ . shows floatingLetVarName
+ . showString ", "
+ . showString "exp="
+ . showString (case floatingLetBoundCode of BoundCodeOpenCode{} -> "BoundCodeOpenCode"; BoundCodeLetInserter{} -> "BoundCodeLetInserter")
+ . showString ", "
+ . showString "fvs="
+ . showListWith (shows) (Set.toList floatingLetFreeVars)
+ . showString ", "
+ . showString "}"
+
+-- * Type 'VLBindings'
+
+-- A virtual let-binding.
+-- The key idea is virtual let-bindings: whereas clet introduces an ordinary let-binding
+-- whose location is fixed, glet generates the code for a fresh variable accompanied by a virtual
+-- binding of that variable. Virtual bindings do not have (yet) a fixed location: they are
+-- attached to the expression that uses their bound variables and ‘float up’ when their attached
+-- expression is incorporated into a bigger expression. Eventually, when they reach a point that
+-- a metaprogrammer has marked with a dedicated primitive, virtual bindings are converted to
+-- real let-bindings.
+newtype FloatingLets code = FloatingLets {unFloatingLets :: [FloatingLet code]}
+instance Show (FloatingLets code) where
+ showsPrec _p (FloatingLets l) = go l
+ where
+ go [] = showString "\n"
+ go (e : es) = showString "\n , " . shows e . go es
+
+-- | Append two lists skipping the duplicates.
+-- The order of elements is preserved
+mergeFloatingLets :: FloatingLets code -> FloatingLets code -> FloatingLets code
+mergeFloatingLets (FloatingLets xs) (FloatingLets ys) =
+ traceShow (["mergeFloatingLets"], xs, ys) $
+ FloatingLets (loop (List.reverse xs) ys)
+ where
+ loop acc = \case
+ [] -> List.reverse acc
+ y@FloatingLet{floatingLetVarName = Var yv} : t ->
+ case List.filter
+ ( \a@FloatingLet{floatingLetVarName = Var av} ->
+ floatingLetLocus y == floatingLetLocus a
+ && floatingLetMemo y == floatingLetMemo a
+ && yv == av
+ )
+ acc of
+ [] -> loop (y : acc) t
+ _ -> loop (acc) t
+
+-- fs ->
+-- loop (List.concatMap (\FloatingLet{floatingLetBoundCode, floatingLetLocus, floatingLetMemo, floatingLetVarName=Var av} ->
+-- if av == yv
+-- then
+-- FloatingLet { floatingLetVarName=Var yv, .. }) fs <> acc) t
+instance Semigroup (FloatingLets code) where
+ (<>) = mergeFloatingLets
+
+-- instance Monoid (FloatingLets code) where
+-- mempty = FloatingLets []
+-- mappend = (<>)
+
+-- * Type 'BoundCode'
+
+-- | Bound expression
+data BoundCode (code :: Type -> Type) a
+ = BoundCodeOpenCode !(OpenCode code a)
+ | -- | In the recursive case,
+ -- a virtual binding may carry a yet to be computed piece of code.
+ BoundCodeLetInserter !(LetInserter code a)
+
+-- * Type 'AnnotatedCode'
+
+-- | A code value.
+-- A code value is annotated only with the type of the expression it generates,
+-- with no further classifiers (at present).
+data AnnotatedCode (code :: Type -> Type) a = AnnotatedCode
+ { annotatedCodeOpenCode :: !(OpenCode code a)
+ , annotatedCodeFloatingLets :: !(FloatingLets code)
+ , annotatedCodeFreeVars :: !(Set.Set VarName)
+ -- ^ The free variables of the code,
+ -- used to limit the floating up of locus-less 'FloatingLet's
+ -- at 'lam' or 'let_' level, in order to avoid scope extrusion.
+ }
+
+-- annotatedCodeFreeVars :: AnnotatedCode code a -> Set.Set VarName
+-- annotatedCodeFreeVars annotatedCode = foldMap floatingLetFreeVars (unFloatingLets (annotatedCodeFloatingLets annotatedCode))
+
+runCD :: Syn.Letable code => AnnotatedCode code a -> code a
+runCD AnnotatedCode{annotatedCodeOpenCode = oc, annotatedCodeFloatingLets = FloatingLets bindingFLS} =
+ let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
+ in (`unOpenCode` []) $ List.foldr bindFloatingLetMemo oc bindingLFSByMemo
+runCD _ = error "runCD: virtual binding extrusion"
+
+type instance Syn.Derived (AnnotatedCode code) = OpenCode code
+instance Syn.LiftDerived (AnnotatedCode code) where
+ liftDerived x = AnnotatedCode{annotatedCodeOpenCode = x, annotatedCodeFloatingLets = FloatingLets [], annotatedCodeFreeVars = Set.empty}
+instance Syn.LiftDerived1 (AnnotatedCode code) where
+ liftDerived1 f e1 =
+ AnnotatedCode
+ { annotatedCodeOpenCode = f (annotatedCodeOpenCode e1)
+ , annotatedCodeFloatingLets = annotatedCodeFloatingLets e1
+ , annotatedCodeFreeVars = annotatedCodeFreeVars e1
+ }
+instance Syn.LiftDerived2 (AnnotatedCode code) where
+ liftDerived2 f e1 e2 =
+ AnnotatedCode
+ { annotatedCodeOpenCode = f (annotatedCodeOpenCode e1) (annotatedCodeOpenCode e2)
+ , annotatedCodeFloatingLets = mergeFloatingLets (annotatedCodeFloatingLets e1) (annotatedCodeFloatingLets e2)
+ , annotatedCodeFreeVars = annotatedCodeFreeVars e1 <> annotatedCodeFreeVars e2
+ }
+instance Syn.LiftDerived3 (AnnotatedCode code) where
+ liftDerived3 f e1 e2 e3 =
+ AnnotatedCode
+ { annotatedCodeOpenCode = f (annotatedCodeOpenCode e1) (annotatedCodeOpenCode e2) (annotatedCodeOpenCode e3)
+ , annotatedCodeFloatingLets = mergeFloatingLets (annotatedCodeFloatingLets e1) (mergeFloatingLets (annotatedCodeFloatingLets e2) (annotatedCodeFloatingLets e3))
+ , annotatedCodeFreeVars = annotatedCodeFreeVars e1 <> annotatedCodeFreeVars e2 <> annotatedCodeFreeVars e3
+ }
+instance Syn.Constantable c code => Syn.Constantable c (AnnotatedCode code)
+instance Syn.Instantiable code => Syn.Instantiable (AnnotatedCode code)
+instance Syn.IfThenElseable code => Syn.IfThenElseable (AnnotatedCode code)
+instance Syn.Equalable code => Syn.Equalable (AnnotatedCode code)
+
+-- * Type 'LetInserter'
+newtype LetInserter code a = LetInserter {unR :: MT.State Natural (AnnotatedCode code a)}
+runLetInserter :: Syn.Letable code => LetInserter code a -> code a
+runLetInserter = runCD . (`MT.evalState` 0) . unR
+
+type instance Syn.Derived (LetInserter code) = AnnotatedCode code
+instance Syn.LiftDerived (LetInserter sem) where
+ liftDerived = LetInserter . return
+instance Syn.LiftDerived1 (LetInserter sem) where
+ liftDerived1 f e1 = LetInserter (f <$> unR e1)
+instance Syn.LiftDerived2 (LetInserter sem) where
+ liftDerived2 f e1 e2 = LetInserter (liftA2 f (unR e1) (unR e2))
+instance Syn.LiftDerived3 (LetInserter sem) where
+ liftDerived3 f e1 e2 e3 = LetInserter (liftA3 f (unR e1) (unR e2) (unR e3))
+instance Syn.IfThenElseable code => Syn.IfThenElseable (LetInserter code)
+instance Syn.Equalable code => Syn.Equalable (LetInserter code)
+instance Syn.Constantable c code => Syn.Constantable c (LetInserter code)
+instance Syn.Instantiable code => Syn.Instantiable (OpenCode code)
+
+freshNatural :: MT.State Natural Natural
+freshNatural = do
+ n <- MT.get
+ MT.put (Prelude.succ n)
+ return n
+
+-- type instance Syn.Derived (LetInserter sem) = Syn.Derived sem
+freshVar :: MT.State Natural (Var a)
+freshVar = Var . Locus <$> freshNatural
+
+-- instance Syn.Constantable c sem => Syn.Constantable c (LetInserter sem) where
+-- constant c = LetInserter $ pure $ Syn.constant c
+instance Syn.Instantiable sem => Syn.Instantiable (LetInserter sem)
+
+-- f .@ x = LetInserter $ Syn.liftDerived2 (Syn..@) (unR f) (unR x)
+-- instance Syn.Abstractable sem => Syn.Abstractable (LetInserter sem) where
+-- lam f = LetInserter $ \loc ->
+-- Syn.lam $ \x ->
+-- unR (f (LetInserter (\_loc -> x)))
+-- (PNote "lam":loc)
+-- instance Syn.Abstractable code => Syn.Abstractable (LetInserter (AnnotatedCode code)) where
+-- lam body = LetInserter $ \loc ->
+-- AnnotatedCode
+-- { annotatedCodeOpenCode = _e
+-- }
+-- -- \x -> unR (body (LetInserter (\_ -> x))) (PNote "lam":loc)
+-- instance Syn.Letable (LetInserter sem) where
+-- let_ exp body = LetInserter $ \loc ->
+-- let x = unR exp (POne:loc) in
+-- unR (body (LetInserter (\_loc -> x))) (PTwo:loc)
+
+-- instance Syn.Letable code => Syn.Letable (LetInserter code) where
+-- let_ e body = LetInserter $ \loc ->
+-- let x = unR e (POne:loc) in
+-- unR (body (LetInserter (\_loc -> x))) (PTwo:loc)
+
+-- instance Syn.Letable (LetInserter sem) where
+-- let_ exp body = LetInserter (\loc -> let x = unR exp (POne:loc) in unR (body (LetInserter (\_loc -> x))) (PTwo:loc))
+-- instance Syn.IfThenElseable code => Syn.IfThenElseable (LetInserter (AnnotatedCode code)) where
+-- ifThenElse =
+-- Syn.liftDerived3 $ \bC okC koC -> OpenCode $ \env ->
+-- Syn.ifThenElse (unOpenCode bC env) (unOpenCode okC env) (unOpenCode koC env)
+-- instance Syn.FromDerived Syn.Equalable sem => Syn.Equalable (LetInserter sem) where
+-- equal = LetInserter (\loc -> trace ("equal "<>show loc) $ Syn.equal)
+
+-- | Check to see there are no duplicate 'VarName's in 'VLBindings'.
+-- This is just a safety check
+check_no_dup_varname :: FloatingLets code -> a -> a
+check_no_dup_varname = loop []
+ where
+ loop :: [VarName] -> FloatingLets code -> a -> a
+ loop _found (FloatingLets []) = id
+ loop found (FloatingLets (FloatingLet{floatingLetVarName = Var v, ..} : t))
+ | v `List.elem` found =
+ error ("Duplicate varname " <> show v <> ", with locus " <> show floatingLetLocus)
+ | otherwise = loop (v : found) (FloatingLets t)
+
+-- | let-bind all vlbindings with the given locus.
+-- This is a non-recursive case. All these let-bindings are independent
+-- It is up to the user to ensure the independence: if the bindings
+-- are dependent, the user should have introduced several loci
+-- Virtual let bindings are sort of free variables.
+-- We bind free variables later. Likewise, we bind let-bindings later.
+-- 'Memo' is ignored here.
+-- class GenLetable sem where
+-- instance Syn.Letable code => GenLetable (LetInserter (AnnotatedCode code)) where
+floatingLetVarname :: FloatingLet code -> VarName
+floatingLetVarname FloatingLet{floatingLetVarName = Var v} = v
+
+instance
+ ( Syn.Abstractable code
+ , Syn.Letable code
+ , Syn.LetRecable Int code
+ ) =>
+ Syn.Abstractable (LetInserter code)
+ where
+ lam body = LetInserter $ do
+ vname <- freshVar
+ unR $
+ Syn.liftDerived1
+ ( \bodyCD ->
+ let (bindingFLS, passingFLS) =
+ List.partition
+ (\fl -> Set.member (unVar vname) (floatingLetFreeVars fl))
+ (unFloatingLets (annotatedCodeFloatingLets bodyCD))
+ in let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
+ in traceShow
+ ( "lam"
+ , ("vname", unVar vname)
+ , ("bindingFLS", FloatingLets bindingFLS)
+ , ("passingFLS", FloatingLets passingFLS)
+ , ("bodyFreeVars", annotatedCodeFreeVars bodyCD)
+ , ("annotatedCodeFloatingLets bodyCD", annotatedCodeFloatingLets bodyCD)
+ )
+ $ Syn.liftDerived1
+ ( \bodyOC ->
+ OpenCode $ \env ->
+ Syn.lam $ \x ->
+ (`unOpenCode` insertVar vname x env) $
+ List.foldr bindFloatingLetMemo bodyOC bindingLFSByMemo
+ )
+ bodyCD
+ { annotatedCodeFloatingLets = FloatingLets passingFLS
+ , annotatedCodeFreeVars =
+ Set.delete (unVar vname) $
+ annotatedCodeFreeVars bodyCD
+ `Set.difference` Set.fromList (floatingLetVarname <$> bindingFLS)
+ }
+ )
+ (body (lookupVarLetInserter vname))
+instance
+ ( Syn.Letable code
+ , Syn.LetRecable Int code
+ ) =>
+ Syn.Letable (LetInserter code)
+ where
+ let_ expR body = LetInserter $ do
+ vname <- freshVar
+ unR $
+ Syn.liftDerived2
+ ( \expCD bodyCD ->
+ let (bindingFLS, passingFLS) =
+ List.partition
+ (\fl -> Set.member (unVar vname) (floatingLetFreeVars fl))
+ (unFloatingLets (annotatedCodeFloatingLets bodyCD))
+ in let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
+ in Syn.liftDerived2
+ ( \expOC bodyOC ->
+ OpenCode $ \env ->
+ Syn.let_ (unOpenCode expOC env) $ \x ->
+ (`unOpenCode` (insertVar vname x env)) $
+ List.foldr bindFloatingLetMemo bodyOC bindingLFSByMemo
+ )
+ expCD
+ bodyCD
+ { annotatedCodeFloatingLets = FloatingLets passingFLS
+ , annotatedCodeFreeVars =
+ Set.delete (unVar vname) $
+ annotatedCodeFreeVars bodyCD
+ `Set.difference` Set.fromList (floatingLetVarname <$> bindingFLS)
+ }
+ )
+ expR
+ (body (lookupVarLetInserter vname))
+
+bindLet :: Syn.Letable code => FloatingLet code -> OpenCode code a -> OpenCode code a
+bindLet fl2@FloatingLet{..} c =
+ traceShow ("bindLet", fl2) $
+ case floatingLetBoundCode of
+ BoundCodeOpenCode oc -> OpenCode $ \env ->
+ Syn.let_ (unOpenCode oc env) $ \x ->
+ unOpenCode c $
+ -- traceShow ("bindLet", floatingLetVarName) $
+ insertVar floatingLetVarName x env
+ _ -> error "bindLet is always called for evaluated bindings, without latent bound exp"
+
+-- instance Syn.LetRecable idx (LetInserter sem) where
+-- letRec _idx f body =
+-- let self idx = LetInserter (\loc ->
+-- --trace ("letRec "<>show loc) $
+-- unR (f self idx) (PNote "fix":loc))
+-- in body self
+
+-- mletRec :: p -> ((t1 -> LetInserter sem a) -> t1 -> LetInserter sem a) -> ((t1 -> LetInserter sem a) -> t2) -> t2
+-- mletRec _idx f body =
+-- let self idx = LetInserter $
+-- --trace ("letRec "<>show loc) $
+-- unR (f self idx)
+-- in body self
+--
+-- letR ::
+-- Syn.LetRecable Int sem =>
+-- (sem a -> sem a) ->
+-- (sem a -> sem w) ->
+-- sem w
+-- letR f body = Syn.letRec (1::Int)
+-- (\self _idx -> f (self 0))
+-- (\self -> body (self 0))
+-- type family MemoKey (sem:: Type -> Type) where MemoKey a = Memo
+
+-- | Memoizing non-recursive genLet
+class MemoGenLetable sem where
+ withLocus :: (Locus -> sem a) -> sem a
+ genLetMemoAtMaybe :: Maybe Memo -> Maybe Locus -> sem a -> sem a
+
+genLetMemo :: MemoGenLetable sem => Memo -> Locus -> sem a -> sem a
+genLetMemo m l = genLetMemoAtMaybe (Just m) (Just l)
+
+genLet :: MemoGenLetable sem => sem a -> sem a
+genLet = genLetMemoAtMaybe Nothing Nothing
+
+genLetAt :: MemoGenLetable sem => Locus -> sem a -> sem a
+genLetAt = genLetMemoAtMaybe Nothing . Just
+
+instance Syn.Letable code => MemoGenLetable (LetInserter code) where
+ withLocus body = LetInserter $ do
+ lname <- Locus <$> freshNatural
+ bodyCD <- unR (body lname)
+ let fls = annotatedCodeFloatingLets bodyCD
+ let bindingByLocusFLS = List.filter (\fl -> floatingLetLocus fl == Just lname) (unFloatingLets fls)
+ let bindingVars = foldMap (Set.singleton . floatingLetVarname) bindingByLocusFLS
+ let (bindingFLS, passingFLS) = List.partition (\fl -> not (Set.disjoint bindingVars (floatingLetFreeVars fl))) (unFloatingLets fls)
+ let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
+ return $
+ traceShow (["withLocus"], ("bindingLFSByMemo", bindingLFSByMemo)) $
+ -- check_no_dup_varname (annotatedCodeFloatingLets bodyCD) $
+ AnnotatedCode
+ { annotatedCodeOpenCode = List.foldr bindFloatingLetMemo (annotatedCodeOpenCode bodyCD) bindingLFSByMemo
+ , annotatedCodeFloatingLets = FloatingLets passingFLS
+ , annotatedCodeFreeVars = annotatedCodeFreeVars bodyCD `Set.difference` Set.fromList (floatingLetVarname <$> bindingFLS)
+ }
+ genLetMemoAtMaybe keyMaybe mlname body = LetInserter $ traceShow (["genLetMemoAtMaybe"]) $ do
+ vname <- freshVar
+ -- mkey <- runIdentity <$> unR key
+ bodyCD <-
+ traceShow ("genLetMemoAtMaybe", ("vname", vname), ("key", keyMaybe)) $
+ unR body
+ let fvs = Set.insert (unVar vname) (annotatedCodeFreeVars bodyCD)
+ -- if the bodyression to let-bind has itself let-bindings,
+ -- they are straightened out
+ -- The new binding is added at the end; it may depend on
+ -- the bindings in evl (as is the case for the nested genLet)
+ return $
+ AnnotatedCode
+ { annotatedCodeOpenCode = lookupVar vname
+ , annotatedCodeFloatingLets =
+ FloatingLets $
+ unFloatingLets (annotatedCodeFloatingLets bodyCD)
+ <> [ FloatingLet
+ { floatingLetLocus = mlname
+ , floatingLetMemo = MaybeMemo keyMaybe
+ , floatingLetVarName = vname
+ , floatingLetBoundCode = BoundCodeOpenCode (annotatedCodeOpenCode bodyCD)
+ , floatingLetFreeVars = fvs
+ }
+ ]
+ , annotatedCodeFreeVars = fvs
+ }
+
+-- Bind the variables in order, preserving the dependency.
+-- Bind only one variable within each group, substituting the others
+bindFloatingLetMemo :: Syn.Letable code => [FloatingLet code] -> OpenCode code a -> OpenCode code a
+bindFloatingLetMemo gr oc =
+ traceShow (["withLocus", "bindFloatingLetMemo"]) $
+ case assertSameLocuses gr of
+ [] -> error "bindFloatingLetMemo: empty group"
+ [fl] -> bindLet fl oc
+ fl@FloatingLet{floatingLetVarName = vName} : fls ->
+ bindLet fl $ OpenCode $ \env ->
+ let defCode = unOpenCode (lookupVar vName) env
+ in let ext_equ env' fl2 =
+ reBind2 (memKey fl) defCode fl2
+ : env'
+ in unOpenCode oc $ List.foldl' ext_equ env fls
+ where
+ memKey fl@FloatingLet{floatingLetBoundCode = BoundCodeOpenCode{}} = floatingLetMemo fl
+ memKey fl = error $ "group pust be canonical: " <> show fl
+
+assertSameLocuses :: [FloatingLet code] -> [FloatingLet code]
+assertSameLocuses fls
+ | Set.size (foldMap (Set.singleton . floatingLetLocus) fls) <= 1 = traceShow ("assertSameLocuses", fls) fls
+ | otherwise = error "assertSameLocuses"
+
+-- | Especially for 'Locus', all bindings have the same type.
+-- In any event, 'Locus' plus the 'Memo' key witness for the bindings' type.
+reBind2 :: MaybeMemo -> code a -> FloatingLet sem -> EnvBind code
+reBind2 k c fl
+ | k == floatingLetMemo fl =
+ traceShow (["reBind2"], ("k", k), ("fl", fl)) $
+ EnvBind (Var (floatingLetVarname fl), c)
+reBind2 k _ fl = error $ "reBind2: locus/memo mismatch" <> show (("k", k), ("fl", fl))
+
+{-
+genLetAt :: LetInserter code a -> LetInserter code a
+genLetAt = LetInserter $
+ k <- freshKey
+ genLetMemo
+-}
+-- TODO: Here genlet is a version of genlet l em e described earlier, for the case of all memo keys being distinct.
+-- TODO: newtype LocusRec = Locus
+{-
+genLetM = LetInserter $ \loc ->
+ k <- freshKey
+ genLetMemo Nothing k
+-}
+
+-- | Unlike withLocus, we now have to evaluate expressions that
+-- may be present in virtual bindings.
+-- The rule: within an equivalence class, we evaluate only
+-- the bexp of its representative (the first member of the group)
+-- That evaluation may create more virtual bindings, which are to be merged
+
+-- Pick vlbindings for the given locus and convert them to
+
+-- * normal* equivalence classes.
+
+-- Return the list of normal equivalence classes and the
+-- remaining bindings (for different loci).
+-- An equivalence class is called normal if its representative
+-- (the first binding in the group) has the BoundCodeOpenCode as the bound
+-- expression (that is, it is determined which future-stage expression to bind).
+-- If a group is not normal, that is, its representative has a not
+-- yet determined bound expression, we have to determine it --
+-- which creates more bindings to normalize (some of which could be
+-- members of existing groups -- but never replace the existing
+-- representative -- we always preserve the order!)
+--
+-- Keeping the correct order and maintain dependency is actually
+-- very difficult. When evaluating the expression bound to var v,
+-- we obtain a code value with vlbindings. Some of them mention v
+-- (and so should be put into the same group as v, but _after_ it),
+-- some are new and so should be put in a group _before_ v because
+-- the v binding may depend on them.
+-- It seems simpler to just forget about the order between groups
+-- and dependencies and generate one big letrec with mutually dependent clauses.
+
+-- | @('groupBy' eq xs)@: partition a list @xs@
+-- into a list of equivalence classes quotiented by the @eq@ function
+--
+-- The order of the groups follows the order in the input list;
+-- within each group, the elements occur in the same order they
+-- do in the input list.
+groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
+groupBy eq = go []
+ where
+ go acc [] = List.reverse acc
+ go acc (x : xs) = go ((x : grp) : acc) rest
+ where
+ (grp, rest) = List.partition (eq x) xs
+
+normalizeGroup :: Locus -> FloatingLets code -> MT.State Natural ([FloatingLets code], FloatingLets code)
+normalizeGroup lname vl = do
+ let (bindingFLS, passingFLS) = List.partition (\FloatingLet{..} -> floatingLetLocus == Just lname) (unFloatingLets vl)
+ let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
+ -- Try to find an abnormal group
+ let (normalGroups, abnormalGroups) =
+ let abnomality_check = \case
+ FloatingLet{floatingLetBoundCode = BoundCodeLetInserter{}} : _ -> True
+ _ -> False
+ in List.break abnomality_check bindingLFSByMemo
+ -- traceShow (["normalizeGroup"], ("lname",lname), ("bindingLFSByMemo", FloatingLets <$> bindingLFSByMemo), ("normalGroups", FloatingLets <$> normalGroups), ("abnormalGroups", FloatingLets <$> abnormalGroups), ("passingFLS", FloatingLets passingFLS)) $
+ case abnormalGroups of
+ -- all groups are normal
+ [] ->
+ return $
+ traceShow (["normalizeGroup", "return"], ("lname", lname), ("normalGroups", FloatingLets <$> normalGroups), ("passingFLS", passingFLS)) $
+ (FloatingLets <$> normalGroups, FloatingLets passingFLS)
+ -- at least one group representative is abnormal
+ (fl0@FloatingLet{floatingLetBoundCode = BoundCodeLetInserter fl0Exp, floatingLetVarName = fl0VarName} : fls0) : grps -> do
+ fl0BodyCD <- unR fl0Exp
+ -- The group has become normal
+ let normalizedFL0 =
+ FloatingLet
+ { floatingLetLocus = floatingLetLocus fl0
+ , floatingLetMemo = floatingLetMemo fl0
+ , floatingLetVarName = fl0VarName
+ , floatingLetBoundCode = BoundCodeOpenCode (annotatedCodeOpenCode fl0BodyCD)
+ , -- Update the free variables, which could not be done in 'genLetMemoRec'
+ -- where fl0BodyCD was not yet available.
+ floatingLetFreeVars = floatingLetFreeVars fl0 <> annotatedCodeFreeVars fl0BodyCD
+ }
+ : fls0
+ let groups = normalGroups <> (normalizedFL0 : grps)
+ -- New bindings
+ -- let vl' = FloatingLets (List.concat groups) <> FloatingLets passingFLS <> annotatedCodeFloatingLets fl0BodyCD
+ let vl' = FloatingLets $ List.concat groups <> passingFLS <> unFloatingLets (annotatedCodeFloatingLets fl0BodyCD)
+ normalizeGroup lname vl'
+ _ -> error "normalizeGroup: groups are always non-empty"
+
+-- * Class 'MemoGenLetRecable'
+class MemoGenLetRecable sem where
+ withLocusRec :: (Locus -> sem a) -> sem a
+ genLetMemoRec :: Locus -> Memo -> sem a -> sem a
+
+instance
+ Syn.LetRecable Int code =>
+ MemoGenLetRecable (LetInserter code)
+ where
+ withLocusRec body = LetInserter $ do
+ lname <- Locus <$> freshNatural
+ bodyCD <- unR $ body lname
+ (bindingFLS, passingFLS) <-
+ check_no_dup_varname (annotatedCodeFloatingLets bodyCD) $
+ normalizeGroup lname (annotatedCodeFloatingLets bodyCD)
+ -- Bind the variables in order, preserving the dependency
+ return $
+ traceShow (["withLocusRec", "return"], ("lname", lname), ("bindingFLS", bindingFLS), ("passingFLS", passingFLS)) $
+ AnnotatedCode
+ { annotatedCodeOpenCode = bindFloatingLetMemoRec bindingFLS (annotatedCodeOpenCode bodyCD)
+ , annotatedCodeFloatingLets = passingFLS
+ , annotatedCodeFreeVars = annotatedCodeFreeVars bodyCD `Set.difference` foldMap (Set.fromList . (floatingLetVarname <$>) . unFloatingLets) bindingFLS
+ }
+ genLetMemoRec lname key body = LetInserter $ do
+ vname <- freshVar
+ -- Cannot compute all the free variables yet
+ -- because body is not yet evaluated to a 'AnnotatedCode'
+ let fvs = Set.singleton (unVar vname)
+ return $
+ traceShow (["genLetMemoRec"], ("key", key), ("vname", vname)) $
+ AnnotatedCode
+ { annotatedCodeOpenCode = lookupVar vname
+ , annotatedCodeFloatingLets =
+ FloatingLets
+ [ FloatingLet
+ { floatingLetLocus = Just lname
+ , floatingLetMemo = MaybeMemo (Just key)
+ , floatingLetVarName = vname
+ , floatingLetBoundCode = BoundCodeLetInserter body
+ , floatingLetFreeVars = fvs
+ }
+ ]
+ , annotatedCodeFreeVars = fvs
+ }
+
+-- | Create mutually-recursive letrec bindings.
+-- All variables are bound at the same time.
+-- The binding expression is taken from the group representative.
+-- It has to be 'BoundCodeOpenCode': all groups assumed to be normal.
+bindFloatingLetMemoRec ::
+ Syn.LetRecable Int code =>
+ [FloatingLets code] ->
+ OpenCode code a ->
+ OpenCode code a
+bindFloatingLetMemoRec [] c = c
+bindFloatingLetMemoRec bindingFLS c =
+ traceShow (["bindFloatingLetMemoRec", "OpenCode"], ("bindingFLS", bindingFLS)) $
+ OpenCode $ \env ->
+ traceShow (["bindFloatingLetMemoRec", "Syn.letRec"], ("bindingFLS", bindingFLS), ("env", env)) $
+ Syn.letRec
+ len
+ ( \self idx ->
+ traceShow (["bindFloatingLetMemoRec", "Syn.letRec", "binds"], ("idx", idx)) $
+ ( traceShow (["bindFloatingLetMemoRec", "Syn.letRec", "binds", "List.!!"], ("len", len), ("idx", idx), ("env", env)) $
+ unOpenCode (tobindOC List.!! idx)
+ )
+ ( traceShow (["bindFloatingLetMemoRec", "Syn.letRec", "binds", "bind_all"], ("idx", idx), ("env", env)) $
+ bind_all self env
+ )
+ )
+ ( \self ->
+ traceShow (["bindFloatingLetMemoRec", "Syn.letRec", "end"], ("env", env)) $
+ unOpenCode c (bind_all self env)
+ )
+ where
+ len = List.length bindingFLS
+ -- (label,key) of group representative
+ lk (fl@FloatingLet{floatingLetBoundCode = BoundCodeOpenCode{}} : _) = floatingLetMemo fl
+ lk _ = error "groups must be non-empty and canonical"
+ bind_group :: code a -> FloatingLets code -> [EnvBind code]
+ -- Create bindings to bind all identifiers in a group
+ bind_group ec (FloatingLets grp) =
+ traceShow (["bindFloatingLetMemoRec", "bind_group"], ("grp", grp)) $
+ List.map (reBind2 (lk grp) ec) (assertSameLocuses grp)
+ bind_all self env =
+ traceShow (["bindFloatingLetMemoRec", "bind_all"], ("bindingFLS", bindingFLS), ("env", env)) $
+ List.concat $
+ List.zipWith (\grp i -> bind_group (self i) grp) bindingFLS [0 :: Int .. pred len] <> [env]
+ tobindOC =
+ traceShow (["bindFloatingLetMemoRec", "tobindOC"], ("bindingFLS", bindingFLS)) $
+ List.map
+ ( \case
+ -- TODO: avoid unwrapping
+ FloatingLets (fl@FloatingLet{floatingLetBoundCode = BoundCodeOpenCode oc} : _) ->
+ traceShow (["bindFloatingLetMemoRec", "tobindOC", "map"], fl) $
+ unsafeCoerce (oc)
+ _ -> error "tobindOC"
+ )
+ bindingFLS
+
+{-
+genLetLocus :: Syn.Letable code => (Locus -> LetInserter code a) -> LetInserter code a
+genLetLocus body = LetInserter $ do
+ lname <- Locus <$> freshNatural
+ bodyCD <-
+ traceShow ("genLetLocus", ("lname", lname)) $
+ unR (body lname)
+ let (bindingFLS, passingFLS) =
+ List.partition (\fl -> floatingLetLocus fl == Just lname)
+ (unFloatingLets (annotatedCodeFloatingLets bodyCD))
+ -- Bind the variables in order, preserving the dependency
+ --traceShow ("genLetLocus", (bindingFLS, passingFLS)) $
+ return $
+ check_no_dup_varname (annotatedCodeFloatingLets bodyCD) $
+ AnnotatedCode{ annotatedCodeOpenCode = List.foldr bindLet (annotatedCodeOpenCode bodyCD) bindingFLS
+ , annotatedCodeFloatingLets = FloatingLets passingFLS
+ , annotatedCodeFreeVars = annotatedCodeFreeVars bodyCD `Set.difference` Set.fromList (floatingLetVarname <$> bindingFLS)
+ }
+-- In MetaOCaml, let(rec) is actually inserted either at the place
+-- of the explicit let locus,
+-- or at the binding that dominates all free variables of the bound expression,
+-- whichever has the narrowest scope.
+genLetAtMaybe :: Maybe Locus -> LetInserter code a -> LetInserter code a
+genLetAtMaybe mlname body = LetInserter $ do
+ vname <- freshVar
+ bodyCD <-
+ traceShow ("genLet", ("vname", vname)) $
+ unR body
+ -- if the expression to let-bind has itself let-bindings,
+ -- they are straightened out
+ -- The new binding is added at the end; it may depend on
+ -- the bindings coming before (as is the case for the nested genLet)
+ return $
+ traceShow (["genLet", "bodyCD"], ("vname", vname), ("bodyCDFreeVars", (annotatedCodeFreeVars bodyCD))) $
+ AnnotatedCode
+ { annotatedCodeOpenCode = traceShow (["genLet", "lookupVar"], ("vname", vname)) $ lookupVar vname
+ , annotatedCodeFloatingLets = FloatingLets $
+ --(\vls -> traceShow (["genLet", "bindings"], vls) vls) $
+ unFloatingLets (annotatedCodeFloatingLets bodyCD) <>
+ [ FloatingLet
+ { floatingLetLocus = mlname
+ , floatingLetMemo = MaybeMemo (Just 0)
+ , floatingLetVarName = vname
+ , floatingLetBoundCode = BoundCodeOpenCode (annotatedCodeOpenCode bodyCD)
+ , floatingLetFreeVars = Set.insert (unVar vname) (annotatedCodeFreeVars bodyCD)
+ }
+ ]
+ , annotatedCodeFreeVars = Set.insert (unVar vname) $ annotatedCodeFreeVars bodyCD
+ }
+genLetAt :: Locus -> LetInserter code a -> LetInserter code a
+genLetAt = genLetAtMaybe . Just
+
+genLet :: LetInserter code a -> LetInserter code a
+genLet = genLetAtMaybe Nothing
+-}
-- | This module provides the 'Viewer' semantic
-- which interprets combinators as human-readable text.
+-- However there is no wrapping nor indenting.
module Symantic.Semantics.Viewer where
import Data.Function qualified as Fun
+import Data.Int (Int)
+import Data.List qualified as List
import Data.String
import Numeric.Natural (Natural)
-import Prelude qualified
import Text.Show
+import Prelude qualified
import Symantic.Semantics.Data
+import Symantic.Semantics.LetInserter
import Symantic.Semantics.Viewer.Fixity
import Symantic.Syntaxes.Classes
import Symantic.Syntaxes.Derive
ViewerInfix :: Infix -> String -> String -> Viewer (a -> b -> c)
ViewerApp :: Viewer (b -> a) -> Viewer b -> Viewer a
-view :: Viewer a -> ViewerEnv -> ShowS
-view (Viewer v) env = v env
-view (ViewerInfix _op name _infixName) _env = showString name
-view (ViewerUnifix _op name _unifixName) _env = showString name
-view (ViewerApp f x) env =
+view :: Viewer a -> String
+view v =
+ runView
+ v
+ ViewerEnv
+ { viewerEnvOp = (infixN 0, SideL)
+ , viewerEnvPair = pairParen
+ , viewerEnvLamDepth = 1
+ }
+ ""
+
+runView :: Viewer a -> ViewerEnv -> ShowS
+runView (Viewer v) env = v env
+runView (ViewerInfix _op name _infixName) _env = showString name
+runView (ViewerUnifix _op name _unifixName) _env = showString name
+runView (ViewerApp f x) env =
pairViewer env op Fun.$
- view f env{viewerEnvOp = (op, SideL)}
+ runView f env{viewerEnvOp = (op, SideL)}
Fun.. showString " "
- Fun.. view x env{viewerEnvOp = (op, SideR)}
+ Fun.. runView x env{viewerEnvOp = (op, SideR)}
where
- op = infixN 10
+ op = infixL 10
-- | Unusual, but enables to leverage default definition of methods.
type instance Derived Viewer = Viewer
instance IsString (Viewer a) where
fromString s = Viewer Fun.$ \_env -> showString s
instance Show (Viewer a) where
- showsPrec p =
- ( `view`
- ViewerEnv
- { viewerEnvOp = (infixN p, SideL)
- , viewerEnvPair = pairParen
- , viewerEnvLamDepth = 1
- }
- )
+ showsPrec p v =
+ runView
+ v
+ ViewerEnv
+ { viewerEnvOp = (infixN p, SideL)
+ , viewerEnvPair = pairParen
+ , viewerEnvLamDepth = 1
+ }
instance Show (SomeData Viewer a) where
showsPrec p (SomeData x) = showsPrec p (derive x :: Viewer a)
lam f = Viewer Fun.$ \env ->
pairViewer env op Fun.$
let x = showString "x" Fun.. shows (viewerEnvLamDepth env)
- in showString "\\"
- Fun.. x
- Fun.. showString " -> "
- Fun.. view
- (f (Viewer (\_env -> x)))
- env
- { viewerEnvOp = (op, SideL)
- , viewerEnvLamDepth = Prelude.succ (viewerEnvLamDepth env)
- }
+ in showString "\\"
+ Fun.. x
+ Fun.. showString " -> "
+ Fun.. runView
+ (f (Viewer (\_env -> x)))
+ env
+ { viewerEnvOp = (op, SideL)
+ , viewerEnvLamDepth = Prelude.succ (viewerEnvLamDepth env)
+ }
where
- op = infixN 0
+ op = infixL 1
+instance Letable Viewer where
+ let_ x f = Viewer Fun.$ \env ->
+ pairViewer env op Fun.$
+ let l = showString "x" Fun.. shows (viewerEnvLamDepth env)
+ in showString "let "
+ Fun.. l
+ Fun.. showString " = "
+ Fun.. runView
+ x
+ env
+ { viewerEnvOp = (infixN 0, SideL)
+ , viewerEnvLamDepth = Prelude.succ (viewerEnvLamDepth env)
+ }
+ Fun.. showString " in "
+ Fun.. runView
+ (f (Viewer (\_env -> l)))
+ env
+ { viewerEnvOp = (infixN 0, SideL)
+ , viewerEnvLamDepth = Prelude.succ (viewerEnvLamDepth env)
+ }
+ where
+ op = infixL 1
+instance LetRecable Int Viewer where
+ letRec len f body = Viewer Fun.$ \env ->
+ let fns =
+ [ showString "u" Fun.. shows (viewerEnvLamDepth env Prelude.+ Prelude.fromIntegral idx)
+ | idx <- [0 .. len Prelude.- 1]
+ ]
+ in let self idx = Viewer Fun.$ \_env -> fns List.!! idx
+ in let lvs = List.zipWith (\v idx -> (v, f self idx)) fns [0 .. len Prelude.- 1]
+ in pairViewer env op Fun.$
+ showString "letRec "
+ Fun.. showListWith
+ ( \(lhs, rhs) ->
+ lhs
+ Fun.. showString " = "
+ Fun.. runView
+ rhs
+ env
+ { viewerEnvOp = (infixN 0, SideL)
+ , viewerEnvLamDepth = Prelude.succ (viewerEnvLamDepth env)
+ }
+ )
+ lvs
+ Fun.. showString " in "
+ Fun.. runView
+ (body self)
+ env
+ { viewerEnvOp = (infixN 0, SideL)
+ , viewerEnvLamDepth = viewerEnvLamDepth env Prelude.+ Prelude.fromIntegral len
+ }
+ where
+ op = infixN 10
instance Abstractable1 Viewer where
lam1 f = Viewer Fun.$ \env ->
pairViewer env op Fun.$
let x = showString "u" Fun.. shows (viewerEnvLamDepth env)
- in showString "\\"
- Fun.. x
- Fun.. showString " -> "
- Fun.. view
- (f (Viewer (\_env -> x)))
- env
- { viewerEnvOp = (op, SideL)
- , viewerEnvLamDepth = Prelude.succ (viewerEnvLamDepth env)
- }
+ in showString "\\"
+ Fun.. x
+ Fun.. showString " -> "
+ Fun.. runView
+ (f (Viewer (\_env -> x)))
+ env
+ { viewerEnvOp = (op, SideL)
+ , viewerEnvLamDepth = Prelude.succ (viewerEnvLamDepth env)
+ }
where
op = infixN 0
instance Instantiable Viewer where
- ViewerInfix op _name infixName .@ ViewerApp x y = Viewer Fun.$ \env ->
+ ViewerApp (ViewerInfix op _name infixName) x .@ y = Viewer Fun.$ \env ->
pairViewer env op Fun.$
- view x env{viewerEnvOp = (op, SideL)}
+ runView x env{viewerEnvOp = (op, SideL)}
Fun.. showString " "
Fun.. showString infixName
Fun.. showString " "
- Fun.. view y env{viewerEnvOp = (op, SideR)}
- ViewerInfix op name _infixName .@ x = Viewer Fun.$ \env ->
- showParen Prelude.True Fun.$
- view x env{viewerEnvOp = (op, SideL)}
- Fun.. showString " "
- Fun.. showString name
+ Fun.. runView y env{viewerEnvOp = (op, SideR)}
f .@ x = ViewerApp f x
instance Unabstractable Viewer where
ap = ViewerInfix (infixL 4) "(<*>)" "<*>"
instance IfThenElseable Viewer where
ifThenElse test ok ko = Viewer Fun.$ \env ->
pairViewer env op Fun.$
- showString "if"
- Fun.. view test env{viewerEnvOp = (op, SideL)}
- Fun.. showString "then"
- Fun.. view ok env{viewerEnvOp = (op, SideL)}
- Fun.. showString "else"
- Fun.. view ko env{viewerEnvOp = (op, SideL)}
+ showString "if "
+ Fun.. runView test env{viewerEnvOp = (op, SideL)}
+ Fun.. showString " then "
+ Fun.. runView ok env{viewerEnvOp = (op, SideL)}
+ Fun.. showString " else "
+ Fun.. runView ko env{viewerEnvOp = (op, SideL)}
where
- op = infixN 0
+ op = infixN 1
+
+{-
+instance MemoGenLetRecable Viewer where
+ group_normalize :: Locus -> Locus -> VLBindings sem -> ([VLBindings sem], VLBindings sem)
+ memoGenLetRecLocus :: (Locus -> sem a) -> sem a
+ memoGenLetRecLocus f = f
+ memoGenLetRec :: Locus -> MemoKey sem -> sem a -> sem a
+-}
(sem a -> sem b) ->
sem (a -> b)
+-- ** Class Letable'
+class Letable sem where
+ let_ :: sem a -> (sem a -> sem b) -> sem b
+ let_ e b = liftDerived (let_ (derive e) (derive Fun.. b Fun.. liftDerived))
+ default let_ ::
+ FromDerived Letable sem =>
+ Derivable sem =>
+ sem a ->
+ (sem a -> sem b) ->
+ sem b
+
+-- *** Class 'LetRecable'
+class LetRecable idx sem where
+ letRec ::
+ idx ->
+ ({-self-} (idx -> sem a) -> idx -> sem a) ->
+ ({-self-} (idx -> sem a) -> sem w) ->
+ sem w
+ default letRec ::
+ FromDerived (LetRecable idx) sem =>
+ Derivable sem =>
+ idx ->
+ ({-self-} (idx -> sem a) -> idx -> sem a) ->
+ ({-self-} (idx -> sem a) -> sem w) ->
+ sem w
+ letRec idx f body =
+ liftDerived Fun.$
+ letRec
+ idx
+ (\self i -> derive (f (liftDerived Fun.. self) i))
+ (\self -> derive (body (liftDerived Fun.. self)))
+
-- ** Class 'Abstractable1'
class Abstractable1 sem where
-- | Like 'lam' but whose argument must be used only once,
sem b
-- ** Class 'Unabstractable'
+
-- | All operations in lambda calculus can be encoded
-- via abstraction elimination into the SK calculus
-- as binary trees whose leaves are one
--- of the three symbols S ('ap') and K ('const').
+-- of the two symbols S ('ap') and K ('const').
class Unabstractable sem where
-- | S
ap :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
+
-- | K
const :: sem (a -> b -> a)
+
-- | I
id :: sem (a -> a)
+
-- | B
(.) :: sem ((b -> c) -> (a -> b) -> a -> c)
+
infixr 9 .
+
-- | C
flip :: sem ((a -> b -> c) -> b -> a -> c)
+
($) :: sem ((a -> b) -> a -> b)
infixr 0 $
c ->
sem c
+bool :: Constantable Bool sem => Bool -> sem Bool
+bool = constant
+char :: Constantable Char sem => Char -> sem Char
+char = constant
+int :: Constantable Int sem => Int -> sem Int
+int = constant
+natural :: Constantable Natural sem => Natural -> sem Natural
+natural = constant
+string :: Constantable String sem => String -> sem String
+string = constant
+unit :: Constantable () sem => sem ()
+unit = constant ()
+
-- * Class 'Eitherable'
class Eitherable sem where
either :: sem ((l -> a) -> (r -> a) -> Either l r -> a)
default infer :: FromDerived (Inferable a) sem => sem a
infer = liftDerived infer
-unit :: Inferable () sem => sem ()
-unit = infer
-bool :: Inferable Bool sem => sem Bool
-bool = infer
-char :: Inferable Char sem => sem Char
-char = infer
-int :: Inferable Int sem => sem Int
-int = infer
-natural :: Inferable Natural sem => sem Natural
-natural = infer
-string :: Inferable String sem => sem String
-string = infer
-
-- * Class 'Listable'
class Listable sem where
cons :: sem (a -> [a] -> [a])
EoTOfRep a =>
CurryN args =>
Tuples args ~ EoT (ADT a) =>
- (args ~ Args (args -..-> a)) =>
+ args ~ Args (args -..-> a) =>
(args -..-> a) ->
sem (Tuples args) ->
sem a
license: AGPL-3.0-or-later
license-file: LICENSES/AGPL-3.0-or-later.txt
--- PVP: +-+------- breaking API changes
--- | | +----- non-breaking API additions
--- | | | +--- code changes with no API change
-version: 0.5.0.20221211
+-- PVP: +-+------- breaking API changes
+-- | | +----- non-breaking API additions
+-- | | | +--- code changes with no API change
+version: 0.5.1.20240520
stability: experimental
category: Data Structures
synopsis:
extra-source-files:
.envrc
cabal.project
- flake.lock
- flake.nix
- Makefile
extra-tmp-files:
type: git
location: git://git.sourcephile.fr/haskell/symantic-base
-library
- hs-source-dirs: src
- exposed-modules:
- Symantic
- Symantic.Semantics
- Symantic.Semantics.Data
- Symantic.Semantics.Forall
- Symantic.Semantics.Identity
- Symantic.Semantics.Reader
- Symantic.Semantics.SharingObserver
- Symantic.Semantics.Viewer
- Symantic.Semantics.Viewer.Fixity
- Symantic.Syntaxes
- Symantic.Syntaxes.Classes
- Symantic.Syntaxes.CurryN
- Symantic.Syntaxes.Derive
- Symantic.Syntaxes.EithersOfTuples
- Symantic.Syntaxes.Reify
- Symantic.Syntaxes.TuplesOfFunctions
-
+common boilerplate
default-language: Haskell2010
default-extensions:
- NoImplicitPrelude
DefaultSignatures
FlexibleContexts
FlexibleInstances
LambdaCase
MultiParamTypeClasses
NamedFieldPuns
+ NoImplicitPrelude
RecordWildCards
ScopedTypeVariables
TupleSections
-Wall -Wincomplete-uni-patterns -Wincomplete-record-updates
-Wpartial-fields -fprint-potential-instances
+common library-deps
build-depends:
, base >=4.10 && <5
, containers
, template-haskell
, transformers
, unordered-containers
+
+library
+ import: boilerplate, library-deps
+ hs-source-dirs: src
+ exposed-modules:
+ Symantic
+ Symantic.Semantics
+ Symantic.Semantics.Data
+ Symantic.Semantics.Forall
+ Symantic.Semantics.Identity
+ Symantic.Semantics.LetInserter
+ Symantic.Semantics.Reader
+ Symantic.Semantics.SharingObserver
+ Symantic.Semantics.Viewer
+ Symantic.Semantics.Viewer.Fixity
+ Symantic.Syntaxes
+ Symantic.Syntaxes.Classes
+ Symantic.Syntaxes.CurryN
+ Symantic.Syntaxes.Derive
+ Symantic.Syntaxes.EithersOfTuples
+ Symantic.Syntaxes.Reify
+ Symantic.Syntaxes.TuplesOfFunctions
+
+test-suite symantic-base-tests
+ import: boilerplate, library-deps
+ type: exitcode-stdio-1.0
+ hs-source-dirs: tests
+ main-is: Spec.hs
+ build-tool-depends: sydtest-discover:sydtest-discover
+ ghc-options: -threaded -rtsopts -with-rtsopts=-N
+
+ -- ghc-prof-options: -fexternal-interpreter
+ -- ghc-options: -ddump-splices -ddump-to-file
+ other-modules:
+ Paths_symantic_base
+ Symantic.Semantics.LetInserterSpec
+ Symantic.Syntaxes.Extras
+
+ autogen-modules: Paths_symantic_base
+ build-depends:
+ , genvalidity
+ , genvalidity-containers
+ , genvalidity-sydtest
+ , genvalidity-text
+ , genvalidity-time
+ , relude
+ , sydtest
+ , symantic-base
+ , validity
+ , validity-containers
+ , validity-text
--- /dev/null
+{-# OPTIONS_GHC -F -pgmF sydtest-discover #-}
--- /dev/null
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE TemplateHaskellQuotes #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module Symantic.Semantics.LetInserterSpec where
+
+import Data.Function (($), (.))
+import Data.Functor.Identity (Identity (..))
+import Data.Int (Int)
+import Data.Maybe (Maybe (..))
+import Data.Semigroup (Semigroup (..))
+import Debug.Trace (trace)
+import Language.Haskell.TH.Syntax qualified as TH
+import Symantic.Semantics.LetInserter
+import Symantic.Semantics.Viewer
+import Symantic.Syntaxes.Classes (Abstractable (..), Constantable, Equalable (..), IfThenElseable (..), Instantiable (..), LetRecable (..), Letable (..), int, unit, (==))
+import Test.Syd
+import Test.Syd.Validity
+import Text.Show (show)
+import Prelude qualified as P
+
+import Symantic.Syntaxes.Extras
+
+-- import Debug.Trace (traceShow)
+
+p12 ::
+ Addable sem =>
+ Instantiable sem =>
+ Constantable Int sem =>
+ sem Int
+p12 = int 1 + int 2
+
+{-
+t1 ::
+ Abstractable sem =>
+ Instantiable sem =>
+ Multiplicable sem =>
+ Addable sem =>
+ Constantable Int sem =>
+ --GHC.Num.Num (sem Int) =>
+ sem Int -> sem Int
+-}
+t1 = (\x -> x * (x + int 1))
+c1 = t1 p12
+
+t2 x = let_ x (\y -> y * (y + int 1))
+c2 = t2 p12
+ft1 t x = lam (\u -> t x + t (x + u))
+c3 = ft1 t2 p12
+
+p12l loc = genLetAt loc (int 1 + int 2)
+c1l = withLocus \loc -> p12l loc
+
+ft11 loc = \t -> \x -> lam (\u -> t x + t (genLetAt loc (x + u)))
+c3l1 = withLocus \loc -> ft11 loc t1 (p12l loc)
+
+ft12 = \t -> \x -> lam (\u -> withLocus \loc -> t x + t (genLetAt loc (x + u)))
+c3l2 = withLocus \loc -> ft12 t1 (p12l loc)
+
+r12 :: Int
+r12 = runIdentity (runLetInserter p12)
+runLII = runIdentity . runLetInserter
+
+{-
+-- letrec (fun self m -> lam @@ fun n ->
+-- if_ (m =. int 0) (n + (int 1)) @@
+-- if_ (n =. int 0) (self / (m - int 1) / int 1) @@
+-- self / (m - int 1) / (self / m / (n - int 1))
+-- ) @@ fun ack -> ack / int 2
+fib =
+ letR
+ (\self ->
+ \n ->
+ ifThenElse (n == int 0) (log "n==0" (int 1)) $
+ ifThenElse (n == int 1) (log "n==1" (int 2)) $
+ self .@ int 2
+ )
+ (\res -> res)
+let sac2 = sack 2
+;;
+ack2 =
+ letR
+ (\self -> \m ->
+ lam $ \n ->
+ ifThenElse (m == int 0) (n + int 1) $
+ ifThenElse (n == int 0) (self .@ (m - int 1) .@ int 1) $
+ self .@ (m - int 1) .@ (self .@ m .@ (n - int 1))
+ )
+ (\res -> res .@ int 2)
+
+let fibonacci n =
+ let rec loop n (x,y) =·
+ if n = 0 then x else if n = 1 then y else·
+ .< .~(loop (n-1) (x,y)) + .~(loop (n-2) (x,y)) >.
+ in .< fun x y -> .~(loop n (.< x >. , .< y >.)) >.
+
+-}
+
+-- derive
+quote :: LetInserter (AnnotatedCode code) a -> LetInserter (AnnotatedCode code) a
+-- quote :: sem a -> a
+quote = P.id
+
+-- liftDerived
+unquote :: a -> sem a
+unquote = P.undefined
+
+-- unQ ::
+
+{-
+fibonacci ::
+ ( P.Eq (sem Int)
+ , P.Num (sem Int)
+ , Substractable sem
+ , Instantiable sem
+ ) =>
+ sem Int -> sem2 Int -> sem3 Int
+fibonacci ::
+ ( Addable code
+ , Abstractable (LetInserter (AnnotatedCode code))
+ , Instantiable code
+ ) => Int -> LetInserter (AnnotatedCode code) (Int -> Int -> Int)
+fibonacci m =
+ let loop n (x,y) =
+ if n P.== 0 then x else
+ if n P.== 1 then y else
+ quote (loop (n P.-1) (x, y) + loop (n P.-2) (x, y))
+ in quote (lam $ \x -> lam $ \y -> loop m (x, y))
+-}
+
+{-
+(* Specialized to m. Without memoization, it diverges *)
+let sack m =
+ with_locus_rec @@ fun l ->
+ let g = mkgenlet l (=) in
+ let rec loop m =
+ if m = 0 then .<fun n -> n + 1>. else
+ .<fun n -> if n = 0 then .~(g loop (m-1)) 1
+ else .~(g loop (m-1)) (.~(g loop m) (n-1))>.
+ in g loop m
+;;
+-}
+-- https://en.wikipedia.org/wiki/Ackermann_function
+-- Specialized to m. Without memoization, it diverges
+sack ::
+ Abstractable code =>
+ Addable code =>
+ Constantable Int code =>
+ Equalable code =>
+ IfThenElseable code =>
+ Instantiable code =>
+ LetRecable Int code =>
+ Letable code =>
+ Substractable code =>
+ Int ->
+ LetInserter code (Int -> Int)
+sack m0 =
+ withLocusRec $ \l ->
+ let
+ memoLoop k = genLetMemoRec l (P.fromIntegral k) (loop k)
+ loop 0 =
+ traceShow (["sack", "loop"], ("m", 0 :: Int)) $
+ lam $
+ \n -> n + int 1
+ loop m =
+ traceShow (["sack", "loop"], ("m", m)) $
+ lam $ \n ->
+ ifThenElse
+ (n == int 0)
+ (memoLoop (m P.- 1) .@ int 1)
+ (memoLoop (m P.- 1) .@ (memoLoop m .@ (n - int 1)))
+ in
+ memoLoop m0
+
+-- https://simple.wikipedia.org/wiki/Fibonacci_number
+fibonacci ::
+ Addable code =>
+ Abstractable code =>
+ Letable code =>
+ Instantiable code =>
+ LetRecable Int code =>
+ Int ->
+ LetInserter code (Int -> Int -> Int)
+fibonacci m =
+ withLocusRec $ \loc ->
+ let
+ memoLoop k = genLetMemoRec loc (P.fromIntegral k) (loop k)
+ loop n =
+ if n P.== 0
+ then lam $ \x -> lam $ \_y -> x
+ else
+ if n P.== 1
+ then lam $ \_x -> lam $ \y -> y
+ else lam $ \x -> lam $ \y ->
+ add
+ .@ (memoLoop (n P.- 1) .@ x .@ y)
+ .@ (memoLoop (n P.- 2) .@ x .@ y)
+ in
+ loop m
+
+-- (int -> int -> int) code =
+-- .< fun x_1 -> fun y_2 -> (((y_2 + x_1) + y_2) + (y_2 + x_1)) + ((y_2 + x_1) + y_2)>.
+tfib :: TH.Quote m => Int -> TH.Code m (Int -> Int -> Int)
+tfib m =
+ let loop n (x, y) =
+ if n P.== 0
+ then x
+ else
+ if n P.== 1
+ then y
+ else [||$$(loop (n P.- 1) (x, y)) P.+ $$(loop (n P.- 2) (x, y))||]
+ in [||\x y -> $$(loop m ([||x||], [||y||]))||]
+
+{-
+acs :: Int -> LetInserter (AnnotatedCode Viewer) (Int -> Int)
+acs m =
+ withLocusRec $ \l ->
+ letR
+ (\self -> --lam $ \mm ->
+ lam $ \n ->
+ --if (runIdentity m P.== 0) then (n + int 1) else
+ ifThenElse (n == int 0) n $
+ --genLetMemoRec l m
+ (self .@ int m) .@ (n - int 1)
+ --ifThenElse (m == int 0) (n + int 1) $
+ --ifThenElse (n == int 0) (self .@ (m - int 1) .@ int 1) $
+ --genLetMemo l m $ self .@ (m - int 1) .@ (self .@ m .@ (n - int 1))
+ )
+ (\self -> genLetMemoRec l (2) (self .@ int 2))
+-}
+ack :: Int -> Int -> Int
+ack 0 n = trace ("ack 0 " <> show n) $ n P.+ 1
+ack m 0 = trace ("ack " <> show m <> " 0") $ ack (m P.- 1) 1
+ack m n = trace ("ack " <> show n <> " " <> show m) $ ack (m P.- 1) (ack m (n P.- 1))
+
+spec :: Spec
+spec = do
+ describe "let_" do
+ it "can bind a literal" do
+ view (runLetInserter (let_ (int 3) (\v -> int 4 + v)))
+ `shouldBe` "let x1 = 3 in 4 + x1"
+ it "can bind an expression of literals" do
+ view (runLetInserter (let_ (int 1 + int 2) (\v -> int 4 + v)))
+ `shouldBe` "let x1 = 1 + 2 in 4 + x1"
+ it "can bind a variable" do
+ view (runLetInserter (lam (\x -> let_ x (\v -> int 4 + v))))
+ `shouldBe` "\\x1 -> let x2 = x1 in 4 + x2"
+ it "can bind an expression with a variable" do
+ view (runLetInserter (lam (\x -> let_ (x + int 1) (\v -> int 4 + v))))
+ `shouldBe` "\\x1 -> let x2 = x1 + 1 in 4 + x2"
+ describe "genLet" do
+ it "can bind" do
+ let exp = int 1 + genLet (int 2)
+ view (runLetInserter exp) `shouldBe` "let x1 = 2 in 1 + x1"
+ runIdentity (runLetInserter exp) `shouldBe` 3
+ it "can bind a literal across a lambda" do
+ let exp = lam (\x -> x + genLet (int 2))
+ view (runLetInserter exp) `shouldBe` "let x1 = 2 in \\x2 -> x2 + x1"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 3
+ it "can bind an operation across a lambda" do
+ let exp = lam (\x -> x + genLet (int 1 + int 2))
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in \\x2 -> x2 + x1"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 4
+ it "can wrap a variable" do
+ let exp = lam (\x -> withLocus (\l -> x + genLetAt l x))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 in x1 + x2"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 2
+ -- This must not raise a lookupVar failure for var=([1]) env=[]
+ it "cannot cause a scope extrusion using withLocus" do
+ view (runLetInserter (withLocus (\l -> lam (\x -> x + genLetAt l x))))
+ `shouldBe` "\\x1 -> let x2 = x1 in x1 + x2"
+ -- Check that 'lam' limits the scope extrusion:
+ -- as soon as that passing a virtual binding would
+ -- make a variable extrude its scope, this virtual binding is bound.
+ it "has its locus limited by lam when wrapping its variable" do
+ let exp = lam (\x -> x + genLet x)
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 in x1 + x2"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 2
+ it "does not have its locus limited by lam when not wrapping its variable" do
+ let exp = lam (\x -> x + genLet (int 1))
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 in \\x2 -> x2 + x1"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 2
+ it "can wrap let_" do
+ let exp = lam (\x -> x + genLet (let_ (int 1) (\y -> y)))
+ view (runLetInserter exp) `shouldBe` "let x1 = let x2 = 1 in x2 in \\x2 -> x2 + x1"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 2
+ it "can have its locus limited by withLocus" do
+ let exp = lam (\x -> withLocus (\l -> x + genLetAt l (let_ (int 1) (\y -> y))))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = let x3 = 1 in x3 in x1 + x2"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 2
+ it "can wrap lam and a variable" do
+ let exp = lam (\x -> x + genLet (lam (\_y -> x)) .@ unit)
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = \\x3 -> x1 in x1 + x2 ()"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 2
+ it "can wrap lam and be called" do
+ let exp = lam (\x -> x + genLet (lam (\y -> y + int 2)) .@ x)
+ view (runLetInserter exp) `shouldBe` "let x1 = \\x2 -> x2 + 2 in \\x2 -> x2 + x1 x2"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 4
+ it "can wrap a variable in an operation" do
+ let exp = lam (\x -> x + genLet (x + int 1))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 + 1 in x1 + x2"
+ runIdentity (runLetInserter exp) 1 `shouldBe` 3
+ it "can wrap literals inside an expression with two variables" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (int 2 + int 3)))
+ view (runLetInserter exp) `shouldBe` "let x1 = 2 + 3 in \\x2 -> \\x3 -> x2 + x3 + x1"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 10
+ it "can wrap the farthest variable inside two lam" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet x))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 in \\x3 -> x1 + x3 + x2"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 6
+ it "can wrap another variable inside two lam" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet y))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 in x1 + x2 + x3"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 9
+ it "can wrap another variable inside two lam" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet y))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 in x1 + x2 + x3"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 9
+ it "can wrap the farthest variable in an expression inside two lam" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (x + int 1)))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 + 1 in \\x3 -> x1 + x3 + x2"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 7
+ it "can wrap the closest variable in an expression inside two lam" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (y + int 1)))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 + 1 in x1 + x2 + x3"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 10
+ it "can wrap both variables in an expression inside two lam" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (y + int 1 + x)))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 + 1 + x1 in x1 + x2 + x3"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 11
+ it "can be nested" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (genLet (y + int 1 + x))))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 + 1 + x1 in let x4 = x3 in x1 + x2 + x4"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 11
+ it "can be nested within an expression of literals" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (y + genLet (int 1 + int 2))))
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in \\x2 -> \\x3 -> let x4 = x3 + x1 in x2 + x3 + x4"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 12
+ it "can be nested within an expression with a variable" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (y + genLet (int 1 + x))))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = 1 + x1 in \\x3 -> let x4 = x3 + x2 in x1 + x3 + x4"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 11
+ it "can be nested within an expression with two variables" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (y + genLet (int 1 + x + y))))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = 1 + x1 + x2 in let x4 = x2 + x3 in x1 + x2 + x4"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 15
+ it "can be nested within another expression with two variables" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (x + genLet (int 1 + x + y))))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = 1 + x1 + x2 in let x4 = x1 + x3 in x1 + x2 + x4"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 12
+ it "can be nested within an expression of literals and one variable" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (int 1 + genLet (int 1 + x + int 2))))
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = 1 + x1 + 2 in let x3 = 1 + x2 in \\x4 -> x1 + x4 + x3"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 10
+ it "can be nested within an expression of literals" do
+ let exp = lam (\x -> lam (\y -> x + y + genLet (int 1 + genLet (int 1 + int 2 + int 3))))
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 + 3 in let x2 = 1 + x1 in \\x3 -> \\x4 -> x3 + x4 + x2"
+ runIdentity (runLetInserter exp) 1 4 `shouldBe` 12
+ it "duplicates literals when used with host-let" do
+ let exp = let x = genLet (int 1 + int 2) in x + x
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + 2 in x1 + x2"
+ runIdentity (runLetInserter exp) `shouldBe` 6
+ it "duplicates literals when using host-let and no specific memo key" do
+ let exp =
+ let x = genLet (int 1 + int 2)
+ in let y = genLet (int 1 + x)
+ in x + y
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + 2 in let x3 = 1 + x2 in x1 + x3"
+ runIdentity (runLetInserter exp) `shouldBe` 7
+ it "does not duplicate host-let when using a specific memo key" do
+ let exp =
+ let x = genLetMemoAtMaybe (Just 0) Nothing (int 1 + int 2)
+ in let y = genLet (int 1 + x)
+ in x + y
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + x1 in x1 + x2"
+ runIdentity (runLetInserter exp) `shouldBe` 7
+ it "does not duplicate host-lets when using specific memo keys" do
+ let exp =
+ let x = genLetMemoAtMaybe (Just 0) Nothing (int 1 + int 2)
+ in let y = genLetMemoAtMaybe (Just 1) Nothing (int 1 + x)
+ in let z = genLet (int 1 + y)
+ in x + z + y
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + x1 in let x3 = 1 + x2 in x1 + x3 + x2"
+ runIdentity (runLetInserter exp) `shouldBe` 12
+ it "does not duplicate host-let when using a specific memo key, inside a lam" do
+ let exp =
+ lam $ \u ->
+ let x = genLetMemoAtMaybe (Just 0) Nothing (int 1 + int 2)
+ in let y = genLet (u + x)
+ in x + y
+ view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in \\x2 -> let x3 = x2 + x1 in x1 + x3"
+ runIdentity (runLetInserter exp) 2 `shouldBe` 8
+ it "does not duplicate host-let when using a specific memo key, inside a lam and using its variable" do
+ let exp =
+ lam $ \u ->
+ let x = genLetMemoAtMaybe (Just 0) Nothing (u + int 2)
+ in let y = genLet (int 1 + x)
+ in x + y
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 + 2 in let x3 = 1 + x2 in x2 + x3"
+ runIdentity (runLetInserter exp) 2 `shouldBe` 9
+ it "does not duplicate host-lets when using specific memo keys, inside a lam and using its variable" do
+ let exp =
+ lam $ \u ->
+ let x = genLetMemoAtMaybe (Just 0) Nothing (u + int 2)
+ in let y = genLetMemoAtMaybe (Just 1) Nothing (int 1 + x)
+ in let z = genLetMemoAtMaybe (Just 2) Nothing (int 1 + y)
+ in x + z + y + z
+ view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 + 2 in let x3 = 1 + x2 in let x4 = 1 + x3 in x2 + x4 + x3 + x4"
+ runIdentity (runLetInserter exp) 2 `shouldBe` 21
+ describe "Ex0" do
+ it "p12" do
+ runLII p12 `shouldBe` 3
+ it "p12" do
+ view (runLetInserter p12)
+ `shouldBe` "1 + 2"
+ it "c1" do
+ view (runLetInserter c1)
+ `shouldBe` "(1 + 2) * (1 + 2 + 1)"
+ it "c2" do
+ view (runLetInserter c2)
+ `shouldBe` "let x1 = 1 + 2 in x1 * (x1 + 1)"
+ it "c3" do
+ view (runLetInserter c3)
+ `shouldBe` "\\x1 -> (let x2 = 1 + 2 in x2 * (x2 + 1)) + (let x2 = 1 + 2 + x1 in x2 * (x2 + 1))"
+ describe "Ex1" do
+ it "c1l" do
+ view (runLetInserter c1l)
+ `shouldBe` "let x1 = 1 + 2 in x1"
+ -- , it "c3l1" do -- expected scope extrusion
+ -- view (runLetInserter c3l1) `shouldBe` ""
+ it "c3l2" do
+ -- serious duplication
+ view (runLetInserter c3l2)
+ `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + 2 in let x3 = 1 + 2 in let x4 = 1 + 2 in \\x5 -> let x6 = x3 + x5 in let x7 = x4 + x5 in x1 * (x2 + 1) + x6 * (x7 + 1)"
+ it "let x1 = 1 in let x2 = 2 in x1 + x2" do
+ let exp = withLocus $ \loc -> genLetAt loc (int 1) + genLetAt loc (int 2)
+ view (runLetInserter exp)
+ `shouldBe` "let x1 = 1 in let x2 = 2 in x1 + x2"
+ it "let_ (genLetAt loc (int 1 + int 2)) (\\x -> x + x)" do
+ let exp = withLocus $ \loc ->
+ let_ (genLetAt loc (int 1 + int 2)) $ \x ->
+ x + x
+ view (runLetInserter exp)
+ `shouldBe` "let x1 = 1 + 2 in let x2 = x1 in x2 + x2"
+ it "withLocus does not cause a scope extrusion" do
+ let exp = withLocus $ \loc1 ->
+ withLocus $ \loc2 ->
+ genLetAt
+ loc1 -- expected scope extrusion if it's not bound at loc2 instead of loc1
+ (int 1 + genLetAt loc2 (int 2))
+ * int 3
+ view (runLetInserter exp)
+ `shouldBe` "let x1 = 2 in let x2 = 1 + x1 in x2 * 3"
+ it "let x1 = 1 + 2 in let x2 = 1 + 2 in let x3 = 1 + x2 in x1 + x3" do
+ let exp = withLocus $ \loc ->
+ let x = (genLetAt loc (int 1 + int 2))
+ in let y = (genLetAt loc (int 1 + x))
+ in x + y
+ view (runLetInserter exp)
+ `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + 2 in let x3 = 1 + x2 in x1 + x3"
+ -- , it "let x1 = 1 + 2 in let x2 = 1 + x1 in x1 + x2" do
+ -- let exp = withLocus $ \loc ->
+ -- let__ (genLetAt loc (int 1 + int 2)) $ \x ->
+ -- let__ (genLetAt loc (int 1 + x)) $ \y ->
+ -- x + y
+ -- view (runLetInserter exp) `shouldBe`
+ -- "let x1 = 1 + 2 in let x2 = 1 + x1 in x1 + x2"
+ it "let x1 = 1 + 2 in let x2 = x1 in let x3 = 1 + x2 in let x4 = x3 in x2 + x4" do
+ let exp = withLocus $ \loc ->
+ let_ (genLetAt loc (int 1 + int 2)) $ \x ->
+ withLocus $ \locX ->
+ let_ (genLetAt locX (int 1 + x)) $ \y ->
+ x + y
+ view (runLetInserter exp)
+ `shouldBe` "let x1 = 1 + 2 in let x2 = x1 in let x3 = 1 + x2 in let x4 = x3 in x2 + x4"
+ describe "Fibonacci" do
+ it "fib 2" do
+ view (runLetInserter (fibonacci 2))
+ `shouldBe` "letRec [u1 = \\x2 -> \\x3 -> x3,u2 = \\x2 -> \\x3 -> x2] in \\x3 -> \\x4 -> u1 x3 x4 + u2 x3 x4"
+ it "fib 5" do
+ view (runLetInserter (fibonacci 5))
+ `shouldBe` "letRec [u1 = \\x2 -> \\x3 -> u2 x2 x3 + u3 x2 x3,u2 = \\x2 -> \\x3 -> u3 x2 x3 + u4 x2 x3,u3 = \\x2 -> \\x3 -> u4 x2 x3 + u5 x2 x3,u4 = \\x2 -> \\x3 -> x3,u5 = \\x2 -> \\x3 -> x2] in \\x6 -> \\x7 -> u1 x6 x7 + u2 x6 x7"
+ it "fib 2" do
+ runIdentity (runLetInserter (fibonacci 2)) 0 1 `shouldBe` 1
+ it "fib 5" do
+ runIdentity (runLetInserter (fibonacci 5)) 0 1 `shouldBe` 5
+ it "fib 10" do
+ runIdentity (runLetInserter (fibonacci 10)) 0 1 `shouldBe` 55
+ describe "Ackermann" do
+ it "sack 2 3" do
+ view (runLetInserter (sack 2))
+ `shouldBe` "letRec [u1 = \\x2 -> if x2 == 0 then u2 1 else u2 (u1 (x2 - 1)),u2 = \\x2 -> if x2 == 0 then u3 1 else u3 (u2 (x2 - 1)),u3 = \\x2 -> x2 + 1] in u1"
+ it "sack 2 3" do
+ runLII (sack 2) 3 `shouldBe` 9
+ it "sack 3 4" do
+ runLII (sack 3) 4 `shouldBe` 125
+
+-- {-
+-- it "fib 0" do
+-- runLII (fib .@ int 0) `shouldBe` 1
+-- , it "fib 1" do
+-- runLII (fib .@ int 1) `shouldBe` 2
+-- , it "fib 2" do
+-- runLII (fib .@ int 2) `shouldBe` 42
+-- it "fib 1" do
+-- runIdentity (fib .@ int 1) `shouldBe` 2
+-- , it "sack 3" do
+-- runIdentity (sack .@ int 3) `shouldBe` 9
+-- , it "acs" do
+-- view (runLetInserter acs) `shouldBe` ""
+-- -}
--- /dev/null
+{-# LANGUAGE UndecidableInstances #-}
+
+module Symantic.Syntaxes.Extras where
+
+import Data.Function qualified as Fun
+import Data.Int (Int)
+import Debug.Trace (trace)
+import Symantic.Semantics.Identity
+import Symantic.Semantics.LetInserter
+import Symantic.Semantics.Viewer
+import Symantic.Semantics.Viewer.Fixity
+import Symantic.Syntaxes.Classes (Abstractable (..), Instantiable (..))
+import Symantic.Syntaxes.Derive
+import Text.Show (show, showString)
+import Prelude qualified
+
+-- * Type 'Addable'
+class Addable sem where
+ add :: sem (Int -> Int -> Int)
+ default add ::
+ FromDerived Addable sem =>
+ sem (Int -> Int -> Int)
+ add = liftDerived add
+infixl 6 `add`, +
+(+) ::
+ Instantiable sem =>
+ Addable sem =>
+ sem Int ->
+ sem Int ->
+ sem Int
+(+) x y = add .@ x .@ y
+instance Addable sem => Addable (OpenCode sem)
+instance Addable sem => Addable (AnnotatedCode sem)
+instance Addable sem => Addable (LetInserter sem)
+instance Addable Viewer where
+ add = ViewerInfix (infixB SideL 6) "(+)" "+"
+instance Addable Identity where
+ add = lam (\x -> lam (x Prelude.+))
+
+-- * Type 'Traceable'
+class Logable sem where
+ log :: Prelude.String -> sem a -> sem a
+ default log ::
+ FromDerived1 Logable sem =>
+ Prelude.String ->
+ sem a ->
+ sem a
+ log msg = liftDerived1 (log msg)
+instance Logable sem => Logable (OpenCode sem)
+instance Logable sem => Logable (AnnotatedCode sem)
+instance Logable sem => Logable (LetInserter sem)
+instance Logable Viewer where
+ log msg a = Viewer (\_env -> showString "log " Fun.. showString (show msg)) .@ a
+instance Logable Identity where
+ log msg = Identity Fun.. trace msg Fun.. runIdentity
+
+-- * Type 'Substractable'
+class Substractable sem where
+ substract :: sem (Int -> Int -> Int)
+ default substract ::
+ FromDerived Substractable sem =>
+ sem (Int -> Int -> Int)
+ substract = liftDerived substract
+infixl 6 `substract`, -
+(-) ::
+ Instantiable sem =>
+ Substractable sem =>
+ sem Int ->
+ sem Int ->
+ sem Int
+(-) x y = substract .@ x .@ y
+instance Substractable sem => Substractable (OpenCode sem)
+instance Substractable sem => Substractable (AnnotatedCode sem)
+instance Substractable sem => Substractable (LetInserter sem)
+instance Substractable Viewer where
+ substract = ViewerInfix (infixB SideL 6) "(-)" "-"
+instance Substractable Identity where
+ substract = lam (\x -> lam (x Prelude.-))
+
+-- * Type Multiplicable
+class Multiplicable sem where
+ multiply :: sem (Int -> Int -> Int)
+ default multiply ::
+ FromDerived Multiplicable sem =>
+ sem (Int -> Int -> Int)
+ multiply = liftDerived multiply
+infixl 7 `multiply`, *
+(*) ::
+ Instantiable sem =>
+ Multiplicable sem =>
+ sem Int ->
+ sem Int ->
+ sem Int
+(*) x y = multiply .@ x .@ y
+instance Multiplicable sem => Multiplicable (OpenCode sem)
+instance Multiplicable sem => Multiplicable (AnnotatedCode sem)
+instance Multiplicable sem => Multiplicable (LetInserter sem)
+instance Multiplicable Viewer where
+ multiply = ViewerInfix (infixB SideL 7) "(*)" "*"
+instance Multiplicable Identity where
+ multiply = lam (\x -> lam (x Prelude.*))
+
+-- * Type Divisible
+class Divisible i sem where
+ divide :: sem (i -> i -> i)
+ default divide ::
+ FromDerived (Divisible i) sem =>
+ sem (i -> i -> i)
+ divide = liftDerived divide
+infixl 7 `divide`, /
+(/) ::
+ Instantiable sem =>
+ Divisible i sem =>
+ sem i ->
+ sem i ->
+ sem i
+(/) x y = divide .@ x .@ y
+instance Divisible i sem => Divisible i (OpenCode sem)
+instance Divisible i sem => Divisible i (AnnotatedCode sem)
+instance Divisible i sem => Divisible i (LetInserter sem)
+instance Divisible i Viewer where
+ divide = ViewerInfix (infixB SideL 7) "(/)" "/"
+instance Prelude.Fractional i => Divisible i Identity where
+ divide = lam (\x -> lam (x Prelude./))
sourcephile / git / haskell / symantic-base.git / commitdiff