[ fix ] compilation

Src/Actor.hs

@@ -138,6 +138,7 @@ mangleActors opts rho tm = go tm where
   go tm = case expand tm of
     VX i de -> pure (var i (ga + de))
     AX a de -> pure (atom a (ga + de))
+    GX g a -> (G g $^) <$> go a
     a :%: b -> (%) <$> go a <*> go b
     t :-: o -> Term.contract <$> ((:-:) <$> go t <*> go o)
     t ::: o -> Term.contract <$> ((:::) <$> go t <*> go o)

Src/Actor/Display.hs

@@ -2,7 +2,7 @@
 
 module Actor.Display where
 
-import Control.Monad.Except
+import Control.Monad (forM)
 
 import qualified Data.Map as Map
 

Src/Bwd.hs

@@ -3,10 +3,14 @@ Description: snoc lists
 -}
 module Bwd where
 
+import Control.Monad (guard)
+import Control.Monad.State
+
 import Data.Map (Map)
-import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
-import Control.Monad.State
+import qualified Data.Map as Map
+
+import GHC.Stack (HasCallStack)
 
 data Bwd x = B0 | Bwd x :< x
   deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
@@ -20,9 +24,10 @@ instance Monoid (Bwd x) where
   mempty = B0
 
 -- | lookup with a more convenient name
-(<!) :: Bwd x -> Int -> x
+(<!) :: HasCallStack => Bwd x -> Int -> x
 (_  :< x) <! 0 = x
 (xs :< _) <! n = xs <! (n - 1)
+_ <! _ = error "Looking up from an empty Bwd"
 
 infixl 4 <><
 
@@ -50,26 +55,30 @@ mapzs f xz = mapzss f xz []
 
 -- | Treat a snoc list as a stack and returns the top.
 -- Warning: incomplete pattern match.
-top :: Bwd x -> x
+top :: HasCallStack => Bwd x -> x
 top (_ :< x) = x
+top _ = error "Taking the top of an empty Bwd"
 
 -- | 'takez' is 'take' but renamed so 'take' can still be used
-takez :: Bwd x -> Int -> Bwd x
+takez :: HasCallStack => Bwd x -> Int -> Bwd x
 takez _ 0 = B0
 takez (xz :< x) w = takez xz (w-1) :< x
+takez _ _ = error "Taking from an empty Bwd"
 
 -- | 'dropz' is 'drop' but renamed so 'drop' can still be used
-dropz :: Bwd x -> Int -> Bwd x
+dropz :: HasCallStack => Bwd x -> Int -> Bwd x
 dropz xz 0 = xz
 dropz (xz :< x) w = dropz xz (w-1)
+dropz _ _ = error "Dropping from an empty Bwd"
 
 -- | singleton snoc list
 singleton :: x -> Bwd x
 singleton x = B0 :< x
 
 -- | matches 'only' singleton, and will fail in not-nice ways otherwise
-only :: Bwd x -> x
+only :: HasCallStack => Bwd x -> x
 only (B0 :< x) = x
+only _ = error "Not a singleton Bwd"
 
 -- | 'focusBy' takes a predicate p and a snoc list, and returns
 -- a pointed cursor into that snoc for the first item that satisfies p
@@ -87,9 +96,10 @@ focus :: Eq x => x -> Bwd x -> Maybe (Bwd x, x, [x])
 focus x = focusBy (\ y -> y <$ guard (x == y))
 
 -- | "curl up" n items from the snoc part onto the list part
-curl :: Int -> (Bwd x, [x]) -> (Bwd x, [x])
+curl :: HasCallStack => Int -> (Bwd x, [x]) -> (Bwd x, [x])
 curl 0 xzs = xzs
 curl n (xz :< x, xs) = curl (n-1) (xz, x : xs)
+curl _ _ = error "Curling from an empty Bwd"
 
 -- | A 'Cursor' is a location in a list (or a snoc list)
 -- Note that it can point to the head or tail, it does not

Src/Command.hs

@@ -2,16 +2,16 @@
 
 module Command where
 
+import Control.Monad (when, forM_, guard)
 import Control.Applicative
-import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
 
 import Data.Bifunctor (bimap, first)
+import Data.Kind (Type)
 import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
 import Data.Traversable (for)
