Lesser than and some bug fixes

Author: tomaz1502

src/Lam/Agda/Lam/Data.agda

@@ -61,6 +61,7 @@ data BinOpT : Set where
   Mul    : BinOpT
   And    : BinOpT
   Or     : BinOpT
+  LtInt  : BinOpT
   MkPair : BinOpT
 
 {-# COMPILE AGDA2HS BinOpT deriving (Eq, Show) #-}
@@ -72,6 +73,7 @@ instance
   iEqBinOp ._==_ Mul Mul = true
   iEqBinOp ._==_ And And = true
   iEqBinOp ._==_ Or Or = true
+  iEqBinOp ._==_ LtInt LtInt = true
   iEqBinOp ._==_ MkPair MkPair = true
   iEqBinOp ._==_ _ _ = false
 

src/Lam/Agda/Lam/Evaluator.agda

@@ -117,6 +117,7 @@ smallStepBinOp o e1 _ Nothing (Just e2') = Just (BinOp o e1 e2')
 smallStepBinOp Add (Const (NumC i1)) (Const (NumC i2)) Nothing Nothing = Just (Const (NumC (i1 + i2)))
 smallStepBinOp Sub (Const (NumC i1)) (Const (NumC i2)) Nothing Nothing = Just (Const (NumC (i1 - i2)))
 smallStepBinOp Mul (Const (NumC i1)) (Const (NumC i2)) Nothing Nothing = Just (Const (NumC (i1 * i2)))
+smallStepBinOp LtInt (Const (NumC i1)) (Const (NumC i2)) Nothing Nothing = Just (Const (BoolC (i1 < i2)))
 smallStepBinOp And (Const (BoolC i1)) (Const (BoolC i2)) Nothing Nothing = Just (Const (BoolC (i1 && i2)))
 smallStepBinOp Or  (Const (BoolC i1)) (Const (BoolC i2)) Nothing Nothing = Just (Const (BoolC (i1 || i2)))
 smallStepBinOp _ _ _ _ _ = Nothing

src/Lam/Agda/Lam/FormalizationEvaluator.agda

@@ -4,7 +4,7 @@ open import Lam.Data
 open import Lam.Evaluator
 open import Lam.UtilsAgda
 
-open import Haskell.Prelude                       using (Just; Nothing; Int; Bool; _+_; _-_; _*_; _&&_; _||_; not)
+open import Haskell.Prelude                       using (Just; Nothing; Int; Bool; _+_; _-_; _*_; _&&_; _||_; not; _<_)
 
 open import Data.Bool                             using (true; false)
 open import Data.Empty                            using (⊥-elim; ⊥)
@@ -58,6 +58,13 @@ data Neutral where
     ---------------------
     → Neutral (BinOp Mul L M)
 
+  noe-ltInt : ∀ {L M : Expr}
+    → Normal L
+    → Normal M
+    → (∀ {i j : Int} → ¬ (L ≡ (Const (NumC i)) × M ≡ (Const (NumC j))))
+    ---------------------
+    → Neutral (BinOp LtInt L M)
+
   noe-and : ∀ {L M : Expr}
     → Normal L
     → Normal M
@@ -140,7 +147,7 @@ data ReducesTo : Expr → Expr → Set where
     → Normal V1
     → Normal V2
     ---------------------------
-    → ReducesTo (App (Lam s ty V1) V2) (substitute V1 V2)
+    → ReducesTo (App (Lam s ty V1) V2) (substitute V2 V1)
     -- using a predicate to specify substitution here gets pretty ugly
 
   r-l' : ∀ {s : Id} {ty : TypeL} {L L' : Expr}
@@ -168,6 +175,9 @@ data ReducesTo : Expr → Expr → Set where
   r-mul : ∀ {i1 i2 : Int}
     → ReducesTo (BinOp Mul (Const (NumC i1)) (Const (NumC i2))) (Const (NumC (i1 * i2)))
 
+  r-ltInt : ∀ {i1 i2 : Int}
+    → ReducesTo (BinOp LtInt (Const (NumC i1)) (Const (NumC i2))) (Const (BoolC (i1 < i2)))
+
   r-and : ∀ {i1 i2 : Bool}
     → ReducesTo (BinOp And (Const (BoolC i1)) (Const (BoolC i2))) (Const (BoolC (i1 && i2)))
 
@@ -290,6 +300,11 @@ stepNothingNormal {BinOp Mul L M} eq | Nothing | Nothing =
   where
     mulStepNothing : ∀ {i j} → smallStepBinOp Mul L M Nothing Nothing ≡ Nothing → ¬ ((L ≡ Const (NumC i)) × (M ≡ Const (NumC j)))
     mulStepNothing () ⟨ refl , refl ⟩
