4 Responses to “Term.lhs”

1. Conor says:

   20/01/2005 at 10:06 am

   I’ve hacked up the basics of the operational behaviour. Next up, a wee parser and printer, so we can have a bit of a play.
2. Conor says:

   20/01/2005 at 1:56 pm

   Module TermParser now contains a highly incomplete parser for fully elaborated raw terms, extracting them as a subset of the concrete syntax, given a resolver for names. You can try it out in ghci thus:

   *TermParser> testTermParser
all _X : * => all x : X => X
STOP
B (All,Impl) (R *) (Sc (B (All,Expl) (V 0) (Sc (V 1))))

3. pwm says:

   20/01/2005 at 2:28 pm

   Sorry Conor I added code tags to that comment, feel free to reverse this :)
4. Conor says:

   23/01/2005 at 10:33 pm

   More excitement!

   
*TermParser> testTermParser
(λ X : * ⇒ (λ x : X ⇒ (λ y : X ⇒ *) x)) * : ∀ x : * ⇒ *
STOP
Term = E (B (Lam,Expl) (R TT.*) (Sc (B (Lam,Expl) (V 0) (Sc (E (B (Lam,Expl) (V 1) (Sc (R TT.*))) (A (V 0))))))) (A (R TT.*))
Whnf = B (Lam,Expl) (R TT.*) (Sc (E (B (Lam,Expl) (R TT.*) (Sc (R TT.*))) (A (V 0))))
Norm = B (Lam,Expl) (R TT.*) (Vac (R TT.*))
Type = B (All,Expl) (R TT.*) (Sc (R TT.*))


   The test routine now takes term : type. It’s your responsibility to be accurate, as there’s no checker yet. You get back the Haskell show of the term, its whnf, its normal form and the type you supplied. The type is necessary (in general) for the quotation operation. Quotation of Whnv to get a whnf is very cheap, as it’s only skin deep. Quotation of normal forms requires a deeper traversal, and a name supply. However, a little inspired by the ∇-ists, I knocked up this little gadget

   nu :: (IKnow i FreshRoot, Abstract t s) ⇒
  Value → (Value → i t) → i s
nu ty f = iknow $ λ (FreshRoot (nom, i)) →
  let noo = (nom /. ("x", i)) := Purple ty
  in iI (noo ) (iknew (FreshRoot (nom, i + 1))
   (f (vR noo))) Ii


   nu’s type is more informative, on the face of it: working in any idiom with a name supply, nu ty f gives you the scope-like thing made by abstracting x from (f x) where x is a fresh variable of type ty. Though I say so myself, the nice thing is that the new free variable doesn’t leak: by the time it reaches the outside world, it’s been bound again!