include constructor names in decl synhashes

This commit is contained in:
Mitchell Rosen 2024-04-16 11:49:59 -04:00
parent efe405f244
commit 75ae8120af
8 changed files with 268 additions and 197 deletions

View File

@ -134,7 +134,7 @@ handleMerge bobBranchName = do
-- Diff LCA->Alice and LCA->Bob
diffs <-
Cli.runTransaction do
Merge.nameBasedNamespaceDiff db defns
Merge.nameBasedNamespaceDiff db declNameLookups defns
debugDiffs diffs
@ -144,7 +144,7 @@ handleMerge bobBranchName = do
-- Combine the LCA->Alice and LCA->Bob diffs together into the conflicted things and the unconflicted things
(conflicts, unconflicts) <-
combineDiffs declNameLookups (ThreeWay.forgetLca defns) diffs & onLeft \name ->
combineDiffs (ThreeWay.forgetLca declNameLookups) (ThreeWay.forgetLca defns) diffs & onLeft \name ->
Cli.returnEarly (mergePreconditionViolationToOutput (Merge.ConflictInvolvingBuiltin name))
debugCombinedDiffs conflicts unconflicts
@ -158,7 +158,12 @@ handleMerge bobBranchName = do
debugDependents dependents
let (newDefns, droppedDefns) =
bumpLca declNameLookups conflicts unconflicts (bimap Map.elemsSet Map.elemsSet dependents) defns.lca
bumpLca
(ThreeWay.forgetLca declNameLookups)
conflicts
unconflicts
(bimap Map.elemsSet Map.elemsSet dependents)
defns.lca
debugMergedDefns newDefns droppedDefns
@ -180,7 +185,12 @@ handleMerge bobBranchName = do
-- Create the Unison file, which may have conflicts, in which case we don't bother trying to parse and typecheck it.
unisonFile <-
if thisMergeHasConflicts
then makeConflictedUnisonFile declNameLookups conflicts dependents mergedDeclNameLookup
then
makeConflictedUnisonFile
(ThreeWay.forgetLca declNameLookups)
conflicts
dependents
mergedDeclNameLookup
else makeUnconflictedUnisonFile dependents mergedDeclNameLookup
-- Load and merge Alice's and Bob's libdeps
@ -283,22 +293,27 @@ loadDefns ::
(forall a. Output -> Transaction a) ->
MergeDatabase ->
MergeInfo ->
(TwoOrThreeWay (V2.Branch Transaction)) ->
Transaction (TwoWay DeclNameLookup, ThreeWay (Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name)))
TwoOrThreeWay (V2.Branch Transaction) ->
Transaction
( ThreeWay DeclNameLookup,
ThreeWay (Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name))
)
loadDefns abort0 db info branches = do
lcaDefns <-
lcaDefns0 <-
case branches.lca of
Nothing -> pure (Defns BiMultimap.empty BiMultimap.empty)
Just lcaBranch -> loadLcaDefinitions abort (referent2to1 db) lcaBranch
Nothing -> pure Nametree {value = Defns Map.empty Map.empty, children = Map.empty}
Just lcaBranch -> loadNamespaceInfo abort db lcaBranch
(lcaDeclNameLookup, lcaDefns1) <-
assertNamespaceSatisfiesPreconditions db abort Nothing (fromMaybe V2.Branch.empty branches.lca) lcaDefns0
aliceDefns0 <- loadNamespaceInfo abort db branches.alice
(aliceDeclNameLookup, aliceDefns1) <-
assertNamespaceSatisfiesPreconditions db abort info.projectBranches.alice.name branches.alice aliceDefns0
assertNamespaceSatisfiesPreconditions db abort (Just info.projectBranches.alice.name) branches.alice aliceDefns0
bobDefns0 <- loadNamespaceInfo abort db branches.bob
(bobDeclNameLookup, bobDefns1) <-
assertNamespaceSatisfiesPreconditions db abort info.projectBranches.bob.name branches.bob bobDefns0
assertNamespaceSatisfiesPreconditions db abort (Just info.projectBranches.bob.name) branches.bob bobDefns0
pure
( TwoWay {alice = aliceDeclNameLookup, bob = bobDeclNameLookup},
ThreeWay {lca = lcaDefns, alice = aliceDefns1, bob = bobDefns1}
( ThreeWay {lca = lcaDeclNameLookup, alice = aliceDeclNameLookup, bob = bobDeclNameLookup},
ThreeWay {lca = lcaDefns1, alice = aliceDefns1, bob = bobDefns1}
)
where
abort :: Merge.PreconditionViolation -> Transaction void
@ -929,7 +944,7 @@ mergePreconditionViolationToOutput = \case
Merge.ConflictedTermName name refs -> Output.MergeConflictedTermName name refs
Merge.ConflictedTypeName name refs -> Output.MergeConflictedTypeName name refs
Merge.ConflictInvolvingBuiltin name -> Output.MergeConflictInvolvingBuiltin name
Merge.ConstructorAlias branch name1 name2 -> Output.MergeConstructorAlias branch name1 name2
Merge.ConstructorAlias maybeBranch name1 name2 -> Output.MergeConstructorAlias maybeBranch name1 name2
Merge.DefnsInLib -> Output.MergeDefnsInLib
Merge.MissingConstructorName name -> Output.MergeMissingConstructorName name
Merge.NestedDeclAlias name -> Output.MergeNestedDeclAlias name
@ -943,11 +958,11 @@ mergePreconditionViolationToOutput = \case
assertNamespaceSatisfiesPreconditions ::
MergeDatabase ->
(forall void. Merge.PreconditionViolation -> Transaction void) ->
ProjectBranchName ->
Maybe ProjectBranchName ->
V2.Branch Transaction ->
Nametree (DefnsF (Map NameSegment) Referent TypeReference) ->
Transaction (DeclNameLookup, Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name))
assertNamespaceSatisfiesPreconditions db abort branchName branch defns = do
assertNamespaceSatisfiesPreconditions db abort maybeBranchName branch defns = do
Map.lookup NameSegment.libSegment branch.children `whenJust` \libdepsCausal -> do
libdepsBranch <- libdepsCausal.value
when (not (Map.null libdepsBranch.terms) || not (Map.null libdepsBranch.types)) do
@ -966,30 +981,11 @@ assertNamespaceSatisfiesPreconditions db abort branchName branch defns = do
incoherentDeclReasonToMergePreconditionViolation :: IncoherentDeclReason -> Merge.PreconditionViolation
incoherentDeclReasonToMergePreconditionViolation = \case
IncoherentDeclReason'ConstructorAlias firstName secondName ->
Merge.ConstructorAlias branchName firstName secondName
Merge.ConstructorAlias maybeBranchName firstName secondName
IncoherentDeclReason'MissingConstructorName name -> Merge.MissingConstructorName name
IncoherentDeclReason'NestedDeclAlias name -> Merge.NestedDeclAlias name
IncoherentDeclReason'StrayConstructor name -> Merge.StrayConstructor name
-- Like `loadNamespaceInfo`, but for loading the LCA, which has fewer preconditions.
--
-- Fails if:
-- * One name is associated with more than one reference.
loadLcaDefinitions ::
(Monad m) =>
(forall void. Merge.PreconditionViolation -> m void) ->
(V2.Referent -> m Referent) ->
V2.Branch m ->
m (Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name))
loadLcaDefinitions abort referent2to1 branch = do
defns0 <- loadNamespaceInfo0 referent2to1 branch
defns1 <- assertNamespaceHasNoConflictedNames defns0 & onLeft abort
pure
Defns
{ terms = flattenNametree (view #terms) defns1,
types = flattenNametree (view #types) defns1
}
findOneConflictedAlias ::
TwoWay ProjectBranch ->
Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name) ->
@ -1108,7 +1104,7 @@ libdepsToBranch0 db libdeps = do
debugDefns ::
MonadIO m =>
TwoWay DeclNameLookup ->
ThreeWay DeclNameLookup ->
ThreeWay (Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name)) ->
m ()
debugDefns declNameLookups defns =

