-- The scope-extension evidence on 'sinkDeclGroups' (a coercion) is its
-- soundness contract, not an argument it can consume, so GHC calls it
-- redundant. It stays.
{-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-redundant-constraints #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Declarations, sections, commands, and the public entry points.
--
-- A top-level entry is a name bound in the outermost scope, so the scope /grows/
-- as a module is checked: each @#define@, @#postulate@ and @#assume@ enters a
-- binder and the rest of the module is checked under it. The driver is therefore
-- written in continuation-passing style, and the result is packaged with the scope
-- it was produced in ('Checked').
--
-- That also gives sections their shape. A @#assume@d assumption is an ordinary
-- binder, and closing the section abstracts it out of the definitions that used it
-- (@makeAssumptionExplicit@), rewriting the later definitions to apply them to it.
module Rzk.TypeCheck.Decl where

import           Control.Monad             (forM, forM_, unless, when)
import           Control.Monad.Except      (catchError)
import           Data.Data                 (Data, cast, gmapQ)
import           Control.Monad.Reader      (ask, asks, local)
import           Data.List                 (intercalate)
import qualified Data.Map                  as Map
import qualified Data.Text                 as T
import           Debug.Trace               (trace)
import           Unsafe.Coerce             (unsafeCoerce)

import           Control.Monad.Foil        (DExt, Distinct, NameBinder)
import qualified Control.Monad.Foil        as Foil
import           Control.Monad.Free.Foil   (AST (Var), ScopedAST (..))

import           Language.Rzk.Foil.Convert (Env, toTerm)
import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names   (Binder (..), TModality (..),
                                            VarIdent, binderName, markUnresolved,
                                            patternToTerm, varIdent, varIdentAt)
import qualified Language.Rzk.Syntax       as Rzk
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Decl.Data
import           Rzk.TypeCheck.Display
import           Rzk.TypeCheck.Error
import           Rzk.TypeCheck.Eval
import           Rzk.TypeCheck.Judgements
import           Rzk.TypeCheck.MetaPrefix
import           Rzk.TypeCheck.Monad
import           Rzk.TypeCheck.Render
import           Rzk.TypeCheck.Unify       (unifyTerms)

-- * Declarations

-- FIXME: merge with VarInfo
data Decl n = Decl
  { forall (n :: S). Decl n -> VarIdent
declName         :: VarIdent
    -- ^ the surface name, as the user wrote it (with its source position)
  , forall (n :: S). Decl n -> Name n
declNameOf       :: Foil.Name n
    -- ^ the name it is bound to in the top-level scope
  , forall (n :: S). Decl n -> TermT n
declType         :: TermT n
  , forall (n :: S). Decl n -> Maybe (TermT n)
declValue        :: Maybe (TermT n)
  , forall (n :: S). Decl n -> Bool
declIsAssumption :: Bool
  , forall (n :: S). Decl n -> [Name n]
declUsedVars     :: [Foil.Name n]
  , forall (n :: S). Decl n -> Maybe LocationInfo
declLocation     :: Maybe LocationInfo
  }

-- | A declaration sinks along a scope extension by coercion, like the
-- context does (see the note in "Rzk.TypeCheck.Context"); the proof
-- obligation is discharged field by field.
instance Foil.Sinkable Decl where
  sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Decl n -> Decl l
sinkabilityProof Name n -> Name l
rename Decl n
decl = Decl n
decl
    { declNameOf = rename (declNameOf decl)
    , declType = Foil.sinkabilityProof rename (declType decl)
    , declValue = Foil.sinkabilityProof rename <$> declValue decl
    , declUsedVars = rename <$> declUsedVars decl
    }

sinkDecl :: DExt n l => Decl n -> Decl l
sinkDecl :: forall (n :: S) (l :: S). DExt n l => Decl n -> Decl l
sinkDecl = Decl n -> Decl l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink

-- | Sinking a whole list is a coercion too, with no per-element rebuild.
sinkDecls :: DExt n l => [Decl n] -> [Decl l]
sinkDecls :: forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls = [Decl n] -> [Decl l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1

-- | The per-file groups also sink by coercion. 'Foil.sink1' cannot
-- see through the pair (its element must be the sunk type itself), but the
-- sinkability argument is the same: only the declarations mention the scope.
sinkDeclGroups :: DExt n l => [(FilePath, [Decl n])] -> [(FilePath, [Decl l])]
sinkDeclGroups :: forall (n :: S) (l :: S).
DExt n l =>
[(FilePath, [Decl n])] -> [(FilePath, [Decl l])]
sinkDeclGroups = [(FilePath, [Decl n])] -> [(FilePath, [Decl l])]
forall a b. a -> b
unsafeCoerce

-- | What a run of the checker produced: the top-level scope, the declarations in
-- it, and the errors found.
--
-- The scope is existential, and the declarations live in it. Anything that wants
-- to /resume/ from a checked prefix (the LSP's incremental path) keeps the whole
-- package and carries on from that context; anything that only displays them reads
-- them through the context's naming.
data Checked where
  Checked
    :: Distinct n
    => Context n
    -> [(FilePath, [Decl n])]
    -> [TypeErrorInScopedContext]
    -> [CheckWarning]
    -> Checked

-- * Entering a top-level entry

-- | Bind a top-level entry and run the rest of the module under it.
withTopLevel
  :: Distinct n
  => VarIdent            -- ^ the surface name
  -> TermT n             -- ^ its type
  -> Maybe (TermT n)     -- ^ its value, for a definition
  -> Bool                -- ^ is it an assumption (a @#assume@)?
  -> [Foil.Name n]       -- ^ the variables it declared it uses
  -> Maybe (DataRole n)  -- ^ its role for a @#data@ declaration, if any
  -> (forall l. (DExt n l, Distinct l) => NameBinder n l -> Decl l -> TypeCheck l r)
  -> TypeCheck n r
withTopLevel :: forall (n :: S) r.
Distinct n =>
VarIdent
-> TermT n
-> Maybe (TermT n)
-> Bool
-> [Name n]
-> Maybe (DataRole n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Decl l -> TypeCheck l r)
-> TypeCheck n r
withTopLevel VarIdent
name TermT n
ty Maybe (TermT n)
mval Bool
isAssumption [Name n]
usedVars Maybe (DataRole n)
mrole forall (l :: S).
(DExt n l, Distinct l) =>
NameBinder n l -> Decl l -> TypeCheck l r
k = do
  VarIdent -> TypeCheck n ()
forall (n :: S). Distinct n => VarIdent -> TypeCheck n ()
checkTopLevelDuplicate VarIdent
name
  metaPrefix <- TermT n -> TypeCheck n Int
forall (n :: S). Distinct n => TermT n -> TypeCheck n Int
metaPrefixOf TermT n
ty
  recordMetaPrefixUses name ty mval
  ctx <- ask
  Foil.withFresh (ctxScope ctx) $ \NameBinder n l
binder -> do
    let info :: VarInfo n
info = VarInfo
          { varType :: TermT n
varType = TermT n
ty
          , varValue :: Maybe (TermT n)
varValue = Maybe (TermT n)
mval
          , varModality :: TModality
varModality = TModality
Id
          , varModAccum :: TModality
varModAccum = TModality
Id
          , varOrig :: Binder
varOrig = Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
name)
          , varIsAssumption :: Bool
varIsAssumption = Bool
isAssumption
          , varIsTopLevel :: Bool
varIsTopLevel = Bool
True
          , varDeclaredAssumptions :: [Name n]
varDeclaredAssumptions = [Name n]
usedVars
          , varLocation :: Maybe LocationInfo
varLocation = Context n -> Maybe LocationInfo
forall (n :: S). Context n -> Maybe LocationInfo
ctxLocation Context n
ctx
          , varDataRole :: Maybe (DataRole n)
varDataRole = Maybe (DataRole n)
mrole
          , varMetaPrefix :: Int
varMetaPrefix = Int
metaPrefix
          }
        ctx' :: Context l
ctx' = Name l -> Context l -> Context l
forall (n :: S). Name n -> Context n -> Context n
recordInSection (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder) (NameBinder n l
-> VarInfo n -> [ModalTope l] -> Context n -> Context l
forall (n :: S) (l :: S).
DExt n l =>
NameBinder n l
-> VarInfo n -> [ModalTope l] -> Context n -> Context l
enterBinder NameBinder n l
binder VarInfo n
info [] Context n
ctx)
        decl :: Decl l
decl = Decl
          { declName :: VarIdent
declName = VarIdent
name
          , declNameOf :: Name l
declNameOf = NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder
          , declType :: TermT l
declType = TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
ty
          , declValue :: Maybe (TermT l)
declValue = Maybe (TermT n) -> Maybe (TermT l)
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 Maybe (TermT n)
mval
          , declIsAssumption :: Bool
declIsAssumption = Bool
isAssumption
          , declUsedVars :: [Name l]
declUsedVars = [Name n] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 [Name n]
usedVars
          , declLocation :: Maybe LocationInfo
declLocation = Context n -> Maybe LocationInfo
forall (n :: S). Context n -> Maybe LocationInfo
ctxLocation Context n
ctx
          }
    Context l
-> TypeCheck l r
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) r
forall (l :: S) a (n :: S).
Context l -> TypeCheck l a -> TypeCheck n a
inContext Context l
ctx' (NameBinder n l -> Decl l -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
NameBinder n l -> Decl l -> TypeCheck l r
k NameBinder n l
binder Decl l
decl)

-- | Record a new entry in the innermost open section.
recordInSection :: Foil.Name n -> Context n -> Context n
recordInSection :: forall (n :: S). Name n -> Context n -> Context n
recordInSection Name n
name Context n
ctx = Context n
ctx
  { ctxSections = case ctxSections ctx of
      []       -> [Maybe SectionName -> [Name n] -> SectionInfo n
forall (n :: S). Maybe SectionName -> [Name n] -> SectionInfo n
SectionInfo Maybe SectionName
forall a. Maybe a
Nothing [Name n
name]]
      SectionInfo n
s : [SectionInfo n]
rest -> SectionInfo n
s { sectionEntries = name : sectionEntries s } SectionInfo n -> [SectionInfo n] -> [SectionInfo n]
forall a. a -> [a] -> [a]
: [SectionInfo n]
rest
  }

-- * Sections

startSection :: Maybe Rzk.SectionName -> TypeCheck n a -> TypeCheck n a
startSection :: forall (n :: S) a.
Maybe SectionName -> TypeCheck n a -> TypeCheck n a
startSection Maybe SectionName
name = (Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> (Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx
  { ctxSections = SectionInfo name [] : ctxSections ctx }

-- | Close a section: abstract each of its assumptions out of the definitions that
-- used it, report the ones that went unused, and take the assumptions back out of
-- scope.
--
-- The definitions stay in scope, with their entries rewritten to take the
-- assumption as an explicit parameter. The assumptions' names stay in the /scope
-- index/ — a scope only ever grows — but they are removed from the surface-name map
-- and from the list of what is in scope, so they can no longer be referred to,
-- shown, or shadowed.
endSection
  :: Distinct n
  => [TypeErrorInScopedContext]
  -> TypeCheck n ([Decl n], [TypeErrorInScopedContext], Context n)
endSection :: forall (n :: S).
Distinct n =>
[TypeErrorInScopedContext]
-> TypeCheck n ([Decl n], [TypeErrorInScopedContext], Context n)
endSection [TypeErrorInScopedContext]
errs = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  let entries = case Context n -> [SectionInfo n]
forall (n :: S). Context n -> [SectionInfo n]
ctxSections Context n
ctx of
        []    -> []
        SectionInfo n
s : [SectionInfo n]
_ -> SectionInfo n -> [Name n]
forall (n :: S). SectionInfo n -> [Name n]
sectionEntries SectionInfo n
s          -- newest first
      infos = [ (Name n
name, Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
name Context n
ctx) | Name n
name <- [Name n]
entries ]

  -- In lenient (hole-checking) mode an as-yet-unfilled hole may still come to use a
  -- declared variable, so we tolerate the unused-variable diagnostics wherever such
  -- a hole is present anywhere in the section. This covers both an unused section
  -- assumption and an unused 'uses' variable, and crucially a hole-free definition
  -- whose body refers to an in-progress (hole-bearing) one: its 'uses' reads as
  -- unused only because the referenced definition is incomplete. Strict mode (the
  -- default, and CI) keeps reporting both.
  lenient <- not <$> asks ctxHolesAreErrors
  let sectionHasHole = ((Name n, VarInfo n) -> Bool) -> [(Name n, VarInfo n)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> (TermT n -> Bool) -> Maybe (TermT n) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False TermT n -> Bool
forall (n :: S). TermT n -> Bool
containsHole (Maybe (TermT n) -> Bool)
-> ((Name n, VarInfo n) -> Maybe (TermT n))
-> (Name n, VarInfo n)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarInfo n -> Maybe (TermT n)
forall (n :: S). VarInfo n -> Maybe (TermT n)
varValue (VarInfo n -> Maybe (TermT n))
-> ((Name n, VarInfo n) -> VarInfo n)
-> (Name n, VarInfo n)
-> Maybe (TermT n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name n, VarInfo n) -> VarInfo n
forall a b. (a, b) -> b
snd) [(Name n, VarInfo n)]
infos
      tolerateUnused = Bool
lenient Bool -> Bool -> Bool
&& Bool
sectionHasHole

  (kept0, errs') <- collectSectionDecls tolerateUnused errs [] infos

  -- Abstracting over the section's assumptions rewrote the entries' types,
  -- which can change their meta-parameter prefix (an assumption such as
  -- funext becomes a leading meta parameter), so recompute it.
  kept <- forM kept0 $ \(Name n
name, VarInfo n
info) -> do
    metaPrefix <- TermT n -> TypeCheck n Int
forall (n :: S). Distinct n => TermT n -> TypeCheck n Int
metaPrefixOf (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
info)
    pure (name, info { varMetaPrefix = metaPrefix })

  loc <- asks ctxLocation
  let decls = ((Name n, VarInfo n) -> Decl n)
-> [(Name n, VarInfo n)] -> [Decl n]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe LocationInfo -> (Name n, VarInfo n) -> Decl n
forall {n :: S}.
Maybe LocationInfo -> (Name n, VarInfo n) -> Decl n
toDecl Maybe LocationInfo
loc) [(Name n, VarInfo n)]
kept
      assumptions = [ Name n
name | (Name n
name, VarInfo n
info) <- [(Name n, VarInfo n)]
infos, VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsAssumption VarInfo n
info ]
      isAssumption Name n
v = (Name n -> Bool) -> [Name n] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name n -> Name n -> Bool
forall {l :: S} {l :: S}. Name l -> Name l -> Bool
sameName Name n
v) [Name n]
assumptions
      -- the names the section's assumptions were written with, which leave scope
      assumedNames =
        [ VarIdent
x | (Name n
_, VarInfo n
info) <- [(Name n, VarInfo n)]
infos, VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsAssumption VarInfo n
info
            , Just VarIdent
x <- [Binder -> Maybe VarIdent
binderName (VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
info)] ]

      -- the definitions of the section are now abstracted over its assumptions
      ctx' = ((Name n, VarInfo n) -> Context n -> Context n)
-> Context n -> [(Name n, VarInfo n)] -> Context n
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Name n -> VarInfo n -> Context n -> Context n)
-> (Name n, VarInfo n) -> Context n -> Context n
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name n -> VarInfo n -> Context n -> Context n
forall (n :: S). Name n -> VarInfo n -> Context n -> Context n
insertVarInfo) Context n
ctx
        { ctxSections = closeInnermost (ctxSections ctx)
        , ctxBound = filter (not . isAssumption) (ctxBound ctx)
        , ctxNamed = Map.filter (not . isAssumption) (ctxNamed ctx)
        , ctxShadow = foldr Map.delete (ctxShadow ctx) assumedNames
        } [(Name n, VarInfo n)]
kept

      -- The section's definitions outlive it, so the enclosing section adopts
      -- them: closing /that/ one must see them too, and abstract them over its own
      -- assumptions in turn.
      closeInnermost [SectionInfo n]
sections = case Int -> [SectionInfo n] -> [SectionInfo n]
forall a. Int -> [a] -> [a]
drop Int
1 [SectionInfo n]
sections of
        []       -> []
        SectionInfo n
s : [SectionInfo n]
rest -> SectionInfo n
s { sectionEntries = reverse (map fst kept) <> sectionEntries s } SectionInfo n -> [SectionInfo n] -> [SectionInfo n]
forall a. a -> [a] -> [a]
: [SectionInfo n]
rest

  -- only issue unused-variable errors if there were none before in the section
  unusedErrors <- fmap concat $ forM decls $ \Decl n
decl -> do
    let unusedUsedVars :: [Name n]
unusedUsedVars = [ Name n
v | Name n
v <- Decl n -> [Name n]
forall (n :: S). Decl n -> [Name n]
declUsedVars Decl n
decl, Name n -> Bool
isAssumption Name n
v ]
    if [TypeErrorInScopedContext] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeErrorInScopedContext]
errs Bool -> Bool -> Bool
&& Bool -> Bool
not ([Name n] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name n]
unusedUsedVars) Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
tolerateUnused
      then (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Context n
c -> Context n
c { ctxLocation = declLocation decl }) (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   [TypeErrorInScopedContext]
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [TypeErrorInScopedContext])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
forall a b. (a -> b) -> a -> b
$ do
        err <- TypeError n -> TypeCheck n TypeErrorInScopedContext
forall (n :: S).
Distinct n =>
TypeError n -> TypeCheck n TypeErrorInScopedContext
typeErrorHere ([Name n] -> Name n -> TypeError n
forall (n :: S). [Name n] -> Name n -> TypeError n
TypeErrorUnusedUsedVariables [Name n]
unusedUsedVars (Decl n -> Name n
forall (n :: S). Decl n -> Name n
declNameOf Decl n
decl))
        return [err]
      else [TypeErrorInScopedContext]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []

  pure (decls, errs' <> unusedErrors, ctx')
  where
    sameName :: Name l -> Name l -> Bool
sameName Name l
a Name l
b = Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name l
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name l
b

    -- The entry records where it was declared; the section-close location is
    -- only the fallback (previously every declaration of a section carried
    -- the #end-time location, i.e. the last command's line).
    toDecl :: Maybe LocationInfo -> (Name n, VarInfo n) -> Decl n
toDecl Maybe LocationInfo
loc (Name n
name, VarInfo n
info) = Decl
      { declName :: VarIdent
declName = case VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
info of
          BinderVar (Just VarIdent
x) -> VarIdent
x
          Binder
_                  -> VarIdent
"_"
      , declNameOf :: Name n
declNameOf = Name n
name
      , declType :: TermT n
declType = VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
info
      , declValue :: Maybe (TermT n)
declValue = VarInfo n -> Maybe (TermT n)
forall (n :: S). VarInfo n -> Maybe (TermT n)
varValue VarInfo n
info
      , declIsAssumption :: Bool
declIsAssumption = VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsAssumption VarInfo n
info
      , declUsedVars :: [Name n]
declUsedVars = VarInfo n -> [Name n]
forall (n :: S). VarInfo n -> [Name n]
varDeclaredAssumptions VarInfo n
info
      , declLocation :: Maybe LocationInfo
declLocation = case VarInfo n -> Maybe LocationInfo
forall (n :: S). VarInfo n -> Maybe LocationInfo
varLocation VarInfo n
info of
          Just LocationInfo
declaredAt -> LocationInfo -> Maybe LocationInfo
forall a. a -> Maybe a
Just LocationInfo
declaredAt
          Maybe LocationInfo
Nothing         -> Maybe LocationInfo
loc
      }

-- | An error, captured in the current context (rather than thrown).
typeErrorHere :: Distinct n => TypeError n -> TypeCheck n TypeErrorInScopedContext
typeErrorHere :: forall (n :: S).
Distinct n =>
TypeError n -> TypeCheck n TypeErrorInScopedContext
typeErrorHere TypeError n
err = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  pure (TypeErrorInScopedContext ctx err)

-- | Turn the section's entries into declarations, abstracting each assumption out
-- of the definitions that follow it.
--
-- The entries come newest first, so the definitions accumulated in @recent@ are
-- exactly those that could have used the assumption currently being processed.
collectSectionDecls
  :: Distinct n
  => Bool                                -- ^ tolerate unused variables
  -> [TypeErrorInScopedContext]
  -> [(Foil.Name n, VarInfo n)]          -- ^ the definitions seen so far (oldest last)
  -> [(Foil.Name n, VarInfo n)]          -- ^ the entries still to process (newest first)
  -> TypeCheck n ([(Foil.Name n, VarInfo n)], [TypeErrorInScopedContext])
collectSectionDecls :: forall (n :: S).
Distinct n =>
Bool
-> [TypeErrorInScopedContext]
-> [(Name n, VarInfo n)]
-> [(Name n, VarInfo n)]
-> TypeCheck n ([(Name n, VarInfo n)], [TypeErrorInScopedContext])
collectSectionDecls Bool
_tolerate [TypeErrorInScopedContext]
errs [(Name n, VarInfo n)]
recent [] = ([(Name n, VarInfo n)], [TypeErrorInScopedContext])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     ([(Name n, VarInfo n)], [TypeErrorInScopedContext])
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Name n, VarInfo n)]
recent, [TypeErrorInScopedContext]
errs)
collectSectionDecls Bool
tolerate [TypeErrorInScopedContext]
errs [(Name n, VarInfo n)]
recent (entry :: (Name n, VarInfo n)
entry@(Name n
name, VarInfo n
info) : [(Name n, VarInfo n)]
rest)
  | VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsAssumption VarInfo n
info = do
      (use, recent') <- (Name n, VarInfo n)
-> [(Name n, VarInfo n)]
-> TypeCheck n (AssumptionUse, [(Name n, VarInfo n)])
forall (n :: S).
Distinct n =>
(Name n, VarInfo n)
-> [(Name n, VarInfo n)]
-> TypeCheck n (AssumptionUse, [(Name n, VarInfo n)])
makeAssumptionExplicit (Name n, VarInfo n)
entry [(Name n, VarInfo n)]
recent
      unusedErr <- case use of
        AssumptionUse
AssumptionUsed -> [TypeErrorInScopedContext]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        AssumptionUse
AssumptionUnused
          | [TypeErrorInScopedContext] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeErrorInScopedContext]
errs Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
tolerate ->
              (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Context n
c -> Context n
c { ctxLocation = varLocation info }) (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   [TypeErrorInScopedContext]
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [TypeErrorInScopedContext])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
forall a b. (a -> b) -> a -> b
$
                TypeErrorInScopedContext -> [TypeErrorInScopedContext]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeErrorInScopedContext -> [TypeErrorInScopedContext])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     TypeErrorInScopedContext
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     TypeErrorInScopedContext
forall (n :: S).
Distinct n =>
TypeError n -> TypeCheck n TypeErrorInScopedContext
typeErrorHere (Name n -> TermT n -> TypeError n
forall (n :: S). Name n -> TermT n -> TypeError n
TypeErrorUnusedVariable Name n
name (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
info))
          | Bool
