From 6eee12d5f2c87237fb1276538aa9d1e8ef4addc8 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Tue, 7 Feb 2023 13:59:06 -0800
Subject: Idiomatic naming conventions

---
 backends/lean/Primitives.lean | 92 +++++++++++++++++++++----------------------
 1 file changed, 46 insertions(+), 46 deletions(-)

(limited to 'backends')

diff --git a/backends/lean/Primitives.lean b/backends/lean/Primitives.lean
index 79958d94..a0892ca7 100644
--- a/backends/lean/Primitives.lean
+++ b/backends/lean/Primitives.lean
@@ -9,69 +9,69 @@ import Mathlib.Tactic.RunCmd
 
 -- Results & monadic combinators
 
--- TODO: use syntactic conventions and capitalize error, result, etc.
-
-inductive error where
-   | assertionFailure: error
-   | integerOverflow: error
-   | arrayOutOfBounds: error
-   | maximumSizeExceeded: error
-   | panic: error
+-- TODO: use syntactic conventions and capitalize Error, Result, etc.
+
+inductive Error where
+   | assertionFailure: Error
+   | integerOverflow: Error
+   | arrayOutOfBounds: Error
+   | maximumSizeExceeded: Error
+   | panic: Error
 deriving Repr, BEq
 
-open error
+open Error
 
-inductive result (α : Type u) where
-  | ret (v: α): result α
-  | fail (e: error): result α 
+inductive Result (α : Type u) where
+  | ret (v: α): Result α
+  | fail (e: Error): Result α 
 deriving Repr, BEq
 
-open result
+open Result
 
 /- HELPERS -/
 
 -- TODO: is there automated syntax for these discriminators?
-def is_ret {α: Type} (r: result α): Bool :=
+def is_ret {α: Type} (r: Result α): Bool :=
   match r with
-  | result.ret _ => true
-  | result.fail _ => false
+  | Result.ret _ => true
+  | Result.fail _ => false
 
-def massert (b:Bool) : result Unit :=
+def massert (b:Bool) : Result Unit :=
   if b then .ret () else fail assertionFailure
 
-def eval_global {α: Type} (x: result α) (_: is_ret x): α :=
+def eval_global {α: Type} (x: Result α) (_: is_ret x): α :=
   match x with
-  | result.fail _ => by contradiction
-  | result.ret x => x
+  | Result.fail _ => by contradiction
+  | Result.ret x => x
 
 /- DO-DSL SUPPORT -/
 
-def bind (x: result α) (f: α -> result β) : result β :=
+def bind (x: Result α) (f: α -> Result β) : Result β :=
   match x with
   | ret v  => f v 
   | fail v => fail v
 
--- Allows using result in do-blocks
-instance : Bind result where
+-- Allows using Result in do-blocks
+instance : Bind Result where
   bind := bind
 
 -- Allows using return x in do-blocks
-instance : Pure result where
+instance : Pure Result where
   pure := fun x => ret x
 
 /- CUSTOM-DSL SUPPORT -/
 
--- Let-binding the result of a monadic operation is oftentimes not sufficient,
+-- Let-binding the Result of a monadic operation is oftentimes not sufficient,
 -- because we may need a hypothesis for equational reasoning in the scope. We
 -- rely on subtype, and a custom let-binding operator, in effect recreating our
 -- own variant of the do-dsl
 
-def result.attach : (o : result α) → result { x : α // o = ret x }
+def Result.attach : (o : Result α) → Result { x : α // o = ret x }
   | .ret x => .ret ⟨x, rfl⟩
   | .fail e   => .fail e
 
 macro "let" h:ident " : " e:term " <-- " f:term : doElem =>
-  `(doElem| let ⟨$e, $h⟩ ← result.attach $f)
+  `(doElem| let ⟨$e, $h⟩ ← Result.attach $f)
 
 -- Silly example of the kind of reasoning that this notation enables
 #eval do
@@ -99,8 +99,8 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem =>
 -- total function over nats...? the hypothesis in the if condition is not used
 -- in the then-branch which confuses me quite a bit
 
--- TODO: add a refinement for the result (just like vec_push_back below) that
--- explains that the toNat of the result (in the case of success) is the sub of
+-- TODO: add a refinement for the Result (just like vec_push_back below) that
+-- explains that the toNat of the Result (in the case of success) is the sub of
 -- the toNat of the arguments (i.e. intrinsic specification)
 -- ... do we want intrinsic specifications for the builtins? that might require
 -- some careful type annotations in the monadic notation for clients, but may
@@ -134,7 +134,7 @@ macro_rules
 -- and
 -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean
 -- which both contain a fair amount of reasoning already!
-def USize.checked_sub (n: USize) (m: USize): result USize :=
+def USize.checked_sub (n: USize) (m: USize): Result USize :=
   -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed?
   if n >= m then
     let n' := USize.toNat n
@@ -150,7 +150,7 @@ def USize.checked_sub (n: USize) (m: USize): result USize :=
   else
     fail integerOverflow
 
-def USize.checked_add (n: USize) (m: USize): result USize :=
+def USize.checked_add (n: USize) (m: USize): Result USize :=
   if h: n.val.val + m.val.val <= 4294967295 then
     .ret ⟨ n.val.val + m.val.val, by
       have h': 4294967295 < USize.size := by intlit
@@ -161,7 +161,7 @@ def USize.checked_add (n: USize) (m: USize): result USize :=
   else
     .fail integerOverflow
 
-def USize.checked_rem (n: USize) (m: USize): result USize :=
+def USize.checked_rem (n: USize) (m: USize): Result USize :=
   if h: m > 0 then
     .ret ⟨ n.val % m.val, by
       have h1: ↑m.val < USize.size := m.val.isLt
@@ -171,7 +171,7 @@ def USize.checked_rem (n: USize) (m: USize): result USize :=
   else
     .fail integerOverflow
 
-def USize.checked_mul (n: USize) (m: USize): result USize :=
+def USize.checked_mul (n: USize) (m: USize): Result USize :=
     if h: n.val.val * m.val.val <= 4294967295 then
     .ret ⟨ n.val.val * m.val.val, by
       have h': 4294967295 < USize.size := by intlit
@@ -182,7 +182,7 @@ def USize.checked_mul (n: USize) (m: USize): result USize :=
   else
     .fail integerOverflow
 
-def USize.checked_div (n: USize) (m: USize): result USize :=
+def USize.checked_div (n: USize) (m: USize): Result USize :=
   if m > 0 then
     .ret ⟨ n.val / m.val, by
       have h1: ↑n.val < USize.size := n.val.isLt
@@ -209,7 +209,7 @@ run_cmd
     end $typeName
   ))
 
