Skip to content
Permalink
Browse files

Merge PR #185: REPL/CLI improvements

  • Loading branch information
cwgoes committed Nov 18, 2019
1 parent 2ee0a8d commit 4e99b4a6c55bb119789efe663329716390305ce3
@@ -0,0 +1,45 @@
module Compile where

import Config
import Control.Monad.IO.Class
import qualified Data.Text as T
import qualified Data.Text.IO as T
import qualified Juvix.Backends.Michelson.Compilation as M
import Juvix.Backends.Michelson.Parameterisation
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.Library
import Options
import Types

typecheck FilePath Backend IO (Erased.Term PrimVal, Erased.Type PrimTy)
typecheck fin Michelson = do
source readFile fin
let parsed = Core.generateParser michelson (T.unpack source)
case parsed of
Just (HR.Elim (HR.Ann usage term ty)) do
erased liftIO (exec (Core.typecheckErase term usage ty) michelson)
case erased of
(Right ((term, ty), typeAssignment), _)
pure (term, ty)
other do
T.putStrLn (show other)
exitFailure
err do
T.putStrLn (show err)
exitFailure
typecheck _ _ = exitFailure

compile FilePath FilePath Backend IO ()
compile fin fout backend = do
(term, ty) typecheck fin backend
let (res, logs) = M.compile term ty
case res of
Left err do
T.putStrLn (show err)
exitFailure
Right c do
T.writeFile fout (M.contractToSource c)
compile _ _ _ = exitFailure
@@ -15,10 +15,10 @@ import qualified Juvix.Interpreter.InteractionNet.Backends.Graph as Graph
import qualified Juvix.Interpreter.InteractionNet.Backends.Maps as Maps ()
import qualified Juvix.Interpreter.InteractionNet.Nets.Default as INet
import Juvix.Library
import Monad
import Options
import qualified System.Console.Haskeline as H
import Text.PrettyPrint.ANSI.Leijen hiding ((<>))
import Types
import Prelude (String)

interactive Context Config IO ()
@@ -66,7 +66,7 @@ handleSpecial str cont = do
H.outputStrLn (show parsed)
case parsed of
Just (HR.Elim (HR.Ann usage term ty)) do
erased liftIO (exec (Core.typecheckErase term usage ty))
erased liftIO (exec (Core.typecheckErase term usage ty) nat)
H.outputStrLn (show erased)
_ H.outputStrLn "must enter a valid annotated core term"
cont
@@ -75,7 +75,7 @@ handleSpecial str cont = do
H.outputStrLn (show parsed)
case parsed of
Just (HR.Elim (HR.Ann usage term ty)) do
erased liftIO (exec (Core.typecheckAffineErase term usage ty))
erased liftIO (exec (Core.typecheckAffineErase term usage ty) nat)
H.outputStrLn (show erased)
case erased of
(Right (term, _), _) do
@@ -2,6 +2,7 @@

module Main where

import Compile
import Config
import Development.GitRev
import Interactive
@@ -73,6 +74,10 @@ run ctx (Options cmd configPath) = do
maybeConfig loadConfig configPath
let conf = fromMaybe defaultConfig maybeConfig
case cmd of
Typecheck fin backend do
typecheck fin backend >> pure ()
Compile fin fout backend
compile fin fout backend
Interactive do
putDoc interactiveDoc
if isJust maybeConfig
@@ -1,7 +1,7 @@
module Options where

import Options.Applicative
import Protolude
import Protolude hiding (option)

data Context
= Context
@@ -15,10 +15,17 @@ data Options
optionsConfigPath FilePath
}

data Backend
= Unit
| Naturals
| Michelson

data Command
= Version
| Config
| Interactive
| Typecheck FilePath Backend
| Compile FilePath FilePath Backend
| Init
| Plan
| Apply
@@ -38,6 +45,8 @@ commandOptions =
<> command "init" (info initOptions (progDesc "Initialise deployment configuration"))
<> command "plan" (info planOptions (progDesc "Plan deployment"))
<> command "apply" (info applyOptions (progDesc "Execute deployment"))
<> command "typecheck" (info typecheckOptions (progDesc "Typecheck a core file"))
<> command "compile" (info compileOptions (progDesc "Compile a core file"))
)

versionOptions Parser Command
@@ -57,3 +66,25 @@ planOptions = pure Plan

applyOptions Parser Command
applyOptions = pure Apply

typecheckOptions Parser Command
typecheckOptions = Typecheck <$> fileOptions <*> backendOptions

compileOptions Parser Command
compileOptions = Compile <$> fileOptions <*> fileOptions <*> backendOptions

fileOptions Parser FilePath
fileOptions = argument str (metavar "FILE")

backendOptions Parser Backend
backendOptions =
option
( maybeReader
( \case
"unit" pure Unit
"naturals" pure Naturals
"michelson" pure Michelson
_ Nothing
)
)
(long "backend" <> short 'b' <> metavar "BACKEND" <> help "Target backend")
@@ -1,12 +1,12 @@
module Monad where
module Types 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 [])
exec EnvExec primTy primVal a Core.Parameterisation primTy primVal IO (Either (Core.PipelineError primTy primVal) a, [Core.PipelineLog primTy primVal])
exec (EnvE env) param = do
(ret, env) runStateT (runExceptT env) (Env param [])
pure (ret, log env)

