Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Create some unit tests for Doc syntax #5376

Merged
merged 5 commits into from
Sep 29, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions codebase2/codebase/U/Codebase/Decl.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import U.Core.ABT qualified as ABT
import U.Core.ABT.Var qualified as ABT
import Unison.Hash (Hash)
import Unison.Prelude
import Unison.Util.Recursion

type ConstructorId = Word64

Expand Down Expand Up @@ -107,7 +108,7 @@ unhashComponent componentHash refToVar m =
{ declType,
modifier,
bound,
constructorTypes = ABT.cata alg <$> constructorTypes
constructorTypes = cata alg <$> constructorTypes
}
where
rewriteTypeReference :: Reference.Id' (Maybe Hash) -> Either v Reference.Reference
Expand All @@ -126,8 +127,8 @@ unhashComponent componentHash refToVar m =
case Map.lookup (fromMaybe componentHash <$> rid) withGeneratedVars of
Nothing -> error "unhashComponent: self-reference not found in component map"
Just (v, _, _) -> Left v
alg :: () -> ABT.ABT (Type.F' TypeRef) v (HashableType v) -> HashableType v
alg () = \case
alg :: ABT.Term' (Type.F' TypeRef) v () (HashableType v) -> HashableType v
alg (ABT.Term' _ () abt) = case abt of
ABT.Var v -> ABT.var () v
ABT.Cycle body -> ABT.cycle () body
ABT.Abs v body -> ABT.abs () v body
Expand Down
7 changes: 4 additions & 3 deletions codebase2/codebase/U/Codebase/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ import U.Core.ABT qualified as ABT
import U.Core.ABT.Var qualified as ABT
import Unison.Hash (Hash)
import Unison.Prelude
import Unison.Util.Recursion

type ConstructorId = Word64

Expand Down Expand Up @@ -281,7 +282,7 @@ unhashComponent componentHash refToVar m =
assignVar :: Reference.Id -> (trm, extra) -> StateT (Set v) Identity (v, trm, extra)
assignVar r (trm, extra) = (,trm,extra) <$> ABT.freshenS (refToVar r)
fillSelfReferences :: Term v -> HashableTerm v
fillSelfReferences = (ABT.cata alg)
fillSelfReferences = cata alg
where
rewriteTermReference :: Reference.Id' (Maybe Hash) -> Either v Reference.Reference
rewriteTermReference rid@(Reference.Id mayH pos) =
Expand All @@ -299,8 +300,8 @@ unhashComponent componentHash refToVar m =
case Map.lookup (fromMaybe componentHash <$> rid) withGeneratedVars of
Nothing -> error "unhashComponent: self-reference not found in component map"
Just (v, _, _) -> Left v
alg :: () -> ABT.ABT (F v) v (HashableTerm v) -> HashableTerm v
alg () = \case
alg :: ABT.Term' (F v) v () (HashableTerm v) -> HashableTerm v
alg (ABT.Term' _ () abt) = case abt of
ABT.Var v -> ABT.var () v
ABT.Cycle body -> ABT.cycle () body
ABT.Abs v body -> ABT.abs () v body
Expand Down
1 change: 1 addition & 0 deletions codebase2/codebase/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ dependencies:
- unison-core
- unison-hash
- unison-prelude
- unison-util-recursion

library:
source-dirs: .
Expand Down
1 change: 1 addition & 0 deletions codebase2/codebase/unison-codebase.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -69,4 +69,5 @@ library
, unison-core
, unison-hash
, unison-prelude
, unison-util-recursion
default-language: GHC2021
26 changes: 8 additions & 18 deletions codebase2/core/U/Core/ABT.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ import Debug.RecoverRTTI qualified as RTTI
import U.Core.ABT.Var (Var (freshIn))
import Unison.Debug qualified as Debug
import Unison.Prelude
import Unison.Util.Recursion
import Prelude hiding (abs, cycle)

data ABT f v r
Expand All @@ -24,6 +25,13 @@ data ABT f v r
data Term f v a = Term {freeVars :: Set v, annotation :: a, out :: ABT f v (Term f v a)}
deriving (Functor, Foldable, Generic, Traversable)

data Term' f v a x = Term' {freeVars' :: Set v, annotation' :: a, out' :: ABT f v x}
deriving (Functor)

instance (Functor f) => Recursive (Term f v a) (Term' f v a) where
embed (Term' vs a abt) = Term vs a abt
project (Term vs a abt) = Term' vs a abt

instance (Foldable f, Functor f, forall a. (Eq a) => Eq (f a), Var v) => Eq (Term f v a) where
-- alpha equivalence, works by renaming any aligned Abs ctors to use a common fresh variable
t1 == t2 = go (out t1) (out t2)
Expand Down Expand Up @@ -97,24 +105,6 @@ vmapM f (Term _ a out) = case out of
Cycle r -> cycle a <$> vmapM f r
Abs v body -> abs a <$> f v <*> vmapM f body

cata ::
(Functor f) =>
(a -> ABT f v x -> x) ->
Term f v a ->
x
cata abtAlg =
let go (Term _fvs a out) = abtAlg a (fmap go out)
in go

para ::
(Functor f) =>
(a -> ABT f v (Term f v a, x) -> x) ->
Term f v a ->
x
para abtAlg =
let go (Term _fvs a out) = abtAlg a (fmap (\x -> (x, go x)) out)
in go

transform ::
(Ord v, Foldable g, Functor g) =>
(forall a. f a -> g a) ->
Expand Down
1 change: 1 addition & 0 deletions codebase2/core/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ dependencies:
- text
- unison-hash
- unison-prelude
- unison-util-recursion

default-extensions:
- ApplicativeDo
Expand Down
1 change: 1 addition & 0 deletions codebase2/core/unison-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -64,4 +64,5 @@ library
, text
, unison-hash
, unison-prelude
, unison-util-recursion
default-language: Haskell2010
3 changes: 2 additions & 1 deletion contrib/cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,10 @@ packages:
lib/unison-util-base32hex
lib/unison-util-bytes
lib/unison-util-cache
lib/unison-util-file-embed
lib/unison-util-recursion
lib/unison-util-relation
lib/unison-util-rope
lib/unison-util-file-embed

parser-typechecker
unison-core
Expand Down
46 changes: 46 additions & 0 deletions lib/unison-util-recursion/package.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
name: unison-util-recursion
github: unisonweb/unison
copyright: Copyright (C) 2013-2022 Unison Computing, PBC and contributors

ghc-options: -Wall

dependencies:
- base
- free

library:
source-dirs: src
when:
- condition: false
other-modules: Paths_unison_util_recursion

default-extensions:
- ApplicativeDo
- BangPatterns
- BlockArguments
- DeriveAnyClass
- DeriveFoldable
- DeriveFunctor
- DeriveGeneric
- DeriveTraversable
- DerivingStrategies
- DerivingVia
- DoAndIfThenElse
- DuplicateRecordFields
- FlexibleContexts
- FlexibleInstances
- FunctionalDependencies
- GeneralizedNewtypeDeriving
- ImportQualifiedPost
- LambdaCase
- MultiParamTypeClasses
- NamedFieldPuns
- OverloadedStrings
- PatternSynonyms
- RankNTypes
- ScopedTypeVariables
- StandaloneDeriving
- TupleSections
- TypeApplications
- TypeFamilies
- ViewPatterns
57 changes: 57 additions & 0 deletions lib/unison-util-recursion/src/Unison/Util/Recursion.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

module Unison.Util.Recursion
( Algebra,
Recursive (..),
cataM,
para,
Fix (..),
Cofree' (..),
)
where

import Control.Arrow ((&&&))
import Control.Comonad.Cofree (Cofree ((:<)))
import Control.Monad ((<=<))

type Algebra f a = f a -> a

class Recursive t f | t -> f where
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just curious why not use recursion-schemes directly?

I personally find your encoding here less confusing than all the Base type-family nonsense, but it's also nice to maintain compatibility with the ecosystem where possible 😄

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, my plan was to replace this with a recursion scheme library eventually. At this point, I was just trying to centralize the (mostly) existing copies of this pattern.

I’m happy to put in recursion-schemes, but I also have my own recursion scheme library, Yaya, which makes some different decisions than recursion-schemes1. One of them is the use of FunctionalDependencies, as you pointed out. Another is that Yaya tries to provide totality (especially when paired with NoRecursion).

So I just punted on that discussion for now.

Footnotes

  1. There’s a more in-depth comparison with recursion-schemes in Yaya’s README.

cata :: (Algebra f a) -> t -> a
default cata :: (Functor f) => (f a -> a) -> t -> a
cata φ = φ . fmap (cata φ) . project
project :: t -> f t
default project :: (Functor f) => t -> f t
project = cata (fmap embed)
embed :: f t -> t
{-# MINIMAL embed, (cata | project) #-}

cataM :: (Recursive t f, Traversable f, Monad m) => (f a -> m a) -> t -> m a
cataM φ = cata $ φ <=< sequenceA

para :: (Recursive t f, Functor f) => (f (t, a) -> a) -> t -> a
para φ = snd . cata (embed . fmap fst &&& φ)

newtype Fix f = Fix (f (Fix f))

deriving instance (forall a. (Show a) => Show (f a)) => Show (Fix f)

deriving instance (forall a. (Eq a) => Eq (f a)) => Eq (Fix f)

deriving instance (Eq (Fix f), forall a. (Ord a) => Ord (f a)) => Ord (Fix f)

instance (Functor f) => Recursive (Fix f) f where
embed = Fix
project (Fix f) = f

data Cofree' f a x = a :<< f x
deriving (Foldable, Functor, Traversable)
Comment on lines +49 to +50
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just curious, any reason why not use CofreeF from free?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I should have. I think I got confused and tried to use the isomorphic EnvT … but that’s from transformers, and I didn’t find it in free (of course), so I was like “oh, maybe the pattern functor isn’t here.”

In my own code, I don’t use those because they’re not strict in the functor parameter, so they don’t result in lawful fixed points. But my Cofree' here isn’t strict either, so …


-- |
--
-- __NB__: `Cofree` from “free” is lazy, so this instance is technically partial.
instance (Functor f) => Recursive (Cofree f a) (Cofree' f a) where
embed (a :<< fco) = a :< fco
project (a :< fco) = a :<< fco
57 changes: 57 additions & 0 deletions lib/unison-util-recursion/unison-util-recursion.cabal
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
cabal-version: 1.12

-- This file has been generated from package.yaml by hpack version 0.36.0.
--
-- see: https://github.com/sol/hpack

name: unison-util-recursion
version: 0.0.0
homepage: https://github.com/unisonweb/unison#readme
bug-reports: https://github.com/unisonweb/unison/issues
copyright: Copyright (C) 2013-2022 Unison Computing, PBC and contributors
build-type: Simple

source-repository head
type: git
location: https://github.com/unisonweb/unison

library
exposed-modules:
Unison.Util.Recursion
hs-source-dirs:
src
default-extensions:
ApplicativeDo
BangPatterns
BlockArguments
DeriveAnyClass
DeriveFoldable
DeriveFunctor
DeriveGeneric
DeriveTraversable
DerivingStrategies
DerivingVia
DoAndIfThenElse
DuplicateRecordFields
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GeneralizedNewtypeDeriving
ImportQualifiedPost
LambdaCase
MultiParamTypeClasses
NamedFieldPuns
OverloadedStrings
PatternSynonyms
RankNTypes
ScopedTypeVariables
StandaloneDeriving
TupleSections
TypeApplications
TypeFamilies
ViewPatterns
ghc-options: -Wall
build-depends:
base
, free
default-language: Haskell2010
1 change: 1 addition & 0 deletions parser-typechecker/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ library:
- unison-util-base32hex
- unison-util-bytes
- unison-util-cache
- unison-util-recursion
- unison-util-relation
- unison-util-rope
- unison-util-serialization
Expand Down
7 changes: 4 additions & 3 deletions parser-typechecker/src/Unison/KindInference/Generate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ import Unison.Prelude
import Unison.Reference (Reference)
import Unison.Term qualified as Term
import Unison.Type qualified as Type
import Unison.Util.Recursion
import Unison.Var (Type (User), Var (typed), freshIn)

--------------------------------------------------------------------------------
Expand Down Expand Up @@ -160,7 +161,7 @@ instantiateType type0 k =
-- | Process type annotations depth-first. Allows processing
-- annotations with lexical scoping.
dfAnns :: (loc -> Type.Type v loc -> b -> b) -> (b -> b -> b) -> b -> Term.Term v loc -> b
dfAnns annAlg cons nil = ABT.cata \ann abt0 -> case abt0 of
dfAnns annAlg cons nil = cata \(ABT.Term' _ ann abt0) -> case abt0 of
ABT.Var _ -> nil
ABT.Cycle x -> x
ABT.Abs _ x -> x
Expand All @@ -173,7 +174,7 @@ dfAnns annAlg cons nil = ABT.cata \ann abt0 -> case abt0 of
-- annotations.
hackyStripAnns :: (Ord v) => Term.Term v loc -> Term.Term v loc
hackyStripAnns =
snd . ABT.cata \ann abt0 -> case abt0 of
snd . cata \(ABT.Term' _ ann abt0) -> case abt0 of
ABT.Var v -> (False, ABT.var ann v)
ABT.Cycle (_, x) -> (False, ABT.cycle ann x)
ABT.Abs v (_, x) -> (False, ABT.abs ann v x)
Expand All @@ -188,7 +189,7 @@ hackyStripAnns =
in (isHack, Term.constructor ann cref)
t -> (False, ABT.tm ann (snd <$> t))
where
stripAnns = ABT.cata \ann abt0 -> case abt0 of
stripAnns = cata \(ABT.Term' _ ann abt0) -> case abt0 of
ABT.Var v -> ABT.var ann v
ABT.Cycle x -> ABT.cycle ann x
ABT.Abs v x -> ABT.abs ann v x
Expand Down
Loading