Kosmikus/contracts

jl4-core/jl4-core.cabal

@@ -31,6 +31,7 @@ library
   hs-source-dirs: src
   build-depends:
     bytestring,
+    placeholder,
     cassava,
     containers,
     data-default,
@@ -53,6 +54,7 @@ library
     text >= 2 && < 2.1.2,
     tree-diff,
     vector,
+    template-haskell,
 
   autogen-modules:
     Paths_jl4_core
@@ -71,6 +73,7 @@ library
     L4.Evaluate.Value
     L4.Evaluate.ValueLazy
     L4.EvaluateLazy
+    L4.EvaluateLazy.ContractFrame
     L4.ExactPrint
     L4.FindDefinition
     L4.HoverInfo
@@ -86,6 +89,7 @@ library
     L4.TypeCheck
     L4.TypeCheck.Annotation
     L4.TypeCheck.Environment
+    L4.TypeCheck.Environment.TH
     L4.TypeCheck.Types
     L4.TypeCheck.Unify
     L4.TypeCheck.With

jl4-core/src/Base.hs

@@ -3,6 +3,8 @@
 module Base (module X) where
 
 import Control.DeepSeq as X
+import Debug.Trace as X
+import Control.Placeholder as X
 import Control.Monad as X
 import Control.Monad.Except as X
 import Control.Monad.Identity as X

jl4-core/src/L4/Annotation.hs

@@ -14,13 +14,14 @@ import qualified Control.Monad.Extra as Extra
 import Data.Default
 import qualified Data.List.NonEmpty as NonEmpty
 import qualified GHC.Generics as GHC
-import GHC.Stack
+import GHC.Stack.CCS
 import Generics.SOP as SOP
 import Generics.SOP.Constraint
 import Generics.SOP.NP
 import Generics.SOP.NS
 import Optics.Generic
 import Optics.Operators
+import System.IO.Unsafe
 
 data NodeVisibility
   = -- | A token cluster that is hidden because it was inserted by some tool.
@@ -157,11 +158,13 @@ instance (Head xs ~ Anno' a, All c (Tail xs), xs ~ (Head xs : Tail xs)) => AnnoF
 -- ----------------------------------------------------------------------------
 
 data TraverseAnnoError
-  = InsufficientHoleFit CallStack
-  deriving (Show)
+  = InsufficientHoleFit (Maybe SrcRange) String
+  deriving stock (Show)
 
 prettyTraverseAnnoError :: TraverseAnnoError -> Text
-prettyTraverseAnnoError (InsufficientHoleFit cs) = "HoleFit requested but not enough given at: " <> Text.pack (prettyCallStack cs)
+prettyTraverseAnnoError (InsufficientHoleFit mr cs) = Text.unlines
+  [ "HoleFit requested but not enough given at: " <> prettySrcRangeM mr
+  , Text.pack cs ]
 
 toNodesEither :: ToConcreteNodes t a => a -> Either TraverseAnnoError [CsnCluster_ t]
 toNodesEither = runExcept . toNodes
@@ -193,17 +196,21 @@ instance ToConcreteNodes t a => ToConcreteNodes t (Maybe a) where
   toNodes =
     maybe (pure []) toNodes
 
-flattenConcreteNodes :: (HasCallStack, MonadError TraverseAnnoError m) => Anno_ t e -> [m [CsnCluster_ t]] -> m [CsnCluster_ t]
+flattenConcreteNodes :: (MonadError TraverseAnnoError m) => Anno_ t e -> [m [CsnCluster_ t]] -> m [CsnCluster_ t]
 flattenConcreteNodes (Anno _ _ csns) = go csns
   where
     go []                 _        = pure []
-    go (AnnoHole _ : cs)  holeFits =
+    go (AnnoHole mr : cs)  holeFits =
       case holeFits of
-        [] -> throwError $ InsufficientHoleFit callStack
+        [] -> throwInsufficientHolefit mr
         (x : xs) -> (<>) <$> x <*> go cs xs
     go (AnnoCsn _ m : cs) holeFits =
       (m :) <$> go cs holeFits
 
+{-# NOINLINE throwInsufficientHolefit #-}
+throwInsufficientHolefit :: MonadError TraverseAnnoError m => Maybe SrcRange -> m a
+throwInsufficientHolefit mr = throwError $ InsufficientHoleFit mr $ renderStack $ unsafePerformIO currentCallStack
+
 -- ----------------------------------------------------------------------------
 -- Source Range manipulation
 -- ----------------------------------------------------------------------------

jl4-core/src/L4/Evaluate.hs

@@ -355,6 +355,7 @@ evalDirective (StrictEval _ann expr) = do
   addEvalDirectiveResult expr v
 evalDirective (LazyEval _ann _expr) = pure ()
 evalDirective (Check _ _) = pure ()
+evalDirective (Contract {}) = pure ()
 
 maximumStackSize :: Int
 maximumStackSize = 50
@@ -448,6 +449,8 @@ forwardExpr env !ss stack (AppNamed ann n nes (Just order)) =
     pushExprFrame env ss stack (App ann n es)
 forwardExpr env !ss stack (IfThenElse _ann e1 e2 e3) = do
   pushEvalFrame env ss (IfThenElse1 e2 e3 env stack) e1
+forwardExpr _env !_ss stack Regulative {} = exception (RuntimeTypeError "strict evaluation of contracts is currently not supported") stack
+forwardExpr _env !_ss stack Event {} = exception (RuntimeTypeError "strict evaluation of events is currently not supported") stack
 forwardExpr env !ss stack (Consider _ann e branches) = do
   pushEvalFrame env ss (Consider1 branches env stack) e
 forwardExpr _env !ss stack (Lit _ann lit) = do

jl4-core/src/L4/Evaluate/ValueLazy.hs

@@ -43,15 +43,20 @@ data Value a =
   | ValNil
   | ValCons a a
   | ValClosure (GivenSig Resolved) (Expr Resolved) Environment
+  | ValObligation Environment MaybeEvaluated MaybeEvaluated (Maybe (Expr Resolved)) (Expr Resolved)
   | ValUnappliedConstructor Resolved
   | ValConstructor Resolved [a]
   | ValAssumed Resolved
   | ValEnvironment Environment
-  deriving stock Show
+  | ValBreached (ReasonForBreach a)
+  deriving stock (Show, Functor, Foldable, Traversable)
+
+data ReasonForBreach a = DeadlineMissed (Value a) (Value a) (Value a) Int
+  deriving stock (Generic, Show, Functor, Foldable, Traversable)
+  deriving anyclass NFData
 
 -- | This is a non-standard instance because environments can be recursive, hence we must
 -- not actually force the environments ...
---
 instance NFData a => NFData (Value a) where
   rnf :: Value a -> ()
   rnf (ValNumber i)               = rnf i
@@ -63,4 +68,9 @@ instance NFData a => NFData (Value a) where
   rnf (ValConstructor r vs)       = rnf r `seq` rnf vs
   rnf (ValAssumed r)              = rnf r
   rnf (ValEnvironment env)        = env `seq` ()
+  rnf (ValBreached ev)            = rnf ev `seq` ()
+  rnf (ValObligation env p a t f) = env `deepseq` p `deepseq` a `deepseq` t `deepseq` f `deepseq` ()
+
+type MaybeEvaluated = Either WHNF RExpr
 
+type RExpr = Expr Resolved