Block examples (not working yet)

This commit is contained in:
Paul Chiusano 2021-05-10 10:58:19 -05:00
parent ca7b32d1ca
commit 4ce85400d5
7 changed files with 57 additions and 18 deletions

View File

@ -142,6 +142,11 @@ displayPretty pped terms typeOf eval types tm = go tm
P.backticked <$> displayTerm pped terms typeOf eval types ex
where ex = Term.lam' (ABT.annotation body) (drop (fromIntegral n) vs) body
DD.Doc2SpecialFormExampleBlock n (DD.Doc2Example vs body) ->
-- todo: maybe do something with `vs` to indicate the variables are free
P.indentN 4 <$> displayTerm pped terms typeOf eval types ex
where ex = Term.lam' (ABT.annotation body) (drop (fromIntegral n) vs) body
-- Link (Either Link.Type Doc2.Term)
DD.Doc2SpecialFormLink e -> let
ppe = PPE.suffixifiedPPE pped

View File

@ -334,7 +334,7 @@ lexemes' eof = P.optional space >> do
leafy ok = groupy ok gs
where
gs = link <|> externalLink <|> ticked <|> expr
gs = link <|> externalLink <|> example <|> expr
<|> boldOrItalicOrStrikethrough ok <|> verbatim
<|> atDoc <|> wordy ok
@ -414,14 +414,23 @@ lexemes' eof = P.optional space >> do
dropNl ('\n':t) = t
dropNl as = as
ticked =
P.label "inline code (examples: ``List.map f xs``, ``[1] :+ 2``)" $
wrap "syntax.docExample" $ do
n <- P.try $ do _ <- lit "`"
length <$> P.takeWhile1P (Just "backticks") (== '`')
let end :: P [Token Lexeme] = [] <$ lit (replicate (n+1) '`')
ex <- CP.space *> lexemes' end
pure ex
example = do
ts@(Token (Open "syntax.docExample") start stop : rest) <- ticked
spaces <- P.lookAhead (P.takeWhileP Nothing isSpace)
let hasBlank s = length (filter (== '\n') s) >= 2
if hasBlank spaces then
pure (Token (Open "syntax.docExampleBlock") start stop : rest)
else
pure ts
where
ticked =
P.label "inline code (examples: ``List.map f xs``, ``[1] :+ 2``)" $
wrap "syntax.docExample" $ do
n <- P.try $ do _ <- lit "`"
length <$> P.takeWhile1P (Just "backticks") (== '`')
let end :: P [Token Lexeme] = [] <$ lit (replicate (n+1) '`')
ex <- CP.space *> lexemes' end
pure ex
docClose = [] <$ lit "}}"
docOpen = [] <$ lit "{{"

View File

@ -111,6 +111,7 @@ pattern Doc2SpecialFormRef <- ((== doc2SpecialFormRef) -> True)
doc2SpecialFormSourceId = constructorNamed doc2SpecialFormRef "Doc2.SpecialForm.Source"
doc2SpecialFormFoldedSourceId = constructorNamed doc2SpecialFormRef "Doc2.SpecialForm.FoldedSource"
doc2SpecialFormExampleId = constructorNamed doc2SpecialFormRef "Doc2.SpecialForm.Example"
doc2SpecialFormExampleBlockId = constructorNamed doc2SpecialFormRef "Doc2.SpecialForm.ExampleBlock"
doc2SpecialFormLinkId = constructorNamed doc2SpecialFormRef "Doc2.SpecialForm.Link"
doc2SpecialFormSignatureId = constructorNamed doc2SpecialFormRef "Doc2.SpecialForm.Signature"
doc2SpecialFormSignatureInlineId = constructorNamed doc2SpecialFormRef "Doc2.SpecialForm.SignatureInline"
@ -122,6 +123,7 @@ doc2SpecialFormEmbedInlineId = constructorNamed doc2SpecialFormRef "Doc2.Special
pattern Doc2SpecialFormSource tm <- Term.App' (Term.Constructor' Doc2SpecialFormRef ((==) doc2SpecialFormSourceId -> True)) tm
pattern Doc2SpecialFormFoldedSource tm <- Term.App' (Term.Constructor' Doc2SpecialFormRef ((==) doc2SpecialFormFoldedSourceId -> True)) tm
pattern Doc2SpecialFormExample n tm <- Term.Apps' (Term.Constructor' Doc2SpecialFormRef ((==) doc2SpecialFormExampleId -> True)) [Term.Nat' n, tm]
pattern Doc2SpecialFormExampleBlock n tm <- Term.Apps' (Term.Constructor' Doc2SpecialFormRef ((==) doc2SpecialFormExampleBlockId -> True)) [Term.Nat' n, tm]
pattern Doc2SpecialFormLink tm <- Term.App' (Term.Constructor' Doc2SpecialFormRef ((==) doc2SpecialFormLinkId -> True)) tm
pattern Doc2SpecialFormSignature tm <- Term.App' (Term.Constructor' Doc2SpecialFormRef ((==) doc2SpecialFormSignatureId -> True)) tm
pattern Doc2SpecialFormSignatureInline tm <- Term.App' (Term.Constructor' Doc2SpecialFormRef ((==) doc2SpecialFormSignatureInlineId -> True)) tm
@ -306,6 +308,8 @@ unique[da70bff6431da17fa515f3d18ded11852b6a745f] type Doc2.SpecialForm
-- Ex: `Example 2 '(x y -> foo x y)` should render as `foo x y`.
-- Ex: `Example 0 '(1 + 1)` should render as `42`.
| Example Nat Doc2.Term
-- Same as `Example`, but as a block rather than inline element
| ExampleBlock Nat Doc2.Term
-- {type Optional} or {List.map}
| Link (Either Link.Type Doc2.Term)
-- @signatures{List.map, List.filter, List.foldLeft}
@ -538,6 +542,7 @@ syntax.docVerbatim c = CodeBlock "raw" c
syntax.docEval d = Special (Eval (Doc2.term d))
syntax.docEvalInline a = Special (EvalInline (Doc2.term a))
syntax.docExample n a = Special (Example n (Doc2.term a))
syntax.docExampleBlock n a = Special (ExampleBlock n (Doc2.term a))
syntax.docLink t = Special (Link t)
syntax.docTransclude d =
guid = "b7a4fb87e34569319591130bf3ec6e24"

