Unit type and fix for vars with location info

rzk/src/Language/Rzk/Free/Syntax.hs

@@ -14,6 +14,8 @@ module Language.Rzk.Free.Syntax where
 import           Data.Bifunctor.TH
 import           Data.Char           (chr, ord)
 import           Data.Coerce
+import           Data.Function       (on)
+import           Data.Functor        (void)
 import           Data.List           (nub, (\\))
 import           Data.String
 
@@ -22,6 +24,14 @@ import           Free.Scoped.TH
 
 import qualified Language.Rzk.Syntax as Rzk
 
+newtype VarIdent = VarIdent { getVarIdent :: Rzk.VarIdent }
+
+instance Eq VarIdent where
+  (==) = (==) `on` (void . getVarIdent)
+
+instance IsString VarIdent where
+  fromString s = VarIdent (Rzk.VarIdent Nothing (fromString s))
+
 data TermF scope term
     = UniverseF
     | UniverseCubeF
@@ -40,16 +50,18 @@ data TermF scope term
     | TopeOrF term term
     | RecBottomF
     | RecOrF [(term, term)]
-    | TypeFunF (Maybe Rzk.VarIdent) term (Maybe scope) scope
-    | TypeSigmaF (Maybe Rzk.VarIdent) term scope
+    | TypeFunF (Maybe VarIdent) term (Maybe scope) scope
+    | TypeSigmaF (Maybe VarIdent) term scope
     | TypeIdF term (Maybe term) term
     | AppF term term
-    | LambdaF (Maybe Rzk.VarIdent) (Maybe (term, Maybe scope)) scope
+    | LambdaF (Maybe VarIdent) (Maybe (term, Maybe scope)) scope
     | PairF term term
     | FirstF term
     | SecondF term
     | ReflF (Maybe (term, Maybe term))
     | IdJF term term term term term term
+    | UnitF
+    | TypeUnitF
     | TypeAscF term term
     | TypeRestrictedF term [(term, term)]
     deriving (Eq)
@@ -89,8 +101,8 @@ invalidateWHNF = transFS $ \(AnnF info f) ->
 substituteT :: TermT var -> Scope TermT var -> TermT var
 substituteT x = substitute x . invalidateWHNF
 
-type Term' = Term Rzk.VarIdent
-type TermT' = TermT Rzk.VarIdent
+type Term' = Term VarIdent
+type TermT' = TermT VarIdent
 
 freeVars :: Term a -> [a]
 freeVars = foldMap pure
@@ -118,24 +130,25 @@ freeVarsT typeOfVar t = go [] (partialFreeVarsT t)
 toTerm' :: Rzk.Term -> Term'
 toTerm' = toTerm Pure
 
-toScope :: Rzk.VarIdent -> (Rzk.VarIdent -> Term a) -> Rzk.Term -> Scope Term a
+toScope :: VarIdent -> (VarIdent -> Term a) -> Rzk.Term -> Scope Term a
 toScope x bvars = toTerm $ \z -> if x == z then Pure Z else S <$> bvars z
 
-toScopePattern :: Rzk.Pattern -> (Rzk.VarIdent -> Term a) -> Rzk.Term -> Scope Term a
+toScopePattern :: Rzk.Pattern -> (VarIdent -> Term a) -> Rzk.Term -> Scope Term a
 toScopePattern pat bvars = toTerm $ \z ->
   case lookup z (bindings pat (Pure Z)) of
     Just t  -> t
     Nothing -> S <$> bvars z
   where
-    bindings (Rzk.PatternWildcard _loc)   _ = []
-    bindings (Rzk.PatternVar _loc x)    t = [(x, t)]
+    bindings (Rzk.PatternWildcard _loc) _ = []
+    bindings (Rzk.PatternUnit _loc)     _ = []
+    bindings (Rzk.PatternVar _loc x)    t = [(VarIdent x, t)]
     bindings (Rzk.PatternPair _loc l r) t = bindings l (First t) <> bindings r (Second t)
 
-toTerm :: (Rzk.VarIdent -> Term a) -> Rzk.Term -> Term a
+toTerm :: (VarIdent -> Term a) -> Rzk.Term -> Term a
 toTerm bvars = go
   where
     go = \case
-      Rzk.Var _loc x -> bvars x
+      Rzk.Var _loc x -> bvars (VarIdent x)
       Rzk.Universe _loc -> Universe
 
       Rzk.UniverseCube _loc -> UniverseCube
