From 8e1febb72b37887727ba0c011e9bebeca9375a35 Mon Sep 17 00:00:00 2001 From: Julien Moutinho Date: Fri, 3 May 2024 12:41:24 +0200 Subject: [PATCH] iface: add interpreter `LetInserter` --- .gitignore | 1 + .hlint.yaml | 2 + .reuse/dep5 | 2 +- Makefile | 27 +- cabal.project | 1 - flake.lock | 93 ++- flake.nix | 66 +- src/Symantic/Semantics/Identity.hs | 68 +- src/Symantic/Semantics/LetInserter.hs | 831 ++++++++++++++++++++ src/Symantic/Semantics/Viewer.hs | 173 ++-- src/Symantic/Syntaxes/Classes.hs | 69 +- symantic-base.cabal | 86 +- tests/Spec.hs | 1 + tests/Symantic/Semantics/LetInserterSpec.hs | 511 ++++++++++++ tests/Symantic/Syntaxes/Extras.hs | 124 +++ 15 files changed, 1893 insertions(+), 162 deletions(-) delete mode 100644 cabal.project create mode 100644 src/Symantic/Semantics/LetInserter.hs create mode 100644 tests/Spec.hs create mode 100644 tests/Symantic/Semantics/LetInserterSpec.hs create mode 100644 tests/Symantic/Syntaxes/Extras.hs diff --git a/.gitignore b/.gitignore index 619db9e..bb3d4b9 100644 --- a/.gitignore +++ b/.gitignore @@ -11,6 +11,7 @@ .direnv/ .ghc.environment.* .stack-work/ +dist/ dist-newstyle/ dump-core/ hlint.html diff --git a/.hlint.yaml b/.hlint.yaml index f8d02d8..077a4ae 100644 --- a/.hlint.yaml +++ b/.hlint.yaml @@ -4,6 +4,7 @@ - name: TypeApplications - ignore: {name: Avoid lambda} +- ignore: {name: Collapse lambdas} - ignore: {name: Move brackets to avoid $} - ignore: {name: Reduce duplication} - ignore: {name: Redundant $} @@ -13,6 +14,7 @@ - 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} diff --git a/.reuse/dep5 b/.reuse/dep5 index e9dd769..9844226 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -7,6 +7,6 @@ Files: *.nix *.lock cabal.project *.cabal *.md .chglog/* .envrc fourmolu.yaml .g Copyright: Julien Moutinho License: CC0-1.0 -Files: src/* +Files: src/* tests/* Copyright: Julien Moutinho License: AGPL-3.0-or-later diff --git a/Makefile b/Makefile index 71184c3..2ac569e 100644 --- a/Makefile +++ b/Makefile @@ -5,17 +5,38 @@ project := $(patsubst %.cabal,%,$(cabal)) 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 diff --git a/cabal.project b/cabal.project deleted file mode 100644 index dc68224..0000000 --- a/cabal.project +++ /dev/null @@ -1 +0,0 @@ -packages:. diff --git a/flake.lock b/flake.lock index e64f0b2..e8ac6d1 100644 --- a/flake.lock +++ b/flake.lock @@ -1,59 +1,98 @@ { "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" } } }, diff --git a/flake.nix b/flake.nix index 72724fa..908b221 100644 --- a/flake.nix +++ b/flake.nix @@ -1,53 +1,67 @@ { 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; + }; }; }; }); diff --git a/src/Symantic/Semantics/Identity.hs b/src/Symantic/Semantics/Identity.hs index 0d730cd..6cdf042 100644 --- a/src/Symantic/Semantics/Identity.hs +++ b/src/Symantic/Semantics/Identity.hs @@ -1,21 +1,57 @@ {-# 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 @@ -30,10 +66,12 @@ instance Eitherable 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 @@ -51,3 +89,13 @@ instance Unabstractable 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)) diff --git a/src/Symantic/Semantics/LetInserter.hs b/src/Symantic/Semantics/LetInserter.hs new file mode 100644 index 0000000..a61a8f8 --- /dev/null +++ b/src/Symantic/Semantics/LetInserter.hs @@ -0,0 +1,831 @@ +{-# 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 +-} diff --git a/src/Symantic/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs index e48c1f2..74f2e81 100644 --- a/src/Symantic/Semantics/Viewer.hs +++ b/src/Symantic/Semantics/Viewer.hs @@ -7,15 +7,19 @@ -- | 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 @@ -27,17 +31,28 @@ data Viewer a where 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 @@ -48,14 +63,14 @@ instance LiftDerived Viewer where 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) @@ -78,45 +93,93 @@ instance Abstractable Viewer where 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) "(<*>)" "<*>" @@ -147,11 +210,19 @@ instance Maybeable Viewer where 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 +-} diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs index 6eec73e..4dca539 100644 --- a/src/Symantic/Syntaxes/Classes.hs +++ b/src/Symantic/Syntaxes/Classes.hs @@ -61,6 +61,38 @@ class Abstractable sem where (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, @@ -94,22 +126,29 @@ class Instantiable sem where 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 $ @@ -157,6 +196,19 @@ class Constantable c sem where 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) @@ -211,19 +263,6 @@ class Inferable a sem where 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]) @@ -357,7 +396,7 @@ construct :: EoTOfRep a => CurryN args => Tuples args ~ EoT (ADT a) => - (args ~ Args (args -..-> a)) => + args ~ Args (args -..-> a) => (args -..-> a) -> sem (Tuples args) -> sem a diff --git a/symantic-base.cabal b/symantic-base.cabal index 0713d42..320d76c 100644 --- a/symantic-base.cabal +++ b/symantic-base.cabal @@ -8,10 +8,10 @@ copyright: Julien Moutinho 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: @@ -27,9 +27,6 @@ extra-doc-files: ChangeLog.md extra-source-files: .envrc cabal.project - flake.lock - flake.nix - Makefile extra-tmp-files: @@ -37,29 +34,9 @@ source-repository head 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 @@ -68,6 +45,7 @@ library LambdaCase MultiParamTypeClasses NamedFieldPuns + NoImplicitPrelude RecordWildCards ScopedTypeVariables TupleSections @@ -79,6 +57,7 @@ library -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Wpartial-fields -fprint-potential-instances +common library-deps build-depends: , base >=4.10 && <5 , containers @@ -86,3 +65,54 @@ library , 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 diff --git a/tests/Spec.hs b/tests/Spec.hs new file mode 100644 index 0000000..ebed7e1 --- /dev/null +++ b/tests/Spec.hs @@ -0,0 +1 @@ +{-# OPTIONS_GHC -F -pgmF sydtest-discover #-} diff --git a/tests/Symantic/Semantics/LetInserterSpec.hs b/tests/Symantic/Semantics/LetInserterSpec.hs new file mode 100644 index 0000000..f0dde86 --- /dev/null +++ b/tests/Symantic/Semantics/LetInserterSpec.hs @@ -0,0 +1,511 @@ +{-# 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 . n + 1>. else + . 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` "" +-- -} diff --git a/tests/Symantic/Syntaxes/Extras.hs b/tests/Symantic/Syntaxes/Extras.hs new file mode 100644 index 0000000..4d79829 --- /dev/null +++ b/tests/Symantic/Syntaxes/Extras.hs @@ -0,0 +1,124 @@ +{-# 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./)) -- 2.44.1