Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .hlint.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@
# - ignore: {name: Use let}
# - ignore: {name: Use const, within: SpecialModule} # Only within certain modules
- ignore: {name: Redundant do}
- ignore: {name: Avoid lambda}
- ignore: {name: Use tuple-section}
- ignore: {name: Redundant lambda}

# Define some custom infix operators
# - fixity: infixr 3 ~^#^~
Expand Down
40 changes: 19 additions & 21 deletions interpreter/src/Language/Granule/Doc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,6 @@ import qualified Data.Map as M

import Control.Monad (when)

-- import Debug.Trace


-- Doc top-level
grDoc :: (?globals::Globals) => String -> AST () () -> IO ()
Expand All @@ -52,7 +50,7 @@ grDoc input ast = do

writeFile ("docs/modules/" <> modName <> ".html") (unpack moduleFile)
-- Generate the Primitives file
when info $ putStrLn $ "Generating docs index file."
when info $ putStrLn "Generating docs index file."
primFile <- generatePrimitivesPage
writeFile "docs/modules/Primitives.html" (unpack primFile)
-- Generate the index file
Expand All @@ -78,12 +76,12 @@ generateModulePage' modName title input ast =
where
inputLines = lines input
content = (if Text.strip preamble == "" then "" else section "Meta-data" preamble)
<> (section "Contents" ((internalNav headings')
<> section "Contents" (internalNav headings'
<> (if modName == "Primitives" then anchor "Built-in Types" else "")
<> Text.concat contentDefs))
<> Text.concat contentDefs)
preamble = parsePreamble inputLines
<> if M.keys (hiddenNames ast) == [] then ""
else (tag "strong" "Module does not export: ") <> Text.intercalate ", " (map (pack . prettyDoc) $ M.keys (hiddenNames ast))
<> if Prelude.null (M.keys (hiddenNames ast)) then ""
else tag "strong" "Module does not export: " <> Text.intercalate ", " (map (pack . prettyDoc) $ M.keys (hiddenNames ast))
(headings, contentDefs) = unzip (map prettyDef topLevelDefs)
headings' =
if modName == "Primitives"
Expand All @@ -92,35 +90,35 @@ generateModulePage' modName title input ast =


-- Combine the data type and function definitions together
topLevelDefs = sortOn startLine $ (map Left (dataTypes ast)) <> (map Right (definitions ast))
topLevelDefs = sortOn startLine $ map Left (dataTypes ast) <> map Right (definitions ast)
startLine = fst . startPos . defSpan'
defSpan' (Left dataDecl) = dataDeclSpan dataDecl
defSpan' (Right def) = defSpan def

prettyDef (Left d) =
let (docs, heading) = scrapeDoc inputLines (dataDeclSpan d)
in (heading,
(maybe "" anchor heading)
maybe "" anchor heading
<> (codeDiv . pack . prettyDoc $ d)
<> (if strip docs == "" then miniBreak else descDiv docs))
prettyDef (Right d) =
let (docs, heading) = scrapeDoc inputLines (defSpan d)
in (heading
, (maybe "" anchor heading)
<> (codeDiv $ breakLine (internalName (defId d)) $ pack $ prettyDoc (defId d) <> " : " <> prettyDoc (defTypeScheme d))
, maybe "" anchor heading
<> codeDiv (breakLine (internalName (defId d)) $ pack $ prettyDoc (defId d) <> " : " <> prettyDoc (defTypeScheme d))
<> (if strip docs == "" then miniBreak else descDiv docs))

breakLine id xs =
if Text.length xs >= 65 && (Text.isInfixOf "forall" xs || Text.isInfixOf "exists" xs) then
case Text.break (== '.') xs of
(before, after) ->
before <> "\n" <> (Data.Text.replicate (length id + 1) " ") <> after
before <> "\n" <> Data.Text.replicate (length id + 1) " " <> after
else xs

anchor :: Text -> Text
anchor x = tagWithAttributes "a"
("name = " <> toUrlName x)
(tag "h3" ((tagWithAttributes "a" ("href='#' class='toplink'") "[top]") <> x))
(tag "h3" (tagWithAttributes "a" "href='#' class='toplink'" "[top]" <> x))


internalNav [] = ""
Expand All @@ -142,7 +140,7 @@ generateIndexPage = do
-- Generates the text of the primitives module
generatePrimitivesPage :: (?globals::Globals) => IO Text
generatePrimitivesPage = do
generateModulePage' "Primitives" "Built-in primitives" (Primitives.builtinSrc) (appendPrimitiveTys $ fst . fromRight $ parseDefs "Primitives" Primitives.builtinSrc)
generateModulePage' "Primitives" "Built-in primitives" Primitives.builtinSrc (appendPrimitiveTys $ fst . fromRight $ parseDefs "Primitives" Primitives.builtinSrc)
where
fromRight (Right x) = x
fromRight (Left x) = error x
Expand Down Expand Up @@ -174,7 +172,7 @@ generatePrimitivesPage = do
matches tyConName (id', (ty, _, _)) =
case (tyConName, resultType ty) of
(internalName -> "Type", Type 0) -> True
(a, b) -> (TyCon a) == b
(a, b) -> TyCon a == b

generateFromTemplate :: PageContext -> Text -> Text -> Text -> IO Text
generateFromTemplate ctxt modName title content = do
Expand All @@ -197,7 +195,7 @@ generateNavigatorText ctxt = do
files <- return $ sort (filter (\file -> takeExtension file == ".html" && takeBaseName file /= "Primitives") files)
-- Build a list of these links
let prefix = if ctxt == ModulePage then "" else "modules/"
let toLi file = li $ link (pack $ takeBaseName file) (prefix <> (pack $ takeBaseName file) <> ".html")
let toLi file = li $ link (pack $ takeBaseName file) (prefix <> pack (takeBaseName file) <> ".html")
-- Link to index page
let indexPrefix = if ctxt == ModulePage then "../" else ""
let topLevelLink = link "<i>Top-level</i><br />" (indexPrefix <> "index.html")
Expand Down Expand Up @@ -251,7 +249,7 @@ parsePreamble inputLines =
presentPrequelLine line =
if name == "Module" -- drop duplicate module info
then ""
else li $ (tag "b" (pack name)) <> pack info
else li $ tag "b" (pack name) <> pack info
where
(name, info) = break (== ':') (drop 4 line)
prequelLines =
Expand All @@ -265,20 +263,20 @@ parsePreamble inputLines =
-- HTML generation helpers

toUrlName :: Text -> Text
toUrlName = (replace " " "-") . (Text.filter isAlpha) . Text.toLower
toUrlName = replace " " "-" . Text.filter isAlpha . Text.toLower

section :: Text -> Text -> Text
section "" contents = tag "section" contents
section name contents = tag "section" (tag "h2" name <> contents)

codeDiv :: Text -> Text
codeDiv = tagWithAttributes "div" ("class='code'") . tag "pre"
codeDiv = tagWithAttributes "div" "class='code'" . tag "pre"

descDiv :: Text -> Text
descDiv = tagWithAttributes "div" ("class='desc'")
descDiv = tagWithAttributes "div" "class='desc'"

navDiv :: Text -> Text
navDiv = tagWithAttributes "div" ("class='mininav'")
navDiv = tagWithAttributes "div" "class='mininav'"

span :: Text -> Text -> Text
span name = tagWithAttributes "span" ("class='" <> name <> "'")
Expand Down
34 changes: 16 additions & 18 deletions interpreter/src/Language/Granule/Interpreter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -85,11 +85,11 @@ main = do
runGrOnFiles :: [FilePath] -> GrConfig -> IO ()
runGrOnFiles globPatterns config = let ?globals = grGlobals config in do
pwd <- getCurrentDirectory
results <- forM globPatterns $ \pattern -> do
paths <- glob pattern
results <- forM globPatterns $ \pat -> do
paths <- glob pat
case paths of
[] -> do
let result = Left $ NoMatchingFiles pattern
let result = Left $ NoMatchingFiles pat
printResult result
return [result]
_ -> forM paths $ \path -> do
Expand All @@ -114,7 +114,7 @@ runGrOnFiles globPatterns config = let ?globals = grGlobals config in do
result <- run config src
printResult result
return result
if all isRight (concat results) then exitSuccess else exitFailure
if all (all isRight) results then exitSuccess else exitFailure

runGrOnStdIn :: GrConfig -> IO ()
runGrOnStdIn config@GrConfig{..}
Expand Down Expand Up @@ -142,7 +142,7 @@ run
=> GrConfig
-> String
-> IO (Either InterpreterError InterpreterResult)
run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrFlags input) <> ?globals in do
run config input = let ?globals = maybe mempty grGlobals (getEmbeddedGrFlags input) <> ?globals in do
if grDocMode config
-- Generate docs mode
then do
Expand Down Expand Up @@ -175,7 +175,7 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF
let holeErrors = getHoleMessages errs
if ignoreHoles && length holeErrors == length errs && not (fromMaybe False $ globalsSynthesise ?globals)
then do
printSuccess $ "OK " ++ (blue $ "(but with " ++ show (length holeErrors) ++ " holes)")
printSuccess $ "OK " ++ blue ("(but with " ++ show (length holeErrors) ++ " holes)")
return $ Right NoEval
else
case (globalsRewriteHoles ?globals, holeErrors) of
Expand Down Expand Up @@ -209,8 +209,8 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF

where
getHoleMessages :: NonEmpty CheckerError -> [CheckerError]
getHoleMessages es =
NonEmpty.filter (\ e -> case e of HoleMessage{} -> True; _ -> False) es
getHoleMessages =
NonEmpty.filter (\case HoleMessage{} -> True; _ -> False)

runHoleSplitter :: (?globals :: Globals)
=> String
Expand Down Expand Up @@ -245,7 +245,7 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF
res <- synthesiseHoles config ast holesWithEmptyMeasurements isGradedBase
let (holes', measurements, _) = unzip3 res
when benchmarkingRawData $ do
forM_ measurements (\m -> case m of (Just m') -> putStrLn $ show m' ; _ -> return ())
forM_ measurements (\case (Just m') -> print m' ; _ -> return ())
return holes'


Expand All @@ -257,10 +257,10 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF
rest <- synthesiseHoles config astSrc holes isGradedBase

gradedExpr <- if cartSynth > 0 then getGradedExpr config defId else return Nothing
let defs' = map (\(x, (Forall tSp con bind ty)) ->
let defs' = map (\(x, Forall tSp con bind ty) ->
if cartSynth > 0
then (x, (Forall tSp con bind (toCart ty)))
else (x, (Forall tSp con bind ty))
then (x, Forall tSp con bind (toCart ty))
else (x, Forall tSp con bind ty)
) defs
let (unrestricted, restricted) = case spec of
Just (Spec _ _ _ comps) ->
Expand Down Expand Up @@ -290,7 +290,7 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF
Just (programs@(_:_), measurement) -> do
when synthHtml $ do
printSynthOutput $ uncurry synthTreeToHtml (last programs)
return $ (HoleMessage sp goal ctxt tyVars hVars synthCtxt [([], fst $ last $ programs)], measurement, attemptNo) : rest
return $ (HoleMessage sp goal ctxt tyVars hVars synthCtxt [([], fst $ last programs)], measurement, attemptNo) : rest


synthesiseHoles config ast (hole:holes) isGradedBase = do
Expand All @@ -309,23 +309,21 @@ synEval ast = do

getGradedExpr :: (?globals :: Globals) => GrConfig -> Id -> IO (Maybe (Def () ()))
getGradedExpr config def = do
let file = (fromJust $ globalsSourceFilePath ?globals) <> ".output"
let file = fromJust (globalsSourceFilePath ?globals) <> ".output"
src <- preprocess
(rewriter config)
(keepBackup config)
file
(literateEnvName config)
((AST _ defs _ _ _), _) <- parseDefsAndDoImports src
(AST _ defs _ _ _, _) <- parseDefsAndDoImports src
return $ find (\(Def _ id _ _ _ _) -> id == def) defs


-- | Get the flags embedded in the first line of a file, e.g.
-- "-- gr --no-eval"
getEmbeddedGrFlags :: String -> Maybe GrConfig
getEmbeddedGrFlags
= foldr (<|>) Nothing
. map getEmbeddedGrFlagsLine
. take 3 -- only check for flags within the top 3 lines
= foldr ((<|>) . getEmbeddedGrFlagsLine) Nothing . take 3 -- only check for flags within the top 3 lines
. filter (not . all isSpace)
. lines
where
Expand Down
Loading
Loading