+stepNothingNormal {BinOp LtInt L M} eq | Nothing | Nothing =
+  no-ne (noe-ltInt (stepNothingNormal eqL) (stepNothingNormal eqM) (ltStepNothing eq))
+  where
+    ltStepNothing : ∀ {i j} → smallStepBinOp LtInt L M Nothing Nothing ≡ Nothing → ¬ ((L ≡ Const (NumC i)) × (M ≡ Const (NumC j)))
+    ltStepNothing () ⟨ refl , refl ⟩
 stepNothingNormal {BinOp And L M} eq | Nothing | Nothing =
   no-ne (noe-and (stepNothingNormal eqL) (stepNothingNormal eqM) (andStepNothing eq))
   where
@@ -368,6 +383,11 @@ neutralStepNothing {BinOp Mul L M} (noe-mul h1 h2 h3)
        |  normalStepNothing h2 with smallStepBinOp Mul L M Nothing Nothing in eq
 neutralStepNothing {BinOp Mul L M} (noe-mul h1 h2 h3) | Nothing = refl
 neutralStepNothing {BinOp Mul (Const (NumC L')) (Const (NumC M'))} (noe-mul h1 h2 h3) | Just V' = ⊥-elim (h3 {L'} {M'} ⟨ refl , refl ⟩)
+neutralStepNothing {BinOp LtInt L M} (noe-ltInt h1 h2 h3)
+  rewrite normalStepNothing h1
+       |  normalStepNothing h2 with smallStepBinOp LtInt L M Nothing Nothing in eq
+neutralStepNothing {BinOp LtInt L M} (noe-ltInt h1 h2 h3) | Nothing = refl
+neutralStepNothing {BinOp LtInt (Const (NumC L')) (Const (NumC M'))} (noe-ltInt h1 h2 h3) | Just V' = ⊥-elim (h3 {L'} {M'} ⟨ refl , refl ⟩)
 neutralStepNothing {BinOp And L M} (noe-and h1 h2 h3)
   rewrite normalStepNothing h1
        |  normalStepNothing h2 with smallStepBinOp And L M Nothing Nothing in eq
@@ -421,6 +441,8 @@ step→red {BinOp Sub (Const (NumC i)) M} {N} h | Nothing | Nothing with M
 ... | Const (NumC j) rewrite sym (Just-injective h) = r-sub
 step→red {BinOp Mul (Const (NumC i)) M} {N} h | Nothing | Nothing with M
 ... | Const (NumC j) rewrite sym (Just-injective h) = r-mul
+step→red {BinOp LtInt (Const (NumC i)) M} {N} h | Nothing | Nothing with M
+... | Const (NumC j) rewrite sym (Just-injective h) = r-ltInt
 step→red {BinOp And (Const (BoolC i)) M} {N} h | Nothing | Nothing with M
 ... | Const (BoolC j) rewrite sym (Just-injective h) = r-and
 step→red {BinOp Or (Const (BoolC i)) M}  {N} h | Nothing | Nothing with M
@@ -457,6 +479,7 @@ red→step (r-binop1 h) rewrite red→step h = refl
 red→step (r-binop2 x h) rewrite normalStepNothing x | red→step h = refl
 red→step r-sub = refl
 red→step r-mul = refl
+red→step r-ltInt = refl
 red→step r-and = refl
 red→step r-or = refl
 red→step r-ite-true = refl

src/Lam/Agda/Lam/FormalizationTypeChecker.agda

@@ -56,6 +56,11 @@ data _⊢_∶_ : TypingContext → Expr → TypeL → Set where
     → Γ ⊢ M ∶ IntT
     → Γ ⊢ BinOp Mul L M ∶ IntT
 
+  ⊢< : ∀ {L M : Expr} {Γ : TypingContext}
+    → Γ ⊢ L ∶ IntT
+    → Γ ⊢ M ∶ IntT
+    → Γ ⊢ BinOp LtInt L M ∶ BoolT
+
   ⊢ite : ∀ {Γ : TypingContext} {b t e : Expr} {A : TypeL}
     → Γ ⊢ b ∶ BoolT
     → Γ ⊢ t ∶ A
@@ -121,6 +126,7 @@ data _⊢_∶_ : TypingContext → Expr → TypeL → Set where
 ⊢→tc (⊢+  h1 h2) rewrite ⊢→tc h1 | ⊢→tc h2 = refl
 ⊢→tc (⊢-  h1 h2) rewrite ⊢→tc h1 | ⊢→tc h2 = refl
 ⊢→tc (⊢*  h1 h2) rewrite ⊢→tc h1 | ⊢→tc h2 = refl
+⊢→tc (⊢<  h1 h2) rewrite ⊢→tc h1 | ⊢→tc h2 = refl
 ⊢→tc {Γ} {Ite b t e} {ty} (⊢ite tb tt te)
   rewrite
     ⊢→tc {Γ} {b} {BoolT} tb
@@ -183,6 +189,9 @@ tc→⊢ {Γ} {BinOp Mul e1 e2} eq with typeCheck' Γ e1 in eqE1
 tc→⊢ {Γ} {BinOp Sub e1 e2} eq with typeCheck' Γ e1 in eqE1
 ... | Just IntT with typeCheck' Γ e2 in eqE2
 ...   | Just IntT rewrite sym (Just-injective eq) = ⊢- (tc→⊢ eqE1) (tc→⊢ eqE2)
+tc→⊢ {Γ} {BinOp LtInt e1 e2} eq with typeCheck' Γ e1 in eqE1
+... | Just IntT with typeCheck' Γ e2 in eqE2
+...   | Just IntT rewrite sym (Just-injective eq) = ⊢< (tc→⊢ eqE1) (tc→⊢ eqE2)
 tc→⊢ {Γ} {BinOp And e1 e2} eq with typeCheck' Γ e1 in eqE1
 ... | Just BoolT with typeCheck' Γ e2 in eqE2
 ...   | Just BoolT rewrite sym (Just-injective eq) = ⊢&& (tc→⊢ eqE1) (tc→⊢ eqE2)

src/Lam/Agda/Lam/TypeChecker.agda

@@ -63,6 +63,15 @@ typeCheck' gam (BinOp Mul e1 e2) =
                }
       ; _ -> Nothing
       }
