{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DerivingVia           #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE NumericUnderscores    #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}

{-# OPTIONS_GHC -fno-warn-name-shadowing
                -fno-warn-redundant-constraints
                -fno-warn-incomplete-record-updates
                -fno-warn-incomplete-uni-patterns
                -fno-warn-unused-top-binds
                #-}
-- TODO: the final -fno-warn here will be removed when we
-- merge the test harness (after PIR generators are merged into core)
-- and know what needs to be exported to make that make as much sense as possible.

module Plutus.Contract.Test.Coverage.Analysis.Interpreter (allNonFailLocations) where
import Control.Arrow hiding ((<+>))
import Data.Foldable
import Data.List hiding (insert)
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text qualified as Text
import GHC.Stack
import PlutusCore.Builtin
import PlutusCore.DeBruijn hiding (DeBruijn)
import PlutusCore.Default
import PlutusIR
import PlutusTx.Code
import PlutusTx.Coverage
import Text.PrettyPrint hiding (integer, (<>))

import Plutus.Contract.Test.Coverage.Analysis.Common
import Plutus.Contract.Test.Coverage.Analysis.DeBruijn
import Plutus.Contract.Test.Coverage.Analysis.Pretty
import Plutus.Contract.Test.Coverage.Analysis.Types

{- Note [Static analysis for non-fail-paths in plutus programs]
  In this module we implement at static analysis tool losely based
  on some form of abstract interpretation for finding program locatations
  (represented as PlutusTx coverage annotations) that are on the success
  paths of a plutus program. For example, in the following program:

    foo x y = if <Program Location 0> x == y then
                <Program Location 1> error "Fail"
              else
                <Program Location 2> ()

  Program locations 0 and 2 are on the success path (that doesn't result in error)
  and program location 1 is on the fail path. This information can be used (and is
  used in `Plutus.Contract.Test.Coverage.Analysis`) to improve coverage annotations
  to make the result of coverage checking significantly more readable.

  The way this works is we basically do abstract interpretation. That is to say we
  interpret PIR programs in a domain of "abstract programs" `Dom`. This domain track
  of possible program locations, unions of possible results,
  representations of datatypes and suspended computations, and a few escape hatches for
  embedding full PIR programs. Abstract interpretation then works by short-cutting recursion
  (by introducing DTop top values in the abstract domain) and aggressively expanding branches
  (case expressions) as unions.

  Most of the complexity in this module is related to the fact that we need to keep track
  of types in order to expand branches. Note that a number of functions have dependent
  types in comments above the type signature. THESE ARE IMPORTANT: not adhering to these
  specifications will most likely break the analysis and because they are not type-checked
  changes in this module have to be made with care.
-}

cost :: DDat -> Int
cost :: DDat -> Int
cost (DDat Bool
_ NamedTyDeBruijn
_ Kin
_ [NamedTyDeBruijn]
_ [DCon]
constrs)
    | [DCon] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DCon]
constrs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 = Int
0
    | Bool
otherwise = Int
1

idDTySubst :: TyCtx -> Subst DTyp
idDTySubst :: TyCtx -> Subst DTyp
idDTySubst TyCtx
ctx = TyCtx -> Index -> Subst DTyp
go TyCtx
ctx Index
0
  where
    go :: TyCtx -> Index -> Subst DTyp
go TyCtx
Nil Index
_ = Subst DTyp
forall a. SnocList a
Nil
    go (TyCtx
ctx :> TyCtxEntry
e) !Index
i =
      case TyCtxEntry
e of
        NamedTyDeBruijn
x ::: Kin
_                   -> TyCtx -> Index -> Subst DTyp
go TyCtx
ctx (Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
+ Index
1) Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar (NamedTyDeBruijn -> Index -> NamedTyDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedTyDeBruijn
x Index
i) []
        TyCtxDat (DDat Bool
_ NamedTyDeBruijn
x Kin
_ [NamedTyDeBruijn]
_ [DCon]
_) -> TyCtx -> Index -> Subst DTyp
go TyCtx
ctx (Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
+ Index
1) Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar (NamedTyDeBruijn -> Index -> NamedTyDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedTyDeBruijn
x Index
i) []
        TyCtxRecDat SnocList DDat
ds            -> TyCtx -> Index -> Subst DTyp
go TyCtx
ctx (Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
+ Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SnocList DDat -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length SnocList DDat
ds)) Subst DTyp -> Subst DTyp -> Subst DTyp
forall a. Semigroup a => a -> a -> a
<> SnocList DDat -> Index -> Subst DTyp
goDats SnocList DDat
ds Index
i

    goDats :: SnocList DDat -> Index -> Subst DTyp
goDats SnocList DDat
Nil Index
_                    = Subst DTyp
forall a. SnocList a
Nil
    goDats (SnocList DDat
ds :> DDat Bool
_ NamedTyDeBruijn
x Kin
_ [NamedTyDeBruijn]
_ [DCon]
_) Index
i = SnocList DDat -> Index -> Subst DTyp
goDats SnocList DDat
ds (Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
+ Index
1) Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar (NamedTyDeBruijn -> Index -> NamedTyDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedTyDeBruijn
x Index
i) []

-- wkDat :: {ctx : TyCtx, ctx' : TyCtx}
--       -> (wk : Subst ctx ctx')
--       -> DDat ctx
--       -> DDat ctx'
wkDat :: Weakening -> DDat -> DDat
wkDat :: Weakening -> DDat -> DDat
wkDat Weakening
w (DDat Bool
rec NamedTyDeBruijn
nm Kin
k [NamedTyDeBruijn]
pars [DCon]
cons) =
  Bool
-> NamedTyDeBruijn -> Kin -> [NamedTyDeBruijn] -> [DCon] -> DDat
DDat Bool
rec (Weakening -> NamedTyDeBruijn -> NamedTyDeBruijn
forall i. IsDbName i => Weakening -> i -> i
wkDbIndex Weakening
w NamedTyDeBruijn
nm) Kin
k [NamedTyDeBruijn]
pars [ [DTyp] -> DCon
DCon (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (Int -> Weakening -> Weakening
shiftsWeakening ([NamedTyDeBruijn] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedTyDeBruijn]
pars Int -> Int -> Int
forall a. Num a => a -> a -> a
+ if Bool
rec then Int
0 else Int
1) Weakening
w) (DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyp]
args)
                                   | DCon [DTyp]
args <- [DCon]
cons ]
  where
    shiftsWeakening :: Int -> Weakening -> Weakening
shiftsWeakening Int
n = ((Weakening -> Weakening)
 -> (Weakening -> Weakening) -> Weakening -> Weakening)
-> (Weakening -> Weakening)
-> [Weakening -> Weakening]
-> Weakening
-> Weakening
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Weakening -> Weakening)
-> (Weakening -> Weakening) -> Weakening -> Weakening
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Weakening -> Weakening
forall a. a -> a
id (Int -> (Weakening -> Weakening) -> [Weakening -> Weakening]
forall a. Int -> a -> [a]
replicate Int
n HasCallStack => Weakening -> Weakening
Weakening -> Weakening
shiftWeakening)

-- lookupDat :: (ctx : TyCtx)
--           -> Index
--           -> DDat ctx
lookupDat :: HasCallStack
          => TyCtx
          -> NamedTyDeBruijn
          -> DDat
lookupDat :: TyCtx -> NamedTyDeBruijn -> DDat
lookupDat TyCtx
ctx NamedTyDeBruijn
nm =
  case HasCallStack => TyCtx -> NamedTyDeBruijn -> Either Kin DDat
TyCtx -> NamedTyDeBruijn -> Either Kin DDat
lookupCtx TyCtx
ctx NamedTyDeBruijn
nm of
    Left{} -> Doc -> DDat
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> DDat) -> Doc -> DDat
forall a b. (a -> b) -> a -> b
$
          Doc
"lookupDat: " Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat [ Doc
"ctx =" Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx
                                 , Doc
"nm =" Doc -> Doc -> Doc
<+> NamedTyDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty NamedTyDeBruijn
nm]
    Right DDat
dat -> DDat
dat

lookupCtx :: HasCallStack => TyCtx -> NamedTyDeBruijn -> Either Kin DDat
lookupCtx :: TyCtx -> NamedTyDeBruijn -> Either Kin DDat
lookupCtx TyCtx
ctx0 NamedTyDeBruijn
nm = TyCtx -> Index -> Weakening -> Either Kin DDat
go TyCtx
ctx0 (NamedTyDeBruijn -> Index
forall n. IsDbName n => n -> Index
getDbIndex NamedTyDeBruijn
nm) Weakening
forall a. Monoid a => a
mempty
  where
    go :: TyCtx -> Index -> Weakening -> Either Kin DDat
    go :: TyCtx -> Index -> Weakening -> Either Kin DDat
go TyCtx
Nil Index
_ Weakening
_ = Doc -> Either Kin DDat
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Either Kin DDat) -> Doc -> Either Kin DDat
forall a b. (a -> b) -> a -> b
$
        Doc
"lookupCtx Nil:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat [ Doc
"ctx0 =" Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx0
                                  , Doc
"nm =" Doc -> Doc -> Doc
<+> NamedTyDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty NamedTyDeBruijn
nm ]

    go (TyCtx
ctx :> NamedTyDeBruijn
_ ::: Kin
k) Index
i Weakening
w
      | Index
i Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== Index
0    = Kin -> Either Kin DDat
forall a b. a -> Either a b
Left Kin
k
      | Bool
otherwise = TyCtx -> Index -> Weakening -> Either Kin DDat
go TyCtx
ctx (Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
- Index
1) (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1 Weakening -> Weakening -> Weakening
forall a. Semigroup a => a -> a -> a
<> Weakening
w)

    go (TyCtx
ctx :> TyCtxRecDat SnocList DDat
ds) Index
i Weakening
w
      | Index
i Index -> Index -> Bool
forall a. Ord a => a -> a -> Bool
< SnocList DDat -> Index
forall (f :: * -> *) i a.
(Functor f, Foldable f, Integral i) =>
f a -> i
len SnocList DDat
ds = DDat -> Either Kin DDat
forall a b. b -> Either a b
Right (DDat -> Either Kin DDat) -> DDat -> Either Kin DDat
forall a b. (a -> b) -> a -> b
$ Weakening -> DDat -> DDat
wkDat Weakening
w (SnocList DDat -> Index -> DDat
forall a. HasCallStack => Subst a -> Index -> a
lookupSubst SnocList DDat
ds Index
i)
      | Bool
otherwise  = TyCtx -> Index -> Weakening -> Either Kin DDat
go TyCtx
ctx (Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
- SnocList DDat -> Index
forall (f :: * -> *) i a.
(Functor f, Foldable f, Integral i) =>
f a -> i
len SnocList DDat
ds) (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy (SnocList DDat -> Index
forall (f :: * -> *) i a.
(Functor f, Foldable f, Integral i) =>
f a -> i
len SnocList DDat
ds) Weakening -> Weakening -> Weakening
forall a. Semigroup a => a -> a -> a
<> Weakening
w)

    go (TyCtx
ctx :> TyCtxDat DDat
d) Index
i Weakening
w
      | Index
i Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== Index
0    = DDat -> Either Kin DDat
forall a b. b -> Either a b
Right (DDat -> Either Kin DDat) -> DDat -> Either Kin DDat
forall a b. (a -> b) -> a -> b
$ Weakening -> DDat -> DDat
wkDat (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1 Weakening -> Weakening -> Weakening
forall a. Semigroup a => a -> a -> a
<> Weakening
w) DDat
d
      | Bool
otherwise = TyCtx -> Index -> Weakening -> Either Kin DDat
go TyCtx
ctx (Index
iIndex -> Index -> Index
forall a. Num a => a -> a -> a
-Index
1) (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1 Weakening -> Weakening -> Weakening
forall a. Semigroup a => a -> a -> a
<> Weakening
w)

dUnion :: Dom -> Dom -> Dom
dUnion :: Dom -> Dom -> Dom
dUnion Dom
DError Dom
d      = Dom
d
dUnion Dom
d Dom
DError      = Dom
d
dUnion (DUnion [Dom]
ds) Dom
d = [Dom] -> Dom
DUnion (Dom -> [Dom] -> [Dom]
insert (HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
d) [Dom]
ds)
dUnion Dom
l Dom
r           = [Dom] -> Dom
DUnion (Dom -> [Dom] -> [Dom]
insert (HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
r) [HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
l])

dUnions :: [Dom] -> Dom
dUnions :: [Dom] -> Dom
dUnions [] = Doc -> Dom
forall a. HasCallStack => Doc -> a
errorDoc Doc
"dUnions []"
dUnions [Dom]
ds = (Dom -> Dom -> Dom) -> [Dom] -> Dom
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Dom -> Dom -> Dom
dUnion [Dom]
ds

