Start adding inferType

diff --git a/Eval.hs b/Eval.hs
index 8915535d63811f12caa7e5cc93dcecb3523c764c..7be6d0013c245602ccbce322f457a267f8268c8e 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -159,10 +159,23 @@ fstVal u | isNeutral u = VFst u
 sndVal (VSPair a b)    = b
 sndVal u | isNeutral u = VSnd u
 
+-- infer the type of a neutral value
+inferType :: Val -> Val
+inferType v = case v of
+  VVar _ t -> t
+  VFst t -> undefined
+  VSnd t -> undefined
+  VSplit t0 t1 -> undefined
+  VApp t0 t1 -> undefined
+  VAppFormula t phi -> undefined
+
 (@@) :: ToFormula a => Val -> a -> Val
-(VPath i u) @@ phi    = u `act` (i, toFormula phi)
+(VPath i u) @@ phi = u `act` (i,toFormula phi)
 -- (KanUElem _ u) @@ phi = u @@ phi
-v @@ phi          = VAppFormula v (toFormula phi)
+v @@ phi = case (inferType v,toFormula phi) of
+  (VIdP  _ a0 _,Dir 0) -> a0
+  (VIdP  _ _ a1,Dir 1) -> a1
+  _  -> VAppFormula v (toFormula phi)
 
 -----------------------------------------------------------
 -- Transport
@@ -285,6 +298,7 @@ conv k u v | u == v    = True
   (VTrans p u,v) | isIndep k j (p @@ j) -> conv k u v
   (u,VTrans p v) | isIndep k j (p @@ j) -> conv k u v
   (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u'
+  (VAppFormula u x,VAppFormula u' x') -> conv k u u' && (x == x')
   -- VAppformula
   -- VTrans
   -- VComp

diff --git a/examples/nat.ctt b/examples/nat.ctt
index 4eccc35b8b29cee086f2ea8cf30c57a64da85384..e1398731104776c1cc795ad7feedabf90228de26 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -71,3 +71,6 @@ J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
 
 defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
        Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d
+
+
+test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
\ No newline at end of file