{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}

-- | The surface-syntax scaffolding of @#data@ declarations, kept separate from
-- the monadic checker in "Rzk.TypeCheck.Decl".
--
-- Two things live here, both pure. First, small builders over the surface
-- syntax (@surfaceApps@, @surfacePi@, …) and the preprocessed forms of a
-- declaration (the 'SortIndex' telescope and the 'DataConSurface'
-- constructors). Second, the construction of the generated eliminators: given
-- an 'ElimSpec' — the declaration's data together with the fresh binders of the
-- generated types and the validated endpoint images — 'elimTerms' produces the
-- surface types of @ind-D@ and @rec-D@ and the path computation rules. The
-- checker then pushes those surface terms through the ordinary elaborator, so
-- nothing here constructs core terms or touches the type-checking monad.
module Rzk.TypeCheck.Decl.Data where

import           Data.Data          (Data, cast, gmapQ)
import qualified Data.Text          as T

import qualified Language.Rzk.Syntax as Rzk
import           Rzk.TypeCheck.Display (panicImpossible)

-- * Surface-syntax builders and preprocessed forms

addParamDecls :: [Rzk.ParamDecl] -> Rzk.Term -> Rzk.Term
addParamDecls :: [ParamDecl] -> Term -> Term
addParamDecls [] = Term -> Term
forall a. a -> a
id
addParamDecls (ParamDecl
paramDecl : [ParamDecl]
paramDecls)
  = BNFC'Position -> ParamDecl -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
Nothing ParamDecl
paramDecl (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ParamDecl] -> Term -> Term
addParamDecls [ParamDecl]
paramDecls

-- | One index of a family, as declared in the sort: its binder (when the
-- sort names it, as in @(n : nat) → U@) and its type.
data SortIndex = SortIndex
  { SortIndex -> Maybe VarIdent
sortIndexVar  :: Maybe Rzk.VarIdent
  , SortIndex -> Term
sortIndexType :: Rzk.Term
  }

-- | The sort of a constructor: a point constructor returns the declared
-- type; a path constructor returns an identity type over it (spelled
-- @l =_{D …} r@), declaring an identification between the two endpoint
-- terms. Path β-rules are propositional (the generated @compute-@ lemmas),
-- following the HoTT-book treatment of higher inductive types.
data DataConSort
  = DataConPoint
  | DataConPath Rzk.Term Rzk.Term
    -- ^ the endpoints of the declared identification, as written

-- | A constructor, preprocessed at the surface level.
data DataConSurface = DataConSurface
  { DataConSurface -> VarIdent
dataConName       :: Rzk.VarIdent
  , DataConSurface -> [ParamDecl]
dataConFields     :: [Rzk.ParamDecl]
    -- ^ the field telescope, one entry per bound variable
  , DataConSurface -> [Term]
dataConFieldPats  :: [Rzk.Term]
    -- ^ the field patterns as terms, in the same order
  , DataConSurface -> [(Int, [Term])]
dataConRecursive  :: [(Int, [Rzk.Term])]
    -- ^ the directly recursive fields (their type is the declared type
    -- applied to its parameters and some index terms): 0-based position
    -- and the index terms; each contributes an induction hypothesis to
    -- the eliminator's method
  , DataConSurface -> [Term]
dataConRetIndices :: [Rzk.Term]
    -- ^ the index terms of the constructor's return type
  , DataConSurface -> Term
dataConType       :: Rzk.Term
    -- ^ the constructor's full surface type: params → fields → D params
  , DataConSurface -> Term
dataConProbe      :: Rzk.Term
    -- ^ the non-recursive fields → Unit, for the positivity and largeness
    -- checks (a directly recursive field mentions the type legitimately)
  , DataConSurface -> [Term]
dataConNonRec     :: [Rzk.Term]
    -- ^ the non-recursive field types, for the per-field error message
  , DataConSurface -> [VarIdentToken]
dataConLocalNames :: [Rzk.VarIdentToken]
    -- ^ every binder token of the constructor, for freshening
  , DataConSurface -> DataConSort
dataConSort       :: DataConSort
  }

surfacePatternVars :: Rzk.Pattern -> [Rzk.VarIdent]
surfacePatternVars :: Pattern -> [VarIdent]
surfacePatternVars = \case
  Rzk.PatternVar BNFC'Position
_ VarIdent
v        -> [VarIdent
v]
  Rzk.PatternPair BNFC'Position
