mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-20 14:57:41 +03:00
ormoluify
This commit is contained in:
parent
775789cdea
commit
419cd16d17
@ -571,7 +571,7 @@ numberedList :: (Foldable f) => f (Pretty ColorText) -> Pretty ColorText
|
||||
numberedList = numberedListFrom 0
|
||||
|
||||
numberedListFrom :: (Foldable f) => Int -> f (Pretty ColorText) -> Pretty ColorText
|
||||
numberedListFrom n = numbered (\i -> hiBlack . fromString $ show (i+n) <> ".")
|
||||
numberedListFrom n = numbered (\i -> hiBlack . fromString $ show (i + n) <> ".")
|
||||
|
||||
leftPad, rightPad :: (IsString s) => Width -> Pretty s -> Pretty s
|
||||
leftPad n p =
|
||||
|
@ -155,55 +155,63 @@ rewriteTermRef :: Reference
|
||||
rewriteTermRef = lookupDeclRef "RewriteTerm"
|
||||
|
||||
pattern RewriteTerm' :: Term2 vt at ap v a -> Term2 vt at ap v a -> Term2 vt at ap v a
|
||||
pattern RewriteTerm' lhs rhs <- (unRewriteTerm -> Just (lhs,rhs))
|
||||
pattern RewriteTerm' lhs rhs <- (unRewriteTerm -> Just (lhs, rhs))
|
||||
|
||||
unRewriteTerm :: Term2 vt at ap v a -> Maybe (Term2 vt at ap v a, Term2 vt at ap v a)
|
||||
unRewriteTerm (Term.Apps' (Term.Constructor' (ConstructorReference r _)) [lhs,rhs])
|
||||
| r == rewriteTermRef = Just (lhs,rhs)
|
||||
unRewriteTerm (Term.Apps' (Term.Constructor' (ConstructorReference r _)) [lhs, rhs])
|
||||
| r == rewriteTermRef = Just (lhs, rhs)
|
||||
unRewriteTerm _ = Nothing
|
||||
|
||||
rewriteCaseRef :: Reference
|
||||
rewriteCaseRef = lookupDeclRef "RewriteCase"
|
||||
|
||||
pattern RewriteCase' :: Term2 vt at ap v a -> Term2 vt at ap v a -> Term2 vt at ap v a
|
||||
pattern RewriteCase' lhs rhs <- (unRewriteCase -> Just (lhs,rhs))
|
||||
pattern RewriteCase' lhs rhs <- (unRewriteCase -> Just (lhs, rhs))
|
||||
|
||||
rewriteCase :: Ord v => a -> Term2 vt at ap v a -> Term2 vt at ap v a -> Term2 vt at ap v a
|
||||
rewriteCase a tm1 tm2 = Term.app a (Term.app a1 (Term.constructor a1 r) tm1) tm2
|
||||
where
|
||||
where
|
||||
a1 = ABT.annotation tm1
|
||||
r = ConstructorReference rewriteCaseRef 0
|
||||
|
||||
rewriteTerm :: Ord v => a -> Term2 vt at ap v a -> Term2 vt at ap v a -> Term2 vt at ap v a
|
||||
rewriteTerm a tm1 tm2 = Term.app a (Term.app a1 (Term.constructor a1 r) tm1) tm2
|
||||
where
|
||||
where
|
||||
a1 = ABT.annotation tm1
|
||||
r = ConstructorReference rewriteTermRef 0
|
||||
|
||||
unRewriteCase :: Term2 vt at ap v a -> Maybe (Term2 vt at ap v a, Term2 vt at ap v a)
|
||||
unRewriteCase (Term.Apps' (Term.Constructor' (ConstructorReference r _)) [lhs,rhs])
|
||||
| r == rewriteCaseRef = Just (lhs,rhs)
|
||||
unRewriteCase (Term.Apps' (Term.Constructor' (ConstructorReference r _)) [lhs, rhs])
|
||||
| r == rewriteCaseRef = Just (lhs, rhs)
|
||||
unRewriteCase _ = Nothing
|
||||
|
||||
rewriteTypeRef :: Reference
|
||||
rewriteTypeRef = lookupDeclRef "RewriteSignature"
|
||||
|
||||
pattern RewriteSignature' :: forall vt at ap v a . [vt] -> Type vt at -> Type vt at -> Term2 vt at ap v a
|
||||
pattern RewriteSignature' vs lhs rhs <- (unRewriteSignature -> Just (vs, lhs,rhs))
|
||||
pattern RewriteSignature' :: forall vt at ap v a. [vt] -> Type vt at -> Type vt at -> Term2 vt at ap v a
|
||||
pattern RewriteSignature' vs lhs rhs <- (unRewriteSignature -> Just (vs, lhs, rhs))
|
||||
|
||||
rewriteType :: (Var v, Semigroup a) => a -> [v] -> Type v a -> Type v a -> Term2 v a a v a
|
||||
rewriteType a vs lhs rhs =
|
||||
Term.app a (Term.constructor la (ConstructorReference rewriteTypeRef 0))
|
||||
(Term.ann a (Term.delay a (Term.delay a (unitTerm a)))
|
||||
(Type.foralls a vs (Type.arrow (la <> ra) lhs (Type.arrow ra rhs (unitType ra)))))
|
||||
rewriteType a vs lhs rhs =
|
||||
Term.app
|
||||
a
|
||||
(Term.constructor la (ConstructorReference rewriteTypeRef 0))
|
||||
( Term.ann
|
||||
a
|
||||
(Term.delay a (Term.delay a (unitTerm a)))
|
||||
(Type.foralls a vs (Type.arrow (la <> ra) lhs (Type.arrow ra rhs (unitType ra))))
|
||||
)
|
||||
where
|
||||
la = ABT.annotation lhs
|
||||
ra = ABT.annotation rhs
|
||||
|
||||
unRewriteSignature :: Term2 vt at ap v a -> Maybe ([vt], Type vt at, Type vt at)
|
||||
unRewriteSignature (Term.App' (Term.Constructor' (ConstructorReference r _))
|
||||
(Term.Ann' _ (Type.ForallsNamedOpt' vs (Type.Arrow' lhs (Type.Arrow' rhs _unit)))))
|
||||
| r == rewriteTypeRef = Just (vs, lhs, rhs)
|
||||
unRewriteSignature
|
||||
( Term.App'
|
||||
(Term.Constructor' (ConstructorReference r _))
|
||||
(Term.Ann' _ (Type.ForallsNamedOpt' vs (Type.Arrow' lhs (Type.Arrow' rhs _unit))))
|
||||
)
|
||||
| r == rewriteTypeRef = Just (vs, lhs, rhs)
|
||||
unRewriteSignature _ = Nothing
|
||||
|
||||
rewritesRef :: Reference
|
||||
@ -214,8 +222,9 @@ pattern Rewrites' ts <- (unRewrites -> Just ts)
|
||||
|
||||
rewrites :: (Var v, Monoid a) => a -> [Term2 vt at ap v a] -> Term2 vt at ap v a
|
||||
rewrites a [] = Term.app a (Term.constructor a (ConstructorReference rewritesRef 0)) (tupleTerm [])
|
||||
rewrites a ts@(hd:_) = Term.app a (Term.constructor a1 (ConstructorReference rewritesRef 0)) (tupleTerm ts)
|
||||
where a1 = ABT.annotation hd
|
||||
rewrites a ts@(hd : _) = Term.app a (Term.constructor a1 (ConstructorReference rewritesRef 0)) (tupleTerm ts)
|
||||
where
|
||||
a1 = ABT.annotation hd
|
||||
|
||||
unRewrites :: Term2 vt at ap v a -> Maybe [Term2 vt at ap v a]
|
||||
unRewrites (Term.App' (Term.Constructor' (ConstructorReference r _)) tup)
|
||||
@ -327,7 +336,7 @@ builtinDataDecls = rs1 ++ rs
|
||||
]
|
||||
rewriteCase =
|
||||
DataDeclaration
|
||||
(Unique "a116f0f1a8d16aba115b7790b09c56820be48798d9fef64fda3ec2325388f769")
|
||||
(Unique "a116f0f1a8d16aba115b7790b09c56820be48798d9fef64fda3ec2325388f769")
|
||||
()
|
||||
[v "a", v "b"]
|
||||
[ ( (),
|
||||
@ -340,7 +349,7 @@ builtinDataDecls = rs1 ++ rs
|
||||
]
|
||||
rewriteTerm =
|
||||
DataDeclaration
|
||||
(Unique "d577219dc862f148bbdbeb78ae977f6a7da22eb44a1b43d484cabd3e4d7e76a1")
|
||||
(Unique "d577219dc862f148bbdbeb78ae977f6a7da22eb44a1b43d484cabd3e4d7e76a1")
|
||||
()
|
||||
[v "a", v "b"]
|
||||
[ ( (),
|
||||
@ -353,7 +362,7 @@ builtinDataDecls = rs1 ++ rs
|
||||
]
|
||||
rewriteType =
|
||||
DataDeclaration
|
||||
(Unique "f9ae4c4263c2f173deeb550dc1f798147c301ea3a6b306810988e4634834507b")
|
||||
(Unique "f9ae4c4263c2f173deeb550dc1f798147c301ea3a6b306810988e4634834507b")
|
||||
()
|
||||
[v "a", v "b"]
|
||||
[ ( (),
|
||||
@ -361,11 +370,12 @@ builtinDataDecls = rs1 ++ rs
|
||||
Type.foralls
|
||||
()
|
||||
[v "a", v "b"]
|
||||
((var "a" `arr` (var "b" `arr` var "Unit")) `arr` Type.apps' (var "RewriteSignature") [var "a", var "b"]))
|
||||
((var "a" `arr` (var "b" `arr` var "Unit")) `arr` Type.apps' (var "RewriteSignature") [var "a", var "b"])
|
||||
)
|
||||
]
|
||||
rewrites =
|
||||
DataDeclaration
|
||||
(Unique "f64795bf31f7eb41e59b31379d6576a4abaca5b4c1bfc0b8c211e608906aff1a")
|
||||
(Unique "f64795bf31f7eb41e59b31379d6576a4abaca5b4c1bfc0b8c211e608906aff1a")
|
||||
()
|
||||
[v "a"]
|
||||
[ ( (),
|
||||
@ -373,7 +383,8 @@ builtinDataDecls = rs1 ++ rs
|
||||
Type.foralls
|
||||
()
|
||||
[v "a"]
|
||||
(var "a" `arr` Type.apps' (var "Rewrites") [var "a"]))
|
||||
(var "a" `arr` Type.apps' (var "Rewrites") [var "a"])
|
||||
)
|
||||
]
|
||||
isTest =
|
||||
DataDeclaration
|
||||
|
@ -68,7 +68,7 @@ file = do
|
||||
(terms, (kind, (v, Term.generalizeTypeSignatures at)) : watches)
|
||||
WatchExpression kind guid _ at ->
|
||||
let v = Var.typed (Var.UnnamedWatch kind guid)
|
||||
in (terms, (kind, (v, Term.generalizeTypeSignatures at)) : watches)
|
||||
in (terms, (kind, (v, Term.generalizeTypeSignatures at)) : watches)
|
||||
Binding ((_, v), at) -> ((v, Term.generalizeTypeSignatures at) : terms, watches)
|
||||
Bindings bs -> ([(v, Term.generalizeTypeSignatures at) | ((_, v), at) <- bs] ++ terms, watches)
|
||||
let (terms, watches) = (reverse termsr, reverse watchesr)
|
||||
|
@ -84,13 +84,13 @@ rewriteBlock = do
|
||||
t <- openBlockWith "@rewrite"
|
||||
elements <- sepBy semi (rewriteTerm <|> rewriteCase <|> rewriteType)
|
||||
b <- closeBlock
|
||||
pure (DD.rewrites (ann t <> ann b) elements)
|
||||
pure (DD.rewrites (ann t <> ann b) elements)
|
||||
where
|
||||
rewriteTermlike kw mk = do
|
||||
kw <- quasikeyword kw
|
||||
lhs <- term
|
||||
rhs <- block "==>"
|
||||
pure (mk (ann kw <> ann rhs) lhs rhs)
|
||||
rewriteTermlike kw mk = do
|
||||
kw <- quasikeyword kw
|
||||
lhs <- term
|
||||
rhs <- block "==>"
|
||||
pure (mk (ann kw <> ann rhs) lhs rhs)
|
||||
rewriteTerm = rewriteTermlike "term" DD.rewriteTerm
|
||||
rewriteCase = rewriteTermlike "case" DD.rewriteCase
|
||||
rewriteType = do
|
||||
|
@ -443,7 +443,7 @@ pretty0
|
||||
(App' f@(Builtin' "Any.Any") arg, _) ->
|
||||
paren (p >= 10) <$> (PP.hang <$> goNormal 9 f <*> goNormal 10 arg)
|
||||
(DD.Rewrites' rs, _) -> do
|
||||
let kw = fmt S.ControlKeyword "@rewrite"
|
||||
let kw = fmt S.ControlKeyword "@rewrite"
|
||||
arr = fmt S.ControlKeyword "==>"
|
||||
control = fmt S.ControlKeyword
|
||||
sub kw lhs = PP.sep " " <$> sequence [pure $ control kw, goNormal 0 lhs, pure arr]
|
||||
@ -452,12 +452,12 @@ pretty0
|
||||
go (DD.RewriteSignature' vs lhs rhs) = do
|
||||
lhs <- TypePrinter.pretty0 im 0 lhs
|
||||
PP.hang (PP.sep " " (stuff lhs)) <$> TypePrinter.pretty0 im 0 rhs
|
||||
where
|
||||
stuff lhs =
|
||||
[ control "signature" ]
|
||||
<> [ fmt S.Var (PP.text (Var.name v)) | v <- vs ]
|
||||
<> (if null vs then [] else [ fmt S.TypeOperator "." ])
|
||||
<> [ lhs, arr ]
|
||||
where
|
||||
stuff lhs =
|
||||
[control "signature"]
|
||||
<> [fmt S.Var (PP.text (Var.name v)) | v <- vs]
|
||||
<> (if null vs then [] else [fmt S.TypeOperator "."])
|
||||
<> [lhs, arr]
|
||||
go tm = goNormal 10 tm
|
||||
PP.hang kw <$> fmap PP.lines (traverse go rs)
|
||||
(Apps' f@(Constructor' _) args, _) ->
|
||||
|
@ -1749,7 +1749,7 @@ handleStructuredFindI rule = do
|
||||
pure $ (t, maybe False (\e -> any ($ e) rules) oe)
|
||||
ok t = pure (t, False)
|
||||
results0 <- traverse ok results
|
||||
let results = [ (hq, r) | ((hq,r), True) <- results0 ]
|
||||
let results = [(hq, r) | ((hq, r), True) <- results0]
|
||||
let toNumArgs = Text.unpack . Reference.toText . Referent.toReference . view _2
|
||||
#numberedArgs .= map toNumArgs results
|
||||
Cli.respond (ListStructuredFind (fst <$> results))
|
||||
@ -1774,19 +1774,18 @@ lookupRewrite onErr rule = do
|
||||
Cli.runTransaction (Codebase.getTerm codebase r)
|
||||
s -> Cli.returnEarly (TermAmbiguous (PPE.suffixifiedPPE ppe) rule s)
|
||||
tm <- maybe (Cli.returnEarly (TermAmbiguous (PPE.suffixifiedPPE ppe) rule mempty)) pure ot
|
||||
let
|
||||
extract tm = case tm of
|
||||
Term.Ann' tm _typ -> extract tm
|
||||
(DD.RewriteTerm' lhs rhs) -> pure (ABT.rewriteExpression lhs rhs, ABT.containsExpression lhs)
|
||||
(DD.RewriteCase' lhs rhs) -> pure (Term.rewriteCasesLHS lhs rhs, fromMaybe False . Term.containsCaseTerm lhs)
|
||||
(DD.RewriteSignature' _vs lhs rhs) -> pure (Term.rewriteSignatures lhs rhs, Term.containsSignature lhs)
|
||||
_ -> Cli.returnEarly (onErr rule)
|
||||
extractOuter tm = case tm of
|
||||
Term.Ann' tm _typ -> extractOuter tm
|
||||
Term.LamsNamed' _vs tm -> extractOuter tm
|
||||
DD.Rewrites' rules -> traverse extract rules
|
||||
_ -> Cli.returnEarly (onErr rule)
|
||||
rules <- extractOuter tm
|
||||
let extract tm = case tm of
|
||||
Term.Ann' tm _typ -> extract tm
|
||||
(DD.RewriteTerm' lhs rhs) -> pure (ABT.rewriteExpression lhs rhs, ABT.containsExpression lhs)
|
||||
(DD.RewriteCase' lhs rhs) -> pure (Term.rewriteCasesLHS lhs rhs, fromMaybe False . Term.containsCaseTerm lhs)
|
||||
(DD.RewriteSignature' _vs lhs rhs) -> pure (Term.rewriteSignatures lhs rhs, Term.containsSignature lhs)
|
||||
_ -> Cli.returnEarly (onErr rule)
|
||||
extractOuter tm = case tm of
|
||||
Term.Ann' tm _typ -> extractOuter tm
|
||||
Term.LamsNamed' _vs tm -> extractOuter tm
|
||||
DD.Rewrites' rules -> traverse extract rules
|
||||
_ -> Cli.returnEarly (onErr rule)
|
||||
rules <- extractOuter tm
|
||||
pure (ppe, currentNames, rules)
|
||||
|
||||
handleStructuredFindReplaceI :: HQ.HashQualified Name -> Cli ()
|
||||
@ -1795,10 +1794,9 @@ handleStructuredFindReplaceI rule = do
|
||||
uf <- Cli.expectLatestParsedFile
|
||||
(dest, _) <- Cli.expectLatestFile
|
||||
#latestFile ?= (dest, True)
|
||||
let
|
||||
go _tm0 tm [] = tm
|
||||
go tm0 tm ((r,_):rules) = go tm0 ((tm <|> tm0) >>= r) rules
|
||||
uf' = UF.rewrite (Set.singleton (HQ.toVar rule)) (\tm -> go (Just tm) Nothing rules) uf
|
||||
let go _tm0 tm [] = tm
|
||||
go tm0 tm ((r, _) : rules) = go tm0 ((tm <|> tm0) >>= r) rules
|
||||
uf' = UF.rewrite (Set.singleton (HQ.toVar rule)) (\tm -> go (Just tm) Nothing rules) uf
|
||||
#latestTypecheckedFile .= Just (Left . snd $ uf')
|
||||
let msg = "| Rewrote using: "
|
||||
Cli.respond $ OutputRewrittenFile ppe dest (msg <> HQ.toString rule) uf'
|
||||
|
@ -230,9 +230,9 @@ data Output
|
||||
| ListOfLinks PPE.PrettyPrintEnv [(HQ.HashQualified Name, Reference, Maybe (Type Symbol Ann))]
|
||||
| ListShallow (IO PPE.PrettyPrintEnv) [ShallowListEntry Symbol Ann]
|
||||
| ListOfPatches (Set Name)
|
||||
| ListStructuredFind [HQ.HashQualified Name]
|
||||
-- ListStructuredFind patternMatchingUsages termBodyUsages
|
||||
| -- show the result of add/update
|
||||
| ListStructuredFind [HQ.HashQualified Name]
|
||||
| -- ListStructuredFind patternMatchingUsages termBodyUsages
|
||||
-- show the result of add/update
|
||||
SlurpOutput Input PPE.PrettyPrintEnv SlurpResult
|
||||
| -- Original source, followed by the errors:
|
||||
ParseErrors Text [Parser.Err Symbol]
|
||||
@ -375,7 +375,7 @@ data Output
|
||||
(ProjectAndBranch ProjectName ProjectBranchName)
|
||||
(ProjectAndBranch ProjectName ProjectBranchName)
|
||||
| RenamedProject ProjectName ProjectName
|
||||
| OutputRewrittenFile PPE.PrettyPrintEnvDecl FilePath String ([Symbol] {- symbols rewritten -}, UF.UnisonFile Symbol Ann)
|
||||
| OutputRewrittenFile PPE.PrettyPrintEnvDecl FilePath String ([Symbol {- symbols rewritten -}], UF.UnisonFile Symbol Ann)
|
||||
| RenamedProjectBranch ProjectName ProjectBranchName ProjectBranchName
|
||||
| CantRenameBranchTo ProjectBranchName
|
||||
| FetchingLatestReleaseOfBase
|
||||
|
@ -123,10 +123,11 @@ parseInput getRoot currentPath numberedArgs patterns segments = runExceptT do
|
||||
command : args -> case Map.lookup command patterns of
|
||||
Just pat@(InputPattern {parse}) -> do
|
||||
let expandedNumbers :: [String]
|
||||
expandedNumbers =
|
||||
foldMap (expandNumber numberedArgs)
|
||||
-- don't expand args of type "raw"
|
||||
(args `zip` map ((/=) (Just "raw") . argName) [0..])
|
||||
expandedNumbers =
|
||||
foldMap
|
||||
(expandNumber numberedArgs)
|
||||
-- don't expand args of type "raw"
|
||||
(args `zip` map ((/=) (Just "raw") . argName) [0 ..])
|
||||
argName i = InputPattern.typeName <$> InputPattern.argType pat i
|
||||
expandedGlobs <- ifor expandedNumbers $ \i arg -> do
|
||||
if Globbing.containsGlob arg
|
||||
@ -152,9 +153,9 @@ parseInput getRoot currentPath numberedArgs patterns segments = runExceptT do
|
||||
|
||||
-- Expand a numeric argument like `1` or a range like `3-9`
|
||||
-- Any argument tagged with 'False' is left alone
|
||||
expandNumber :: [String] -> (String,Bool) -> [String]
|
||||
expandNumber _ (s,False) = [s]
|
||||
expandNumber numberedArgs (s,True) =
|
||||
expandNumber :: [String] -> (String, Bool) -> [String]
|
||||
expandNumber _ (s, False) = [s]
|
||||
expandNumber numberedArgs (s, True) =
|
||||
maybe
|
||||
[s]
|
||||
(map (\i -> fromMaybe (show i) . atMay numberedArgs $ i - 1))
|
||||
|
@ -485,7 +485,7 @@ viewByPrefix =
|
||||
)
|
||||
|
||||
rawTermQueryArg :: ArgumentType
|
||||
rawTermQueryArg = exactDefinitionTermQueryArg { typeName = "raw" }
|
||||
rawTermQueryArg = exactDefinitionTermQueryArg {typeName = "raw"}
|
||||
|
||||
sfind :: InputPattern
|
||||
sfind =
|
||||
@ -532,7 +532,7 @@ sfindReplace =
|
||||
P.wrap $
|
||||
"Here, `x` will stand in for any expression wherever this rewrite is applied,"
|
||||
<> "so this rule will match "
|
||||
<> P.backticked "(42+10+11) + 1"
|
||||
<> P.backticked "(42+10+11) + 1"
|
||||
<> "and replace it with"
|
||||
<> P.backticked' "Nat.increment (42+10+11)" "."
|
||||
]
|
||||
|
@ -3665,13 +3665,13 @@ endangeredDependentsTable ppeDecl m =
|
||||
listStructuredFind :: [HQ.HashQualified Name] -> Pretty
|
||||
listStructuredFind [] = "😶 I couldn't find any matches."
|
||||
listStructuredFind tms =
|
||||
P.callout "🔎" . P.lines $ [
|
||||
"These definitions from the current namespace (excluding `lib`) have matches:",
|
||||
"",
|
||||
P.indentN 2 $ P.numberedList (pnames tms),
|
||||
"",
|
||||
tip (msg (length tms))
|
||||
]
|
||||
P.callout "🔎" . P.lines $
|
||||
[ "These definitions from the current namespace (excluding `lib`) have matches:",
|
||||
"",
|
||||
P.indentN 2 $ P.numberedList (pnames tms),
|
||||
"",
|
||||
tip (msg (length tms))
|
||||
]
|
||||
where
|
||||
pnames hqs = P.syntaxToColor . prettyHashQualified <$> hqs
|
||||
msg 1 = "Try " <> IP.makeExample IP.edit ["1"] <> " to bring this into your scratch file."
|
||||
|
@ -419,13 +419,13 @@ rebuildMaybeUp ::
|
||||
Term f v a ->
|
||||
Maybe (Term f v a)
|
||||
rebuildMaybeUp f tm@(Term _ ann body) = f $ case body of
|
||||
Var _ -> tm
|
||||
Var _ -> tm
|
||||
Cycle body -> fromMaybe tm $ fmap (cycle' ann) (rebuildMaybeUp f body)
|
||||
Abs x e -> fromMaybe tm $ fmap (abs' ann x) (rebuildMaybeUp f e)
|
||||
Tm body ->
|
||||
Tm body ->
|
||||
if all (isNothing . snd) body'
|
||||
then tm
|
||||
else tm' ann (fmap (uncurry fromMaybe) body')
|
||||
then tm
|
||||
else tm' ann (fmap (uncurry fromMaybe) body')
|
||||
where
|
||||
body' = fmap (\tm -> (tm, rebuildMaybeUp f tm)) body
|
||||
|
||||
@ -507,7 +507,7 @@ reannotateUp g t = case out t of
|
||||
ann = g t <> foldMap (snd . annotation) body'
|
||||
in tm' (annotation t, ann) body'
|
||||
|
||||
-- given a list of terms, freshen all their free variables
|
||||
-- given a list of terms, freshen all their free variables
|
||||
-- to not overlap with any variables used within `wrt`.
|
||||
freshenWrt :: (Var v, Traversable f) => Term f v a -> [Term f v a] -> [Term f v a]
|
||||
freshenWrt wrt tms = renames varChanges <$> tms
|
||||
@ -519,8 +519,8 @@ freshenWrt wrt tms = renames varChanges <$> tms
|
||||
go (m, u) v = let v' = freshIn u v in (Map.insert v v' m, Set.insert v' u)
|
||||
|
||||
freshenBothWrt :: (Var v, Traversable f) => Term f v a -> Term f v a -> Term f v a -> (Term f v a, Term f v a)
|
||||
freshenBothWrt wrt tm1 tm2 = case freshenWrt wrt [tm1,tm2] of
|
||||
[tm1,tm2] -> (tm1, tm2)
|
||||
freshenBothWrt wrt tm1 tm2 = case freshenWrt wrt [tm1, tm2] of
|
||||
[tm1, tm2] -> (tm1, tm2)
|
||||
_ -> error "freshenWrt impossible"
|
||||
|
||||
rewriteExpression ::
|
||||
|
@ -67,22 +67,22 @@ updateDependencies tms p = case p of
|
||||
SequenceOp loc (updateDependencies tms lhs) op (updateDependencies tms rhs)
|
||||
|
||||
hasSubpattern :: Pattern loc -> Pattern loc -> Bool
|
||||
hasSubpattern (Unbound {}) _ = True
|
||||
hasSubpattern (Var {}) _ = True
|
||||
hasSubpattern (Unbound {}) _ = True
|
||||
hasSubpattern (Var {}) _ = True
|
||||
hasSubpattern needle haystack = needle == haystack || go haystack
|
||||
where
|
||||
go Unbound{} = False
|
||||
go Var{} = False
|
||||
go Int{} = False
|
||||
go Nat{} = False
|
||||
go Float{} = False
|
||||
go Boolean{} = False
|
||||
go Text{} = False
|
||||
go Char{} = False
|
||||
where
|
||||
go Unbound {} = False
|
||||
go Var {} = False
|
||||
go Int {} = False
|
||||
go Nat {} = False
|
||||
go Float {} = False
|
||||
go Boolean {} = False
|
||||
go Text {} = False
|
||||
go Char {} = False
|
||||
go (Constructor _ _ ps) = any (hasSubpattern needle) ps
|
||||
go (As _ p) = hasSubpattern needle p
|
||||
go (EffectPure _ p) = hasSubpattern needle p
|
||||
go (EffectBind _ _ ps p) = any (hasSubpattern needle) ps || hasSubpattern needle p
|
||||
go (EffectPure _ p) = hasSubpattern needle p
|
||||
go (EffectBind _ _ ps p) = any (hasSubpattern needle) ps || hasSubpattern needle p
|
||||
go (SequenceLiteral _ ps) = any (hasSubpattern needle) ps
|
||||
go (SequenceOp _ ph _ pt) = hasSubpattern needle ph || hasSubpattern needle pt
|
||||
|
||||
|
@ -1388,62 +1388,65 @@ rewriteSignatures tyLhs tyRhs tm = ABT.rebuildMaybeUp go tm
|
||||
go a@(Ann' tm tp) = ann (ABT.annotation a) tm <$> ABT.rewriteExpression tyLhs tyRhs tp
|
||||
go _ = Nothing
|
||||
|
||||
rewriteCasesLHS :: forall v typeVar typeAnn a
|
||||
. (Var v, Var typeVar, Ord v, Show typeVar, Eq typeAnn, Semigroup a)
|
||||
=> Term2 typeVar typeAnn a v a
|
||||
-> Term2 typeVar typeAnn a v a
|
||||
-> Term2 typeVar typeAnn a v a
|
||||
-> Maybe (Term2 typeVar typeAnn a v a)
|
||||
rewriteCasesLHS pat0 pat0' =
|
||||
rewriteCasesLHS ::
|
||||
forall v typeVar typeAnn a.
|
||||
(Var v, Var typeVar, Ord v, Show typeVar, Eq typeAnn, Semigroup a) =>
|
||||
Term2 typeVar typeAnn a v a ->
|
||||
Term2 typeVar typeAnn a v a ->
|
||||
Term2 typeVar typeAnn a v a ->
|
||||
Maybe (Term2 typeVar typeAnn a v a)
|
||||
rewriteCasesLHS pat0 pat0' =
|
||||
(\tm -> out <$> ABT.rewriteExpression pat pat' (into tm))
|
||||
where
|
||||
ann = ABT.annotation
|
||||
embedPattern t = app (ann t) (builtin (ann t) "#pattern") t
|
||||
embedPattern t = app (ann t) (builtin (ann t) "#pattern") t
|
||||
pat = ABT.rebuildUp' embedPattern pat0
|
||||
pat' = pat0'
|
||||
|
||||
into :: Term2 typeVar typeAnn a v a -> Term2 typeVar typeAnn a v a
|
||||
into = ABT.rebuildUp' go where
|
||||
go t@(Match' scrutinee cases) =
|
||||
apps' (builtin at "#match") [scrutinee, apps' (builtin at "#cases") (map matchCaseToTerm cases)]
|
||||
where
|
||||
at = ann t
|
||||
go t = t
|
||||
into = ABT.rebuildUp' go
|
||||
where
|
||||
go t@(Match' scrutinee cases) =
|
||||
apps' (builtin at "#match") [scrutinee, apps' (builtin at "#cases") (map matchCaseToTerm cases)]
|
||||
where
|
||||
at = ann t
|
||||
go t = t
|
||||
|
||||
out :: Term2 typeVar typeAnn a v a -> Term2 typeVar typeAnn a v a
|
||||
out = ABT.rebuildUp' go where
|
||||
go (App' (Builtin' "#pattern") t) = t
|
||||
go t@(Apps' (Builtin' "#match") [scrute, Apps' (Builtin' "#cases") cases]) =
|
||||
match at scrute (tweak . matchCaseFromTerm <$> cases)
|
||||
where
|
||||
at = ABT.annotation t
|
||||
tweak Nothing = MatchCase (Pattern.Unbound at) Nothing (text at "🆘 rewrite produced an invalid pattern")
|
||||
tweak (Just mc) = mc
|
||||
go t = t
|
||||
out = ABT.rebuildUp' go
|
||||
where
|
||||
go (App' (Builtin' "#pattern") t) = t
|
||||
go t@(Apps' (Builtin' "#match") [scrute, Apps' (Builtin' "#cases") cases]) =
|
||||
match at scrute (tweak . matchCaseFromTerm <$> cases)
|
||||
where
|
||||
at = ABT.annotation t
|
||||
tweak Nothing = MatchCase (Pattern.Unbound at) Nothing (text at "🆘 rewrite produced an invalid pattern")
|
||||
tweak (Just mc) = mc
|
||||
go t = t
|
||||
|
||||
toPattern :: Var v => Term2 tv ta tb v loc -> Maybe (Pattern loc)
|
||||
toPattern tm = case tm of
|
||||
Var' v | "_" `Text.isPrefixOf` Var.name v -> pure $ Pattern.Unbound loc
|
||||
Var' _ -> pure $ Pattern.Var loc
|
||||
toPattern :: Var v => Term2 tv ta tb v loc -> Maybe (Pattern loc)
|
||||
toPattern tm = case tm of
|
||||
Var' v | "_" `Text.isPrefixOf` Var.name v -> pure $ Pattern.Unbound loc
|
||||
Var' _ -> pure $ Pattern.Var loc
|
||||
Apps' (Builtin' "#as") [Var' _, tm] -> Pattern.As loc <$> toPattern tm
|
||||
App' (Builtin' "#effect-pure") p -> Pattern.EffectPure loc <$> toPattern p
|
||||
Apps' (Builtin' "#effect-bind") [Apps' (Request' r) args, k] ->
|
||||
App' (Builtin' "#effect-pure") p -> Pattern.EffectPure loc <$> toPattern p
|
||||
Apps' (Builtin' "#effect-bind") [Apps' (Request' r) args, k] ->
|
||||
Pattern.EffectBind loc r <$> traverse toPattern args <*> toPattern k
|
||||
Apps' (Request' r) args -> Pattern.EffectBind loc r <$> traverse toPattern args <*> pure (Pattern.Unbound loc)
|
||||
Apps' (Constructor' r) args -> Pattern.Constructor loc r <$> traverse toPattern args
|
||||
Constructor' r -> pure $ Pattern.Constructor loc r []
|
||||
Request' r -> pure $ Pattern.EffectBind loc r [] (Pattern.Unbound loc)
|
||||
Int' i -> pure $ Pattern.Int loc i
|
||||
Nat' n -> pure $ Pattern.Nat loc n
|
||||
Float' f -> pure $ Pattern.Float loc f
|
||||
Int' i -> pure $ Pattern.Int loc i
|
||||
Nat' n -> pure $ Pattern.Nat loc n
|
||||
Float' f -> pure $ Pattern.Float loc f
|
||||
Boolean' b -> pure $ Pattern.Boolean loc b
|
||||
Text' t -> pure $ Pattern.Text loc t
|
||||
Char' c -> pure $ Pattern.Char loc c
|
||||
Blank' _ -> pure $ Pattern.Unbound loc
|
||||
List' xs -> Pattern.SequenceLiteral loc <$> traverse toPattern (toList xs)
|
||||
Apps' (Builtin' "List.cons") [a, b] -> Pattern.SequenceOp loc <$> toPattern a <*> pure Pattern.Cons <*> toPattern b
|
||||
Apps' (Builtin' "List.cons") [a, b] -> Pattern.SequenceOp loc <$> toPattern a <*> pure Pattern.Cons <*> toPattern b
|
||||
Apps' (Builtin' "List.snoc") [a, b] -> Pattern.SequenceOp loc <$> toPattern a <*> pure Pattern.Snoc <*> toPattern b
|
||||
Apps' (Builtin' "List.++") [a, b] -> Pattern.SequenceOp loc <$> toPattern a <*> pure Pattern.Concat <*> toPattern b
|
||||
Apps' (Builtin' "List.++") [a, b] -> Pattern.SequenceOp loc <$> toPattern a <*> pure Pattern.Concat <*> toPattern b
|
||||
_ -> Nothing
|
||||
where
|
||||
loc = ABT.annotation tm
|
||||
@ -1452,72 +1455,73 @@ matchCaseFromTerm :: Var v => Term2 typeVar typeAnn a v a -> Maybe (MatchCase a
|
||||
matchCaseFromTerm (App' (Builtin' "#case") (ABT.unabsA -> (_, Apps' _ci [pat, guard, body]))) = do
|
||||
p <- toPattern pat
|
||||
let g = unguard guard
|
||||
pure $ MatchCase p (rechain pat <$> g) (rechain pat body)
|
||||
pure $ MatchCase p (rechain pat <$> g) (rechain pat body)
|
||||
where
|
||||
unguard (App' (Builtin' "#guard") t) = Just t
|
||||
unguard (Builtin' "#noguard") = Nothing
|
||||
unguard (App' (Builtin' "#guard") t) = Just t
|
||||
unguard (Builtin' "#noguard") = Nothing
|
||||
unguard _ = Nothing
|
||||
rechain pat tm = foldr (\v tm -> ABT.abs' (ABT.annotation tm) v tm) tm (ABT.allVars pat)
|
||||
matchCaseFromTerm t =
|
||||
matchCaseFromTerm t =
|
||||
Just (MatchCase (Pattern.Unbound (ABT.annotation t)) Nothing (text (ABT.annotation t) "💥 bug: matchCaseToTerm"))
|
||||
|
||||
matchCaseToTerm :: (Semigroup a, Ord v) => MatchCase a (Term2 typeVar typeAnn a v a) -> Term2 typeVar typeAnn a v a
|
||||
matchCaseToTerm (MatchCase pat guard (ABT.unabsA -> (avs, body))) =
|
||||
matchCaseToTerm (MatchCase pat guard (ABT.unabsA -> (avs, body))) =
|
||||
app loc0 (builtin loc0 "#case") chain
|
||||
where
|
||||
loc0 = Pattern.loc pat
|
||||
chain = ABT.absChain' avs (apps' ci [evalState (embedPattern <$> intop pat) avs, intog guard, body])
|
||||
where
|
||||
ci = builtin loc0 "#case.inner"
|
||||
intog Nothing = builtin loc0 "#noguard"
|
||||
intog (Just (ABT.unabsA -> (_,t))) = app (ABT.annotation t) (builtin (ABT.annotation t) "#guard") t
|
||||
|
||||
embedPattern t = ABT.rebuildUp' embed t
|
||||
where embed t = app (ABT.annotation t) (builtin (ABT.annotation t) "#pattern") t
|
||||
intop pat = case pat of
|
||||
Pattern.Unbound loc -> pure (blank loc)
|
||||
Pattern.Var loc -> do
|
||||
avs <- State.get
|
||||
case avs of
|
||||
(a,v):avs -> State.put avs $> var a v
|
||||
_ -> pure (blank loc)
|
||||
Pattern.Boolean loc b -> pure (boolean loc b)
|
||||
Pattern.Int loc i -> pure (int loc i)
|
||||
Pattern.Nat loc n -> pure (nat loc n)
|
||||
Pattern.Float loc f -> pure (float loc f)
|
||||
Pattern.Text loc t -> pure (text loc t)
|
||||
Pattern.Char loc c -> pure (char loc c)
|
||||
Pattern.Constructor loc r ps -> apps' (constructor loc r) <$> traverse intop ps
|
||||
Pattern.As loc p -> do
|
||||
avs <- State.get
|
||||
case avs of
|
||||
(a,v):avs -> do
|
||||
State.put avs
|
||||
p <- intop p
|
||||
pure $ apps' (builtin loc "#as") [var a v, p]
|
||||
_ -> pure (blank loc)
|
||||
Pattern.EffectPure loc p -> app loc (builtin loc "#effect-pure") <$> intop p
|
||||
Pattern.EffectBind loc r ps k -> do
|
||||
ps <- traverse intop ps
|
||||
k <- intop k
|
||||
pure $ apps' (builtin loc "#effect-bind") [apps' (request loc r) ps, k]
|
||||
Pattern.SequenceLiteral loc ps -> list loc <$> traverse intop ps
|
||||
Pattern.SequenceOp loc p op q -> do
|
||||
p <- intop p
|
||||
q <- intop q
|
||||
pure $ apps' (intoOp op) [p, q]
|
||||
loc0 = Pattern.loc pat
|
||||
chain = ABT.absChain' avs (apps' ci [evalState (embedPattern <$> intop pat) avs, intog guard, body])
|
||||
where
|
||||
intoOp Pattern.Concat = builtin loc "List.++"
|
||||
intoOp Pattern.Snoc = builtin loc "List.snoc"
|
||||
intoOp Pattern.Cons = builtin loc "List.cons"
|
||||
ci = builtin loc0 "#case.inner"
|
||||
intog Nothing = builtin loc0 "#noguard"
|
||||
intog (Just (ABT.unabsA -> (_, t))) = app (ABT.annotation t) (builtin (ABT.annotation t) "#guard") t
|
||||
|
||||
embedPattern t = ABT.rebuildUp' embed t
|
||||
where
|
||||
embed t = app (ABT.annotation t) (builtin (ABT.annotation t) "#pattern") t
|
||||
intop pat = case pat of
|
||||
Pattern.Unbound loc -> pure (blank loc)
|
||||
Pattern.Var loc -> do
|
||||
avs <- State.get
|
||||
case avs of
|
||||
(a, v) : avs -> State.put avs $> var a v
|
||||
_ -> pure (blank loc)
|
||||
Pattern.Boolean loc b -> pure (boolean loc b)
|
||||
Pattern.Int loc i -> pure (int loc i)
|
||||
Pattern.Nat loc n -> pure (nat loc n)
|
||||
Pattern.Float loc f -> pure (float loc f)
|
||||
Pattern.Text loc t -> pure (text loc t)
|
||||
Pattern.Char loc c -> pure (char loc c)
|
||||
Pattern.Constructor loc r ps -> apps' (constructor loc r) <$> traverse intop ps
|
||||
Pattern.As loc p -> do
|
||||
avs <- State.get
|
||||
case avs of
|
||||
(a, v) : avs -> do
|
||||
State.put avs
|
||||
p <- intop p
|
||||
pure $ apps' (builtin loc "#as") [var a v, p]
|
||||
_ -> pure (blank loc)
|
||||
Pattern.EffectPure loc p -> app loc (builtin loc "#effect-pure") <$> intop p
|
||||
Pattern.EffectBind loc r ps k -> do
|
||||
ps <- traverse intop ps
|
||||
k <- intop k
|
||||
pure $ apps' (builtin loc "#effect-bind") [apps' (request loc r) ps, k]
|
||||
Pattern.SequenceLiteral loc ps -> list loc <$> traverse intop ps
|
||||
Pattern.SequenceOp loc p op q -> do
|
||||
p <- intop p
|
||||
q <- intop q
|
||||
pure $ apps' (intoOp op) [p, q]
|
||||
where
|
||||
intoOp Pattern.Concat = builtin loc "List.++"
|
||||
intoOp Pattern.Snoc = builtin loc "List.snoc"
|
||||
intoOp Pattern.Cons = builtin loc "List.cons"
|
||||
|
||||
containsCase :: Pattern loc -> Term2 typeVar typeAnn loc v a -> Bool
|
||||
containsCase pat tm = case ABT.out tm of
|
||||
ABT.Var _ -> False
|
||||
ABT.Cycle tm -> containsCase pat tm
|
||||
ABT.Abs _ tm -> containsCase pat tm
|
||||
ABT.Tm (Match scrute cases) ->
|
||||
containsCase pat scrute || any hasPat cases
|
||||
ABT.Tm (Match scrute cases) ->
|
||||
containsCase pat scrute || any hasPat cases
|
||||
where
|
||||
hasPat (MatchCase p _ rhs) = Pattern.hasSubpattern pat p || containsCase pat rhs
|
||||
ABT.Tm f -> any (containsCase pat) (toList f)
|
||||
|
@ -1013,7 +1013,7 @@ lexemes' eof =
|
||||
Just t | t == "type" || Set.member t typeModifiers -> pure [Token (Reserved "=") start end]
|
||||
Just _ -> S.put (env {opening = Just "="}) >> pure [Token (Open "=") start end]
|
||||
_ -> err start LayoutError
|
||||
|
||||
|
||||
rewriteArr = do
|
||||
[Token _ start end] <- symbolyKw "==>"
|
||||
env <- S.get
|
||||
|
Loading…
Reference in New Issue
Block a user