View File

@ -401,7 +401,7 @@ data Output
| MergeConflictedTermName !Name !(Set Referent)
| MergeConflictedTypeName !Name !(Set Reference.TypeReference)
| MergeConflictInvolvingBuiltin !Name
| MergeConstructorAlias !ProjectBranchName !Name !Name
| MergeConstructorAlias !(Maybe ProjectBranchName) !Name !Name
| MergeDefnsInLib
| MergeMissingConstructorName !Name
| MergeNestedDeclAlias !Name

View File

@ -1660,10 +1660,12 @@ notifyUser dir = \case
"There's a merge conflict on"
<> P.group (prettyName name <> ",")
<> "but it's a builtin on one or both branches. We can't yet handle merge conflicts on builtins."
MergeConstructorAlias branch name1 name2 ->
MergeConstructorAlias maybeBranch name1 name2 ->
pure . P.wrap $
"On"
<> P.group (prettyProjectBranchName branch <> ",")
<> case maybeBranch of
Nothing -> "the LCA,"
Just branch -> P.group (prettyProjectBranchName branch <> ",")
<> prettyName name1
<> "and"
<> prettyName name2

View File

@ -102,6 +102,7 @@ oingoBoingo declNameLookups defns diff =
bitraverse honkTerms honkTypes diff
-- added term: we keep the add
--
-- added constructor:
-- - if its type is me-conflicted then we drop the add
-- - else if its type is them-conflicted then we promote our type to me-conflicted