_ Pattern
a Pattern
b     -> Pattern -> [VarIdent]
surfacePatternVars Pattern
a [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Semigroup a => a -> a -> a
<> Pattern -> [VarIdent]
surfacePatternVars Pattern
b
  Rzk.PatternTuple BNFC'Position
_ Pattern
a Pattern
b [Pattern]
cs -> (Pattern -> [VarIdent]) -> [Pattern] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern -> [VarIdent]
surfacePatternVars (Pattern
a Pattern -> [Pattern] -> [Pattern]
forall a. a -> [a] -> [a]
: Pattern
b Pattern -> [Pattern] -> [Pattern]
forall a. a -> [a] -> [a]
: [Pattern]
cs)
  Rzk.PatternUnit BNFC'Position
_         -> []

identTokenOf :: Rzk.VarIdent -> Rzk.VarIdentToken
identTokenOf :: VarIdent -> VarIdentToken
identTokenOf (Rzk.VarIdent BNFC'Position
_ VarIdentToken
tok) = VarIdentToken
tok

surfaceVar :: Rzk.VarIdent -> Rzk.Term
surfaceVar :: VarIdent -> Term
surfaceVar = BNFC'Position -> VarIdent -> Term
forall a. a -> VarIdent' a -> Term' a
Rzk.Var BNFC'Position
forall a. Maybe a
Nothing

-- | A λ over plain (untyped) variable patterns; only ever used in checking
-- position, where the domains come from the expected type.
surfaceLambda :: [Rzk.VarIdent] -> Rzk.Term -> Rzk.Term
surfaceLambda :: [VarIdent] -> Term -> Term
surfaceLambda [VarIdent]
vs = BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
forall a. Maybe a
Nothing
  [ BNFC'Position -> Pattern -> Param' BNFC'Position
forall a. a -> Pattern' a -> Param' a
Rzk.ParamPattern BNFC'Position
forall a. Maybe a
Nothing (BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
forall a. Maybe a
Nothing VarIdent
v) | VarIdent
v <- [VarIdent]
vs ]

-- | The wildcard binder, for a generated λ that ignores an argument.
underscoreIdent :: Rzk.VarIdent
underscoreIdent :: VarIdent
underscoreIdent = BNFC'Position -> VarIdentToken -> VarIdent
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent BNFC'Position
forall a. Maybe a
Nothing (Text -> VarIdentToken
Rzk.VarIdentToken Text
"_")

-- | Every variable-occurrence token in a surface term, collected
-- generically. Used for the endpoint well-formedness check of path
-- constructors, which is deliberately syntactic.
surfaceVarTokens :: Data a => a -> [Rzk.VarIdentToken]
surfaceVarTokens :: forall a. Data a => a -> [VarIdentToken]
surfaceVarTokens a
x = [[VarIdentToken]] -> [VarIdentToken]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [VarIdentToken]
-> (Term -> [VarIdentToken]) -> Maybe Term -> [VarIdentToken]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Term -> [VarIdentToken]
varTok (a -> Maybe Term
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
x)
  , [[VarIdentToken]] -> [VarIdentToken]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((forall a. Data a => a -> [VarIdentToken])
-> a -> [[VarIdentToken]]
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 -> [VarIdentToken]
forall a. Data a => a -> [VarIdentToken]
surfaceVarTokens a
x)
  ]
  where
    varTok :: Rzk.Term -> [Rzk.VarIdentToken]
    varTok :: Term -> [VarIdentToken]
varTok = \case
      Rzk.Var BNFC'Position
_ VarIdent
v -> [VarIdent -> VarIdentToken
identTokenOf VarIdent
v]
      Term
_           -> []

surfaceApps :: Rzk.Term -> [Rzk.Term] -> Rzk.Term
surfaceApps :: Term -> [Term] -> Term
surfaceApps Term
f []       = Term
f
surfaceApps Term
f (Term
x : [Term]
xs) = Term -> [Term] -> Term
surfaceApps (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App BNFC'Position
forall a. Maybe a
Nothing Term
f Term
x) [Term]
xs

surfaceAppSpine :: Rzk.Term -> (Rzk.Term, [Rzk.Term])
surfaceAppSpine :: Term -> (Term, [Term])
surfaceAppSpine = [Term] -> Term -> (Term, [Term])
forall {a}. [Term' a] -> Term' a -> (Term' a, [Term' a])
go []
  where
    go :: [Term' a] -> Term' a -> (Term' a, [Term' a])