otherwise -> [TypeErrorInScopedContext]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TypeErrorInScopedContext]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      collectSectionDecls tolerate (errs <> unusedErr) recent' rest
  | Bool
otherwise =
      Bool
-> [TypeErrorInScopedContext]
-> [(Name n, VarInfo n)]
-> [(Name n, VarInfo n)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     ([(Name n, VarInfo n)], [TypeErrorInScopedContext])
forall (n :: S).
Distinct n =>
Bool
-> [TypeErrorInScopedContext]
-> [(Name n, VarInfo n)]
-> [(Name n, VarInfo n)]
-> TypeCheck n ([(Name n, VarInfo n)], [TypeErrorInScopedContext])
collectSectionDecls Bool
tolerate [TypeErrorInScopedContext]
errs ((Name n, VarInfo n)
entry (Name n, VarInfo n)
-> [(Name n, VarInfo n)] -> [(Name n, VarInfo n)]
forall a. a -> [a] -> [a]
: [(Name n, VarInfo n)]
recent) [(Name n, VarInfo n)]
rest

-- | Abstract one assumption out of the definitions that come after it.
--
-- A definition that mentions the assumption gains it as an explicit parameter, and
-- every later definition that mentions /that/ definition is rewritten to apply it
-- to the assumption. A definition that mentions it without declaring it in its
-- @uses@ clause is an implicit assumption, and an error.
-- | Whether an assumption was taken up by (abstracted into) any definition
-- that followed it in its section.
data AssumptionUse = AssumptionUsed | AssumptionUnused

makeAssumptionExplicit
  :: forall n. Distinct n
  => (Foil.Name n, VarInfo n)
  -> [(Foil.Name n, VarInfo n)]
  -> TypeCheck n (AssumptionUse, [(Foil.Name n, VarInfo n)])
makeAssumptionExplicit :: forall (n :: S).
Distinct n =>
(Name n, VarInfo n)
-> [(Name n, VarInfo n)]
-> TypeCheck n (AssumptionUse, [(Name n, VarInfo n)])
makeAssumptionExplicit (Name n
a, VarInfo n
aInfo) [(Name n, VarInfo n)]
entries = do
    -- A #data family closes over a section assumption uniformly: its type
    -- former is abstracted whenever any entry of the family uses the
    -- assumption, even though the former's own type (params → U) cannot
    -- mention it. Abstracting the former rewrites every later use of it to
    -- an application, so the constructors and eliminators (which all
    -- mention the former) follow through the ordinary deep-use path; not
    -- forcing the former would leave one unparameterised type inhabited by
    -- constructors of every instantiation.
    forced <- ([[Int]] -> [Int])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[Int]]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Int]
forall a b.
(a -> b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   [[Int]]
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [Int])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[Int]]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Int]
forall a b. (a -> b) -> a -> b
$ [(Name n, VarInfo n)]
-> ((Name n, VarInfo n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         [Int])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[Int]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name n, VarInfo n)]
entries (((Name n, VarInfo n)
  -> ReaderT
       (Context n)
       (ExceptT TypeErrorInScopedContext (State CheckLog))
       [Int])
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [[Int]])
-> ((Name n, VarInfo n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         [Int])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[Int]]
forall a b. (a -> b) -> a -> b
$ \(Name n
_x, VarInfo n
xInfo) ->
      case VarInfo n -> Maybe (DataRole n)
forall (n :: S). VarInfo n -> Maybe (DataRole n)
varDataRole VarInfo n
xInfo of
        Maybe (DataRole n)
Nothing   -> [Int]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Int]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        Just DataRole n
role -> do
          inTy <- TermT n -> TypeCheck n [Name n]
forall (n :: S). TermT n -> TypeCheck n [Name n]
freeVarsDeep (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
xInfo)
          pure [ Foil.nameId (dataRoleDataType role) | a `elemName` inTy ]
    go forced entries
  where
    go :: [Int]
-> [(Name n, VarInfo n)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (AssumptionUse, [(Name n, VarInfo n)])
go [Int]
_ [] = (AssumptionUse, [(Name n, VarInfo n)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (AssumptionUse, [(Name n, VarInfo n)])
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AssumptionUse
AssumptionUnused, [])
    go [Int]
forced ((Name n
x, VarInfo n
xInfo) : [(Name n, VarInfo n)]
xs) = do
      scope <- (Context n -> Scope n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Scope n)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Scope n
forall (n :: S). Context n -> Scope n
ctxScope
      -- Two notions of use, and the difference between them is what 'implicit' means.
      -- The deep one follows the types of the variables the entry mentions, so it sees
      -- a dependency the entry never names; the shallow one is a syntactic occurrence.
      deepVars <- do
        inTy <- freeVarsDeep (varType xInfo)
        inVal <- concat <$> traverse freeVarsDeep (varValue xInfo)
        pure (inTy <> inVal)
      -- The syntactic check reads the declaration as the user wrote it, from the
      -- context — not the entry, which the assumptions abstracted before this one have
      -- already rewritten (and which therefore mentions them).
      written <- asks (lookupVarInfo x)
      let forcedFormer = Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
x Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
forced
          hasAssumption = Bool
forcedFormer Bool -> Bool -> Bool
|| Name n
a Name n -> [Name n] -> Bool
forall (n :: S). Name n -> [Name n] -> Bool
`elemName` [Name n]
deepVars
          inTypeSyntactically = Name n
a Name n -> [Name n] -> Bool
forall (n :: S). Name n -> [Name n] -> Bool
`elemName` TermT n -> [Name n]
forall (n :: S). TermT n -> [Name n]
freeVarsOfTermT (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
written)
          inBodySyntactically = (TermT n -> Bool) -> Maybe (TermT n) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name n -> [Name n] -> Bool
forall (n :: S). Name n -> [Name n] -> Bool
elemName Name n
a ([Name n] -> Bool) -> (TermT n -> [Name n]) -> TermT n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> [Name n]
forall (n :: S). TermT n -> [Name n]
freeVarsOfTermT) (VarInfo n -> Maybe (TermT n)
forall (n :: S). VarInfo n -> Maybe (TermT n)
varValue VarInfo n
written)
          declared = Name n
a Name n -> [Name n] -> Bool
forall (n :: S). Name n -> [Name n] -> Bool
`elemName` VarInfo n -> [Name n]
forall (n :: S). VarInfo n -> [Name n]
varDeclaredAssumptions VarInfo n
xInfo
          -- used, but never written down: neither in the type, nor in the body, nor in
          -- the 'uses' clause. A forced type former is exempt: the use lives in its
          -- constructors, which have their own declarations.
          implicit = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
            [ Bool
hasAssumption
            , Bool -> Bool
not (Bool
inTypeSyntactically Bool -> Bool -> Bool
|| Bool
inBodySyntactically)
            , Bool -> Bool
not Bool
declared
            , Bool -> Bool
not Bool
forcedFormer
            ]
      if hasAssumption
        then do
          when implicit $
            issueTypeError $ TypeErrorImplicitAssumption (a, varType aInfo) x
          let xInfo' = Scope n -> Name n -> VarInfo n -> VarInfo n -> VarInfo n
forall (n :: S).
Distinct n =>
Scope n -> Name n -> VarInfo n -> VarInfo n -> VarInfo n
abstractOver Scope n
scope Name n
a VarInfo n
aInfo VarInfo n
xInfo
              xs' = ((Name n, VarInfo n) -> (Name n, VarInfo n))
-> [(Name n, VarInfo n)] -> [(Name n, VarInfo n)]
forall a b. (a -> b) -> [a] -> [b]
map ((VarInfo n -> VarInfo n)
-> (Name n, VarInfo n) -> (Name n, VarInfo n)
forall a b. (a -> b) -> (Name n, a) -> (Name n, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Scope n -> Name n -> (Name n, VarInfo n) -> VarInfo n -> VarInfo n
forall (n :: S).
Distinct n =>
Scope n -> Name n -> (Name n, VarInfo n) -> VarInfo n -> VarInfo n
applyToAssumption Scope n
scope Name n
a (Name n
x, VarInfo n
xInfo'))) [(Name n, VarInfo n)]
xs
          (_use, xs'') <- go forced xs'
          return (AssumptionUsed, (x, xInfo') : xs'')
        else do
          (use, xs'') <- go forced xs
          return (use, (x, xInfo) : xs'')

-- | Give an entry the assumption as an explicit parameter.
abstractOver
  :: Distinct n
  => Foil.Scope n -> Foil.Name n -> VarInfo n -> VarInfo n -> VarInfo n
abstractOver :: forall (n :: S).
Distinct n =>
Scope n -> Name n -> VarInfo n -> VarInfo n -> VarInfo n
abstractOver Scope n
scope Name n
a VarInfo n
aInfo VarInfo n
info = VarInfo n
info
  { varType = newType
  , varValue = fmap abstractValue (varValue info)
  , varModality = Id
  , varModAccum = Id
  , varDeclaredAssumptions =
      filter (\Name n
v -> Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
a) (varDeclaredAssumptions info)
  -- All products of a #data depend on the datatype (deeply, through their
  -- types), so a section assumption is abstracted over all of them
  -- uniformly, and the spine layouts the ι-rule relies on shift together.
  , varDataRole = bumpDataRoleParams <$> varDataRole info
  }
  where
    orig :: Binder
orig = VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
aInfo
    newType :: TermT n
newType =
      Scope n
-> Name n
-> TermT n
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> TermT l -> TermT n)
-> TermT n
forall (n :: S) r.
Distinct n =>
Scope n
-> Name n
-> TermT n
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT l -> r)
-> r
abstractName Scope n
scope Name n
a (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
info) ((forall (l :: S).
  DExt n l =>
  NameBinder n l -> TermT l -> TermT n)
 -> TermT n)
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> TermT l -> TermT n)
-> TermT n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder TermT l
body ->
        Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT Binder
orig TModality
Id (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
aInfo) Maybe (ScopedTermT n)
forall a. Maybe a
Nothing (NameBinder n l -> TermT l -> ScopedTermT n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
binder TermT l
body)
    abstractValue :: TermT n -> TermT n
abstractValue TermT n
value =
      Scope n
-> Name n
-> TermT n
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> TermT l -> TermT n)
-> TermT n
forall (n :: S) r.
Distinct n =>
Scope n
-> Name n
-> TermT n
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT l -> r)
-> r
abstractName Scope n
scope Name n
a TermT n
value ((forall (l :: S).
  DExt n l =>
  NameBinder n l -> TermT l -> TermT n)
 -> TermT n)
-> (forall (l :: S).
    DExt n l =>
    NameBinder n l -> TermT l -> TermT n)
-> TermT n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder TermT l
body ->
        TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
forall (n :: S).
TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
lambdaT TermT n
newType Binder
orig Maybe (LambdaParam (ScopedTermT n) (TermT n))
forall a. Maybe a
Nothing (NameBinder n l -> TermT l -> ScopedTermT n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
binder TermT l
body)

-- | Rewrite every use of a definition into an application of it to the assumption
-- it has just been abstracted over.
applyToAssumption
  :: Distinct n
  => Foil.Scope n -> Foil.Name n -> (Foil.Name n, VarInfo n) -> VarInfo n -> VarInfo n
applyToAssumption :: forall (n :: S).
Distinct n =>
Scope n -> Name n -> (Name n, VarInfo n) -> VarInfo n -> VarInfo n
applyToAssumption Scope n
scope Name n
a (Name n
defName, VarInfo n
defInfo) VarInfo n
info
  | VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsAssumption VarInfo n
info = VarInfo n
info
  | Bool
otherwise = VarInfo n
info
      { varType = rewrite (varType info)
      , varValue = rewrite <$> varValue info
      }
  where
    applied :: TermT n
applied = TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
defInfo) (Name n -> TermT n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
defName) (Name n -> TermT n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
a)
    rewrite :: TermT n -> TermT n
rewrite = Scope n -> Name n -> TermT n -> TermT n -> TermT n
forall (n :: S).
Distinct n =>
Scope n -> Name n -> TermT n -> TermT n -> TermT n
substituteName Scope n
scope Name n
defName TermT n
applied

-- * Commands

countCommands :: Integral a => [Rzk.Command] -> a
countCommands :: forall a. Integral a => [Command] -> a
countCommands = Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> a) -> ([Command] -> Int) -> [Command] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Command] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length

setOption :: Distinct n => String -> String -> TypeCheck n a -> TypeCheck n a
setOption :: forall (n :: S) a.
Distinct n =>
FilePath -> FilePath -> TypeCheck n a -> TypeCheck n a
setOption FilePath
"verbosity" = \case
  FilePath
"debug"   -> Verbosity -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity Verbosity
Debug
  FilePath
"normal"  -> Verbosity -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity Verbosity
Normal
  FilePath
"silent"  -> Verbosity -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity Verbosity
Silent
  FilePath
_ -> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. a -> b -> a
const (TypeCheck n a -> TypeCheck n a -> TypeCheck n a)
-> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$
    TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther FilePath
"unknown verbosity level (use \"debug\", \"normal\", or \"silent\")"
setOption FilePath
"render" = \case
  FilePath
"svg"   -> Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
localRenderBackend (RenderBackend -> Maybe RenderBackend
forall a. a -> Maybe a
Just RenderBackend
RenderSVG)
  FilePath
"latex" -> Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
localRenderBackend (RenderBackend -> Maybe RenderBackend
forall a. a -> Maybe a
Just RenderBackend
RenderLaTeX)
  FilePath
"none"  -> Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
localRenderBackend Maybe RenderBackend
forall a. Maybe a
Nothing
  FilePath
_ -> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. a -> b -> a
const (TypeCheck n a -> TypeCheck n a -> TypeCheck n a)
-> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$
    TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther FilePath
"unknown render backend (use \"svg\", \"latex\", or \"none\")"
-- Render the shape only, hiding the proof term (drop the <title> everywhere and
-- blank interior labels), so a worked term can be shown as the cell it builds
-- without giving the term away.
setOption FilePath
"render-hide-term" = \case
  FilePath
"yes" -> Bool -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localHideTerm Bool
True
  FilePath
"no"  -> Bool -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localHideTerm Bool
False
  FilePath
_ -> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. a -> b -> a
const (TypeCheck n a -> TypeCheck n a -> TypeCheck n a)
-> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$
    TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther FilePath
"unknown value for \"render-hide-term\" (use \"yes\" or \"no\")"
-- The overhang hint costs a solver entailment per restriction face and recOR
-- guard, so it is off by default and opted into per module (or scope).
setOption FilePath
"warn-overhang" = \case
  FilePath
"yes" -> Bool -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localWarnOverhang Bool
True
  FilePath
"no"  -> Bool -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localWarnOverhang Bool
False
  FilePath
_ -> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. a -> b -> a
const (TypeCheck n a -> TypeCheck n a -> TypeCheck n a)
-> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$
    TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther FilePath
"unknown value for \"warn-overhang\" (use \"yes\" or \"no\")"
-- The sensitivity of the meta-parameter layer check (see
-- "Rzk.TypeCheck.MetaPrefix"); strict by default.
setOption FilePath
"warn-meta-prefix" = \case
  FilePath
"off"        -> MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
localMetaPrefixSensitivity MetaPrefixSensitivity
MetaPrefixOff
  FilePath
"structural" -> MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
localMetaPrefixSensitivity MetaPrefixSensitivity
MetaPrefixStructural
  FilePath
"strict"     -> MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
localMetaPrefixSensitivity MetaPrefixSensitivity
MetaPrefixStrict
  FilePath
_ -> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. a -> b -> a
const (TypeCheck n a -> TypeCheck n a -> TypeCheck n a)
-> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$
    TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther FilePath
"unknown value for \"warn-meta-prefix\" (use \"off\", \"structural\", or \"strict\")"
setOption FilePath
optionName = (TypeCheck n a -> TypeCheck n a)
-> FilePath -> TypeCheck n a -> TypeCheck n a
forall a b. a -> b -> a
const ((TypeCheck n a -> TypeCheck n a)
 -> FilePath -> TypeCheck n a -> TypeCheck n a)
-> (TypeCheck n a -> TypeCheck n a)
-> FilePath
-> TypeCheck n a
-> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. a -> b -> a
const (TypeCheck n a -> TypeCheck n a -> TypeCheck n a)
-> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$
  TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath
"unknown option " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
optionName)

unsetOption :: Distinct n => String -> TypeCheck n a -> TypeCheck n a
unsetOption :: forall (n :: S) a.
Distinct n =>
FilePath -> TypeCheck n a -> TypeCheck n a
unsetOption FilePath
"verbosity" = Verbosity -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity (Context 'VoidS -> Verbosity
forall (n :: S). Context n -> Verbosity
ctxVerbosity Context 'VoidS
emptyContext)
unsetOption FilePath
"render" = Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
localRenderBackend (Context 'VoidS -> Maybe RenderBackend
forall (n :: S). Context n -> Maybe RenderBackend
ctxRenderBackend Context 'VoidS
emptyContext)
unsetOption FilePath
"render-hide-term" = Bool -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localHideTerm (Context 'VoidS -> Bool
forall (n :: S). Context n -> Bool
ctxRenderHideTerm Context 'VoidS
emptyContext)
unsetOption FilePath
"warn-overhang" = Bool -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localWarnOverhang (Context 'VoidS -> Bool
forall (n :: S). Context n -> Bool
ctxWarnOverhang Context 'VoidS
emptyContext)
unsetOption FilePath
"warn-meta-prefix" =
  MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
localMetaPrefixSensitivity (Context 'VoidS -> MetaPrefixSensitivity
forall (n :: S). Context n -> MetaPrefixSensitivity
ctxMetaPrefixSensitivity Context 'VoidS
emptyContext)
unsetOption FilePath
optionName = TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. a -> b -> a
const (TypeCheck n a -> TypeCheck n a -> TypeCheck n a)
-> TypeCheck n a -> TypeCheck n a -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$
  TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath
"unknown option " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
optionName)

paramToParamDecl :: Distinct n => Rzk.Param -> TypeCheck n [Rzk.ParamDecl]
paramToParamDecl :: forall (n :: S). Distinct n => Param -> TypeCheck n [ParamDecl]
paramToParamDecl (Rzk.ParamPatternShape BNFC'Position
loc [Pattern' BNFC'Position]
pats Term' BNFC'Position
cube Term' BNFC'Position
tope) = [ParamDecl]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ParamDecl]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  [ BNFC'Position
-> Term' BNFC'Position
-> Term' BNFC'Position
-> Term' BNFC'Position
-> ParamDecl
forall a. a -> Term' a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermShape BNFC'Position
loc (Pattern' BNFC'Position -> Term' BNFC'Position
patternToTerm Pattern' BNFC'Position
pat) Term' BNFC'Position
cube Term' BNFC'Position
tope | Pattern' BNFC'Position
pat <- [Pattern' BNFC'Position]
pats]
paramToParamDecl (Rzk.ParamPatternType BNFC'Position
loc [Pattern' BNFC'Position]
pats Term' BNFC'Position
ty) = [ParamDecl]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ParamDecl]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  [ BNFC'Position
-> Term' BNFC'Position -> Term' BNFC'Position -> ParamDecl
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
loc (Pattern' BNFC'Position -> Term' BNFC'Position
patternToTerm Pattern' BNFC'Position
pat) Term' BNFC'Position
ty | Pattern' BNFC'Position
pat <- [Pattern' BNFC'Position]
pats ]
paramToParamDecl Rzk.ParamPattern{} = TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ParamDecl]
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [ParamDecl])
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ParamDecl]
forall a b. (a -> b) -> a -> b
$
  FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther FilePath
"untyped pattern in parameters"
paramToParamDecl (Rzk.ParamPatternModalType BNFC'Position
loc [Pattern' BNFC'Position]
pats ModalColon' BNFC'Position
mc Term' BNFC'Position
ty) = [ParamDecl]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ParamDecl]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  [ BNFC'Position
-> Term' BNFC'Position
-> ModalColon' BNFC'Position
-> Term' BNFC'Position
-> ParamDecl
forall a. a -> Term' a -> ModalColon' a -> Term' a -> ParamDecl' a
Rzk.ParamTermModalType BNFC'Position
loc (Pattern' BNFC'Position -> Term' BNFC'Position
patternToTerm Pattern' BNFC'Position
pat) ModalColon' BNFC'Position
mc Term' BNFC'Position
ty | Pattern' BNFC'Position
pat <- [Pattern' BNFC'Position]
pats ]
paramToParamDecl (Rzk.ParamPatternModalShape BNFC'Position
loc [Pattern' BNFC'Position]
pats ModalColon' BNFC'Position
mc Term' BNFC'Position
cube Term' BNFC'Position
tope) = [ParamDecl]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ParamDecl]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  [ BNFC'Position
-> Term' BNFC'Position
-> ModalColon' BNFC'Position
-> Term' BNFC'Position
-> Term' BNFC'Position
-> ParamDecl
forall a.
a -> Term' a -> ModalColon' a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermModalShape BNFC'Position
loc (Pattern' BNFC'Position -> Term' BNFC'Position
patternToTerm Pattern' BNFC'Position
pat) ModalColon' BNFC'Position
mc Term' BNFC'Position
cube Term' BNFC'Position
tope | Pattern' BNFC'Position
pat <- [Pattern' BNFC'Position]
pats ]

addParams :: [Rzk.Param] -> Rzk.Term -> Rzk.Term
addParams :: [Param] -> Term' BNFC'Position -> Term' BNFC'Position
addParams []     = Term' BNFC'Position -> Term' BNFC'Position
forall a. a -> a
id
addParams [Param]
params = BNFC'Position
-> [Param] -> Term' BNFC'Position -> Term' BNFC'Position
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
forall a. Maybe a
Nothing [Param]
params

-- * @#data@ declarations
--
-- A @#data@ elaborates to ordinary top-level entries: the type former, one
-- entry per constructor, and the generated eliminators @ind-D@ and @rec-D@.
-- All of them are opaque (no value); computation is the ι-rule in
-- "Rzk.TypeCheck.Eval", driven by the 'DataRole's recorded here. The types
-- of the generated entries are built as /surface/ terms and pushed through
-- the ordinary 'elaborate' and 'typecheck', so nothing here constructs core
-- terms by hand.
--
-- The declaration grammar already covers the later stages; this checker
-- rejects what it does not support (cube/shape and modal constructor
-- fields, function-typed recursive fields).

-- | The index telescope of the sort. The sort must be @U@ (no indices) or a
-- Π-telescope of plain types ending in @U@.
dataSortIndices :: Distinct n => Rzk.DataSort -> TypeCheck n [SortIndex]
dataSortIndices :: forall (n :: S). Distinct n => DataSort -> TypeCheck n [SortIndex]
dataSortIndices = \case
  Rzk.NoDataSort BNFC'Position
