automatic position

Author: janmasrovira

AVM/Action/DummyResource.lean

@@ -1,5 +1,6 @@
 import Prelude
 import Anoma
+import Anoma.Logic
 
 namespace AVM.Action
 
@@ -16,6 +17,8 @@ def isDummyResource (res : Anoma.Resource) : Bool :=
   res.ephemeral &&
   res.quantity == 0
 
+#check Anoma.Logic.Error.rawError
+
 /-- The resource logic of any dummy resource. -/
 private def dummyResourceLogic : Anoma.Logic :=
   { reference := dummyResourceLogicRef,

AVM/Class/Translation/Logics.lean

@@ -298,6 +298,9 @@ private def logicFun
   (args : Logic.Args)
   : Anoma.LogicM :=
   let try self : Object classId := Object.fromResource args.self
+    failwith throw (.custom here# s!"Failed to decode self to an Object:
+                                     {repr args.self}"
+      )
   check eco.classes classId |>.invariant self args
   match args.status with
   | Created => .true

Anoma/Logic.lean

@@ -2,6 +2,17 @@ import Anoma.Resource
 
 namespace Anoma
 
+inductive Logic.Error : Type where
+  | rawError (pos : FilePosition)
+  | custom (pos : FilePosition) (msg : String)
+  -- | rawError
+
+instance : Repr Logic.Error where
+  reprPrec e _ :=
+    match e with
+    | .rawError p => repr p
+    | .custom p msg => s!"{repr p}: {msg}"
+
 structure Logic.Args : Type 2 where
   self : Resource
   status : ConsumedCreated
@@ -13,7 +24,7 @@ structure Logic.Args : Type 2 where
 
 def Logic.Args.isConsumed (d : Logic.Args) := d.status.isConsumed
 
-abbrev LogicM : Type := Except String Unit
+abbrev LogicM : Type := Except Logic.Error Unit
 
 abbrev LogicM.true : LogicM := pure .unit
 

Anoma/Program.lean

@@ -29,7 +29,7 @@ structure Program.Error.BalanceCheck : Type 2 where
 inductive Program.Error : Type 2 where
   | identityError (msg : String)
   | storageError (msg : String)
-  | logicFailed (logRef : LogicRef) (reason : String)
+  | logicFailed (logRef : LogicRef) (reason : Logic.Error)
   | missingLogic (ref : LogicRef)
   | balanceCheck (err : Program.Error.BalanceCheck)
   | typeError (msg : String)

Applib/Surface/Program/Syntax.lean

@@ -21,7 +21,7 @@ def findProof (scope : Term) : TacticM Unit := do
   let possibleIndices : List (Fin card) := List.finRange card
   let tryN (n : Fin card) : TacticM Unit := do
     let sn := Syntax.mkNumLit (toString n)
-    let labelId ← `(term| $f $sn)
+    let labelId : TSyntax `term ← `(term| $f $sn)
     let t ← `(tactic| try exact ⟨$labelId, by rfl⟩)
     evalTactic t
   for x in possibleIndices do

Prelude/CustomDefault.lean

@@ -6,18 +6,23 @@ open Elab.Tactic Meta
 
 elab "mydefault" : tactic => do
    let tgt ← getMainTarget
-   if tgt.isAppOf `LogicM
+   -- logInfo s!"unchecked default {tgt}"
+   if tgt.isAppOf `Anoma.LogicM
      then
-        let t ← `(tactic| exact (throw here#))
+        -- logInfo "XXXXXXXX unchecked default"
+        let rawErr : TSyntax `term := mkIdent `Anoma.Logic.Error.rawError
+        let t ← `(tactic| exact (throw ($rawErr here#)))
         evalTactic t
      else do
       let t ← `(tactic| exact default)
       evalTactic t
 
 elab "mydefaultM" : tactic => do
    let tgt ← getMainTarget
+   -- logInfo "mydefaultM"
    if tgt.isAppOf `LogicM
      then
+        -- logInfo "MMMMMMM  unchecked default M"
         let t ← `(tactic| exact (throw here#))
         evalTactic t
      else do

Prelude/Debug.lean

@@ -2,14 +2,26 @@ import Lean
 
 open Lean
 
+structure FilePosition where
+  file : String
+  pos : Position
+  deriving ToExpr
+
+instance : Repr FilePosition where
+  reprPrec p _ := s!"{p.file}:{p.pos.line}:{p.pos.column}"
+
+def FilePosition.unknown : FilePosition where
+  file := "<unknown-file>"
+  pos := ⟨0, 0⟩
+
+-- returns FilePosition for the location where it is inserted
 elab "here#" : term => do
   let file ← getFileName
   let ref ← getRef
-  let some pos := ref.getPos?
-    | return mkStrLit "<unknown position>"
   let fm ← getFileMap
-  let lc := fm.toPosition pos
-  return mkStrLit s!"{file}:{lc.line}:{lc.column}"
-
-instance (priority := high) [Pure m] : Inhabited (ExceptT String m α) where
-  default := pure (f := m) (throw here#)
+  let some pos := ref.getPos?
+    | return (toExpr FilePosition.unknown)
+  let lc : FilePosition :=
+         { file
+           pos := fm.toPosition pos }
+  return (toExpr lc)