Remove U

src/Lam/Agda/Lam/Data.agda

@@ -14,7 +14,6 @@ Id = String
 data RawTypeL : Set where
   RawBoolT : RawTypeL
   RawIntT  : RawTypeL
-  RawU     : RawTypeL
   RawProd  : RawTypeL → RawTypeL → RawTypeL
   RawSum   : RawTypeL → RawTypeL → RawTypeL
   RawArrow : RawTypeL → RawTypeL → RawTypeL
@@ -25,13 +24,22 @@ data RawTypeL : Set where
 data TypeL : Set where
   BoolT : TypeL
   IntT  : TypeL
--- U is an opaque type
-  U     : TypeL
   Arrow : TypeL → TypeL → TypeL
   Prod  : TypeL → TypeL → TypeL
   Sum   : TypeL → TypeL → TypeL
 
-{-# COMPILE AGDA2HS TypeL deriving (Eq, Show) #-}
+{-# COMPILE AGDA2HS TypeL deriving Show #-}
+
+instance
+  iEqType : Eq TypeL
+  iEqType ._==_ BoolT BoolT = true
+  iEqType ._==_ IntT IntT = true
+  iEqType ._==_ (Arrow t11 t12) (Arrow t21 t22) = t11 == t21 && t12 == t22
+  iEqType ._==_ (Prod t11 t12) (Prod t21 t22) = t11 == t21 && t12 == t22
+  iEqType ._==_ (Sum t11 t12) (Sum t21 t22) = t11 == t21 && t12 == t22
+  iEqType ._==_ _ _ = false
+
+{-# COMPILE AGDA2HS iEqType #-}
 
 data ConstT : Set where
   NumC : Int → ConstT
@@ -123,6 +131,8 @@ instance
     o1 == o2 && e1 == e2
   iExprEq ._==_ (Ite b1 t1 e1) (Ite b2 t2 e2) =
     b1 == b2 && t1 == t2 && e1 == e2
+  iExprEq ._==_ (Inl e1 t1) (Inl e2 t2) = e1 == e2 && t1 == t2
+  iExprEq ._==_ (Inr e1 t1) (Inr e2 t2) = e1 == e2 && t1 == t2
   iExprEq ._==_ _ _ = false
 
 {-# COMPILE AGDA2HS iExprEq #-}

src/Lam/Agda/Lam/TypeChecker.agda

@@ -24,7 +24,7 @@ typeCheck' gam (Ite b t e)       =
     { BoolT ->
         typeCheck' gam t >>= λ tt ->
           typeCheck' gam e >>= λ te ->
-            if eqType tt te then (Just tt) else Nothing
+            if tt == te then (Just tt) else Nothing
     ; _ -> Nothing
     }
 typeCheck' _ (Const (NumC _))  = Just IntT
@@ -34,7 +34,7 @@ typeCheck' gam (Lam _ t e)       =
   typeCheck' (t ∷ gam) e >>= λ t' -> Just (Arrow t t')
 typeCheck' gam (App e1 e2) =
   myCaseOf (typeCheck' gam e1)
-    λ { (Just (Arrow t11 t12)) -> typeCheck' gam e2 >>= λ t2 -> if eqType t11 t2 then Just t12 else Nothing
+    λ { (Just (Arrow t11 t12)) -> typeCheck' gam e2 >>= λ t2 -> if t11 == t2 then Just t12 else Nothing
       ; _ -> Nothing
       }
 typeCheck' gam (BinOp Add e1 e2) =
@@ -109,25 +109,25 @@ typeCheck' gam (BinOp MkPair e1 e2) =
   Just (Prod t1 t2)
 typeCheck' gam (Inl e t) =
   myCaseOf t λ
-    { (Sum tl tr) -> typeCheck' gam e >>= λ te -> if eqType tl te then Just (Sum tl tr) else Nothing
+    { (Sum tl tr) -> typeCheck' gam e >>= λ te -> if tl == te then Just (Sum tl tr) else Nothing
     ; _ -> Nothing
     }
 typeCheck' gam (Inr e t) =
   myCaseOf t λ
-    { (Sum tl tr) -> typeCheck' gam e >>= λ te -> if eqType tr te then Just (Sum tl tr) else Nothing
+    { (Sum tl tr) -> typeCheck' gam e >>= λ te -> if tr == te then Just (Sum tl tr) else Nothing
     ; _ -> Nothing
     }
 typeCheck' gam (Case e1 _ e2 _ e3) =
   myCaseOf (typeCheck' gam e1) λ
     { (Just (Sum tl tr)) ->
         typeCheck' (tl ∷ gam) e2 >>= λ t2 ->
         typeCheck' (tr ∷ gam) e3 >>= λ t3 ->
-        if eqType t2 t3 then Just t2 else Nothing
+        if t2 == t3 then Just t2 else Nothing
     ; _ -> Nothing
     }
 typeCheck' gam (Fix e) =
   myCaseOf (typeCheck' gam e) λ
-  { (Just (Arrow te1 te2)) -> if eqType te1 te2 then Just te1 else Nothing
+  { (Just (Arrow te1 te2)) -> if te1 == te2 then Just te1 else Nothing
   ; _ -> Nothing
   }
 

src/Lam/Agda/Lam/UtilsAgda.agda

@@ -19,45 +19,32 @@ myCaseOf x f = f x
 
 {-# COMPILE AGDA2HS myCaseOf #-}
 
-eqType : TypeL → TypeL → Bool
-eqType BoolT        BoolT       = True
-eqType IntT         IntT        = True
-eqType U            U           = True
-eqType (Arrow t11 t12)  (Arrow t21 t22) = (eqType t11 t21) && (eqType t12 t22)
-eqType (Prod t11 t12)  (Prod t21 t22) = (eqType t11 t21) && (eqType t12 t22)
-eqType (Sum t11 t12)  (Sum t21 t22) = (eqType t11 t21) && (eqType t12 t22)
-eqType _            _           = False
-
-{-# COMPILE AGDA2HS eqType #-}
-
 lookup≡ : {t : Set} {l : List t} {i : Nat} → (h : i < length l) → (lookupMaybe i l) ≡ Just (lookup l i h)
 lookup≡ {t} {x ∷ l} {Z} h = refl
 lookup≡ {t} {x ∷ l} {S i} (s≤s h) = lookup≡ h 
 
 &&to× : {a b : Bool} → (a && b) ≡ True → a ≡ True × b ≡ True
 &&to× {True} {True} h = ⟨ refl , refl ⟩
 
-eqType->≡ : {t₁ t₂ : TypeL} → eqType t₁ t₂ ≡ True → t₁ ≡ t₂
+eqType->≡ : {t₁ t₂ : TypeL} → (t₁ == t₂) ≡ True → t₁ ≡ t₂
 eqType->≡ {BoolT} {BoolT} _ = refl
 eqType->≡ {IntT} {IntT} _ = refl
-eqType->≡ {U} {U} _ = refl
 eqType->≡ {Arrow t t₁} {Arrow t' t''} h with &&to× h
 ... | ⟨ t==t' , t₁==t'' ⟩ = cong₂ Arrow (eqType->≡ t==t') (eqType->≡ t₁==t'')
 eqType->≡ {Prod t t₁} {Prod t' t''} h with &&to× h
 ... | ⟨ t==t' , t₁==t'' ⟩ = cong₂ Prod (eqType->≡ t==t') (eqType->≡ t₁==t'')
 eqType->≡ {Sum t t₁} {Sum t' t''} h with &&to× h
 ... | ⟨ t==t' , t₁==t'' ⟩ = cong₂ Sum (eqType->≡ t==t') (eqType->≡ t₁==t'')
 
-eqType-refl : (t : TypeL) → eqType t t ≡ True
+eqType-refl : (t : TypeL) → (t == t) ≡ True
 eqType-refl BoolT = refl
 eqType-refl IntT = refl
-eqType-refl U = refl
 eqType-refl (Arrow dom codom) =
-  trans (cong (λ x → x && eqType codom codom) (eqType-refl dom)) (cong (λ x → True && x) (eqType-refl codom))
+  trans (cong (λ x → x && codom == codom) (eqType-refl dom)) (cong (λ x → True && x) (eqType-refl codom))
 eqType-refl (Prod t1 t2) =
-  trans (cong (λ x → x && eqType t2 t2) (eqType-refl t1)) (cong (λ x → True && x) (eqType-refl t2))
+  trans (cong (λ x → x && t2 == t2) (eqType-refl t1)) (cong (λ x → True && x) (eqType-refl t2))
 eqType-refl (Sum t1 t2) =
-  trans (cong (λ x → x && eqType t2 t2) (eqType-refl t1)) (cong (λ x → True && x) (eqType-refl t2))
+  trans (cong (λ x → x && t2 == t2) (eqType-refl t1)) (cong (λ x → True && x) (eqType-refl t2))
 
 injection-maybe : ∀ {t : Set} {a : t} → ¬ (Nothing ≡ Just a)
 injection-maybe = λ ()

src/Lam/Context.hs

@@ -28,7 +28,6 @@ expandType gctx (RawProd t1 t2) =
   Right (Prod t1' t2')
 expandType _ RawBoolT = Right BoolT
 expandType _ RawIntT = Right IntT
-expandType _ RawU = Right U
 expandType gctx (RawArrow t1 t2) =
   expandType gctx t1 >>= \t1' ->
   expandType gctx t2 >>= \t2' ->

src/Lam/Handler.hs

@@ -116,4 +116,4 @@ handleFile fName = do
   mapM_ handleCommand prog
 
 handleFileWrapper :: String -> Result ()
-handleFileWrapper fName = runInRawMode (handleFile fName)
+handleFileWrapper = runInRawMode . handleFile

src/Lam/Parser/Parser.y

@@ -149,7 +149,7 @@ ExitCommand :: { () }
 UntypedRawExpr :: { RawExpr }
   : UntypedRawExpr "." UntypedRawExpr { RawApp $1 $3  }
   | "lam" CommaSeparatedIdents "->" UntypedRawExpr %shift
-    { joinLams $2 RawU $4 }
+    { joinLams $2 RawIntT $4 }
   | var { RawVar $1 }
   | number { RawConst (NumC $1) }
   | boolean { RawConst (BoolC $1) }
@@ -196,7 +196,6 @@ ParExpr : "(" RawExpr ")" { $2 }
 
 RawTypeL :: { RawTypeL }
   : RawTypeL "=>" RawTypeL { RawArrow $1 $3 }
-  | "U" { RawU }
   | "Int" { RawIntT }
   | "Bool" { RawBoolT }
   | var { FreeType $1 }

src/Lam/Utils.hs

@@ -24,7 +24,6 @@ pickFresh ctx nm
 prettyPrintType :: TypeL -> String
 prettyPrintType BoolT = "Bool"
 prettyPrintType IntT = "Int"
-prettyPrintType U = "U"
 prettyPrintType (Prod t1 t2) =
   unwords [ "( Prod", prettyPrintType t1, prettyPrintType t2, ")" ]
 prettyPrintType (Sum t1 t2) =