mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
relax merge preconditions on lca
This commit is contained in:
parent
52283ed3f7
commit
32cde2cd35
@ -43,7 +43,7 @@ import U.Codebase.Sqlite.Project (Project (..))
|
||||
import U.Codebase.Sqlite.ProjectBranch (ProjectBranch (..))
|
||||
import U.Codebase.Sqlite.Queries qualified as Queries
|
||||
import Unison.Builtin.Decls qualified as Builtin.Decls
|
||||
import Unison.Cli.MergeTypes (MergeSource (..), MergeSourceOrTarget (..), MergeSourceAndTarget (..))
|
||||
import Unison.Cli.MergeTypes (MergeSource (..), MergeSourceAndTarget (..), MergeSourceOrTarget (..))
|
||||
import Unison.Cli.Monad (Cli)
|
||||
import Unison.Cli.Monad qualified as Cli
|
||||
import Unison.Cli.MonadUtils qualified as Cli
|
||||
@ -76,7 +76,7 @@ import Unison.HashQualified qualified as HQ
|
||||
import Unison.HashQualified' qualified as HQ'
|
||||
import Unison.Merge.CombineDiffs (CombinedDiffOp (..), combineDiffs)
|
||||
import Unison.Merge.Database (MergeDatabase (..), makeMergeDatabase, referent2to1)
|
||||
import Unison.Merge.DeclCoherencyCheck (IncoherentDeclReason (..), checkDeclCoherency)
|
||||
import Unison.Merge.DeclCoherencyCheck (IncoherentDeclReason (..), checkDeclCoherency, lenientCheckDeclCoherency)
|
||||
import Unison.Merge.DeclNameLookup (DeclNameLookup (..), expectConstructorNames)
|
||||
import Unison.Merge.Diff qualified as Merge
|
||||
import Unison.Merge.DiffOp (DiffOp (..))
|
||||
@ -220,7 +220,7 @@ doMerge info = do
|
||||
let aliceBranchNames = ProjectAndBranch info.alice.project.name info.alice.projectBranch.name
|
||||
let mergeSource = MergeSourceOrTarget'Source info.bob.source
|
||||
let mergeTarget = MergeSourceOrTarget'Target aliceBranchNames
|
||||
let mergeSourceAndTarget = MergeSourceAndTarget { alice = aliceBranchNames, bob = info.bob.source }
|
||||
let mergeSourceAndTarget = MergeSourceAndTarget {alice = aliceBranchNames, bob = info.bob.source}
|
||||
|
||||
Cli.Env {codebase} <- ask
|
||||
|
||||
@ -267,19 +267,17 @@ doMerge info = do
|
||||
Cli.returnEarly (Output.MergeDefnsInLib who)
|
||||
|
||||
-- Load Alice/Bob/LCA definitions and decl name lookups
|
||||
(defns3, declNameLookups3) <- do
|
||||
(defns3, declNameLookups, lcaDeclToConstructors) <- do
|
||||
let emptyNametree = Nametree {value = Defns Map.empty Map.empty, children = Map.empty}
|
||||
let loadDefns branch =
|
||||
Cli.runTransaction (loadNamespaceDefinitions (referent2to1 db) branch) & onLeftM \conflictedName ->
|
||||
Cli.returnEarly case conflictedName of
|
||||
ConflictedName'Term name refs -> Output.MergeConflictedTermName name refs
|
||||
ConflictedName'Type name refs -> Output.MergeConflictedTypeName name refs
|
||||
let load = \case
|
||||
Nothing ->
|
||||
pure
|
||||
( Nametree {value = Defns Map.empty Map.empty, children = Map.empty},
|
||||
DeclNameLookup Map.empty Map.empty
|
||||
)
|
||||
Nothing -> pure (emptyNametree, DeclNameLookup Map.empty Map.empty)
|
||||
Just (who, branch) -> do
|
||||
defns <-
|
||||
Cli.runTransaction (loadNamespaceDefinitions (referent2to1 db) branch) & onLeftM \conflictedName ->
|
||||
Cli.returnEarly case conflictedName of
|
||||
ConflictedName'Term name refs -> Output.MergeConflictedTermName name refs
|
||||
ConflictedName'Type name refs -> Output.MergeConflictedTypeName name refs
|
||||
defns <- loadDefns branch
|
||||
declNameLookup <-
|
||||
Cli.runTransaction (checkDeclCoherency db.loadDeclNumConstructors defns) & onLeftM \err ->
|
||||
Cli.returnEarly case err of
|
||||
@ -291,23 +289,23 @@ doMerge info = do
|
||||
IncoherentDeclReason'StrayConstructor name -> Output.MergeStrayConstructor who name
|
||||
pure (defns, declNameLookup)
|
||||
|
||||
(aliceDefns0, aliceDeclNameLookup) <- load (Just (Just mergeTarget, branches.alice))
|
||||
(bobDefns0, bobDeclNameLookup) <- load (Just (Just mergeSource, branches.bob))
|
||||
(lcaDefns0, lcaDeclNameLookup) <- load ((Nothing,) <$> branches.lca)
|
||||
(aliceDefns0, aliceDeclNameLookup) <- load (Just (mergeTarget, branches.alice))
|
||||
(bobDefns0, bobDeclNameLookup) <- load (Just (mergeSource, branches.bob))
|
||||
lcaDefns0 <- maybe (pure emptyNametree) loadDefns branches.lca
|
||||
lcaDeclToConstructors <- Cli.runTransaction (lenientCheckDeclCoherency db.loadDeclNumConstructors lcaDefns0)
|
||||
|
||||
let flatten defns = Defns (flattenNametree (view #terms) defns) (flattenNametree (view #types) defns)
|
||||
let defns3 = flatten <$> ThreeWay {alice = aliceDefns0, bob = bobDefns0, lca = lcaDefns0}
|
||||
let declNameLookups3 = ThreeWay {alice = aliceDeclNameLookup, bob = bobDeclNameLookup, lca = lcaDeclNameLookup}
|
||||
let declNameLookups = TwoWay {alice = aliceDeclNameLookup, bob = bobDeclNameLookup}
|
||||
|
||||
pure (defns3, declNameLookups3)
|
||||
pure (defns3, declNameLookups, lcaDeclToConstructors)
|
||||
|
||||
let defns = ThreeWay.forgetLca defns3
|
||||
let declNameLookups = ThreeWay.forgetLca declNameLookups3
|
||||
|
||||
liftIO (debugFunctions.debugDefns defns3 declNameLookups3)
|
||||
liftIO (debugFunctions.debugDefns defns3 declNameLookups lcaDeclToConstructors)
|
||||
|
||||
-- Diff LCA->Alice and LCA->Bob
|
||||
diffs <- Cli.runTransaction (Merge.nameBasedNamespaceDiff db declNameLookups3 defns3)
|
||||
diffs <- Cli.runTransaction (Merge.nameBasedNamespaceDiff db declNameLookups lcaDeclToConstructors defns3)
|
||||
|
||||
liftIO (debugFunctions.debugDiffs diffs)
|
||||
|
||||
@ -1032,7 +1030,8 @@ data DebugFunctions = DebugFunctions
|
||||
{ debugCausals :: TwoOrThreeWay (V2.CausalBranch Transaction) -> IO (),
|
||||
debugDefns ::
|
||||
ThreeWay (Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name)) ->
|
||||
ThreeWay DeclNameLookup ->
|
||||
TwoWay DeclNameLookup ->
|
||||
Map Name [Maybe Name] ->
|
||||
IO (),
|
||||
debugDiffs :: TwoWay (DefnsF3 (Map Name) DiffOp Synhashed Referent TypeReference) -> IO (),
|
||||
debugCombinedDiff :: DefnsF2 (Map Name) CombinedDiffOp Referent TypeReference -> IO (),
|
||||
@ -1073,9 +1072,10 @@ realDebugCausals causals = do
|
||||
|
||||
realDebugDefns ::
|
||||
ThreeWay (Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name)) ->
|
||||
ThreeWay DeclNameLookup ->
|
||||
TwoWay DeclNameLookup ->
|
||||
Map Name [Maybe Name] ->
|
||||
IO ()
|
||||
realDebugDefns defns declNameLookups = do
|
||||
realDebugDefns defns declNameLookups _lcaDeclNameLookup = do
|
||||
Text.putStrLn (Text.bold "\n=== Alice definitions ===")
|
||||
debugDefns1 (bimap BiMultimap.range BiMultimap.range defns.alice)
|
||||
|
||||
|
@ -395,11 +395,11 @@ data Output
|
||||
| MergeConflictedTermName !Name !(NESet Referent)
|
||||
| MergeConflictedTypeName !Name !(NESet TypeReference)
|
||||
| MergeConflictInvolvingBuiltin !Name
|
||||
| MergeConstructorAlias !(Maybe MergeSourceOrTarget) !Name !Name
|
||||
| MergeConstructorAlias !MergeSourceOrTarget !Name !Name
|
||||
| MergeDefnsInLib !MergeSourceOrTarget
|
||||
| MergeMissingConstructorName !(Maybe MergeSourceOrTarget) !Name
|
||||
| MergeNestedDeclAlias !(Maybe MergeSourceOrTarget) !Name !Name
|
||||
| MergeStrayConstructor !(Maybe MergeSourceOrTarget) !Name
|
||||
| MergeMissingConstructorName !MergeSourceOrTarget !Name
|
||||
| MergeNestedDeclAlias !MergeSourceOrTarget !Name !Name
|
||||
| MergeStrayConstructor !MergeSourceOrTarget !Name
|
||||
| InstalledLibdep !(ProjectAndBranch ProjectName ProjectBranchName) !NameSegment
|
||||
|
||||
data UpdateOrUpgrade = UOUUpdate | UOUUpgrade
|
||||
|
@ -1488,12 +1488,10 @@ 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 maybeAliceOrBob name1 name2 ->
|
||||
MergeConstructorAlias aliceOrBob name1 name2 ->
|
||||
pure . P.wrap $
|
||||
"On"
|
||||
<> case maybeAliceOrBob of
|
||||
Nothing -> "the LCA,"
|
||||
Just aliceOrBob -> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> prettyName name1
|
||||
<> "and"
|
||||
<> prettyName name2
|
||||
@ -1504,32 +1502,26 @@ notifyUser dir = \case
|
||||
<> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> "there's a type or term directly in the `lib` namespace, but I expected only library dependencies to be in there."
|
||||
<> "Please remove it before merging."
|
||||
MergeMissingConstructorName maybeAliceOrBob name ->
|
||||
MergeMissingConstructorName aliceOrBob name ->
|
||||
pure . P.wrap $
|
||||
"On"
|
||||
<> case maybeAliceOrBob of
|
||||
Nothing -> "the LCA,"
|
||||
Just aliceOrBob -> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> "the type"
|
||||
<> prettyName name
|
||||
<> "is missing a name for one of its constructors. Please add one before merging."
|
||||
MergeNestedDeclAlias maybeAliceOrBob shorterName longerName ->
|
||||
MergeNestedDeclAlias aliceOrBob shorterName longerName ->
|
||||
pure . P.wrap $
|
||||
"On"
|
||||
<> case maybeAliceOrBob of
|
||||
Nothing -> "the LCA,"
|
||||
Just aliceOrBob -> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> "the type"
|
||||
<> prettyName longerName
|
||||
<> "is an alias of"
|
||||
<> P.group (prettyName shorterName <> ".")
|
||||
<> "Type aliases cannot be nested. Please make them disjoint before merging."
|
||||
MergeStrayConstructor maybeAliceOrBob name ->
|
||||
MergeStrayConstructor aliceOrBob name ->
|
||||
pure . P.wrap $
|
||||
"On"
|
||||
<> case maybeAliceOrBob of
|
||||
Nothing -> "the LCA,"
|
||||
Just aliceOrBob -> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> P.group (prettyMergeSourceOrTarget aliceOrBob <> ",")
|
||||
<> "the constructor"
|
||||
<> prettyName name
|
||||
<> "is not in a subnamespace of a name of its type."
|
||||
|
@ -33,10 +33,11 @@ module Unison.DataDeclaration
|
||||
constructors_,
|
||||
asDataDecl_,
|
||||
declAsDataDecl_,
|
||||
setConstructorNames,
|
||||
)
|
||||
where
|
||||
|
||||
import Control.Lens (Iso', Lens', imap, iso, lens, over, _3)
|
||||
import Control.Lens (Iso', Lens', imap, iso, lens, over, set, _2, _3)
|
||||
import Control.Monad.State (evalState)
|
||||
import Data.Map qualified as Map
|
||||
import Data.Set qualified as Set
|
||||
@ -164,6 +165,20 @@ constructorVars dd = fst <$> constructors dd
|
||||
constructorNames :: (Var v) => DataDeclaration v a -> [Text]
|
||||
constructorNames dd = Var.name <$> constructorVars dd
|
||||
|
||||
-- | Overwrite the constructor names with the given list, given in canonical order, which is assumed to be of the
|
||||
-- correct length.
|
||||
--
|
||||
-- Presumably this is called because the decl was loaded from the database outside of the context of a namespace,
|
||||
-- since it's not stored with names there, so we had plugged in dummy names like "Constructor1", "Constructor2", ...
|
||||
--
|
||||
-- Then, at some point, we discover the constructors' names in a namespace, and now we'd like to combine the two
|
||||
-- together to get a Decl structure in memory with good/correct names for constructors.
|
||||
setConstructorNames :: [v] -> Decl v a -> Decl v a
|
||||
setConstructorNames constructorNames =
|
||||
over
|
||||
(declAsDataDecl_ . constructors_)
|
||||
(zipWith (set _2) constructorNames)
|
||||
|
||||
-- This function is unsound, since the `rid` and the `decl` have to match.
|
||||
-- It should probably be hashed directly from the Decl, once we have a
|
||||
-- reliable way of doing that. —AI
|
||||
|
@ -217,6 +217,12 @@ checkDeclCoherency loadDeclNumConstructors =
|
||||
fullName name =
|
||||
Name.fromReverseSegments (name :| prefix)
|
||||
|
||||
-- | A lenient variant of 'checkDeclCoherency' - so lenient it can't even fail! It returns a mapping from decl name to
|
||||
-- constructor names, where constructor names can be missing.
|
||||
--
|
||||
-- This function exists merely to extract a best-effort decl-name-to-constructor-name mapping for the LCA of a merge.
|
||||
-- We require Alice and Bob to have coherent decls, but their LCA is out of the user's control and may have incoherent
|
||||
-- decls, and whether or not it does, we still need to compute *some* syntactic hash for its decls.
|
||||
lenientCheckDeclCoherency ::
|
||||
forall m.
|
||||
Monad m =>
|
||||
|
@ -2,24 +2,13 @@ module Unison.Merge.DeclNameLookup
|
||||
( DeclNameLookup (..),
|
||||
expectDeclName,
|
||||
expectConstructorNames,
|
||||
setConstructorNames,
|
||||
)
|
||||
where
|
||||
|
||||
import Control.Lens (over)
|
||||
import Data.Map.Strict qualified as Map
|
||||
import Data.Semigroup.Generic (GenericSemigroupMonoid (..))
|
||||
import Unison.DataDeclaration (Decl)
|
||||
import Unison.DataDeclaration qualified as DataDeclaration
|
||||
import Unison.Name (Name)
|
||||
import Unison.NameSegment (NameSegment)
|
||||
import Unison.Prelude
|
||||
import Unison.Reference (TypeReference)
|
||||
import Unison.Referent (Referent)
|
||||
import Unison.Syntax.Name qualified as Name
|
||||
import Unison.Util.Defns (Defns (..), DefnsF)
|
||||
import Unison.Util.Nametree (Nametree (..))
|
||||
import Unison.Var (Var)
|
||||
|
||||
-- | A lookup from decl-to-constructor name and vice-versa.
|
||||
--
|
||||
@ -62,22 +51,3 @@ expectConstructorNames DeclNameLookup {declToConstructors} x =
|
||||
case Map.lookup x declToConstructors of
|
||||
Nothing -> error (reportBug "E077058" ("Expected decl name key " <> show x <> " in decl name lookup"))
|
||||
Just y -> y
|
||||
|
||||
-- | Set the constructor names of a data declaration.
|
||||
--
|
||||
-- Presumably this is used because the decl was loaded from the database outside of the context of a namespace, because
|
||||
-- it's not stored with names there, so we plugged in dummy names like "Constructor1", "Constructor2", ...
|
||||
--
|
||||
-- Then, at some point, a `DeclNameLookup` was constructed for the corresponding namespace, and now we'd like to
|
||||
-- combine the two together to get a Decl structure in memory with good/correct names for constructors.
|
||||
setConstructorNames :: forall a v. Var v => DeclNameLookup -> Name -> Decl v a -> Decl v a
|
||||
setConstructorNames declNameLookup name =
|
||||
case Map.lookup name declNameLookup.declToConstructors of
|
||||
Nothing -> id
|
||||
Just constructorNames ->
|
||||
over
|
||||
(DataDeclaration.declAsDataDecl_ . DataDeclaration.constructors_)
|
||||
( zipWith
|
||||
(\realConName (ann, _junkConName, typ) -> (ann, Name.toVar realConName, typ))
|
||||
constructorNames
|
||||
)
|
||||
|
@ -9,23 +9,30 @@ import Data.Semialign (alignWith)
|
||||
import Data.Set qualified as Set
|
||||
import Data.These (These (..))
|
||||
import U.Codebase.Reference (TypeReference)
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.DataDeclaration (Decl)
|
||||
import Unison.DataDeclaration qualified as DataDeclaration
|
||||
import Unison.Hash (Hash (Hash))
|
||||
import Unison.HashQualified' qualified as HQ'
|
||||
import Unison.Merge.Database (MergeDatabase (..))
|
||||
import Unison.Merge.DeclNameLookup (DeclNameLookup)
|
||||
import Unison.Merge.DeclNameLookup qualified as DeclNameLookup
|
||||
import Unison.Merge.DiffOp (DiffOp (..))
|
||||
import Unison.Merge.Synhash qualified as Synhash
|
||||
import Unison.Merge.Synhash
|
||||
import Unison.Merge.Synhashed (Synhashed (..))
|
||||
import Unison.Merge.ThreeWay (ThreeWay (..))
|
||||
import Unison.Merge.ThreeWay qualified as ThreeWay
|
||||
import Unison.Merge.TwoWay (TwoWay (..))
|
||||
import Unison.Merge.Updated (Updated (..))
|
||||
import Unison.Name (Name)
|
||||
import Unison.Parser.Ann (Ann)
|
||||
import Unison.Prelude hiding (catMaybes)
|
||||
import Unison.PrettyPrintEnv (PrettyPrintEnv (..))
|
||||
import Unison.PrettyPrintEnv qualified as Ppe
|
||||
import Unison.Reference (Reference' (..), TypeReferenceId)
|
||||
import Unison.Referent (Referent)
|
||||
import Unison.Sqlite (Transaction)
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Syntax.Name qualified as Name
|
||||
import Unison.Util.BiMultimap (BiMultimap)
|
||||
import Unison.Util.BiMultimap qualified as BiMultimap
|
||||
import Unison.Util.Defns (Defns (..), DefnsF2, DefnsF3, zipDefnsWith)
|
||||
@ -40,12 +47,29 @@ import Unison.Util.Defns (Defns (..), DefnsF2, DefnsF3, zipDefnsWith)
|
||||
-- branches. If the hash of a name did not change, it will not appear in the map.
|
||||
nameBasedNamespaceDiff ::
|
||||
MergeDatabase ->
|
||||
ThreeWay DeclNameLookup ->
|
||||
TwoWay DeclNameLookup ->
|
||||
Map Name [Maybe Name] ->
|
||||
ThreeWay (Defns (BiMultimap Referent Name) (BiMultimap TypeReference Name)) ->
|
||||
Transaction (TwoWay (DefnsF3 (Map Name) DiffOp Synhashed Referent TypeReference))
|
||||
nameBasedNamespaceDiff db declNameLookups defns = do
|
||||
diffs <- sequence (synhashDefns <$> declNameLookups <*> defns)
|
||||
pure (diffNamespaceDefns diffs.lca <$> TwoWay {alice = diffs.alice, bob = diffs.bob})
|
||||
nameBasedNamespaceDiff db declNameLookups lcaDeclToConstructors defns = do
|
||||
lcaHashes <-
|
||||
synhashDefnsWith
|
||||
hashTerm
|
||||
( \name -> \case
|
||||
ReferenceBuiltin builtin -> pure (synhashBuiltinDecl builtin)
|
||||
ReferenceDerived ref ->
|
||||
case sequence (lcaDeclToConstructors Map.! name) of
|
||||
-- If we don't have a name for every constructor, that's okay, just use a dummy syntactic hash here.
|
||||
-- This is safe; Alice/Bob can't have such a decl (it violates a merge precondition), so there's no risk
|
||||
-- that we accidentally get an equal hash and classify a real update as unchanged.
|
||||
Nothing -> pure (Hash mempty)
|
||||
Just names -> do
|
||||
decl <- loadDeclWithGoodConstructorNames names ref
|
||||
pure (synhashDerivedDecl ppe name decl)
|
||||
)
|
||||
defns.lca
|
||||
hashes <- sequence (synhashDefns <$> declNameLookups <*> ThreeWay.forgetLca defns)
|
||||
pure (diffNamespaceDefns lcaHashes <$> hashes)
|
||||
where
|
||||
synhashDefns ::
|
||||
DeclNameLookup ->
|
||||
@ -55,16 +79,20 @@ nameBasedNamespaceDiff db declNameLookups defns = do
|
||||
-- FIXME: use cache so we only synhash each thing once
|
||||
synhashDefnsWith hashTerm hashType
|
||||
where
|
||||
hashTerm :: Referent -> Transaction Hash
|
||||
hashTerm =
|
||||
Synhash.hashTerm db.loadV1Term ppe
|
||||
|
||||
hashType :: Name -> TypeReference -> Transaction Hash
|
||||
hashType name =
|
||||
Synhash.hashDecl
|
||||
(fmap (DeclNameLookup.setConstructorNames declNameLookup name) . db.loadV1Decl)
|
||||
ppe
|
||||
name
|
||||
hashType name = \case
|
||||
ReferenceBuiltin builtin -> pure (synhashBuiltinDecl builtin)
|
||||
ReferenceDerived ref -> do
|
||||
decl <- loadDeclWithGoodConstructorNames (DeclNameLookup.expectConstructorNames declNameLookup name) ref
|
||||
pure (synhashDerivedDecl ppe name decl)
|
||||
|
||||
loadDeclWithGoodConstructorNames :: [Name] -> TypeReferenceId -> Transaction (Decl Symbol Ann)
|
||||
loadDeclWithGoodConstructorNames names =
|
||||
fmap (DataDeclaration.setConstructorNames (map Name.toVar names)) . db.loadV1Decl
|
||||
|
||||
hashTerm :: Referent -> Transaction Hash
|
||||
hashTerm =
|
||||
synhashTerm db.loadV1Term ppe
|
||||
|
||||
ppe :: PrettyPrintEnv
|
||||
ppe =
|
||||
|
@ -24,9 +24,10 @@
|
||||
-- "foo" would have the same syntactic hash. This indicates (to our merge algorithm) that this was an auto-propagated
|
||||
-- update.
|
||||
module Unison.Merge.Synhash
|
||||
( hashType,
|
||||
hashTerm,
|
||||
hashDecl,
|
||||
( synhashType,
|
||||
synhashTerm,
|
||||
synhashBuiltinDecl,
|
||||
synhashDerivedDecl,
|
||||
)
|
||||
where
|
||||
|
||||
@ -72,8 +73,8 @@ isDeclTag, isTermTag :: H.Token Hash
|
||||
isDeclTag = H.Tag 0
|
||||
isTermTag = H.Tag 1
|
||||
|
||||
hashBuiltinDecl :: Text -> Hash
|
||||
hashBuiltinDecl name =
|
||||
synhashBuiltinDecl :: Text -> Hash
|
||||
synhashBuiltinDecl name =
|
||||
H.accumulate [isBuiltinTag, isDeclTag, H.Text name]
|
||||
|
||||
hashBuiltinTerm :: Text -> Hash
|
||||
@ -104,23 +105,6 @@ hashConstructorNameToken declName conName =
|
||||
)
|
||||
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 name = \case
|
||||
ReferenceBuiltin builtin -> pure (hashBuiltinDecl builtin)
|
||||
ReferenceDerived ref -> do
|
||||
decl <- loadDecl ref
|
||||
pure (hashDerivedDecl ppe name decl)
|
||||
|
||||
hashDerivedTerm :: Var v => PrettyPrintEnv -> Term v a -> Hash
|
||||
hashDerivedTerm ppe t =
|
||||
H.accumulate $ isNotBuiltinTag : hashTermTokens ppe t
|
||||
@ -148,8 +132,12 @@ 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 =
|
||||
-- | 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.
|
||||
synhashDerivedDecl :: Var v => PrettyPrintEnv -> Name -> Decl v a -> Hash
|
||||
synhashDerivedDecl ppe name decl =
|
||||
H.accumulate $ isNotBuiltinTag : hashDeclTokens ppe name decl
|
||||
|
||||
hashHQNameToken :: HashQualified Name -> Token
|
||||
@ -218,8 +206,14 @@ hashReferentTokens 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
|
||||
synhashTerm ::
|
||||
forall m v a.
|
||||
(Monad m, Var v) =>
|
||||
(TypeReferenceId -> m (Term v a)) ->
|
||||
PrettyPrintEnv ->
|
||||
V1.Referent ->
|
||||
m Hash
|
||||
synhashTerm 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)
|
||||
@ -269,8 +263,8 @@ hashTermFTokens ppe = \case
|
||||
-- | 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 =
|
||||
synhashType :: Var v => PrettyPrintEnv -> Type v a -> Hash
|
||||
synhashType ppe t =
|
||||
H.accumulate $ hashTypeTokens ppe t
|
||||
|
||||
hashTypeTokens :: forall v a. Var v => PrettyPrintEnv -> Type v a -> [Token]
|
||||
|
@ -1300,3 +1300,70 @@ project/alice> merge /bob
|
||||
```ucm:hide
|
||||
.> project.delete project
|
||||
```
|
||||
|
||||
## LCA precondition violations
|
||||
|
||||
The LCA is not subject to most precondition violations, which is good, because the user can't easily manipulate it!
|
||||
|
||||
Here's an example. We'll delete a constructor name from the LCA and still be able to merge Alice and Bob's stuff
|
||||
together.
|
||||
|
||||
```ucm:hide
|
||||
.> project.create-empty project
|
||||
project/main> builtins.mergeio
|
||||
```
|
||||
|
||||
LCA:
|
||||
|
||||
```unison
|
||||
structural type Foo = Bar Nat | Baz Nat Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
project/main> add
|
||||
project/main> delete.term Foo.Baz
|
||||
```
|
||||
|
||||
Alice's branch:
|
||||
|
||||
```ucm
|
||||
project/main> branch alice
|
||||
project/alice> delete.type Foo
|
||||
project/alice> delete.term Foo.Bar
|
||||
```
|
||||
|
||||
```unison
|
||||
alice : Nat
|
||||
alice = 100
|
||||
```
|
||||
|
||||
```ucm
|
||||
project/alice> add
|
||||
```
|
||||
|
||||
Bob's branch:
|
||||
|
||||
```ucm
|
||||
project/main> branch bob
|
||||
project/bob> delete.type Foo
|
||||
project/bob> delete.term Foo.Bar
|
||||
```
|
||||
|
||||
```unison
|
||||
bob : Nat
|
||||
bob = 101
|
||||
```
|
||||
|
||||
```ucm
|
||||
project/bob> add
|
||||
```
|
||||
|
||||
Now we merge:
|
||||
|
||||
```ucm
|
||||
project/alice> merge /bob
|
||||
```
|
||||
|
||||
```ucm:hide
|
||||
.> project.delete project
|
||||
```
|
||||
|
@ -1144,3 +1144,139 @@ project/alice> merge /bob
|
||||
there. Please remove it before merging.
|
||||
|
||||
```
|
||||
## LCA precondition violations
|
||||
|
||||
The LCA is not subject to most precondition violations, which is good, because the user can't easily manipulate it!
|
||||
|
||||
Here's an example. We'll delete a constructor name from the LCA and still be able to merge Alice and Bob's stuff
|
||||
together.
|
||||
|
||||
LCA:
|
||||
|
||||
```unison
|
||||
structural type Foo = Bar Nat | Baz Nat Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
structural type Foo
|
||||
|
||||
```
|
||||
```ucm
|
||||
project/main> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
structural type Foo
|
||||
|
||||
project/main> delete.term Foo.Baz
|
||||
|
||||
Done.
|
||||
|
||||
```
|
||||
Alice's branch:
|
||||
|
||||
```ucm
|
||||
project/main> branch alice
|
||||
|
||||
Done. I've created the alice branch based off of main.
|
||||
|
||||
Tip: To merge your work back into the main branch, first
|
||||
`switch /main` then `merge /alice`.
|
||||
|
||||
project/alice> delete.type Foo
|
||||
|
||||
Done.
|
||||
|
||||
project/alice> delete.term Foo.Bar
|
||||
|
||||
Done.
|
||||
|
||||
```
|
||||
```unison
|
||||
alice : Nat
|
||||
alice = 100
|
||||
```
|
||||
|
||||
```ucm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
alice : Nat
|
||||
|
||||
```
|
||||
```ucm
|
||||
project/alice> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
alice : Nat
|
||||
|
||||
```
|
||||
Bob's branch:
|
||||
|
||||
```ucm
|
||||
project/main> branch bob
|
||||
|
||||
Done. I've created the bob branch based off of main.
|
||||
|
||||
Tip: To merge your work back into the main branch, first
|
||||
`switch /main` then `merge /bob`.
|
||||
|
||||
project/bob> delete.type Foo
|
||||
|
||||
Done.
|
||||
|
||||
project/bob> delete.term Foo.Bar
|
||||
|
||||
Done.
|
||||
|
||||
```
|
||||
```unison
|
||||
bob : Nat
|
||||
bob = 101
|
||||
```
|
||||
|
||||
```ucm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
bob : Nat
|
||||
|
||||
```
|
||||
```ucm
|
||||
project/bob> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
bob : Nat
|
||||
|
||||
```
|
||||
Now we merge:
|
||||
|
||||
```ucm
|
||||
project/alice> merge /bob
|
||||
|
||||
I merged project/bob into project/alice.
|
||||
|
||||
```
|
||||
|
Loading…
Reference in New Issue
Block a user