_        -> [SortIndex] -> TypeCheck n [SortIndex]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  Rzk.SomeDataSort BNFC'Position
_ Term' BNFC'Position
sort -> Term' BNFC'Position -> TypeCheck n [SortIndex]
go Term' BNFC'Position
sort
  where
    go :: Term' BNFC'Position -> TypeCheck n [SortIndex]
go = \case
      Rzk.Universe{} -> [SortIndex] -> TypeCheck n [SortIndex]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      Rzk.TypeFun BNFC'Position
_ ParamDecl
param Term' BNFC'Position
ret       -> (:) (SortIndex -> [SortIndex] -> [SortIndex])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     ([SortIndex] -> [SortIndex])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParamDecl
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
indexOf ParamDecl
param ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  ([SortIndex] -> [SortIndex])
-> TypeCheck n [SortIndex] -> TypeCheck n [SortIndex]
forall a b.
ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (a -> b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term' BNFC'Position -> TypeCheck n [SortIndex]
go Term' BNFC'Position
ret
      Rzk.ASCII_TypeFun BNFC'Position
_ ParamDecl
param Term' BNFC'Position
ret -> (:) (SortIndex -> [SortIndex] -> [SortIndex])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     ([SortIndex] -> [SortIndex])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParamDecl
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
indexOf ParamDecl
param ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  ([SortIndex] -> [SortIndex])
-> TypeCheck n [SortIndex] -> TypeCheck n [SortIndex]
forall a b.
ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (a -> b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term' BNFC'Position -> TypeCheck n [SortIndex]
go Term' BNFC'Position
ret
      Term' BNFC'Position
sort -> TypeError n -> TypeCheck n [SortIndex]
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n [SortIndex])
-> TypeError n -> TypeCheck n [SortIndex]
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
        FilePath
"the sort of a #data must be U, or an index telescope ending in U, got "
          FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
sort
    indexOf :: ParamDecl
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
indexOf = \case
      Rzk.ParamType BNFC'Position
_ Term' BNFC'Position
ty -> SortIndex
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe VarIdent -> Term' BNFC'Position -> SortIndex
SortIndex Maybe VarIdent
forall a. Maybe a
Nothing Term' BNFC'Position
ty)
      Rzk.ParamTermType BNFC'Position
_ (Rzk.Var BNFC'Position
_ VarIdent
v) Term' BNFC'Position
ty -> SortIndex
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe VarIdent -> Term' BNFC'Position -> SortIndex
SortIndex (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
v) Term' BNFC'Position
ty)
      Rzk.ParamTermType BNFC'Position
_ Term' BNFC'Position
pat Term' BNFC'Position
_ -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      SortIndex)
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
        FilePath
"an index binder of a #data sort must be a plain variable, got "
          FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
pat
      ParamDecl
p -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      SortIndex)
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     SortIndex
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
        FilePath
"an index of a #data sort must be a plain type, got " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> ParamDecl -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree ParamDecl
p

dataBodyParts :: Rzk.DataBody -> ([Rzk.Constructor], [Rzk.DataElim])
dataBodyParts :: DataBody -> ([Constructor], [DataElim])
dataBodyParts = \case
  Rzk.NoDataBody BNFC'Position
_              -> ([], [])
  Rzk.SomeDataBody BNFC'Position
_ [Constructor]
cons [DataElim]
elims -> ([Constructor]
cons, [DataElim]
elims)

-- | The parameters of a @#data@ must be plain typed variables @(x : A)@:
-- the constructors and eliminators apply the type former to them.
dataParamVars :: Distinct n => [Rzk.Param] -> TypeCheck n [Rzk.VarIdent]
dataParamVars :: forall (n :: S). Distinct n => [Param] -> TypeCheck n [VarIdent]
dataParamVars = ([[VarIdent]] -> [VarIdent])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[VarIdent]]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent]
forall a b.
(a -> b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[VarIdent]] -> [VarIdent]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   [[VarIdent]]
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [VarIdent])
-> ([Param]
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         [[VarIdent]])
-> [Param]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Param
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [VarIdent])
-> [Param]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[VarIdent]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Param
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent]
forall {a}.
Param' a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent' a]
paramVarsOf
  where
    paramVarsOf :: Param' a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent' a]
paramVarsOf = \case
      Rzk.ParamPatternType a
_ [Pattern' a]
pats Term' a
_ty -> [Pattern' a]
-> (Pattern' a
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (VarIdent' a))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent' a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Pattern' a]
pats ((Pattern' a
  -> ReaderT
       (Context n)
       (ExceptT TypeErrorInScopedContext (State CheckLog))
       (VarIdent' a))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [VarIdent' a])
-> (Pattern' a
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (VarIdent' a))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent' a]
forall a b. (a -> b) -> a -> b
$ \case
        Rzk.PatternVar a
_ VarIdent' a
v -> VarIdent' a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (VarIdent' a)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarIdent' a
v
        Pattern' a
pat -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (VarIdent' a)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (VarIdent' a))
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (VarIdent' a)
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
          FilePath
"a parameter of a #data must be a plain variable, got "
            FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Pattern' a -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Pattern' a
pat
      Param' a
p -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent' a]
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [VarIdent' a])
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent' a]
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
        FilePath
"a parameter of a #data must be a typed variable (x : A), got "
          FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Param' a -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Param' a
p

-- | A constructor field: a typed parameter, with cube/shape fields rejected
-- (over a directed interval they would declare directed cells, out of scope
-- for M3) and modal fields deferred (crisp induction).
dataFieldToParamDecl :: Distinct n => Rzk.VarIdent -> Rzk.Param -> TypeCheck n [Rzk.ParamDecl]
dataFieldToParamDecl :: forall (n :: S).
Distinct n =>
VarIdent -> Param -> TypeCheck n [ParamDecl]
dataFieldToParamDecl VarIdent
cname = \case
  p :: Param
p@Rzk.ParamPatternType{} -> Param -> TypeCheck n [ParamDecl]
forall (n :: S). Distinct n => Param -> TypeCheck n [ParamDecl]
paramToParamDecl Param
p
  Rzk.ParamPattern BNFC'Position
_ Pattern' BNFC'Position
pat -> TypeError n -> TypeCheck n [ParamDecl]
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n [ParamDecl])
-> TypeError n -> TypeCheck n [ParamDecl]
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
    FilePath
"untyped field " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Pattern' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Pattern' BNFC'Position
pat FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" in constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname
  Rzk.ParamPatternShape{} -> TypeError n -> TypeCheck n [ParamDecl]
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n [ParamDecl])
-> TypeError n -> TypeCheck n [ParamDecl]
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
    FilePath
"constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname
      FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" takes a cube or shape argument; over the directed interval this would declare a directed cell, which is not supported"
  Rzk.ParamPatternModalType{} -> VarIdent -> TypeCheck n [ParamDecl]
forall (n :: S) a. Distinct n => VarIdent -> TypeCheck n a
modalFieldError VarIdent
cname
  Rzk.ParamPatternModalShape{} -> VarIdent -> TypeCheck n [ParamDecl]
forall (n :: S) a. Distinct n => VarIdent -> TypeCheck n a
modalFieldError VarIdent
cname

modalFieldError :: Distinct n => Rzk.VarIdent -> TypeCheck n a
modalFieldError :: forall (n :: S) a. Distinct n => VarIdent -> TypeCheck n a
modalFieldError VarIdent
cname = TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
  FilePath
"modal fields are not supported yet in constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname

dataConSurface
  :: Distinct n
  => Rzk.VarIdent -> [Rzk.VarIdent] -> [Rzk.ParamDecl] -> Int -> Rzk.Constructor
  -> TypeCheck n DataConSurface
dataConSurface :: forall (n :: S).
Distinct n =>
VarIdent
-> [VarIdent]
-> [ParamDecl]
-> Int
-> Constructor
-> TypeCheck n DataConSurface
dataConSurface VarIdent
dataName [VarIdent]
paramVars [ParamDecl]
paramDecls Int
indexArity (Rzk.Constructor BNFC'Position
_loc VarIdent
cname [Param]
cparams ConstructorType' BNFC'Position
ctype) = do
  fieldDecls <- [[ParamDecl]] -> [ParamDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[ParamDecl]] -> [ParamDecl])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[ParamDecl]]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ParamDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Param
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [ParamDecl])
-> [Param]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[ParamDecl]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (VarIdent
-> Param
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ParamDecl]
forall (n :: S).
Distinct n =>
VarIdent -> Param -> TypeCheck n [ParamDecl]
dataFieldToParamDecl VarIdent
cname) [Param]
cparams
  let defaultRet = Term' BNFC'Position -> [Term' BNFC'Position] -> Term' BNFC'Position
surfaceApps (VarIdent -> Term' BNFC'Position
surfaceVar VarIdent
dataName) ((VarIdent -> Term' BNFC'Position)
-> [VarIdent] -> [Term' BNFC'Position]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> Term' BNFC'Position
surfaceVar [VarIdent]
paramVars)
      recIndicesOf = VarIdent
-> [VarIdent]
-> Int
-> Term' BNFC'Position
-> Maybe [Term' BNFC'Position]
dataAppliedIndices VarIdent
dataName [VarIdent]
paramVars Int
indexArity
  (ret, retIndices, sort) <- case ctype of
    Rzk.NoConstructorType BNFC'Position
_
      | Int
indexArity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term' BNFC'Position
defaultRet, [], DataConSort
DataConPoint)
      | Bool
otherwise -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Term' BNFC'Position, [Term' BNFC'Position], DataConSort))
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
          FilePath
"constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname
            FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" must spell out its return type: the family has "
            FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show Int
indexArity FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" index(es)"
    Rzk.SomeConstructorType BNFC'Position
_ Term' BNFC'Position
ret
      | Just [Term' BNFC'Position]
ixs <- Term' BNFC'Position -> Maybe [Term' BNFC'Position]
recIndicesOf Term' BNFC'Position
ret -> (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term' BNFC'Position
ret, [Term' BNFC'Position]
ixs, DataConSort
DataConPoint)
    Rzk.SomeConstructorType BNFC'Position
_ ret :: Term' BNFC'Position
ret@(Rzk.TypeId BNFC'Position
_ Term' BNFC'Position
l Term' BNFC'Position
carrier Term' BNFC'Position
r)
      | Just [Term' BNFC'Position]
_ <- Term' BNFC'Position -> Maybe [Term' BNFC'Position]
recIndicesOf Term' BNFC'Position
carrier ->
          if Int
indexArity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
            then (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term' BNFC'Position
ret, [], Term' BNFC'Position -> Term' BNFC'Position -> DataConSort
DataConPath Term' BNFC'Position
l Term' BNFC'Position
r)
            else TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Term' BNFC'Position, [Term' BNFC'Position], DataConSort))
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
              FilePath
"path constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname
                FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" in an indexed family is not supported"
      | Term' BNFC'Position -> Bool
forall {a}. Term' a -> Bool
isIdentity Term' BNFC'Position
carrier -> ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
higherPathError
    Rzk.SomeConstructorType BNFC'Position
_ (Rzk.TypeIdSimple BNFC'Position
_ Term' BNFC'Position
_ Term' BNFC'Position
_) ->
      TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Term' BNFC'Position, [Term' BNFC'Position], DataConSort))
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
        FilePath
"the return type of path constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname
          FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" must spell out the carrier of the identification, like l =_{"
          FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
defaultRet FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"} r"
    Rzk.SomeConstructorType BNFC'Position
_ Term' BNFC'Position
_ -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Term' BNFC'Position, [Term' BNFC'Position], DataConSort))
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
      FilePath
"the return type of constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname
        FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" must be the declared type applied to its parameters and "
        FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show Int
indexArity FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" index(es), like "
        FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
defaultRet FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" …"
  let fieldTypes = [ Term' BNFC'Position
ty | Rzk.ParamTermType BNFC'Position
_ Term' BNFC'Position
_ Term' BNFC'Position
ty <- [ParamDecl]
fieldDecls ]
      recursive =
        [ (Int
j, [Term' BNFC'Position]
ixs) | (Int
j, Term' BNFC'Position
ty) <- [Int] -> [Term' BNFC'Position] -> [(Int, Term' BNFC'Position)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Term' BNFC'Position]
fieldTypes, Just [Term' BNFC'Position]
ixs <- [Term' BNFC'Position -> Maybe [Term' BNFC'Position]
recIndicesOf Term' BNFC'Position
ty] ]
      isRec Term' BNFC'Position
ty = Bool
-> ([Term' BNFC'Position] -> Bool)
-> Maybe [Term' BNFC'Position]
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> [Term' BNFC'Position] -> Bool
forall a b. a -> b -> a
const Bool
True) (Term' BNFC'Position -> Maybe [Term' BNFC'Position]
recIndicesOf Term' BNFC'Position
ty)
      nonRecTypes = [ Term' BNFC'Position
ty | Term' BNFC'Position
ty <- [Term' BNFC'Position]
fieldTypes, Bool -> Bool
not (Term' BNFC'Position -> Bool
isRec Term' BNFC'Position
ty) ]
      nonRecDecls = [ ParamDecl
d | d :: ParamDecl
d@(Rzk.ParamTermType BNFC'Position
_ Term' BNFC'Position
_ Term' BNFC'Position
ty) <- [ParamDecl]
fieldDecls, Bool -> Bool
not (Term' BNFC'Position -> Bool
isRec Term' BNFC'Position
ty) ]
  forM_ fieldTypes $ \case
    fieldTy :: Term' BNFC'Position
fieldTy@(Rzk.TypeId BNFC'Position
_ Term' BNFC'Position
_ Term' BNFC'Position
carrier Term' BNFC'Position
_)
      | VarIdent -> [VarIdent] -> Int -> Term' BNFC'Position -> Bool
matchesDataApplied VarIdent
dataName [VarIdent]
paramVars Int
indexArity Term' BNFC'Position
carrier ->
          TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
            FilePath
"constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname
              FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" has a field of an identity type over the declared type ("
              FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
fieldTy
              FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"); higher paths are not supported yet"
    Term' BNFC'Position
_ -> ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  pure DataConSurface
    { dataConName = cname
    , dataConFields = fieldDecls
    , dataConFieldPats = concatMap fieldPats cparams
    , dataConRecursive = recursive
    , dataConRetIndices = retIndices
    , dataConType = addParamDecls (paramDecls <> fieldDecls) ret
    , dataConProbe = addParamDecls nonRecDecls (Rzk.TypeUnit Nothing)
    , dataConNonRec = nonRecTypes
    , dataConLocalNames = identTokenOf cname
        : map identTokenOf (concatMap fieldVars cparams)
    , dataConSort = sort
    }
  where
    fieldVars :: Param -> [VarIdent]
fieldVars = \case
      Rzk.ParamPatternType BNFC'Position
_ [Pattern' BNFC'Position]
pats Term' BNFC'Position
_ -> (Pattern' BNFC'Position -> [VarIdent])
-> [Pattern' BNFC'Position] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern' BNFC'Position -> [VarIdent]
surfacePatternVars [Pattern' BNFC'Position]
pats
      Param
_                             -> []
    fieldPats :: Param -> [Term' BNFC'Position]
fieldPats = \case
      Rzk.ParamPatternType BNFC'Position
_ [Pattern' BNFC'Position]
pats Term' BNFC'Position
_ -> (Pattern' BNFC'Position -> Term' BNFC'Position)
-> [Pattern' BNFC'Position] -> [Term' BNFC'Position]
forall a b. (a -> b) -> [a] -> [b]
map Pattern' BNFC'Position -> Term' BNFC'Position
patternToTerm [Pattern' BNFC'Position]
pats
      Param
_                             -> []
    isIdentity :: Term' a -> Bool
isIdentity = \case
      Rzk.TypeId{}       -> Bool
True
      Rzk.TypeIdSimple{} -> Bool
True
      Term' a
_                  -> Bool
False
    higherPathError :: ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
higherPathError = TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Term' BNFC'Position, [Term' BNFC'Position], DataConSort))
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position, [Term' BNFC'Position], DataConSort)
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
      FilePath
"constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
cname
        FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" declares a path between paths; higher path constructors are not supported yet"

-- | The assumptions an entry depends on, possibly only through the types of
-- what it mentions. The generated entries of a @#data@ declare these
-- dependencies, so that closing a section abstracts the assumption over all
-- of them uniformly instead of reporting an implicit assumption.
assumptionDepsOf :: TermT n -> TypeCheck n [Foil.Name n]
assumptionDepsOf :: forall (n :: S). TermT n -> TypeCheck n [Name n]
assumptionDepsOf TermT n
ty = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  deep <- freeVarsDeep ty
  pure [ v | v <- deep, varIsAssumption (lookupVarInfo v ctx) ]

-- | Several distinct fresh identifiers with a shared base.
freshIdents
  :: Int -> [Rzk.VarIdentToken] -> T.Text -> TypeCheck n [Rzk.VarIdent]
freshIdents :: forall (n :: S).
Int -> [VarIdentToken] -> Text -> TypeCheck n [VarIdent]
freshIdents Int
n [VarIdentToken]
avoid Text
base = Int
-> [VarIdentToken]
-> [VarIdent]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent]
go Int
n [VarIdentToken]
avoid []
  where
    go :: Int
-> [VarIdentToken]
-> [VarIdent]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent]
go Int
0 [VarIdentToken]
_ [VarIdent]
acc = [VarIdent]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VarIdent] -> [VarIdent]
forall a. [a] -> [a]
reverse [VarIdent]
acc)
    go Int
k [VarIdentToken]
avoidNow [VarIdent]
acc = do
      ident <- Maybe FilePath -> [VarIdentToken] -> Text -> TypeCheck n VarIdent
forall (n :: S).
Maybe FilePath -> [VarIdentToken] -> Text -> TypeCheck n VarIdent
freshIdent Maybe FilePath
forall a. Maybe a
Nothing [VarIdentToken]
avoidNow Text
base
      go (k - 1) (identTokenOf ident : avoidNow) (ident : acc)

-- | An identifier that is neither bound at the top level nor among the given
-- local binder tokens; primes are appended until one is free. Used for the
-- motive and scrutinee binders of the generated eliminator types, which
-- close over the user's field types.
freshIdent
  :: Maybe FilePath -> [Rzk.VarIdentToken] -> T.Text -> TypeCheck n Rzk.VarIdent
freshIdent :: forall (n :: S).
Maybe FilePath -> [VarIdentToken] -> Text -> TypeCheck n VarIdent
freshIdent Maybe FilePath
path [VarIdentToken]
avoid Text
base = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  let candidates =
        [ BNFC'Position -> VarIdentToken -> VarIdent
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent BNFC'Position
forall a. Maybe a
Nothing (Text -> VarIdentToken
Rzk.VarIdentToken (Text
base Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text -> Text
T.replicate Int
p Text
"'"))
        | Int
p <- [Int
0 ..] ]
      isFree VarIdent
cand = VarIdent -> VarIdentToken
identTokenOf VarIdent
cand VarIdentToken -> [VarIdentToken] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VarIdentToken]
avoid
        Bool -> Bool -> Bool
&& case VarIdent -> Context n -> Maybe (Name n)
forall (n :: S). VarIdent -> Context n -> Maybe (Name n)
lookupNamed (Maybe FilePath -> VarIdent -> VarIdent
varIdentAt Maybe FilePath
path VarIdent
cand) Context n
ctx of
             Maybe (Name n)
Nothing -> Bool
True
             Just Name n
_  -> Bool
False
  case filter isFree candidates of
    VarIdent
cand : [VarIdent]
_ -> VarIdent
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     VarIdent
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarIdent
cand
    []       -> FilePath
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     VarIdent
forall a. FilePath -> a
panicImpossible FilePath
"no fresh identifier candidate"

-- | Bind the products of one @#data@ declaration: the type former, the
-- constructors (checked in a scope where the type former exists), and the
-- generated eliminators @ind-D@ and @rec-D@.
withDataDecls
  :: forall n r. Distinct n
  => Maybe FilePath
  -> [Foil.Name n]        -- ^ the declared used variables
  -> Rzk.VarIdent         -- ^ the datatype name (surface)
  -> [Rzk.VarIdent]       -- ^ the parameter variables
  -> [Rzk.ParamDecl]      -- ^ the parameter telescope
  -> [SortIndex]          -- ^ the index telescope of the sort
  -> [DataConSurface]     -- ^ the constructors, preprocessed
  -> [Rzk.DataElim]       -- ^ the re-ascription clauses
  -> (forall l. (DExt n l, Distinct l) => [Decl l] -> TypeCheck l r)
  -> TypeCheck n r
withDataDecls :: forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> [Name n]
-> VarIdent
-> [VarIdent]
-> [ParamDecl]
-> [SortIndex]
-> [DataConSurface]
-> [DataElim]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> TypeCheck l r)
-> TypeCheck n r
withDataDecls Maybe FilePath
path [Name n]
used VarIdent
name [VarIdent]
paramVars [ParamDecl]
paramDecls [SortIndex]
sortIndices [DataConSurface]
consData [DataElim]
elims forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> TypeCheck l r
k = do
  -- The type former's type spells the sort as written: params → indices → U.
  let sortTerm :: Term' BNFC'Position
sortTerm = (SortIndex -> Term' BNFC'Position -> Term' BNFC'Position)
-> Term' BNFC'Position -> [SortIndex] -> Term' BNFC'Position
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SortIndex -> Term' BNFC'Position -> Term' BNFC'Position
wrapIndex (BNFC'Position -> Term' BNFC'Position
forall a. a -> Term' a
Rzk.Universe BNFC'Position
forall a. Maybe a
Nothing) [SortIndex]
sortIndices
      wrapIndex :: SortIndex -> Term' BNFC'Position -> Term' BNFC'Position
wrapIndex (SortIndex Maybe VarIdent
mv Term' BNFC'Position
ty) Term' BNFC'Position
body = case Maybe VarIdent
mv of
        Just VarIdent
v  -> VarIdent
-> Term' BNFC'Position
-> Term' BNFC'Position
-> Term' BNFC'Position
surfacePi VarIdent
v Term' BNFC'Position
ty Term' BNFC'Position
body
        Maybe VarIdent
Nothing -> Term' BNFC'Position -> Term' BNFC'Position -> Term' BNFC'Position
surfaceArrow Term' BNFC'Position
ty Term' BNFC'Position
body
  dTyTerm <- Term' BNFC'Position -> TypeCheck n (Term n)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate ([ParamDecl] -> Term' BNFC'Position -> Term' BNFC'Position
addParamDecls [ParamDecl]
paramDecls Term' BNFC'Position
sortTerm)
  dTy <- memoizeWHNF =<< typecheck dTyTerm universeT
  dDeps <- assumptionDepsOf dTy
  withTopLevel (varIdentAt path name) dTy Nothing False
    (nubNames (used <> dDeps)) Nothing $ \NameBinder n l
