Make stack flags customizable in GNUmakefile.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Unit.hs

diff --git a/symantic-lib/Language/Symantic/Lib/Unit.hs b/symantic-lib/Language/Symantic/Lib/Unit.hs
index 6af27721fcc6a406d2a8c1e7dfce160b3014ec39..573afc294eb9431db91f39578698186ff3ca1915 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Unit.hs
+++ b/symantic-lib/Language/Symantic/Lib/Unit.hs
@@ -9,7 +9,7 @@ import Language.Symantic
 import Language.Symantic.Grammar
 
 -- * Class 'Sym_Unit'
-type instance Sym (Proxy ()) = Sym_Unit
+type instance Sym () = Sym_Unit
 class Sym_Unit term where
        unit :: term ()
        default unit :: Sym_Unit (UnT term) => Trans term => term ()
@@ -27,6 +27,8 @@ instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
 
 -- Typing
+instance NameTyOf () where
+       nameTyOf _c = [] `Mod` ""
 instance ClassInstancesFor () where
        proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
         | Just HRefl <- proj_ConstKiTy @_ @() z
@@ -46,23 +48,21 @@ instance
  ( Gram_Source src g
  , Gram_Rule g
  , Gram_Comment g
- , Inj_Sym ss ()
+ , SymInj ss ()
  ) => Gram_Term_AtomsFor src ss g () where
-       g_term_atomsFor _t =
+       g_term_atomsFor =
         [ rule "teUnit" $
-               g_source $
-               (\src -> BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teUnit)
+               source $
+               (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
                 <$ symbol "("
                 <* symbol ")"
         ]
 instance ModuleFor src ss ()
 
 -- ** 'Type's
-tyUnit :: Source src => Inj_Len vs => Type src vs ()
+tyUnit :: Source src => LenInj vs => Type src vs ()
 tyUnit = tyConst @(K ()) @()
 
 -- ** 'Term's
-teUnit ::
- Source src => Inj_Sym ss () =>
- Term src ss ts '[] ()
+teUnit :: TermDef () '[] (() #> ())
 teUnit = Term noConstraint tyUnit $ teSym @() $ unit