@@ -156,6 +169,8 @@ toTerm bvars = go
       Rzk.RecOr _loc rs -> RecOr [ (go tope, go term) | Rzk.Restriction _loc tope term <- rs ]
       Rzk.TypeId _loc x tA y -> TypeId (go x) (Just (go tA)) (go y)
       Rzk.TypeIdSimple _loc x y -> TypeId (go x) Nothing (go y)
+      Rzk.TypeUnit _loc -> TypeUnit
+      Rzk.Unit _loc -> Unit
       Rzk.App _loc f x -> App (go f) (go x)
       Rzk.Pair _loc l r -> Pair (go l) (go r)
       Rzk.First _loc term -> First (go term)
@@ -196,20 +211,20 @@ toTerm bvars = go
       Rzk.Hole _loc _ident -> error "holes are not supported"
 
 
-    patternVar (Rzk.PatternVar _loc x) = Just x
+    patternVar (Rzk.PatternVar _loc x) = Just (VarIdent x)
     patternVar _                       = Nothing
 
 fromTerm' :: Term' -> Rzk.Term
 fromTerm' t = fromTermWith' vars (defaultVarIdents \\ vars) t
   where vars = freeVars t
 
-fromScope' :: Rzk.VarIdent -> [Rzk.VarIdent] -> [Rzk.VarIdent] -> Scope Term Rzk.VarIdent -> Rzk.Term
-fromScope' x used xs = fromTermWith' (x : used) xs . (>>= f)
+fromScope' :: Rzk.VarIdent -> [VarIdent] -> [VarIdent] -> Scope Term VarIdent -> Rzk.Term
+fromScope' x used xs = fromTermWith' (VarIdent x : used) xs . (>>= fmap VarIdent . f . fmap getVarIdent)
   where
     f Z     = Pure x
     f (S z) = Pure z
 
-fromTermWith' :: [Rzk.VarIdent] -> [Rzk.VarIdent] -> Term' -> Rzk.Term
+fromTermWith' :: [VarIdent] -> [VarIdent] -> Term' -> Rzk.Term
 fromTermWith' used vars = go
   where
     withFresh Nothing f =
@@ -221,8 +236,10 @@ fromTermWith' used vars = go
         z' = refreshVar used z
 
     loc = Nothing
+
+    go :: Term' -> Rzk.Term
     go = \case
-      Pure z -> Rzk.Var loc z
+      Pure z -> Rzk.Var loc (getVarIdent z)
 
       Universe -> Rzk.Universe loc
       UniverseCube -> Rzk.UniverseCube loc
@@ -242,28 +259,30 @@ fromTermWith' used vars = go
       RecBottom -> Rzk.RecBottom loc
       RecOr rs -> Rzk.RecOr loc [ Rzk.Restriction loc (go tope) (go term) | (tope, term) <- rs ]
 