data Env primTy primVal
@@ -30,3 +30,6 @@ newtype EnvExec primTy primVal a = EnvE (ExceptT (Core.PipelineError primTy prim
deriving
(HasThrow "error" (Core.PipelineError primTy primVal))
via MonadError (ExceptT (Core.PipelineError primTy primVal) (StateT (Env primTy primVal) IO))

data SomeBackend where
SomeBackend primTy primVal. Core.Parameterisation primTy primVal SomeBackend
@@ -0,0 +1 @@
@ (\x -> (+ x 2)) : 1 ([Π] 1 Nat Nat)
@@ -0,0 +1 @@
@ (\x -> x) : 1 ([Π] 1 () ())
@@ -5,18 +5,20 @@ import Juvix.Core.EAC.ConstraintGen
import Juvix.Core.EAC.Solve
import Juvix.Core.EAC.Types
import Juvix.Core.Erased.Types
import Juvix.Core.Types
import Juvix.Library hiding (link, reduce)

validEal
primTy primVal.
(Eq primTy)
Parameterisation primTy primVal
Term primVal
TypeAssignment primTy
IO (Either (Errors primTy primVal) (RPT primVal, ParamTypeAssignment primTy))
validEal term typMap = do
validEal parameterisation term typMap = do
let ((rpt, typ), env) =
execWithAssignment typMap $
generateTypeAndConstraints term
generateTypeAndConstraints parameterisation term
constraint = constraints env
-- Z3 constraint assignment
assignment getConstraints constraint
@@ -31,7 +33,7 @@ validEal term typMap = do
case bracketCheckerErr valAssignment of
Left e Left e
Right _
case typCheckerErr valAssignment typAssignment of
case typCheckerErr parameterisation valAssignment typAssignment of
Left e Left e
Right _ Right (valAssignment, typAssignment)
Nothing
@@ -41,6 +43,7 @@ assignType ∷ [Integer] → ParamTypeAssignment primTy → ParamTypeAssignment
assignType assignment typ = typ >>| placeVals
where
conMap = Map.fromList (zip [0 ..] (fromInteger <$> assignment))
placeVals (PPrimT p) = PPrimT p
placeVals (PArrT p t1 t2) = PArrT (conMap Map.! p) (placeVals t1) (placeVals t2)
placeVals (PSymT p s) = PSymT (conMap Map.! p) s

@@ -52,6 +55,7 @@ assignTerm assignment syn = placeVals syn
RBang
(conMap Map.! i)
( case t of
RPrim p RPrim p
RLam s t RLam s (placeVals t)
RApp t1 t2 RApp (placeVals t1) (placeVals t2)
RVar s RVar s
@@ -3,6 +3,7 @@ module Juvix.Core.EAC.ConstraintGen where
import Control.Arrow (left)
import Juvix.Core.EAC.Types
import Juvix.Core.Erased.Types
import Juvix.Core.Types
import Juvix.Library hiding (Type, link, reduce)
import qualified Juvix.Library.HashMap as Map
import Prelude (error)
@@ -15,6 +16,8 @@ import Prelude (error)
setOccurrenceMap m primVal. (HasState "occurrenceMap" OccurrenceMap m) Term primVal m ()
setOccurrenceMap term = do
case term of
Prim _
pure ()
Var sym
modify' @"occurrenceMap" (Map.insertWith (+) sym 1)
Lam _ b do
@@ -36,6 +39,8 @@ parameterizeType ty = do
-- Typing constraint: m >= 0
addConstraint (Constraint [ConstraintVar 1 param] (Gte 0))
case ty of
PrimTy p
pure (PPrimT p)
SymT sym
pure (PSymT param sym)
Pi arg body do
@@ -68,6 +73,7 @@ reparameterize pty = do
-- Typing constraint: m >= 0
addConstraint (Constraint [ConstraintVar 1 param] (Gte 0))
case pty of
PPrimT p pure (PPrimT p)
PSymT _ sym pure (PSymT param sym)
PArrT _ a b pure (PArrT param a b)

@@ -77,6 +83,8 @@ unificationConstraints ∷
PType primTy
PType primTy
m ()
unificationConstraints (PPrimT p1) (PPrimT p2) =
pure ()
unificationConstraints (PSymT a _) (PSymT b _) =
addConstraint (Constraint [ConstraintVar 1 a, ConstraintVar (- 1) b] (Eq 0))
unificationConstraints (PArrT a aArg aRes) (PArrT b bArg bRes) = do
@@ -97,17 +105,21 @@ boxAndTypeConstraint ∷
HasWriter "constraints" [Constraint] m,
HasState "occurrenceMap" OccurrenceMap m
)
Parameterisation primTy primVal
ParamTypeAssignment primTy
Term primVal
m (RPT primVal, PType primTy)
boxAndTypeConstraint parameterizedAssignment term = do
let rec = boxAndTypeConstraint parameterizedAssignment
boxAndTypeConstraint parameterisation parameterizedAssignment term = do
let rec = boxAndTypeConstraint parameterisation parameterizedAssignment
arrow [x] = PPrimT x
arrow (x : xs) = PArrT 0 (PPrimT x) (arrow xs)
varPaths get @"varPaths"
param addPath
path get @"path"
-- Boxing constraint.
addConstraint (Constraint (ConstraintVar 1 <$> path) (Gte 0))
case term of
Prim p pure (RBang 0 (RPrim p), arrow (typeOf parameterisation p))
Var sym do
-- Boxing constraint.
case varPaths Map.!? sym of
@@ -210,12 +222,13 @@ generateTypeAndConstraints ∷
HasWriter "constraints" [Constraint] m,
HasState "occurrenceMap" OccurrenceMap m
)
Parameterisation primTy primVal
Term primVal
m (RPT primVal, ParamTypeAssignment primTy)
generateTypeAndConstraints term = do
generateTypeAndConstraints parameterisation term = do
parameterizedAssignment parameterizeTypeAssignment
setOccurrenceMap term
boxAndTypeConstraint parameterizedAssignment term
boxAndTypeConstraint parameterisation parameterizedAssignment term
>>| second (const parameterizedAssignment)

generateConstraints
@@ -226,10 +239,11 @@ generateConstraints ∷
HasWriter "constraints" [Constraint] m,
HasState "occurrenceMap" OccurrenceMap m
)
Parameterisation primTy primVal
Term primVal
m (RPT primVal)
generateConstraints term =
generateTypeAndConstraints term
generateConstraints parameterisation term =
generateTypeAndConstraints parameterisation term
>>| fst

