ml71 rides again!

README.md

@@ -131,14 +131,15 @@ or an output place governed by a one-subject postcondition can be replaced by
 the condition itself. For (thank goodness) example:
 
 ````
-type {T}
-{type T] :> {t}
-(e) <: [type S}
+judgement type {T}
+judgement {type T] :> {t}
+judgement (e) <: [type S}
 ````
 
-The above specifies three judgement forms (there should probably be some keyword).
+The above specifies three judgement forms.
 The first has but a subject, a term, which we are judging to be a type.
 The second also judges a term, with respect to another term already required to be
 a type.
 The third judges a usage, yielding a term which is promised to be a type.
 
+

src/Ch.hs

@@ -212,7 +212,7 @@ judge thy ga (Ju js)
     ga' = shlCx ga n <> ((fmap . stb) <$> bwdPos <*> de)
 judge thy ga (Eq js) = case fmap shy js of
     js | Just (i, js) <- jigJ varqq Nothing js
-       -> judge thy ga (Ju js)
+       -> if null [() | O _ <- js] then return [] else judge thy ga (Ju js)
        | Just (_, js) <- jigJ eliqq Nothing js
        -> ju js
        | otherwise
@@ -303,7 +303,7 @@ ml71 = Theory
   { typingRules =
     [ [ B0 :- PJu [S (Sj (Syy :?: "e")), X "<:", O (Chy :<: pA TY)]
       ] :-----:
-      [X "type", S (Chy :<: pY "e")]
+      [X "type", S (Chy :<: pE "e")]
 
     , [
       ] :-----:
@@ -317,7 +317,7 @@ ml71 = Theory
     , [ B0 :- PJu [S (Sj (Syy :?: "e")), X "<:", O (Chy :<: pH "S")]
       , B0 :- PEq [X "type", S (Chy :>=: ((Chy :?: "S") %- [], (Chy :?: "T") %- []))]
       ] :-----:
-      [I (Chy :<: pH "T"), X ":>", S (Chy :<: pY "e")]
+      [I (Chy :<: pH "T"), X ":>", S (Chy :<: pE "e")]
 
     , [ B0 :- PJu [X "type", S (Sj (Chy :?: "T"))]
       ] :-----:
@@ -328,15 +328,29 @@ ml71 = Theory
       ] :-----:
       [I (Chy :<: (PI ?- [pH "S", pS (pH "T")])), X ":>", S (Chy :<: pS (pH "t"))]
 
+    , [ B0 :- PJu [S (Sj (Syy :?: "e")), X "<:", O (Chy :<: (PI ?- [pH "S", pS (pH "T")]))]
+      , B0 :- PJu [I (Chy :>: ((Chy :?: "S") %- [])), X ":>", S (Sj (Chy :?: "s"))]
+      ] :-----:
+      [ S (Syy :<: pE "e"), S (Chy :<: pH "s")
+      , X "<:"
+      , O (Chy :>: ((Chy :?: "T") %- [((Chy :?: "s") %- []) <:> ((Chy :?: "s") %- [])]))
+      ]
+
+    , [ B0 :- PJu [X "type", S (Sj (Chy :?: "T"))]
+      , B0 :- PJu [I (Chy :>: ((Chy :?: "T") %- [])), X ":>", S (Sj (Chy :?: "t"))]
+      ] :-----:
+      [S (Chy :<: pH "t"), X ":", S (Chy :<: pH "T"), X "<:", O (Chy :>: ((Chy :?: "T") %- []))]
     ]
   , betaRules =
-    [
+    [(PI ?- [pH "S", pS (pH "T")]) :~> pS (pH "t") :~> pH "s" :~>
+     let sS = ((Chy :?: "s") %- []) <:> ((Chy :?: "S") %- []) in
+     ((Chy :?: "t") %- [sS], (Chy :?: "T") %- [sS])
     ]
   }
 
 tests :: [Maybe (Env (TmT NoMeta))]
 tests = map (judge ml71 B0 . Ju)
-  [ [X "type", S (Chy :>: (PI $- [tA TY, tS (tA TY)]))]
+  [{- [X "type", S (Chy :>: (PI $- [tA TY, tS (tA TY)]))]
   , [X "type", S (Chy :>: (PI $- [tA TY, tS (PI $- [tV 0, tS (tV 1)])]))]
   , [I (Chy :>: tA TY), X ":>", S (Chy :>: tA TY)]
   , [I (Chy :>: (PI $- [tA TY, tS (tA TY)])), X ":>", S (Chy :>: tS (tA TY))]
@@ -345,6 +359,20 @@ tests = map (judge ml71 B0 . Ju)
     , X ":>"
     , S (Chy :>: tS (tS (tV 0)))
     ]
+  , [I (Chy :>: (PI $- [tA TY, tS
+                   (PI $- [PI $- [tV 0, tS (tV 1)], tS
+                    (PI $- [tV 1, tS
+                     (tV 2)])])]))
+    , X ":>"
+    , S (Chy :>: tS (tS (tS (tV 1 -$ (tV 1 -$ tV 0)))))
+    ]
+  , [ S (Syy :>: (tS (tS (tV 0)) <:> (PI $- [tA TY, tS (PI $- [tV 0, tS (tV 1)])])))
+    , X "<:", O (Chy :<: pH "X")
+    ]
+  ,-}
+    [ I (Chy :>: ((tS (tV 0) <:> PI $- [tA TY, tS (tA TY)]) -$ tA TY)), X ":>",
+      S (Chy :>: tA TY)
+    ]
   ]
 
 {-

src/Pat.hs

-{-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures, RankNTypes #-}
+{-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures, RankNTypes, ScopedTypeVariables #-}
 
 module Pat where
 
@@ -65,8 +65,10 @@ An open Cod Pat has a negative thinning.
 pH :: String -> PaV Ch
 pH y = PM (Chy :?: y) :^ idth
 
-pY :: String -> PaV Ch
-pY y = PE (PM (Syy :?: y)) :^ idth
+pE :: forall d. DIRY d => String -> PaV d
+pE y = case (diry :: Diry d) of
+  Syy -> PM (Syy :?: y) :^ idth
+  Chy -> PE (PM (Syy :?: y)) :^ idth
 
 pA :: Atom -> Cod (Pat m Ch)
 pA a = PA a :^ 0