Skip to content
Permalink
Browse files

Merge branch 'develop' into mariari/LLVM

  • Loading branch information...
mariari committed Nov 8, 2019
2 parents 7609386 + 6c2f941 commit 362274973e1439d1ae5df16c361fc4f564622abe
Showing with 1,489 additions and 824 deletions.
  1. +1 −0 .circleci/config.yml
  2. +4 −2 app/Config.hs
  3. +32 −66 app/Interactive.hs
  4. +1 −1 app/Main.hs
  5. +32 −0 app/Monad.hs
  6. BIN doc/reference/language-reference.pdf
  7. +317 −317 doc/reference/misc/aspell_dict
  8. +3 −3 doc/reference/src/core-language.pdc
  9. +1 −1 doc/reference/src/distributed-ledger-integration.pdc
  10. +2 −2 doc/reference/src/frontend-language.pdc
  11. +1 −1 doc/reference/src/low-level-execution-model.pdc
  12. +2 −2 doc/reference/src/reasoning.pdc
  13. +17 −7 package.yaml
  14. +8 −0 scripts/Dockerfile
  15. +39 −0 scripts/llvm-install.sh
  16. +11 −0 src/Juvix/Bohm.hs
  17. +2 −0 src/Juvix/Core.hs
  18. +16 −0 src/Juvix/Core/EAC.hs
  19. +13 −7 src/Juvix/{ → Core}/EAC/Check.hs
  20. +42 −40 src/Juvix/{EAC/EAC.hs → Core/EAC/ConstraintGen.hs}
  21. +18 −0 src/Juvix/Core/EAC/Erasure.hs
  22. +15 −2 src/Juvix/{ → Core}/EAC/Parser.hs
  23. +3 −3 src/Juvix/{ → Core}/EAC/Solve.hs
  24. +39 −63 src/Juvix/{ → Core}/EAC/Types.hs
  25. +8 −0 src/Juvix/Core/Erased.hs
  26. +38 −0 src/Juvix/Core/Erased/Evaluator.hs
  27. +21 −0 src/Juvix/Core/Erased/Types.hs
  28. +2 −81 src/Juvix/Core/Erasure.hs
  29. +88 −0 src/Juvix/Core/Erasure/Algorithm.hs
  30. +33 −0 src/Juvix/Core/Erasure/Types.hs
  31. +14 −11 src/Juvix/Core/HR/Parser.hs
  32. +11 −9 src/Juvix/Core/HR/Types.hs
  33. +114 −56 src/Juvix/Core/IR/Typechecker.hs
  34. +46 −9 src/Juvix/Core/Parameterisations/Naturals.hs
  35. +50 −0 src/Juvix/Core/Parameterisations/Unit.hs
  36. +80 −0 src/Juvix/Core/Pipeline.hs
  37. +18 −1 src/Juvix/Core/Types.hs
  38. +0 −14 src/Juvix/EAC.hs
  39. +6 −1 src/Juvix/Library.hs
  40. +1 −1 src/Juvix/Utility/HashMap.hs
  41. +1 −1 src/Juvix/Utility/PrettyPrint.hs
  42. +9 −3 stack.yaml
  43. +5 −1 test/Bohm.hs
  44. +79 −16 test/CoreParser.hs
  45. +224 −88 test/CoreTypechecker.hs
  46. +6 −6 test/EAC.hs
  47. +15 −8 test/EAC2.hs
  48. +1 −1 test/Erasure.hs
@@ -37,6 +37,7 @@ jobs:
- run:
name: Run tests
command: stack test
no_output_timeout: 1200

workflows:
version: 2.1
@@ -8,13 +8,15 @@ import Protolude