-def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): result dst :=
+def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): Result dst :=
   if h: MachineInteger.val x < MachineInteger.size dst then
     .ret (MachineInteger.ofNatCore (MachineInteger.val x).val h)
   else
@@ -249,11 +249,11 @@ def vec_len (α : Type u) (v : vec α) : USize :=
 def vec_push_fwd (α : Type u) (_ : vec α) (_ : α) : Unit := ()
 
 -- NOTE: old version trying to use a subtype notation, but probably better to
--- leave result elimination to auxiliary lemmas with suitable preconditions
+-- leave Result elimination to auxiliary lemmas with suitable preconditions
 -- TODO: I originally wrote `List.length v.val < USize.size - 1`; how can one
 -- make the proof work in that case? Probably need to import tactics from
 -- mathlib to deal with inequalities... would love to see an example.
-def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec α) //
+def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: Result (vec α) //
   match res with | fail _ => True | ret v' => List.length v'.val = List.length v.val + 1}
   :=
   if h : List.length v.val + 1 < USize.size then
@@ -272,12 +272,12 @@ def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec 
   -- annotate `x`, which relieves us of having to write `.val` on the right-hand
   -- side of the monadic let.
   let v := vec_new Nat
-  let x: vec Nat ← (vec_push_back_old Nat v 1: result (vec Nat)) -- WHY do we need the type annotation here?
+  let x: vec Nat ← (vec_push_back_old Nat v 1: Result (vec Nat)) -- WHY do we need the type annotation here?
   -- TODO: strengthen post-condition above and do a demo to show that we can
   -- safely eliminate the `fail` case
   return (vec_len Nat x)
 
-def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α)
+def vec_push_back (α : Type u) (v : vec α) (x : α) : Result (vec α)
   :=
   if h : List.length v.val + 1 <= 4294967295 then
     return ⟨ List.concat v.val x,
@@ -295,13 +295,13 @@ def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α)
   else
     fail maximumSizeExceeded
 
-def vec_insert_fwd (α : Type u) (v: vec α) (i: USize) (_: α): result Unit :=
+def vec_insert_fwd (α : Type u) (v: vec α) (i: USize) (_: α): Result Unit :=
   if i.val < List.length v.val then
     .ret ()
   else
     .fail arrayOutOfBounds
 
-def vec_insert_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α) :=
+def vec_insert_back (α : Type u) (v: vec α) (i: USize) (x: α): Result (vec α) :=
   if i.val < List.length v.val then
     .ret ⟨ List.set v.val i.val x, by
       have h: List.length v.val < USize.size := v.property
@@ -311,25 +311,25 @@ def vec_insert_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α
   else
     .fail arrayOutOfBounds
 
-def vec_index_fwd (α : Type u) (v: vec α) (i: USize): result α :=
+def vec_index_fwd (α : Type u) (v: vec α) (i: USize): Result α :=
   if h: i.val < List.length v.val then
     .ret (List.get v.val ⟨i.val, h⟩)
   else
     .fail arrayOutOfBounds
 
-def vec_index_back (α : Type u) (v: vec α) (i: USize) (_: α): result Unit :=
+def vec_index_back (α : Type u) (v: vec α) (i: USize) (_: α): Result Unit :=
   if i.val < List.length v.val then
     .ret ()
   else
     .fail arrayOutOfBounds
 
-def vec_index_mut_fwd (α : Type u) (v: vec α) (i: USize): result α :=
+def vec_index_mut_fwd (α : Type u) (v: vec α) (i: USize): Result α :=
   if h: i.val < List.length v.val then
     .ret (List.get v.val ⟨i.val, h⟩)
   else
     .fail arrayOutOfBounds
 
-def vec_index_mut_back (α : Type u) (v: vec α) (i: USize) (x: α): result (vec α) :=
+def vec_index_mut_back (α : Type u) (v: vec α) (i: USize) (x: α): Result (vec α) :=
   if i.val < List.length v.val then
     .ret ⟨ List.set v.val i.val x, by
       have h: List.length v.val < USize.size := v.property
@@ -364,7 +364,7 @@ def assertImpl : CommandElab := fun (_stx: Syntax) => do
   runTermElabM (fun _ => do
     let e ← Term.elabTerm _stx[1] none
     logInfo (Expr.dbgToString e)
-    -- How to evaluate the term and compare the result to true?
+    -- How to evaluate the term and compare the Result to true?
     pure ())
   -- logInfo (Expr.dbgToString (``true))
   -- throwError "TODO: assert"
-- 
cgit v1.2.3