1  (define (instance-of? pattern-term)
  2    (lambda (test-term)
  3      ))
  4  
  5  (define o ...)
  6  
  7  (check ((instance-of? (term (o unbound)))
  8          (term (o unbound)))
  9         => #T)
 10  (check ((instance-of? (term (o unbound1)))
 11          (term (o unbound2)))
 12         => #F)
 13  (check ((instance-of? (term (o unbound)))
 14          (let () (term (o unbound))))
 15         => #T)
 16  
 17  (check ((instance-of? (term o))
 18          (let ((z o)) (term z)))
 19         => #T)
 20  (check ((instance-of? (term o))
 21          (let ((o +)) (term o)))
 22         => #F)
 23  
 24  (let-type ((a integer?))
 25    (check ((instance-of? (term (o a)))
 26            (o 1))
 27           => #T)
 28    (check ((instance-of? (term (o a)))
 29            (let-type ((b integer?)) (o b)))
 30           => #T))
 31  
 32  HOW?
 33  (let-type ((a number?))
 34    (check ((instance-of? (term (o a)))
 35            (o 1))
 36           => #T)
 37    (check ((instance-of? (term (o a)))
 38            (let-type ((b integer?)) (o b)))
 39           => #T))
 40  
 41  So, instance-of? requires bunch (type) inclusion operator/predicate
 42  
 43  (check (includes? 1 naturals) => #T)
 44  (check (includes? naturals integers) => #T)
 45  (check (includes? rationals numbers) => #T)
 46  
 47  But implementing includes? completely requires other advanced/built-up facilities such as known-value evaluation (to use axioms like (includes? naturals integers)) which requires matching terms against each other, which is what instance-of? does.  So a more primitive means of matching terms is required to avoid the cyclic dependency.
 48  
 49  
 50  
 51  Idea: (term ...) constructs new term value only if same term not already registered in environment, if already registered then returns registered term.  This seems to allow the way of identifying registered terms by their symbolic structure like bound values are identified by symbols, without the ambiguity of whether a syntax means to evaluated by default method (Kernel semantics) or means to find a registered term and yield its value.
 52  
 53  With the above term idea and a basic term matcher, much could be built on these I think.  Maybe with only above term idea, eq? is useful basic term matcher?:
 54  
 55  (check (eq? (term o) (term o)) => #T)
 56  (check (eq? (term o) (let () (term o))) => #T)
 57  
 58  But for term to find registered term, some way of basic matching other than eq? is required.
 59  
 60  But how is a term initially registered in an environment?  letrec is not needed/desired for terms, so some sort of functional fold cons'ing to extend environments sounds good, such as a sequence operative that evaluates successive expressions in env extended by previous expressions in the sequence:
 61  
 62  ($context  ; maybe name it something else
 63   ($term/value (includes? naturals integers) #T)
 64   ($term (includes? naturals integers)))
 65  =>
 66  #[term form = (includes? naturals integers)
 67         env = <the-dyn-env>
 68         value = #T]
 69  
 70  But what about issues like?:
 71  ($context
 72   ($term/value a #T)
 73   ($term/value a #F))
 74  Or?:
 75  (context
 76   (term/vaue o ...)
 77   (let ((o ...different...))
 78     (term o)))
 79  
 80  If term strucs are used for all environment bindings, then
 81  ($context ($term/value a 1) a)
 82  is equivalent to
 83  (let ((a 1)) a)
 84  and
 85  (let ((a 1)) (term a))
 86  is equivalent to
 87  ($context ($term/value a 1) (term a))
 88  
 89  
 90  
 91  (define term
 92    (vau (form) env
 93      (if (env-ref ))))
 94  
 95  
 96  
 97  
 98  Need sophisticated matching and binding that does destructuring-binding as well as equality matching of symbols, terms, and arbitrary objects, as well as binding terms to values.  Trying to have both equality matching and binding of terms requires syntax that distinguishes these uses.  Maybe matching of symbols should just be a case of term matching where the symbol is unbound in the pattern's static environment.  Maybe predicate matching should use the fundamental facility of binding terms to type predicates (but not values) if I decide to have this facility.
 99  
100  Pattern ideas:
101  
102  (a) ; any list of length 1, binds a
103  ('a) ; any list of length 1, binds (term a) 
104  (,a) ; any list of length 1 if car matches predicate a evals to
105  (,'a) ; any list of length 1 if car matches (term a)
106  
107  (,'= (o1 . opnds1) (o1 . opnds1))
108  
109  But a lot of desired checking is too complicated to specify in patterns anyway, so why have patterns more sophisticated than just the needed binding of terms and variables to values or types?
110  
111  
112  
113