View File

@ -486,6 +486,9 @@ doc2Block =
tm -> Term.apps' f [Term.nat (ann tm) 0, addDelay tm]
"syntax.docTransclude" -> evalLike id
"syntax.docEvalInline" -> evalLike addDelay
"syntax.docExampleBlock" -> do
tm <- block'' False True "syntax.docExampleBlock" (pure (void t)) closeBlock
pure $ Term.apps' f [addDelay tm]
"syntax.docEval" -> do
tm <- block' False "syntax.docEval" (pure (void t)) closeBlock
pure $ Term.apps' f [addDelay tm]
@ -984,15 +987,19 @@ substImports ns imports =
Term.substTypeVars [ (suffix, Type.var () full)
| (suffix, full) <- imports, Names.hasTypeNamed (Name.fromVar full) ns ]
block'
block' :: Var v => IsTop -> String -> P v (L.Token ()) -> P v b -> TermP v
block' isTop = block'' isTop False
block''
:: forall v b
. Var v
=> IsTop
-> Bool -- `True` means insert `()` at end of block if it ends with a statement
-> String
-> P v (L.Token ())
-> P v b
-> TermP v
block' isTop s openBlock closeBlock = do
block'' isTop implicitUnitAtEnd s openBlock closeBlock = do
open <- openBlock
(names, imports) <- imports
_ <- optional semi
@ -1026,10 +1033,12 @@ block' isTop s openBlock closeBlock = do
DestructuringBind (_, f) -> f body
body bs = case reverse bs of
Binding ((a, _v), _) : _ -> pure $
Term.var a (positionalVar a Var.missingResult)
if implicitUnitAtEnd then DD.unitTerm a
else Term.var a (positionalVar a Var.missingResult)
Action e : _ -> pure e
DestructuringBind (a, _) : _ -> pure $
Term.var a (positionalVar a Var.missingResult)
if implicitUnitAtEnd then DD.unitTerm a
else Term.var a (positionalVar a Var.missingResult)
[] -> customFailure $ EmptyBlock (const s <$> open)
in toTm bs

View File

@ -1371,16 +1371,20 @@ toDocEvalInline ppe (App' (Ref' r) (Delay' tm))
| nameEndsWith ppe ".docEvalInline" r = Just tm
toDocEvalInline _ _ = Nothing
toDocExample :: Ord v => PrettyPrintEnv -> Term3 v PrintAnnotation -> Maybe (Term3 v PrintAnnotation)
toDocExample ppe (Apps' (Ref' r) [Nat' n, l@(LamsNamed' vs tm)])
| nameEndsWith ppe ".docExample" r,
toDocExample, toDocExampleBlock :: Ord v => PrettyPrintEnv -> Term3 v PrintAnnotation -> Maybe (Term3 v PrintAnnotation)
toDocExample = toDocExample' ".docExample"
toDocExampleBlock = toDocExample' ".docExampleBlock"
toDocExample' :: Ord v => Text -> PrettyPrintEnv -> Term3 v PrintAnnotation -> Maybe (Term3 v PrintAnnotation)
toDocExample' suffix ppe (Apps' (Ref' r) [Nat' n, l@(LamsNamed' vs tm)])
| nameEndsWith ppe suffix r,
ABT.freeVars l == mempty,
ok tm =
Just (lam' (ABT.annotation l) (drop (fromIntegral n) vs) tm)
where
ok (Apps' f _) = ABT.freeVars f == mempty
ok tm = ABT.freeVars tm == mempty
toDocExample _ _ = Nothing
toDocExample' _ _ _ = Nothing
toDocTransclude :: PrettyPrintEnv -> Term3 v PrintAnnotation -> Maybe (Term3 v PrintAnnotation)
toDocTransclude ppe (App' (Ref' r) tm)

View File

@ -73,6 +73,13 @@ id x = x
id (sqr 10)
```
Use two backticks if you just want to include a snippet of code without evaluating it.
``
cube : Nat -> Nat
cube x = x * x * x
``
}}
sqr x = x Nat.* x

View File

@ -35,7 +35,7 @@ And for a limited time, you can get even more builtin goodies:
.foo> ls
1. builtin/ (503 definitions)
1. builtin/ (505 definitions)
```
More typically, you'd start out by pulling `base.