Calculator.lean

inductive Transcendental where
  | sin
  | cos
  | tan
  | exp
  | log
  deriving Repr

/-- A simple vector type with a proof that the size is the same as the length of the array-/
structure Vector (a : Type) (n : Nat) where
  /--Underlying data-/
  data : Array a
  /--Proof that the size is the same as the length of the array-/
  _pf : n = data.size
  deriving Repr

/-- A simple calculator expression-/
inductive Expr' where
  /--A number-/
  | number (value : Float)
  /--Addition-/
  | add (left right : Expr')
  /--Multiplication-/
  | mul (left right : Expr')
  /--Division-/
  | div (left right : Expr')
  /--Subtraction-/
  | sub (left right : Expr')
  /--A transcendental function-/
  | function (fn : Transcendental) (args : Array Expr')
  -- TODO: use Vector 1 Float instead of Array Expr' to eliminate need for error handling
  deriving Repr

/-- Evaluates an expression to a float, returning `none` if the expression is not valid-/
def Expr'.eval (expr: Expr') : Option Float := do
  match expr with
  | .number value => pure value -- base case
  | .add left right => pure ((<-left.eval) + (<-right.eval))
  | .mul left right => pure ((<-left.eval) * (<-right.eval))
  | .div left right => pure ((<-left.eval) / (<-right.eval))
  | .sub left right => pure ((<-left.eval) - (<-right.eval))
  | .function .sin #[value] => pure (Float.sin (<- value.eval))
  | .function .cos #[value] => pure (Float.cos (<- value.eval))
  | .function .tan #[value] => pure (Float.tan (<- value.eval))
  | .function .exp #[value] => pure (Float.exp (<- value.eval))
  | .function .log #[value] => pure (Float.log (<- value.eval))
  | _ => .none

/-- Demonstrates how `..` can ignore the arguments of a constructor-/
def Expr'.name : Expr' -> String
  | .number _ => "number"
  | .add .. => "add"
  | .mul .. => "mul"
  | .div .. => "div"
  | .sub .. => "sub"
  | .function .. => "function"


#eval (Expr'.function .sin #[.number 1]).eval
#eval 1 :: 2 :: [3]