{- Bracket Checker. -}
@@ -252,16 +266,18 @@ bracketChecker t = runEither (rec' t 0 mempty)
RLam s t rec' t n' (Map.insert s (negate n') map)
RApp t1 t2 rec' t1 n' map >> rec' t2 n' map
RVar _ error "already is matched"
RPrim _ undefined
RPrim _ pure ()

bracketCheckerErr RPTO primVal Either (Errors primTy primVal) ()
bracketCheckerErr t = left Brack (bracketChecker t)

{- Type Checker. -}
-- Precondition ∷ all terms inside of RPTO must be unique
typChecker primTy primVal. (Eq primTy) RPTO primVal ParamTypeAssignment primTy Either (TypeErrors primTy primVal) ()
typChecker t typAssign = runEither (() <$ rec' t typAssign)
typChecker primTy primVal. (Eq primTy) Parameterisation primTy primVal RPTO primVal ParamTypeAssignment primTy Either (TypeErrors primTy primVal) ()
typChecker parameterisation t typAssign = runEither (() <$ rec' t typAssign)
where
arrow [x] = PPrimT x
arrow (x : xs) = PArrT 0 (PPrimT x) (arrow xs)
rec' (RBang bangVar (RVar s)) assign =
case assign Map.!? s of
Nothing throw @"typ" MissingOverUse
@@ -285,24 +301,27 @@ typChecker t typAssign = runEither (() <$ rec' t typAssign)
case assign Map.!? s of
Just arg pure (newAssign, PArrT x arg bodyType)
Nothing throw @"typ" MissingOverUse
rec' (RBang _bangVar (RPrim _p)) _assign = undefined
rec' (RBang _bangVar (RPrim _p)) _assign = pure (_assign, (arrow (typeOf parameterisation _p)))

typCheckerErr primTy primVal. (Eq primTy) RPTO primVal ParamTypeAssignment primTy Either (Errors primTy primVal) ()
typCheckerErr t typeAssing = left Typ (typChecker t typeAssing)
typCheckerErr primTy primVal. (Eq primTy) Parameterisation primTy primVal RPTO primVal ParamTypeAssignment primTy Either (Errors primTy primVal) ()
typCheckerErr parameterisation t typeAssign = left Typ (typChecker parameterisation t typeAssign)

{- Utility. -}

-- The outer bang parameter.
bangParam primTy. PType primTy Param
bangParam (PPrimT _) = 0
bangParam (PSymT param _) = param
bangParam (PArrT param _ _) = param

putParam primTy. Param PType primTy PType primTy
putParam _ (PPrimT p) = PPrimT p
putParam p (PSymT _ s) = PSymT p s
putParam p (PArrT _ t1 t2) = PArrT p t1 t2

-- putParamPos ∷ Param → PType → PType
addParamPos m primTy primVal. HasThrow "typ" (TypeErrors primTy primVal) m Param PType primTy m (PType primTy)
addParamPos _ (PPrimT p) = pure (PPrimT p)
addParamPos toAdd (PSymT p s)
| toAdd + p < 0 = throw @"typ" TooManyHats
| otherwise = pure (PSymT (toAdd + p) s)

0 comments on commit 4e99b4a

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