data Config
= Config
{ configTezosNode Text
{ configTezosNodeHost Text,
configTezosNodePort Int
}
deriving (Generic)

defaultConfig Config
defaultConfig = Config
{ configTezosNode = "127.0.0.1"
{ configTezosNodeHost = "127.0.0.1",
configTezosNodePort = 8732
}

loadConfig FilePath IO (Maybe Config)
@@ -8,12 +8,14 @@ import qualified Juvix.Backends.Graph as Graph
import qualified Juvix.Backends.Maps as Maps ()
import qualified Juvix.Bohm as Bohm
import qualified Juvix.Core as Core
import qualified Juvix.Core.Erased as Erased
import qualified Juvix.Core.HR as HR
import qualified Juvix.Core.HR as Core
import Juvix.Core.Parameterisations.Naturals
import qualified Juvix.EAC as EAC
import Juvix.Library
import qualified Juvix.Nets.Bohm as Bohm
import Monad
import Options
import Protolude
import qualified System.Console.Haskeline as H
import Text.PrettyPrint.ANSI.Leijen hiding ((<>))
import Prelude (String)
@@ -44,7 +46,7 @@ mainLoop func = do
mainLoop func

parseString String Maybe (Core.Term NatTy NatVal)
parseString = Core.generateParser naturals
parseString = Core.generateParser nat

handleSpecial String H.InputT IO () H.InputT IO ()
handleSpecial str cont = do
@@ -56,65 +58,35 @@ handleSpecial str cont = do
cont
'c' : 'p' : ' ' : rest do
let parsed = parseString rest
H.outputStrLn $ show parsed
cont
{-
'c' : 't' : ' ' : rest → do
let parsed = Core.parseString Core.term rest
H.outputStrLn $ show parsed
case parsed of
Just cterm → do
let eval = Core.cEval cterm []
H.outputStrLn $ show eval
Nothing → return ()
H.outputStrLn (show parsed)
cont
'c' : 'e' : ' ' : rest do
let parsed = Core.parseString Core.term rest
H.outputStrLn $ show parsed
case parsed of
Just cterm → do
eal ← eraseAndSolveCore cterm
case eal of
Right (term, _) → do
transformAndEvaluateEal True term
_ → return ()
Nothing → return ()
cont
-}
'e' : 'p' : ' ' : rest do
let parsed = EAC.parseEal rest
case parsed of
Right r transformAndEvaluateEal True r
_ return ()
cont
'e' : 'q' : ' ' : rest do
let parsed = EAC.parseEal rest
let parsed = parseString rest
H.outputStrLn (show parsed)
case parsed of
Right r transformAndEvaluateEal False r
_ return ()
Just (HR.Elim (HR.Ann usage term ty)) do
erased liftIO (exec (Core.typecheckErase term usage ty))
H.outputStrLn (show erased)
_ H.outputStrLn "must enter a valid annotated core term"
cont
'e' : 'e' : ' ' : rest do
let parsed = EAC.parseEal rest
H.outputStrLn $ show parsed
'c' : 't' : ' ' : rest do
let parsed = parseString rest
H.outputStrLn (show parsed)
case parsed of
Right r transformAndEvaluateEal True r
_ return ()
Just (HR.Elim (HR.Ann usage term ty)) do
erased liftIO (exec (Core.typecheckAffineErase term usage ty))
H.outputStrLn (show erased)
case erased of
(Right (term, _), _) do
transformAndEvaluateErasedCore True term
_ return ()
_ H.outputStrLn "must enter a valid annotated core term"
cont
_ H.outputStrLn "Unknown special command" >> cont

{-
eraseAndSolveCore ∷
Core.Term → H.InputT IO (Either EAC.Errors (EAC.RPT, EAC.ParamTypeAssignment))
eraseAndSolveCore cterm = do
let (term, typeAssignment) = Core.erase' cterm
res ← liftIO (EAC.validEal term typeAssignment)
H.outputStrLn ("Inferred EAC term & type: " <> show res)
pure res
-}

transformAndEvaluateEal Bool EAC.RPTO H.InputT IO ()
transformAndEvaluateEal debug term = do
let bohm = EAC.ealToBohm term
transformAndEvaluateErasedCore primVal. Bool Erased.Term primVal H.InputT IO ()
transformAndEvaluateErasedCore debug term = do
let bohm = Bohm.erasedCoreToBohm term
when debug $ H.outputStrLn ("Converted to BOHM: " <> show bohm)
let net Graph.FlipNet Bohm.Lang
net = Bohm.astToNet bohm Bohm.defaultEnv
@@ -129,26 +101,20 @@ transformAndEvaluateEal debug term = do

specialsDoc Doc
specialsDoc =
mconcat
[ line,
mconcat (fmap (flip (<>) line . specialDoc) specials),
line
]
mconcat [line, mconcat (fmap (flip (<>) line . specialDoc) specials), line]

specialDoc Special Doc
specialDoc (Special command helpDesc) =
text $ T.unpack $ mconcat [":", command, " - ", helpDesc]

specials [Special]
specials =
[ Special "cp [term]" "Parse a Juvix Core term",
Special "ct [term}" "Parse, typecheck, & evaluate a Juvix Core term",
[ Special "cp [term]" "Parse a core term",
Special "ce [term]" "Parse, typecheck, & erase a core term",
Special "ct [term}" "Parse, typecheck, & evaluate a core term",
Special
"ce [term"
"Parse a Juvix Core term, translate to EAC, solve constraints, evaluate & read-back",
Special "ep [term]" "Parse an EAC term",
Special "ee [term]" "Parse an EAC term, evaluate & read-back",
Special "eq [term]" "Parse an EAC term, evaluate & read-back quietly",
"cs [term"
"Parse a core term, erase it, translate it to EAC, solve constraints, evaluate & read-back",
Special "tutorial" "Embark upon an interactive tutorial",
Special "?" "Show this help message",
Special "exit" "Quit interactive mode"
@@ -65,7 +65,7 @@ interactiveDoc =
| |_| | \ V / / \| |
\___/ \_/ /_/\_\_|
|],
mconcat [line, "Juvix interactive alpha. Currently supported backends: in-process interpreter.", line, "Enter :? for help. Enter :tutorial for an interactive tutorial.", line]
mconcat [line, "Juvix interactive alpha.", line, "Currently supported backends: in-process interpreter, in-process interaction net.", line, "Coming soon: Michelson, LLVM, WASM.", line, "Enter :? for help. Enter :tutorial for an interactive tutorial.", line]
]

run Context Options IO ()
@@ -0,0 +1,32 @@
module Monad where

import Juvix.Core.Parameterisations.Naturals
import qualified Juvix.Core.Types as Core
import Juvix.Library hiding (log)

exec EnvExec NatTy NatVal a IO (Either (Core.PipelineError NatTy NatVal) a, [Core.PipelineLog NatTy NatVal])
exec (EnvE env) = do
(ret, env) runStateT (runExceptT env) (Env nat [])
pure (ret, log env)

data Env primTy primVal
= Env
{ parameterisation Core.Parameterisation primTy primVal,
log [Core.PipelineLog primTy primVal]
}
deriving (Generic)

newtype EnvExec primTy primVal a = EnvE (ExceptT (Core.PipelineError primTy primVal) (StateT (Env primTy primVal) IO) a)
deriving (Functor, Applicative, Monad, MonadIO)
deriving
( HasStream "log" [Core.PipelineLog primTy primVal],
HasWriter "log" [Core.PipelineLog primTy primVal]
)
via WriterLog (Field "log" () (MonadState (ExceptT (Core.PipelineError primTy primVal) (StateT (Env primTy primVal) IO))))
deriving
-- TODO: Should be HasReader, this library is finicky.
(HasState "parameterisation" (Core.Parameterisation primTy primVal))
via (Field "parameterisation" () (MonadState (ExceptT (Core.PipelineError primTy primVal) (StateT (Env primTy primVal) IO))))
deriving
(HasThrow "error" (Core.PipelineError primTy primVal))
via MonadError (ExceptT (Core.PipelineError primTy primVal) (StateT (Env primTy primVal) IO))
Binary file not shown.

0 comments on commit 3622749

Please sign in to comment.
You can’t perform that action at this time.