{-# LANGUAGE LambdaCase #-}

{-# OPTIONS_GHC -fno-warn-typed-holes #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

-- | Auxiliary functions for abstract syntax.

module Abstract where

import Control.Monad

import Sit.Abs as A

import Lens

-- data AppView
--   = FixV [Exp]
--   | SetV [Exp]
--   | VarV [Exp]
--   | ZeroV [Exp]
--   | SucV  [Exp]

-- | Gather applications to expose head.

appView :: Exp -> (Exp, [Exp])
appView :: Exp -> (Exp, [Exp])
appView = \case
  App Exp
f Exp
e -> Lens (Exp, [Exp]) [Exp]
-> ([Exp] -> [Exp]) -> (Exp, [Exp]) -> (Exp, [Exp])
forall a b. Lens a b -> (b -> b) -> a -> a
over Lens (Exp, [Exp]) [Exp]
forall a b. Lens (a, b) b
_2 ([Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
++ [Exp
e]) ((Exp, [Exp]) -> (Exp, [Exp])) -> (Exp, [Exp]) -> (Exp, [Exp])
forall a b. (a -> b) -> a -> b
$ Exp -> (Exp, [Exp])
appView Exp
f
  Exp
e -> (Exp
e, [])

-- | Can this expression only denote a type?

mustBeType :: Exp -> Bool
mustBeType :: Exp -> Bool
mustBeType = \case
  Exp
Nat      -> Bool
True
  Exp
Set      -> Bool
True
  Exp
Set1     -> Bool
True
  Exp
Set2     -> Bool
True
  Forall{} -> Bool
True
  Pi{}     -> Bool
True
  Arrow{}  -> Bool
True
  App Exp
f Exp
_  -> Exp -> Bool
mustBeType Exp
f
  Exp
_ -> Bool
False

-- | Is this expression an introduction?

introduction :: Exp -> Bool
introduction :: Exp -> Bool
introduction = \case
  Var{}    -> Bool
False
  App{}    -> Bool
False
  Case{}   -> Bool
False
  Int{}    -> Bool
True
  Exp
Infty    -> Bool
True
  Exp
Size     -> Bool
True
  Exp
Nat      -> Bool
True
  Exp
Set      -> Bool
True
  Exp
Set1     -> Bool
True
  Exp
Set2     -> Bool
True
  Exp
Zero     -> Bool
True
  Exp
Suc      -> Bool
True
  Exp
Fix      -> Bool
True
  Exp
LZero    -> Bool
True
  Exp
LSuc     -> Bool
True
  Lam{}    -> Bool
True
  Forall{} -> Bool
True
  Pi{}     -> Bool
True
  Arrow{}  -> Bool
True
  Plus{}   -> Bool
True
  ELam{}   -> Bool
True

-- | Convert "identifier-or-underscore" to string.

fromIdU :: A.IdU -> String
fromIdU :: IdU -> String
fromIdU = \case
  A.Id (A.Ident String
x) -> String
x
  IdU
A.Under -> String
"_"

-- | Try to convert an expression to a list of A.IdU

parseIdUs :: A.Exp -> Maybe [A.IdU]
parseIdUs :: Exp -> Maybe [IdU]
parseIdUs Exp
e = do
  let (Exp
f, [Exp]
es) = Exp -> (Exp, [Exp])
appView Exp
e
  [Exp] -> (Exp -> Maybe IdU) -> Maybe [IdU]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Exp
f Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
es) ((Exp -> Maybe IdU) -> Maybe [IdU])
-> (Exp -> Maybe IdU) -> Maybe [IdU]
forall a b. (a -> b) -> a -> b
$ \case
    A.Var IdU
x -> IdU -> Maybe IdU
forall a. a -> Maybe a
Just IdU
x
    Exp
_ -> Maybe IdU
forall a. Maybe a
Nothing