more progress on add command, handling ambiguity

This commit is contained in:
Paul Chiusano 2016-10-30 11:18:11 -04:00
parent 4ed3451dba
commit 5b8abcb9d0
3 changed files with 70 additions and 28 deletions

View File

@ -47,6 +47,9 @@ uc help
uc eval [name]
-}
view :: Codebase IO v Reference (Type v) (Term v) -> Term v -> String
view code e = "todo"
process :: (Show v, Var v) => IO (Codebase IO v Reference (Type v) (Term v)) -> [String] -> IO ()
process _ [] = putStrLn $ intercalate "\n"
[ "usage: uc <subcommand> [<args>]"
@ -90,30 +93,62 @@ process codebase ("add" : []) = do
putStr " "
putStrLn . Text.unpack . Text.intercalate "\n " $ ufiles
putStrLn "Supply one of these files as the argument to `uc add`"
process codebase ("add" : [name]) = do
codebase <- codebase
str <- readFile name
let ok = putStrLn "OK"
putStr $ "Parsing " ++ name ++ " ... "
bs <- case Parser.run TermParser.moduleBindings str TypeParser.s0 of
Parser.Fail err _ -> putStrLn " FAILED" >> mapM_ putStrLn err >> fail "parse failure"
Parser.Succeed bs _ _ -> pure bs
ok
putStr "Checking for name ambiguities ... "
let hooks = Codebase.Hooks ok before after False
before (v, _) = putStr $ "Typechecking " ++ show v ++ " ... "
after (_, _, h) = do ok; putStrLn $ "Added to codebase; definition has hash " ++ show h
baseName = stripu name -- todo - more robust file extension stripping
results <- Note.run $ Codebase.declareCheckAmbiguous hooks Term.ref bs codebase
case results of
Nothing -> do
Directory.removeFile (baseName `mappend` ".markdown") <|> pure ()
Directory.removeFile (baseName `mappend` ".u") <|> pure ()
hasParent <- (True <$ Directory.removeFile (baseName `mappend` ".parent")) <|> pure False
let suffix = if hasParent then ".{u, markdown, parent}" else ".{u, markdown}"
putStrLn $ "Removed files " ++ baseName ++ suffix
-- todo - if hasParent, ask if want to update usages
Just ambiguous -> error "todo"
process codebase ("add" : [name]) = go0 name False where
baseName = stripu name -- todo - more robust file extension stripping
go0 name allowShadowing = do
codebase <- codebase
str <- readFile name
putStr $ "Parsing " ++ name ++ " ... "
bs <- case Parser.run TermParser.moduleBindings str TypeParser.s0 of
Parser.Fail err _ -> putStrLn "FAILED" >> mapM_ putStrLn err >> fail "parse failure"
Parser.Succeed bs _ _ -> pure bs
putStrLn "OK"
putStr "Checking for name ambiguities ... "
go codebase name allowShadowing bs
go codebase name allowShadowing bs = do
let hooks' = Codebase.Hooks ok before after allowShadowing
ok = putStrLn "OK" >> putStrLn "Typechecking and adding definition(s) to codebase: "
before (v, _) = putStr $ " " ++ show v ++ " ... "
after (_, _, h) = do putStrLn $ "OK, added hash " ++ show h
results <- Note.run $ Codebase.declareCheckAmbiguous hooks' Term.ref bs codebase
case results of
Nothing -> do
Directory.removeFile (baseName `mappend` ".markdown") <|> pure ()
Directory.removeFile (baseName `mappend` ".u") <|> pure ()
hasParent <- (True <$ Directory.removeFile (baseName `mappend` ".parent")) <|> pure False
let suffix = if hasParent then ".{u, markdown, parent}" else ".{u, markdown}"
putStrLn $ "OK, removed files " ++ baseName ++ suffix
-- todo - if hasParent, ask if want to update usages
Just ambiguous -> putStrLn "FAILED" >> case ambiguous of
_ | all (\(v, tms) -> Term.var v `elem` tms) ambiguous -> do
putStrLn "Definition(s) have names that collide with existing hashes:\n "
mapM_ showAmbiguity ambiguous
putStrLn $ unlines
[ "", "You can:"
, "1) `rename <newname>` - rename the old definition"
, "2) `rename` - append first few characters of hash to old name"
, "3) `allow` the ambiguity - uses will need to disambiguate via hash"
, "4) `cancel` - exit without making changes" ]
putStr "> "
line <- Text.strip . Text.pack <$> getLine
case line of
_ | line == "rename" || line == "2" -> error "todo"
| "rename" `Text.isPrefixOf` line -> error "todo"
| line == "allow" || line == "3" -> go codebase name True bs -- todo: Bool not sufficient
| otherwise -> putStrLn "Cancelled"
-- three ways to handle ambiguous declarations - with a rename of old, with an error,
-- or just allowing collision (forcing dependents to disambiguate)
-- just make this a data type in Codebase
-- data HandleAmbiguity = FailIfAmbiguous | RenameOldIfAmbiguous | AllowIfAmbiguous
_ | otherwise -> error "todo"
where
putIndent s = putStrLn s >> putStr " "
showTerms tms = intercalate "," $ map show tms
showAmbiguity (v, tms)
| Term.var v `elem` tms =
putIndent $ show v ++ " has same name as " ++ showTerms (delete (Term.var v) tms)
| otherwise =
putIndent $ show v ++ " reference is ambiguous, multiple hashes with this name: " ++ showTerms tms
process codebase _ = process codebase []
stripu :: [a] -> [a]

View File

@ -291,7 +291,14 @@ data Hooks m v h =
Hooks { beforeAnyTypechecking :: m ()
, beforeTypechecking :: (v, Term v) -> m ()
, afterDeclaration :: (v, Term v, h) -> m ()
, allowShadowing :: Bool }
, handleShadowing :: Bool }
-- | Controls how situation is handled if name assigned to a new declaration
-- shadows an existing declaration
data HandleShadowing
= FailIfShadowed -- fails with an error
| RenameOldIfShadowed -- renames the old definition (appends first few hash characters)
| AllowShadowed -- allows the shadowing (users of that name will have to disambiguate via hash)
hooks0 :: Applicative m => Hooks m v h
hooks0 = Hooks (pure ()) (const $ pure ()) (const $ pure ()) True
@ -327,7 +334,7 @@ declareCheckAmbiguous hooks ref bindings code = do
go (v, hashPrefix) = (v, filter (startsWith hashPrefix) $ Map.findWithDefault [] v names)
shadowed = Set.toList $ Map.keysSet names `Set.intersection` (Set.fromList $ map fst bindings)
shadowedBindings = [ (name, Term.var name : b) | name <- shadowed, Just b <- [Map.lookup name names]]
isShadowed = not (allowShadowing hooks) || null shadowedBindings
isShadowed = not (handleShadowing hooks) || null shadowedBindings
resolvedFreeVars' = Map.unionWith (++) (Map.fromList resolvedFreeVars) (Map.fromList shadowedBindings)
ok = all (\(v,tms) -> length tms == 1) (Map.toList resolvedFreeVars')
case ok of

View File

@ -139,8 +139,8 @@ Vector.sum = Vector.fold-left (+) 0;
Vector.dedup : ∀ a . Order a -> Vector a -> Vector a;
Vector.dedup o v = Vector.dedup-adjacent (Order.equal o) (Vector.sort o v);
Remote.map : ∀ a b . (a -> b) -> Remote a -> Remote b;
Remote.map f = Remote.bind (f `and-then` Remote.pure);
-- Remote.map : ∀ a b . (a -> b) -> Remote a -> Remote b;
-- Remote.map f = Remote.bind (f `and-then` Remote.pure);
Remote.map2 : ∀ a b c . (a -> b -> c) -> Remote a -> Remote b -> Remote c;
Remote.map2 f a b = do Remote