[plt-scheme] redex: meta-function with alternatives

From: Eric Tanter (etanter at dcc.uchile.cl)
Date: Fri Sep 11 19:46:47 EDT 2009

Hi,

I want to define a simple recursive metafunction, but which has the  
particularity of needing to somehow backtrack. It is doing a lookup in  
terms, but some terms have two branches, and if the first one fails,  
it should go in the second one.

I see two options to do it:
- use exception handling (the "not found in first branch" case being  
caught as a "no match for clause...")
- have a base case returns #f, and then somehow distinguish whether  
the recursive call returned a normal term or #f, if normal term return  
it, otherwise go through second branch.

I actually can't figure out how to make either case work... I imagine  
the latter solution is cleaner than exceptions, but couldn't make it  
work (with term-let).

This is a simplified version of what I have:

(define-metafunction foo
   lookup : os f S -> any
   ;; lookup f in os
   ; os = (def f v)
   ((lookup (def f v) f (store (l os) ...)) v)

   ; 'fail case'
   ((lookup (def f_1 v) f_2 (store (l os) ...)) #f
    (side-condition (not (eq? (term f_1) (term f_2)))))

   ; os = (with os1 os2)
   ((lookup (with os_1 os_2) f (store (l_3 os_3) ...))

     ;; try that first
      (lookup os_2 f (store (l_3 os_3) ...)

     ;; if above fails (exception or #f) then try that:
      (lookup os_1 f (store (l_3 os_3) ...))
)

any idea?

Thanks in advance,

-- Éric




Posted on the users mailing list.