


{-# LANGUAGE OverloadedStrings #-}




-- |
-- Copyright :  (c) Andreas Reuleaux 2015
-- License   :  BSD2
-- Maintainer:  Andreas Reuleaux <rx@a-rx.info>
-- Stability :  experimental
-- Portability: non-portable
--
-- This module provides Pire's syntax,
-- ie. Pire's flavour of Pi-forall syntax: smart constructors, and destructors



module Pire.Syntax.Smart where


import Bound
import Bound.Name


import Data.List


import Pire.Syntax.Expr
import Pire.Syntax.Ws
import Pire.Syntax.Token
import Pire.Syntax.Binder


-- smart constructors



-- |
-- >>> lam "x" $ V "x"
-- Lam "x" (Scope (V (B ())))
-- >>> lam "x" $ V "f" :@ V "x"
-- Lam "x" (Scope (V (F (V "f")) :@ V (B ())))
-- >>> lam "y" $ lam "x" $ V "x" :@ V "y"
-- Lam "y" (Scope (Lam "x" (Scope (V (B ()) :@ V (F (V (B ())))))))
-- >>> lam "y" $ lam "x" $ V "x" :@ (V "y" :@ V "z")
-- Lam "y" (Scope (Lam "x" (Scope (V (B ()) :@ (V (F (V (B ()))) :@ V (F (V (F (V "z")))))))))

lam v b = Lam v (abstract1 v b)


-- doctests missing
elam v e = ErasedLam v (abstract1 v e)


-- |
-- >>> lam_ "x" $ (Ws_ (V "b") $ Ws "{-foo-}")
-- Lam_ (LamTok "\\" NoWs) (Binder "x") (Dot "." NoWs) (Scope (Ws_ (V (F (V "b"))) (Ws "{-foo-}")))

lam_ v e = Lam_ (LamTok "\\" NoWs) (Binder v) (Dot "." $ NoWs) (abstract1 v e)






-- |
-- >>> lam' "x" $ V "x"
-- Lam' "x" (Scope (V (B (Name "x" ()))))
-- >>> lam' "x" $ V "f" :@ V "x"
-- Lam' "x" (Scope (V (F (V "f")) :@ V (B (Name "x" ()))))
-- >>> lam' "y" $ lam' "x" $ V "x" :@ V "y"
-- Lam' "y" (Scope (Lam' "x" (Scope (V (B (Name "x" ())) :@ V (F (V (B (Name "y" ()))))))))

lam' v b = Lam' v (abstract1Name v b)






-- |
-- >>> lams ["x", "y"] $ V "z" :@ V "x"
-- Lams ["x","y"] (Scope (V (F (V "z")) :@ V (B 0)))
-- >>> lams ["x", "y"] $ lams ["a", "b"] $ V "x" :@ V "a"
-- Lams ["x","y"] (Scope (Lams ["a","b"] (Scope (V (F (V (B 0))) :@ V (B 0)))))

lams ls b = Lams ls $ abstract (`elemIndex` ls) b



-- |
-- >>> lams_ ["x", "y"] $ V "z" :@ V "x"
-- Lams_ (LamTok "\\" NoWs) [Binder "x",Binder "y"] (Dot "." NoWs) (Scope (V (F (V "z")) :@ V (B 0)))
-- >>> lams_ ["x", "y"] $ (Ws_ (V "b") $ Ws "{-foo-}")
-- Lams_ (LamTok "\\" NoWs) [Binder "x",Binder "y"] (Dot "." NoWs) (Scope (Ws_ (V (F (V "b"))) (Ws "{-foo-}")))


lams_ vs b = Lams_ (LamTok "\\" $ NoWs) [Binder v | v <- vs] (Dot "." NoWs) $ abstract (`elemIndex` vs) b




-- |
-- >>> lams' ["x", "y"] $ V "z" :@ V "x"
-- Lams' ["x","y"] (Scope (V (F (V "z")) :@ V (B (Name "x" 0))))

lams' ls b = Lams' ls $ abstractName (`elemIndex` ls) b





-- -- smart destructors


scope (Lam _ s)      = s
scope (Lam_ _ _ _ s) = s
scope (Pi _ _ s)     = s


-- plural (Int index) version of the above
scopepl (Lams _ s)        = s
scopepl (Lams_ _ _ _ s)   = s
scopepl (LamPAs _ s)      = s
scopepl (LamPAs_ _ _ _ s)      = s




-- scopes w/ Name's
scope' (Lam' _ s) = s
scopepl' (Lams' _ s) = s