-      TypeFun z arg Nothing ret -> withFresh z $ \(x, xs) ->
+      TypeFun z arg Nothing ret -> withFresh z $ \(VarIdent x, xs) ->
         Rzk.TypeFun loc (Rzk.ParamVarType loc (Rzk.PatternVar loc x) (go arg)) (fromScope' x used xs ret)
-      TypeFun z arg (Just tope) ret -> withFresh z $ \(x, xs) ->
+      TypeFun z arg (Just tope) ret -> withFresh z $ \(VarIdent x, xs) ->
         Rzk.TypeFun loc (Rzk.ParamVarShape loc (Rzk.PatternVar loc x) (go arg) (fromScope' x used xs tope)) (fromScope' x used xs ret)
 
-      TypeSigma z a b -> withFresh z $ \(x, xs) ->
+      TypeSigma z a b -> withFresh z $ \(VarIdent x, xs) ->
         Rzk.TypeSigma loc (Rzk.PatternVar loc x) (go a) (fromScope' x used xs b)
       TypeId l (Just tA) r -> Rzk.TypeId loc (go l) (go tA) (go r)
       TypeId l Nothing r -> Rzk.TypeIdSimple loc (go l) (go r)
       App l r -> Rzk.App loc (go l) (go r)
 
-      Lambda z Nothing scope -> withFresh z $ \(x, xs) ->
+      Lambda z Nothing scope -> withFresh z $ \(VarIdent x, xs) ->
         Rzk.Lambda loc [Rzk.ParamPattern loc (Rzk.PatternVar loc x)] (fromScope' x used xs scope)
-      Lambda z (Just (ty, Nothing)) scope -> withFresh z $ \(x, xs) ->
+      Lambda z (Just (ty, Nothing)) scope -> withFresh z $ \(VarIdent x, xs) ->
         Rzk.Lambda loc [Rzk.ParamPatternType loc [Rzk.PatternVar loc x] (go ty)] (fromScope' x used xs scope)
-      Lambda z (Just (cube, Just tope)) scope -> withFresh z $ \(x, xs) ->
+      Lambda z (Just (cube, Just tope)) scope -> withFresh z $ \(VarIdent x, xs) ->
         Rzk.Lambda loc [Rzk.ParamPatternShape loc (Rzk.PatternVar loc x) (go cube) (fromScope' x used xs tope)] (fromScope' x used xs scope)
       -- Lambda (Maybe (term, Maybe scope)) scope -> Rzk.Lambda loc (Maybe (term, Maybe scope)) scope
 
       Pair l r -> Rzk.Pair loc (go l) (go r)
       First term -> Rzk.First loc (go term)
       Second term -> Rzk.Second loc (go term)
+      TypeUnit -> Rzk.TypeUnit loc
+      Unit -> Rzk.Unit loc
       Refl Nothing -> Rzk.Refl loc
       Refl (Just (t, Nothing)) -> Rzk.ReflTerm loc (go t)
       Refl (Just (t, Just ty)) -> Rzk.ReflTermType loc (go t) (go ty)
@@ -272,9 +291,9 @@ fromTermWith' used vars = go
       TypeRestricted ty rs ->
         Rzk.TypeRestricted loc (go ty) (map (\(tope, term) -> (Rzk.Restriction loc (go tope) (go term))) rs)
 
-defaultVarIdents :: [Rzk.VarIdent]
+defaultVarIdents :: [VarIdent]
 defaultVarIdents =
-  [ Rzk.VarIdent Nothing (Rzk.VarIdentToken name)
+  [ VarIdent (Rzk.VarIdent Nothing (Rzk.VarIdentToken name))
   | n <- [1..]
   , let name = "x" <> map digitToSub (show n) ]
   where
@@ -285,14 +304,14 @@ defaultVarIdents =
 --
 -- >>> refreshVar ["x", "y", "x₁", "z"] "x"
 -- x₂
-refreshVar :: [Rzk.VarIdent] -> Rzk.VarIdent -> Rzk.VarIdent
+refreshVar :: [VarIdent] -> VarIdent -> VarIdent
 refreshVar vars x
   | x `elem` vars = refreshVar vars (incVarIdentIndex x)
   | otherwise     = x
 
-incVarIdentIndex :: Rzk.VarIdent -> Rzk.VarIdent
-incVarIdentIndex (Rzk.VarIdent loc token) =
-  Rzk.VarIdent loc (coerce incIndex token)
+incVarIdentIndex :: VarIdent -> VarIdent
+incVarIdentIndex (VarIdent (Rzk.VarIdent loc token)) =
+  VarIdent (Rzk.VarIdent loc (coerce incIndex token))
 
 -- | Increment the subscript number at the end of the indentifier.
 --

rzk/src/Language/Rzk/Syntax.cf

@@ -57,6 +57,7 @@ SomeSectionName.  SectionName ::= VarIdent ;
 
 -- Patterns
 PatternWildcard.  Pattern ::= "_" ;
+PatternUnit.      Pattern ::= "unit" ;
 PatternVar.       Pattern ::= VarIdent ;
 PatternPair.      Pattern ::= "(" Pattern "," Pattern ")" ;
 separator nonempty Pattern "" ;
@@ -106,6 +107,7 @@ define recOr psi phi a b = RecOr [ Restriction psi a, Restriction phi b ] ;
 -- Types
 TypeFun.        Term1 ::= ParamDecl "->" Term1 ;
 TypeSigma.      Term1 ::= "Sigma" "(" Pattern ":" Term ")" "," Term1 ;
+TypeUnit.       Term1 ::= "Unit" ;
 TypeId.         Term1 ::= Term2 "=_{" Term "}" Term2 ;
 TypeIdSimple.   Term1 ::= Term2 "=" Term2 ;
 TypeRestricted. Term6  ::= Term6 "[" [Restriction] "]" ;
@@ -117,6 +119,7 @@ Lambda.         Term1 ::= "\\" [Param] "->" Term1 ;
 Pair.           Term7 ::= "(" Term "," Term ")" ;
 First.          Term6 ::= "first" Term7 ;
 Second.         Term6 ::= "second" Term7 ;
+Unit.           Term7 ::= "unit" ;
 Refl.           Term7 ::= "refl";
 ReflTerm.       Term7 ::= "refl_{" Term "}" ;
 ReflTermType.   Term7 ::= "refl_{" Term ":" Term "}" ;

rzk/src/Language/Rzk/Syntax/Abs.hs

@@ -69,6 +69,7 @@ data SectionName' a
 type Pattern = Pattern' BNFC'Position
 data Pattern' a
     = PatternWildcard a
+    | PatternUnit a
     | PatternVar a (VarIdent' a)
     | PatternPair a (Pattern' a) (Pattern' a)
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
@@ -113,6 +114,7 @@ data Term' a
     | RecOr a [Restriction' a]
     | TypeFun a (ParamDecl' a) (Term' a)
     | TypeSigma a (Pattern' a) (Term' a) (Term' a)
+    | TypeUnit a
     | TypeId a (Term' a) (Term' a) (Term' a)
     | TypeIdSimple a (Term' a) (Term' a)
     | TypeRestricted a (Term' a) [Restriction' a]
@@ -121,6 +123,7 @@ data Term' a
     | Pair a (Term' a) (Term' a)
     | First a (Term' a)
     | Second a (Term' a)
+    | Unit a
     | Refl a
     | ReflTerm a (Term' a)
     | ReflTermType a (Term' a) (Term' a)
@@ -238,6 +241,7 @@ instance HasPosition SectionName where
 instance HasPosition Pattern where
   hasPosition = \case
     PatternWildcard p -> p
+    PatternUnit p -> p
     PatternVar p _ -> p
     PatternPair p _ _ -> p
 
@@ -279,6 +283,7 @@ instance HasPosition Term where
     RecOr p _ -> p
     TypeFun p _ _ -> p
     TypeSigma p _ _ _ -> p
+    TypeUnit p -> p
     TypeId p _ _ _ -> p
     TypeIdSimple p _ _ -> p
     TypeRestricted p _ _ -> p
@@ -287,6 +292,7 @@ instance HasPosition Term where
     Pair p _ _ -> p
     First p _ -> p
     Second p _ -> p
+    Unit p -> p
     Refl p -> p
     ReflTerm p _ -> p
     ReflTermType p _ _ -> p

rzk/src/Language/Rzk/Syntax/Doc.txt

@@ -33,9 +33,10 @@ The set of reserved words is the set of terminals appearing in the grammar. Thos
 
 The reserved words used in Syntax are the following:
   | ``BOT`` | ``CUBE`` | ``Sigma`` | ``TOP``
-  | ``TOPE`` | ``U`` | ``as`` | ``first``
-  | ``idJ`` | ``recBOT`` | ``recOR`` | ``refl``
-  | ``second`` | ``uses`` | ``Σ`` |
+  | ``TOPE`` | ``U`` | ``Unit`` | ``as``
+  | ``first`` | ``idJ`` | ``recBOT`` | ``recOR``
+  | ``refl`` | ``second`` | ``unit`` | ``uses``
+  | ``Σ`` |  |  |
 
 The symbols used in Syntax are the following:
   | #lang | ; | rzk-1 | #set-option
@@ -90,6 +91,7 @@ All other symbols are terminals.
   | //SectionName// | -> | **eps**
   |  |  **|**  | //VarIdent//
   | //Pattern// | -> | ``_``
+  |  |  **|**  | ``unit``
   |  |  **|**  | //VarIdent//
   |  |  **|**  | ``(`` //Pattern// ``,`` //Pattern// ``)``
   | //[Pattern]// | -> | //Pattern//
@@ -123,6 +125,7 @@ All other symbols are terminals.
   |  |  **|**  | ``recOR`` ``(`` //Term// ``,`` //Term// ``,`` //Term// ``,`` //Term// ``)``
   |  |  **|**  | ``<`` //ParamDecl// ``->`` //Term// ``>``
   |  |  **|**  | ``(`` //Term// ``,`` //Term// ``)``
+  |  |  **|**  | ``unit``
   |  |  **|**  | ``refl``
   |  |  **|**  | ``refl_{`` //Term// ``}``
   |  |  **|**  | ``refl_{`` //Term// ``:`` //Term// ``}``
@@ -141,6 +144,7 @@ All other symbols are terminals.
   |  |  **|**  | //Term3//
   | //Term1// | -> | //ParamDecl// ``->`` //Term1//
   |  |  **|**  | ``Sigma`` ``(`` //Pattern// ``:`` //Term// ``)`` ``,`` //Term1//
+  |  |  **|**  | ``Unit``
   |  |  **|**  | //Term2// ``=_{`` //Term// ``}`` //Term2//
   |  |  **|**  | //Term2// ``=`` //Term2//
   |  |  **|**  | ``\`` //[Param]// ``->`` //Term1//

rzk/src/Language/Rzk/Syntax/Layout.hs

@@ -42,11 +42,11 @@ layoutSep   = List.nub $ TokSymbol ";" 29 : map (delimSep . snd) layoutWords
 parenOpen, parenClose :: [TokSymbol]
 parenOpen  =
   [ TokSymbol "(" 16
-  , TokSymbol "[" 42
+  , TokSymbol "[" 43
   ]
 parenClose =
   [ TokSymbol ")" 17
-  , TokSymbol "]" 45
+  , TokSymbol "]" 46
   ]
 
 -- | Report an error during layout resolution.

rzk/src/Language/Rzk/Syntax/Lex.hs

@@ -321,38 +321,38 @@ eitherResIdent tv s = treeFind resWords
 -- | The keywords and symbols of the language organized as binary search tree.
 resWords :: BTree
 resWords =
-  b "=" 32
-    (b "(" 16
-       (b "#end" 8
-          (b "#compute-nf" 4
-             (b "#check" 2 (b "#assume" 1 N N) (b "#compute" 3 N N))
-             (b "#def" 6 (b "#compute-whnf" 5 N N) (b "#define" 7 N N)))
-          (b "#set-option" 12
-             (b "#postulate" 10 (b "#lang" 9 N N) (b "#section" 11 N N))
-             (b "#variable" 14
-                (b "#unset-option" 13 N N) (b "#variables" 15 N N))))
-       (b "1" 24
-          (b "," 20
-             (b "*" 18 (b ")" 17 N N) (b "*_1" 19 N N))
-             (b "/\\" 22 (b "->" 21 N N) (b "0_2" 23 N N)))
-          (b ":=" 28
-             (b "2" 26 (b "1_2" 25 N N) (b ":" 27 N N))
-             (b "<" 30 (b ";" 29 N N) (b "<=" 31 N N)))))
-    (b "first" 48
-       (b "TOPE" 40
-          (b "BOT" 36
-             (b "=_{" 34 (b "===" 33 N N) (b ">" 35 N N))
-             (b "Sigma" 38 (b "CUBE" 37 N N) (b "TOP" 39 N N)))
-          (b "\\/" 44
-             (b "[" 42 (b "U" 41 N N) (b "\\" 43 N N))
-             (b "_" 46 (b "]" 45 N N) (b "as" 47 N N))))
-       (b "uses" 56
-          (b "refl" 52
-             (b "recBOT" 50 (b "idJ" 49 N N) (b "recOR" 51 N N))
-             (b "rzk-1" 54 (b "refl_{" 53 N N) (b "second" 55 N N)))
-          (b "}" 60
-             (b "|" 58 (b "{" 57 N N) (b "|->" 59 N N))
-             (b "\8594" 62 (b "\931" 61 N N) (b "\8721" 63 N N)))))
+  b "===" 33
+    (b ")" 17
+       (b "#lang" 9
+          (b "#compute-whnf" 5
+             (b "#compute" 3
+                (b "#check" 2 (b "#assume" 1 N N) N) (b "#compute-nf" 4 N N))
+             (b "#define" 7 (b "#def" 6 N N) (b "#end" 8 N N)))
+          (b "#unset-option" 13
+             (b "#section" 11 (b "#postulate" 10 N N) (b "#set-option" 12 N N))
+             (b "#variables" 15 (b "#variable" 14 N N) (b "(" 16 N N))))
+       (b "1_2" 25
+          (b "->" 21
+             (b "*_1" 19 (b "*" 18 N N) (b "," 20 N N))
+             (b "0_2" 23 (b "/\\" 22 N N) (b "1" 24 N N)))
+          (b ";" 29
+             (b ":" 27 (b "2" 26 N N) (b ":=" 28 N N))
+             (b "<=" 31 (b "<" 30 N N) (b "=" 32 N N)))))
+    (b "idJ" 50
+       (b "Unit" 42
+          (b "Sigma" 38
+             (b "BOT" 36 (b ">" 35 (b "=_{" 34 N N) N) (b "CUBE" 37 N N))
+             (b "TOPE" 40 (b "TOP" 39 N N) (b "U" 41 N N)))
+          (b "]" 46
+             (b "\\" 44 (b "[" 43 N N) (b "\\/" 45 N N))
+             (b "as" 48 (b "_" 47 N N) (b "first" 49 N N))))
+       (b "uses" 58
+          (b "refl_{" 54
+             (b "recOR" 52 (b "recBOT" 51 N N) (b "refl" 53 N N))
+             (b "second" 56 (b "rzk-1" 55 N N) (b "unit" 57 N N)))
+          (b "}" 62
+             (b "|" 60 (b "{" 59 N N) (b "|->" 61 N N))
+             (b "\8594" 64 (b "\931" 63 N N) (b "\8721" 65 N N)))))
   where
   b s n = B bs (TS bs n)
     where