go [Term' a]
acc (Rzk.App a
_ Term' a
f Term' a
x) = [Term' a] -> Term' a -> (Term' a, [Term' a])
go (Term' a
x Term' a -> [Term' a] -> [Term' a]
forall a. a -> [a] -> [a]
: [Term' a]
acc) Term' a
f
    go [Term' a]
acc Term' a
t               = (Term' a
t, [Term' a]
acc)

surfaceArrow :: Rzk.Term -> Rzk.Term -> Rzk.Term
surfaceArrow :: Term -> Term -> Term
surfaceArrow Term
a = BNFC'Position -> ParamDecl -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
Nothing (BNFC'Position -> Term -> ParamDecl
forall a. a -> Term' a -> ParamDecl' a
Rzk.ParamType BNFC'Position
forall a. Maybe a
Nothing Term
a)

-- | The domains and codomain of a surface Π-chain (domain types only; for
-- the shaped and modal parameter forms the carrier is what matters here).
surfacePiSpine :: Rzk.Term -> ([Rzk.Term], Rzk.Term)
surfacePiSpine :: Term -> ([Term], Term)
surfacePiSpine = [Term] -> Term -> ([Term], Term)
forall {a}. [Term' a] -> Term' a -> ([Term' a], Term' a)
go []
  where
    go :: [Term' a] -> Term' a -> ([Term' a], Term' a)
go [Term' a]
acc (Rzk.TypeFun a
_ ParamDecl' a
param Term' a
ret)       = [Term' a] -> Term' a -> ([Term' a], Term' a)
go (ParamDecl' a -> [Term' a]
forall {a}. ParamDecl' a -> [Term' a]
domainsOf ParamDecl' a
param [Term' a] -> [Term' a] -> [Term' a]
forall a. Semigroup a => a -> a -> a
<> [Term' a]
acc) Term' a
ret
    go [Term' a]
acc (Rzk.ASCII_TypeFun a
_ ParamDecl' a
param Term' a
ret) = [Term' a] -> Term' a -> ([Term' a], Term' a)
go (ParamDecl' a -> [Term' a]
forall {a}. ParamDecl' a -> [Term' a]
domainsOf ParamDecl' a
param [Term' a] -> [Term' a] -> [Term' a]
forall a. Semigroup a => a -> a -> a
<> [Term' a]
acc) Term' a
ret
    go [Term' a]
acc Term' a
t                               = ([Term' a] -> [Term' a]
forall a. [a] -> [a]
reverse [Term' a]
acc, Term' a
t)
    domainsOf :: ParamDecl' a -> [Term' a]
domainsOf = \case
      Rzk.ParamType a
_ Term' a
t                 -> [Term' a
t]
      Rzk.ParamTermType a
_ Term' a
_ Term' a
t           -> [Term' a
t]
      Rzk.ParamTermShape a
_ Term' a
_ Term' a
cube Term' a
_     -> [Term' a
cube]
      Rzk.ParamTermModalType a
_ Term' a
_ ModalColon' a
_ Term' a
t    -> [Term' a
t]
      Rzk.ParamTermModalShape a
_ Term' a
_ ModalColon' a
_ Term' a
c Term' a
_ -> [Term' a
c]

-- | Is the term the given name applied to exactly the given parameter
-- variables (in order, the uniformity requirement) and then exactly
-- @arity@ index terms? Returns those index terms. A syntactic check: this
-- is how constructor return types and directly recursive fields are
-- recognised.
dataAppliedIndices :: Rzk.VarIdent -> [Rzk.VarIdent] -> Int -> Rzk.Term -> Maybe [Rzk.Term]
dataAppliedIndices :: VarIdent -> [VarIdent] -> Int -> Term -> Maybe [Term]
dataAppliedIndices VarIdent
dataName [VarIdent]
paramVars Int
arity Term
t = case Term -> (Term, [Term])
surfaceAppSpine Term
t of
  (Rzk.Var BNFC'Position
_ VarIdent
h, [Term]
args)
    | VarIdent -> VarIdentToken
identTokenOf VarIdent
h VarIdentToken -> VarIdentToken -> Bool
forall a. Eq a => a -> a -> Bool
== VarIdent -> VarIdentToken
identTokenOf VarIdent
dataName
    , ([Term]
paramArgs, [Term]
indexArgs) <- Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt ([VarIdent] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VarIdent]
paramVars) [Term]
args
    , (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 [Maybe VarIdentToken] -> [Maybe VarIdentToken] -> Bool
forall a. Eq a => a -> a -> Bool
== (Term -> Maybe VarIdentToken) -> [Term] -> [Maybe VarIdentToken]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Maybe VarIdentToken
varTokenOf [Term]
paramArgs
    , [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
indexArgs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
arity
    -> [Term] -> Maybe [Term]
forall a. a -> Maybe a
Just [Term]
indexArgs
  (Term, [Term])
_ -> Maybe [Term]
forall a. Maybe a
Nothing
  where
    varTokenOf :: Term -> Maybe VarIdentToken
varTokenOf (Rzk.Var BNFC'Position
_ VarIdent
v) = VarIdentToken -> Maybe VarIdentToken
forall a. a -> Maybe a
Just (VarIdent -> VarIdentToken
identTokenOf VarIdent
v)
    varTokenOf Term
_             = Maybe VarIdentToken
forall a. Maybe a
Nothing

matchesDataApplied :: Rzk.VarIdent -> [Rzk.VarIdent] -> Int -> Rzk.Term -> Bool
matchesDataApplied :: VarIdent -> [VarIdent] -> Int -> Term -> Bool
matchesDataApplied VarIdent
dataName [VarIdent]
paramVars Int
arity =
  Bool -> ([Term] -> Bool) -> Maybe [Term] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> [Term] -> Bool
forall a b. a -> b -> a
const Bool
True) (Maybe [Term] -> Bool) -> (Term -> Maybe [Term]) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarIdent -> [VarIdent] -> Int -> Term -> Maybe [Term]
dataAppliedIndices VarIdent
dataName [VarIdent]
paramVars Int
arity

surfacePi :: Rzk.VarIdent -> Rzk.Term -> Rzk.Term -> Rzk.Term
surfacePi :: VarIdent -> Term -> Term -> Term
surfacePi VarIdent
v Term
ty = BNFC'Position -> ParamDecl -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
Nothing (BNFC'Position -> Term -> Term -> ParamDecl
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
forall a. Maybe a
Nothing (VarIdent -> Term
surfaceVar VarIdent
v) Term
ty)

prefixedIdent :: T.Text -> Rzk.VarIdent -> Rzk.VarIdent
prefixedIdent :: Text -> VarIdent -> VarIdent
prefixedIdent Text
p (Rzk.VarIdent BNFC'Position
pos (Rzk.VarIdentToken Text
t)) =
  BNFC'Position -> VarIdentToken -> VarIdent
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent BNFC'Position
pos (Text -> VarIdentToken
Rzk.VarIdentToken (Text
p Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t))

-- | Index into a list that is long enough by construction, panicking with a
-- label instead of the opaque @Prelude.!!@ message if that invariant is ever
-- broken. Used where an index is derived from the same data as the list (the
-- induction-hypothesis binders, a constructor's field patterns).
nthByConstruction :: String -> [a] -> Int -> a
nthByConstruction :: forall a. String -> [a] -> Int -> a
nthByConstruction String
what [a]
xs Int
i = case Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
i [a]
xs of
  a
x : [a]
_ -> a
x
  []    -> String -> a
forall a. String -> a
panicImpossible (String
what String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
": index " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" out of range")

-- | The 0-based positions of a constructor's directly recursive fields.
recPositionsOf :: DataConSurface -> [Int]
recPositionsOf :: DataConSurface -> [Int]
recPositionsOf = ((Int, [Term]) -> Int) -> [(Int, [Term])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [Term]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [Term])] -> [Int])
-> (DataConSurface -> [(Int, [Term])]) -> DataConSurface -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConSurface -> [(Int, [Term])]
dataConRecursive

-- * Eliminator construction

-- | Everything the pure construction of the eliminators closes over: the
-- declaration's name, its parameters and index telescope, the fresh binders of
-- the generated types (the motive, the scrutinee, the induction hypotheses,
-- the path-method names, and the binders of the inlined transport), the
-- preprocessed constructors, and — for each path constructor — the images of
-- its endpoints under the section being defined. Assembled by
-- "Rzk.TypeCheck.Decl" once the fresh names are allocated and the endpoints
-- validated.
data ElimSpec = ElimSpec
  { ElimSpec -> VarIdent
esName       :: Rzk.VarIdent
  , ElimSpec -> [VarIdent]
esParamVars  :: [Rzk.VarIdent]
  , ElimSpec -> [ParamDecl]
esParamDecls :: [Rzk.ParamDecl]
  , ElimSpec -> [VarIdent]
esIndexVars  :: [Rzk.VarIdent]
  , ElimSpec -> [ParamDecl]
esIndexDecls :: [Rzk.ParamDecl]
  , ElimSpec -> VarIdent
esMotiveV    :: Rzk.VarIdent
  , ElimSpec -> VarIdent
esScrutV     :: Rzk.VarIdent
  , ElimSpec -> [VarIdent]
esIhNames    :: [Rzk.VarIdent]
  , ElimSpec -> Maybe [VarIdent]
esMethodVars :: Maybe [Rzk.VarIdent]
  , ElimSpec -> VarIdent
esEndpointV  :: Rzk.VarIdent
  , ElimSpec -> VarIdent
esPathV      :: Rzk.VarIdent
  , ElimSpec -> VarIdent
esTransportV :: Rzk.VarIdent
  , ElimSpec -> [DataConSurface]
esConsData   :: [DataConSurface]
  , ElimSpec -> [Maybe ((Term, Term), (Term, Term))]
esPathData   :: [Maybe ((Rzk.Term, Rzk.Term), (Rzk.Term, Rzk.Term))]
  }

-- | The generated surface types of a declaration's eliminators and the path
-- computation rules, all as surface terms for the ordinary elaborator.
data ElimTerms = ElimTerms
  { ElimTerms -> Term
indTypeTerm  :: Rzk.Term
    -- ^ the type of @ind-D@ (the dependent eliminator)
  , ElimTerms -> Term
recTypeTerm  :: Rzk.Term
    -- ^ the type of @rec-D@ (the non-dependent eliminator)
  , ElimTerms -> [(VarIdent, Term)]
computeRules :: [(Rzk.VarIdent, Rzk.Term)]
    -- ^ one @compute-ind-@/@compute-rec-@ lemma per path constructor
  }

elimTerms :: ElimSpec -> ElimTerms
elimTerms :: ElimSpec -> ElimTerms
elimTerms ElimSpec
spec = ElimTerms
    { indTypeTerm :: Term
indTypeTerm  = Bool -> Term
elimTy Bool
True
    , recTypeTerm :: Term
recTypeTerm  = Bool -> Term
elimTy Bool
False
    , computeRules :: [(VarIdent, Term)]
computeRules = [(VarIdent, Term)]
computes
    }
  where
    ElimSpec
      { esName :: ElimSpec -> VarIdent
esName = VarIdent
name, esParamVars :: ElimSpec -> [VarIdent]
esParamVars = [VarIdent]
paramVars, esParamDecls :: ElimSpec -> [ParamDecl]
esParamDecls = [ParamDecl]
paramDecls
      , esIndexVars :: ElimSpec -> [VarIdent]
esIndexVars = [VarIdent]
indexVars, esIndexDecls :: ElimSpec -> [ParamDecl]
esIndexDecls = [ParamDecl]
indexDecls, esMotiveV :: ElimSpec -> VarIdent
esMotiveV = VarIdent
motiveV
      , esScrutV :: ElimSpec -> VarIdent
esScrutV = VarIdent
scrutV, esIhNames :: ElimSpec -> [VarIdent]
esIhNames = [VarIdent]
ihNames, esMethodVars :: ElimSpec -> Maybe [VarIdent]
esMethodVars = Maybe [VarIdent]
methodVars
      , esEndpointV :: ElimSpec -> VarIdent
esEndpointV = VarIdent
endpointV, esPathV :: ElimSpec -> VarIdent
esPathV = VarIdent
pathV, esTransportV :: ElimSpec -> VarIdent
esTransportV = VarIdent
transportV
      , esConsData :: ElimSpec -> [DataConSurface]
esConsData = [DataConSurface]
consData, esPathData :: ElimSpec -> [Maybe ((Term, Term), (Term, Term))]
esPathData = [Maybe ((Term, Term), (Term, Term))]
pathData } = ElimSpec
spec
    dApplied :: Term
dApplied = Term -> [Term] -> Term
surfaceApps (VarIdent -> Term
surfaceVar VarIdent
name) ((VarIdent -> Term) -> [VarIdent] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> Term
surfaceVar [VarIdent]
paramVars)
    dAppliedIx :: Term
dAppliedIx = Term -> [Term] -> Term
surfaceApps Term
dApplied ((VarIdent -> Term) -> [VarIdent] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> Term
surfaceVar [VarIdent]
indexVars)
    motive :: Term
motive = VarIdent -> Term
surfaceVar VarIdent
motiveV
    -- The motive abstracts over the indices (and, dependently, the
    -- scrutinee); a method's hypotheses and codomain instantiate it
    -- at the relevant index terms.
    motiveSort :: Bool -> Term
motiveSort Bool
dependent = [ParamDecl] -> Term -> Term
addParamDecls [ParamDecl]
indexDecls (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
      if Bool
dependent
        then Term -> Term -> Term
surfaceArrow Term
dAppliedIx (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Universe BNFC'Position
forall a. Maybe a
Nothing)
        else BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Universe BNFC'Position
forall a. Maybe a
Nothing
    -- The constructor applied to the parameters and its own fields
    -- (for a path constructor, this is the declared identification).
    conApplied :: DataConSurface -> Term
conApplied DataConSurface
con = Term -> [Term] -> Term
surfaceApps (VarIdent -> Term
surfaceVar (DataConSurface -> VarIdent
dataConName DataConSurface
con))
      ((VarIdent -> Term) -> [VarIdent] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> Term
surfaceVar [VarIdent]
paramVars [Term] -> [Term] -> [Term]
forall a. Semigroup a => a -> a -> a
<> DataConSurface -> [Term]
dataConFieldPats DataConSurface
con)
    -- @transport@ in the motive along a path @p : l = rEnd@, spelled
    -- through idJ (rzk has no primitive transport):
    -- @idJ (D …, l, \y' _ → C l → C y', \y' → y', rEnd, p) u@.
    transportAlong :: Term -> Term -> Term -> Term -> Term
transportAlong Term
l Term
rEnd Term
p Term
u =
      BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App BNFC'Position
forall a. Maybe a
Nothing
        (BNFC'Position
-> Term -> Term -> Term -> Term -> Term -> Term -> Term
forall a.
a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
Rzk.IdJ BNFC'Position
forall a. Maybe a
Nothing Term
dApplied Term
l
          ([VarIdent] -> Term -> Term
surfaceLambda [VarIdent
transportV, VarIdent
underscoreIdent]
            (Term -> Term -> Term
surfaceArrow (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App BNFC'Position
forall a. Maybe a
Nothing Term
motive Term
l)
              (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App BNFC'Position
forall a. Maybe a
Nothing Term
motive (VarIdent -> Term
surfaceVar VarIdent
transportV))))
          ([VarIdent] -> Term -> Term
surfaceLambda [VarIdent
transportV] (VarIdent -> Term
surfaceVar VarIdent
transportV))
          Term
rEnd Term
p)
        Term
u
    -- One method per constructor: its fields with an induction
    -- hypothesis interleaved after each recursive field (HoTT-book
    -- style). A point method then ends in the motive at the
    -- constructor's return indices (and, for @ind-D@, at the
    -- constructor applied to parameters and fields); a path method
    -- ends in an equation between the images of the endpoints, over
    -- the path for @ind-D@ (β on a path constructor stays
    -- propositional: the equation is the type of the generated
    -- @compute-@ lemma, not a rule the checker computes with).
    methodTy :: Bool
-> (DataConSurface, Maybe ((Term, Term), (Term, Term))) -> Term
methodTy Bool
dependent (DataConSurface
con, Maybe ((Term, Term), (Term, Term))
mpath) = Int -> [(Int, (ParamDecl, Term))] -> Term
wrapFields (Int
0 :: Int)
      ([Int] -> [(ParamDecl, Term)] -> [(Int, (ParamDecl, Term))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] ([ParamDecl] -> [Term] -> [(ParamDecl, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip (DataConSurface -> [ParamDecl]
dataConFields DataConSurface
con) (DataConSurface -> [Term]
dataConFieldPats DataConSurface
con)))
      where
        wrapFields :: Int -> [(Int, (ParamDecl, Term))] -> Term
wrapFields Int
_ [] = case Maybe ((Term, Term), (Term, Term))
mpath of
          Maybe ((Term, Term), (Term, Term))
Nothing -> Term -> [Term] -> Term
surfaceApps Term
motive ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$
            DataConSurface -> [Term]
dataConRetIndices DataConSurface
con [Term] -> [Term] -> [Term]
forall a. Semigroup a => a -> a -> a
<> [ DataConSurface -> Term
conApplied DataConSurface
con | Bool
dependent ]
          Just ((Term
l, Term
r), (Term
iL, Term
iR))
            | Bool
dependent -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeIdSimple BNFC'Position
forall a. Maybe a
Nothing
                (Term -> Term -> Term -> Term -> Term
transportAlong Term
l Term
r (DataConSurface -> Term
conApplied DataConSurface
con) Term
iL) Term
iR
            | Bool
otherwise -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeIdSimple BNFC'Position
forall a. Maybe a
Nothing Term
iL Term
iR
        wrapFields Int
nRec ((Int
j, (ParamDecl
fieldDecl, Term
fpat)) : [(Int, (ParamDecl, Term))]
more)
          | Just [Term]
fieldIxs <- Int -> [(Int, [Term])] -> Maybe [Term]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
j (DataConSurface -> [(Int, [Term])]
dataConRecursive DataConSurface
con) =
              BNFC'Position -> ParamDecl -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
Nothing ParamDecl
fieldDecl (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                VarIdent -> Term -> Term -> Term
surfacePi (String -> [VarIdent] -> Int -> VarIdent
forall a. String -> [a] -> Int -> a
nthByConstruction String
"induction hypotheses" [VarIdent]
ihNames Int
nRec)
                  (Term -> [Term] -> Term
surfaceApps Term
motive ([Term]
fieldIxs [Term] -> [Term] -> [Term]
forall a. Semigroup a => a -> a -> a
<> [ Term
fpat | Bool
dependent ]))
                  (Int -> [(Int, (ParamDecl, Term))] -> Term
wrapFields (Int
nRec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Int, (ParamDecl, Term))]
more)
          | Bool
otherwise =
              BNFC'Position -> ParamDecl -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
Nothing ParamDecl
fieldDecl (Int -> [(Int, (ParamDecl, Term))] -> Term
wrapFields Int
nRec [(Int, (ParamDecl, Term))]
more)
    elimTail :: Bool -> Term
elimTail Bool
dependent = [ParamDecl] -> Term -> Term
addParamDecls [ParamDecl]
indexDecls (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
      if Bool
dependent
        then VarIdent -> Term -> Term -> Term
surfacePi VarIdent
scrutV Term
dAppliedIx (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
          Term -> [Term] -> Term
surfaceApps Term
motive ((VarIdent -> Term) -> [VarIdent] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> Term
surfaceVar [VarIdent]
indexVars [Term] -> [Term] -> [Term]
forall a. Semigroup a => a -> a -> a
<> [VarIdent -> Term
surfaceVar VarIdent
scrutV])
        else Term -> Term -> Term
surfaceArrow Term
dAppliedIx (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
          Term -> [Term] -> Term
surfaceApps Term
motive ((VarIdent -> Term) -> [VarIdent] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> Term
surfaceVar [VarIdent]
indexVars)
    conWithPath :: [(DataConSurface, Maybe ((Term, Term), (Term, Term)))]
conWithPath = [DataConSurface]
-> [Maybe ((Term, Term), (Term, Term))]
-> [(DataConSurface, Maybe ((Term, Term), (Term, Term)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [DataConSurface]
consData [Maybe ((Term, Term), (Term, Term))]
pathData
    methodsPis :: Bool -> Term -> Term
methodsPis Bool
dependent Term
inner = case Maybe [VarIdent]
methodVars of
      Maybe [VarIdent]
Nothing -> ((DataConSurface, Maybe ((Term, Term), (Term, Term)))
 -> Term -> Term)
-> Term
-> [(DataConSurface, Maybe ((Term, Term), (Term, Term)))]
-> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Term -> Term -> Term
surfaceArrow (Term -> Term -> Term)
-> ((DataConSurface, Maybe ((Term, Term), (Term, Term))) -> Term)
-> (DataConSurface, Maybe ((Term, Term), (Term, Term)))
-> Term
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> (DataConSurface, Maybe ((Term, Term), (Term, Term))) -> Term
methodTy Bool
dependent) Term
inner [(DataConSurface, Maybe ((Term, Term), (Term, Term)))]
conWithPath
      Just [VarIdent]
ms -> ((VarIdent, (DataConSurface, Maybe ((Term, Term), (Term, Term))))
 -> Term -> Term)
-> Term
-> [(VarIdent,
     (DataConSurface, Maybe ((Term, Term), (Term, Term))))]
-> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
        (\(VarIdent
m, (DataConSurface, Maybe ((Term, Term), (Term, Term)))
cp) Term
rest -> VarIdent -> Term -> Term -> Term
surfacePi VarIdent
m (Bool
-> (DataConSurface, Maybe ((Term, Term), (Term, Term))) -> Term
methodTy Bool
dependent (DataConSurface, Maybe ((Term, Term), (Term, Term)))
cp) Term
rest)
        Term
inner ([VarIdent]
-> [(DataConSurface, Maybe ((Term, Term), (Term, Term)))]
-> [(VarIdent,
     (DataConSurface, Maybe ((Term, Term), (Term, Term))))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VarIdent]
ms [(DataConSurface, Maybe ((Term, Term), (Term, Term)))]
conWithPath)
    elimTy :: Bool -> Term
elimTy Bool
dependent = [ParamDecl] -> Term -> Term
addParamDecls [ParamDecl]
paramDecls (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
      VarIdent -> Term -> Term -> Term
surfacePi VarIdent
motiveV (Bool -> Term
motiveSort Bool
dependent) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
        Bool -> Term -> Term
methodsPis Bool
dependent (Bool -> Term
elimTail Bool
dependent)
    indName :: VarIdent
indName = Text -> VarIdent -> VarIdent
prefixedIdent Text
"ind-" VarIdent
name
    recName :: VarIdent
recName = Text -> VarIdent -> VarIdent
prefixedIdent Text
"rec-" VarIdent
name
    -- The propositional β-lemma per path constructor and eliminator:
    -- the section's action on the constructor's path (ap/apd, spelled
    -- through idJ) equals the path method at the fields, with the
    -- section applied to each recursive field as its hypothesis.
    -- Generated as opaque entries, like the eliminators themselves.
    sectionOf :: VarIdent -> Term
sectionOf VarIdent
elimIdent = Term -> [Term] -> Term
surfaceApps (VarIdent -> Term
surfaceVar VarIdent
elimIdent)
      ((VarIdent -> Term) -> [VarIdent] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> Term
surfaceVar [VarIdent]
paramVars [Term] -> [Term] -> [Term]
forall a. Semigroup a => a -> a -> a
<> [Term
motive]
        [Term] -> [Term] -> [Term]
forall a. Semigroup a => a -> a -> a
<> [Term] -> ([VarIdent] -> [Term]) -> Maybe [VarIdent] -> [Term]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((VarIdent -> Term) -> [VarIdent] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> Term
surfaceVar) Maybe [VarIdent]
methodVars)
    methodArgs :: Term -> DataConSurface -> [Term]
methodArgs Term
f DataConSurface
con = [[Term]] -> [Term]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ Term
fpat Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [ BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App BNFC'Position
forall a. Maybe a
Nothing Term
f Term
fpat | 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
con ]
      | (Int
j, Term
fpat) <- [Int] -> [Term] -> [(Int, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (DataConSurface -> [Term]
dataConFieldPats DataConSurface
con) ]
    computeTy :: Bool
-> VarIdent -> VarIdent -> DataConSurface -> Term -> Term -> Term
computeTy Bool
dependent VarIdent
elimIdent VarIdent
m DataConSurface
con Term
l Term
r =
      [ParamDecl] -> Term -> Term
addParamDecls [ParamDecl]
paramDecls (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
        VarIdent -> Term -> Term -> Term
surfacePi VarIdent
motiveV (Bool -> Term
motiveSort Bool
dependent) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
          Bool -> Term -> Term
methodsPis Bool
dependent (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
            [ParamDecl] -> Term -> Term
addParamDecls (DataConSurface -> [ParamDecl]
dataConFields DataConSurface
con) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
              let f :: Term
f = VarIdent -> Term
sectionOf VarIdent
elimIdent
                  fAt :: Term -> Term
fAt = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App BNFC'Position
forall a. Maybe a
Nothing Term
f
                  -- apd (dependent) or ap: the motive of the outer
                  -- idJ states what the section does to a path
                  motiveBody :: Term
motiveBody
                    | Bool
dependent = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeIdSimple BNFC'Position
forall a. Maybe a
Nothing
                        (Term -> Term -> Term -> Term -> Term
transportAlong Term
l (VarIdent -> Term
surfaceVar VarIdent
endpointV)
                          (VarIdent -> Term
surfaceVar VarIdent
pathV) (Term -> Term
fAt Term
l))
                        (Term -> Term
fAt (VarIdent -> Term
surfaceVar VarIdent
endpointV))
                    | Bool
otherwise = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeIdSimple BNFC'Position
forall a. Maybe a
Nothing
                        (Term -> Term
fAt Term
l) (Term -> Term
fAt (VarIdent -> Term
surfaceVar VarIdent
endpointV))
                  lhs :: Term
lhs = BNFC'Position
-> Term -> Term -> Term -> Term -> Term -> Term -> Term
forall a.
a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
Rzk.IdJ BNFC'Position
forall a. Maybe a
Nothing Term
dApplied Term
l
                    ([VarIdent] -> Term -> Term
surfaceLambda [VarIdent
endpointV, VarIdent
pathV] Term
motiveBody)
                    (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Refl BNFC'Position
forall a. Maybe a
Nothing) Term
r (DataConSurface -> Term
conApplied DataConSurface
con)
                  rhs :: Term
rhs = Term -> [Term] -> Term
surfaceApps (VarIdent -> Term
surfaceVar VarIdent
m) (Term -> DataConSurface -> [Term]
methodArgs Term
f DataConSurface
con)
               in BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeIdSimple BNFC'Position
forall a. Maybe a
Nothing Term
lhs Term
rhs
    computeNameFor :: Text -> DataConSurface -> VarIdent
computeNameFor Text
pfx DataConSurface
con =
      let Rzk.VarIdent BNFC'Position
pos (Rzk.VarIdentToken Text
d) = VarIdent
name
          Rzk.VarIdentToken Text
c = VarIdent -> VarIdentToken
identTokenOf (DataConSurface -> VarIdent
dataConName DataConSurface
con)
       in BNFC'Position -> VarIdentToken -> VarIdent
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent BNFC'Position
pos (Text -> VarIdentToken
Rzk.VarIdentToken (Text
pfx Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
d Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"-" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
c))
    computes :: [(VarIdent, Term)]
computes = case Maybe [VarIdent]
methodVars of
      Maybe [VarIdent]
Nothing -> []
      Just [VarIdent]
ms ->
        [ (VarIdent, Term)
entry
        | (VarIdent
m, (DataConSurface
con, Just ((Term
l, Term
r), (Term, Term)
_))) <- [VarIdent]
-> [(DataConSurface, Maybe ((Term, Term), (Term, Term)))]
-> [(VarIdent,
     (DataConSurface, Maybe ((Term, Term), (Term, Term))))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VarIdent]
ms [(DataConSurface, Maybe ((Term, Term), (Term, Term)))]
conWithPath
        , (VarIdent, Term)
entry <-
            [ ( Text -> DataConSurface -> VarIdent
computeNameFor Text
"compute-ind-" DataConSurface
con
              , Bool
-> VarIdent -> VarIdent -> DataConSurface -> Term -> Term -> Term
computeTy Bool
True VarIdent
indName VarIdent
m DataConSurface
con Term
l Term
r )
            , ( Text -> DataConSurface -> VarIdent
computeNameFor Text
"compute-rec-" DataConSurface
con
              , Bool
-> VarIdent -> VarIdent -> DataConSurface -> Term -> Term -> Term
computeTy Bool
False VarIdent
recName VarIdent
m DataConSurface
con Term
l Term
r ) ] ]