insert :: Dom -> [Dom] -> [Dom]
insert :: Dom -> [Dom] -> [Dom]
insert d :: Dom
d@DLam{} [Dom]
ds     = Dom
d Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
insert (DUnion [Dom]
ds') [Dom]
ds = (Dom -> [Dom] -> [Dom]) -> [Dom] -> [Dom] -> [Dom]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Dom -> [Dom] -> [Dom]
insert [Dom]
ds [Dom]
ds'
insert Dom
d []            = [Dom
d]
insert Dom
d (Dom
d':[Dom]
ds)       = case (Dom
d, Dom
d') of
  (DTop DTyp
ty Int
depth Set CoverageAnnotation
locs , DTop DTyp
ty' Int
depth' Set CoverageAnnotation
locs')
    | Bool -> Bool
not Bool
debug Bool -> Bool -> Bool
|| DTyp -> DTyp
normTy DTyp
ty DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy DTyp
ty' ->
      DTyp -> Int -> Set CoverageAnnotation -> Dom
DTop DTyp
ty (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
depth Int
depth') (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
locs') Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
    | Bool
otherwise -> Doc -> [Dom]
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> [Dom]) -> Doc -> [Dom]
forall a b. (a -> b) -> a -> b
$ Doc
"insert DTop type error:" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [Doc
"ty =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty, Doc
"ty' =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty']
  (DSusp Set CoverageAnnotation
locs Dom
inner , DSusp Set CoverageAnnotation
locs' Dom
inner')
    | Set CoverageAnnotation
locs Set CoverageAnnotation -> Set CoverageAnnotation -> Bool
forall a. Eq a => a -> a -> Bool
== Set CoverageAnnotation
locs' -> Set CoverageAnnotation -> Dom -> Dom
DSusp Set CoverageAnnotation
locs (Dom -> Dom -> Dom
dUnion Dom
inner Dom
inner') Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
    | [Dom
inner''] <- Dom -> [Dom] -> [Dom]
insert Dom
inner [Dom
inner'] -> Set CoverageAnnotation -> Dom -> Dom
DSusp (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
locs') Dom
inner'' Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
  (DTySusp NamedTyDeBruijn
nm Kin
k Set CoverageAnnotation
locs Dom
inner , DTySusp NamedTyDeBruijn
_ Kin
_ Set CoverageAnnotation
locs' Dom
inner')
    | Set CoverageAnnotation
locs Set CoverageAnnotation -> Set CoverageAnnotation -> Bool
forall a. Eq a => a -> a -> Bool
== Set CoverageAnnotation
locs' -> NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
nm Kin
k Set CoverageAnnotation
locs (Dom -> Dom -> Dom
dUnion Dom
inner Dom
inner') Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
    | [Dom
inner''] <- Dom -> [Dom] -> [Dom]
insert Dom
inner [Dom
inner'] -> NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
nm Kin
k (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
locs') Dom
inner'' Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
  (DIf DTyp
ty Set CoverageAnnotation
locs , DIf DTyp
ty' Set CoverageAnnotation
locs')
    | Bool -> Bool
not Bool
debug Bool -> Bool -> Bool
|| DTyp -> DTyp
normTy DTyp
ty DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy DTyp
ty' ->
      DTyp -> Set CoverageAnnotation -> Dom
DIf DTyp
ty (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
locs') Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
    | Bool
otherwise -> Doc -> [Dom]
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> [Dom]) -> Doc -> [Dom]
forall a b. (a -> b) -> a -> b
$ Doc
"insert DIf type error:" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [Doc
"ty =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty, Doc
"ty' =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty']
  (DTrace DTyp
ty Set CoverageAnnotation
locs , DTrace DTyp
ty' Set CoverageAnnotation
locs')
    | Bool -> Bool
not Bool
debug Bool -> Bool -> Bool
|| DTyp -> DTyp
normTy DTyp
ty DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy DTyp
ty' ->
      DTyp -> Set CoverageAnnotation -> Dom
DTrace DTyp
ty (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
locs') Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
    | Bool
otherwise -> Doc -> [Dom]
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> [Dom]) -> Doc -> [Dom]
forall a b. (a -> b) -> a -> b
$ Doc
"insert DTrace type error:" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [Doc
"ty =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty, Doc
"ty' =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty']
  (DLoc CoverageAnnotation
l , DLoc CoverageAnnotation
l')
    | CoverageAnnotation
l CoverageAnnotation -> CoverageAnnotation -> Bool
forall a. Eq a => a -> a -> Bool
== CoverageAnnotation
l' ->
      CoverageAnnotation -> Dom
DLoc CoverageAnnotation
l Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
  (DConstr DTyp
dat Int
idx SnocList Dom
argsD Set CoverageAnnotation
locs , DConstr DTyp
dat' Int
idx' SnocList Dom
argsD' Set CoverageAnnotation
locs')
    | Bool -> Bool
not Bool
debug Bool -> Bool -> Bool
|| (DTyp -> DTyp
normTy DTyp
dat DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy DTyp
dat' Bool -> Bool -> Bool
&& SnocList Dom -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length SnocList Dom
argsD Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== SnocList Dom -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length SnocList Dom
argsD')
    , Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
idx' ->
      DTyp -> Int -> SnocList Dom -> Set CoverageAnnotation -> Dom
DConstr DTyp
dat Int
idx ((Dom -> Dom -> Dom) -> SnocList Dom -> SnocList Dom -> SnocList Dom
forall a b c.
(a -> b -> c) -> SnocList a -> SnocList b -> SnocList c
zipWithSnoc Dom -> Dom -> Dom
dUnion SnocList Dom
argsD SnocList Dom
argsD') (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
locs') Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
    | Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
idx' -> Doc -> [Dom]
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> [Dom]) -> Doc -> [Dom]
forall a b. (a -> b) -> a -> b
$ Doc
"insert DConstr type error:"
      Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [Doc
"idx =" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
idx
               ,Doc
"dat =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
dat, Doc
"dat' =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
dat'
               ,Doc
"argsD =" Doc -> Doc -> Doc
<+> SnocList Dom -> Doc
forall a. Pretty a => a -> Doc
pretty SnocList Dom
argsD, Doc
"argsD' =" Doc -> Doc -> Doc
<+> SnocList Dom -> Doc
forall a. Pretty a => a -> Doc
pretty SnocList Dom
argsD']
  (DMatch DTyp
dat Set CoverageAnnotation
locs , DMatch DTyp
dat' Set CoverageAnnotation
locs')
    | DTyp
dat DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp
dat' ->
      DTyp -> Set CoverageAnnotation -> Dom
DMatch DTyp
dat (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
locs') Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
ds
  (Dom, Dom)
_ -> Dom
d' Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: Dom -> [Dom] -> [Dom]
insert Dom
d [Dom]
ds

aggro :: Int
aggro :: Int
aggro = Int
100

addLocations :: HasCallStack => Set CoverageAnnotation -> Dom -> Dom
addLocations :: Set CoverageAnnotation -> Dom -> Dom
addLocations Set CoverageAnnotation
locs Dom
d | Set CoverageAnnotation -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set CoverageAnnotation
locs = Dom
d
addLocations Set CoverageAnnotation
locs (DUnion [Dom]
ds) = [Dom] -> Dom
DUnion (HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations Set CoverageAnnotation
locs (Dom -> Dom) -> [Dom] -> [Dom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom]
ds)
addLocations Set CoverageAnnotation
locs (DWeaken Weakening
n Dom
d) = Weakening -> Dom -> Dom
DWeaken Weakening
n (HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations Set CoverageAnnotation
locs Dom
d)
addLocations Set CoverageAnnotation
_    Dom
DError = Dom
DError
addLocations Set CoverageAnnotation
_    (DLoc CoverageAnnotation
l) = CoverageAnnotation -> Dom
DLoc CoverageAnnotation
l
addLocations Set CoverageAnnotation
locs Dom
d = Dom
d { _locations :: Set CoverageAnnotation
_locations = Dom -> Set CoverageAnnotation
_locations Dom
d Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
locs }

allLocations :: HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
allLocations :: TyCtx -> Dom -> Set CoverageAnnotation
allLocations TyCtx
ctx Dom
d = case HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
d of
  DSusp Set CoverageAnnotation
locs Dom
d                      -> Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations TyCtx
ctx Dom
d
  DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
locs Dom
d                -> Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations (TyCtx
ctx TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn
x NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
k) Dom
d
  DLam NamedDeBruijn
_ DTyp
ty SnocList Dom
substD Subst DTyp
substT Trm
body Set CoverageAnnotation
locs -> Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> ((TyCtx -> Dom -> Set CoverageAnnotation)
-> (TyCtx, Dom) -> Set CoverageAnnotation
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations ((TyCtx, Dom) -> Set CoverageAnnotation)
-> ((TyCtx, Dom) -> (TyCtx, Dom))
-> (TyCtx, Dom)
-> Set CoverageAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> TyCtx) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (TyCtx
ctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<>)
                                               ((TyCtx, Dom) -> Set CoverageAnnotation)
-> (TyCtx, Dom) -> Set CoverageAnnotation
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
interp TyCtx
ctx (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop DTyp
ty Int
aggro Set CoverageAnnotation
forall a. Monoid a => a
mempty) Subst DTyp
substT Trm
body [])
  DUnion [Dom]
ds                         -> (Dom -> Set CoverageAnnotation) -> [Dom] -> Set CoverageAnnotation
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations TyCtx
ctx) [Dom]
ds
  DWeaken{}                         -> [Char] -> Set CoverageAnnotation
forall a. HasCallStack => [Char] -> a
error [Char]
"allLocations: DWeaken"
  DConstr DTyp
_ Int
_ SnocList Dom
args Set CoverageAnnotation
locs             -> Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> (Dom -> Set CoverageAnnotation) -> [Dom] -> Set CoverageAnnotation
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations TyCtx
ctx) (SnocList Dom -> [Dom]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList SnocList Dom
args)
  DLoc CoverageAnnotation
_                            -> Set CoverageAnnotation
forall a. Monoid a => a
mempty
  Dom
_                                 -> HasCallStack => Dom -> Set CoverageAnnotation
Dom -> Set CoverageAnnotation
topLevelLocations Dom
d

normalize_ :: HasCallStack => TyCtx -> Dom -> Dom
normalize_ :: TyCtx -> Dom -> Dom
normalize_ TyCtx
ctx Dom
d = Dom
nf
  where (TyCtx
Nil, Dom
nf) = HasCallStack => TyCtx -> Dom -> (TyCtx, Dom)
TyCtx -> Dom -> (TyCtx, Dom)
normalize TyCtx
ctx Dom
d

normalize :: HasCallStack => TyCtx -> Dom -> (TyCtx, Dom)
normalize :: TyCtx -> Dom -> (TyCtx, Dom)
normalize TyCtx
ctx Dom
d = let d' :: Dom
d' = HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
d in
  case Dom
d' of
    DSusp Set CoverageAnnotation
locs Dom
d                      -> (Dom -> Dom) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Set CoverageAnnotation -> Dom -> Dom
DSusp Set CoverageAnnotation
locs) (HasCallStack => TyCtx -> Dom -> (TyCtx, Dom)
TyCtx -> Dom -> (TyCtx, Dom)
normalize TyCtx
ctx Dom
d)
    DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
locs Dom
d                -> (TyCtx
forall a. SnocList a
Nil, NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
locs (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ HasCallStack => TyCtx -> Dom -> Dom
TyCtx -> Dom -> Dom
normalize_ (TyCtx
ctx TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn
x NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
k) Dom
d)
    DLam NamedDeBruijn
_ DTyp
ty SnocList Dom
substD Subst DTyp
substT Trm
body Set CoverageAnnotation
locs -> (TyCtx
ctx' TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx'', Set CoverageAnnotation -> Dom -> Dom
DSusp Set CoverageAnnotation
locs Dom
nf)
      where
        (TyCtx
ctx', Dom
d'') = HasCallStack =>
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
interp TyCtx
ctx (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop DTyp
ty Int
aggro Set CoverageAnnotation
forall a. Monoid a => a
mempty) Subst DTyp
substT Trm
body []
        (TyCtx
ctx'', Dom
nf) = HasCallStack => TyCtx -> Dom -> (TyCtx, Dom)
TyCtx -> Dom -> (TyCtx, Dom)
normalize (TyCtx
ctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx') Dom
d''
    DUnion [Dom]
ds ->
      case [(TyCtx, Dom)] -> ([TyCtx], [Dom])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(TyCtx, Dom)] -> ([TyCtx], [Dom]))
-> [(TyCtx, Dom)] -> ([TyCtx], [Dom])
forall a b. (a -> b) -> a -> b
$ HasCallStack => TyCtx -> Dom -> (TyCtx, Dom)
TyCtx -> Dom -> (TyCtx, Dom)
normalize TyCtx
ctx (Dom -> (TyCtx, Dom)) -> [Dom] -> [(TyCtx, Dom)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom]
ds of
        (TyCtx
ctx : [TyCtx]
ctxs, [Dom]
ds) | (TyCtx -> Bool) -> [TyCtx] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TyCtx
ctx TyCtx -> TyCtx -> Bool
forall a. Eq a => a -> a -> Bool
==) [TyCtx]
ctxs -> (TyCtx
ctx, [Dom] -> Dom
dUnions [Dom]
ds)
        ([TyCtx]
ctxs, [Dom]
ds)                           -> Doc -> (TyCtx, Dom)
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> (TyCtx, Dom)) -> Doc -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ Doc
"normalize DUnion:" Doc -> Doc -> Doc
<+> [(TyCtx, Dom)] -> Doc
forall a. Pretty a => a -> Doc
pretty ([TyCtx] -> [Dom] -> [(TyCtx, Dom)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyCtx]
ctxs [Dom]
ds)
    DConstr DTyp
dat Int
con SnocList Dom
args Set CoverageAnnotation
locs         ->
      (TyCtx
forall a. SnocList a
Nil, DTyp -> Int -> SnocList Dom -> Set CoverageAnnotation -> Dom
DConstr (DTyp -> DTyp
normTy DTyp
dat) Int
con (HasCallStack => TyCtx -> Dom -> Dom
TyCtx -> Dom -> Dom
normalize_ TyCtx
ctx (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnocList Dom
args) Set CoverageAnnotation
locs)
    DTop DTyp
ty Int
d Set CoverageAnnotation
locs -> (TyCtx
forall a. SnocList a
Nil, DTyp -> Int -> Set CoverageAnnotation -> Dom
DTop (DTyp -> DTyp
normTy DTyp
ty) Int
d Set CoverageAnnotation
locs)
    Dom
_ -> (TyCtx
forall a. SnocList a
Nil, Dom
d')

wkD :: HasCallStack => Weakening -> Dom -> Dom
wkD :: Weakening -> Dom -> Dom
wkD (Wk []) Dom
d        = Dom
d
wkD Weakening
w (DWeaken Weakening
wk Dom
d) = Weakening -> Dom -> Dom
DWeaken (Weakening
w Weakening -> Weakening -> Weakening
forall a. Semigroup a => a -> a -> a
<> Weakening
wk) Dom
d
wkD Weakening
w (DUnion [Dom]
ds)    = [Dom] -> Dom
DUnion (HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD Weakening
w (Dom -> Dom) -> [Dom] -> [Dom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom]
ds)
wkD Weakening
w Dom
d              = Weakening -> Dom -> Dom
DWeaken Weakening
w Dom
d

wkT :: HasCallStack => Weakening -> DTyp -> DTyp
wkT :: Weakening -> DTyp -> DTyp
wkT (Wk []) DTyp
a     = DTyp
a
wkT Weakening
w (DTWk Weakening
wk DTyp
a) = Weakening -> DTyp -> DTyp
DTWk (Weakening
w Weakening -> Weakening -> Weakening
forall a. Semigroup a => a -> a -> a
<> Weakening
wk) DTyp
a
wkT Weakening
w DTyp
a           = Weakening -> DTyp -> DTyp
DTWk Weakening
w DTyp
a

wkArg :: HasCallStack => Weakening -> DArg -> DArg
wkArg :: Weakening -> DArg -> DArg
wkArg Weakening
w (TyArg DTyp
t) = DTyp -> DArg
TyArg (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
t)
wkArg Weakening
w (DArg Dom
d)  = Dom -> DArg
DArg  (HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD Weakening
w Dom
d)

--lookupSubst :: {_ctx ctx}
--            -> Subst _ctx (f ctx)
--            -> Index
--            -> f ctx
lookupSubst :: HasCallStack => Subst a -> Index -> a
lookupSubst :: Subst a -> Index -> a
lookupSubst (Subst a
_   :> a
x) Index
0 = a
x
lookupSubst (Subst a
sub :> a
_) Index
i = Subst a -> Index -> a
forall a. HasCallStack => Subst a -> Index -> a
lookupSubst Subst a
sub (Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
- Index
1)
lookupSubst Subst a
Nil        Index
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"lookupSubst: out of bounds"

len :: (Functor f, Foldable f, Integral i) => f a -> i
len :: f a -> i
len = f i -> i
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (f i -> i) -> (f a -> f i) -> f a -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> i) -> f a -> f i
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (i -> a -> i
forall a b. a -> b -> a
const i
1)

ctxLen :: HasCallStack => TyCtx -> Index
ctxLen :: TyCtx -> Index
ctxLen = SnocList Index -> Index
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (SnocList Index -> Index)
-> (TyCtx -> SnocList Index) -> TyCtx -> Index
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtxEntry -> Index) -> TyCtx -> SnocList Index
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyCtxEntry -> Index
forall p. Integral p => TyCtxEntry -> p
entryLen
  where
    entryLen :: TyCtxEntry -> p
entryLen (NamedTyDeBruijn
_ ::: Kin
_)        = p
1
    entryLen TyCtxDat{}       = p
1
    entryLen (TyCtxRecDat SnocList DDat
ds) = SnocList DDat -> p
forall (f :: * -> *) i a.
(Functor f, Foldable f, Integral i) =>
f a -> i
len SnocList DDat
ds

pushWeaken :: HasCallStack => Dom -> Dom
pushWeaken :: Dom -> Dom
pushWeaken (DWeaken Weakening
w Dom
d) = case Dom
d of
  DTop DTyp
ty Int
dep Set CoverageAnnotation
locs                  -> DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
ty) Int
dep Set CoverageAnnotation
locs
  Dom
DError                            -> Dom
DError
  DSusp Set CoverageAnnotation
locs Dom
d                      -> Set CoverageAnnotation -> Dom -> Dom
DSusp Set CoverageAnnotation
locs (HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD Weakening
w Dom
d)
  DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
locs Dom
d                -> NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
locs (HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD (HasCallStack => Weakening -> Weakening
Weakening -> Weakening
shiftWeakening Weakening
w) Dom
d)
  DIf DTyp
ty Set CoverageAnnotation
locs                       -> DTyp -> Set CoverageAnnotation -> Dom
DIf (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
ty) Set CoverageAnnotation
locs
  DTrace DTyp
ty Set CoverageAnnotation
locs                    -> DTyp -> Set CoverageAnnotation -> Dom
DTrace (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
ty) Set CoverageAnnotation
locs
  DLoc{}                            -> Dom
d
  DLam NamedDeBruijn
x DTyp
ty SnocList Dom
substD Subst DTyp
substT Trm
body Set CoverageAnnotation
locs -> NamedDeBruijn
-> DTyp
-> SnocList Dom
-> Subst DTyp
-> Trm
-> Set CoverageAnnotation
-> Dom
DLam NamedDeBruijn
x (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
ty) (HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD Weakening
w (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnocList Dom
substD) (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w (DTyp -> DTyp) -> Subst DTyp -> Subst DTyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst DTyp
substT) Trm
body Set CoverageAnnotation
locs
  DConstr DTyp
dat Int
con SnocList Dom
args Set CoverageAnnotation
locs         -> DTyp -> Int -> SnocList Dom -> Set CoverageAnnotation -> Dom
DConstr (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
dat) Int
con (HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD Weakening
w (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnocList Dom
args) Set CoverageAnnotation
locs
  DMatch DTyp
dat Set CoverageAnnotation
locs                   -> DTyp -> Set CoverageAnnotation -> Dom
DMatch (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
dat) Set CoverageAnnotation
locs
  DUnion{}                          -> [Char] -> Dom
forall a. HasCallStack => [Char] -> a
error [Char]
"pushWeaken: DWeaken/DUnion"
  DWeaken{}                         -> [Char] -> Dom
forall a. HasCallStack => [Char] -> a
error [Char]
"pushWeaken: DWeaken/DWeaken"
pushWeaken (DUnion [Dom]
ds) = [Dom] -> Dom
DUnion (HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken (Dom -> Dom) -> [Dom] -> [Dom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom]
ds)
pushWeaken Dom
d = Dom
d

wkDbIndex :: IsDbName i => Weakening -> i -> i
wkDbIndex :: Weakening -> i -> i
wkDbIndex Weakening
w i
x = i -> Index -> i
forall n. IsDbName n => n -> Index -> n
setDbIndex i
x (HasCallStack => Weakening -> Index -> Index
Weakening -> Index -> Index
wkIndex Weakening
w (i -> Index
forall n. IsDbName n => n -> Index
getDbIndex i
x))

pushWeakenTy :: HasCallStack => DTyp -> DTyp
pushWeakenTy :: DTyp -> DTyp
pushWeakenTy (DTWk Weakening
w DTyp
a) = case DTyp
a of
  DTVar NamedTyDeBruijn
x [DTyp]
ts     -> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar (Weakening -> NamedTyDeBruijn -> NamedTyDeBruijn
forall i. IsDbName i => Weakening -> i -> i
wkDbIndex Weakening
w NamedTyDeBruijn
x) (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w (DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyp]
ts)
  DTFun DTyp
s DTyp
t      -> DTyp -> DTyp -> DTyp
DTFun (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
s) (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
w DTyp
t)
  DTLam NamedTyDeBruijn
x Kin
k DTyp
t    -> NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTLam NamedTyDeBruijn
x Kin
k (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Weakening -> Weakening
Weakening -> Weakening
shiftWeakening Weakening
w) DTyp
t)
  DTForall NamedTyDeBruijn
x Kin
k DTyp
t -> NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTForall NamedTyDeBruijn
x Kin
k (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Weakening -> Weakening
Weakening -> Weakening
shiftWeakening Weakening
w) DTyp
t)
  DTyBuiltin Kin
k   -> Kin -> DTyp
DTyBuiltin Kin
k
  DTWk Weakening
_ DTyp
_       -> [Char] -> DTyp
forall a. HasCallStack => [Char] -> a
error [Char]
"pushWeakenTy: DTWk"
pushWeakenTy DTyp
a = DTyp
a

normTy :: DTyp -> DTyp
normTy :: DTyp -> DTyp
normTy DTyp
a = case HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy DTyp
a of
  DTVar NamedTyDeBruijn
x [DTyp]
ts     -> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
x (DTyp -> DTyp
normTy (DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyp]
ts)
  DTFun DTyp
s DTyp
t      -> DTyp -> DTyp -> DTyp
DTFun (DTyp -> DTyp
normTy DTyp
s) (DTyp -> DTyp
normTy DTyp
t)
  DTLam NamedTyDeBruijn
x Kin
k DTyp
t    -> NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTLam NamedTyDeBruijn
x Kin
k (DTyp -> DTyp
normTy DTyp
t)
  DTForall NamedTyDeBruijn
x Kin
k DTyp
t -> NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTForall NamedTyDeBruijn
x Kin
k (DTyp -> DTyp
normTy DTyp
t)
  DTyBuiltin Kin
k   -> Kin -> DTyp
DTyBuiltin Kin
k
  DTWk{}         -> [Char] -> DTyp
forall a. HasCallStack => [Char] -> a
error [Char]
"normTy: DTWk"

tyCheck :: TyCtx -> DTyp -> Dom -> Bool
tyCheck :: TyCtx -> DTyp -> Dom -> Bool
tyCheck TyCtx
ctx DTyp
a Dom
d = case HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
d of
  DTop DTyp
b Int
_ Set CoverageAnnotation
_ -> DTyp -> DTyp
normTy DTyp
a DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy DTyp
b
  DSusp Set CoverageAnnotation
_ Dom
d  ->
    case HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy DTyp
a of
      DTFun DTyp
_ DTyp
b -> TyCtx -> DTyp -> Dom -> Bool
tyCheck TyCtx
ctx DTyp
b Dom
d
      DTyp
_         -> Bool
False
  DError{}   -> Bool
True
  DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
_ Dom
d ->
    case HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy DTyp
a of
      DTForall NamedTyDeBruijn
y Kin
k' DTyp
b | NamedTyDeBruijn
x NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
forall a. Eq a => a -> a -> Bool
== NamedTyDeBruijn
y, Kin
k Kin -> Kin -> Bool
forall a. Eq a => a -> a -> Bool
== Kin
k' -> TyCtx -> DTyp -> Dom -> Bool
tyCheck (TyCtx
ctx TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn
x NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
k) DTyp
b Dom
d
      DTyp
_                                 -> Bool
False
  DLam NamedDeBruijn
_ DTyp
ty SnocList Dom
_ Subst DTyp
_ Trm
_ Set CoverageAnnotation
_ ->
    case HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy DTyp
a of
      DTFun DTyp
argTy DTyp
_ -> DTyp -> DTyp
normTy DTyp
ty DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy DTyp
argTy
      DTyp
_             -> Bool
False
  DConstr (DTyp -> DTyp
normTy -> ddat :: DTyp
ddat@(DTVar NamedTyDeBruijn
dat [DTyp]
pars)) Int
i SnocList Dom
args Set CoverageAnnotation
_
    | [DTyp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyp]
pars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [NamedTyDeBruijn] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedTyDeBruijn]
xs       -> Bool
False
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [DCon] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DCon]
cs                 -> Bool
False
    | SnocList Dom -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length SnocList Dom
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [DTyp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyp]
conArgTys -> Bool
False
    | Bool
otherwise                      ->
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (DTyp -> DTyp
normTy DTyp
a DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy ((DTyp -> DTyp -> DTyp) -> DTyp -> [DTyp] -> DTyp
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr DTyp -> DTyp -> DTyp
DTFun DTyp
ddat [DTyp]
conArgTys2))
          Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: (DTyp -> Dom -> Bool) -> [DTyp] -> [Dom] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TyCtx -> DTyp -> Dom -> Bool
tyCheck TyCtx
ctx) [DTyp]
conArgTys1 (SnocList Dom -> [Dom]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList SnocList Dom
args)
    where
      -- DDat ctx, so cs : [DCon (ctx :> (if rec then Nil else dat ::: _) :> xs ::: _)]
      DDat Bool
rec NamedTyDeBruijn
_ Kin
_ [NamedTyDeBruijn]
xs [DCon]
cs       = HasCallStack => TyCtx -> NamedTyDeBruijn -> DDat
TyCtx -> NamedTyDeBruijn -> DDat
lookupDat TyCtx
ctx NamedTyDeBruijn
dat
      DCon [DTyp]
conArgTys           = [DCon]
cs [DCon] -> Int -> DCon
forall a. [a] -> Int -> a
!! Int
i
      ([DTyp]
conArgTys1, [DTyp]
conArgTys2) = Int -> [DTyp] -> ([DTyp], [DTyp])
forall a. Int -> [a] -> ([a], [a])
splitAt (SnocList Dom -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length SnocList Dom
args) ([DTyp] -> ([DTyp], [DTyp])) -> [DTyp] -> ([DTyp], [DTyp])
forall a b. (a -> b) -> a -> b
$ (DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall a b. (a -> b) -> [a] -> [b]
map DTyp -> DTyp
inst [DTyp]
conArgTys
      inst :: DTyp -> DTyp
inst DTyp
ty | Bool
rec       = DTyp -> [DTyp] -> DTyp
tyInsts DTyp
ty [DTyp]
pars
              -- inst : DTyp (ctx :> dat ::: _ :> xs ::: _) -> DTyp ctx
              | Bool
otherwise = DTyp -> [DTyp] -> DTyp
tyInsts DTyp
ty (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
dat [] DTyp -> [DTyp] -> [DTyp]
forall a. a -> [a] -> [a]
: [DTyp]
pars)

  DConstr{}  -> Bool
False

  DMatch (DTyp -> DTyp
normTy -> (DTVar NamedTyDeBruijn
dat [DTyp]
pars)) Set CoverageAnnotation
_ -> case DTyp -> DTyp
normTy DTyp
a of
    DTFun (DTVar NamedTyDeBruijn
dat' [DTyp]
pars') (DTForall NamedTyDeBruijn
r Kin
Star DTyp
body)
      | NamedTyDeBruijn
dat' NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
forall a. Eq a => a -> a -> Bool
/= NamedTyDeBruijn
dat                         -> Bool
False
      | (DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall a b. (a -> b) -> [a] -> [b]
map DTyp -> DTyp
normTy [DTyp]
pars [DTyp] -> [DTyp] -> Bool
forall a. Eq a => a -> a -> Bool
/= (DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall a b. (a -> b) -> [a] -> [b]
map DTyp -> DTyp
normTy [DTyp]
pars' -> Bool
False
      | [DTyp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyp]
pars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [NamedTyDeBruijn] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedTyDeBruijn]
xs            -> Bool
False
      | Bool
otherwise                           ->
        [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (DTyp -> DTyp
normTy DTyp
bodyRes DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
r []) Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: [ DTyp -> DTyp
normTy DTyp
b DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy ((DTyp -> DTyp -> DTyp) -> DTyp -> [DTyp] -> DTyp
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr DTyp -> DTyp -> DTyp
DTFun (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
r []) ((DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall a b. (a -> b) -> [a] -> [b]
map (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) (DTyp -> DTyp) -> (DTyp -> DTyp) -> DTyp -> DTyp
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  DTyp -> DTyp
inst) [DTyp]
conArgs))
                                               | (DTyp
b, DCon [DTyp]
conArgs) <- [DTyp] -> [DCon] -> [(DTyp, DCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip [DTyp]
bodyArgs [DCon]
cs ]
                                    where ([DTyp]
bodyArgs, DTyp
bodyRes) = DTyp -> ([DTyp], DTyp)
view DTyp
body
    DTyp
_ -> Bool
False
    where DDat Bool
rec NamedTyDeBruijn
_ Kin
_ [NamedTyDeBruijn]
xs [DCon]
cs = HasCallStack => TyCtx -> NamedTyDeBruijn -> DDat
TyCtx -> NamedTyDeBruijn -> DDat
lookupDat TyCtx
ctx NamedTyDeBruijn
dat
          inst :: DTyp -> DTyp
inst DTyp
ty | Bool
rec       = DTyp -> [DTyp] -> DTyp
tyInsts DTyp
ty [DTyp]
pars
                  | Bool
otherwise = DTyp -> [DTyp] -> DTyp
tyInsts DTyp
ty (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
dat [] DTyp -> [DTyp] -> [DTyp]
forall a. a -> [a] -> [a]
: [DTyp]
pars)
          view :: DTyp -> ([DTyp], DTyp)
view (DTFun DTyp
a DTyp
b) = ([DTyp] -> [DTyp]) -> ([DTyp], DTyp) -> ([DTyp], DTyp)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (DTyp
aDTyp -> [DTyp] -> [DTyp]
forall a. a -> [a] -> [a]
:) (DTyp -> ([DTyp], DTyp)
view DTyp
b)
          view DTyp
a           = ([], DTyp
a)

  DMatch{} -> Bool
False

  DIf DTyp
ty Set CoverageAnnotation
_    -> DTyp -> DTyp
normTy (DTyp -> DTyp -> DTyp
DTFun (Kin -> DTyp
DTyBuiltin Kin
Star) (DTyp -> DTyp -> DTyp
DTFun DTyp
ty (DTyp -> DTyp -> DTyp
DTFun DTyp
ty DTyp
ty))) DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy DTyp
a
  DTrace DTyp
ty Set CoverageAnnotation
_ -> DTyp -> DTyp
normTy (DTyp -> DTyp -> DTyp
DTFun (Kin -> DTyp
DTyBuiltin Kin
Star) (DTyp -> DTyp -> DTyp
DTFun DTyp
ty DTyp
ty)) DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== DTyp -> DTyp
normTy DTyp
a
  DUnion [Dom]
ds   -> (Dom -> Bool) -> [Dom] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TyCtx -> DTyp -> Dom -> Bool
tyCheck TyCtx
ctx DTyp
a) [Dom]
ds
  DLoc{}      -> DTyp -> DTyp
normTy DTyp
a DTyp -> DTyp -> Bool
forall a. Eq a => a -> a -> Bool
== Kin -> DTyp
DTyBuiltin Kin
Star
  DWeaken{}   -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"tyCheck: DWeaken"

-- dTop :: {ctx :: TyCtx} -> DTyp ctx -> Int -> Set CoverageAnnotation -> Dom ctx
dTop :: DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop :: DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop (HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy -> DTForall NamedTyDeBruijn
x Kin
k DTyp
dt) Int
i Set CoverageAnnotation
locs = NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
locs (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop DTyp
dt Int
i Set CoverageAnnotation
forall a. Monoid a => a
mempty
dTop DTyp
ty Int
i Set CoverageAnnotation
locs                                = DTyp -> Int -> Set CoverageAnnotation -> Dom
DTop DTyp
ty Int
i Set CoverageAnnotation
locs

-- tyInsts :: DTyp (ctx :> ctx')
--         -> { xs : [DTyp ctx] | length xs = length ctx', xs !! i : toList ctx' !! i }
--         -> DTyp ctx
tyInsts :: DTyp -> [DTyp] -> DTyp
tyInsts :: DTyp -> [DTyp] -> DTyp
tyInsts DTyp
a []     = DTyp
a
tyInsts DTyp
a (DTyp
x:[DTyp]
xs) = DTyp -> [DTyp] -> DTyp
tyInsts (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst (Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Index) -> Int -> Index
forall a b. (a -> b) -> a -> b
$ [DTyp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyp]
xs) DTyp
a DTyp
x) [DTyp]
xs

domApp :: HasCallStack
       => TyCtx   -- (ctx : TyCtx)
       -> Dom     -- Dom ctx
       -> Dom     -- Dom ctx
       -> Dom     -- Dom ctx
domApp :: TyCtx -> Dom -> Dom -> Dom
domApp TyCtx
_ Dom
DError Dom
_ = Dom
DError -- DONT MOVE! The order of this case shortcuts unions in the argument
domApp TyCtx
ctx Dom
d (HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken -> DUnion [Dom]
ds) = [Dom] -> Dom
dUnions (HasCallStack => TyCtx -> Dom -> Dom -> Dom
TyCtx -> Dom -> Dom -> Dom
domApp TyCtx
ctx Dom
d (Dom -> Dom) -> [Dom] -> [Dom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom]
ds)
domApp TyCtx
_ Dom
_ Dom
DError = Dom
DError
domApp TyCtx
ctx Dom
d Dom
arg = HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations (HasCallStack => Dom -> Set CoverageAnnotation
Dom -> Set CoverageAnnotation
topLevelLocations Dom
arg) (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ case Dom
d of
  DTop (HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy -> DTFun DTyp
argT DTyp
b) Int
dep Set CoverageAnnotation
locs
    | Bool -> Bool
not Bool
debug Bool -> Bool -> Bool
|| TyCtx -> DTyp -> Dom -> Bool
tyCheck TyCtx
ctx DTyp
argT Dom
arg ->
      DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop DTyp
b Int
dep (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations TyCtx
ctx Dom
arg)
    | Bool
otherwise -> Doc -> Dom
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Dom) -> Doc -> Dom
forall a b. (a -> b) -> a -> b
$ Doc
"domApp - type error - DTop:"
                                Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [Doc
"d =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
d
                                         ,Doc
"arg =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
arg]

  Dom
DError -> Dom
DError

  DSusp Set CoverageAnnotation
locs Dom
d -> HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations TyCtx
ctx Dom
arg) Dom
d

  DIf DTyp
ty Set CoverageAnnotation
locs -> case Dom
arg of
    DTop (HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy -> DTyBuiltin Type{}) Int
_ Set CoverageAnnotation
_ ->
      let x :: NamedDeBruijn
x = Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
"x" Index
0
          y :: NamedDeBruijn
y = Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
"y" Index
0
          a :: Type NamedTyDeBruijn uni ()
a = () -> NamedTyDeBruijn -> Type NamedTyDeBruijn uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () (NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
"a" Index
0))
          substT' :: Subst DTyp
substT' = Subst DTyp
forall a. SnocList a
Nil Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> DTyp
ty
          -- Here _ctx = a{0}
          -- and under the LamAbs it's (in the mixed ctx format) _ctx = a{0} :> y : a{0}
          dTrue :: Dom
dTrue  = NamedDeBruijn
-> DTyp
-> SnocList Dom
-> Subst DTyp
-> Trm
-> Set CoverageAnnotation
-> Dom
DLam NamedDeBruijn
x DTyp
ty SnocList Dom
forall a. Monoid a => a
mempty Subst DTyp
substT' (()
-> NamedDeBruijn
-> Type NamedTyDeBruijn DefaultUni ()
-> Trm
-> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () NamedDeBruijn
y Type NamedTyDeBruijn DefaultUni ()
forall (uni :: * -> *). Type NamedTyDeBruijn uni ()
a (() -> NamedDeBruijn -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () (NamedDeBruijn -> Index -> NamedDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedDeBruijn
x Index
1))) Set CoverageAnnotation
locs
          dFalse :: Dom
dFalse = NamedDeBruijn
-> DTyp
-> SnocList Dom
-> Subst DTyp
-> Trm
-> Set CoverageAnnotation
-> Dom
DLam NamedDeBruijn
x DTyp
ty SnocList Dom
forall a. Monoid a => a
mempty Subst DTyp
substT' (()
-> NamedDeBruijn
-> Type NamedTyDeBruijn DefaultUni ()
-> Trm
-> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () NamedDeBruijn
y Type NamedTyDeBruijn DefaultUni ()
forall (uni :: * -> *). Type NamedTyDeBruijn uni ()
a (() -> NamedDeBruijn -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () NamedDeBruijn
y)) Set CoverageAnnotation
locs
      in Dom -> Dom -> Dom
dUnion Dom
dTrue Dom
dFalse
    Dom
_ -> Doc -> Dom
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Dom) -> Doc -> Dom
forall a b. (a -> b) -> a -> b
$ Doc
"domApp: DIf" Doc -> Doc -> Doc
<?> (Doc
"arg =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
arg)

  DTrace DTyp
ty Set CoverageAnnotation
locs -> case HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
arg of
    DLoc CoverageAnnotation
l              ->
      let x :: NamedDeBruijn
x = Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
"x" Index
0
      in NamedDeBruijn
-> DTyp
-> SnocList Dom
-> Subst DTyp
-> Trm
-> Set CoverageAnnotation
-> Dom
DLam NamedDeBruijn
x DTyp
ty SnocList Dom
forall a. Monoid a => a
mempty Subst DTyp
forall a. Monoid a => a
mempty (() -> NamedDeBruijn -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () NamedDeBruijn
x) (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> CoverageAnnotation -> Set CoverageAnnotation
forall a. a -> Set a
Set.singleton CoverageAnnotation
l)
    DTop (HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy -> DTyBuiltin Type{}) Int
_ Set CoverageAnnotation
_ ->
      let x :: NamedDeBruijn
x = Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
"x" Index
0
      in NamedDeBruijn
-> DTyp
-> SnocList Dom
-> Subst DTyp
-> Trm
-> Set CoverageAnnotation
-> Dom
DLam NamedDeBruijn
x DTyp
ty SnocList Dom
forall a. Monoid a => a
mempty Subst DTyp
forall a. Monoid a => a
mempty (() -> NamedDeBruijn -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () NamedDeBruijn
x) Set CoverageAnnotation
locs
    Dom
_                  -> Doc -> Dom
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Dom) -> Doc -> Dom
forall a b. (a -> b) -> a -> b
$ Doc
"domApp: DTrace" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [ Doc
"arg =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
arg ]

  DLam NamedDeBruijn
_ DTyp
ty SnocList Dom
substD Subst DTyp
substT Trm
body Set CoverageAnnotation
locs
    | Bool -> Bool
not Bool
debug Bool -> Bool -> Bool
|| TyCtx -> DTyp -> Dom -> Bool
tyCheck TyCtx
ctx DTyp
ty Dom
arg ->
      HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations Set CoverageAnnotation
locs (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ TyCtx
ctx (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
arg) Subst DTyp
substT Trm
body []
    | Bool
otherwise -> Doc -> Dom
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Dom) -> Doc -> Dom
forall a b. (a -> b) -> a -> b
$ Doc
"domApp - type error - DLam:"
                                Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [Doc
"ty =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty (DTyp -> DTyp
normTy DTyp
ty)
                                         ,Doc
"body =" Doc -> Doc -> Doc
<+> Trm -> Doc
forall a. Pretty a => a -> Doc
pretty Trm
body
                                         ,Doc
"arg =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
arg]

  DConstr DTyp
dat Int
con SnocList Dom
args Set CoverageAnnotation
locs -> DTyp -> Int -> SnocList Dom -> Set CoverageAnnotation -> Dom
DConstr DTyp
dat Int
con (SnocList Dom
args SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
arg) Set CoverageAnnotation
locs

  match :: Dom
match@(DMatch (HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy -> DTVar NamedTyDeBruijn
d [DTyp]
pars) Set CoverageAnnotation
locs) -> case HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
arg of

    DTop (HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy -> DTyp
ty) Int
depth Set CoverageAnnotation
alocs
      | DTVar{} <- DTyp
ty
      , dat :: DDat
dat@(DDat Bool
False NamedTyDeBruijn
nm Kin
_ [NamedTyDeBruijn]
_ [DCon]
constrs) <- HasCallStack => TyCtx -> NamedTyDeBruijn -> DDat
TyCtx -> NamedTyDeBruijn -> DDat
lookupDat TyCtx
ctx NamedTyDeBruijn
d
      , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [DCon] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DCon]
constrs
      , Int
depth Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= DDat -> Int
cost DDat
dat ->
         -- We are matching on datatype `C` and the argument is `T[C p0 ... pn]`
         Verbosity -> Doc -> Dom -> Dom
forall a. Verbosity -> Doc -> a -> a
traceDoc Verbosity
Med (Doc
"domApp - lookupDat" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [Doc
"ctx =" Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx, Doc
"d =" Doc -> Doc -> Doc
<+> NamedTyDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty NamedTyDeBruijn
d]) (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$
         -- Here we are working in `ctx`
         let topArgs :: DCon -> SnocList Dom
topArgs (DCon [DTyp]
args) = (SnocList Dom -> Dom -> SnocList Dom)
-> SnocList Dom -> [Dom] -> SnocList Dom
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
(:>) SnocList Dom
forall a. SnocList a
Nil
              [ DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop (DTyp -> [DTyp] -> DTyp
tyInsts DTyp
a (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
nm [] DTyp -> [DTyp] -> [DTyp]
forall a. a -> [a] -> [a]
: [DTyp]
pars)) (Int
depthInt -> Int -> Int
forall a. Num a => a -> a -> a
-DDat -> Int
cost DDat
dat) Set CoverageAnnotation
forall a. Monoid a => a
mempty
              | DTyp
a <- [DTyp]
args ]
         in Verbosity -> Doc -> Dom -> Dom
forall a. Verbosity -> Doc -> a -> a
traceDoc Verbosity
Unions ((Doc
"expand" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
brackets (Int -> Doc
forall a. Pretty a => a -> Doc
pretty (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ [DCon] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DCon]
constrs)) Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty)
            (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ (Dom -> Dom -> Dom) -> [Dom] -> Dom
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Dom -> Dom -> Dom
dUnion [ HasCallStack => TyCtx -> Dom -> Dom -> Dom
TyCtx -> Dom -> Dom -> Dom
domApp TyCtx
ctx Dom
match (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ DTyp -> Int -> SnocList Dom -> Set CoverageAnnotation -> Dom
DConstr DTyp
ty Int
i (DCon -> SnocList Dom
topArgs DCon
c) Set CoverageAnnotation
alocs
                            | (Int
i, DCon
c) <- [Int] -> [DCon] -> [(Int, DCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [DCon]
constrs ]
      -- TODO: unuglyfy
      | DTVar{} <- DTyp
ty
      , (DDat Bool
True NamedTyDeBruijn
_ Kin
_ [NamedTyDeBruijn]
_ [DCon]
_) <- HasCallStack => TyCtx -> NamedTyDeBruijn -> DDat
TyCtx -> NamedTyDeBruijn -> DDat
lookupDat TyCtx
ctx NamedTyDeBruijn
d ->
        let ty :: DTyp
ty = NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTForall NamedTyDeBruijn
r Kin
Star (DTyp -> DTyp) -> DTyp -> DTyp
forall a b. (a -> b) -> a -> b
$ (DTyp -> DTyp -> DTyp) -> DTyp -> [DTyp] -> DTyp
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr DTyp -> DTyp -> DTyp
DTFun (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
r []) [DTyp]
argTypes
        in DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop DTyp
ty Int
aggro (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations TyCtx
ctx Dom
arg)
      | Bool
otherwise ->
        let ty :: DTyp
ty = NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTForall NamedTyDeBruijn
r Kin
Star (DTyp -> DTyp) -> DTyp -> DTyp
forall a b. (a -> b) -> a -> b
$ (DTyp -> DTyp -> DTyp) -> DTyp -> [DTyp] -> DTyp
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr DTyp -> DTyp -> DTyp
DTFun (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
r []) [DTyp]
argTypes
        in DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop DTyp
ty Int
0 (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations TyCtx
ctx Dom
arg)

    -- Constructor argument
    -- TODO: refactor lambdas (maybe have named (DLam) and un-named (DSusp) abstraction in the language
    -- and push closures over terms to their own constructor?)
    DConstr DTyp
_ Int
conIdx SnocList Dom
argsD Set CoverageAnnotation
alocs ->
      let n :: Int
n = [DCon] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DCon]
constrs
          m :: Int
m = SnocList Dom -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length SnocList Dom
argsD
          -- c_0{0} , ... , c_(n-1){0}
          xCargs :: [NamedDeBruijn]
xCargs = [ Text -> Index -> NamedDeBruijn
NamedDeBruijn (Text
"c" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
Text.pack (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)) Index
0
                   | Int
i <- [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]
          -- a_0{n} , ... , a_(m-1){n+m-1} :: Trm (_ctx :> c_0 ... c_(n-1))
          xAargs :: [Trm]
xAargs = [ () -> NamedDeBruijn -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () (NamedDeBruijn -> Trm) -> NamedDeBruijn -> Trm
forall a b. (a -> b) -> a -> b
$ Text -> Index -> NamedDeBruijn
NamedDeBruijn (Text
"a" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
Text.pack (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)) (Index -> NamedDeBruijn) -> Index -> NamedDeBruijn
forall a b. (a -> b) -> a -> b
$ Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)
                   | Int
i <- [Int
0..Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]
          -- a_m :> ... :> a_0
          -- argsD :: SnocList (DTyp ctx)
          -- means we need to shift it into ctx'
          substD :: SnocList Dom
substD = HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SnocList Dom -> Dom -> SnocList Dom)
-> SnocList Dom -> [Dom] -> SnocList Dom
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
(:>) SnocList Dom
forall a. SnocList a
Nil ([Dom] -> [Dom]
forall a. [a] -> [a]
reverse ([Dom] -> [Dom]) -> [Dom] -> [Dom]
forall a b. (a -> b) -> a -> b
$ SnocList Dom -> [Dom]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList SnocList Dom
argsD)
          -- t_1{0} , ... , t_(n-1){n-2}
          targs :: [Type NamedTyDeBruijn DefaultUni ()]
targs = [ () -> NamedTyDeBruijn -> Type NamedTyDeBruijn DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () (NamedTyDeBruijn -> Type NamedTyDeBruijn DefaultUni ())
-> NamedTyDeBruijn -> Type NamedTyDeBruijn DefaultUni ()
forall a b. (a -> b) -> a -> b
$ NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn
                             (NamedDeBruijn -> NamedTyDeBruijn)
-> NamedDeBruijn -> NamedTyDeBruijn
forall a b. (a -> b) -> a -> b
$ Text -> Index -> NamedDeBruijn
NamedDeBruijn (Text
"t" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
Text.pack (Int -> [Char]
forall a. Show a => a -> [Char]
show (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)))
                             (Index -> NamedDeBruijn) -> Index -> NamedDeBruijn
forall a b. (a -> b) -> a -> b
$ Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i
                  | Int
i <- [Int
0..Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2] ]
          -- t_n :> ... :> t_1
          substT :: Subst DTyp
substT = (Subst DTyp -> DTyp -> Subst DTyp)
-> Subst DTyp -> [DTyp] -> Subst DTyp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
(:>) Subst DTyp
forall a. SnocList a
Nil ([DTyp] -> [DTyp]
forall a. [a] -> [a]
reverse ([DTyp] -> [DTyp]) -> [DTyp] -> [DTyp]
forall a b. (a -> b) -> a -> b
$ [DTyp] -> [DTyp]
forall a. [a] -> [a]
tail [DTyp]
argTypes)
          -- c_conIdx{(n-1)-conIdx}
          con :: Trm
con = () -> NamedDeBruijn -> Trm
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () (NamedDeBruijn -> Trm) -> NamedDeBruijn -> Trm
forall a b. (a -> b) -> a -> b
$ Text -> Index -> NamedDeBruijn
NamedDeBruijn (Text
"c" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
Text.pack (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
conIdx)) (Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Index) -> Int -> Index
forall a b. (a -> b) -> a -> b
$ (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
conIdx)
      in NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
r Kin
Star (Set CoverageAnnotation
locs Set CoverageAnnotation
-> Set CoverageAnnotation -> Set CoverageAnnotation
forall a. Semigroup a => a -> a -> a
<> Set CoverageAnnotation
alocs) (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$
          -- \ c_0 : ta_0 ->
          NamedDeBruijn
-> DTyp
-> SnocList Dom
-> Subst DTyp
-> Trm
-> Set CoverageAnnotation
-> Dom
DLam ([NamedDeBruijn] -> NamedDeBruijn
forall a. [a] -> a
head [NamedDeBruijn]
xCargs) ([DTyp] -> DTyp
forall a. [a] -> a
head [DTyp]
argTypes)
               SnocList Dom
substD -- a_m :> ... :> a_0
               Subst DTyp
substT -- t_n :> ... :> t_1
               -- \ c_1 : t_1{0} , ... , c_n : t_n{n-1} ->
               ((Trm
 -> [(NamedDeBruijn, Type NamedTyDeBruijn DefaultUni ())] -> Trm)
-> [(NamedDeBruijn, Type NamedTyDeBruijn DefaultUni ())]
-> Trm
-> Trm
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((NamedDeBruijn, Type NamedTyDeBruijn DefaultUni ()) -> Trm -> Trm)
-> Trm
-> [(NamedDeBruijn, Type NamedTyDeBruijn DefaultUni ())]
-> Trm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((NamedDeBruijn -> Type NamedTyDeBruijn DefaultUni () -> Trm -> Trm)
-> (NamedDeBruijn, Type NamedTyDeBruijn DefaultUni ())
-> Trm
-> Trm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (()
-> NamedDeBruijn
-> Type NamedTyDeBruijn DefaultUni ()
-> Trm
-> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs ()))) ([NamedDeBruijn]
-> [Type NamedTyDeBruijn DefaultUni ()]
-> [(NamedDeBruijn, Type NamedTyDeBruijn DefaultUni ())]
forall a b. [a] -> [b] -> [(a, b)]
zip ([NamedDeBruijn] -> [NamedDeBruijn]
forall a. [a] -> [a]
tail [NamedDeBruijn]
xCargs) [Type NamedTyDeBruijn DefaultUni ()]
targs) (Trm -> Trm) -> Trm -> Trm
forall a b. (a -> b) -> a -> b
$
                -- c_conIdx{n-conIdx} a_0{0} ... a_m{m}
                (Trm -> Trm -> Trm) -> Trm -> [Trm] -> Trm
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (() -> Trm -> Trm -> Trm
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply ()) Trm
con [Trm]
xAargs)
               Set CoverageAnnotation
forall a. Monoid a => a
mempty

    Dom
_ -> [Char] -> Dom
forall a. HasCallStack => [Char] -> a
error ([Char] -> Dom) -> [Char] -> Dom
forall a b. (a -> b) -> a -> b
$ [Char]
"domApp: DMatch\narg = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Dom -> [Char]
forall a. Show a => a -> [Char]
show Dom
arg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\nctx = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyCtx -> [Char]
forall a. Show a => a -> [Char]
show TyCtx
ctx

    where
      r :: NamedTyDeBruijn
r    = NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (NamedDeBruijn -> NamedTyDeBruijn)
-> NamedDeBruijn -> NamedTyDeBruijn
forall a b. (a -> b) -> a -> b
$ Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
"r" Index
0
      ctx' :: TyCtx
ctx' = TyCtx
ctx TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn
r NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
Star
      -- pars :: [DTyp ctx]
      -- pars' :: [DTyp ctx']
      pars' :: [DTyp]
pars' = HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) (DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyp]
pars
      -- d' :: DTyp ctx'
      d' :: NamedTyDeBruijn
d'    = Weakening -> NamedTyDeBruijn -> NamedTyDeBruijn
forall i. IsDbName i => Weakening -> i -> i
wkDbIndex (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) NamedTyDeBruijn
d
      -- constrs :: [DCon (ctx' :> _nm ::: _k :> (_pars ::: _someKinds))]
      -- _nm = d'
      DDat Bool
_r NamedTyDeBruijn
_nm Kin
_k [NamedTyDeBruijn]
_pars [DCon]
constrs = HasCallStack => TyCtx -> NamedTyDeBruijn -> DDat
TyCtx -> NamedTyDeBruijn -> DDat
lookupDat TyCtx
ctx' NamedTyDeBruijn
d'
      -- mkConTy :: DCon (ctx' :> _nm{0} ::: _k :> (_pars ::: _someKinds)) -> DTyp ctx'
      mkConTy :: DCon -> DTyp
mkConTy (DCon [DTyp]
args) = (DTyp -> DTyp -> DTyp) -> DTyp -> [DTyp] -> DTyp
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr DTyp -> DTyp -> DTyp
DTFun (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
r []) ([DTyp] -> DTyp) -> [DTyp] -> DTyp
forall a b. (a -> b) -> a -> b
$ (DTyp -> [DTyp] -> DTyp) -> [DTyp] -> DTyp -> DTyp
forall a b c. (a -> b -> c) -> b -> a -> c
flip DTyp -> [DTyp] -> DTyp
tyInsts (if Bool
_r then [DTyp]
pars' else NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
d' [] DTyp -> [DTyp] -> [DTyp]
forall a. a -> [a] -> [a]
: [DTyp]
pars') (DTyp -> DTyp) -> [DTyp] -> [DTyp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyp]
args
      -- argTypes :: [DTyp ctx']
      argTypes :: [DTyp]
argTypes = (DCon -> DTyp) -> [DCon] -> [DTyp]
forall a b. (a -> b) -> [a] -> [b]
map DCon -> DTyp
mkConTy [DCon]
constrs

  Dom
_                                 -> Doc -> Dom
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Dom) -> Doc -> Dom
forall a b. (a -> b) -> a -> b
$ Doc
"domApp: " Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [ Doc
"d =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
d
                                                                      , Doc
"arg =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
arg
                                                                      , Doc
"ctx =" Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx]

domTyApp :: HasCallStack
         => TyCtx   -- (ctx : TyCtx)
         -> Dom     -- Dom ctx
         -> DTyp    -- DTyp ctx
         -> Dom     -- Dom ctx
domTyApp :: TyCtx -> Dom -> DTyp -> Dom
domTyApp TyCtx
ctx DTySusp{Set CoverageAnnotation
Kin
NamedTyDeBruijn
Dom
kind :: Dom -> Kin
suspName :: Dom -> NamedTyDeBruijn
inner :: Dom -> Dom
inner :: Dom
_locations :: Set CoverageAnnotation
kind :: Kin
suspName :: NamedTyDeBruijn
_locations :: Dom -> Set CoverageAnnotation
..} DTyp
a = HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations Set CoverageAnnotation
_locations (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ HasCallStack => TyCtx -> Dom -> DTyp -> Dom
TyCtx -> Dom -> DTyp -> Dom
domTyInst TyCtx
ctx Dom
inner DTyp
a
domTyApp TyCtx
_ Dom
DError        DTyp
_ = Dom
DError
domTyApp TyCtx
_ Dom
d DTyp
t             = Doc -> Dom
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Dom) -> Doc -> Dom
forall a b. (a -> b) -> a -> b
$ Doc
"domTyApps: " Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [ Doc
"d =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
d
                                                                 , Doc
"t =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
t ]

-- tyInst :: {ctx ctx' : TyCtx}
--        -> (i : Index | i == length ctx')
--        -> DTyp (ctx :> a ::: k :> ctx')
--        -> DTyp ctx
--        -> DTyp (ctx :> ctx')
tyInst :: HasCallStack => Index -> DTyp -> DTyp -> DTyp
tyInst :: Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
a DTyp
b = case HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy DTyp
a of
  DTVar NamedTyDeBruijn
x [DTyp]
ts | NamedTyDeBruijn -> Index
forall n. IsDbName n => n -> Index
getDbIndex NamedTyDeBruijn
x Index -> Index -> Bool
forall a. Ord a => a -> a -> Bool
> Index
i  -> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar (NamedTyDeBruijn -> Index -> NamedTyDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedTyDeBruijn
x (NamedTyDeBruijn -> Index
forall n. IsDbName n => n -> Index
getDbIndex NamedTyDeBruijn
x Index -> Index -> Index
forall a. Num a => a -> a -> a
- Index
1)) [DTyp]
ts'
             | NamedTyDeBruijn -> Index
forall n. IsDbName n => n -> Index
getDbIndex NamedTyDeBruijn
x Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== Index
i -> HasCallStack => DTyp -> [DTyp] -> DTyp
DTyp -> [DTyp] -> DTyp
tyApps (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
i) DTyp
b) [DTyp]
ts'
             | Bool
otherwise         -> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
x [DTyp]
ts'
             where ts' :: [DTyp]
ts' = [ HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
a DTyp
b | DTyp
a <- [DTyp]
ts ]
  DTFun DTyp
s DTyp
t      -> DTyp -> DTyp -> DTyp
DTFun (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
s DTyp
b) (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
t DTyp
b)
  DTLam NamedTyDeBruijn
x Kin
k DTyp
t    -> NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTLam NamedTyDeBruijn
x Kin
k (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst (Index
iIndex -> Index -> Index
forall a. Num a => a -> a -> a
+Index
1) DTyp
t DTyp
b)
  DTForall NamedTyDeBruijn
x Kin
k DTyp
t -> NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTForall NamedTyDeBruijn
x Kin
k (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst (Index
iIndex -> Index -> Index
forall a. Num a => a -> a -> a
+Index
1) DTyp
t DTyp
b)
  DTyBuiltin Kin
k   -> Kin -> DTyp
DTyBuiltin Kin
k
  DTWk Weakening
_ DTyp
_       -> [Char] -> DTyp
forall a. HasCallStack => [Char] -> a
error [Char]
"tyInst: DTWk"

domTyInst :: HasCallStack
          => TyCtx  -- (ctx : TyCtx)
          -> Dom    -- Dom (ctx :> x ::: k)
          -> DTyp   -- DTyp ctx
          -> Dom    -- Dom ctx
domTyInst :: TyCtx -> Dom -> DTyp -> Dom
domTyInst TyCtx
_ Dom
d DTyp
t = Index -> Dom -> Dom
go Index
0 Dom
d
  where
    -- go :: {ctx' : TyCtx}
    --    -> (i : Index | i == length ctx')
    --    -> Dom (ctx :> a ::: k :> ctx')
    --    -> Dom (ctx :> ctx')
    go :: Index -> Dom -> Dom
go !Index
i Dom
d = case HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
d of
      DTop DTyp
ty Int
dep Set CoverageAnnotation
locs                  -> DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
ty DTyp
t) Int
dep Set CoverageAnnotation
locs
      Dom
DError                            -> Dom
DError
      DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
locs Dom
body             -> NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
locs (Index -> Dom -> Dom
go (Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
+ Index
1) Dom
body)
      DSusp Set CoverageAnnotation
locs Dom
d                      -> Set CoverageAnnotation -> Dom -> Dom
DSusp Set CoverageAnnotation
locs (Index -> Dom -> Dom
go Index
i Dom
d)
      DIf DTyp
ty Set CoverageAnnotation
locs                       -> DTyp -> Set CoverageAnnotation -> Dom
DIf (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
ty DTyp
t) Set CoverageAnnotation
locs
      DTrace DTyp
ty Set CoverageAnnotation
locs                    -> DTyp -> Set CoverageAnnotation -> Dom
DTrace (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
ty DTyp
t) Set CoverageAnnotation
locs
      DLam NamedDeBruijn
x DTyp
ty SnocList Dom
substD Subst DTyp
substT Trm
body Set CoverageAnnotation
locs -> NamedDeBruijn
-> DTyp
-> SnocList Dom
-> Subst DTyp
-> Trm
-> Set CoverageAnnotation
-> Dom
DLam NamedDeBruijn
x (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
ty DTyp
t) (Index -> Dom -> Dom
go Index
i (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnocList Dom
substD)
                                                                  ((DTyp -> DTyp -> DTyp) -> DTyp -> DTyp -> DTyp
forall a b c. (a -> b -> c) -> b -> a -> c
flip (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i) DTyp
t (DTyp -> DTyp) -> Subst DTyp -> Subst DTyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst DTyp
substT)
                                                                  Trm
body Set CoverageAnnotation
locs
      DConstr DTyp
dat Int
con SnocList Dom
args Set CoverageAnnotation
locs         -> DTyp -> Int -> SnocList Dom -> Set CoverageAnnotation -> Dom
DConstr (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
dat DTyp
t) Int
con (Index -> Dom -> Dom
go Index
i (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnocList Dom
args) Set CoverageAnnotation
locs
      DMatch DTyp
dat Set CoverageAnnotation
locs                   -> DTyp -> Set CoverageAnnotation -> Dom
DMatch (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
i DTyp
dat DTyp
t) Set CoverageAnnotation
locs
      DLoc{}                            -> Dom
d
      DUnion [Dom]
ds                         -> [Dom] -> Dom
dUnions (Index -> Dom -> Dom
go Index
i (Dom -> Dom) -> [Dom] -> [Dom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom]
ds)
      DWeaken{}                         -> [Char] -> Dom
forall a. HasCallStack => [Char] -> a
error [Char]
"domTyInst: DWeaken"

tyApps :: HasCallStack => DTyp -> [DTyp] -> DTyp
tyApps :: DTyp -> [DTyp] -> DTyp
tyApps DTyp
t []                              = DTyp
t
tyApps t :: DTyp
t@DTWk{} [DTyp]
args                     = HasCallStack => DTyp -> [DTyp] -> DTyp
DTyp -> [DTyp] -> DTyp
tyApps (HasCallStack => DTyp -> DTyp
DTyp -> DTyp
pushWeakenTy DTyp
t) [DTyp]
args
tyApps (DTVar NamedTyDeBruijn
x [DTyp]
args0) [DTyp]
args              = NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
x ([DTyp]
args0 [DTyp] -> [DTyp] -> [DTyp]
forall a. Semigroup a => a -> a -> a
<> [DTyp]
args)
tyApps (DTLam NamedTyDeBruijn
_ Kin
_ DTyp
body) (DTyp
arg : [DTyp]
args)     = HasCallStack => DTyp -> [DTyp] -> DTyp
DTyp -> [DTyp] -> DTyp
tyApps (HasCallStack => Index -> DTyp -> DTyp -> DTyp
Index -> DTyp -> DTyp -> DTyp
tyInst Index
0 DTyp
body DTyp
arg) [DTyp]
args
tyApps (DTyBuiltin (Kin
_ :-> Kin
k)) (DTyp
_ : [DTyp]
args) = HasCallStack => DTyp -> [DTyp] -> DTyp
DTyp -> [DTyp] -> DTyp
tyApps (Kin -> DTyp
DTyBuiltin Kin
k) [DTyp]
args
tyApps DTyp
t [DTyp]
args                            = Doc -> DTyp
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> DTyp) -> Doc -> DTyp
forall a b. (a -> b) -> a -> b
$ Doc
"tyApps:" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [ Doc
"t =" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
t
                                                                         , Doc
"args =" Doc -> Doc -> Doc
<+> [DTyp] -> Doc
forall a. Pretty a => a -> Doc
pretty [DTyp]
args ]

domApps :: HasCallStack
        => TyCtx
        -> Dom
        -> [DArg] -> Dom
domApps :: TyCtx -> Dom -> [DArg] -> Dom
domApps TyCtx
ctx = (Dom -> DArg -> Dom) -> Dom -> [DArg] -> Dom
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Dom -> DArg -> Dom
app (Dom -> DArg -> Dom) -> (Dom -> Dom) -> Dom -> DArg -> Dom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken)
  where
    app :: Dom -> DArg -> Dom
app d :: Dom
d@(DUnion [Dom]
ds) DArg
a =
      let res0 :: [Dom]
res0 = (Dom -> DArg -> Dom
`app` DArg
a) (Dom -> Dom) -> [Dom] -> [Dom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom]
ds
          res :: Dom
res = [Dom] -> Dom
dUnions [Dom]
res0 in
      Verbosity -> Doc -> Dom -> Dom
forall a. Verbosity -> Doc -> a -> a
traceDoc Verbosity
High (Doc
"dUnionsApp:" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [ Doc
"ctx =" Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx
                                            , Doc
"d =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
d
                                            , Doc
"a =" Doc -> Doc -> Doc
<+> DArg -> Doc
forall a. Pretty a => a -> Doc
pretty DArg
a
                                            , Doc
"ds app a=" Doc -> Doc -> Doc
<+> [Dom] -> Doc
forall a. Pretty a => a -> Doc
pretty [Dom]
res0
                                            , Doc
"res =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
res ])
            Dom
res
    app Dom
d a :: DArg
a@(TyArg DTyp
t)   =
      let res :: Dom
res = HasCallStack => TyCtx -> Dom -> DTyp -> Dom
TyCtx -> Dom -> DTyp -> Dom
domTyApp TyCtx
ctx Dom
d DTyp
t in
      Verbosity -> Doc -> Dom -> Dom
forall a. Verbosity -> Doc -> a -> a
traceDoc Verbosity
High (Doc
"domTyApp:" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [ Doc
"ctx =" Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx
                                          , Doc
"d =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
d
                                          , Doc
"a =" Doc -> Doc -> Doc
<+> DArg -> Doc
forall a. Pretty a => a -> Doc
pretty DArg
a
                                          , Doc
"res =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
res ])
            Dom
res
    app Dom
d a :: DArg
a@(DArg Dom
d')      =
      let res :: Dom
res = HasCallStack => TyCtx -> Dom -> Dom -> Dom
TyCtx -> Dom -> Dom -> Dom
domApp TyCtx
ctx Dom
d (HasCallStack => Dom -> Dom
Dom -> Dom
pushWeaken Dom
d') in
      Verbosity -> Doc -> Dom -> Dom
forall a. Verbosity -> Doc -> a -> a
traceDoc Verbosity
High (Doc
"domApp:" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [ Doc
"ctx =" Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx
                                        , Doc
"d =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
d
                                        , Doc
"a =" Doc -> Doc -> Doc
<+> DArg -> Doc
forall a. Pretty a => a -> Doc
pretty DArg
a
                                        , Doc
"res =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty Dom
res ])
            Dom
res

interpTy :: HasCallStack
         => TyCtx         -- (ctx : TyCtx) {_ctx : TyCtx}
         -> Subst DTyp    -- Subst _ctx (DTyp ctx)
         -> Typ           -- Typ _ctx
         -> [DTyp]        -- [DTyp ctx]
         -> DTyp          -- DTyp ctx
interpTy :: TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx Subst DTyp
substT Type NamedTyDeBruijn DefaultUni ()
ty [DTyp]
args = case Type NamedTyDeBruijn DefaultUni ()
ty of
  TyVar ()
_ NamedTyDeBruijn
x     -> Subst DTyp -> Index -> DTyp
forall a. HasCallStack => Subst a -> Index -> a
lookupSubst Subst DTyp
substT (NamedTyDeBruijn -> Index
forall n. IsDbName n => n -> Index
getDbIndex NamedTyDeBruijn
x) HasCallStack => DTyp -> [DTyp] -> DTyp
DTyp -> [DTyp] -> DTyp
`tyApps` [DTyp]
args
  TyBuiltin ()
_ SomeTypeIn DefaultUni
c -> Kin -> DTyp
DTyBuiltin (SomeTypeIn DefaultUni -> Kin
builtinKind SomeTypeIn DefaultUni
c Kin -> [DTyp] -> Kin
`kindApp` [DTyp]
args)
    where
      kindApp :: Kin -> [DTyp] -> Kin
kindApp Kin
k         []         = Kin
k
      kindApp (Kin
_ :-> Kin
k) (DTyp
_ : [DTyp]
args) = Kin -> [DTyp] -> Kin
kindApp Kin
k [DTyp]
args
      kindApp Kin
Star      [DTyp]
_          = Doc -> Kin
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Kin) -> Doc -> Kin
forall a b. (a -> b) -> a -> b
$ Doc
"interpTy TyBuiltin:" Doc -> Doc -> Doc
<+> Type NamedTyDeBruijn DefaultUni () -> Doc
forall a. Pretty a => a -> Doc
pretty Type NamedTyDeBruijn DefaultUni ()
ty
  TyFun ()
_ Type NamedTyDeBruijn DefaultUni ()
a Type NamedTyDeBruijn DefaultUni ()
b | [] <- [DTyp]
args -> DTyp -> DTyp -> DTyp
DTFun (HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx Subst DTyp
substT Type NamedTyDeBruijn DefaultUni ()
a []) (HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx Subst DTyp
substT Type NamedTyDeBruijn DefaultUni ()
b [])
              | Bool
otherwise  -> [Char] -> DTyp
forall a. HasCallStack => [Char] -> a
error [Char]
"interpTy: TyFun"
  TyForall ()
_ NamedTyDeBruijn
x Kin
k Type NamedTyDeBruijn DefaultUni ()
b
    | [] <- [DTyp]
args -> NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTForall NamedTyDeBruijn
x Kin
k (DTyp -> DTyp) -> DTyp -> DTyp
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy (TyCtx
ctx TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn
x NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
k) ((HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) (DTyp -> DTyp) -> Subst DTyp -> Subst DTyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst DTyp
substT) Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
x []) Type NamedTyDeBruijn DefaultUni ()
b []
    | Bool
otherwise  -> [Char] -> DTyp
forall a. HasCallStack => [Char] -> a
error [Char]
"interpTy: TyForall"
  TyLam ()
_ NamedTyDeBruijn
x Kin
k Type NamedTyDeBruijn DefaultUni ()
b ->
    case [DTyp]
args of
      []         -> NamedTyDeBruijn -> Kin -> DTyp -> DTyp
DTLam NamedTyDeBruijn
x Kin
k (DTyp -> DTyp) -> DTyp -> DTyp
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy (TyCtx
ctx TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn
x NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
k) ((HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) (DTyp -> DTyp) -> Subst DTyp -> Subst DTyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst DTyp
substT) Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
x []) Type NamedTyDeBruijn DefaultUni ()
b []
      DTyp
arg : [DTyp]
args -> HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx (Subst DTyp
substT Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> DTyp
arg) Type NamedTyDeBruijn DefaultUni ()
b [DTyp]
args
  TyApp ()
_ Type NamedTyDeBruijn DefaultUni ()
a Type NamedTyDeBruijn DefaultUni ()
b   -> HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx Subst DTyp
substT Type NamedTyDeBruijn DefaultUni ()
a (HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx Subst DTyp
substT Type NamedTyDeBruijn DefaultUni ()
b [] DTyp -> [DTyp] -> [DTyp]
forall a. a -> [a] -> [a]
: [DTyp]
args)
  TyIFix ()
_ Type NamedTyDeBruijn DefaultUni ()
_ Type NamedTyDeBruijn DefaultUni ()
_  -> [Char] -> DTyp
forall a. HasCallStack => [Char] -> a
error [Char]
"interpTy: TyIFix"

-- interpDat :: {_ctx : TyCtx} (ctx : TyCtx)
--           -> Subst _ctx (DTyp ctx)
--           -> Dat _ctx
--           -> DDat ctx
interpDat :: HasCallStack
          => TyCtx
          -> Subst DTyp
          -> Dat
          -> Bool
          -> DDat
interpDat :: TyCtx -> Subst DTyp -> Dat -> Bool -> DDat
interpDat TyCtx
ctx Subst DTyp
substT (Datatype ()
_ (TyVarDecl ()
_ NamedTyDeBruijn
n Kin
k) [TyVarDecl NamedTyDeBruijn ()]
pars NamedDeBruijn
_ [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs) Bool
rec =
  Bool
-> NamedTyDeBruijn -> Kin -> [NamedTyDeBruijn] -> [DCon] -> DDat
DDat Bool
rec NamedTyDeBruijn
n Kin
k [ NamedTyDeBruijn
n | TyVarDecl ()
_ NamedTyDeBruijn
n Kin
_ <- [TyVarDecl NamedTyDeBruijn ()]
pars ] [ VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> DCon
mkDCon VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
c | VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
c <- [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs ]
  where
    ctxExts :: [TyCtxEntry]
ctxExts = [ NamedTyDeBruijn
n NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
k | Bool -> Bool
not Bool
rec ] [TyCtxEntry] -> [TyCtxEntry] -> [TyCtxEntry]
forall a. [a] -> [a] -> [a]
++ [ NamedTyDeBruijn
n NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
k | TyVarDecl ()
_ NamedTyDeBruijn
n Kin
k <- [TyVarDecl NamedTyDeBruijn ()]
pars ]
    ctx' :: TyCtx
ctx' = (TyCtx -> TyCtxEntry -> TyCtx) -> TyCtx -> [TyCtxEntry] -> TyCtx
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
(:>) TyCtx
ctx [TyCtxEntry]
ctxExts
    wkAmt :: Index
wkAmt = [TyCtxEntry] -> Index
forall i a. Num i => [a] -> i
genericLength [TyCtxEntry]
ctxExts

    substExts :: [DTyp]
substExts = [ NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
n [] | Bool -> Bool
not Bool
rec ] [DTyp] -> [DTyp] -> [DTyp]
forall a. [a] -> [a] -> [a]
++
                [ NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar (NamedTyDeBruijn -> Index -> NamedTyDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedTyDeBruijn
n (Index -> NamedTyDeBruijn) -> Index -> NamedTyDeBruijn
forall a b. (a -> b) -> a -> b
$ Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) []
                | (Int
i, TyVarDecl ()
_ NamedTyDeBruijn
n Kin
_) <- [Int]
-> [TyVarDecl NamedTyDeBruijn ()]
-> [(Int, TyVarDecl NamedTyDeBruijn ())]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int
0..[TyVarDecl NamedTyDeBruijn ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarDecl NamedTyDeBruijn ()]
pars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]) [TyVarDecl NamedTyDeBruijn ()]
pars]

    substT' :: Subst DTyp
substT' = (Subst DTyp -> DTyp -> Subst DTyp)
-> Subst DTyp -> [DTyp] -> Subst DTyp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
(:>) ((HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
wkAmt) (DTyp -> DTyp) -> Subst DTyp -> Subst DTyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst DTyp
substT)) [DTyp]
substExts

    mkDCon :: VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
-> DCon
mkDCon (VarDecl ()
_ NamedDeBruijn
_ Type NamedTyDeBruijn DefaultUni ()
ty) = [DTyp] -> DCon
DCon [ HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx' Subst DTyp
substT' Type NamedTyDeBruijn DefaultUni ()
a []
                                   | Type NamedTyDeBruijn DefaultUni ()
a <- Type NamedTyDeBruijn DefaultUni ()
-> [Type NamedTyDeBruijn DefaultUni ()]
-> [Type NamedTyDeBruijn DefaultUni ()]
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [Type tyname uni ann] -> [Type tyname uni ann]
funArgs Type NamedTyDeBruijn DefaultUni ()
ty [] ]

    funArgs :: Type tyname uni ann
-> [Type tyname uni ann] -> [Type tyname uni ann]
funArgs (TyFun ann
_ Type tyname uni ann
a Type tyname uni ann
b) [Type tyname uni ann]
args = Type tyname uni ann
-> [Type tyname uni ann] -> [Type tyname uni ann]
funArgs Type tyname uni ann
b (Type tyname uni ann
a Type tyname uni ann
-> [Type tyname uni ann] -> [Type tyname uni ann]
forall a. a -> [a] -> [a]
: [Type tyname uni ann]
args)
    funArgs Type tyname uni ann
_ [Type tyname uni ann]
args             = [Type tyname uni ann] -> [Type tyname uni ann]
forall a. [a] -> [a]
reverse [Type tyname uni ann]
args

-- interp_ :: {_ctx : TyCtx}
--         -> (ctx : TyCtx)
--         -> Subst _ctx (Dom ctx)
--         -> Subst _ctx (Typ ctx)
--         -> Trm _ctx
--         -> [DArg ctx]
--         -> Dom ctx
interp_ :: HasCallStack
        => TyCtx
        -> Subst Dom
        -> Subst DTyp
        -> Trm
        -> [DArg]
        -> Dom
interp_ :: TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ TyCtx
ctx SnocList Dom
substD Subst DTyp
substT Trm
trm [DArg]
args =
  case HasCallStack =>
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
interp TyCtx
ctx SnocList Dom
substD Subst DTyp
substT Trm
trm [DArg]
args of
    (TyCtx
Nil, Dom
d)  -> Dom
d
    (TyCtx
ctx', Dom
_) -> Doc -> Dom
forall a. HasCallStack => Doc -> a
errorDoc (Doc -> Dom) -> Doc -> Dom
forall a b. (a -> b) -> a -> b
$ Doc
"interp_: " Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx'

-- interp :: {_ctx : TyCtx}
--        -> (ctx : TyCtx)
--        -> Subst _ctx (Dom ctx)
--        -> Subst _ctx (Typ ctx)
--        -> Trm _ctx
--        -> [DArg ctx]
--        -> (ctx' : TyCtx) * Dom (ctx <> ctx')
interp :: HasCallStack
       => TyCtx
       -> Subst Dom
       -> Subst DTyp
       -> Trm
       -> [DArg]
       -> (TyCtx, Dom)
interp :: TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
interp TyCtx
ctx SnocList Dom
substD Subst DTyp
substT Trm
trm [DArg]
args =
  Verbosity -> Doc -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a. Verbosity -> Doc -> a -> a
traceDoc Verbosity
High (Doc
"interp:" Doc -> Doc -> Doc
<?> [Doc] -> Doc
vcat [ Doc
"ctx =" Doc -> Doc -> Doc
<+> TyCtx -> Doc
forall a. Pretty a => a -> Doc
pretty TyCtx
ctx
                                    , Doc
"substD =" Doc -> Doc -> Doc
<+> SnocList Dom -> Doc
forall a. Pretty a => a -> Doc
pretty SnocList Dom
substD
                                    , Doc
"substT =" Doc -> Doc -> Doc
<+> Subst DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty Subst DTyp
substT
                                    , Doc
"trm =" Doc -> Doc -> Doc
<+> Trm -> Doc
forall a. Pretty a => a -> Doc
pretty Trm
trm
                                    , Doc
"args =" Doc -> Doc -> Doc
<+> [DArg] -> Doc
forall a. Pretty a => a -> Doc
pretty [DArg]
args
                                    , Doc
"res =" Doc -> Doc -> Doc
<+> Dom -> Doc
forall a. Pretty a => a -> Doc
pretty ((TyCtx, Dom) -> Dom
forall a b. (a, b) -> b
snd (TyCtx, Dom)
res)])
        (TyCtx, Dom)
res
  where res :: (TyCtx, Dom)
res = case Trm
trm of
                Trm
BIF_Trace -> (TyCtx
forall a. SnocList a
Nil, HasCallStack => TyCtx -> Dom -> [DArg] -> Dom
TyCtx -> Dom -> [DArg] -> Dom
domApps TyCtx
ctx (NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
a Kin
Star Set CoverageAnnotation
forall a. Monoid a => a
mempty (DTyp -> Set CoverageAnnotation -> Dom
DTrace (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
a []) Set CoverageAnnotation
forall a. Monoid a => a
mempty)) [DArg]
args)
                  where a :: NamedTyDeBruijn
a = NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (NamedDeBruijn -> NamedTyDeBruijn)
-> NamedDeBruijn -> NamedTyDeBruijn
forall a b. (a -> b) -> a -> b
$ Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
"a" Index
0

                Trm
BIF_If -> (TyCtx
forall a. SnocList a
Nil, HasCallStack => TyCtx -> Dom -> [DArg] -> Dom
TyCtx -> Dom -> [DArg] -> Dom
domApps TyCtx
ctx (NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
a Kin
Star Set CoverageAnnotation
forall a. Monoid a => a
mempty (DTyp -> Set CoverageAnnotation -> Dom
DIf (NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
a []) Set CoverageAnnotation
forall a. Monoid a => a
mempty)) [DArg]
args)
                  where a :: NamedTyDeBruijn
a = NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (NamedDeBruijn -> NamedTyDeBruijn)
-> NamedDeBruijn -> NamedTyDeBruijn
forall a b. (a -> b) -> a -> b
$ Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
"a" Index
0

                LIT_Loc CoverageAnnotation
l
                  | [] <- [DArg]
args -> (TyCtx
forall a. SnocList a
Nil, CoverageAnnotation -> Dom
DLoc CoverageAnnotation
l)
                  | Bool
otherwise  -> [Char] -> (TyCtx, Dom)
forall a. HasCallStack => [Char] -> a
error [Char]
"interp: DLoc"

                Let ()
_ Recursivity
Rec NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
binds Trm
body -> (TyCtx -> TyCtx) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (TyCtx
dctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<>) ((TyCtx, Dom) -> (TyCtx, Dom)) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go SnocList Dom
substDwk (NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
binds)
                  where
                    fv :: Weakening
fv              = HasCallStack => Index -> Weakening
Index -> Weakening
wkBy (SnocList DDat -> Index
forall (f :: * -> *) i a.
(Functor f, Foldable f, Integral i) =>
f a -> i
len SnocList DDat
dats)
                    substDwk :: SnocList Dom
substDwk        = HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD Weakening
fv (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnocList Dom
substD
                    (SnocList DDat
dats, Subst DTyp
substT') = SnocList DDat
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (SnocList DDat, Subst DTyp)
buildTSubst SnocList DDat
forall a. SnocList a
Nil (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT Weakening
fv (DTyp -> DTyp) -> Subst DTyp -> Subst DTyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst DTyp
substT) (NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
binds)
                    dctx :: TyCtx
dctx | SnocList DDat
Nil <- SnocList DDat
dats = TyCtx
forall a. SnocList a
Nil
                         | Bool
otherwise   = TyCtx
forall a. SnocList a
Nil TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> SnocList DDat -> TyCtxEntry
TyCtxRecDat SnocList DDat
dats
                    ctx' :: TyCtx
ctx'            = TyCtx
ctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
dctx
                    substDR :: SnocList Dom
substDR         = SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> SnocList Dom
buildDSubst SnocList Dom
substDwk (NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
binds)

                    buildTSubst :: SnocList DDat
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (SnocList DDat, Subst DTyp)
buildTSubst SnocList DDat
dats Subst DTyp
substT [] = (SnocList DDat
dats, Subst DTyp
substT)
                    buildTSubst SnocList DDat
dats Subst DTyp
substT (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
b:[Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds) = case Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
b of
                      TypeBind ()
_ (TyVarDecl ()
_ NamedTyDeBruijn
_ Kin
_) Type NamedTyDeBruijn DefaultUni ()
ty ->
                        -- This is subtle! We use the ctx' and substT' that we are in the process of computing
                        -- (laziness ftw). This is fine (insert dog meme) because type synonyms can't be recursive.
                        SnocList DDat
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (SnocList DDat, Subst DTyp)
buildTSubst SnocList DDat
dats (Subst DTyp
substT Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx' Subst DTyp
substT' Type NamedTyDeBruijn DefaultUni ()
ty []) [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                      DatatypeBind ()
_ dat :: Dat
dat@(Datatype ()
_ (TyVarDecl ()
_ NamedTyDeBruijn
n Kin
_) [TyVarDecl NamedTyDeBruijn ()]
pars NamedDeBruijn
_ [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs) ->
                        let normDat :: DDat
normDat      = HasCallStack => TyCtx -> Subst DTyp -> Dat -> Bool -> DDat
TyCtx -> Subst DTyp -> Dat -> Bool -> DDat
interpDat TyCtx
ctx' Subst DTyp
substT' Dat
dat Bool
True -- :: Dat ctx'
                            (DTyp
dDat, Dom
_, [Dom]
_) = NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (DTyp, Dom, [Dom])
forall (t :: * -> *) (t :: * -> *) a tyname name (uni :: * -> *)
       fun a.
(Foldable t, Foldable t) =>
NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> t a
-> t (Binding tyname name uni fun a)
-> (DTyp, Dom, [Dom])
mkDat NamedTyDeBruijn
n [TyVarDecl NamedTyDeBruijn ()]
pars [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                        in SnocList DDat
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (SnocList DDat, Subst DTyp)
buildTSubst (SnocList DDat
dats SnocList DDat -> DDat -> SnocList DDat
forall a. SnocList a -> a -> SnocList a
:> DDat
normDat) (Subst DTyp
substT Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> DTyp
dDat) [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                      Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
_ -> SnocList DDat
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (SnocList DDat, Subst DTyp)
buildTSubst SnocList DDat
dats Subst DTyp
substT [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds

                    buildDSubst :: SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> SnocList Dom
buildDSubst SnocList Dom
substD [] = SnocList Dom
substD
                    buildDSubst SnocList Dom
substD (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
b:[Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds) = case Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
b of                                    -- TODO: locations?? (should be all locations in the letrec!) really use aggro here?
                      TermBind ()
_ Strictness
_ (VarDecl ()
_ NamedDeBruijn
_ Type NamedTyDeBruijn DefaultUni ()
ty) Trm
_ -> SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> SnocList Dom
buildDSubst (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop (HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx' Subst DTyp
substT' Type NamedTyDeBruijn DefaultUni ()
ty []) Int
aggro Set CoverageAnnotation
forall a. Monoid a => a
mempty)
                                                                     [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                      DatatypeBind ()
_ (Datatype ()
_ (TyVarDecl ()
_ NamedTyDeBruijn
n Kin
_) [TyVarDecl NamedTyDeBruijn ()]
pars NamedDeBruijn
_ [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs) ->
                        let (DTyp
_, Dom
dMatch, [Dom]
dConstrs) = NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (DTyp, Dom, [Dom])
forall (t :: * -> *) (t :: * -> *) a tyname name (uni :: * -> *)
       fun a.
(Foldable t, Foldable t) =>
NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> t a
-> t (Binding tyname name uni fun a)
-> (DTyp, Dom, [Dom])
mkDat NamedTyDeBruijn
n [TyVarDecl NamedTyDeBruijn ()]
pars [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                            substD' :: SnocList Dom
substD'   = (SnocList Dom -> Dom -> SnocList Dom)
-> SnocList Dom -> [Dom] -> SnocList Dom
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
(:>) SnocList Dom
substD (Dom
dMatch Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
dConstrs)
                        in SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> SnocList Dom
buildDSubst SnocList Dom
substD' [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                      Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
_ -> SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> SnocList Dom
buildDSubst SnocList Dom
substD [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds

                    go :: SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go SnocList Dom
substD [] = HasCallStack =>
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
interp TyCtx
ctx' SnocList Dom
substD Subst DTyp
substT' Trm
body ([DArg] -> (TyCtx, Dom)) -> [DArg] -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ HasCallStack => Weakening -> DArg -> DArg
Weakening -> DArg -> DArg
wkArg Weakening
fv (DArg -> DArg) -> [DArg] -> [DArg]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DArg]
args
                    go SnocList Dom
substD (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
b:[Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds) = case Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
b of
                      TermBind ()
_ Strictness
s (VarDecl ()
_ NamedDeBruijn
_ Type NamedTyDeBruijn DefaultUni ()
_) Trm
body ->
                        let result :: Dom
result = HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ TyCtx
ctx' SnocList Dom
substDR Subst DTyp
substT' Trm
body []
                            locs :: Dom -> Set CoverageAnnotation
locs Dom
result = if Strictness
s Strictness -> Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness
Strict then HasCallStack => Dom -> Set CoverageAnnotation
Dom -> Set CoverageAnnotation
topLevelLocations Dom
result else Set CoverageAnnotation
forall a. Monoid a => a
mempty
                        in case Dom
result of
                            -- TODO: the compiler bug also affects this line below!
                            Dom
DError | Strictness
s Strictness -> Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness
Strict -> (Dom -> Dom) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Dom -> Dom -> Dom
forall a b. a -> b -> a
const Dom
DError) ((TyCtx, Dom) -> (TyCtx, Dom)) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
result) [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                            DUnion [Dom]
ds            ->
                              let rs :: [(TyCtx, Dom)]
rs = [ (Dom -> Dom) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations (Dom -> Set CoverageAnnotation
locs Dom
result))
                                           ((TyCtx, Dom) -> (TyCtx, Dom)) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
result) [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds | Dom
result <- [Dom]
ds ]
                              in ((TyCtx, Dom) -> TyCtx
forall a b. (a, b) -> a
fst ([(TyCtx, Dom)] -> (TyCtx, Dom)
forall a. [a] -> a
head [(TyCtx, Dom)]
rs), [Dom] -> Dom
dUnions ([Dom] -> Dom) -> [Dom] -> Dom
forall a b. (a -> b) -> a -> b
$ ((TyCtx, Dom) -> Dom) -> [(TyCtx, Dom)] -> [Dom]
forall a b. (a -> b) -> [a] -> [b]
map (TyCtx, Dom) -> Dom
forall a b. (a, b) -> b
snd [(TyCtx, Dom)]
rs)
                            Dom
_                    -> (Dom -> Dom) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations (Dom -> Set CoverageAnnotation
locs Dom
result))
                                                      ((TyCtx, Dom) -> (TyCtx, Dom)) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
result) [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds

                      DatatypeBind ()
_ (Datatype ()
_ (TyVarDecl ()
_ NamedTyDeBruijn
n Kin
_) [TyVarDecl NamedTyDeBruijn ()]
pars NamedDeBruijn
_ [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs) ->
                        let (DTyp
_, Dom
dMatch, [Dom]
dConstrs) = NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (DTyp, Dom, [Dom])
forall (t :: * -> *) (t :: * -> *) a tyname name (uni :: * -> *)
       fun a.
(Foldable t, Foldable t) =>
NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> t a
-> t (Binding tyname name uni fun a)
-> (DTyp, Dom, [Dom])
mkDat NamedTyDeBruijn
n [TyVarDecl NamedTyDeBruijn ()]
pars [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                            substD' :: SnocList Dom
substD'  = (SnocList Dom -> Dom -> SnocList Dom)
-> SnocList Dom -> [Dom] -> SnocList Dom
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
(:>) SnocList Dom
substD (Dom
dMatch Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
dConstrs)
                        in SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go SnocList Dom
substD' [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds

                      Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
_ -> SnocList Dom
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go SnocList Dom
substD [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds

                Let ()
_ Recursivity
_ NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
binds Trm
body -> TyCtx
-> SnocList Dom
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go TyCtx
forall a. SnocList a
Nil SnocList Dom
substD Subst DTyp
substT (NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty
  (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
binds)
                  where
                    -- go :: {_ctx : Ctx} (ctx' : Ctx)
                    --    -> Subst _ctx (Dom (ctx <> ctx'))
                    --    -> Subst _ctx (Typ (ctx <> ctx'))
                    --    -> Binds _ctx
                    --    -> (ctx'' : Ctx) * Dom (ctx <> ctx'')
                    go :: TyCtx
-> SnocList Dom
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go TyCtx
ctx' SnocList Dom
substD Subst DTyp
substT [] = (TyCtx -> TyCtx) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (TyCtx
ctx' TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<>) ((TyCtx, Dom) -> (TyCtx, Dom)) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
interp (TyCtx
ctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx') SnocList Dom
substD Subst DTyp
substT Trm
body
                                                                  ([DArg] -> (TyCtx, Dom)) -> [DArg] -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ HasCallStack => Weakening -> DArg -> DArg
Weakening -> DArg -> DArg
wkArg (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy (Index -> Weakening) -> Index -> Weakening
forall a b. (a -> b) -> a -> b
$ HasCallStack => TyCtx -> Index
TyCtx -> Index
ctxLen TyCtx
ctx') (DArg -> DArg) -> [DArg] -> [DArg]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DArg]
args
                    go TyCtx
ctx' SnocList Dom
substD Subst DTyp
substT (Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
b:[Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds) = case Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
b of
                      TermBind ()
_ Strictness
s (VarDecl ()
_ NamedDeBruijn
_ Type NamedTyDeBruijn DefaultUni ()
_) Trm
body ->
                        let result :: Dom
result = HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ (TyCtx
ctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx') SnocList Dom
substD Subst DTyp
substT Trm
body []
                            locs :: Dom -> Set CoverageAnnotation
locs Dom
result = if Strictness
s Strictness -> Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness
Strict then HasCallStack => Dom -> Set CoverageAnnotation
Dom -> Set CoverageAnnotation
topLevelLocations Dom
result else Set CoverageAnnotation
forall a. Monoid a => a
mempty
                        in case Dom
result of
                            -- TODO: not the fastest way to do this (datatypes in the continuation?)
                            Dom
DError | Strictness
s Strictness -> Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness
Strict -> (Dom -> Dom) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Dom -> Dom -> Dom
forall a b. a -> b -> a
const Dom
DError)
                                                    ((TyCtx, Dom) -> (TyCtx, Dom)) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ TyCtx
-> SnocList Dom
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go TyCtx
ctx' (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
result) Subst DTyp
substT [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                            DUnion [Dom]
ds            ->
                              let rs :: [(TyCtx, Dom)]
rs = [(Dom -> Dom) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations (Dom -> Set CoverageAnnotation
locs Dom
result))
                                                                ((TyCtx, Dom) -> (TyCtx, Dom)) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ TyCtx
-> SnocList Dom
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go TyCtx
ctx' (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
result) Subst DTyp
substT [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds
                                                            | Dom
result <- [Dom]
ds ]
                              in ((TyCtx, Dom) -> TyCtx
forall a b. (a, b) -> a
fst ([(TyCtx, Dom)] -> (TyCtx, Dom)
forall a. [a] -> a
head [(TyCtx, Dom)]
rs), [Dom] -> Dom
dUnions (((TyCtx, Dom) -> Dom) -> [(TyCtx, Dom)] -> [Dom]
forall a b. (a -> b) -> [a] -> [b]
map (TyCtx, Dom) -> Dom
forall a b. (a, b) -> b
snd [(TyCtx, Dom)]
rs))
                            Dom
_                    -> (Dom -> Dom) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations (Dom -> Set CoverageAnnotation
locs Dom
result))
                                                    ((TyCtx, Dom) -> (TyCtx, Dom)) -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a b. (a -> b) -> a -> b
$ TyCtx
-> SnocList Dom
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go TyCtx
ctx' (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
result) Subst DTyp
substT [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds

                      -- TODO: remove (also wrong?)
                      TypeBind ()
_ (TyVarDecl ()
_ NamedTyDeBruijn
_ Kin
_) Type NamedTyDeBruijn DefaultUni ()
ty    ->
                        TyCtx
-> SnocList Dom
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go TyCtx
ctx' SnocList Dom
substD (Subst DTyp
substT Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy (TyCtx
ctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx') Subst DTyp
substT Type NamedTyDeBruijn DefaultUni ()
ty []) [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds

                      DatatypeBind ()
_ dat :: Dat
dat@(Datatype ()
_ (TyVarDecl ()
_ NamedTyDeBruijn
n Kin
_) [TyVarDecl NamedTyDeBruijn ()]
pars NamedDeBruijn
_ [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs) ->
                        let (DTyp
dDat, Dom
dMatch, [Dom]
dConstrs) = NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> SnocList (Binding Any Any Any Any Any)
-> (DTyp, Dom, [Dom])
forall (t :: * -> *) (t :: * -> *) a tyname name (uni :: * -> *)
       fun a.
(Foldable t, Foldable t) =>
NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> t a
-> t (Binding tyname name uni fun a)
-> (DTyp, Dom, [Dom])
mkDat NamedTyDeBruijn
n [TyVarDecl NamedTyDeBruijn ()]
pars [VarDecl NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
constrs SnocList (Binding Any Any Any Any Any)
forall a. SnocList a
Nil  -- dDat == Var 0
                            normDat :: DDat
normDat = HasCallStack => TyCtx -> Subst DTyp -> Dat -> Bool -> DDat
TyCtx -> Subst DTyp -> Dat -> Bool -> DDat
interpDat (TyCtx
ctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx') Subst DTyp
substT Dat
dat Bool
False -- :: DDat (ctx <> ctx')
                            substD' :: SnocList Dom
substD' = (SnocList Dom -> Dom -> SnocList Dom)
-> SnocList Dom -> [Dom] -> SnocList Dom
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
(:>) (HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnocList Dom
substD) (Dom
dMatch Dom -> [Dom] -> [Dom]
forall a. a -> [a] -> [a]
: [Dom]
dConstrs)
                        in TyCtx
-> SnocList Dom
-> Subst DTyp
-> [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
-> (TyCtx, Dom)
go (TyCtx
ctx' TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> DDat -> TyCtxEntry
TyCtxDat DDat
normDat) SnocList Dom
substD' ((DTyp -> DTyp) -> Subst DTyp -> Subst DTyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1)) Subst DTyp
substT Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> DTyp
dDat) [Binding NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()]
binds

                Error{} -> (TyCtx
forall a. SnocList a
Nil, Dom
DError)

                Var ()
_ nm :: NamedDeBruijn
nm@(NamedDeBruijn Text
_ Index
idx) ->
                  Verbosity -> Doc -> (TyCtx, Dom) -> (TyCtx, Dom)
forall a. Verbosity -> Doc -> a -> a
traceDoc Verbosity
Low (Doc
"interp: lookupVar" Doc -> Doc -> Doc
<+> NamedDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty NamedDeBruijn
nm)
                    (TyCtx
forall a. SnocList a
Nil, HasCallStack => TyCtx -> Dom -> [DArg] -> Dom
TyCtx -> Dom -> [DArg] -> Dom
domApps TyCtx
ctx (SnocList Dom -> Index -> Dom
forall a. HasCallStack => Subst a -> Index -> a
lookupSubst SnocList Dom
substD Index
idx) [DArg]
args)

                TyAbs ()
_ NamedTyDeBruijn
x Kin
k Trm
t
                  | TyArg DTyp
a : [DArg]
args' <- [DArg]
args -> (TyCtx
forall a. SnocList a
Nil, HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ TyCtx
ctx SnocList Dom
substD (Subst DTyp
substT Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> DTyp
a) Trm
t [DArg]
args')

                  | [] <- [DArg]
args              -> (TyCtx
forall a. SnocList a
Nil, NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
forall a. Monoid a => a
mempty (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ (TyCtx
ctx TyCtx -> TyCtxEntry -> TyCtx
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn
x NamedTyDeBruijn -> Kin -> TyCtxEntry
::: Kin
k)
                                                                                  (HasCallStack => Weakening -> Dom -> Dom
Weakening -> Dom -> Dom
wkD (HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) (Dom -> Dom) -> SnocList Dom -> SnocList Dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnocList Dom
substD)
                                                                                  ((DTyp -> DTyp) -> Subst DTyp -> Subst DTyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HasCallStack => Weakening -> DTyp -> DTyp
Weakening -> DTyp -> DTyp
wkT (Weakening -> DTyp -> DTyp) -> Weakening -> DTyp -> DTyp
forall a b. (a -> b) -> a -> b
$ HasCallStack => Index -> Weakening
Index -> Weakening
wkBy Index
1) Subst DTyp
substT Subst DTyp -> DTyp -> Subst DTyp
forall a. SnocList a -> a -> SnocList a
:> NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar NamedTyDeBruijn
x [])
                                                                                  Trm
t []) -- x is guaranteed to be 0 + a name

                  | Bool
otherwise              -> [Char] -> (TyCtx, Dom)
forall a. HasCallStack => [Char] -> a
error [Char]
"interp: TyAbs"

                (LamAbs ()
_ NamedDeBruijn
x Type NamedTyDeBruijn DefaultUni ()
a Trm
t)
                  | DArg (DUnion [Dom]
ds) : [DArg]
args' <- [DArg]
args -> (TyCtx
forall a. SnocList a
Nil, [Dom] -> Dom
dUnions [ Dom -> [DArg] -> Dom
app Dom
d [DArg]
args' | Dom
d <- [Dom]
ds ])

                  | DArg Dom
d : [DArg]
args' <- [DArg]
args -> (TyCtx
forall a. SnocList a
Nil, Dom -> [DArg] -> Dom
app Dom
d [DArg]
args')

                  | [] <- [DArg]
args -> (TyCtx
forall a. SnocList a
Nil, NamedDeBruijn
-> DTyp
-> SnocList Dom
-> Subst DTyp
-> Trm
-> Set CoverageAnnotation
-> Dom
DLam NamedDeBruijn
x (HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx Subst DTyp
substT Type NamedTyDeBruijn DefaultUni ()
a []) SnocList Dom
substD Subst DTyp
substT Trm
t Set CoverageAnnotation
forall a. Monoid a => a
mempty)

                  | Bool
otherwise -> [Char] -> (TyCtx, Dom)
forall a. HasCallStack => [Char] -> a
error [Char]
"interp: LamAbs"
                  where app :: Dom -> [DArg] -> Dom
app Dom
d [DArg]
args' = HasCallStack => Set CoverageAnnotation -> Dom -> Dom
Set CoverageAnnotation -> Dom -> Dom
addLocations (HasCallStack => Dom -> Set CoverageAnnotation
Dom -> Set CoverageAnnotation
topLevelLocations Dom
d) (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ TyCtx
ctx (SnocList Dom
substD SnocList Dom -> Dom -> SnocList Dom
forall a. SnocList a -> a -> SnocList a
:> Dom
d) Subst DTyp
substT Trm
t [DArg]
args'

                Apply ()
_ Trm
t Trm
t' -> case HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ TyCtx
ctx SnocList Dom
substD Subst DTyp
substT Trm
t' [] of
                  Dom
DError -> (TyCtx
forall a. SnocList a
Nil, Dom
DError)
                  Dom
d      -> (TyCtx
forall a. SnocList a
Nil, HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ TyCtx
ctx SnocList Dom
substD Subst DTyp
substT Trm
t (Dom -> DArg
DArg Dom
d DArg -> [DArg] -> [DArg]
forall a. a -> [a] -> [a]
: [DArg]
args))

                TyInst ()
_ Trm
t Type NamedTyDeBruijn DefaultUni ()
a -> (TyCtx
forall a. SnocList a
Nil, HasCallStack =>
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
TyCtx -> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> Dom
interp_ TyCtx
ctx SnocList Dom
substD Subst DTyp
substT Trm
t (DTyp -> DArg
TyArg (HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx Subst DTyp
substT Type NamedTyDeBruijn DefaultUni ()
a []) DArg -> [DArg] -> [DArg]
forall a. a -> [a] -> [a]
: [DArg]
args))

                Constant ()
_ Some (ValueOf DefaultUni)
_
                  | [] <- [DArg]
args -> (TyCtx
forall a. SnocList a
Nil, DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop (Kin -> DTyp
DTyBuiltin (Kin -> DTyp) -> Kin -> DTyp
forall a b. (a -> b) -> a -> b
$ Kin
Star) Int
aggro Set CoverageAnnotation
forall a. Monoid a => a
mempty)
                  | Bool
otherwise   -> [Char] -> (TyCtx, Dom)
forall a. HasCallStack => [Char] -> a
error [Char]
"interp: Constant"

                Builtin ()
_ DefaultFun
b -> (TyCtx
forall a. SnocList a
Nil, HasCallStack => TyCtx -> Dom -> [DArg] -> Dom
TyCtx -> Dom -> [DArg] -> Dom
domApps TyCtx
ctx (DTyp -> Int -> Set CoverageAnnotation -> Dom
dTop (HasCallStack =>
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
TyCtx
-> Subst DTyp
-> Type NamedTyDeBruijn DefaultUni ()
-> [DTyp]
-> DTyp
interpTy TyCtx
ctx Subst DTyp
substT
                                                                 (HasCallStack =>
DBCtx TyName -> Typ' -> Type NamedTyDeBruijn DefaultUni ()
DBCtx TyName -> Typ' -> Type NamedTyDeBruijn DefaultUni ()
toDeBruijn_Typ [] (Typ' -> Type NamedTyDeBruijn DefaultUni ())
-> Typ' -> Type NamedTyDeBruijn DefaultUni ()
forall a b. (a -> b) -> a -> b
$ DefaultFun -> Typ'
forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
fun -> Type TyName uni ()
typeOfBuiltinFunction DefaultFun
b) [])
                                                       Int
aggro Set CoverageAnnotation
forall a. Monoid a => a
mempty) [DArg]
args)

                IWrap{} -> [Char] -> (TyCtx, Dom)
forall a. HasCallStack => [Char] -> a
error [Char]
"interp: IWrap"
                Unwrap{} -> [Char] -> (TyCtx, Dom)
forall a. HasCallStack => [Char] -> a
error [Char]
"interp: Unwrap"
                where
                  mkDat :: NamedTyDeBruijn
-> [TyVarDecl NamedTyDeBruijn ()]
-> t a
-> t (Binding tyname name uni fun a)
-> (DTyp, Dom, [Dom])
mkDat NamedTyDeBruijn
n [TyVarDecl NamedTyDeBruijn ()]
pars t a
constrs t (Binding tyname name uni fun a)
binds = ( Int -> [DTyp] -> DTyp
dDat Int
0 []
                                               , Dom -> Dom
susp (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ DTyp -> Set CoverageAnnotation -> Dom
DMatch (Int -> [DTyp] -> DTyp
dDat ([TyVarDecl NamedTyDeBruijn ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarDecl NamedTyDeBruijn ()]
pars) [DTyp]
args) Set CoverageAnnotation
forall a. Monoid a => a
mempty
                                               , [ Dom -> Dom
susp (Dom -> Dom) -> Dom -> Dom
forall a b. (a -> b) -> a -> b
$ DTyp -> Int -> SnocList Dom -> Set CoverageAnnotation -> Dom
DConstr (Int -> [DTyp] -> DTyp
dDat ([TyVarDecl NamedTyDeBruijn ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarDecl NamedTyDeBruijn ()]
pars) [DTyp]
args) Int
i SnocList Dom
forall a. SnocList a
Nil Set CoverageAnnotation
forall a. Monoid a => a
mempty
                                                 | Int
i <- [Int
0..t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
constrs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ])
                    where
                      susp :: Dom -> Dom
susp = ((Dom -> Dom) -> (Dom -> Dom) -> Dom -> Dom)
-> (Dom -> Dom) -> [Dom -> Dom] -> Dom -> Dom
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Dom -> Dom) -> (Dom -> Dom) -> Dom -> Dom
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Dom -> Dom
forall a. a -> a
id [ NamedTyDeBruijn -> Kin -> Set CoverageAnnotation -> Dom -> Dom
DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
forall a. Monoid a => a
mempty | TyVarDecl ()
_ NamedTyDeBruijn
x Kin
k <- [TyVarDecl NamedTyDeBruijn ()]
pars ]
                      args :: [DTyp]
args = [DTyp] -> [DTyp]
forall a. [a] -> [a]
reverse [ NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar (NamedTyDeBruijn -> Index -> NamedTyDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedTyDeBruijn
x Index
i) [] | (Index
i, TyVarDecl ()
_ NamedTyDeBruijn
x Kin
_ ) <- [Index]
-> [TyVarDecl NamedTyDeBruijn ()]
-> [(Index, TyVarDecl NamedTyDeBruijn ())]
forall a b. [a] -> [b] -> [(a, b)]
zip [Index
0..] ([TyVarDecl NamedTyDeBruijn ()] -> [TyVarDecl NamedTyDeBruijn ()]
forall a. [a] -> [a]
reverse [TyVarDecl NamedTyDeBruijn ()]
pars) ]
                      -- Compute db index for a datatype by counting number of data type binds remaining.
                      dDat :: Int -> [DTyp] -> DTyp
dDat Int
k = NamedTyDeBruijn -> [DTyp] -> DTyp
DTVar (NamedTyDeBruijn -> Index -> NamedTyDeBruijn
forall n. IsDbName n => n -> Index -> n
setDbIndex NamedTyDeBruijn
n (Index -> NamedTyDeBruijn) -> Index -> NamedTyDeBruijn
forall a b. (a -> b) -> a -> b
$ Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Index) -> Int -> Index
forall a b. (a -> b) -> a -> b
$ Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [() | DatatypeBind{} <- t (Binding tyname name uni fun a)
-> [Binding tyname name uni fun a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t (Binding tyname name uni fun a)
binds])

interpCode :: HasCallStack => CompiledCodeIn DefaultUni DefaultFun a -> (TyCtx, Dom)
interpCode :: CompiledCodeIn DefaultUni DefaultFun a -> (TyCtx, Dom)
interpCode CompiledCodeIn DefaultUni DefaultFun a
cc = HasCallStack =>
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
TyCtx
-> SnocList Dom -> Subst DTyp -> Trm -> [DArg] -> (TyCtx, Dom)
interp TyCtx
forall a. SnocList a
Nil SnocList Dom
forall a. SnocList a
Nil Subst DTyp
forall a. SnocList a
Nil (CompiledCodeIn DefaultUni DefaultFun a -> Trm
forall a. HasCallStack => CompiledCode a -> Trm
getTrm CompiledCodeIn DefaultUni DefaultFun a
cc) []

allNonFailLocations :: HasCallStack => CompiledCodeIn DefaultUni DefaultFun a -> Set CoverageAnnotation
allNonFailLocations :: CompiledCodeIn DefaultUni DefaultFun a -> Set CoverageAnnotation
allNonFailLocations = (TyCtx -> Dom -> Set CoverageAnnotation)
-> (TyCtx, Dom) -> Set CoverageAnnotation
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry HasCallStack => TyCtx -> Dom -> Set CoverageAnnotation
TyCtx -> Dom -> Set CoverageAnnotation
allLocations ((TyCtx, Dom) -> Set CoverageAnnotation)
-> (CompiledCodeIn DefaultUni DefaultFun a -> (TyCtx, Dom))
-> CompiledCodeIn DefaultUni DefaultFun a
-> Set CoverageAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompiledCodeIn DefaultUni DefaultFun a -> (TyCtx, Dom)
forall a.
HasCallStack =>
CompiledCodeIn DefaultUni DefaultFun a -> (TyCtx, Dom)
interpCode