{-# LANGUAGE NamedFieldPuns #-}
-- concrete syntax
module Concrete where

import Prelude hiding (null)

import Util
import Abstract
  (Co, Sized, PiSigma(..), Dec, Override(..), Measure(..), Bound(..), HasPred(..), LtLe(..), polarity)
import Polarity

-- | Concrete names.
data Name = Name { Name -> String
theName :: String }
  deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
/= :: Name -> Name -> Bool
Eq, Eq Name
Eq Name =>
(Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Name -> Name -> Ordering
compare :: Name -> Name -> Ordering
$c< :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
>= :: Name -> Name -> Bool
$cmax :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
min :: Name -> Name -> Name
Ord)

instance Show Name where
  show :: Name -> String
show (Name String
n) = String
n

-- | Possibly qualified names.
data QName
  = Qual  { QName -> Name
qual :: Name, QName -> Name
name :: Name }  -- ^ @X.x@ e.g. qualified constructor.
  | QName { name :: Name }                -- ^ @x@.
  deriving (QName -> QName -> Bool
(QName -> QName -> Bool) -> (QName -> QName -> Bool) -> Eq QName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QName -> QName -> Bool
== :: QName -> QName -> Bool
$c/= :: QName -> QName -> Bool
/= :: QName -> QName -> Bool
Eq, Eq QName
Eq QName =>
(QName -> QName -> Ordering)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> QName)
-> (QName -> QName -> QName)
-> Ord QName
QName -> QName -> Bool
QName -> QName -> Ordering
QName -> QName -> QName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: QName -> QName -> Ordering
compare :: QName -> QName -> Ordering
$c< :: QName -> QName -> Bool
< :: QName -> QName -> Bool
$c<= :: QName -> QName -> Bool
<= :: QName -> QName -> Bool
$c> :: QName -> QName -> Bool
> :: QName -> QName -> Bool
$c>= :: QName -> QName -> Bool
>= :: QName -> QName -> Bool
$cmax :: QName -> QName -> QName
max :: QName -> QName -> QName
$cmin :: QName -> QName -> QName
min :: QName -> QName -> QName
Ord)

unqual :: QName -> Name
unqual :: QName -> Name
unqual (QName Name
n) = Name
n

instance Show QName where
  show :: QName -> String
show (Qual Name
m Name
n) = Name -> String
forall a. Show a => a -> String
show Name
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
  show (QName Name
n)  = Name -> String
forall a. Show a => a -> String
show Name
n

set0 :: Expr
set0 :: Expr
set0 = Expr -> Expr
Set Expr
Zero

ident :: Name -> Expr
ident :: Name -> Expr
ident Name
n = QName -> Expr
Ident (Name -> QName
QName Name
n)

-- | Concrete expressions syntax.
data Expr
  = Set Expr                        -- ^ Universe @Set e@; @Set@ for @Set 0@.
  | CoSet Expr
  | Size                            -- ^ @Size@ type of sizes.
  | Succ Expr                       -- ^ @$e@.
  | Zero                            -- ^ @0@.
  | Infty                           -- ^ @#@.
  | Max                             -- ^ @max@.
  | Plus Expr Expr                  -- ^ @e + e'@.
  | RApp Expr Expr                  -- ^ @e |> f@.
  | App Expr [Expr]                 -- ^ @f e1 ... en@ or @f <| e@.
  | Lam Name Expr                   -- ^ @\ x -> e@.
  | Case Expr (Maybe Type) [Clause] -- ^ @case e : A { cls }@.
  | LLet LetDef Expr                -- ^ @let x = e in e'@ local let.
  | Quant PiSigma Telescope Expr    -- ^ @(x : A) -> B@, @[x : A] -> B@, @(x : A) & B@.
  | Pair Expr Expr                  -- ^ @e , e'@.
  | Record [([Name],Expr)]          -- ^ @record { x = e, x' y = e' }@.
  | Proj Name                       -- ^ @.x@.
  | Ident QName                     -- ^ @x@ or @D.c@.
  | Unknown                         -- ^ @_@.
  | Sing Expr Expr                  -- ^ @<e : A>@ singleton type.