dBinder Decl l
dDecl ->
      Name l
-> [Name l]
-> Int
-> [DataConSurface]
-> [Decl l]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    Name l -> [Name l] -> [Decl l] -> TypeCheck l r)
-> TypeCheck l r
forall (m :: S).
DExt n m =>
Name m
-> [Name m]
-> Int
-> [DataConSurface]
-> [Decl m]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    Name l -> [Name l] -> [Decl l] -> TypeCheck l r)
-> TypeCheck m r
bindCons (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
dBinder) ([Name n] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 [Name n]
used) Int
0 [DataConSurface]
consData [Decl l -> Decl l
forall (n :: S) (l :: S). DExt n l => Decl n -> Decl l
sinkDecl Decl l
dDecl] ((forall (l :: S).
  (DExt n l, Distinct l) =>
  Name l -> [Name l] -> [Decl l] -> TypeCheck l r)
 -> TypeCheck l r)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    Name l -> [Name l] -> [Decl l] -> TypeCheck l r)
-> TypeCheck l r
forall a b. (a -> b) -> a -> b
$
        \Name l
dName [Name l]
usedL [Decl l]
declsAcc -> Name l -> [Name l] -> [Decl l] -> TypeCheck l r
forall (m :: S).
DExt n m =>
Name m -> [Name m] -> [Decl m] -> TypeCheck m r
bindElims Name l
dName [Name l]
usedL [Decl l]
declsAcc
  where
    numParams :: Int
numParams  = [ParamDecl] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ParamDecl]
paramDecls
    numMethods :: Int
numMethods = [DataConSurface] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DataConSurface]
consData
    indexArity :: Int
indexArity = [SortIndex] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SortIndex]
sortIndices

    bindCons
      :: forall m. DExt n m
      => Foil.Name m -> [Foil.Name m] -> Int -> [DataConSurface] -> [Decl m]
      -> (forall l. (DExt n l, Distinct l)
            => Foil.Name l -> [Foil.Name l] -> [Decl l] -> TypeCheck l r)
      -> TypeCheck m r
    bindCons :: forall (m :: S).
DExt n m =>
Name m
-> [Name m]
-> Int
-> [DataConSurface]
-> [Decl m]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    Name l -> [Name l] -> [Decl l] -> TypeCheck l r)
-> TypeCheck m r
bindCons Name m
dName [Name m]
usedHere Int
_index [] [Decl m]
acc forall (l :: S).
(DExt n l, Distinct l) =>
Name l -> [Name l] -> [Decl l] -> TypeCheck l r
kk = Name m -> [Name m] -> [Decl m] -> TypeCheck m r
forall (l :: S).
(DExt n l, Distinct l) =>
Name l -> [Name l] -> [Decl l] -> TypeCheck l r
kk Name m
dName [Name m]
usedHere [Decl m]
acc
    bindCons Name m
dName [Name m]
usedHere Int
index (DataConSurface
con : [DataConSurface]
rest) [Decl m]
acc forall (l :: S).
(DExt n l, Distinct l) =>
Name l -> [Name l] -> [Decl l] -> TypeCheck l r
kk = do
      -- Directly recursive fields (type = the declared type applied to its
      -- parameters) are recognised syntactically and excluded from the
      -- probe; any other occurrence of the type in a field is an error.
      let dOccursIn :: Term m -> Bool
dOccursIn Term m
t = (Name m -> Bool) -> [Name m] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Name m -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name m
dName) (Int -> Bool) -> (Name m -> Int) -> Name m -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name m -> Int
forall (l :: S). Name l -> Int
Foil.nameId) (Term m -> [Name m]
forall (n :: S). Term n -> [Name n]
freeVarsOfTerm Term m
t)
      probeT <- Term' BNFC'Position -> TypeCheck m (Term m)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate (DataConSurface -> Term' BNFC'Position
dataConProbe DataConSurface
con)
      when (dOccursIn probeT) $ do
        -- Locate the offending field for a precise message: a positive but
        -- function-typed recursive field is meaningful and merely
        -- unsupported; anything else violates strict positivity.
        offending <- forM (dataConNonRec con) $ \Term' BNFC'Position
ty -> do
          t <- Term' BNFC'Position -> TypeCheck m (Term m)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate Term' BNFC'Position
ty
          pure (ty, dOccursIn t)
        funRec <- case [ ty | (ty, True) <- offending ] of
          Term' BNFC'Position
ty : [Term' BNFC'Position]
_ -> do
            let ([Term' BNFC'Position]
domains, Term' BNFC'Position
codomain) = Term' BNFC'Position -> ([Term' BNFC'Position], Term' BNFC'Position)
surfacePiSpine Term' BNFC'Position
ty
            domainsClean <- (Term' BNFC'Position
 -> ReaderT
      (Context m)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Bool)
-> [Term' BNFC'Position]
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Term m -> Bool)
-> TypeCheck m (Term m)
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a b.
(a -> b)
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool) -> (Term m -> Bool) -> Term m -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term m -> Bool
dOccursIn) (TypeCheck m (Term m)
 -> ReaderT
      (Context m)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Bool)
-> (Term' BNFC'Position -> TypeCheck m (Term m))
-> Term' BNFC'Position
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term' BNFC'Position -> TypeCheck m (Term m)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate) [Term' BNFC'Position]
domains
            pure (matchesDataApplied name paramVars indexArity codomain && and domainsClean)
          [] -> Bool
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
        issueTypeError $ TypeErrorOther $ if funRec
          then "constructor " <> Rzk.printTree (dataConName con)
            <> " has a function-typed recursive field; only directly recursive fields are supported for now"
          else "constructor " <> Rzk.printTree (dataConName con)
            <> " is not strictly positive: the declared type may occur in a field only as the type of the whole field"
      when (containsUniverse probeT) $ do
        loc <- asks ctxLocation
        recordCheckWarning $ LargeInductiveTypeWarning
          (varIdentAt path name)
          (varIdentAt path (dataConName con))
          loc
      conTyTerm <- elaborate (dataConType con)
      conTy <- memoizeWHNF =<< typecheck conTyTerm universeT
      conDeps <- assumptionDepsOf conTy
      let conSort = case DataConSurface -> DataConSort
dataConSort DataConSurface
con of
            DataConSort
DataConPoint  -> ConSort
PointCon
            DataConPath{} -> ConSort
PathCon
          role = Name m -> Int -> DataRoleKind -> DataRole m
forall (n :: S). Name n -> Int -> DataRoleKind -> DataRole n
DataRole Name m
dName Int
numParams
            (ConSort -> Int -> Int -> [Int] -> DataRoleKind
DataConKind ConSort
conSort Int
index ([ParamDecl] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataConSurface -> [ParamDecl]
dataConFields DataConSurface
con))
              (((Int, [Term' BNFC'Position]) -> Int)
-> [(Int, [Term' BNFC'Position])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [Term' BNFC'Position]) -> Int
forall a b. (a, b) -> a
fst (DataConSurface -> [(Int, [Term' BNFC'Position])]
dataConRecursive DataConSurface
con)))
      withTopLevel (varIdentAt path (dataConName con)) conTy Nothing False
        (nubNames (usedHere <> conDeps)) (Just role) $ \NameBinder m l
_conBinder Decl l
conDecl ->
          Name l
-> [Name l]
-> Int
-> [DataConSurface]
-> [Decl l]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    Name l -> [Name l] -> [Decl l] -> TypeCheck l r)
-> TypeCheck l r
forall (m :: S).
DExt n m =>
Name m
-> [Name m]
-> Int
-> [DataConSurface]
-> [Decl m]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    Name l -> [Name l] -> [Decl l] -> TypeCheck l r)
-> TypeCheck m r
bindCons (Name m -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Name m
dName) ([Name m] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 [Name m]
usedHere) (Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [DataConSurface]
rest
            ([Decl m] -> [Decl l]
forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls [Decl m]
acc [Decl l] -> [Decl l] -> [Decl l]
forall a. Semigroup a => a -> a -> a
<> [Decl l
conDecl]) Name l -> [Name l] -> [Decl l] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
Name l -> [Name l] -> [Decl l] -> TypeCheck l r
kk

    bindElims
      :: forall m. DExt n m
      => Foil.Name m -> [Foil.Name m] -> [Decl m] -> TypeCheck m r
    bindElims :: forall (m :: S).
DExt n m =>
Name m -> [Name m] -> [Decl m] -> TypeCheck m r
bindElims Name m
dName [Name m]
usedHere [Decl m]
declsAcc = do
      let avoid :: [VarIdentToken]
avoid = VarIdent -> VarIdentToken
identTokenOf VarIdent
name
            VarIdentToken -> [VarIdentToken] -> [VarIdentToken]
forall a. a -> [a] -> [a]
: (VarIdent -> VarIdentToken) -> [VarIdent] -> [VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> VarIdentToken
identTokenOf [VarIdent]
paramVars
            [VarIdentToken] -> [VarIdentToken] -> [VarIdentToken]
forall a. Semigroup a => a -> a -> a
<> [ VarIdent -> VarIdentToken
identTokenOf VarIdent
v | SortIndex (Just VarIdent
v) Term' BNFC'Position
_ <- [SortIndex]
sortIndices ]
            [VarIdentToken] -> [VarIdentToken] -> [VarIdentToken]
forall a. Semigroup a => a -> a -> a
<> (DataConSurface -> [VarIdentToken])
-> [DataConSurface] -> [VarIdentToken]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataConSurface -> [VarIdentToken]
dataConLocalNames [DataConSurface]
consData
      -- Anonymous indices of the sort get fresh names; named ones keep the
      -- user's spelling (later index types may depend on them).
      freshIx <- Int -> [VarIdentToken] -> Text -> TypeCheck m [VarIdent]
forall (n :: S).
Int -> [VarIdentToken] -> Text -> TypeCheck n [VarIdent]
freshIdents ([()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ () | SortIndex Maybe VarIdent
Nothing Term' BNFC'Position
_ <- [SortIndex]
sortIndices ]) [VarIdentToken]
avoid Text
"i"
      let indexVars = [SortIndex] -> [VarIdent] -> [VarIdent]
go [SortIndex]
sortIndices [VarIdent]
freshIx
            where
              go :: [SortIndex] -> [VarIdent] -> [VarIdent]
go [] [VarIdent]
_ = []
              go (SortIndex (Just VarIdent
v) Term' BNFC'Position
_ : [SortIndex]
rest) [VarIdent]
fresh = VarIdent
v VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [SortIndex] -> [VarIdent] -> [VarIdent]
go [SortIndex]
rest [VarIdent]
fresh
              go (SortIndex Maybe VarIdent
Nothing Term' BNFC'Position
_ : [SortIndex]
rest) (VarIdent
f : [VarIdent]
fresh) = VarIdent
f VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [SortIndex] -> [VarIdent] -> [VarIdent]
go [SortIndex]
rest [VarIdent]
fresh
              go (SortIndex Maybe VarIdent
Nothing Term' BNFC'Position
_ : [SortIndex]
_) [] =
                FilePath -> [VarIdent]
forall a. HasCallStack => FilePath -> a
error FilePath
"impossible: not enough fresh index names"
          indexDecls =
            [ BNFC'Position
-> Term' BNFC'Position -> Term' BNFC'Position -> ParamDecl
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
forall a. Maybe a
Nothing (VarIdent -> Term' BNFC'Position
surfaceVar VarIdent
v) (SortIndex -> Term' BNFC'Position
sortIndexType SortIndex
si)
            | (VarIdent
v, SortIndex
si) <- [VarIdent] -> [SortIndex] -> [(VarIdent, SortIndex)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VarIdent]
indexVars [SortIndex]
sortIndices ]
          avoid' = (VarIdent -> VarIdentToken) -> [VarIdent] -> [VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> VarIdentToken
identTokenOf [VarIdent]
indexVars [VarIdentToken] -> [VarIdentToken] -> [VarIdentToken]
forall a. Semigroup a => a -> a -> a
<> [VarIdentToken]
avoid
      motiveV <- freshIdent path avoid' "C"
      scrutV <- freshIdent path (identTokenOf motiveV : avoid') "x"
      -- Distinct induction-hypothesis binders, one per recursive field of
      -- the widest constructor; separate methods reuse the same names.
      let maxRec = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (DataConSurface -> Int) -> [DataConSurface] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([(Int, [Term' BNFC'Position])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Int, [Term' BNFC'Position])] -> Int)
-> (DataConSurface -> [(Int, [Term' BNFC'Position])])
-> DataConSurface
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConSurface -> [(Int, [Term' BNFC'Position])]
dataConRecursive) [DataConSurface]
consData)
      ihNames <- freshIdents maxRec
        (identTokenOf motiveV : identTokenOf scrutV : avoid') "ih"
      -- A path-method type refers to the point methods by name, so a
      -- declaration with path constructors binds its methods (@m-<con>@);
      -- a point-only declaration keeps the anonymous arrows it always had.
      let hasPaths = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Bool
True | DataConPath{} <- (DataConSurface -> DataConSort)
-> [DataConSurface] -> [DataConSort]
forall a b. (a -> b) -> [a] -> [b]
map DataConSurface -> DataConSort
dataConSort [DataConSurface]
consData ]
          avoidM = (VarIdent -> VarIdentToken) -> [VarIdent] -> [VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> VarIdentToken
identTokenOf (VarIdent
motiveV VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: VarIdent
scrutV VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
ihNames) [VarIdentToken] -> [VarIdentToken] -> [VarIdentToken]
forall a. Semigroup a => a -> a -> a
<> [VarIdentToken]
avoid'
      methodVars <-
        if not hasPaths then pure Nothing else Just <$>
          let go [VarIdentToken]
_ [] = [VarIdent] -> TypeCheck m [VarIdent]
forall a.
a
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
              go [VarIdentToken]
av (DataConSurface
con : [DataConSurface]
rest) = do
                let Rzk.VarIdentToken Text
t = VarIdent -> VarIdentToken
identTokenOf (DataConSurface -> VarIdent
dataConName DataConSurface
con)
                m <- Maybe FilePath -> [VarIdentToken] -> Text -> TypeCheck m VarIdent
forall (n :: S).
Maybe FilePath -> [VarIdentToken] -> Text -> TypeCheck n VarIdent
freshIdent Maybe FilePath
path [VarIdentToken]
av (Text
"m-" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t)
                (m :) <$> go (identTokenOf m : av) rest
           in go avoidM consData
      -- Binders of the inlined transport/apd spellings (rzk has no
      -- primitive transport, so the generated types spell it through idJ).
      let avoidM' = [VarIdentToken]
-> ([VarIdent] -> [VarIdentToken])
-> Maybe [VarIdent]
-> [VarIdentToken]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((VarIdent -> VarIdentToken) -> [VarIdent] -> [VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> VarIdentToken
identTokenOf) Maybe [VarIdent]
methodVars [VarIdentToken] -> [VarIdentToken] -> [VarIdentToken]
forall a. Semigroup a => a -> a -> a
<> [VarIdentToken]
avoidM
      endpointV <- freshIdent path avoidM' "y"
      pathV <- freshIdent path (identTokenOf endpointV : avoidM') "q"
      -- the inlined transport gets its own binder: it ends up nested inside
      -- a λ that binds 'endpointV' (the apd motive), and reusing the name
      -- there would shadow it
      transportV <- freshIdent path
        (identTokenOf endpointV : identTokenOf pathV : avoidM') "y"
      -- The images of a path constructor's endpoints under the section
      -- being defined; also the endpoint well-formedness check (an endpoint
      -- must be built from constructors and fields, so that its image is
      -- syntactically computable — the standard HIT schema restriction).
      let conMethods = case Maybe [VarIdent]
methodVars of
            Just [VarIdent]
ms -> [VarIdentToken]
-> [(VarIdent, DataConSurface)]
-> [(VarIdentToken, (VarIdent, DataConSurface))]
forall a b. [a] -> [b] -> [(a, b)]
zip ((DataConSurface -> VarIdentToken)
-> [DataConSurface] -> [VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map (VarIdent -> VarIdentToken
identTokenOf (VarIdent -> VarIdentToken)
-> (DataConSurface -> VarIdent) -> DataConSurface -> VarIdentToken
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConSurface -> VarIdent
dataConName) [DataConSurface]
consData)
                           ([VarIdent] -> [DataConSurface] -> [(VarIdent, DataConSurface)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VarIdent]
ms [DataConSurface]
consData)
            Maybe [VarIdent]
Nothing -> []
          dataTok = VarIdent -> VarIdentToken
identTokenOf VarIdent
name
          conToks = (DataConSurface -> VarIdentToken)
-> [DataConSurface] -> [VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map (VarIdent -> VarIdentToken
identTokenOf (VarIdent -> VarIdentToken)
-> (DataConSurface -> VarIdent) -> DataConSurface -> VarIdentToken
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConSurface -> VarIdent
dataConName) [DataConSurface]
consData
          -- the induction-hypothesis binder for each recursive field of a
          -- constructor, by the field's token (a recursive field is a plain
          -- variable: no pattern form inhabits the datatype)
          ihByFieldTok DataConSurface
c =
            [ (VarIdent -> VarIdentToken
identTokenOf VarIdent
v, VarIdent
ih)
            | (VarIdent
ih, Int
j) <- [VarIdent] -> [Int] -> [(VarIdent, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VarIdent]
ihNames (DataConSurface -> [Int]
recPositionsOf DataConSurface
c)
            , Rzk.Var BNFC'Position
_ VarIdent
v <-
                [FilePath -> [Term' BNFC'Position] -> Int -> Term' BNFC'Position
forall a. FilePath -> [a] -> Int -> a
nthByConstruction FilePath
"constructor field patterns" (DataConSurface -> [Term' BNFC'Position]
dataConFieldPats DataConSurface
c) Int
j] ]
          endpointErr DataConSurface
c a
t = TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
            FilePath
"in path constructor " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree (DataConSurface -> VarIdent
dataConName DataConSurface
c)
              FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
": an endpoint must be built from the declaration's"
              FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" constructors and the constructor's fields, but "
              FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> a -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree a
t FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" is not"
          -- a subterm at a non-recursive argument position must not touch
          -- the datatype at all: the section being defined does not act on it
          ensureDFree DataConSurface
c Term' BNFC'Position
t =
            let bad :: [VarIdentToken]
bad = VarIdentToken
dataTok VarIdentToken -> [VarIdentToken] -> [VarIdentToken]
forall a. a -> [a] -> [a]
: [VarIdentToken]
conToks [VarIdentToken] -> [VarIdentToken] -> [VarIdentToken]
forall a. Semigroup a => a -> a -> a
<> ((VarIdentToken, VarIdent) -> VarIdentToken)
-> [(VarIdentToken, VarIdent)] -> [VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map (VarIdentToken, VarIdent) -> VarIdentToken
forall a b. (a, b) -> a
fst (DataConSurface -> [(VarIdentToken, VarIdent)]
ihByFieldTok DataConSurface
c)
             in Bool
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ () | VarIdentToken
tk <- Term' BNFC'Position -> [VarIdentToken]
forall a. Data a => a -> [VarIdentToken]
surfaceVarTokens Term' BNFC'Position
t, VarIdentToken
tk VarIdentToken -> [VarIdentToken] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VarIdentToken]
bad ])
                  (DataConSurface
-> Term' BNFC'Position
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall {n :: S} {a} {a}.
(Distinct n, Print a) =>
DataConSurface -> a -> TypeCheck n a
endpointErr DataConSurface
c Term' BNFC'Position
t)
          imageOf DataConSurface
c Term' BNFC'Position
t = case Term' BNFC'Position -> (Term' BNFC'Position, [Term' BNFC'Position])
surfaceAppSpine Term' BNFC'Position
t of
            (Rzk.Var BNFC'Position
_ VarIdent
v, [Term' BNFC'Position]
args)
              | Just (VarIdent
m, DataConSurface
target) <- VarIdentToken
-> [(VarIdentToken, (VarIdent, DataConSurface))]
-> Maybe (VarIdent, DataConSurface)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (VarIdent -> VarIdentToken
identTokenOf VarIdent
v) [(VarIdentToken, (VarIdent, DataConSurface))]
conMethods -> do
                  let nP :: Int
nP = [VarIdent] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VarIdent]
paramVars
                      arity :: Int
arity = [ParamDecl] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataConSurface -> [ParamDecl]
dataConFields DataConSurface
target)
                      ([Term' BNFC'Position]
pArgs, [Term' BNFC'Position]
fArgs) = Int
-> [Term' BNFC'Position]
-> ([Term' BNFC'Position], [Term' BNFC'Position])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
nP [Term' BNFC'Position]
args
                      varTokOf :: Term' BNFC'Position -> Maybe VarIdentToken
varTokOf = \case
                        Rzk.Var BNFC'Position
_ VarIdent
u -> VarIdentToken -> Maybe VarIdentToken
forall a. a -> Maybe a
Just (VarIdent -> VarIdentToken
identTokenOf VarIdent
u)
                        Term' BNFC'Position
_           -> Maybe VarIdentToken
forall a. Maybe a
Nothing
                  Bool
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Term' BNFC'Position] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term' BNFC'Position]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nP Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
arity
                      Bool -> Bool -> Bool
