Walnut/Advanced Topics/Build your Own Guards

From Erights

Build Your Own Guards

# E template

 def simple_guard {
   to coerce(specimen, optEjector) :near {
     if (specimen fits criteria) {
       return specimen
     } else {
       throw.eject(optEjector, "Specimen didnt fit criteria")
     }
   }
 }

First, here is a simple guard that matches integer strings and converts them to integers:

def asInt {
  to coerce(specimen, optEjector) :int {
    try {
      return __makeInt(specimen :String)
    } catch ex {
      throw.eject(optEjector, ex)
    }
  }
}

You can use it like this:

def str := "5 + 7 = 12"
def `@{a:asInt} + @{b:asInt} = @{c:asInt}` := str
require(a + b == c)

Now for a more complicated example...

Here is the emaker that makes a pair of VOC claim check guards, a proveAuth (i.e., a claimCheck), and a checkAuth (i.e., a checkedClaim):

# E sample

def makeVOCPair(brandName :String) :near {

    var myTempContents := def none {}

    def brand {
        to __printOn(out :TextWriter) :void {
            out.print(brandName)
        }
    }

    def ProveAuth {
        to __printOn(out :TextWriter) :void {
            out.print(`<$brandName prover>`)
        }
        to getBrand() :near { return brand }
        to coerce(specimen, optEjector) :near {
            def sealedBox {
                to getBrand() :near { return brand }
                to offerContent() :void {
                    myTempContents := specimen
                }
            }
            return sealedBox
        }
    }
    def CheckAuth {
        to __printOn(out :TextWriter) :void {
            out.print(`<$brandName checker template>`)
        }
        to getBrand() :near { return brand }
        match [`get`, authList :any[]] {
            def checker {
                to __printOn(out :TextWriter) :void {
                    out.print(`<$brandName checker>`)
                }
                to getBrand() :near { return brand }
                to coerce(specimenBox, optEjector) :any {
                    myTempContents := null
                    if (specimenBox.__respondsTo("offerContent", 0)) {
                      # XXX Using __respondsTo/2 here is a kludge
                        specimenBox.offerContent()
                    } else {
                        myTempContents := specimenBox
                    }
                    for auth in authList {
                        if (auth == myTempContents) {
                            return auth
                        }
                    }
                    myTempContents := none
                    throw.eject(optEjector,
                                `Unmatched $brandName authorization`)
                }
            }
        }
        match [`__respondsTo`, [`get`, _]] {
            true
        }
        match [`__respondsTo`, [_, _]] {
            false
        }
        match [`__getAllegedType`, []] {
            null.__getAllegedType()
        }
    }
    return [ProveAuth, CheckAuth]
}

Now here is an example of the pair of VOC guards in use:

? def [ProveAuth, CheckAuth] := <elib:sealing.makeVOCPair>("voc")
     # value: [<voc prover>, <voc checker template>]
 
     ? def f1 := <file:~/.bashrc>
     # value: <file:c:/Documents and Settings/millerm1/.bashrc>
 
     ? def f2 := <file:~/Desktop>
     # value: <file:c:/Documents and Settings/millerm1/Desktop/>
 
     ? def foo(f :CheckAuth[f1,f2]) :void {
     >     println(f.getPath())
     > }
     # value: <foo>
 
     ? foo(f1)
     # stdout: c:/Documents and Settings/millerm1/.bashrc
     #
 
     ? def f3 := <file:~>
     # value: <file:c:/Documents and Settings/millerm1/>
 
     ? foo(f3)
     # problem: Unmatched voc authorization
 
     ? foo(f1 :ProveAuth)
     # stdout: c:/Documents and Settings/millerm1/.bashrc
     #
 
     ? foo(f3 :ProveAuth)
     # problem: Unmatched voc authorization
 
     ? def bar(f) :void {
     >     println(f.getPath())
     > }
     # value: <bar>
 
     ? bar(f1)
     # stdout: c:/Documents and Settings/millerm1/.bashrc
     #
     
     ? bar(f1 :ProveAuth)
     # problem: <NoSuchMethodException: <a sealedBox>.getPath/0>