--  | EBind TBind Expr                -- ^ @[x : A] B@
  deriving (Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
/= :: Expr -> Expr -> Bool
Eq)

data LetDef = LetDef
  { LetDef -> Dec
letDefDec :: Dec
  , LetDef -> Name
letDefName :: Name
  , LetDef -> Telescope
letDefTel  ::  Telescope
  , LetDef -> Maybe Expr
letDefType :: (Maybe Type)
  , LetDef -> Expr
letDefExpr :: Expr
  } deriving (LetDef -> LetDef -> Bool
(LetDef -> LetDef -> Bool)
-> (LetDef -> LetDef -> Bool) -> Eq LetDef
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LetDef -> LetDef -> Bool
== :: LetDef -> LetDef -> Bool
$c/= :: LetDef -> LetDef -> Bool
/= :: LetDef -> LetDef -> Bool
Eq, Int -> LetDef -> ShowS
[LetDef] -> ShowS
LetDef -> String
(Int -> LetDef -> ShowS)
-> (LetDef -> String) -> ([LetDef] -> ShowS) -> Show LetDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LetDef -> ShowS
showsPrec :: Int -> LetDef -> ShowS
$cshow :: LetDef -> String
show :: LetDef -> String
$cshowList :: [LetDef] -> ShowS
showList :: [LetDef] -> ShowS
Show)

instance Show Expr where
    show :: Expr -> String
show = Expr -> String
prettyExpr

instance HasPred Expr where
  predecessor :: Expr -> Maybe Expr
predecessor (Succ Expr
e) = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
  predecessor Expr
_ = Maybe Expr
forall a. Maybe a
Nothing

data Declaration
  = DataDecl Name Sized Co Telescope Type [Constructor]
      [Name] -- list of field names
  | RecordDecl Name Telescope Type Constructor
      [Name] -- list of field names
  | FunDecl Co TypeSig [Clause]
  | LetDecl Bool LetDef -- True = if eval
--  | LetDecl Bool Name Telescope (Maybe Type) Expr -- True = if eval
  | PatternDecl Name [Name] Pattern
  | MutualDecl [Declaration]
  | OverrideDecl Override [Declaration] -- fail etc.
    deriving (Declaration -> Declaration -> Bool
(Declaration -> Declaration -> Bool)
-> (Declaration -> Declaration -> Bool) -> Eq Declaration
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Declaration -> Declaration -> Bool
== :: Declaration -> Declaration -> Bool
$c/= :: Declaration -> Declaration -> Bool
/= :: Declaration -> Declaration -> Bool
Eq,Int -> Declaration -> ShowS
[Declaration] -> ShowS
Declaration -> String
(Int -> Declaration -> ShowS)
-> (Declaration -> String)
-> ([Declaration] -> ShowS)
-> Show Declaration
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Declaration -> ShowS
showsPrec :: Int -> Declaration -> ShowS
$cshow :: Declaration -> String
show :: Declaration -> String
$cshowList :: [Declaration] -> ShowS
showList :: [Declaration] -> ShowS
Show)

data TypeSig = TypeSig Name Type
             deriving (TypeSig -> TypeSig -> Bool
(TypeSig -> TypeSig -> Bool)
-> (TypeSig -> TypeSig -> Bool) -> Eq TypeSig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypeSig -> TypeSig -> Bool
== :: TypeSig -> TypeSig -> Bool
$c/= :: TypeSig -> TypeSig -> Bool
/= :: TypeSig -> TypeSig -> Bool
Eq)

instance Show TypeSig where
  show :: TypeSig -> String
show (TypeSig Name
n Expr
t) = Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
t

type Type = Expr