View File

@ -5,14 +5,19 @@ module Unison.Merge.Diff
)
where
import Control.Lens (over)
import Data.Bitraversable (bitraverse)
import Data.Map.Strict qualified as Map
import Data.Semialign (alignWith)
import Data.Set qualified as Set
import Data.These (These (..))
import U.Codebase.Reference (TypeReference)
import Unison.DataDeclaration (Decl)
import Unison.DataDeclaration qualified as DD
import Unison.Hash (Hash)
import Unison.HashQualified' qualified as HQ'
import Unison.Merge.Database (MergeDatabase (..))
import Unison.Merge.DeclNameLookup (DeclNameLookup, expectConstructorNames)
import Unison.Merge.DiffOp (DiffOp (..))
import Unison.Merge.Synhash qualified as Synhash
import Unison.Merge.Synhashed (Synhashed (..))
@ -22,11 +27,15 @@ import Unison.Name (Name)
import Unison.Prelude hiding (catMaybes)
import Unison.PrettyPrintEnv (PrettyPrintEnv (..))
import Unison.PrettyPrintEnv qualified as Ppe
import Unison.Reference (TypeReferenceId)
import Unison.Referent (Referent)
import Unison.Sqlite (Transaction)
import Unison.Syntax.Name qualified as Name
import Unison.Type (Type)
import Unison.Util.BiMultimap (BiMultimap)
import Unison.Util.BiMultimap qualified as BiMultimap
import Unison.Util.Defns (Defns (..), DefnsF)
import Unison.Var (Var)
-- | @nameBasedNamespaceDiff db defns@ returns Alice's and Bob's name-based namespace diffs, each in the form:
--
@ -40,6 +49,7 @@ import Unison.Util.Defns (Defns (..), DefnsF)
-- branches is considered an add.
nameBasedNamespaceDiff ::
MergeDatabase ->
ThreeWay DeclNameLookup ->
ThreeWay (Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name)) ->
Transaction
( TwoWay
@ -49,24 +59,47 @@ nameBasedNamespaceDiff ::
(DiffOp (Synhashed TypeReference))
)
)
nameBasedNamespaceDiff db defns = do
lca <- synhashDefns defns.lca
alice <- synhashDefns defns.alice
bob <- synhashDefns defns.bob
pure (diffNamespaceDefns lca <$> TwoWay {alice, bob})
nameBasedNamespaceDiff db declNameLookups defns = do
diffs <- sequence (synhashDefns <$> declNameLookups <*> defns)
pure (diffNamespaceDefns diffs.lca <$> TwoWay {alice = diffs.alice, bob = diffs.bob})
where
synhashDefns ::
DeclNameLookup ->
Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name) ->
Transaction (DefnsF (Map Name) (Synhashed Referent) (Synhashed TypeReference))
synhashDefns =
synhashDefns declNameLookup =
-- FIXME: use cache so we only synhash each thing once
synhashDefnsWith (Synhash.hashTerm db.loadV1Term ppe) (Synhash.hashDecl db.loadV1Decl ppe)
synhashDefnsWith
(Synhash.hashTerm db.loadV1Term ppe)
( \name ->
Synhash.hashDecl
(withAccurateConstructorNames db.loadV1Decl declNameLookup name)
ppe
name
)
where
ppe :: PrettyPrintEnv
ppe =
-- The order isn't important here for syntactic hashing
(deepNamespaceDefinitionsToPpe defns.alice `Ppe.addFallback` deepNamespaceDefinitionsToPpe defns.bob)
withAccurateConstructorNames ::
forall a v.
Var v =>
(TypeReferenceId -> Transaction (Decl v a)) ->
DeclNameLookup ->
Name ->
TypeReferenceId ->
Transaction (Decl v a)
withAccurateConstructorNames load declNameLookup name ref = do
load ref <&> over (DD.declAsDataDecl_ . DD.constructors_) setConstructorNames
where
setConstructorNames :: [(a, v, Type v a)] -> [(a, v, Type v a)]
setConstructorNames =
zipWith
(\realConName (ann, _junkConName, typ) -> (ann, Name.toVar realConName, typ))
(expectConstructorNames declNameLookup name)
diffNamespaceDefns ::
DefnsF (Map Name) (Synhashed Referent) (Synhashed TypeReference) ->
DefnsF (Map Name) (Synhashed Referent) (Synhashed TypeReference) ->
@ -110,18 +143,18 @@ deepNamespaceDefinitionsToPpe Defns {terms, types} =
synhashDefnsWith ::
Monad m =>
(term -> m Hash) ->
(typ -> m Hash) ->
(Name -> typ -> m Hash) ->
Defns (BiMultimap term Name) (BiMultimap typ Name) ->
m (DefnsF (Map Name) (Synhashed term) (Synhashed typ))
synhashDefnsWith hashTerm hashType defns = do
terms <- BiMultimap.range <$> BiMultimap.unsafeTraverseDom hashTerm1 defns.terms
types <- BiMultimap.range <$> BiMultimap.unsafeTraverseDom hashType1 defns.types
pure Defns {terms, types}
synhashDefnsWith hashTerm hashType = do
bitraverse
(traverse hashTerm1 . BiMultimap.range)
(Map.traverseWithKey hashType1 . BiMultimap.range)
where
hashTerm1 term = do
hash <- hashTerm term
pure (Synhashed hash term)
hashType1 typ = do
hash <- hashType typ
hashType1 name typ = do
hash <- hashType name typ
pure (Synhashed hash typ)