&& (Term' BNFC'Position -> Maybe VarIdentToken)
-> [Term' BNFC'Position] -> [Maybe VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map Term' BNFC'Position -> Maybe VarIdentToken
varTokOf [Term' BNFC'Position]
pArgs [Maybe VarIdentToken] -> [Maybe VarIdentToken] -> Bool
forall a. Eq a => a -> a -> Bool
== (VarIdent -> Maybe VarIdentToken)
-> [VarIdent] -> [Maybe VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map (VarIdentToken -> Maybe VarIdentToken
forall a. a -> Maybe a
Just (VarIdentToken -> Maybe VarIdentToken)
-> (VarIdent -> VarIdentToken) -> VarIdent -> Maybe VarIdentToken
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarIdent -> VarIdentToken
identTokenOf) [VarIdent]
paramVars) (ReaderT
   (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
 -> ReaderT
      (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$
                    DataConSurface
-> Term' BNFC'Position
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall {n :: S} {a} {a}.
(Distinct n, Print a) =>
DataConSurface -> a -> TypeCheck n a
endpointErr DataConSurface
c Term' BNFC'Position
t
                  imgArgs <- [(Int, Term' BNFC'Position)]
-> ((Int, Term' BNFC'Position)
    -> ReaderT
         (Context m)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         [Term' BNFC'Position])
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[Term' BNFC'Position]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Int] -> [Term' BNFC'Position] -> [(Int, Term' BNFC'Position)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [Term' BNFC'Position]
fArgs) (((Int, Term' BNFC'Position)
  -> ReaderT
       (Context m)
       (ExceptT TypeErrorInScopedContext (State CheckLog))
       [Term' BNFC'Position])
 -> ReaderT
      (Context m)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [[Term' BNFC'Position]])
-> ((Int, Term' BNFC'Position)
    -> ReaderT
         (Context m)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         [Term' BNFC'Position])
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[Term' BNFC'Position]]
forall a b. (a -> b) -> a -> b
$ \(Int
j, Term' BNFC'Position
a) ->
                    if Int
j Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` DataConSurface -> [Int]
recPositionsOf DataConSurface
target
                      then do { ia <- DataConSurface
-> Term' BNFC'Position
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position)
imageOf DataConSurface
c Term' BNFC'Position
a; pure [a, ia] }
                      else do { DataConSurface
-> Term' BNFC'Position
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
ensureDFree DataConSurface
c Term' BNFC'Position
a; [Term' BNFC'Position]
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Term' BNFC'Position]
forall a.
a
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term' BNFC'Position
a] }
                  pure (surfaceApps (surfaceVar m) (concat imgArgs))
              | [Term' BNFC'Position] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term' BNFC'Position]
args
              , Just VarIdent
ih <- VarIdentToken -> [(VarIdentToken, VarIdent)] -> Maybe VarIdent
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (VarIdent -> VarIdentToken
identTokenOf VarIdent
v) (DataConSurface -> [(VarIdentToken, VarIdent)]
ihByFieldTok DataConSurface
c) ->
                  Term' BNFC'Position
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position)
forall a.
a
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarIdent -> Term' BNFC'Position
surfaceVar VarIdent
ih)
            (Term' BNFC'Position, [Term' BNFC'Position])
_ -> DataConSurface
-> Term' BNFC'Position
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position)
forall {n :: S} {a} {a}.
(Distinct n, Print a) =>
DataConSurface -> a -> TypeCheck n a
endpointErr DataConSurface
c Term' BNFC'Position
t
      pathData <- forM consData $ \DataConSurface
con -> case DataConSurface -> DataConSort
dataConSort DataConSurface
con of
        DataConSort
DataConPoint    -> Maybe
  ((Term' BNFC'Position, Term' BNFC'Position),
   (Term' BNFC'Position, Term' BNFC'Position))
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe
        ((Term' BNFC'Position, Term' BNFC'Position),
         (Term' BNFC'Position, Term' BNFC'Position)))
forall a.
a
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe
  ((Term' BNFC'Position, Term' BNFC'Position),
   (Term' BNFC'Position, Term' BNFC'Position))
forall a. Maybe a
Nothing
        DataConPath Term' BNFC'Position
l Term' BNFC'Position
r -> do
          iL <- DataConSurface
-> Term' BNFC'Position
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Term' BNFC'Position)
imageOf DataConSurface
con Term' BNFC'Position
l
          iR <- imageOf con r
          pure (Just ((l, r), (iL, iR)))
      -- The surface types of the eliminators and the path computation rules
      -- (see "Rzk.TypeCheck.Decl.Data"), pushed through the ordinary
      -- elaborator below just like any user-written type.
      let spec = ElimSpec
            { esName :: VarIdent
esName = VarIdent
name, esParamVars :: [VarIdent]
esParamVars = [VarIdent]
paramVars, esParamDecls :: [ParamDecl]
esParamDecls = [ParamDecl]
paramDecls
            , esIndexVars :: [VarIdent]
esIndexVars = [VarIdent]
indexVars, esIndexDecls :: [ParamDecl]
esIndexDecls = [ParamDecl]
indexDecls, esMotiveV :: VarIdent
esMotiveV = VarIdent
motiveV
            , esScrutV :: VarIdent
esScrutV = VarIdent
scrutV, esIhNames :: [VarIdent]
esIhNames = [VarIdent]
ihNames, esMethodVars :: Maybe [VarIdent]
esMethodVars = Maybe [VarIdent]
methodVars
            , esEndpointV :: VarIdent
esEndpointV = VarIdent
endpointV, esPathV :: VarIdent
esPathV = VarIdent
pathV, esTransportV :: VarIdent
esTransportV = VarIdent
transportV
            , esConsData :: [DataConSurface]
esConsData = [DataConSurface]
consData, esPathData :: [Maybe
   ((Term' BNFC'Position, Term' BNFC'Position),
    (Term' BNFC'Position, Term' BNFC'Position))]
esPathData = [Maybe
   ((Term' BNFC'Position, Term' BNFC'Position),
    (Term' BNFC'Position, Term' BNFC'Position))]
pathData }
          et = ElimSpec -> ElimTerms
elimTerms ElimSpec
spec
          indName = Text -> VarIdent -> VarIdent
prefixedIdent Text
"ind-" VarIdent
name
          recName = Text -> VarIdent -> VarIdent
prefixedIdent Text
"rec-" VarIdent
name
      (mindTy, mrecTy, computeReasc) <- splitClauses indName recName (map fst (computeRules et))
      indTyT <- elaborate (indTypeTerm et)
      indCanonical <- memoizeWHNF =<< typecheck indTyT universeT
      indTy' <- reascribe indName indCanonical mindTy
      indDeps <- assumptionDepsOf indTy'
      withTopLevel (varIdentAt path indName) indTy' Nothing False
        (nubNames (usedHere <> indDeps))
        (Just (DataRole dName numParams (DataElimKind numMethods indexArity ElimInd))) $ \NameBinder m l
_ Decl l
indDecl -> do
          recTyT <- Term' BNFC'Position -> TypeCheck l (Term l)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate (ElimTerms -> Term' BNFC'Position
recTypeTerm ElimTerms
et)
          recCanonical <- memoizeWHNF =<< typecheck recTyT universeT
          recTy' <- reascribe recName recCanonical mrecTy
          recDeps <- assumptionDepsOf recTy'
          let usedAtInd = [Name m] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 [Name m]
usedHere
          withTopLevel (varIdentAt path recName) recTy' Nothing False
            (nubNames (usedAtInd <> recDeps))
            (Just (DataRole (Foil.sink dName) numParams (DataElimKind numMethods indexArity ElimRec))) $ \NameBinder l l
_ Decl l
recDecl ->
              [Name l]
-> [(VarIdentToken, Term' BNFC'Position)]
-> [(VarIdent, Term' BNFC'Position)]
-> [Decl l]
-> TypeCheck l r
forall (m :: S).
DExt n m =>
[Name m]
-> [(VarIdentToken, Term' BNFC'Position)]
-> [(VarIdent, Term' BNFC'Position)]
-> [Decl m]
-> TypeCheck m r
bindComputes
                ([Name l] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 [Name l]
usedAtInd)
                [(VarIdentToken, Term' BNFC'Position)]
computeReasc
                (ElimTerms -> [(VarIdent, Term' BNFC'Position)]
computeRules ElimTerms
et)
                ([Decl l] -> [Decl l]
forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls ([Decl m] -> [Decl l]
forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls [Decl m]
declsAcc [Decl l] -> [Decl l] -> [Decl l]
forall a. Semigroup a => a -> a -> a
<> [Decl l
indDecl]) [Decl l] -> [Decl l] -> [Decl l]
forall a. Semigroup a => a -> a -> a
<> [Decl l
recDecl])

    -- | Bind the generated @compute-@ lemmas (one @ind@/@rec@ pair per
    -- path constructor), re-ascribing the ones a @compute with@ clause
    -- names, then hand the accumulated declarations to the continuation of
    -- 'withDataDecls'.
    bindComputes
      :: forall m. DExt n m
      => [Foil.Name m] -> [(Rzk.VarIdentToken, Rzk.Term)]
      -> [(Rzk.VarIdent, Rzk.Term)] -> [Decl m]
      -> TypeCheck m r
    bindComputes :: forall (m :: S).
DExt n m =>
[Name m]
-> [(VarIdentToken, Term' BNFC'Position)]
-> [(VarIdent, Term' BNFC'Position)]
-> [Decl m]
-> TypeCheck m r
bindComputes [Name m]
_used [(VarIdentToken, Term' BNFC'Position)]
_reasc [] [Decl m]
acc = [Decl m] -> TypeCheck m r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> TypeCheck l r
k [Decl m]
acc
    bindComputes [Name m]
usedHere [(VarIdentToken, Term' BNFC'Position)]
reasc ((VarIdent
cname, Term' BNFC'Position
cty) : [(VarIdent, Term' BNFC'Position)]
rest) [Decl m]
acc = do
      tyT <- Term' BNFC'Position -> TypeCheck m (Term m)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate Term' BNFC'Position
cty
      canonical <- memoizeWHNF =<< typecheck tyT universeT
      ty' <- reascribe cname canonical (lookup (identTokenOf cname) reasc)
      deps <- assumptionDepsOf ty'
      withTopLevel (varIdentAt path cname) ty' Nothing False
        (nubNames (usedHere <> deps)) Nothing $ \NameBinder m l
_ Decl l
decl ->
          [Name l]
-> [(VarIdentToken, Term' BNFC'Position)]
-> [(VarIdent, Term' BNFC'Position)]
-> [Decl l]
-> TypeCheck l r
forall (m :: S).
DExt n m =>
[Name m]
-> [(VarIdentToken, Term' BNFC'Position)]
-> [(VarIdent, Term' BNFC'Position)]
-> [Decl m]
-> TypeCheck m r
bindComputes ([Name m] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 [Name m]
usedHere) [(VarIdentToken, Term' BNFC'Position)]
reasc [(VarIdent, Term' BNFC'Position)]
rest
            ([Decl m] -> [Decl l]
forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls [Decl m]
acc [Decl l] -> [Decl l] -> [Decl l]
forall a. Semigroup a => a -> a -> a
<> [Decl l
decl])

    -- | Split the re-ascription clauses among the generated entries: the
    -- two eliminators (@eliminate with@) and the computation rules of the
    -- path constructors (@compute with@). A clause must name an entry of
    -- the matching kind, at most once each.
    splitClauses
      :: Distinct m
      => Rzk.VarIdent -> Rzk.VarIdent -> [Rzk.VarIdent]
      -> TypeCheck m
           (Maybe Rzk.Term, Maybe Rzk.Term, [(Rzk.VarIdentToken, Rzk.Term)])
    splitClauses :: forall (m :: S).
Distinct m =>
VarIdent
-> VarIdent
-> [VarIdent]
-> TypeCheck
     m
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
splitClauses VarIdent
indName VarIdent
recName [VarIdent]
computeNames = (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
 [(VarIdentToken, Term' BNFC'Position)])
-> [DataElim]
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
go (Maybe (Term' BNFC'Position)
forall a. Maybe a
Nothing, Maybe (Term' BNFC'Position)
forall a. Maybe a
Nothing, []) [DataElim]
elims
      where
        go :: (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
 [(VarIdentToken, Term' BNFC'Position)])
-> [DataElim]
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
go (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
 [(VarIdentToken, Term' BNFC'Position)])
acc [] = (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
 [(VarIdentToken, Term' BNFC'Position)])
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
forall a.
a
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
 [(VarIdentToken, Term' BNFC'Position)])
acc
        go (Maybe (Term' BNFC'Position)
mind, Maybe (Term' BNFC'Position)
mrec, [(VarIdentToken, Term' BNFC'Position)]
mcomp) (Rzk.DataElim BNFC'Position
_loc VarIdent
elimName Term' BNFC'Position
ty : [DataElim]
rest)
          | VarIdent -> VarIdent -> Bool
sameIdent VarIdent
elimName VarIdent
indName =
              case Maybe (Term' BNFC'Position)
mind of
                Maybe (Term' BNFC'Position)
Nothing -> (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
 [(VarIdentToken, Term' BNFC'Position)])
-> [DataElim]
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
go (Term' BNFC'Position -> Maybe (Term' BNFC'Position)
forall a. a -> Maybe a
Just Term' BNFC'Position
ty, Maybe (Term' BNFC'Position)
mrec, [(VarIdentToken, Term' BNFC'Position)]
mcomp) [DataElim]
rest
                Just Term' BNFC'Position
_  -> VarIdent
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
forall {n :: S} {a} {a}.
(Distinct n, Print a) =>
a -> TypeCheck n a
duplicate VarIdent
elimName
          | VarIdent -> VarIdent -> Bool
sameIdent VarIdent
elimName VarIdent
recName =
              case Maybe (Term' BNFC'Position)
mrec of
                Maybe (Term' BNFC'Position)
Nothing -> (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
 [(VarIdentToken, Term' BNFC'Position)])
-> [DataElim]
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
go (Maybe (Term' BNFC'Position)
mind, Term' BNFC'Position -> Maybe (Term' BNFC'Position)
forall a. a -> Maybe a
Just Term' BNFC'Position
ty, [(VarIdentToken, Term' BNFC'Position)]
mcomp) [DataElim]
rest
                Just Term' BNFC'Position
_  -> VarIdent
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
forall {n :: S} {a} {a}.
(Distinct n, Print a) =>
a -> TypeCheck n a
duplicate VarIdent
elimName
          | Bool
otherwise = TypeError m
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError m
 -> ReaderT
      (Context m)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
       [(VarIdentToken, Term' BNFC'Position)]))
-> TypeError m
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError m
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError m) -> FilePath -> TypeError m
forall a b. (a -> b) -> a -> b
$
              FilePath
"eliminate with clause for " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
elimName
                FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
", which is not an eliminator of " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
name
                FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" (the eliminators are " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
indName
                FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" and " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
recName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
")"
        go (Maybe (Term' BNFC'Position)
mind, Maybe (Term' BNFC'Position)
mrec, [(VarIdentToken, Term' BNFC'Position)]
mcomp) (Rzk.DataCompute BNFC'Position
_loc VarIdent
ruleName Term' BNFC'Position
ty : [DataElim]
rest)
          | (VarIdent -> Bool) -> [VarIdent] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (VarIdent -> VarIdent -> Bool
sameIdent VarIdent
ruleName) [VarIdent]
computeNames =
              if VarIdent -> VarIdentToken
identTokenOf VarIdent
ruleName VarIdentToken -> [VarIdentToken] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((VarIdentToken, Term' BNFC'Position) -> VarIdentToken)
-> [(VarIdentToken, Term' BNFC'Position)] -> [VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map (VarIdentToken, Term' BNFC'Position) -> VarIdentToken
forall a b. (a, b) -> a
fst [(VarIdentToken, Term' BNFC'Position)]
mcomp
                then VarIdent
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
forall {n :: S} {a} {a}.
(Distinct n, Print a) =>
a -> TypeCheck n a
duplicate VarIdent
ruleName
                else (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
 [(VarIdentToken, Term' BNFC'Position)])
-> [DataElim]
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
go (Maybe (Term' BNFC'Position)
mind, Maybe (Term' BNFC'Position)
mrec, [(VarIdentToken, Term' BNFC'Position)]
mcomp [(VarIdentToken, Term' BNFC'Position)]
-> [(VarIdentToken, Term' BNFC'Position)]
-> [(VarIdentToken, Term' BNFC'Position)]
forall a. Semigroup a => a -> a -> a
<> [(VarIdent -> VarIdentToken
identTokenOf VarIdent
ruleName, Term' BNFC'Position
ty)]) [DataElim]
rest
          | Bool
otherwise = TypeError m
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError m
 -> ReaderT
      (Context m)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
       [(VarIdentToken, Term' BNFC'Position)]))
-> TypeError m
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Term' BNFC'Position), Maybe (Term' BNFC'Position),
      [(VarIdentToken, Term' BNFC'Position)])
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError m
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError m) -> FilePath -> TypeError m
forall a b. (a -> b) -> a -> b
$
              FilePath
"compute with clause for " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
ruleName
                FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
", which is not a computation rule of " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
name
                FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> case [VarIdent]
computeNames of
                     [] -> FilePath
" (the declaration has no path constructors, so no computation rules are generated)"
                     [VarIdent]
_  -> FilePath
" (the computation rules are "
                             FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " ((VarIdent -> FilePath) -> [VarIdent] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree [VarIdent]
computeNames)
                             FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
")"
        duplicate :: a -> TypeCheck n a
duplicate a
n = TypeError n -> TypeCheck n a
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n a) -> TypeError n -> TypeCheck n a
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
          FilePath
"duplicate re-ascription clause for " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> a -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree a
n
        sameIdent :: VarIdent -> VarIdent -> Bool
sameIdent VarIdent
a VarIdent
b = VarIdent -> VarIdentToken
identTokenOf VarIdent
a VarIdentToken -> VarIdentToken -> Bool
forall a. Eq a => a -> a -> Bool
== VarIdent -> VarIdentToken
identTokenOf VarIdent
b

    -- | Check a re-ascribed generated type (an eliminator's or a
    -- computation rule's) against the canonical one and pick the type to
    -- store. The user's spelling must be definitionally equal to the
    -- canonical type (checked with the type former and constructors in
    -- scope); definitionally equal types are interchangeable, so storing
    -- the user's spelling only changes how the entry's type is displayed,
    -- not what it accepts or computes.
    reascribe
      :: Distinct m
      => Rzk.VarIdent -> TermT m -> Maybe Rzk.Term -> TypeCheck m (TermT m)
    reascribe :: forall (m :: S).
Distinct m =>
VarIdent
-> TermT m -> Maybe (Term' BNFC'Position) -> TypeCheck m (TermT m)
reascribe VarIdent
_entryName TermT m
canonical Maybe (Term' BNFC'Position)
Nothing = TermT m
-> ReaderT
     (Context m)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT m)
forall a.
a
-> ReaderT
     (Context m) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT m
canonical
    reascribe VarIdent
entryName TermT m
canonical (Just Term' BNFC'Position
ty) = do
      tyT <- Term' BNFC'Position -> TypeCheck m (Term m)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate Term' BNFC'Position
ty
      ty' <- memoizeWHNF =<< typecheck tyT universeT
      unifyTerms canonical ty' `catchError` \TypeErrorInScopedContext
_ ->
        TypeError m -> TypeCheck m ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError m -> TypeCheck m ()) -> TypeError m -> TypeCheck m ()
forall a b. (a -> b) -> a -> b
$
          VarIdent -> TermT m -> TermT m -> TypeError m
forall (n :: S). VarIdent -> TermT n -> TermT n -> TypeError n
TypeErrorReascribedTypeMismatch (Maybe FilePath -> VarIdent -> VarIdent
varIdentAt Maybe FilePath
path VarIdent
entryName) TermT m
canonical TermT m
ty'
      pure ty'

-- | Run a command, recording which one it is and where.
--
-- An error raised anywhere in the command (or in the rest of the module, which is
-- checked inside it) is /collected/ rather than thrown: the declarations made
-- before it stand, the error is reported, and the rest of the module is skipped.
-- The strict entry points turn the first collected error back into a thrown one.
withCommand
  :: Distinct n
  => Rzk.Command
  -> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
  -> TypeCheck n r
  -> TypeCheck n r
withCommand :: forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
k TypeCheck n r
action =
  (Context n -> Context n) -> TypeCheck n r -> TypeCheck n r
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local Context n -> Context n
atCommand (TypeCheck n r
checked TypeCheck n r
-> (TypeErrorInScopedContext -> TypeCheck n r) -> TypeCheck n r
forall a.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TypeErrorInScopedContext
err -> [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
k [] [TypeErrorInScopedContext
err])
  where
    checked :: TypeCheck n r
checked = case Command -> [(VarIdent, [VarIdent])]
forall a. Data a => a -> [(VarIdent, [VarIdent])]
duplicateBinders Command
command of
      (VarIdent
dup, [VarIdent]
previous) : [(VarIdent, [VarIdent])]
_ -> TypeError n -> TypeCheck n r
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (VarIdent -> [VarIdent] -> TypeError n
forall (n :: S). VarIdent -> [VarIdent] -> TypeError n
TypeErrorRepeatedBinder VarIdent
dup [VarIdent]
previous)
      []                  -> TypeCheck n r
action
    atCommand :: Context n -> Context n
atCommand Context n
ctx = Context n
ctx
      { ctxCurrentCommand = Just command
      , ctxLocation = updatePosition (Rzk.hasPosition command) <$> ctxLocation ctx
      }
    -- Where the command starts. A judgement made inside it narrows this to the
    -- sub-term it is about (see @narrowLocation@); this is what an error with
    -- no sub-term of its own falls back to.
    updatePosition :: BNFC'Position -> LocationInfo -> LocationInfo
updatePosition BNFC'Position
pos LocationInfo
loc =
      LocationInfo
loc { locationLine = fst <$> pos, locationColumn = snd <$> pos }

-- | The binder leaves repeated within one binder /group/ of a surface
-- command: the parameter list of a λ, of a declaration, or of a constructor
-- (a single pattern's leaves are part of their group). Each hit pairs the
-- repeated occurrence with the earlier ones it clashes with.
--
-- Shadowing an outer binder stays a warning ('checkNameShadowing'); a
-- duplicate inside one group can only be a mistake, and the silent
-- freshening it used to get showed names the user never wrote (issue #321).
duplicateBinders :: Data a => a -> [(VarIdent, [VarIdent])]
duplicateBinders :: forall a. Data a => a -> [(VarIdent, [VarIdent])]
duplicateBinders a
x = [[(VarIdent, [VarIdent])]] -> [(VarIdent, [VarIdent])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [(VarIdent, [VarIdent])]
-> (Term' BNFC'Position -> [(VarIdent, [VarIdent])])
-> Maybe (Term' BNFC'Position)
-> [(VarIdent, [VarIdent])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Term' BNFC'Position -> [(VarIdent, [VarIdent])]
termGroup (a -> Maybe (Term' BNFC'Position)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
x)
  , [(VarIdent, [VarIdent])]
-> (Command -> [(VarIdent, [VarIdent])])
-> Maybe Command
-> [(VarIdent, [VarIdent])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Command -> [(VarIdent, [VarIdent])]
commandGroup (a -> Maybe Command
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
x)
  , [(VarIdent, [VarIdent])]
-> (Constructor -> [(VarIdent, [VarIdent])])
-> Maybe Constructor
-> [(VarIdent, [VarIdent])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Constructor -> [(VarIdent, [VarIdent])]
constructorGroup (a -> Maybe Constructor
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
x)
  , [[(VarIdent, [VarIdent])]] -> [(VarIdent, [VarIdent])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((forall a. Data a => a -> [(VarIdent, [VarIdent])])
-> a -> [[(VarIdent, [VarIdent])]]
forall a u. Data a => (forall d. Data d => d -> u) -> a -> [u]
forall u. (forall d. Data d => d -> u) -> a -> [u]
gmapQ d -> [(VarIdent, [VarIdent])]
forall a. Data a => a -> [(VarIdent, [VarIdent])]
duplicateBinders a
x)
  ]
  where
    termGroup :: Rzk.Term -> [(VarIdent, [VarIdent])]
    termGroup :: Term' BNFC'Position -> [(VarIdent, [VarIdent])]
termGroup = \case
      Rzk.Lambda BNFC'Position
_ [Param]
params Term' BNFC'Position
_       -> [VarIdent] -> [(VarIdent, [VarIdent])]
groupDuplicates ((Param -> [VarIdent]) -> [Param] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Param -> [VarIdent]
paramLeaves [Param]
params)
      Rzk.ASCII_Lambda BNFC'Position
_ [Param]
params Term' BNFC'Position
_ -> [VarIdent] -> [(VarIdent, [VarIdent])]
groupDuplicates ((Param -> [VarIdent]) -> [Param] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Param -> [VarIdent]
paramLeaves [Param]
params)
      Term' BNFC'Position
_                           -> []

    commandGroup :: Rzk.Command -> [(VarIdent, [VarIdent])]
    commandGroup :: Command -> [(VarIdent, [VarIdent])]
commandGroup = \case
      Rzk.CommandDefine BNFC'Position
_ VarIdent
_ DeclUsedVars' BNFC'Position
_ [Param]
params Term' BNFC'Position
_ Term' BNFC'Position
_  -> [VarIdent] -> [(VarIdent, [VarIdent])]
groupDuplicates ((Param -> [VarIdent]) -> [Param] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Param -> [VarIdent]
paramLeaves [Param]
params)
      Rzk.CommandPostulate BNFC'Position
_ VarIdent
_ DeclUsedVars' BNFC'Position
_ [Param]
params Term' BNFC'Position
_ -> [VarIdent] -> [(VarIdent, [VarIdent])]
groupDuplicates ((Param -> [VarIdent]) -> [Param] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Param -> [VarIdent]
paramLeaves [Param]
params)
      Rzk.CommandData BNFC'Position
_ VarIdent
_ DeclUsedVars' BNFC'Position
_ [Param]
params DataSort
_ DataBody
_    -> [VarIdent] -> [(VarIdent, [VarIdent])]
groupDuplicates ((Param -> [VarIdent]) -> [Param] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Param -> [VarIdent]
paramLeaves [Param]
params)
      Command
_                                   -> []

    constructorGroup :: Rzk.Constructor -> [(VarIdent, [VarIdent])]
    constructorGroup :: Constructor -> [(VarIdent, [VarIdent])]
constructorGroup (Rzk.Constructor BNFC'Position
_ VarIdent
_ [Param]
params ConstructorType' BNFC'Position
_) =
      [VarIdent] -> [(VarIdent, [VarIdent])]
groupDuplicates ((Param -> [VarIdent]) -> [Param] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Param -> [VarIdent]
paramLeaves [Param]
params)

    paramLeaves :: Rzk.Param -> [Rzk.VarIdent]
    paramLeaves :: Param -> [VarIdent]
paramLeaves = \case
      Rzk.ParamPattern BNFC'Position
_ Pattern' BNFC'Position
pat                  -> Pattern' BNFC'Position -> [VarIdent]
patternLeaves Pattern' BNFC'Position
pat
      Rzk.ParamPatternType BNFC'Position
_ [Pattern' BNFC'Position]
pats Term' BNFC'Position
_           -> (Pattern' BNFC'Position -> [VarIdent])
-> [Pattern' BNFC'Position] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern' BNFC'Position -> [VarIdent]
patternLeaves [Pattern' BNFC'Position]
pats
      Rzk.ParamPatternShape BNFC'Position
_ [Pattern' BNFC'Position]
pats Term' BNFC'Position
_ Term' BNFC'Position
_        -> (Pattern' BNFC'Position -> [VarIdent])
-> [Pattern' BNFC'Position] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern' BNFC'Position -> [VarIdent]
patternLeaves [Pattern' BNFC'Position]
pats
      Rzk.ParamPatternModalType BNFC'Position
_ [Pattern' BNFC'Position]
pats ModalColon' BNFC'Position
_ Term' BNFC'Position
_    -> (Pattern' BNFC'Position -> [VarIdent])
-> [Pattern' BNFC'Position] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern' BNFC'Position -> [VarIdent]
patternLeaves [Pattern' BNFC'Position]
pats
      Rzk.ParamPatternModalShape BNFC'Position
_ [Pattern' BNFC'Position]
pats ModalColon' BNFC'Position
_ Term' BNFC'Position
_ Term' BNFC'Position
_ -> (Pattern' BNFC'Position -> [VarIdent])
-> [Pattern' BNFC'Position] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern' BNFC'Position -> [VarIdent]
patternLeaves [Pattern' BNFC'Position]
pats

    patternLeaves :: Rzk.Pattern -> [Rzk.VarIdent]
    patternLeaves :: Pattern' BNFC'Position -> [VarIdent]
patternLeaves = \case
      Rzk.PatternUnit BNFC'Position
_ -> []
      Rzk.PatternVar BNFC'Position
_ v :: VarIdent
v@(Rzk.VarIdent BNFC'Position
_ (Rzk.VarIdentToken Text
t)) -> [ VarIdent
v | Text
t Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Text
"_" ]
      Rzk.PatternPair BNFC'Position
_ Pattern' BNFC'Position
l Pattern' BNFC'Position
r -> Pattern' BNFC'Position -> [VarIdent]
patternLeaves Pattern' BNFC'Position
l [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Semigroup a => a -> a -> a
<> Pattern' BNFC'Position -> [VarIdent]
patternLeaves Pattern' BNFC'Position
r
      Rzk.PatternTuple BNFC'Position
_ Pattern' BNFC'Position
a Pattern' BNFC'Position
b [Pattern' BNFC'Position]
cs -> (Pattern' BNFC'Position -> [VarIdent])
-> [Pattern' BNFC'Position] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern' BNFC'Position -> [VarIdent]
patternLeaves (Pattern' BNFC'Position
a Pattern' BNFC'Position
-> [Pattern' BNFC'Position] -> [Pattern' BNFC'Position]
forall a. a -> [a] -> [a]
: Pattern' BNFC'Position
b Pattern' BNFC'Position
-> [Pattern' BNFC'Position] -> [Pattern' BNFC'Position]
forall a. a -> [a] -> [a]
: [Pattern' BNFC'Position]
cs)

    -- positions differ between occurrences, so compare by spelling
    groupDuplicates :: [VarIdent] -> [(VarIdent, [VarIdent])]
groupDuplicates = [VarIdent] -> [VarIdent] -> [(VarIdent, [VarIdent])]
go []
      where
        go :: [VarIdent] -> [VarIdent] -> [(VarIdent, [VarIdent])]
go [VarIdent]
_ [] = []
        go [VarIdent]
seen (VarIdent
v : [VarIdent]
vs) =
          case [ VarIdent
e | VarIdent
e <- [VarIdent]
seen, VarIdent -> VarIdent -> Bool
forall {a} {a}. VarIdent' a -> VarIdent' a -> Bool
sameSpelling VarIdent
e VarIdent
v ] of
            []      -> [VarIdent] -> [VarIdent] -> [(VarIdent, [VarIdent])]
go (VarIdent
v VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
seen) [VarIdent]
vs
            [VarIdent]
earlier -> (VarIdent -> VarIdent
varIdent VarIdent
v, (VarIdent -> VarIdent) -> [VarIdent] -> [VarIdent]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> VarIdent
varIdent ([VarIdent] -> [VarIdent]
forall a. [a] -> [a]
reverse [VarIdent]
earlier)) (VarIdent, [VarIdent])
-> [(VarIdent, [VarIdent])] -> [(VarIdent, [VarIdent])]
forall a. a -> [a] -> [a]
: [VarIdent] -> [VarIdent] -> [(VarIdent, [VarIdent])]
go (VarIdent
v VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
seen) [VarIdent]
vs
    sameSpelling :: VarIdent' a -> VarIdent' a -> Bool
sameSpelling (Rzk.VarIdent a
_ VarIdentToken
a) (Rzk.VarIdent a
_ VarIdentToken
b) = VarIdentToken
a VarIdentToken -> VarIdentToken -> Bool
forall a. Eq a => a -> a -> Bool
== VarIdentToken
b

-- | Report a command's error and go on to the next one, with the command
-- itself contributing nothing to the scope.
--
-- This is the recovery for a command that cannot be stood in for: a
-- declaration whose /type/ does not check has no type to enter it at. The uses
-- of it below then report an undefined variable, which is noisier than the one
-- error but keeps the rest of the file's own errors and holes visible, which is
-- what a file being edited is wanted for.
skippingCommand
  :: Distinct n
  => TypeErrorInScopedContext
  -> Maybe FilePath -> Integer -> Integer -> [Rzk.Command]
  -> (forall l. (DExt n l, Distinct l)
        => [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
  -> TypeCheck n r
skippingCommand :: forall (n :: S) r.
Distinct n =>
TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
skippingCommand TypeErrorInScopedContext
err Maybe FilePath
path Integer
i Integer
total [Command]
more forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k =
  Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more ((forall (l :: S).
  (DExt n l, Distinct l) =>
  [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) r)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) r
forall a b. (a -> b) -> a -> b
$ \[Decl l]
decls [TypeErrorInScopedContext]
errs -> [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k [Decl l]
decls (TypeErrorInScopedContext
err TypeErrorInScopedContext
-> [TypeErrorInScopedContext] -> [TypeErrorInScopedContext]
forall a. a -> [a] -> [a]
: [TypeErrorInScopedContext]
errs)

-- | Run a check, handing back its error instead of propagating it.
--
-- What it recorded on the way is kept: the record lives in the state beneath
-- the error channel, so the holes the user wrote in a definition that fails are
-- still reported (see "Rzk.TypeCheck.Monad").
tryCheck :: TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck :: forall (n :: S) a.
TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck TypeCheck n a
action = (a -> Either TypeErrorInScopedContext a
forall a b. b -> Either a b
Right (a -> Either TypeErrorInScopedContext a)
-> TypeCheck n a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Either TypeErrorInScopedContext a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeCheck n a
action) ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Either TypeErrorInScopedContext a)
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Either TypeErrorInScopedContext a))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Either TypeErrorInScopedContext a)
forall a.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (Either TypeErrorInScopedContext a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Either TypeErrorInScopedContext a)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either TypeErrorInScopedContext a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Either TypeErrorInScopedContext a))
-> (TypeErrorInScopedContext -> Either TypeErrorInScopedContext a)
-> TypeErrorInScopedContext
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Either TypeErrorInScopedContext a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeErrorInScopedContext -> Either TypeErrorInScopedContext a
forall a b. a -> Either a b
Left)

-- | Run a check with the location narrowed to where a surface term was written.
--
-- Descending through a judgement already narrows to the sub-term it is about
-- (@narrowLocation@ in "Rzk.TypeCheck.Monad"), but only a /node/ carries a
-- position: a variable is a leaf of the core syntax, with nowhere to put one.
-- So a check that starts from a surface term says where that term starts, and a
-- definition whose body is a bare variable is reported at the body rather than
-- at the declaration above it.
atSurface :: Rzk.HasPosition a => a -> TypeCheck n b -> TypeCheck n b
atSurface :: forall a (n :: S) b.
HasPosition a =>
a -> TypeCheck n b -> TypeCheck n b
atSurface a
x = (Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> (Context n -> Context n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall a b. (a -> b) -> a -> b
$ \Context n
ctx ->
  Context n
ctx { ctxLocation = narrow <$> ctxLocation ctx }
  where
    narrow :: LocationInfo -> LocationInfo
narrow LocationInfo
loc = case a -> BNFC'Position
forall a. HasPosition a => a -> BNFC'Position
Rzk.hasPosition a
x of
      BNFC'Position
Nothing          -> LocationInfo
loc
      Just (Int
line, Int
col) ->
        LocationInfo
loc { locationLine = Just line, locationColumn = Just col }

-- | Elaborate a surface term in the current top-level scope: a free identifier
-- resolves to the top-level entry it names.
elaborate :: forall n. Distinct n => Rzk.Term -> TypeCheck n (Term n)
elaborate :: forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate Term' BNFC'Position
term = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  let env :: Env n
      env VarIdent
name = case VarIdent -> Context n -> Maybe (Name n)
forall (n :: S). VarIdent -> Context n -> Maybe (Name n)
lookupNamed VarIdent
name Context n
ctx of
        Just Name n
v  -> Name n -> Term n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
v
        Maybe (Name n)
Nothing -> Maybe VarIdent -> Term n
forall {n :: S}. Maybe VarIdent -> Term n
Hole (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (VarIdent -> VarIdent
markUnresolved VarIdent
name))
  pure (toTerm (ctxScope ctx) env term)

-- | Is a surface identifier defined at the top level?
checkDefined :: Distinct n => VarIdent -> TypeCheck n (Foil.Name n)
checkDefined :: forall (n :: S). Distinct n => VarIdent -> TypeCheck n (Name n)
checkDefined VarIdent
name = (Context n -> Maybe (Name n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (Name n))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (VarIdent -> Context n -> Maybe (Name n)
forall (n :: S). VarIdent -> Context n -> Maybe (Name n)
lookupNamed VarIdent
name) ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Maybe (Name n))
-> (Maybe (Name n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Name n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just Name n
v  -> Name n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name n
v
  Maybe (Name n)
Nothing -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (VarIdent -> TypeError n
forall (n :: S). VarIdent -> TypeError n
TypeErrorUndefined VarIdent
name)

splitSectionCommands
  :: Distinct n
  => Rzk.SectionName -> [Rzk.Command] -> TypeCheck n ([Rzk.Command], [Rzk.Command])
splitSectionCommands :: forall (n :: S).
Distinct n =>
SectionName -> [Command] -> TypeCheck n ([Command], [Command])
splitSectionCommands SectionName
name [] =
  TypeError n -> TypeCheck n ([Command], [Command])
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$ FilePath
"Section " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> SectionName -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree SectionName
name FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" is not closed with an #end")
splitSectionCommands SectionName
name (Rzk.CommandSection BNFC'Position
_loc SectionName
name' : [Command]
moreCommands) = do
  (cs1, cs2) <- SectionName -> [Command] -> TypeCheck n ([Command], [Command])
forall (n :: S).
Distinct n =>
SectionName -> [Command] -> TypeCheck n ([Command], [Command])
splitSectionCommands SectionName
name' [Command]
moreCommands
  (cs3, cs4) <- splitSectionCommands name cs2
  return (cs1 <> cs3, cs4)
splitSectionCommands SectionName
name (Rzk.CommandSectionEnd BNFC'Position
_loc SectionName
endName : [Command]
moreCommands) = do
  Bool
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SectionName -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree SectionName
name FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
/= SectionName -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree SectionName
endName) (ReaderT
   (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$
    TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
      FilePath
"unexpected #end " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> SectionName -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree SectionName
endName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
", expecting #end " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> SectionName -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree SectionName
name
  ([Command], [Command]) -> TypeCheck n ([Command], [Command])
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Command]
moreCommands)
splitSectionCommands SectionName
name (Command
command : [Command]
moreCommands) = do
  (cs1, cs2) <- SectionName -> [Command] -> TypeCheck n ([Command], [Command])
forall (n :: S).
Distinct n =>
SectionName -> [Command] -> TypeCheck n ([Command], [Command])
splitSectionCommands SectionName
name [Command]
moreCommands
  return (command : cs1, cs2)

-- * The module driver

-- | Check a module's commands, extending the scope with each definition.
--
-- The continuation runs in the /final/ scope, with the declarations the module
-- produced (sunk into it) and the errors found.
checkCommands
  :: forall n r. Distinct n
  => Maybe FilePath -> Integer -> Integer -> [Rzk.Command]
  -> (forall l. (DExt n l, Distinct l)
        => [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
  -> TypeCheck n r
checkCommands :: forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path Integer
i Integer
total [Command]
commands forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k = case [Command]
commands of
  [] -> [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k [] []

  command :: Command
command@(Rzk.CommandUnsetOption BNFC'Position
_loc FilePath
optionName) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
"Unsetting option " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
optionName) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
        FilePath -> TypeCheck n r -> TypeCheck n r
forall (n :: S) a.
Distinct n =>
FilePath -> TypeCheck n a -> TypeCheck n a
unsetOption FilePath
optionName (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
          Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k

  command :: Command
command@(Rzk.CommandSetOption BNFC'Position
_loc FilePath
optionName FilePath
optionValue) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
"Setting option " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
optionName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" = " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
optionValue) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
        FilePath -> FilePath -> TypeCheck n r -> TypeCheck n r
forall (n :: S) a.
Distinct n =>
FilePath -> FilePath -> TypeCheck n a -> TypeCheck n a
setOption FilePath
optionName FilePath
optionValue (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
          Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k

  command :: Command
command@(Rzk.CommandDefine BNFC'Position
_loc VarIdent
name (Rzk.DeclUsedVars BNFC'Position
_ [VarIdent]
vars) [Param]
params Term' BNFC'Position
ty Term' BNFC'Position
term) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
" Checking #define " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
name) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ do
        -- Store the elaborated type and term unreduced, but memoise their WHNF on
        -- the top node. Reducing in place would discard or expose a variable
        -- occurrence, so the section unused/implicit-assumption checks (run over the
        -- stored type and value) would disagree with the term the user wrote;
        -- keeping the WHNF cached preserves the original one-shot reduction.
        typeResult <- TypeCheck n ([Name n], TermT n)
-> TypeCheck
     n (Either TypeErrorInScopedContext ([Name n], TermT n))
forall (n :: S) a.
TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck (TypeCheck n ([Name n], TermT n)
 -> TypeCheck
      n (Either TypeErrorInScopedContext ([Name n], TermT n)))
-> TypeCheck n ([Name n], TermT n)
-> TypeCheck
     n (Either TypeErrorInScopedContext ([Name n], TermT n))
forall a b. (a -> b) -> a -> b
$ do
          used <- (VarIdent
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Name n))
-> [VarIdent]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Name n]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (VarIdent
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall (n :: S). Distinct n => VarIdent -> TypeCheck n (Name n)
checkDefined (VarIdent
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Name n))
-> (VarIdent -> VarIdent)
-> VarIdent
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe FilePath -> VarIdent -> VarIdent
varIdentAt Maybe FilePath
path) [VarIdent]
vars
          paramDecls <- concat <$> mapM paramToParamDecl params
          tyTerm <- elaborate (addParamDecls paramDecls ty)
          ty' <- atSurface ty $ memoizeWHNF =<< typecheck tyTerm universeT
          pure (used, ty')
        case typeResult of
          Left TypeErrorInScopedContext
typeError -> TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
skippingCommand TypeErrorInScopedContext
typeError Maybe FilePath
path Integer
i Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k
          Right ([Name n]
used, TermT n
ty') -> do
            -- The body is checked on its own, so that a definition whose type
            -- is fine but whose proof is not still enters the scope, as a
            -- postulate of that type. The rest of the file is then checked
            -- against it and its own errors and holes reported, instead of the
            -- run stopping at this one.
            result <- TypeCheck n (TermT n)
-> TypeCheck n (Either TypeErrorInScopedContext (TermT n))
forall (n :: S) a.
TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck (TypeCheck n (TermT n)
 -> TypeCheck n (Either TypeErrorInScopedContext (TermT n)))
-> TypeCheck n (TermT n)
-> TypeCheck n (Either TypeErrorInScopedContext (TermT n))
forall a b. (a -> b) -> a -> b
$ do
              valTerm <- Term' BNFC'Position -> TypeCheck n (Term n)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate ([Param] -> Term' BNFC'Position -> Term' BNFC'Position
addParams [Param]
params Term' BNFC'Position
term)
              atSurface term $ memoizeWHNF =<< typecheck valTerm ty'
            let (mvalue, bodyErrors) = case result of
                  Right TermT n
term'  -> (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
term', [])
                  Left TypeErrorInScopedContext
bodyErr -> (Maybe (TermT n)
forall a. Maybe a
Nothing, [TypeErrorInScopedContext
bodyErr])
            withTopLevel (varIdentAt path name) ty' mvalue False used Nothing $ \NameBinder n l
binder Decl l
decl -> do
              -- A definition with no proof term has no diagram to draw.
              termSVG <- case Maybe (TermT n)
mvalue of
                Maybe (TermT n)
Nothing -> Maybe FilePath
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe FilePath)
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe FilePath
forall a. Maybe a
Nothing
                Just TermT n
_  -> (Context l -> Maybe RenderBackend)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe RenderBackend)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context l -> Maybe RenderBackend
forall (n :: S). Context n -> Maybe RenderBackend
ctxRenderBackend ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Maybe RenderBackend)
-> (Maybe RenderBackend
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe FilePath))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe FilePath)
forall a b.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  Just RenderBackend
RenderSVG   -> TermT l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe FilePath)
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (Maybe FilePath)
renderTermSVG (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))
                  Just RenderBackend
RenderLaTeX -> TypeError l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe FilePath)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError l
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe FilePath))
-> TypeError l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$
                    FilePath -> TypeError l
forall (n :: S). FilePath -> TypeError n
TypeErrorOther FilePath
"\"latex\" rendering is not yet supported"
                  Maybe RenderBackend
Nothing          -> Maybe FilePath
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe FilePath)
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe FilePath
forall a. Maybe a
Nothing
              maybe id trace termSVG $
                checkCommands path (i + 1) total more $ \[Decl l]
decls [TypeErrorInScopedContext]
errs ->
                  [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (Decl l -> Decl l
forall (n :: S) (l :: S). DExt n l => Decl n -> Decl l
sinkDecl Decl l
decl Decl l -> [Decl l] -> [Decl l]
forall a. a -> [a] -> [a]
: [Decl l]
decls) ([TypeErrorInScopedContext]
bodyErrors [TypeErrorInScopedContext]
-> [TypeErrorInScopedContext] -> [TypeErrorInScopedContext]
forall a. Semigroup a => a -> a -> a
<> [TypeErrorInScopedContext]
errs)

  command :: Command
command@(Rzk.CommandData BNFC'Position
_loc VarIdent
name (Rzk.DeclUsedVars BNFC'Position
_ [VarIdent]
vars) [Param]
params DataSort
sort DataBody
body) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
" Checking #data " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
name) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ do
        used <- (VarIdent
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Name n))
-> [VarIdent]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Name n]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (VarIdent
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall (n :: S). Distinct n => VarIdent -> TypeCheck n (Name n)
checkDefined (VarIdent
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Name n))
-> (VarIdent -> VarIdent)
-> VarIdent
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe FilePath -> VarIdent -> VarIdent
varIdentAt Maybe FilePath
path) [VarIdent]
vars
        sortIndices <- dataSortIndices sort
        let (cons, elims) = dataBodyParts body
        paramVars <- dataParamVars params
        paramDecls <- concat <$> mapM paramToParamDecl params
        consData <- mapM
          (dataConSurface name paramVars paramDecls (length sortIndices)) cons
        withDataDecls path used name paramVars paramDecls sortIndices consData elims $ \[Decl l]
decls ->
          Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more ((forall (l :: S).
  (DExt l l, Distinct l) =>
  [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
 -> TypeCheck l r)
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall a b. (a -> b) -> a -> b
$ \[Decl l]
moreDecls [TypeErrorInScopedContext]
errs ->
            [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k ([Decl l] -> [Decl l]
forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls [Decl l]
decls [Decl l] -> [Decl l] -> [Decl l]
forall a. Semigroup a => a -> a -> a
<> [Decl l]
moreDecls) [TypeErrorInScopedContext]
errs

  command :: Command
command@(Rzk.CommandPostulate BNFC'Position
_loc VarIdent
name (Rzk.DeclUsedVars BNFC'Position
_ [VarIdent]
vars) [Param]
params Term' BNFC'Position
ty) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
" Checking #postulate " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
name) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ do
        typeResult <- TypeCheck n ([Name n], TermT n)
-> TypeCheck
     n (Either TypeErrorInScopedContext ([Name n], TermT n))
forall (n :: S) a.
TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck (TypeCheck n ([Name n], TermT n)
 -> TypeCheck
      n (Either TypeErrorInScopedContext ([Name n], TermT n)))
-> TypeCheck n ([Name n], TermT n)
-> TypeCheck
     n (Either TypeErrorInScopedContext ([Name n], TermT n))
forall a b. (a -> b) -> a -> b
$ do
          used <- (VarIdent
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Name n))
-> [VarIdent]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Name n]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (VarIdent
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall (n :: S). Distinct n => VarIdent -> TypeCheck n (Name n)
checkDefined (VarIdent
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Name n))
-> (VarIdent -> VarIdent)
-> VarIdent
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe FilePath -> VarIdent -> VarIdent
varIdentAt Maybe FilePath
path) [VarIdent]
vars
          paramDecls <- concat <$> mapM paramToParamDecl params
          tyTerm <- elaborate (addParamDecls paramDecls ty)
          ty' <- atSurface ty $ memoizeWHNF =<< typecheck tyTerm universeT
          pure (used, ty')
        case typeResult of
          Left TypeErrorInScopedContext
typeError -> TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
skippingCommand TypeErrorInScopedContext
typeError Maybe FilePath
path Integer
i Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k
          Right ([Name n]
used, TermT n
ty') ->
            VarIdent
-> TermT n
-> Maybe (TermT n)
-> Bool
-> [Name n]
-> Maybe (DataRole n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Decl l -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
VarIdent
-> TermT n
-> Maybe (TermT n)
-> Bool
-> [Name n]
-> Maybe (DataRole n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Decl l -> TypeCheck l r)
-> TypeCheck n r
withTopLevel (Maybe FilePath -> VarIdent -> VarIdent
varIdentAt Maybe FilePath
path VarIdent
name) TermT n
ty' Maybe (TermT n)
forall a. Maybe a
Nothing Bool
False [Name n]
used Maybe (DataRole n)
forall a. Maybe a
Nothing ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> Decl l -> TypeCheck l r)
 -> TypeCheck n r)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Decl l -> TypeCheck l r)
-> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
_binder Decl l
decl ->
              Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more ((forall (l :: S).
  (DExt l l, Distinct l) =>
  [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
 -> TypeCheck l r)
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall a b. (a -> b) -> a -> b
$ \[Decl l]
decls [TypeErrorInScopedContext]
errs ->
                [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (Decl l -> Decl l
forall (n :: S) (l :: S). DExt n l => Decl n -> Decl l
sinkDecl Decl l
decl Decl l -> [Decl l] -> [Decl l]
forall a. a -> [a] -> [a]
: [Decl l]
decls) [TypeErrorInScopedContext]
errs

  command :: Command
command@(Rzk.CommandAssume BNFC'Position
_loc [VarIdent]
names Term' BNFC'Position
ty) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
" Checking #assume "
        FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
" " [ VarIdent -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree VarIdent
name | VarIdent
name <- [VarIdent]
names ]) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ do
        typeResult <- TypeCheck n (TermT n)
-> TypeCheck n (Either TypeErrorInScopedContext (TermT n))
forall (n :: S) a.
TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck (TypeCheck n (TermT n)
 -> TypeCheck n (Either TypeErrorInScopedContext (TermT n)))
-> TypeCheck n (TermT n)
-> TypeCheck n (Either TypeErrorInScopedContext (TermT n))
forall a b. (a -> b) -> a -> b
$ do
          tyTerm <- Term' BNFC'Position -> TypeCheck n (Term n)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate Term' BNFC'Position
ty
          atSurface ty $ typecheck tyTerm universeT
        case typeResult of
          Left TypeErrorInScopedContext
typeError -> TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
skippingCommand TypeErrorInScopedContext
typeError Maybe FilePath
path Integer
i Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k
          Right TermT n
ty' ->
            [VarIdent]
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
[VarIdent]
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> TypeCheck l r)
-> TypeCheck n r
assume ((VarIdent -> VarIdent) -> [VarIdent] -> [VarIdent]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe FilePath -> VarIdent -> VarIdent
varIdentAt Maybe FilePath
path) [VarIdent]
names) TermT n
ty' ((forall (l :: S).
  (DExt n l, Distinct l) =>
  [Decl l] -> TypeCheck l r)
 -> TypeCheck n r)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> TypeCheck l r)
-> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ \[Decl l]
assumed ->
              Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more ((forall (l :: S).
  (DExt l l, Distinct l) =>
  [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
 -> TypeCheck l r)
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall a b. (a -> b) -> a -> b
$ \[Decl l]
decls [TypeErrorInScopedContext]
errs ->
                [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k ([Decl l] -> [Decl l]
forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls [Decl l]
assumed [Decl l] -> [Decl l] -> [Decl l]
forall a. Semigroup a => a -> a -> a
<> [Decl l]
decls) [TypeErrorInScopedContext]
errs

  command :: Command
command@(Rzk.CommandCheck BNFC'Position
_loc Term' BNFC'Position
term Term' BNFC'Position
ty) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
" Checking " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
term FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" : " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
ty) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ do
        -- A #check declares nothing, so its failure costs the rest of the file
        -- nothing either.
        result <- TypeCheck n () -> TypeCheck n (Either TypeErrorInScopedContext ())
forall (n :: S) a.
TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck (TypeCheck n ()
 -> TypeCheck n (Either TypeErrorInScopedContext ()))
-> TypeCheck n ()
-> TypeCheck n (Either TypeErrorInScopedContext ())
forall a b. (a -> b) -> a -> b
$ do
          tyTerm <- Term' BNFC'Position -> TypeCheck n (Term n)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate Term' BNFC'Position
ty
          ty' <- atSurface ty $ typecheck tyTerm universeT >>= whnfT
          termTerm <- elaborate term
          _term' <- atSurface term $ typecheck termTerm ty'
          pure ()
        case result of
          Left TypeErrorInScopedContext
err -> TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
skippingCommand TypeErrorInScopedContext
err Maybe FilePath
path Integer
i Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k
          Right () -> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k

  Rzk.CommandCompute BNFC'Position
loc Term' BNFC'Position
term : [Command]
more ->
    Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path Integer
i Integer
total (BNFC'Position -> Term' BNFC'Position -> Command
forall a. a -> Term' a -> Command' a
Rzk.CommandComputeWHNF BNFC'Position
loc Term' BNFC'Position
term Command -> [Command] -> [Command]
forall a. a -> [a] -> [a]
: [Command]
more) [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k

  command :: Command
command@(Rzk.CommandComputeNF BNFC'Position
_loc Term' BNFC'Position
term) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
" Computing NF for " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
term) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ do
        result <- TypeCheck n FilePath
-> TypeCheck n (Either TypeErrorInScopedContext FilePath)
forall (n :: S) a.
TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck (TypeCheck n FilePath
 -> TypeCheck n (Either TypeErrorInScopedContext FilePath))
-> TypeCheck n FilePath
-> TypeCheck n (Either TypeErrorInScopedContext FilePath)
forall a b. (a -> b) -> a -> b
$ do
          term' <- Term' BNFC'Position
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a (n :: S) b.
HasPosition a =>
a -> TypeCheck n b -> TypeCheck n b
atSurface Term' BNFC'Position
term (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term' BNFC'Position -> TypeCheck n (Term n)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate Term' BNFC'Position
term TypeCheck n (Term n)
-> (Term n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
nfT
          ppInContext term'
        case result of
          Left TypeErrorInScopedContext
err -> TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
skippingCommand TypeErrorInScopedContext
err Maybe FilePath
path Integer
i Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k
          Right FilePath
shown -> Verbosity -> FilePath -> TypeCheck n r -> TypeCheck n r
forall (n :: S) a.
Verbosity -> FilePath -> TypeCheck n a -> TypeCheck n a
traceTypeCheck Verbosity
Normal (FilePath
"  " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
shown) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
            Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k

  command :: Command
command@(Rzk.CommandComputeWHNF BNFC'Position
_loc Term' BNFC'Position
term) : [Command]
more ->
    FilePath -> TypeCheck n r -> TypeCheck n r
forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce (FilePath
" Computing WHNF for " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree Term' BNFC'Position
term) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ do
        result <- TypeCheck n FilePath
-> TypeCheck n (Either TypeErrorInScopedContext FilePath)
forall (n :: S) a.
TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
tryCheck (TypeCheck n FilePath
 -> TypeCheck n (Either TypeErrorInScopedContext FilePath))
-> TypeCheck n FilePath
-> TypeCheck n (Either TypeErrorInScopedContext FilePath)
forall a b. (a -> b) -> a -> b
$ do
          term' <- Term' BNFC'Position
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a (n :: S) b.
HasPosition a =>
a -> TypeCheck n b -> TypeCheck n b
atSurface Term' BNFC'Position
term (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term' BNFC'Position -> TypeCheck n (Term n)
forall (n :: S).
Distinct n =>
Term' BNFC'Position -> TypeCheck n (Term n)
elaborate Term' BNFC'Position
term TypeCheck n (Term n)
-> (Term n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT
          ppInContext term'
        case result of
          Left TypeErrorInScopedContext
err -> TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
TypeErrorInScopedContext
-> Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
skippingCommand TypeErrorInScopedContext
err Maybe FilePath
path Integer
i Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k
          Right FilePath
shown -> Verbosity -> FilePath -> TypeCheck n r -> TypeCheck n r
forall (n :: S) a.
Verbosity -> FilePath -> TypeCheck n a -> TypeCheck n a
traceTypeCheck Verbosity
Normal (FilePath
"  " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
shown) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
            Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
total [Command]
more [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k

  command :: Command
command@(Rzk.CommandSection BNFC'Position
_loc SectionName
name) : [Command]
more ->
    Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ do
      (sectionCommands, more') <- SectionName -> [Command] -> TypeCheck n ([Command], [Command])
forall (n :: S).
Distinct n =>
SectionName -> [Command] -> TypeCheck n ([Command], [Command])
splitSectionCommands SectionName
name [Command]
more
      withSection (Just name) i sectionCommands path total $ \[Decl l]
sectionDecls [TypeErrorInScopedContext]
sectionErrs ->
        if [TypeErrorInScopedContext] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeErrorInScopedContext]
sectionErrs
          then Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ [Command] -> Integer
forall a. Integral a => [Command] -> a
countCommands [Command]
sectionCommands) Integer
total [Command]
more' ((forall (l :: S).
  (DExt l l, Distinct l) =>
  [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
 -> TypeCheck l r)
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall a b. (a -> b) -> a -> b
$
            \[Decl l]
decls [TypeErrorInScopedContext]
errs -> [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k ([Decl l] -> [Decl l]
forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls [Decl l]
sectionDecls [Decl l] -> [Decl l] -> [Decl l]
forall a. Semigroup a => a -> a -> a
<> [Decl l]
decls) [TypeErrorInScopedContext]
errs
          else [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k [Decl l]
sectionDecls [TypeErrorInScopedContext]
sectionErrs

  command :: Command
command@(Rzk.CommandSectionEnd BNFC'Position
_loc SectionName
endName) : [Command]
_more ->
    Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Command
-> ([Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r)
-> TypeCheck n r
-> TypeCheck n r
withCommand Command
command [Decl n] -> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      TypeError n -> TypeCheck n r
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n r) -> TypeError n -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError n
forall (n :: S). FilePath -> TypeError n
TypeErrorOther (FilePath -> TypeError n) -> FilePath -> TypeError n
forall a b. (a -> b) -> a -> b
$
        FilePath
"unexpected #end " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> SectionName -> FilePath
forall a. Print a => a -> FilePath
Rzk.printTree SectionName
endName FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
", no section was declared!"
  where
    announce :: String -> TypeCheck n a -> TypeCheck n a
    announce :: forall a. FilePath -> TypeCheck n a -> TypeCheck n a
announce FilePath
what =
      Verbosity -> FilePath -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a.
Verbosity -> FilePath -> TypeCheck n a -> TypeCheck n a
traceTypeCheck Verbosity
Normal
        (FilePath
"[ " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
i FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" out of " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
total FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" ]" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
what)

-- | Assume a list of names of the same type, each a top-level entry.
assume
  :: Distinct n
  => [VarIdent] -> TermT n
  -> (forall l. (DExt n l, Distinct l) => [Decl l] -> TypeCheck l r)
  -> TypeCheck n r
assume :: forall (n :: S) r.
Distinct n =>
[VarIdent]
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> TypeCheck l r)
-> TypeCheck n r
assume [] TermT n
_ty forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> TypeCheck l r
k = [Decl n] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> TypeCheck l r
k []
assume (VarIdent
name : [VarIdent]
names) TermT n
ty forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> TypeCheck l r
k =
  VarIdent
-> TermT n
-> Maybe (TermT n)
-> Bool
-> [Name n]
-> Maybe (DataRole n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Decl l -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
VarIdent
-> TermT n
-> Maybe (TermT n)
-> Bool
-> [Name n]
-> Maybe (DataRole n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Decl l -> TypeCheck l r)
-> TypeCheck n r
withTopLevel VarIdent
name TermT n
ty Maybe (TermT n)
forall a. Maybe a
Nothing Bool
True [] Maybe (DataRole n)
forall a. Maybe a
Nothing ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> Decl l -> TypeCheck l r)
 -> TypeCheck n r)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Decl l -> TypeCheck l r)
-> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
_binder Decl l
decl ->
    [VarIdent]
-> TermT l
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> TypeCheck l r)
-> TypeCheck l r
forall (n :: S) r.
Distinct n =>
[VarIdent]
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> TypeCheck l r)
-> TypeCheck n r
assume [VarIdent]
names (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
ty) ((forall (l :: S).
  (DExt l l, Distinct l) =>
  [Decl l] -> TypeCheck l r)
 -> TypeCheck l r)
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [Decl l] -> TypeCheck l r)
-> TypeCheck l r
forall a b. (a -> b) -> a -> b
$ \[Decl l]
decls ->
      [Decl l] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> TypeCheck l r
k (Decl l -> Decl l
forall (n :: S) (l :: S). DExt n l => Decl n -> Decl l
sinkDecl Decl l
decl Decl l -> [Decl l] -> [Decl l]
forall a. a -> [a] -> [a]
: [Decl l]
decls)

-- | Check the commands of a section, then close it.
withSection
  :: forall n r. Distinct n
  => Maybe Rzk.SectionName -> Integer -> [Rzk.Command] -> Maybe FilePath -> Integer
  -> (forall l. (DExt n l, Distinct l)
        => [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
  -> TypeCheck n r
withSection :: forall (n :: S) r.
Distinct n =>
Maybe SectionName
-> Integer
-> [Command]
-> Maybe FilePath
-> Integer
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
withSection Maybe SectionName
name Integer
i [Command]
sectionCommands Maybe FilePath
path Integer
total forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k =
  Maybe SectionName -> TypeCheck n r -> TypeCheck n r
forall (n :: S) a.
Maybe SectionName -> TypeCheck n a -> TypeCheck n a
startSection Maybe SectionName
name (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
    Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Integer
-> Integer
-> [Command]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkCommands Maybe FilePath
path Integer
i Integer
total [Command]
sectionCommands ((forall (l :: S).
  (DExt n l, Distinct l) =>
  [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
 -> TypeCheck n r)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ \[Decl l]
_decls [TypeErrorInScopedContext]
errs ->
      Action l -> TypeCheck l r -> TypeCheck l r
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing (Maybe SectionName -> Action l
forall (n :: S). Maybe SectionName -> Action n
ActionCloseSection Maybe SectionName
name) (TypeCheck l r -> TypeCheck l r) -> TypeCheck l r -> TypeCheck l r
forall a b. (a -> b) -> a -> b
$ do
        result <- (([Decl l], [TypeErrorInScopedContext], Context l)
-> Either
     TypeErrorInScopedContext
     ([Decl l], [TypeErrorInScopedContext], Context l)
forall a b. b -> Either a b
Right (([Decl l], [TypeErrorInScopedContext], Context l)
 -> Either
      TypeErrorInScopedContext
      ([Decl l], [TypeErrorInScopedContext], Context l))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     ([Decl l], [TypeErrorInScopedContext], Context l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Either
        TypeErrorInScopedContext
        ([Decl l], [TypeErrorInScopedContext], Context l))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypeErrorInScopedContext]
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     ([Decl l], [TypeErrorInScopedContext], Context l)
forall (n :: S).
Distinct n =>
[TypeErrorInScopedContext]
-> TypeCheck n ([Decl n], [TypeErrorInScopedContext], Context n)
endSection [TypeErrorInScopedContext]
errs) ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Either
     TypeErrorInScopedContext
     ([Decl l], [TypeErrorInScopedContext], Context l))
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Either
            TypeErrorInScopedContext
            ([Decl l], [TypeErrorInScopedContext], Context l)))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Either
        TypeErrorInScopedContext
        ([Decl l], [TypeErrorInScopedContext], Context l))
forall a.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (Either
  TypeErrorInScopedContext
  ([Decl l], [TypeErrorInScopedContext], Context l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Either
        TypeErrorInScopedContext
        ([Decl l], [TypeErrorInScopedContext], Context l))
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   TypeErrorInScopedContext
   ([Decl l], [TypeErrorInScopedContext], Context l)
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Either
         TypeErrorInScopedContext
         ([Decl l], [TypeErrorInScopedContext], Context l)))
-> (TypeErrorInScopedContext
    -> Either
         TypeErrorInScopedContext
         ([Decl l], [TypeErrorInScopedContext], Context l))
-> TypeErrorInScopedContext
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Either
        TypeErrorInScopedContext
        ([Decl l], [TypeErrorInScopedContext], Context l))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeErrorInScopedContext
-> Either
     TypeErrorInScopedContext
     ([Decl l], [TypeErrorInScopedContext], Context l)
forall a b. a -> Either a b
Left)
        case result of
          Left TypeErrorInScopedContext
err -> [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k [] ([TypeErrorInScopedContext]
errs [TypeErrorInScopedContext]
-> [TypeErrorInScopedContext] -> [TypeErrorInScopedContext]
forall a. Semigroup a => a -> a -> a
<> [TypeErrorInScopedContext
err])
          Right ([Decl l]
decls', [TypeErrorInScopedContext]
errs', Context l
ctx') -> Context l -> TypeCheck l r -> TypeCheck l r
forall (l :: S) a (n :: S).
Context l -> TypeCheck l a -> TypeCheck n a
inContext Context l
ctx' ([Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k [Decl l]
decls' [TypeErrorInScopedContext]
errs')

-- | Check one module.
checkModule
  :: forall n r. Distinct n
  => Maybe FilePath -> Rzk.Module
  -> (forall l. (DExt n l, Distinct l)
        => [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
  -> TypeCheck n r
checkModule :: forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Module
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkModule Maybe FilePath
path (Rzk.Module BNFC'Position
_moduleLoc LanguageDecl' BNFC'Position
_lang [Command]
commands) forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k =
  -- FIXME: use the module name? or an anonymous section?
  Maybe SectionName
-> Integer
-> [Command]
-> Maybe FilePath
-> Integer
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe SectionName
-> Integer
-> [Command]
-> Maybe FilePath
-> Integer
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
withSection Maybe SectionName
forall a. Maybe a
Nothing Integer
1 [Command]
commands Maybe FilePath
path ([Command] -> Integer
forall a. Integral a => [Command] -> a
countCommands [Command]
commands) [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k

checkModuleWithLocation
  :: Distinct n
  => (FilePath, Rzk.Module)
  -> (forall l. (DExt n l, Distinct l)
        => [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
  -> TypeCheck n r
checkModuleWithLocation :: forall (n :: S) r.
Distinct n =>
(FilePath, Module)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkModuleWithLocation (FilePath
path, Module
module_) forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k =
  Verbosity -> FilePath -> TypeCheck n r -> TypeCheck n r
forall (n :: S) a.
Verbosity -> FilePath -> TypeCheck n a -> TypeCheck n a
traceTypeCheck Verbosity
Normal (FilePath
"Checking module from " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
path) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
    LocationInfo -> TypeCheck n r -> TypeCheck n r
forall (n :: S) a. LocationInfo -> TypeCheck n a -> TypeCheck n a
withLocation (LocationInfo
      { locationFilePath :: Maybe FilePath
locationFilePath = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
path
      , locationLine :: Maybe Int
locationLine = Maybe Int
forall a. Maybe a
Nothing
      , locationColumn :: Maybe Int
locationColumn = Maybe Int
forall a. Maybe a
Nothing }) (TypeCheck n r -> TypeCheck n r) -> TypeCheck n r -> TypeCheck n r
forall a b. (a -> b) -> a -> b
$
      Maybe FilePath
-> Module
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
Maybe FilePath
-> Module
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkModule (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
path) Module
module_ [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r
k

-- | Check a list of modules, one after another, in a scope that grows as it goes.
--
-- Checking stops at the first module with an error, as it did before.
checkModules
  :: forall n r. Distinct n
  => [(FilePath, Rzk.Module)]
  -> (forall l. (DExt n l, Distinct l)
        => [(FilePath, [Decl l])] -> [TypeErrorInScopedContext] -> TypeCheck l r)
  -> TypeCheck n r
checkModules :: forall (n :: S) r.
Distinct n =>
[(FilePath, Module)]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkModules [] forall (l :: S).
(DExt n l, Distinct l) =>
[(FilePath, [Decl l])]
-> [TypeErrorInScopedContext] -> TypeCheck l r
k = [(FilePath, [Decl n])]
-> [TypeErrorInScopedContext] -> TypeCheck n r
forall (l :: S).
(DExt n l, Distinct l) =>
[(FilePath, [Decl l])]
-> [TypeErrorInScopedContext] -> TypeCheck l r
k [] []
checkModules (m :: (FilePath, Module)
m@(FilePath
path, Module
_) : [(FilePath, Module)]
ms) forall (l :: S).
(DExt n l, Distinct l) =>
[(FilePath, [Decl l])]
-> [TypeErrorInScopedContext] -> TypeCheck l r
k =
  (FilePath, Module)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall (n :: S) r.
Distinct n =>
(FilePath, Module)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkModuleWithLocation (FilePath, Module)
m ((forall (l :: S).
  (DExt n l, Distinct l) =>
  [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
 -> TypeCheck n r)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
forall a b. (a -> b) -> a -> b
$ \[Decl l]
decls [TypeErrorInScopedContext]
errs ->
    case [TypeErrorInScopedContext]
errs of
      TypeErrorInScopedContext
_:[TypeErrorInScopedContext]
_ -> [(FilePath, [Decl l])]
-> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[(FilePath, [Decl l])]
-> [TypeErrorInScopedContext] -> TypeCheck l r
k [(FilePath
path, [Decl l]
decls)] [TypeErrorInScopedContext]
errs
      [TypeErrorInScopedContext]
_ -> [(FilePath, Module)]
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall (n :: S) r.
Distinct n =>
[(FilePath, Module)]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkModules [(FilePath, Module)]
ms ((forall (l :: S).
  (DExt l l, Distinct l) =>
  [(FilePath, [Decl l])]
  -> [TypeErrorInScopedContext] -> TypeCheck l r)
 -> TypeCheck l r)
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck l r
forall a b. (a -> b) -> a -> b
$ \[(FilePath, [Decl l])]
rest [TypeErrorInScopedContext]
errors ->
        [(FilePath, [Decl l])]
-> [TypeErrorInScopedContext] -> TypeCheck l r
forall (l :: S).
(DExt n l, Distinct l) =>
[(FilePath, [Decl l])]
-> [TypeErrorInScopedContext] -> TypeCheck l r
k ((FilePath
path, [Decl l] -> [Decl l]
forall (n :: S) (l :: S). DExt n l => [Decl n] -> [Decl l]
sinkDecls [Decl l]
decls) (FilePath, [Decl l])
-> [(FilePath, [Decl l])] -> [(FilePath, [Decl l])]
forall a. a -> [a] -> [a]
: [(FilePath, [Decl l])]
rest) [TypeErrorInScopedContext]
errors

-- * The public entry points

-- | Check the modules, and package the result with the scope it was checked in.
-- The warnings are recorded during the run and are folded into the 'Checked'
-- package here.
checkedModules :: [(FilePath, Rzk.Module)] -> Context Foil.VoidS -> Either TypeErrorInScopedContext (Checked, [HoleInfo])
checkedModules :: [(FilePath, Module)]
-> Context 'VoidS
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
checkedModules [(FilePath, Module)]
modules Context 'VoidS
ctx =
  (Either TypeErrorInScopedContext Checked,
 ([HoleInfo], [CheckWarning]))
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
forall {a} {b}.
(Either a Checked, (b, [CheckWarning])) -> Either a (Checked, b)
package ((Either TypeErrorInScopedContext Checked,
  ([HoleInfo], [CheckWarning]))
 -> Either TypeErrorInScopedContext (Checked, [HoleInfo]))
-> (Either TypeErrorInScopedContext Checked,
    ([HoleInfo], [CheckWarning]))
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
forall a b. (a -> b) -> a -> b
$ Context 'VoidS
-> TypeCheck 'VoidS Checked
-> (Either TypeErrorInScopedContext Checked,
    ([HoleInfo], [CheckWarning]))
forall (n :: S) a.
Context n
-> TypeCheck n a
-> (Either TypeErrorInScopedContext a,
    ([HoleInfo], [CheckWarning]))
runTypeCheckWith Context 'VoidS
ctx (TypeCheck 'VoidS Checked
 -> (Either TypeErrorInScopedContext Checked,
     ([HoleInfo], [CheckWarning])))
-> TypeCheck 'VoidS Checked
-> (Either TypeErrorInScopedContext Checked,
    ([HoleInfo], [CheckWarning]))
forall a b. (a -> b) -> a -> b
$
    [(FilePath, Module)]
-> (forall (l :: S).
    (DExt 'VoidS l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l Checked)
-> TypeCheck 'VoidS Checked
forall (n :: S) r.
Distinct n =>
[(FilePath, Module)]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkModules [(FilePath, Module)]
modules ((forall (l :: S).
  (DExt 'VoidS l, Distinct l) =>
  [(FilePath, [Decl l])]
  -> [TypeErrorInScopedContext] -> TypeCheck l Checked)
 -> TypeCheck 'VoidS Checked)
-> (forall (l :: S).
    (DExt 'VoidS l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l Checked)
-> TypeCheck 'VoidS Checked
forall a b. (a -> b) -> a -> b
$ \[(FilePath, [Decl l])]
decls [TypeErrorInScopedContext]
errs -> do
      ctx' <- ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context l)
forall r (m :: * -> *). MonadReader r m => m r
ask
      pure (Checked ctx' decls errs [])
  where
    package :: (Either a Checked, (b, [CheckWarning])) -> Either a (Checked, b)
package (Left a
err, (b, [CheckWarning])
_) = a -> Either a (Checked, b)
forall a b. a -> Either a b
Left a
err
    package (Right (Checked Context n
ctx' [(FilePath, [Decl n])]
decls [TypeErrorInScopedContext]
errs [CheckWarning]
_), (b
holes, [CheckWarning]
warnings)) =
      (Checked, b) -> Either a (Checked, b)
forall a b. b -> Either a b
Right (Context n
-> [(FilePath, [Decl n])]
-> [TypeErrorInScopedContext]
-> [CheckWarning]
-> Checked
forall (n :: S).
Distinct n =>
Context n
-> [(FilePath, [Decl n])]
-> [TypeErrorInScopedContext]
-> [CheckWarning]
-> Checked
Checked Context n
ctx' [(FilePath, [Decl n])]
decls [TypeErrorInScopedContext]
errs [CheckWarning]
warnings, b
holes)

-- | Check the modules strictly: an unfilled hole is an error, and the first error
-- stops the run.
typecheckModules
  :: [(FilePath, Rzk.Module)] -> Either TypeErrorInScopedContext Checked
typecheckModules :: [(FilePath, Module)] -> Either TypeErrorInScopedContext Checked
typecheckModules [(FilePath, Module)]
modules = do
  (checked@(Checked _ _ errs _), _holes) <- [(FilePath, Module)]
-> Context 'VoidS
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
checkedModules [(FilePath, Module)]
modules Context 'VoidS
emptyContext
  case errs of
    TypeErrorInScopedContext
err : [TypeErrorInScopedContext]
_ -> TypeErrorInScopedContext -> Either TypeErrorInScopedContext Checked
forall a b. a -> Either a b
Left TypeErrorInScopedContext
err
    []      -> Checked -> Either TypeErrorInScopedContext Checked
forall a b. b -> Either a b
Right Checked
checked

-- | Check the modules in lenient hole mode, returning the holes recorded (each
-- with its goal and local context). This is the structured goal/context query the
-- LSP and the game consume.
typecheckModulesWithHoles
  :: [(FilePath, Rzk.Module)]
  -> Either TypeErrorInScopedContext (Checked, [HoleInfo])
typecheckModulesWithHoles :: [(FilePath, Module)]
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
typecheckModulesWithHoles = [VarIdent]
-> [(FilePath, Module)]
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
typecheckModulesWithHolesAndLemmas []

-- | Like 'typecheckModulesWithHoles', but additionally offers the given named
-- top-level definitions as hole candidates (each applied to holes when its type
-- fits the goal, and never below its meta prefix — an unsaturated schema is not
-- a suggestion, see "Rzk.TypeCheck.MetaPrefix"). The game passes a level's
-- allow-list of relevant lemmas so they surface as moves; an empty list
-- reproduces 'typecheckModulesWithHoles'.
typecheckModulesWithHolesAndLemmas
  :: [VarIdent]
  -> [(FilePath, Rzk.Module)]
  -> Either TypeErrorInScopedContext (Checked, [HoleInfo])
typecheckModulesWithHolesAndLemmas :: [VarIdent]
-> [(FilePath, Module)]
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
typecheckModulesWithHolesAndLemmas [VarIdent]
lemmas [(FilePath, Module)]
modules =
  [(FilePath, Module)]
-> Context 'VoidS
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
checkedModules [(FilePath, Module)]
modules ([VarIdent] -> Context 'VoidS -> Context 'VoidS
forall (n :: S). [VarIdent] -> Context n -> Context n
withHintLemmas [VarIdent]
lemmas (Context 'VoidS -> Context 'VoidS
forall (n :: S). Context n -> Context n
allowHoles Context 'VoidS
emptyContext))

-- * What a consumer sees

-- | A declaration, rendered: no scope index, and nothing to re-elaborate.
--
-- This is what the LSP shows — a name, a type, a location — and it is all it needs.
-- The elaborated terms stay inside the 'Checked' package, which is what a /resume/
-- needs.
data DeclView = DeclView
  { DeclView -> VarIdent
declViewName         :: VarIdent
  , DeclView -> Rendered
declViewType         :: Rendered
  , DeclView -> Bool
declViewIsAssumption :: Bool
  , DeclView -> Maybe LocationInfo
declViewLocation     :: Maybe LocationInfo
  , DeclView -> DeclKind
declViewKind         :: DeclKind
  } deriving (DeclView -> DeclView -> Bool
(DeclView -> DeclView -> Bool)
-> (DeclView -> DeclView -> Bool) -> Eq DeclView
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DeclView -> DeclView -> Bool
== :: DeclView -> DeclView -> Bool
$c/= :: DeclView -> DeclView -> Bool
/= :: DeclView -> DeclView -> Bool
Eq, Int -> DeclView -> FilePath -> FilePath
[DeclView] -> FilePath -> FilePath
DeclView -> FilePath
(Int -> DeclView -> FilePath -> FilePath)
-> (DeclView -> FilePath)
-> ([DeclView] -> FilePath -> FilePath)
-> Show DeclView
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
$cshowsPrec :: Int -> DeclView -> FilePath -> FilePath
showsPrec :: Int -> DeclView -> FilePath -> FilePath
$cshow :: DeclView -> FilePath
show :: DeclView -> FilePath
$cshowList :: [DeclView] -> FilePath -> FilePath
showList :: [DeclView] -> FilePath -> FilePath
Show)

-- | What kind of declaration a 'DeclView' renders: a plain definition, a
-- postulate, or one of the products of a @#data@ (the symbol providers group
-- constructors under their type and keep the generated eliminators out of
-- the outline; the semantic tokens highlight postulates distinctly).
data DeclKind
  = DeclKindDefine
  | DeclKindPostulate          -- ^ a @#postulate@ or @#assume@: declared, but not proven
  | DeclKindData
  | DeclKindDataCon VarIdent   -- ^ a constructor of the named type
  | DeclKindDataElim VarIdent  -- ^ a generated eliminator of the named type
  deriving (DeclKind -> DeclKind -> Bool
(DeclKind -> DeclKind -> Bool)
-> (DeclKind -> DeclKind -> Bool) -> Eq DeclKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DeclKind -> DeclKind -> Bool
== :: DeclKind -> DeclKind -> Bool
$c/= :: DeclKind -> DeclKind -> Bool
/= :: DeclKind -> DeclKind -> Bool
Eq, Int -> DeclKind -> FilePath -> FilePath
[DeclKind] -> FilePath -> FilePath
DeclKind -> FilePath
(Int -> DeclKind -> FilePath -> FilePath)
-> (DeclKind -> FilePath)
-> ([DeclKind] -> FilePath -> FilePath)
-> Show DeclKind
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
$cshowsPrec :: Int -> DeclKind -> FilePath -> FilePath
showsPrec :: Int -> DeclKind -> FilePath -> FilePath
$cshow :: DeclKind -> FilePath
show :: DeclKind -> FilePath
$cshowList :: [DeclKind] -> FilePath -> FilePath
showList :: [DeclKind] -> FilePath -> FilePath
Show)

-- | The declarations of a checked run, rendered, grouped by the file they came
-- from.
declViews :: Checked -> [(FilePath, [DeclView])]
declViews :: Checked -> [(FilePath, [DeclView])]
declViews (Checked Context n
ctx [(FilePath, [Decl n])]
decls [TypeErrorInScopedContext]
_errs [CheckWarning]
_warnings) = ((FilePath, [Decl n]) -> (FilePath, [DeclView]))
-> [(FilePath, [Decl n])] -> [(FilePath, [DeclView])]
forall a b. (a -> b) -> [a] -> [b]
map (([Decl n] -> [DeclView])
-> (FilePath, [Decl n]) -> (FilePath, [DeclView])
forall a b. (a -> b) -> (FilePath, a) -> (FilePath, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Decl n -> DeclView) -> [Decl n] -> [DeclView]
forall a b. (a -> b) -> [a] -> [b]
map Decl n -> DeclView
view)) [(FilePath, [Decl n])]
decls
  where
    naming :: Naming n
naming = Context n -> Naming n
forall (n :: S). Context n -> Naming n
namingOfContext Context n
ctx
    -- The type formers carry no role themselves; they are the names the
    -- constructor and eliminator roles point at.
    formerIds :: [Int]
formerIds =
      [ Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId (DataRole n -> Name n
forall (n :: S). DataRole n -> Name n
dataRoleDataType DataRole n
role)
      | Decl n
d <- ((FilePath, [Decl n]) -> [Decl n])
-> [(FilePath, [Decl n])] -> [Decl n]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FilePath, [Decl n]) -> [Decl n]
forall a b. (a, b) -> b
snd [(FilePath, [Decl n])]
decls
      , Just DataRole n
role <- [VarInfo n -> Maybe (DataRole n)
forall (n :: S). VarInfo n -> Maybe (DataRole n)
varDataRole (Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo (Decl n -> Name n
forall (n :: S). Decl n -> Name n
declNameOf Decl n
d) Context n
ctx)] ]
    parentNameOf :: Name n -> VarIdent
parentNameOf Name n
p = case Binder -> Maybe VarIdent
binderName (VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig (Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
p Context n
ctx)) of
      Just VarIdent
x  -> VarIdent
x
      Maybe VarIdent
Nothing -> VarIdent
"_"
    kindOf :: Decl n -> DeclKind
kindOf Decl n
d = case VarInfo n -> Maybe (DataRole n)
forall (n :: S). VarInfo n -> Maybe (DataRole n)
varDataRole (Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo (Decl n -> Name n
forall (n :: S). Decl n -> Name n
declNameOf Decl n
d) Context n
ctx) of
      Just (DataRole Name n
parent Int
_ DataConKind{})  -> VarIdent -> DeclKind
DeclKindDataCon (Name n -> VarIdent
parentNameOf Name n
parent)
      Just (DataRole Name n
parent Int
_ DataElimKind{}) -> VarIdent -> DeclKind
DeclKindDataElim (Name n -> VarIdent
parentNameOf Name n
parent)
      Maybe (DataRole n)
Nothing
        | Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId (Decl n -> Name n
forall (n :: S). Decl n -> Name n
declNameOf Decl n
d) Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
formerIds -> DeclKind
DeclKindData
        -- A declaration with no value is an axiom, whether written as a
        -- @#postulate@ or an @#assume@ (in practice both are used for
        -- axioms such as function extensionality).
        | Maybe (TermT n)
Nothing <- Decl n -> Maybe (TermT n)
forall (n :: S). Decl n -> Maybe (TermT n)
declValue Decl n
d -> DeclKind
DeclKindPostulate
        | Bool
otherwise -> DeclKind
DeclKindDefine
    view :: Decl n -> DeclView
view Decl n
decl = DeclView
      { declViewName :: VarIdent
declViewName = Decl n -> VarIdent
forall (n :: S). Decl n -> VarIdent
declName Decl n
decl
      , declViewType :: Rendered
declViewType = Naming n -> Term n -> Rendered
forall (n :: S). Naming n -> Term n -> Rendered
renderTerm Naming n
naming (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped (Decl n -> TermT n
forall (n :: S). Decl n -> TermT n
declType Decl n
decl))
      , declViewIsAssumption :: Bool
declViewIsAssumption = Decl n -> Bool
forall (n :: S). Decl n -> Bool
declIsAssumption Decl n
decl
      , declViewLocation :: Maybe LocationInfo
declViewLocation = Decl n -> Maybe LocationInfo
forall (n :: S). Decl n -> Maybe LocationInfo
declLocation Decl n
decl
      , declViewKind :: DeclKind
declViewKind = Decl n -> DeclKind
kindOf Decl n
decl
      }

-- | Continue checking from a prefix that has already been checked.
--
-- This is the incremental path: the cached context /is/ the elaborated prefix, so
-- nothing is replayed and nothing is re-elaborated.
recheckFrom
  :: Checked
  -> [(FilePath, Rzk.Module)]
  -> Either TypeErrorInScopedContext (Checked, [HoleInfo])
recheckFrom :: Checked
-> [(FilePath, Module)]
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
recheckFrom (Checked Context n
ctx [(FilePath, [Decl n])]
decls [TypeErrorInScopedContext]
_errs [CheckWarning]
_warnings) [(FilePath, Module)]
modules =
  (Either TypeErrorInScopedContext Checked,
 ([HoleInfo], [CheckWarning]))
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
forall {a} {b}.
(Either a Checked, (b, [CheckWarning])) -> Either a (Checked, b)
package ((Either TypeErrorInScopedContext Checked,
  ([HoleInfo], [CheckWarning]))
 -> Either TypeErrorInScopedContext (Checked, [HoleInfo]))
-> (Either TypeErrorInScopedContext Checked,
    ([HoleInfo], [CheckWarning]))
-> Either TypeErrorInScopedContext (Checked, [HoleInfo])
forall a b. (a -> b) -> a -> b
$ Context n
-> TypeCheck n Checked
-> (Either TypeErrorInScopedContext Checked,
    ([HoleInfo], [CheckWarning]))
forall (n :: S) a.
Context n
-> TypeCheck n a
-> (Either TypeErrorInScopedContext a,
    ([HoleInfo], [CheckWarning]))
runTypeCheckWith Context n
ctx (TypeCheck n Checked
 -> (Either TypeErrorInScopedContext Checked,
     ([HoleInfo], [CheckWarning])))
-> TypeCheck n Checked
-> (Either TypeErrorInScopedContext Checked,
    ([HoleInfo], [CheckWarning]))
forall a b. (a -> b) -> a -> b
$
    [(FilePath, Module)]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l Checked)
-> TypeCheck n Checked
forall (n :: S) r.
Distinct n =>
[(FilePath, Module)]
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l r)
-> TypeCheck n r
checkModules [(FilePath, Module)]
modules ((forall (l :: S).
  (DExt n l, Distinct l) =>
  [(FilePath, [Decl l])]
  -> [TypeErrorInScopedContext] -> TypeCheck l Checked)
 -> TypeCheck n Checked)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    [(FilePath, [Decl l])]
    -> [TypeErrorInScopedContext] -> TypeCheck l Checked)
-> TypeCheck n Checked
forall a b. (a -> b) -> a -> b
$ \[(FilePath, [Decl l])]
newDecls [TypeErrorInScopedContext]
errs -> do
      ctx' <- ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context l)
forall r (m :: * -> *). MonadReader r m => m r
ask
      pure (Checked ctx' (sinkDeclGroups decls <> newDecls) errs [])
  where
    -- Only this run's warnings: like the errors, the prefix's warnings were
    -- already reported when the prefix was checked.
    package :: (Either a Checked, (b, [CheckWarning])) -> Either a (Checked, b)
package (Left a
err, (b, [CheckWarning])
_) = a -> Either a (Checked, b)
forall a b. a -> Either a b
Left a
err
    package (Right (Checked Context n
ctx' [(FilePath, [Decl n])]
decls' [TypeErrorInScopedContext]
errs [CheckWarning]
_), (b
holes, [CheckWarning]
warnings)) =
      (Checked, b) -> Either a (Checked, b)
forall a b. b -> Either a b
Right (Context n
-> [(FilePath, [Decl n])]
-> [TypeErrorInScopedContext]
-> [CheckWarning]
-> Checked
forall (n :: S).
Distinct n =>
Context n
-> [(FilePath, [Decl n])]
-> [TypeErrorInScopedContext]
-> [CheckWarning]
-> Checked
Checked Context n
ctx' [(FilePath, [Decl n])]
decls' [TypeErrorInScopedContext]
errs [CheckWarning]
warnings, b
holes)

-- | The errors of a checked run.
checkedErrors :: Checked -> [TypeErrorInScopedContext]
checkedErrors :: Checked -> [TypeErrorInScopedContext]
checkedErrors (Checked Context n
_ [(FilePath, [Decl n])]
_ [TypeErrorInScopedContext]
errs [CheckWarning]
_) = [TypeErrorInScopedContext]
errs

-- | The warnings of a checked run.
checkedWarnings :: Checked -> [CheckWarning]
checkedWarnings :: Checked -> [CheckWarning]
checkedWarnings (Checked Context n
_ [(FilePath, [Decl n])]
_ [TypeErrorInScopedContext]
_ [CheckWarning]
warnings) = [CheckWarning]
warnings

-- | Nothing checked yet: the empty context, and no declarations.
emptyChecked :: Checked
emptyChecked :: Checked
emptyChecked = Context 'VoidS
-> [(FilePath, [Decl 'VoidS])]
-> [TypeErrorInScopedContext]
-> [CheckWarning]
-> Checked
forall (n :: S).
Distinct n =>
Context n
-> [(FilePath, [Decl n])]
-> [TypeErrorInScopedContext]
-> [CheckWarning]
-> Checked
Checked Context 'VoidS
emptyContext [] [] []

-- | Nothing checked yet, in lenient hole mode: what an editor resumes from.
--
-- A hole is work in progress there, to be reported with its goal and context
-- rather than as an error (see 'allowHoles'). 'recheckFrom' continues in the
-- context it is given, so the mode has to be set on the empty one it starts
-- with: resuming from 'emptyChecked' made every hole a @TypeErrorUnsolvedHole@
-- and stopped the file at the first one.
emptyCheckedWithHoles :: Checked
emptyCheckedWithHoles :: Checked
emptyCheckedWithHoles = Context 'VoidS
-> [(FilePath, [Decl 'VoidS])]
-> [TypeErrorInScopedContext]
-> [CheckWarning]
-> Checked
forall (n :: S).
Distinct n =>
Context n
-> [(FilePath, [Decl n])]
-> [TypeErrorInScopedContext]
-> [CheckWarning]
-> Checked
Checked (Context 'VoidS -> Context 'VoidS
forall (n :: S). Context n -> Context n
allowHoles Context 'VoidS
emptyContext) [] [] []