data Constructor = Constructor
  { Constructor -> Name
conName :: Name
  , Constructor -> Telescope
conTel  :: Telescope
  , Constructor -> Maybe Expr
conType :: Maybe Type -- can be omitted *but* for families
  } deriving (Constructor -> Constructor -> Bool
(Constructor -> Constructor -> Bool)
-> (Constructor -> Constructor -> Bool) -> Eq Constructor
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Constructor -> Constructor -> Bool
== :: Constructor -> Constructor -> Bool
$c/= :: Constructor -> Constructor -> Bool
/= :: Constructor -> Constructor -> Bool
Eq)

instance Show Constructor where
  show :: Constructor -> String
show (Constructor Name
n Telescope
tel (Just Expr
t)) = Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Telescope -> String
forall a. Show a => a -> String
show Telescope
tel String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
t
  show (Constructor Name
n Telescope
tel  Maybe Expr
Nothing) = Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Telescope -> String
forall a. Show a => a -> String
show Telescope
tel

type TBind = TBinding Type
type LBind = TBinding (Maybe Type)  -- possibly domain-free

data TBinding a = TBind
  { forall a. TBinding a -> Dec
boundDec   :: Dec
  , forall a. TBinding a -> [Name]
boundNames :: [Name] -- [] if no name is given, then its a single bind
  , forall a. TBinding a -> a
boundType  :: a
  }
  | TBounded  -- bounded quantification
  { boundDec   :: Dec
  , forall a. TBinding a -> Name
boundName  :: Name -- [] if no name is given, then its a single bind
  , forall a. TBinding a -> LtLe
ltle       :: LtLe
  , forall a. TBinding a -> Expr
upperBound :: Expr
--  , boundMType :: Maybe Type -- type is inferred from upperBound
  }
  | TMeasure (Measure Expr)
  | TBound (Bound Expr)
--  | TSized { boundName :: Name } -- the size parameter of a sized record
    deriving (TBinding a -> TBinding a -> Bool
(TBinding a -> TBinding a -> Bool)
-> (TBinding a -> TBinding a -> Bool) -> Eq (TBinding a)
forall a. Eq a => TBinding a -> TBinding a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => TBinding a -> TBinding a -> Bool
== :: TBinding a -> TBinding a -> Bool
$c/= :: forall a. Eq a => TBinding a -> TBinding a -> Bool
/= :: TBinding a -> TBinding a -> Bool
Eq,Int -> TBinding a -> ShowS
[TBinding a] -> ShowS
TBinding a -> String
(Int -> TBinding a -> ShowS)
-> (TBinding a -> String)
-> ([TBinding a] -> ShowS)
-> Show (TBinding a)
forall a. Show a => Int -> TBinding a -> ShowS
forall a. Show a => [TBinding a] -> ShowS
forall a. Show a => TBinding a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> TBinding a -> ShowS
showsPrec :: Int -> TBinding a -> ShowS
$cshow :: forall a. Show a => TBinding a -> String
show :: TBinding a -> String
$cshowList :: forall a. Show a => [TBinding a] -> ShowS
showList :: [TBinding a] -> ShowS
Show)

type Telescope = [TBind]

data DefClause = DefClause
   Name         -- function identifier
   [Elim]
   (Maybe Expr) -- Nothing for absurd pattern clause
 deriving (DefClause -> DefClause -> Bool
(DefClause -> DefClause -> Bool)
-> (DefClause -> DefClause -> Bool) -> Eq DefClause
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DefClause -> DefClause -> Bool
== :: DefClause -> DefClause -> Bool
$c/= :: DefClause -> DefClause -> Bool
/= :: DefClause -> DefClause -> Bool
Eq,Int -> DefClause -> ShowS
[DefClause] -> ShowS
DefClause -> String
(Int -> DefClause -> ShowS)
-> (DefClause -> String)
-> ([DefClause] -> ShowS)
-> Show DefClause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DefClause -> ShowS
showsPrec :: Int -> DefClause -> ShowS
$cshow :: DefClause -> String
show :: DefClause -> String
$cshowList :: [DefClause] -> ShowS
showList :: [DefClause] -> ShowS
Show)