+typeCheck' gam (BinOp LtInt e1 e2) =
+  myCaseOf (typeCheck' gam e1)
+    λ { (Just IntT) ->
+           myCaseOf (typeCheck' gam e2)
+             λ { (Just IntT) -> Just BoolT
+               ; _ -> Nothing
+               }
+      ; _ -> Nothing
+      }
 typeCheck' gam (BinOp And e1 e2) =
   myCaseOf (typeCheck' gam e1)
     λ { (Just BoolT) ->

src/Lam/Handler.hs

@@ -49,7 +49,6 @@ handleEval :: RawExpr -> Result ()
 handleEval rExpr = do
   gctx    <- get
   expr    <- liftEither (eraseNames gctx rExpr)
-  liftIO (putStrLnFlush (show expr))
   isUntyped <- askUntyped
   if isUntyped then
     liftIO (putStrLnFlush (untypedPrettyPrint (eval expr)))

src/Lam/Parser/Parser.y

@@ -24,14 +24,17 @@ import Lam.Parser.Lexer qualified as L
 %right "else"
 %left "."
 %right "=>"
-%right "&&" "||"
-%right "+" "-" "+T"
-%right "*" "*T"
-%right "!"
-%right "proj1"
-%right "proj2"
-%right "inl"
-%right "inr"
+%left "<" ">"
+%left "&&" "||"
+%left "+" "-"
+%right "+T"
+%left "*"
+%right "*T"
+%left "!"
+%left "proj1"
+%left "proj2"
+%left "inl"
+%left "inr"
 
 %token
   "lam"     { L.Lam        }
@@ -162,6 +165,7 @@ RawExpr :: { RawExpr }
   | RawExpr "*" RawExpr { RawBinOp Mul $1 $3 }
   | RawExpr "&&" RawExpr { RawBinOp And $1 $3 }
   | RawExpr "||" RawExpr { RawBinOp Or $1 $3 }
+  | RawExpr "<" RawExpr { RawBinOp LtInt $1 $3 }
   | "!" RawExpr { RawUnOp Not $2 }
   | "if" RawExpr "then" RawExpr "else" RawExpr { RawIte $2 $4 $6 }
   | "proj1" RawExpr { RawUnOp Proj1 $2 }

src/Lam/Utils.hs

@@ -40,6 +40,7 @@ prettyPrint = go []
         ppBinOp Mul = "*"
         ppBinOp And = "&&"
         ppBinOp Or = "||"
+        ppBinOp LtInt = "<"
         ppBinOp MkPair = undefined
         ppUnOp Not = "!"
         ppUnOp Proj1 = "proj1"