Re: Typechecking I

[Andy Wingo <wingo@pobox.com>]

Hi,

Just some superficial notes while reading your code :)

On Tue 16 Nov 2010 00:10, Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> (define-module  (language prolog typecheck equationalize)
>   #:use-module (srfi srfi-1                    )
>   #:use-module (ice-9 pretty-print             )  
>   #:use-module (ice-9 match                    )  
>   #:use-module (ice-9 receive                  )
>   #:export (equationalize check))

Thanks for making it depend on only modules in Guile :-)

The extra spaces before the close-parens should be removed, though.

> (define-syntax rlet

This is usually known as let-values, fwiw.

> (define (compute-type Const Code)  
>   (define (type? X) (and (symbol? X) (char-upper-case? (car (string->list (symbol->string X))))))

Try to keep your lines to less than 80 characters, please :)

>   (define (gen-map Code Bind Lam)
>     (match Code
>            ([X . L]     (gen-map X Bind (lambda (Bind) (gen-map L Bind Lam))))

The conventional indentation for this is:

      (match Code
        ([X . L]  ...))

If your emacs doesn't do this, add this to your .emacs:

  (put 'match 'scheme-indent-function 1)

> (define (check X)
>   (rlet ((A          X)
>          ((Ba Ea)   (equationalize '() '() A 'Texp)))
>         (pp A)

Likewise for rlet -- though it should be just let*-values, if it were a
macro of your own, you could add a similar block to the .emacs.

>   (match Expr
>          (['and X Y]   (let ((F1 (equationalize-bool Bind Eq X))
>                              (F2 (equationalize-bool Bind Eq Y)))
>                          (lambda (X) 
>                            (if X 
>                                (rlet (((Bind1 Eq1) (F1 #t))
>                                       ((Bind2 Eq2) (F2 #t)))
>                                   (values (union Bind1 Bind2) `(and ,Eq1 ,Eq2)))
>                                (rlet (((Bind1 Eq1) (F1 #f))
>                                       ((Bind2 Eq2) (F2 #f)))
>                                   (values (union Bind1 Bind2) `(or  ,Eq1 ,Eq2)))))))
>
>          (['or X Y]    (let ((F1 (equationalize-bool Bind Eq X))
>                              (F2 (equationalize-bool Bind Eq Y)))
>           

Here again, much more conventional would be

    (match Expr
      (['and X Y]
       (let ((F1 (equationalize-bool Bind Eq X))
             (F2 (equationalize-bool Bind Eq Y)))
         (lambda (X) 
           (if X 
               (rlet (((Bind1 Eq1) (F1 #t))
                      ((Bind2 Eq2) (F2 #t)))
                 (values (union Bind1 Bind2) `(and ,Eq1 ,Eq2)))
               (rlet (((Bind1 Eq1) (F1 #f))
                      ((Bind2 Eq2) (F2 #f)))
                 (values (union Bind1 Bind2) `(or ,Eq1 ,Eq2)))))))

      (['or X Y]
       ...))

Your style is has gotten a lot more readable, for which I am grateful :)
There is still some small ways to go yet, though.

Syntactically yours,

Andy
-- 
http://wingolog.org/