data Elim
  = EApp Pattern          -- application to a pattern
  | EProj Name [Pattern]  -- projection with arguments
    deriving (Elim -> Elim -> Bool
(Elim -> Elim -> Bool) -> (Elim -> Elim -> Bool) -> Eq Elim
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Elim -> Elim -> Bool
== :: Elim -> Elim -> Bool
$c/= :: Elim -> Elim -> Bool
/= :: Elim -> Elim -> Bool
Eq,Int -> Elim -> ShowS
[Elim] -> ShowS
Elim -> String
(Int -> Elim -> ShowS)
-> (Elim -> String) -> ([Elim] -> ShowS) -> Show Elim
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Elim -> ShowS
showsPrec :: Int -> Elim -> ShowS
$cshow :: Elim -> String
show :: Elim -> String
$cshowList :: [Elim] -> ShowS
showList :: [Elim] -> ShowS
Show)

data Clause = Clause
                (Maybe Name) -- Just funId | Nothing for case clauses
                [Pattern]
                (Maybe Expr) -- Nothing for absurd pattern clause
            deriving (Clause -> Clause -> Bool
(Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool) -> Eq Clause
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Clause -> Clause -> Bool
== :: Clause -> Clause -> Bool
$c/= :: Clause -> Clause -> Bool
/= :: Clause -> Clause -> Bool
Eq,Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> String
(Int -> Clause -> ShowS)
-> (Clause -> String) -> ([Clause] -> ShowS) -> Show Clause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Clause -> ShowS
showsPrec :: Int -> Clause -> ShowS
$cshow :: Clause -> String
show :: Clause -> String
$cshowList :: [Clause] -> ShowS
showList :: [Clause] -> ShowS
Show)