-import Data.Foldable (asum)
 
 import Actor
 import Actor.Display ()
@@ -45,7 +45,7 @@ import Operator.Eval (HeadUpData' (..))
 import Hide (Hide(..))
 import Scope (Scope(..))
 
-type family DEFNPROTOCOL (ph :: Phase) :: *
+type family DEFNPROTOCOL (ph :: Phase) :: Type
 type instance DEFNPROTOCOL Concrete = ()
 type instance DEFNPROTOCOL Abstract = AProtocol
 
@@ -141,6 +141,7 @@ instance Pretty CCommand where
     Go a -> keyword "exec" <+> pretty a
     Trace ts -> keyword "trace" <+> collapse (BracesList $ map pretty ts)
     Typecheck t ty -> keyword "typecheck" <+> pretty t <+> ":" <+> pretty ty
+    OpBlock _ -> undefined -- TODO
 
 instance Unelab ACommand where
   type UnelabEnv ACommand = Naming
@@ -159,6 +160,7 @@ instance Unelab ACommand where
     Go a -> Go <$> withEnv initDAEnv (unelab a)
     Trace ts -> pure $ Trace ts
     Typecheck t ty -> Typecheck <$> unelab t <*> unelab ty
+    OpBlock t -> error "Unhandled input"
 
 instance Unelab AStatement where
   type UnelabEnv AStatement = ()
@@ -333,12 +335,13 @@ scommand = \case
 
 sopBlock :: [OPENTRY Concrete] -> Elab ([OPENTRY Abstract], Globals)
 sopBlock [] = ([],) <$> asks globals
+sopBlock (DefnOp (_, [], _) : _) = error "Broken invariant"
 sopBlock (DefnOp (rp, opelims@((rpty,_,_):_), rhs) : rest) = do
   -- p : pty0 -[ opelim0 ] : pty1 -[ opelim1 ] ... : ptyn -[ opelimn ] ~> rhs
   (p, opelimz, decls, lhsTy) <- sopelims0 (getRange rp <> getRange rpty) rp opelims
   rhs <- local (setDecls decls) $ stm DontLog lhsTy rhs
   -- this is the outer op being extended
-  let op = case opelimz of (_ :< (_, op, _)) -> op
+  let op = case opelimz of { (_ :< (_, op, _)) -> op; B0 -> error "Broken invariant" }
   let cl = toClause p opelimz rhs
   (bl , gl) <- sopBlock rest
   pure (DefnOp (op, cl) : bl, gl)
@@ -358,6 +361,7 @@ sopelims :: Range
          -> Either RawP (Pat, (ASemanticsDesc, ACTm))
          -> [(RawP, OPERATOR Concrete, [RawP])]
          -> Elab (Pat, Bwd (Pat, OPERATOR Abstract, [Pat]), Decls, ASemanticsDesc)
+sopelims _ _ (Left _) [] = error "Unhandled input"
 sopelims r opelimz (Right (p, (inty, t))) [] = (p,opelimz,,inty) <$> asks declarations
 sopelims r opelimz acc ((rpty, op, args):opelims) = do
   -- We need to worry about freshening up names in operator
@@ -406,6 +410,7 @@ sopelims r opelimz acc ((rpty, op, args):opelims) = do
       (Tele desc (Scope (Hide name) tele))
       (LamP r (Scope (Hide x) rp)) =
       elabUnder (x, desc) $ sparamSemantics binder (namez :< name) tele rp
+    sparamSemantics _ _ _ _ = error "Unhandled input"
 
     -- cf. itms
     spats :: Range

Src/Concrete/Base.hs

@@ -1,14 +1,16 @@
 {-# LANGUAGE UndecidableInstances #-}
 module Concrete.Base where
 
+import Data.Bifunctor (Bifunctor (..))
 import Data.Function (on)
+import Data.Kind (Type)
 
 import Bwd
 import Format
 import Scope
 import Hide
 import Location
-import Data.Bifunctor (Bifunctor (..))
+
 
 data Variable = Variable
   { variableLoc :: Range
@@ -177,9 +179,9 @@ isSubjectMode :: Mode a -> Bool
 isSubjectMode (Subject _) = True
 isSubjectMode _           = False
 
-type family SYNTAXCAT (ph :: Phase) :: *
+type family SYNTAXCAT (ph :: Phase) :: Type
 
-type family SYNTAXDESC (ph :: Phase) :: *
+type family SYNTAXDESC (ph :: Phase) :: Type
 type instance SYNTAXDESC Concrete = Raw
 type CSyntaxDesc = SYNTAXDESC Concrete
 type ASyntaxDesc = SYNTAXDESC Abstract
@@ -205,6 +207,9 @@ data ContextStack k v = ContextStack
   , valueDesc :: v {- closed semantics desc -}
   } deriving (Show)
 
+instance Functor (ContextStack a) where
+  fmap f (ContextStack k v) = ContextStack k (f v)
+
 instance Bifunctor ContextStack where
   bimap f g (ContextStack k v) = ContextStack (f k) (g v)
 
@@ -237,20 +242,20 @@ instance Show Keyword where
 
 data Phase = Concrete | Elaboration | Abstract
 
-type family JUDGEMENTNAME (ph :: Phase) :: *
-type family CHANNEL (ph :: Phase) :: *
-type family BINDER (ph :: Phase) :: *
-type family ACTORVAR (ph :: Phase) :: *
-type family TERMVAR (ph :: Phase) :: *
-type family TERM (ph :: Phase) :: *
-type family PATTERN (ph :: Phase) :: *
-type family CONNECT (ph :: Phase) :: *
-type family STACK (ph :: Phase) :: *
-type family STACKDESC (ph :: Phase) :: *
-type family SCRUTINEEVAR (ph :: Phase) :: *
-type family SCRUTINEETERM (ph :: Phase) :: *
-type family LOOKEDUP (ph :: Phase) :: *
-type family GUARD (ph :: Phase) :: *
+type family JUDGEMENTNAME (ph :: Phase) :: Type
+type family CHANNEL (ph :: Phase) :: Type
+type family BINDER (ph :: Phase) :: Type
+type family ACTORVAR (ph :: Phase) :: Type
+type family TERMVAR (ph :: Phase) :: Type
+type family TERM (ph :: Phase) :: Type
+type family PATTERN (ph :: Phase) :: Type
+type family CONNECT (ph :: Phase) :: Type
+type family STACK (ph :: Phase) :: Type
+type family STACKDESC (ph :: Phase) :: Type
+type family SCRUTINEEVAR (ph :: Phase) :: Type
+type family SCRUTINEETERM (ph :: Phase) :: Type
+type family LOOKEDUP (ph :: Phase) :: Type
+type family GUARD (ph :: Phase) :: Type
 
 type instance JUDGEMENTNAME Concrete = Variable
 type instance CHANNEL Concrete = Variable

Src/Concrete/Pretty.hs

@@ -73,6 +73,7 @@ instance Pretty RawP where
     LamP _ (Scope x p) -> multiBindP (B0 :< x) p
     ThP _ (thxz, thd) p -> braces (hsep (pretty <$> thxz <>> []) <> pretty thd) <+> pretty p
     UnderscoreP _ -> "_"
+    Irrefutable _ p -> "~" <+> pretty p
 
 prettyCdrP :: RawP -> [Doc Annotations]
 prettyCdrP = \case

Src/Elaboration.hs

@@ -1,17 +1,18 @@
 module Elaboration where
 
-import Control.Monad.Except
+import Control.Monad (when, unless, guard, forM)
 import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Writer
 
+import Data.Bitraversable
 import Data.Function
 import Data.List (isPrefixOf)
 import qualified Data.List as List
 import qualified Data.Map as Map
-import qualified Data.Set as Set
 import Data.Maybe
-import Data.Bitraversable
+import Data.Monoid (All(..))
+import qualified Data.Set as Set
 
 import Actor
 import Bwd
@@ -45,6 +46,7 @@ import GHC.Stack.Types (HasCallStack)
 type CPattern = PATTERN Concrete
 type APattern = PATTERN Abstract
 
+dmesg :: a -> b -> b
 dmesg = const id
 
 isSubject :: EScrutinee -> IsSubject' ()
@@ -197,6 +199,7 @@ smacro xz (Op r obj opps) = do
   smacro xz obj
   smacro xz opps
 smacro xz (Guarded r t) = smacro xz t
+smacro _ _ = error "Unsupported arguments"
 
 smacros :: Bwd String -> [Assign] -> Elab (Bwd String)
 smacros xz [] = pure xz
@@ -652,6 +655,7 @@ stm usage desc rt = do
         (tdesc, t) <- itm usage rt
         compatibleInfos (getRange rt) (Known desc) (Known tdesc)
         pure t
+      _ -> error "stm: unsupported argument"
 
 senumortag :: Range -> String -> Raw -> Raw -> Elab ACTm
 senumortag r a es tds = do
@@ -849,6 +853,7 @@ spatBase isSub desc rest rp = do
         elabUnder (x, s) $
 --          local (addHint (getVariable <$> x) (Known s)) $
             spatBase isSub desc (extend rest (getVariable <$> x)) p
+      _ -> error "spatBase: unsupported argument"
 
 isObjVar :: Variable -> Elab (ASemanticsDesc, DB)
 isObjVar p = resolve p >>= \case
@@ -893,8 +898,9 @@ isContextStack stk = resolve stk >>= \case
 channelScope :: Channel -> Elab ObjVars
 channelScope (Channel ch) = do
   ds <- asks declarations
-  case fromJust (focusBy (\ (y, k) -> k <$ guard (ch == y)) ds) of
-    (_, AChannel sc, _) -> pure sc
+  case focusBy (\ (y, k) -> k <$ guard (ch == y)) ds of
+    Just (_, AChannel sc, _) -> pure sc
+    _ -> error "Broken invariant"
 
 steppingChannel :: Range -> Channel
                 -> (Direction -> [AProtocolEntry] -> Elab (a, [AProtocolEntry]))
@@ -921,6 +927,7 @@ close b r ch = do
       _ -> when b $
             -- if we cannot win, we don't care
             throwComplaint r (UnfinishedProtocol ch (Protocol ps))
+    _ -> error "Broken invariant"
   modify (channelDelete ch)
 
 withChannel :: Range -> Direction -> Channel -> AProtocol -> Elab a -> Elab a
@@ -1039,6 +1046,7 @@ sact = \case
         Subject _ -> ((SentAsSubject r ,) <$>) $ asks elabMode >>= \case
           Execution  -> pure Nothing
           Definition -> checkSendableSubject tm
+        Input -> error "Broken invariant"
 
     -- Send
     tm <- during (SendTermElaboration ch tm) $ do

Src/Elaboration/Monad.hs

@@ -2,6 +2,7 @@
 {-# OPTIONS_GHC -Wincomplete-patterns #-}
 module Elaboration.Monad where
 
+import Control.Monad (when, guard)
 import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
@@ -11,6 +12,7 @@ import Data.List.NonEmpty (NonEmpty)
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
+import Data.Monoid (All)
 
 import Actor
 import Bwd

Src/LaTeX.hs

@@ -3,10 +3,11 @@
 
 module LaTeX where
 
-import Data.Char (isDigit)
+import Control.Monad.Reader
 
+import Data.Char (isDigit)
 import qualified Data.Map as Map
-import Control.Monad.Reader
+import Data.Maybe (fromMaybe)
 
 import Concrete.Base
 import Text.PrettyPrint.Compact
@@ -112,8 +113,8 @@ instance LaTeX Raw where
       _ -> call False "typosAtom" [text a] -- as atom
     Cons _ p q -> ask >>= \ table -> case expand table d of
       Just (VEnumOrTag _ ts) -> do
-        let At _ a = p
-        let Just ds = lookup a ts
+        let a = case p of { At _ a -> a; _ -> error "Broken invariant" }
+        let ds = fromMaybe (error "Broken invariant") $ lookup a ts
         let qs = asList q
         call False (text (aTag a (length ds))) <$> traverse (uncurry toLaTeX) (zip ds qs) -- as tags
       Just (VCons dp dq) -> do
@@ -136,7 +137,9 @@ instance LaTeX Raw where
       bd <- toLaTeX () x
       pure $ call False "typosScope" [bd, sc]
     Sbst _ bwd raw -> pure ""
+    _ -> undefined -- TODO
 
+test :: IO ()
 test =
   putStrLn $
   let syntaxT = syntaxDesc ["Syntax"] in