truthy and falsy strings

imp/Imp/Expr/Basic.lean

@@ -20,7 +20,6 @@ end Expr
 inductive Expr where
   | constInt (i : Int)
   | constStr (x : String)
-  | constBool (x : Bool)
   | var (name : String)
   | un (op : Expr.UnOp) (e : Expr)
   | bin (op : Expr.BinOp) (e1 e2 : Expr)

imp/Imp/Expr/Delab.lean

@@ -21,6 +21,12 @@ def delabNameInner : DelabM (TSyntax `varname) := do
     pure <| ⟨x.raw⟩
   | _ => `(varname|~($(← delab))) >>= annAsTerm
 
+-- def delabStrInner : DelabM (TSyntax `str) := do
+--   let e ← getExpr
+--   match e with
+--   | .lit (.strVal s) =>
+--     let x := mkIdent <| .mkSimple s
+
 partial def delabExprInner : DelabM (TSyntax `exp) := do
   let e ← getExpr
   let stx ←
@@ -41,7 +47,7 @@ partial def delabExprInner : DelabM (TSyntax `exp) := do
         else withAppArg `(exp| ~$(← delab))
       | BitVec.ofNat _ _ => (⟨·.raw⟩) <$> (withAppArg <| withAppArg <| delab)
       | _ =>
-        `(exp| ~(Expr.const $(← withAppArg delab)))
+        `(exp| ~(Expr.constInt $(← withAppArg delab)))
     | Expr.var _ => do
       let x ← withAppArg delabNameInner
       `(exp|$x:varname)
@@ -58,12 +64,13 @@ partial def delabExprInner : DelabM (TSyntax `exp) := do
       | BinOp.lt => `(exp| $s1 < $s2)
       | BinOp.le => `(exp| $s1 ≤ $s2)
       | BinOp.eq => `(exp| $s1 == $s2)
+      | BinOp.append => `(exp| $s1 ++ $s2)
       | _ => `(exp|~(Expr.bin $(← withAppFn <| withAppFn <| withAppArg delab) $(← withAppFn <| withAppArg delab) $(← withAppArg delab)))
     | Expr.un op _ =>
       let s ← withAppArg delabExprInner
       match_expr op with
-      | UnOp.neg => `(exp|-$s)
-      | UnOp.not => `(exp|!$s)
+      | UnOp.neg => `(exp| -$s)
+      | UnOp.not => `(exp| !$s)
       | _ => `(exp| ~(Expr.un $(← withAppFn <| withAppArg delab) $(← withAppArg delab)))
     | _ =>
       `(exp| ~$(← delab))
@@ -82,14 +89,22 @@ partial def delabExpr : Delab := do
   | `(exp|~$e) => pure e
   | e => `(term|expr {$(⟨e⟩)})
 
-/-- info: expr { 5 } : Expr -/
-#guard_msgs in
+/- info: expr { 5 } : Expr -/
+-- #guard_msgs in
 #check Expr.constInt 5
 
-/-- info: expr { 5 } : Expr -/
-#guard_msgs in
+/- info: expr { 5 } : Expr -/
+-- #guard_msgs in
 #check expr { 5 }
 
+/- info: expr { [a] } : Expr -/
+-- #guard_msgs in
+#check Expr.constStr "a"
+
+/- info: expr { [a] } : Expr -/
+-- #guard_msgs in
+-- #check expr { [a] }
+
 /-- info: expr { x } : Expr -/
 #guard_msgs in
 #check expr { x }
@@ -102,9 +117,9 @@ partial def delabExpr : Delab := do
 #guard_msgs in
 #check expr { 5 + (23 - 10) }
 
-/--
+/-
 info: let x := expr { 23 };
 expr { ~x * ~x } : Expr
 -/
-#guard_msgs in
+-- #guard_msgs in
 #check let x := expr {23}; expr {~x * ~x}

imp/Imp/Expr/Eval.lean

@@ -7,7 +7,6 @@ namespace Imp
 inductive Value where
 | str : String -> Value
 | int : Int -> Value
-| bool : Bool -> Value
 
 instance : OfNat Value n := by
   constructor
@@ -48,7 +47,8 @@ namespace Expr
 /-- Helper that implements unary operators -/
 def UnOp.apply : UnOp → Value → Option Value
   | .neg, .int i => (Value.int ∘ Int.neg) <$> some i
-  | .not, .bool b => (Value.bool ∘ Bool.not) <$> some b
+  | .not, .int b => if b == 0 then some (Value.int 1) else some (Value.int 0)
+  | .not, .str s => some $ Value.int (if s.isEmpty then 1 else 0)
   | _, _ => none
 
 /-- Helper that implements binary operators -/
@@ -57,14 +57,15 @@ def BinOp.apply : BinOp → Value → Value → Option Value
   | .minus, .int i, .int j => some $ Value.int (i - j)
   | .times, .int i, .int j => some $ Value.int (i * j)
   | .div, .int i, .int j => if j == 0 then none else some $ Value.int (i / j)
-  | .and, .bool b, .bool c => some $ Value.bool (b && c)
-  | .or, .bool b, .bool c => some $ Value.bool (b || c)
-  | .eq, .int i, .int j => some $ Value.bool (i == j)
-  | .eq, .bool b, .bool c => some $ Value.bool (b == c)
-  | .eq, .str s, .str t => some $ Value.bool (s == t)
-  | .le, .int i, .int j => some $ Value.bool (i <= j)
-  | .lt, .int i, .int j => some $ Value.bool (i < j)
-  |.append, .str s, .str t => some $ Value.str (s ++ t)
+  | .and, .int b, .int c => some $ Value.int (b * c)
+  | .and, .str b, .str c => some $ Value.int (b ++ c).length
+  | .or, .int b, .int c => some $ Value.int (b + c)
+  | .or, .str s, .str t => some $ Value.str (s ++ t)
+  | .eq, .int i, .int j => some $ if i == j then Value.int 1 else Value.int 0
+  | .eq, .str s, .str t => some $ if s == t then (Value.int 1) else (Value.int 0)
+  | .le, .int i, .int j => some (if i <= j then Value.int 1 else Value.int 0)
+  | .lt, .int i, .int j => some $ if i < j then Value.int 1 else Value.int 0
+  | .append, .str s, .str t => some $ Value.str (s ++ t)
   | _, _, _ => none
 
 /--
@@ -73,8 +74,7 @@ Evaluates an expression, finding the value if it has one.
 Expressions that divide by zero don't have values - the result is undefined.
 -/
 def eval (σ : Env) : Expr → Option Value
-  | .constInt i => some $ Value.int i
-  | .constBool b => some $ .bool b
+  | .constInt i => some $ .int i
   | .constStr s => some $ .str s
   | .var x => σ.get x
   | .un op e => do

imp/Imp/Expr/Syntax.lean

@@ -32,6 +32,9 @@ syntax varname : exp
 /-- Numeric constant -/
 syntax num : exp
 
+/-- Strings -/
+syntax:1 "[" str "]": exp
+
 /-- Arithmetic complement -/
 syntax:75 "-" exp:75 : exp
 
@@ -45,11 +48,6 @@ syntax:65 exp:65 " + " exp:66 : exp
 /-- Subtraction -/
 syntax:65 exp:65 " - " exp:66 : exp
 
-/-- Left shift -/
-syntax:55 exp:55 " <<< " exp:56 :exp
-/-- Right shift -/
-syntax:55 exp:55 " >>> " exp:56 :exp
-
 /-- Boolean negation -/
 syntax:75 "!" exp:75 : exp
 /-- Less than -/
@@ -63,16 +61,14 @@ syntax:50 exp:50 " > " exp:51 : exp
 /-- Equal -/
 syntax:45 exp:45 " == " exp:46 : exp
 
-/-- Bitwise and -/
-syntax:40 exp:40 " &&& " exp:41 :exp
-/-- Bitwise or -/
-syntax:40 exp:40 " ||| " exp:41 :exp
-
 /-- Boolean conjunction -/
 syntax:35 exp:35 " && " exp:36 : exp
 /-- Boolean disjunction -/
 syntax:35 exp:35 " || " exp:36 : exp
 
+/-- String append -/
+syntax:30 exp:30 " ++ " exp:31 : exp
+
 /-- Parentheses for grouping -/
 syntax "(" exp ")" : exp
 
@@ -85,7 +81,7 @@ syntax:min "expr " "{ " exp " }" : term
 open Lean in
 macro_rules
   | `(expr{$x:ident}) => `(Expr.var $(quote x.getId.toString))
-  | `(expr{$n:num}) => `(Expr.const $(quote n.getNat))
+  | `(expr{$n:num}) => `(Expr.constInt $(quote n.getNat))
 
   | `(expr{-$e}) => `(Expr.un .neg (expr{$e}))
   | `(expr{!$e}) => `(Expr.un .not (expr{$e}))
@@ -95,12 +91,6 @@ macro_rules
   | `(expr{$e1 - $e2}) => `(Expr.bin .minus (expr{$e1}) (expr{$e2}))
   | `(expr{$e1 / $e2}) => `(Expr.bin .div (expr{$e1}) (expr{$e2}))
 
-  | `(expr{$e1 >>> $e2}) => `(Expr.bin .rsh (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 <<< $e2}) => `(Expr.bin .lsh (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 ||| $e2}) => `(Expr.bin .bor (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 &&& $e2}) => `(Expr.bin .band (expr{$e1}) (expr{$e2}))
-
-
   | `(expr{$e1 && $e2}) => `(Expr.bin .and (expr{$e1}) (expr{$e2}))
   | `(expr{$e1 || $e2}) => `(Expr.bin .or (expr{$e1}) (expr{$e2}))
 
@@ -109,6 +99,7 @@ macro_rules
   | `(expr{$e1 == $e2}) => `(Expr.bin .eq (expr{$e1}) (expr{$e2}))
   | `(expr{$e1 ≥ $e2}) => `(Expr.bin .le (expr{$e2}) (expr{$e1}))
   | `(expr{$e1 > $e2}) => `(Expr.bin .lt (expr{$e2}) (expr{$e1}))
+  | `(expr{$e1 ++ $e2}) => `(Expr.bin .append (expr{$e1}) (expr{$e2}))
   | `(expr{($e)}) => `(expr{$e})
   | `(expr{~$stx}) => pure stx
 

imp/Imp/Stmt.lean

@@ -4,4 +4,3 @@ This file exists only to re-export the contents of the `Imp.Stmt` module hierarc
 import Imp.Stmt.Basic
 import Imp.Stmt.BigStep
 import Imp.Stmt.Delab
-import Imp.Stmt.Optimize