View File

@ -26,7 +26,9 @@ data PreconditionViolation
-- Foo#Foo
-- Foo.Bar#Foo#0
-- Foo.Some.Other.Name.For.Bar#Foo#0
ConstructorAlias !ProjectBranchName !Name !Name -- first name we found, second name we found
--
-- If the project branch name is missing, it means the LCA is in violation.
ConstructorAlias !(Maybe ProjectBranchName) !Name !Name -- first name we found, second name we found
| -- | There were some definitions at the top level of lib.*, which we don't like
DefnsInLib
| MissingConstructorName !Name

View File

@ -35,13 +35,16 @@ import Data.Text qualified as Text
import U.Codebase.Reference (TypeReference)
import Unison.ABT qualified as ABT
import Unison.ConstructorReference (GConstructorReference (..))
import Unison.ConstructorType (ConstructorType)
import Unison.ConstructorType qualified as CT
import Unison.DataDeclaration (Decl)
import Unison.DataDeclaration (DataDeclaration, Decl)
import Unison.DataDeclaration qualified as DD
import Unison.Hash (Hash)
import Unison.HashQualified as HQ
import Unison.Hashable qualified as H
import Unison.Kind qualified as K
import Unison.Name (Name)
import Unison.Name qualified as Name
import Unison.Pattern qualified as Pattern
import Unison.Prelude
import Unison.PrettyPrintEnv (PrettyPrintEnv)
@ -49,7 +52,7 @@ import Unison.PrettyPrintEnv qualified as PPE
import Unison.Reference (Reference' (..), TypeReferenceId)
import Unison.Referent qualified as V1 (Referent)
import Unison.Referent qualified as V1.Referent
import Unison.Syntax.Name qualified as Name (toText)
import Unison.Syntax.Name qualified as Name (toText, unsafeParseVar)
import Unison.Term (Term)
import Unison.Term qualified as Term
import Unison.Type (Type)
@ -69,104 +72,103 @@ isDeclTag, isTermTag :: H.Token Hash
isDeclTag = H.Tag 0
isTermTag = H.Tag 1
-- | Syntactically hash a type, using reference names rather than hashes.
-- Two types will have the same syntactic hash if they would
-- print the the same way under the given pretty-print env.
hashType :: Var v => PrettyPrintEnv -> Type v a -> Hash
hashType ppe t = H.accumulate $ hashTypeTokens ppe t
-- | Syntactically hash a term, using reference names rather than hashes.
-- Two terms will have the same syntactic hash if they would
-- print the the same way under the given pretty-print env.
hashTerm :: forall m v a. (Monad m, Var v) => (TypeReferenceId -> m (Term v a)) -> PrettyPrintEnv -> V1.Referent -> m Hash
hashTerm loadTerm ppe = \case
V1.Referent.Con r t -> pure $ hashDerivedTerm ppe case t of
CT.Data -> Term.constructor @v () r
CT.Effect -> Term.request @v () r
V1.Referent.Ref ref -> case ref of
ReferenceBuiltin name -> pure (hashBuiltinTerm name)
ReferenceDerived x -> do
term <- loadTerm x
pure (hashDerivedTerm ppe term)
-- hashCons :: (Monad m, var v) => (ConstructorReferenceId -> m
hashDerivedTerm :: Var v => PrettyPrintEnv -> Term v a -> Hash
hashDerivedTerm ppe t = H.accumulate $ isNotBuiltinTag : hashTermTokens ppe t
hashBuiltinDecl :: Text -> Hash
hashBuiltinDecl name =
H.accumulate [isBuiltinTag, isDeclTag, H.Text name]
hashBuiltinTerm :: Text -> Hash
hashBuiltinTerm name =
H.accumulate [isBuiltinTag, isTermTag, H.Text name]
-- | Syntactically hash a decl, using reference names rather than hashes.
-- Two decls will have the same syntactic hash if they they are
-- the same sort of decl (both are data decls or both are effect decls),
-- the unique type guid is the same, and the constructors appear in the
-- same order and their types have the same syntactic hash.
hashCaseTokens :: PrettyPrintEnv -> Term.MatchCase loc a -> [Token]
hashCaseTokens ppe (Term.MatchCase pat Nothing _) = H.Tag 0 : hashPatternTokens ppe pat
hashCaseTokens ppe (Term.MatchCase pat (Just _) _) = H.Tag 1 : hashPatternTokens ppe pat
-- | The hash of a constructor name determined by how it looks when rendered, i.e. without the decl name prefix.
--
-- For example, in the decl "Maybe" with constructors "Maybe.Just" and "Maybe.Nothing", the hash of constructor
-- "Maybe.Nothing" is hash of the string "Nothing".
hashConstructorNameToken :: Name -> Name -> Token
hashConstructorNameToken declName conName =
let strippedConName =
Name.stripNamePrefix declName conName
& fromMaybe
( error $
reportBug
"E784201"
( "constructor "
++ Text.unpack (Name.toText conName)
++ " not under decl "
++ Text.unpack (Name.toText declName)
)
)
in H.Text (Name.toText strippedConName)
-- | Syntactically hash a decl, using reference names rather than hashes. Two decls will have the same syntactic hash if
-- they they are the same sort of decl (both are data decls or both are effect decls), the unique type guid is the same,
-- the constructors appear in the same order and have the same names, and the constructors' types have the same
-- syntactic hashes.
hashDecl ::
(Monad m, Var v) =>
(TypeReferenceId -> m (Decl v a)) ->
PrettyPrintEnv ->
Name ->
TypeReference ->
m Hash
hashDecl loadDecl ppe = \case
ReferenceBuiltin name -> pure (hashBuiltinDecl name)
hashDecl loadDecl ppe name = \case
ReferenceBuiltin builtin -> pure (hashBuiltinDecl builtin)
ReferenceDerived ref -> do
decl <- loadDecl ref
pure (hashDerivedDecl ppe ref decl)
pure (hashDerivedDecl ppe name decl)
hashDerivedDecl :: Var v => PrettyPrintEnv -> TypeReferenceId -> Decl v a -> Hash
hashDerivedDecl ppe r t = H.accumulate $ isNotBuiltinTag : hashDeclTokens ppe r t
hashDerivedTerm :: Var v => PrettyPrintEnv -> Term v a -> Hash
hashDerivedTerm ppe t =
H.accumulate $ isNotBuiltinTag : hashTermTokens ppe t
hashBuiltinDecl :: Text -> Hash
hashBuiltinDecl name =
H.accumulate [isBuiltinTag, isDeclTag, H.Text name]
hashConstructorType :: ConstructorType -> Token
hashConstructorType = \case
CT.Effect -> H.Tag 0
CT.Data -> H.Tag 1
hashDeclTokens :: Var v => PrettyPrintEnv -> TypeReferenceId -> Decl v a -> [Token]
hashDeclTokens ppe r = \case
Left (DD.EffectDeclaration dd) -> H.Tag 0 : go CT.Effect dd
Right dd -> H.Tag 1 : go CT.Data dd
hashDataDeclTokens :: Var v => PrettyPrintEnv -> Name -> DataDeclaration v a -> [Token]
hashDataDeclTokens ppe declName (DD.DataDeclaration modifier _ vs ctors) =
hashModifierTokens modifier <> goVs <> (ctors >>= hashConstructorTokens ppe declName)
where
goMod = \case
DD.Structural -> [H.Tag 0]
DD.Unique txt -> [H.Tag 1, H.Text txt]
goVs vs = hashLengthToken vs : (H.Text . Var.name <$> vs)
-- separating constructor types with tag of 99, which isn't used elsewhere
goCtor ct ((_, _, ty), i) = H.Tag 99 : ctorName ct i : hashTypeTokens ppe ty
ctorName ct i = hashReferentToken ppe (V1.Referent.Con (ConstructorReference (ReferenceDerived r) i) ct)
go ct (DD.DataDeclaration x _ vs ctors) =
goMod x <> goVs vs <> ((zip ctors [0 ..]) >>= goCtor ct)
goVs =
hashLengthToken vs : map hashVarToken vs
-- separating constructor types with tag of 99, which isn't used elsewhere
hashConstructorTokens :: Var v => PrettyPrintEnv -> Name -> (a, v, Type v a) -> [Token]
hashConstructorTokens ppe declName (_, conName, ty) =
H.Tag 99
: hashConstructorNameToken declName (Name.unsafeParseVar conName)
: hashTypeTokens ppe ty
hashDeclTokens :: Var v => PrettyPrintEnv -> Name -> Decl v a -> [Token]
hashDeclTokens ppe name decl =
hashConstructorType (DD.constructorType decl) : hashDataDeclTokens ppe name (DD.asDataDecl decl)
hashDerivedDecl :: Var v => PrettyPrintEnv -> Name -> Decl v a -> Hash
hashDerivedDecl ppe name decl =
H.accumulate $ isNotBuiltinTag : hashDeclTokens ppe name decl
hashHQNameToken :: HashQualified Name -> Token
hashHQNameToken =
H.Text . HQ.toTextWith Name.toText
hashKindTokens :: K.Kind -> [Token]
hashKindTokens k = case k of
K.Star -> [H.Tag 0]
K.Arrow k1 k2 -> H.Tag 1 : (hashKindTokens k1 <> hashKindTokens k2)
hashTypeTokens :: forall v a. Var v => PrettyPrintEnv -> Type v a -> [Token]
hashTypeTokens ppe = go
where
ft :: Type.F () -> [Token]
ft = \case
Type.Ref r -> [H.Tag 0, hashTypeReferenceToken ppe r]
Type.Arrow {} -> [H.Tag 1]
Type.Ann _ k -> H.Tag 2 : hashKindTokens k
Type.App {} -> [H.Tag 3]
Type.Effect {} -> [H.Tag 4]
Type.Effects es -> [H.Tag 5, hashLengthToken es]
Type.Forall {} -> [H.Tag 6]
Type.IntroOuter {} -> [H.Tag 7]
go :: Type v a -> [Token]
go t =
H.Tag 254 : case ABT.out t of
ABT.Var v -> [H.Tag 0, H.Text (Var.name v)]
-- trick: encode the structure, followed the children as a flat list
ABT.Tm f -> H.Tag 1 : (ft (void f) <> (toList f >>= go))
ABT.Cycle c -> H.Tag 2 : go c
ABT.Abs v body -> H.Tag 3 : H.Text (Var.name v) : go body
hashLengthToken :: Foldable t => t a -> Token
hashLengthToken =
H.Nat . fromIntegral @Int @Word64 . length
hashCaseTokens :: PrettyPrintEnv -> Term.MatchCase loc a -> [Token]
hashCaseTokens ppe (Term.MatchCase pat Nothing _) = H.Tag 0 : hashPatternTokens ppe pat
hashCaseTokens ppe (Term.MatchCase pat (Just _) _) = H.Tag 1 : hashPatternTokens ppe pat
hashModifierTokens :: DD.Modifier -> [Token]
hashModifierTokens = \case
DD.Structural -> [H.Tag 0]
DD.Unique txt -> [H.Tag 1, H.Text txt]
hashPatternTokens :: PrettyPrintEnv -> Pattern.Pattern loc -> [Token]
hashPatternTokens ppe = \case
@ -189,84 +191,115 @@ hashPatternTokens ppe = \case
H.Tag 11
: hashReferentToken ppe (V1.Referent.Con cr CT.Effect)
: hashLengthToken ps
: (hashPatternTokens ppe k <> (ps >>= hashPatternTokens ppe))
: hashPatternTokens ppe k <> (ps >>= hashPatternTokens ppe)
Pattern.SequenceLiteral _ ps -> H.Tag 12 : hashLengthToken ps : (ps >>= hashPatternTokens ppe)
Pattern.SequenceOp _ p op q -> H.Tag 16 : top op : (hashPatternTokens ppe p <> hashPatternTokens ppe q)
Pattern.SequenceOp _ p op q -> H.Tag 16 : top op : hashPatternTokens ppe p <> hashPatternTokens ppe q
where
top = \case
Pattern.Concat -> H.Tag 0
Pattern.Snoc -> H.Tag 1
Pattern.Cons -> H.Tag 2
hashTermTokens :: forall v a. Var v => PrettyPrintEnv -> Term v a -> [Token]
hashTermTokens ppe = go
where
ft :: Term.F v a a () -> [Token]
ft = \case
Term.Int n -> [H.Tag 0, H.Int n]
Term.Nat n -> [H.Tag 1, H.Nat n]
Term.Float n -> [H.Tag 2, H.Double n]
Term.Boolean b -> [H.Tag 3, if b then H.Tag 0 else H.Tag 1]
Term.Text t -> [H.Tag 4, H.Text t]
Term.Char c -> [H.Tag 5, H.Nat (fromIntegral (ord c))]
Term.Blank {} -> error "tried to hash a term with blanks, something's very wrong"
-- note: these are all hashed the same, just based on the name
Term.Ref r -> [H.Tag 7, hashReferentToken ppe (V1.Referent.Ref r)]
Term.Constructor cr -> [H.Tag 7, hashReferentToken ppe (V1.Referent.Con cr CT.Data)]
Term.Request cr -> [H.Tag 7, hashReferentToken ppe (V1.Referent.Con cr CT.Effect)]
Term.Handle {} -> [H.Tag 8]
Term.App {} -> [H.Tag 9]
Term.Ann _ ty -> H.Tag 10 : hashTypeTokens ppe ty
Term.List xs -> [H.Tag 11, hashLengthToken xs]
Term.If {} -> [H.Tag 12]
Term.And {} -> [H.Tag 13]
Term.Or {} -> [H.Tag 14]
Term.Lam {} -> [H.Tag 15]
Term.LetRec _ bs _ -> [H.Tag 16, hashLengthToken bs]
Term.Let {} -> [H.Tag 17]
Term.Match _scrute cases ->
H.Tag 18 : hashLengthToken cases : (cases >>= hashCaseTokens ppe)
Term.TermLink rf -> [H.Tag 19, hashReferentToken ppe rf]
Term.TypeLink r -> [H.Tag 20, hashTypeReferenceToken ppe r]
go :: Term v a -> [Token]
go t =
H.Tag 255 : case ABT.out t of
ABT.Var v -> [H.Tag 0, H.Text (Var.name v)]
-- trick: encode the structure, followed the children as a flat list
ABT.Tm f -> H.Tag 1 : (ft (void f) <> (toList f >>= go))
ABT.Cycle c -> H.Tag 2 : go c
ABT.Abs v body -> H.Tag 3 : H.Text (Var.name v) : go body
hashLengthToken :: Foldable t => t a -> Token
hashLengthToken =
H.Nat . fromIntegral @Int @Word64 . length
hashReferentToken :: PrettyPrintEnv -> V1.Referent -> Token
hashReferentToken ppe =
H.Hashed . H.accumulate . hashReferentTokens ppe
hashReferentTokens :: PrettyPrintEnv -> V1.Referent -> [Token]
hashReferentTokens ppe referent = case referent of
-- Concern
--
-- What if the decl is declared in two places of the namespace and
-- the PPE picks the decl from one but a constructor from the
-- other?
V1.Referent.Con (ConstructorReference ref _i) _ct ->
let declName = HQ.toTextWith Name.toText (PPE.typeNameOrHashOnlyFq ppe ref)
conName =
let cname = HQ.toTextWith Name.toText (referentName referent)
in case Text.stripPrefix declName cname of
Nothing -> error "[hashReferentTokens] Precondition violation: constructor name not under decl name"
Just x -> x
declTok = hashTypeReferenceToken ppe ref
conTok = H.Text conName
in [declTok, conTok]
V1.Referent.Ref _ -> [nameToToken (referentName referent)]
hashReferentTokens ppe referent =
case referent of
-- distinguish constructor name from terms by tumbling in a name (of any alias of) its decl
V1.Referent.Con (ConstructorReference ref _i) _ct -> [hashTypeReferenceToken ppe ref, nameTok]
V1.Referent.Ref _ -> [nameTok]
where
referentName = PPE.termNameOrHashOnlyFq ppe
nameToToken = H.Text . HQ.toTextWith Name.toText
nameTok :: Token
nameTok =
hashHQNameToken (PPE.termNameOrHashOnlyFq ppe referent)
-- | Syntactically hash a term, using reference names rather than hashes.
-- Two terms will have the same syntactic hash if they would
-- print the the same way under the given pretty-print env.
hashTerm :: forall m v a. (Monad m, Var v) => (TypeReferenceId -> m (Term v a)) -> PrettyPrintEnv -> V1.Referent -> m Hash
hashTerm loadTerm ppe = \case
V1.Referent.Con ref CT.Data -> pure (hashDerivedTerm ppe (Term.constructor @v () ref))
V1.Referent.Con ref CT.Effect -> pure (hashDerivedTerm ppe (Term.request @v () ref))
V1.Referent.Ref (ReferenceBuiltin builtin) -> pure (hashBuiltinTerm builtin)
V1.Referent.Ref (ReferenceDerived ref) -> hashDerivedTerm ppe <$> loadTerm ref
hashTermTokens :: forall v a. Var v => PrettyPrintEnv -> Term v a -> [Token]
hashTermTokens ppe =
go
where
go :: Term v a -> [Token]
go t =
H.Tag 255 : case ABT.out t of
ABT.Var v -> [H.Tag 0, hashVarToken v]
-- trick: encode the structure, followed the children as a flat list
ABT.Tm f -> H.Tag 1 : hashTermFTokens ppe (void f) <> (toList f >>= go)
ABT.Cycle c -> H.Tag 2 : go c
ABT.Abs v body -> H.Tag 3 : hashVarToken v : go body
hashTermFTokens :: Var v => PrettyPrintEnv -> Term.F v a a () -> [Token]
hashTermFTokens ppe = \case
Term.Int n -> [H.Tag 0, H.Int n]
Term.Nat n -> [H.Tag 1, H.Nat n]
Term.Float n -> [H.Tag 2, H.Double n]
Term.Boolean b -> [H.Tag 3, if b then H.Tag 0 else H.Tag 1]
Term.Text t -> [H.Tag 4, H.Text t]
Term.Char c -> [H.Tag 5, H.Nat (fromIntegral (ord c))]
Term.Blank {} -> error "tried to hash a term with blanks, something's very wrong"
-- note: these are all hashed the same, just based on the name
Term.Ref r -> [H.Tag 7, hashReferentToken ppe (V1.Referent.Ref r)]
Term.Constructor cr -> [H.Tag 7, hashReferentToken ppe (V1.Referent.Con cr CT.Data)]
Term.Request cr -> [H.Tag 7, hashReferentToken ppe (V1.Referent.Con cr CT.Effect)]
Term.Handle {} -> [H.Tag 8]
Term.App {} -> [H.Tag 9]
Term.Ann _ ty -> H.Tag 10 : hashTypeTokens ppe ty
Term.List xs -> [H.Tag 11, hashLengthToken xs]
Term.If {} -> [H.Tag 12]
Term.And {} -> [H.Tag 13]
Term.Or {} -> [H.Tag 14]
Term.Lam {} -> [H.Tag 15]
Term.LetRec _ bs _ -> [H.Tag 16, hashLengthToken bs]
Term.Let {} -> [H.Tag 17]
Term.Match _scrute cases ->
H.Tag 18 : hashLengthToken cases : (cases >>= hashCaseTokens ppe)
Term.TermLink rf -> [H.Tag 19, hashReferentToken ppe rf]
Term.TypeLink r -> [H.Tag 20, hashTypeReferenceToken ppe r]
-- | Syntactically hash a type, using reference names rather than hashes.
-- Two types will have the same syntactic hash if they would
-- print the the same way under the given pretty-print env.
hashType :: Var v => PrettyPrintEnv -> Type v a -> Hash
hashType ppe t =
H.accumulate $ hashTypeTokens ppe t
hashTypeTokens :: forall v a. Var v => PrettyPrintEnv -> Type v a -> [Token]
hashTypeTokens ppe = go
where
go :: Type v a -> [Token]
go t =
H.Tag 254 : case ABT.out t of
ABT.Var v -> [H.Tag 0, hashVarToken v]
-- trick: encode the structure, followed the children as a flat list
ABT.Tm f -> H.Tag 1 : (hashTypeFTokens ppe (void f) <> (toList f >>= go))
ABT.Cycle c -> H.Tag 2 : go c
ABT.Abs v body -> H.Tag 3 : hashVarToken v : go body
hashTypeFTokens :: PrettyPrintEnv -> Type.F () -> [Token]
hashTypeFTokens ppe = \case
Type.Ref r -> [H.Tag 0, hashTypeReferenceToken ppe r]
Type.Arrow {} -> [H.Tag 1]
Type.Ann _ k -> H.Tag 2 : hashKindTokens k
Type.App {} -> [H.Tag 3]
Type.Effect {} -> [H.Tag 4]
Type.Effects es -> [H.Tag 5, hashLengthToken es]
Type.Forall {} -> [H.Tag 6]
Type.IntroOuter {} -> [H.Tag 7]
hashTypeReferenceToken :: PrettyPrintEnv -> TypeReference -> Token
hashTypeReferenceToken ppe =
H.Text . HQ.toTextWith Name.toText . PPE.typeNameOrHashOnlyFq ppe
hashHQNameToken . PPE.typeNameOrHashOnlyFq ppe
hashVarToken :: Var v => v -> Token
hashVarToken =
H.Text . Var.name

View File

@ -12,7 +12,11 @@ data ThreeWay a = ThreeWay
alice :: !a,
bob :: !a
}
deriving stock (Functor, Generic)
deriving stock (Foldable, Functor, Generic, Traversable)
instance Applicative ThreeWay where
pure x = ThreeWay x x x
ThreeWay f g h <*> ThreeWay x y z = ThreeWay (f x) (g y) (h z)
forgetLca :: ThreeWay a -> TwoWay a
forgetLca ThreeWay {alice, bob} =