data Pattern
  = ConP Bool QName [Pattern] -- ^ @(c ps)@ if @False; @(.c ps)@ if @True@.
  | PairP Pattern Pattern     -- ^ @(p, p')@
  | SuccP Pattern             -- ^ @($ p)@
  | DotP Expr                 -- ^ @.e@
  | IdentP QName              -- ^ @x@ or @c@ or @D.c@.
  | SizeP Expr Name           -- ^ @(x > y)@ or @y < #@ or ...
  | AbsurdP                   -- ^ @()@
    deriving (Pattern -> Pattern -> Bool
(Pattern -> Pattern -> Bool)
-> (Pattern -> Pattern -> Bool) -> Eq Pattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pattern -> Pattern -> Bool
== :: Pattern -> Pattern -> Bool
$c/= :: Pattern -> Pattern -> Bool
/= :: Pattern -> Pattern -> Bool
Eq,Int -> Pattern -> ShowS
[Pattern] -> ShowS
Pattern -> String
(Int -> Pattern -> ShowS)
-> (Pattern -> String) -> ([Pattern] -> ShowS) -> Show Pattern
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Pattern -> ShowS
showsPrec :: Int -> Pattern -> ShowS
$cshow :: Pattern -> String
show :: Pattern -> String
$cshowList :: [Pattern] -> ShowS
showList :: [Pattern] -> ShowS
Show)

type Case = (Pattern,Expr)

-- | Used in Parser.
patApp :: Pattern -> [Pattern] -> Pattern
patApp :: Pattern -> [Pattern] -> Pattern
patApp (IdentP QName
c)         [Pattern]
ps' = Bool -> QName -> [Pattern] -> Pattern
ConP Bool
False  QName
c [Pattern]
ps'
patApp (ConP Bool
dotted QName
c [Pattern]
ps) [Pattern]
ps' = Bool -> QName -> [Pattern] -> Pattern
ConP Bool
dotted QName
c ([Pattern]
ps [Pattern] -> [Pattern] -> [Pattern]
forall a. [a] -> [a] -> [a]
++ [Pattern]
ps')

-- * Pretty printing.

prettyLBind :: LBind -> String
-- prettyLBind (TSized x)                   = prettyTBind False (TSized x)
prettyLBind :: LBind -> String
prettyLBind (TMeasure Measure Expr
mu)                = Bool -> TBind -> String
prettyTBind Bool
False (Measure Expr -> TBind
forall a. Measure Expr -> TBinding a
TMeasure Measure Expr
mu)
prettyLBind (TBound (Bound LtLe
ltle Measure Expr
mu Measure Expr
mu')) = Bool -> TBind -> String
prettyTBind Bool
False (Bound Expr -> TBind
forall a. Bound Expr -> TBinding a
TBound (LtLe -> Measure Expr -> Measure Expr -> Bound Expr
forall a. LtLe -> Measure a -> Measure a -> Bound a
Bound LtLe
ltle Measure Expr
mu Measure Expr
mu'))
prettyLBind (TBounded Dec
dec Name
x LtLe
ltle Expr
e)      = Bool -> TBind -> String
prettyTBind Bool
False (Dec -> Name -> LtLe -> Expr -> TBind
forall a. Dec -> Name -> LtLe -> Expr -> TBinding a
TBounded Dec
dec Name
x LtLe
ltle Expr
e)
prettyLBind (TBind Dec
dec [Name]
xs (Just Expr
t))      = Bool -> TBind -> String
prettyTBind Bool
False (Dec -> [Name] -> Expr -> TBind
forall a. Dec -> [Name] -> a -> TBinding a
TBind Dec
dec [Name]
xs Expr
t)
prettyLBind (TBind Dec
dec [Name]
xs Maybe Expr
Nothing) =
  if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then Bool -> ShowS
addPol Bool
False ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
brackets String
binding
   else Bool -> ShowS
addPol Bool
True String
binding
  where binding :: String
binding = String -> (Name -> String) -> [Name] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
" " Name -> String
forall a. Show a => a -> String
show [Name]
xs
        pol :: Pol
pol = Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity Dec
dec
        addPol :: Bool -> ShowS
addPol Bool
b String
x = if Pol
polPol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
==Pol
defaultPol
                      then String
x
                      else Pol -> String
forall a. Show a => a -> String
show Pol
pol String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
b then String
" " else String
"") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x


prettyTBind :: Bool -> TBind -> String
-- prettyTBind inPi (TSized x) = parens ("sized " ++ x)
prettyTBind :: Bool -> TBind -> String
prettyTBind Bool
inPi (TMeasure Measure Expr
mu) = String
"|" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  (String -> (Expr -> String) -> [Expr] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
","  Expr -> String
prettyExpr (Measure Expr -> [Expr]
forall a. Measure a -> [a]
measure Measure Expr
mu)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"
prettyTBind Bool
inPi (TBound (Bound LtLe
ltle Measure Expr
mu Measure Expr
mu')) = String
"|" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  (String -> (Expr -> String) -> [Expr] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
","  Expr -> String
prettyExpr (Measure Expr -> [Expr]
forall a. Measure a -> [a]
measure Measure Expr
mu))  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"| " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LtLe -> String
forall a. Show a => a -> String
show LtLe
ltle String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" |" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  (String -> (Expr -> String) -> [Expr] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
","  Expr -> String
prettyExpr (Measure Expr -> [Expr]
forall a. Measure a -> [a]
measure Measure Expr
mu')) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"
prettyTBind Bool
inPi (TBind Dec
dec [Name]
xs Expr
t) =
  if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then Bool -> ShowS
addPol Bool
False ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
brackets String
binding
   else if ([Name] -> Bool
forall a. Null a => a -> Bool
null [Name]
xs) then Bool -> ShowS
addPol Bool
True String
s
   else Bool -> ShowS
addPol (Bool -> Bool
not Bool
inPi) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (if Bool
inPi then ShowS
parens else ShowS
forall a. a -> a
id) String
binding
  where s :: String
s = Expr -> String
prettyExpr Expr
t
        binding :: String
binding = if [Name] -> Bool
forall a. Null a => a -> Bool
null [Name]
xs then String
s else
          (Name -> ShowS) -> String -> [Name] -> String
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Name
x String
s -> Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) (String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) [Name]
xs
        pol :: Pol
pol = Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity Dec
dec
        addPol :: Bool -> ShowS
addPol Bool
b String
x = if Pol
polPol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
==Pol
defaultPol
                      then String
x
                      else Pol -> String
forall a. Show a => a -> String
show Pol
pol String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
b then String
" " else String
"") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x
prettyTBind Bool
inPi (TBounded Dec
dec Name
x LtLe
ltle Expr
e) =
  if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then Bool -> ShowS
addPol Bool
False ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
brackets String
binding
   else Bool -> ShowS
addPol (Bool -> Bool
not Bool
inPi) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (if Bool
inPi then ShowS
parens else ShowS
forall a. a -> a
id) String
binding
  where binding :: String
binding = Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" < " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e
        pol :: Pol
pol = Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity Dec
dec
        addPol :: Bool -> ShowS
addPol Bool
b String
x = if Pol
polPol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
==Pol
defaultPol
                      then String
x
                      else Pol -> String
forall a. Show a => a -> String
show Pol
pol String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
b then String
" " else String
"") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x
{-
prettyTBind :: Bool -> TBind -> String
prettyTBind inPi (TBind dec x t) =
  if erased dec then addPol False $ brackets binding
   else if x=="" then addPol True s
   else addPol (not inPi) $ (if inPi then parens else id) binding
  where s = prettyExpr t
        binding = if x == "" then s else x ++ " : " ++ s
        pol = polarity dec
        addPol b x = if pol==Mixed then x
                      else show pol ++ (if b then " " else "") ++ x
-}
prettyLetBody :: String -> Expr -> String
prettyLetBody :: String -> Expr -> String
prettyLetBody String
s Expr
e = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e

prettyLetAssign :: String -> Expr -> String
prettyLetAssign :: String -> Expr -> String
prettyLetAssign String
s Expr
e = String
"let " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e

prettyLetDef :: LetDef -> String
prettyLetDef :: LetDef -> String
prettyLetDef (LetDef Dec
dec Name
n [] Maybe Expr
mt Expr
e) = String -> Expr -> String
prettyLetAssign (LBind -> String
prettyLBind LBind
tb) Expr
e
  where tb :: LBind
tb = Dec -> [Name] -> Maybe Expr -> LBind
forall a. Dec -> [Name] -> a -> TBinding a
TBind Dec
dec [Name
n] Maybe Expr
mt
prettyLetDef (LetDef Dec
dec Name
n Telescope
tel Maybe Expr
mt Expr
e) = String -> Expr -> String
prettyLetAssign String
s Expr
e
  where s :: String
s = Dec -> Name -> String
prettyDecId Dec
dec Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> Telescope -> String
prettyTel Bool
False Telescope
tel String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Expr -> String
prettyMaybeType Maybe Expr
mt

prettyDecId :: Dec -> Name -> String
prettyDecId :: Dec -> Name -> String
prettyDecId Dec
dec Name
x
  | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec = ShowS
brackets ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
x
  | Bool
otherwise  =
     let pol :: Pol
pol = Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity Dec
dec
     in  if Pol
pol Pol -> Pol -> Bool
forall a. Eq a => a -> a -> Bool
== Pol
defaultPol then Name -> String
forall a. Show a => a -> String
show Name
x else Pol -> String
forall a. Show a => a -> String
show Pol
pol String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x

prettyTel :: Bool -> Telescope -> String
prettyTel :: Bool -> Telescope -> String
prettyTel Bool
inPi = String -> (TBind -> String) -> Telescope -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
" " (Bool -> TBind -> String
prettyTBind Bool
inPi)

prettyMaybeType :: Maybe Expr -> String
prettyMaybeType :: Maybe Expr -> String
prettyMaybeType = String -> (Expr -> String) -> Maybe Expr -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ((Expr -> String) -> Maybe Expr -> String)
-> (Expr -> String) -> Maybe Expr -> String
forall a b. (a -> b) -> a -> b
$ \ Expr
t -> String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
t

prettyExpr :: Expr -> String
prettyExpr :: Expr -> String
prettyExpr Expr
e =
    case Expr
e of
      -- Type e          -> "Type " ++ prettyExpr e
      CoSet Expr
e         -> String
"CoSet " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e
      Set Expr
e         -> String
"CoSet " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e
      -- Set             -> "Set"
      Expr
Size            -> String
"Size"
      Expr
Max             -> String
"max"
      Succ Expr
e          -> String
"$ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e -- ++ ")"
      Expr
Zero            -> String
"0"
      Expr
Infty           -> String
"#"
      Plus Expr
e1 Expr
e2      -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++  Expr -> String
prettyExpr Expr
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      Pair Expr
e1 Expr
e2      -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" , " String -> ShowS
forall a. [a] -> [a] -> [a]
++  Expr -> String
prettyExpr Expr
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      App Expr
e1 [Expr]
el       -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Expr] -> String
prettyExprs (Expr
e1Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
el) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      Lam Name
x Expr
e1        -> String
"(\\" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      Case Expr
e Maybe Expr
Nothing [Clause]
cs -> String
"case " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" { " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (Clause -> String) -> [Clause] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
"; " Clause -> String
prettyCase [Clause]
cs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" } "
      Case Expr
e (Just Expr
t) [Clause]
cs -> String
"case " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" { " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (Clause -> String) -> [Clause] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
"; " Clause -> String
prettyCase [Clause]
cs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" } "
      LLet LetDef
letdef Expr
e -> String -> Expr -> String
prettyLetBody (LetDef -> String
prettyLetDef LetDef
letdef) Expr
e
{-
      LLet tb e1 e2 -> "(let " ++ prettyLBind tb ++ " = " ++ prettyExpr e1 ++ " in " ++ prettyExpr e2 ++ ")"
-}
      Record [([Name], Expr)]
rs       -> String
"record {" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (([Name], Expr) -> String) -> [([Name], Expr)] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
"; " ([Name], Expr) -> String
prettyRecordLine [([Name], Expr)]
rs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
      Proj Name
n          -> String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
      Ident QName
n         -> QName -> String
forall a. Show a => a -> String
show QName
n
      Expr
Unknown         -> String
"_"
      Sing Expr
e Expr
t        -> String
"<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
--      Quant pisig tb t2 -> parens $ prettyTBind True tb
      Quant PiSigma
pisig Telescope
tel Expr
t2 -> ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Bool -> Telescope -> String
prettyTel Bool
True Telescope
tel
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PiSigma -> String
forall a. Show a => a -> String
show PiSigma
pisig String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
t2

prettyRecordLine :: ([Name], Expr) -> String
prettyRecordLine :: ([Name], Expr) -> String
prettyRecordLine ([Name]
xs, Expr
e) = String -> (Name -> String) -> [Name] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
" " Name -> String
forall a. Show a => a -> String
show [Name]
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e

prettyCase :: Clause -> String
prettyCase :: Clause -> String
prettyCase (Clause Maybe Name
Nothing [Pattern
p] Maybe Expr
Nothing)  = Pattern -> String
prettyPattern Pattern
p
prettyCase (Clause Maybe Name
Nothing [Pattern
p] (Just Expr
e)) = Pattern -> String
prettyPattern Pattern
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e

prettyPattern :: Pattern -> String
prettyPattern :: Pattern -> String
prettyPattern (ConP Bool
dotted QName
c [Pattern]
ps) = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (String -> Pattern -> String) -> String -> [Pattern] -> String
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ String
acc Pattern
p -> String
acc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern -> String
prettyPattern Pattern
p) (if Bool
dotted then String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
c else QName -> String
forall a. Show a => a -> String
show QName
c) [Pattern]
ps
prettyPattern (PairP Pattern
p1 Pattern
p2) = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Pattern -> String
prettyPattern Pattern
p1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                Pattern -> String
prettyPattern Pattern
p2
prettyPattern (SuccP Pattern
p)   = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"$ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern -> String
prettyPattern Pattern
p
prettyPattern (DotP Expr
e)    = String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
prettyExpr Expr
e
prettyPattern (IdentP QName
x)  = QName -> String
forall a. Show a => a -> String
show QName
x
prettyPattern (SizeP Expr
e Name
y) = ShowS
parens ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Expr -> String
prettyExpr Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" > " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
y
prettyPattern (Pattern
AbsurdP)   = ShowS
parens String
""

prettyExprs :: [Expr] -> String
prettyExprs :: [Expr] -> String
prettyExprs = String -> (Expr -> String) -> [Expr] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
" " Expr -> String
prettyExpr

prettyDecl :: Declaration -> String
prettyDecl :: Declaration -> String
prettyDecl (PatternDecl Name
n [Name]
ns Pattern
p) = String
"pattern " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String -> (Name -> String) -> [Name] -> String
forall a. String -> (a -> String) -> [a] -> String
Util.showList String
" " Name -> String
forall a. Show a => a -> String
show (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern -> String
prettyPattern Pattern
p

teleToType :: Telescope -> Type -> Type
teleToType :: Telescope -> Expr -> Expr
teleToType [] Expr
t = Expr
t
teleToType (TBind
tb:Telescope
tel) Expr
t2 = PiSigma -> Telescope -> Expr -> Expr
Quant PiSigma
Pi [TBind
tb] (Telescope -> Expr -> Expr
teleToType Telescope
tel Expr
t2)
--teleToType (PosTB dec n t:tel) t2 = Pi dec n t (teleToType tel t2)

typeToTele :: Type -> (Telescope, Type)
typeToTele :: Expr -> (Telescope, Expr)
typeToTele (Quant PiSigma
Pi Telescope
tel0 Expr
c) =
  let (Telescope
tel, Expr
a) = Expr -> (Telescope, Expr)
typeToTele Expr
c in (Telescope
tel0 Telescope -> Telescope -> Telescope
forall a. [a] -> [a] -> [a]
++ Telescope
tel, Expr
a)
typeToTele Expr
a = ([],Expr
a)

{-
teleToType :: Telescope -> Type -> Type
teleToType [] t = t
teleToType (tb:tel) t2 = Quant Pi tb (teleToType tel t2)
--teleToType (PosTB dec n t:tel) t2 = Pi dec n t (teleToType tel t2)

typeToTele :: Type -> (Telescope, Type)
typeToTele = typeToTele' (-1)

typeToTele' :: Int -> Type -> (Telescope, Type)
typeToTele' k (Quant A.Pi tb c) | k /= 0 =
  let (tel, a) = typeToTele' (k-1) c in (tb:tel, a)
typeToTele' _ a = ([],a)
-}

teleNames :: Telescope -> [Name]
teleNames :: Telescope -> [Name]
teleNames Telescope
tel = [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Name]] -> [Name]) -> [[Name]] -> [Name]
forall a b. (a -> b) -> a -> b
$ (TBind -> [Name]) -> Telescope -> [[Name]]
forall a b. (a -> b) -> [a] -> [b]
map TBind -> [Name]
tbindNames Telescope
tel

tbindNames :: TBind -> [Name]
tbindNames :: TBind -> [Name]
tbindNames TBind{ [Name]
boundNames :: forall a. TBinding a -> [Name]
boundNames :: [Name]
boundNames }   = [Name]
boundNames
tbindNames TBounded{ Name
boundName :: forall a. TBinding a -> Name
boundName :: Name
boundName } = [Name
boundName]
-- tbindNames TSized{ boundName }   = [boundName]
tbindNames TBind
tb = String -> [Name]
forall a. HasCallStack => String -> a
error (String -> [Name]) -> String -> [Name]
forall a b. (a -> b) -> a -> b
$ String
"tbindNames (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TBind -> String
forall a. Show a => a -> String
show TBind
tb String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"