The progress of hacking guile and prolog

The progress of hacking guile and prolog

[Stefan Israelsson Tampe]

Hi,

I think it's good to discuss what I do with the prolog and unifer. So this
is what I've been doing.

1. Incorporate a theorem prover for extension and playing
2. Kanren like hygienic macro package
3. Make the c-code variables printable and hence much less segfaults at bt :-)
   e.g. robustify
4. Hygienify the fast umatcher.
5. try to design a type checker mimiking typed racket.
6. Play with compiled guile vm code to check for speed
7. Redesign and unugglify and improve the main prolog compiler
8. Introduce interesting features like higher order functional behavior.
9. Move the code over closer to guile Head.

Hew oh well, thats feels like a lot, let's check it out.

1. The theorem prover (leanCop) is a nice exercise to incorporate and use 
because it uses quite a lot of prolog features and beeing able to compile that 
into working code led me back to read up about some of my ignorantic parts of 
prolog I've not setled here how to solve it. the thing is that one meld the
operator parser in prolog to whatever one may like and use that to parse 
general code. I really don't like that the core languge changes behavior as
you parse language x, and added a feature where the parser enters a new
context e.g. the parsing language x and hence one can separate the two. This 
is 
not iso behavior although you can still modify the core language. There will
be incompabilities but you can give the users some advice how to avoid these
by using parenthesises. I think that this is a design choise for the better 
though. Anyhow with some luck there will be a code prover for guile in a
couple of years :-)

2. Kanren is a nice way to program like with prolog, but using code more true
to scheme. So I've been working with a hygienic macro package that should 
give such a feature. These macros will then be used in the prolog compiler 
to beutyfy it. I reallt think that this is the right way and really like 
what I've churn out so far.

3. The speedy umatch thingy was quite terrible to work with because it entered 
these home cooked c variables into guile which just segfaulted when trying to 
print it. (ugly) Anyway the print routine was hacked in my repo to print the 
it better. Still there probably are some dragons sleeping here but at least
the coding experience is much better.

4. The umatch hackity hack was turned into a much more hygienic creature. Not 
perfect but at least it should now play much nicer with the macro system. The 
key issue was that everything was a defmacro (i did not now better then) and
the matcher introduced syntactics from outer s(pace)cope so it was not to just
bless the beast with (datum->syntax). One needed to take the x in
(syntax->datum x) and split it up, tryying to keep bits of syntactic
information to transfer it into the old macro compiler. Here comes a 
pretty cool hack actually. Consider the following module:

-----------------------------------------------------------
(define-module (ice-9 syntax-matcher)
  #:use-module (ice-9 match-phd-lookup)
  #:export     (match-syntax-hack))


(define (syntax-null?  x  ) (null? (syntax->datum1 x)))
(define (syntax-equal? x y) (equal? (syntax->datum1 x) y))
(define (syntax-id x)
  (define (syntax? x) (not (eq? x (syntax->datum1 x))))
  (if (pair? x) 
      x
      (let ((r (syntax->datum1 x)))
        (if (pair? r)
            (let ((h (if (syntax? (car r)) (car r) (datum->syntax x (car r))))
                  (l (if (syntax? (cdr r)) (cdr r) (datum->syntax x (cdr 
r)))))
              (cons h l))
            x))))

          
(make-phd-matcher match-syntax-hack ( (car cdr pair? syntax-null?
syntax-equal? syntax-id) ()))
------------------------------------------------------------


syntax->datum1 transfer a syntax object to a datum for only it's root, e.g. it 
does not try to make everything a datum.

id is a lookup creature and match-phd-lookup is a modded match generator that
uses custom lookup or syntax-id as I call it. it's just an unpacking command 
that is done befor car cdr and pair? is executes like

(let ((v (lookup v))) (if (pair? v) (f (car v) (cdr v))))

so it's a stupid efficiency hack so that we don't lookup all the time. Now
syntax id will open up a pair and if some of them it's children is not of a
syntax kind it will bless the child with the syntax of the parent syntax 
object. Now with this matcher I want to chop up the following structure 

(arg1 ... argn ((pat1, ..., patn code) ...))

and can then use:

(define (my-unsyntax X)
  (define (unsyntax2 X)
    (define (unsyntax3 X)
      (define (unsyntax4 X)
        (match-syntax-hack X
           (('unquote  X)     (list 'unquote  X))
           (('uunquote X)     (list 'uunquote X))
           (('?        X)     (list '?        X))
           (('=  X     P)     (list '=        X (unsyntax4 P)))
           (('?  X P    )     (list '?        X (unsyntax4 P)))
           ((H . L)           (cons (unsyntax4 H) (unsyntax4 L)))
           ( H                (syntax->datum1 H))))

      (match-syntax-hack X
         ((Code)     (cons Code '()))
         ((M . L)    (cons (unsyntax4 M) (unsyntax3 L)))))

          
    (match-syntax-hack X
       ((X . L)  (cons (unsyntax3 X) (unsyntax2 L)))
       (()      '())))

  (match-syntax-hack X
      ( (X)     (cons (unsyntax2 X) '()))
      ( (X . L) (cons X (my-unsyntax L)))))

It's not perfect syntaction but it is vastly better then before and the code 
is yum yum.

5) Typechecking is for safty and optimisation, in the end it can be cool to 
have and I'm working to understand all sides of this and have a pretty good 
idea what is needed. It will be a goos testcase for the code.

6) I copied the  glil->assembly compiler and modded the code to spit out 
c-code in stead of assembly. For functions which does not call other scheme
functions except in tail call manner this should be quite fast to adapt. And
of cause loops becomes wickedly fast when compiling this way. Wingo:s example 
without consing tok 7ns for each loop on my machine. (For cleaned up C it
should be less then 1 ns) Kind of interesting and a nice playground to try 
out optimisations directed by type inference.

7,8,9. No more to say but that you rock, upgrading to guile head was really
a nice experience.


Now I will continue to struggle with these topics for some time (I also hope 
to return to the postpone topic but to get the core in shape has higher 
priority)

Happy Hacking : - )
/Stefan

Re: The progress of hacking guile and prolog

[Ludovic Courtès]

Hi Stefan,

Lots of stuff here, which is why I took the time to read it.  :-)

Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> 1. The theorem prover (leanCop) is a nice exercise 

[...]

> 2. Kanren is a nice way to program like with prolog,

Great that you’re mentioning them.  It looks like there’s a lot of
interesting work that’s been done around Kanren, such as the “toy” type
inference engine and, better, αleanTAP.  I don’t grok it all I’m glad
you’re looking at it from a Guile perspective.  :-)

> 4. The umatch hackity hack was turned into a much more hygienic creature.

Funny sentence.  :-)

> 5) Typechecking is for safty and optimisation, in the end it can be cool to 
> have and I'm working to understand all sides of this and have a pretty good 
> idea what is needed. It will be a goos testcase for the code.

Yes, if the type inference engine that comes with Kanren could somehow
be hooked into Guile’s compiler, so that it can emit type-mismatch
warnings or determine whether type-checks can be optimized away (which
would require changes in the VM), that’d be great.

What’s amazing is that Kanren + type-inference.scm weigh in at “only”
~3,500 SLOC.

> 6) I copied the  glil->assembly compiler and modded the code to spit out 
> c-code in stead of assembly. For functions which does not call other scheme
> functions except in tail call manner this should be quite fast to adapt. And
> of cause loops becomes wickedly fast when compiling this way. Wingo:s example 
> without consing tok 7ns for each loop on my machine.

Interesting.  Is it a sufficiently isolated change that you could point
us to?

Thanks,
Ludo’.

Re: The progress of hacking guile and prolog

[Noah Lavine]

Hello all,

Not to derail the thread of discussion, but I've had an idea for a
feature bouncing around that I think might hook into this. I think
that Guile should offer optional static checking - not just of types,
but of everything that we can check. It could be used partly for
optimization, but partly also as a way to verify that you're reasoning
about the program correctly. (Like assert, but you prove things
correct.) For instance,

(define (map func list)
    (check (= (arity func) 1))
    ....)

or

(define (search-binary-search-tree tree key)
    (check (binary-search-tree? tree) ; or whatever conditions make sense
    ....)

I'm afraid I don't know much about how theorem provers like that would
be used to make static checkers, but is there a way to use LeanCOP or
Kanren to provide something like this? I think the easiest interface
would be one where you could put arbitrary Scheme code in check
statements, but the prover would be able to reject it as "unable to
check this", in which case it could insert a runtime check (if you
asked it to).

On a completely different note, I'm now looking at writing a compiler
for a subset of C, which could eventually become a JIT compiler. If we
could attach your GLIL->C compiler to that, it could produce a full
Scheme->machine code compiler in Guile.

Noah

On Wed, Nov 3, 2010 at 7:43 PM, Ludovic Courtès <ludo@gnu.org> wrote:
> Hi Stefan,
>
> Lots of stuff here, which is why I took the time to read it.  :-)
>
> Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:
>
>> 1. The theorem prover (leanCop) is a nice exercise
>
> [...]
>
>> 2. Kanren is a nice way to program like with prolog,
>
> Great that you’re mentioning them.  It looks like there’s a lot of
> interesting work that’s been done around Kanren, such as the “toy” type
> inference engine and, better, αleanTAP.  I don’t grok it all I’m glad
> you’re looking at it from a Guile perspective.  :-)
>
>> 4. The umatch hackity hack was turned into a much more hygienic creature.
>
> Funny sentence.  :-)
>
>> 5) Typechecking is for safty and optimisation, in the end it can be cool to
>> have and I'm working to understand all sides of this and have a pretty good
>> idea what is needed. It will be a goos testcase for the code.
>
> Yes, if the type inference engine that comes with Kanren could somehow
> be hooked into Guile’s compiler, so that it can emit type-mismatch
> warnings or determine whether type-checks can be optimized away (which
> would require changes in the VM), that’d be great.
>
> What’s amazing is that Kanren + type-inference.scm weigh in at “only”
> ~3,500 SLOC.
>
>> 6) I copied the  glil->assembly compiler and modded the code to spit out
>> c-code in stead of assembly. For functions which does not call other scheme
>> functions except in tail call manner this should be quite fast to adapt. And
>> of cause loops becomes wickedly fast when compiling this way. Wingo:s example
>> without consing tok 7ns for each loop on my machine.
>
> Interesting.  Is it a sufficiently isolated change that you could point
> us to?
>
> Thanks,
> Ludo’.
>
>
>

Re: The progress of hacking guile and prolog

[Stefan Israelsson Tampe]

On Thursday, November 04, 2010 03:40:09 am Noah Lavine wrote:
> Hello all,
> 
> Not to derail the thread of discussion, but I've had an idea for a
> feature bouncing around that I think might hook into this. I think
> that Guile should offer optional static checking - not just of types,
> but of everything that we can check. It could be used partly for
> optimization, but partly also as a way to verify that you're reasoning
> about the program correctly. (Like assert, but you prove things
> correct.) For instance,
> 
> (define (map func list)
>     (check (= (arity func) 1))
>     ....)
> 
> or
> (define (search-binary-search-tree tree key)
>     (check (binary-search-tree? tree) ; or whatever conditions make sense
>     ....)
> 
> I'm afraid I don't know much about how theorem provers like that would
> be used to make static checkers, but is there a way to use LeanCOP or
> Kanren to provide something like this? I think the easiest interface
> would be one where you could put arbitrary Scheme code in check
> statements, but the prover would be able to reject it as "unable to
> check this", in which case it could insert a runtime check (if you
> asked it to).

I think that we have similar synaptical fireworks here. The actual 
implementation and syntax should be a result of understanding the line of 
reasoning in these theorem povers and checkers. So let my try to explain what
I'm heading. I will try to write a little about where I am in a few days and
we can continue the discussion then.


> On a completely different note, I'm now looking at writing a compiler
> for a subset of C, which could eventually become a JIT compiler. If we
> could attach your GLIL->C compiler to that, it could produce a full
> Scheme->machine code compiler in Guile.

Shall we say that you implement a JIT compiler and I progress with the glil->c 
stuff. I was uncertain an a little afraid that I toed you here. 

/Stefan

Re: The progress of hacking guile and prolog

[Noah Lavine]

Hello,

> I think that we have similar synaptical fireworks here. The actual
> implementation and syntax should be a result of understanding the line of
> reasoning in these theorem povers and checkers. So let my try to explain what
> I'm heading. I will try to write a little about where I am in a few days and
> we can continue the discussion then.

Great!

> Shall we say that you implement a JIT compiler and I progress with the glil->c
> stuff. I was uncertain an a little afraid that I toed you here.

That sounds good. In general though, please don't worry about treading
on my territory or anything like that. I will be happy as long as
Guile gets new features, and I am fine not being the person who writes
them.

Noah

Re: The progress of hacking guile and prolog

[Ludovic Courtès]

Hi,

Noah Lavine <noah.b.lavine@gmail.com> writes:

> On a completely different note, I'm now looking at writing a compiler
> for a subset of C, which could eventually become a JIT compiler. If we
> could attach your GLIL->C compiler to that, it could produce a full
> Scheme->machine code compiler in Guile.

Interesting.  I thought you were going rather to compile a subset of
Scheme to C, which could be used to implement VM instructions, no?

Thanks,
Ludo’.

Re: The progress of hacking guile and prolog

[Noah Lavine]

Yes, that's right. I was unclear. I am intending to come up with a
language that I can compile to C, to implement VM instructions. I
meant I would compile something to C, not from it to machine code.

Just to clarify, it probably won't be a subset of Scheme (although one
could compile a subset of Scheme to this language). I was thinking of
something more like register transfer language, so the compiler will
be very simple.

Noah

On Thu, Nov 11, 2010 at 11:26 AM, Ludovic Courtès <ludo@gnu.org> wrote:
> Hi,
>
> Noah Lavine <noah.b.lavine@gmail.com> writes:
>
>> On a completely different note, I'm now looking at writing a compiler
>> for a subset of C, which could eventually become a JIT compiler. If we
>> could attach your GLIL->C compiler to that, it could produce a full
>> Scheme->machine code compiler in Guile.
>
> Interesting.  I thought you were going rather to compile a subset of
> Scheme to C, which could be used to implement VM instructions, no?
>
> Thanks,
> Ludo’.
>
>
>

Re: The progress of hacking guile and prolog

[Noah Lavine]

> Interesting.  I thought you were going rather to compile a subset of
> Scheme to C, which could be used to implement VM instructions, no?

Yes, that was my plan, sorry. I want to compile things to C, not from
C to machine code.

Also, to clarify, I am looking at compiling not a subset of C, but
something like register transfer language. That way the compiler can
be very simple and hopefully obviously correct.

Noah

Typechecking I

[Stefan Israelsson Tampe]

[-- Attachment #1: Type: Text/Plain, Size: 4998 bytes --]

Hi,

Ok, here is a first step to analyse code.

Note,
attached to the mail is a modul /put it at a suitable place and fixup the
reference for the module. Then use e.g. (check '(if 1 1 1)) and you will get 
the output you see further down in the email.

We will assume that local variables in the following is gensymed to be unique
and no name clashes apear.

For typechecking i find it interesting to consider an equational approach
first. e.g. translate code to an equation system.

let's take a first simple step here and and assume that the typecheck function
just finds the equation we need to solve in order to understand type
consistency and discovery. we will assume that typecheck is of the form
(typecheck Eq Code Type) or in short
Eq     is current equational state, 
Code   the code to draw equations out of.
Type   the type associated with the result of Code

******************* Item I *******************************
[let X Y Z] : T

Translates to
(typecheck (typecheck Eq Y X) Z T)

Example of equation generation:
(let x 1 x):
((= integer x) (= x Texp))

(let x 1 (let y x y)):
((= integer x) (= x y) (= y Texp))

TODO: Note: (= y x) should be more nicer for the understanding!!!

This is not earthshaken. But I think it is wise to handle first such an 
translational step in order to write a solver in kanren or prolog or racklog
or guilelog :-) for the more general case.

******************* Item II ***************************
[begin x ... xx] : T

(typecheck x e) o ... o (typecheck xx T)

the symbol e will mean an anything object so that essentially [= e x] is true 
for all x. You could say everything that we have not assigned a type to has
type e and then (the idea) is that the all scheme expression should
typecheck. It remains to define the properties and rules associated with e to
make this work. The target is to be able to gradually mix typed expressions
with untyped expression.

Example:
(begin 1 "a" 1):
((= integer  e) 
 (= string   e) 
 (= integer  Texp))

******************* Item III ****************************
[lambda [x ...] code]

What to look up for here is that essentialle every usage of a lambda inside
a function has to, to be general, have a unique set of equations and do a 
unique deduction. This can be expensive, but is the correct way to treat the 
typechecking of the lambda. So we must tell the solver later on that we are 
going to treat a lambda, e.g. x ... will be a unique version at every usage
of the lambda the directive for the solver is (lambda vars res equation)
lambda conceptually translates to an abstraction of an equations.

Example
(lambda (x y) x):
((= (lambda (x y) Tlam6583 
       ((= x Tlam6583))) Texp))

********************** Item IV **************************
[apply f [x ...]] : T

First of all we need to deduce the equation of f, to yield a lambda. e.g.
(typecheck f [lamda [ArgType(x) ...] ResType]) o
(typecheck x [arg ArgType(x)]                ) o ... o
(add-equation [= [res ResType] T])

so
1. define the functional signatur.
2. find the equations typececked to [arg X], arg is a directive to the solver
   to tell it that we are equating a function argument why? well the equality
   needs to be treated differnetly in order to be correct.
3. the same reason for the addition of the last equation. we need to inform 
the
   solver that ResType is of a result type.

Example:
(apply (lambda (x y) x) (1 2)) :
((= (lambda (x y) Tlam6954 ((= x Tlam6954)))   ;; a lambda type abstraction 
    (lambda (Targ6951 Targ6952) Tres6953))     ;; a lambda type
 (= integer (arg Targ6951))
 (= integer (arg Targ6952))
 (= (res Tres6953) Texp))


Can you see how res and arg differ
(= T (arg (or A B C)))   ; argument can be A or B or C
(= T (res (or A B C)))   ; function produces A or B or C

**************** Item V *************
[if P X Y] : T

(integer? X) makes a promise that if true then X is an integer and
is a string. Consider (= (res A) (arg integer)) if the result of a function
is anything it follows that it can't unify with an argument that has to 
take an inte integer as in the case
(+ (g X) 1) and g is not typehcecked and we cannot ussume anything
about it hence the typecheck should fail. On the other hand
(if (integer? (g X)) (+ (g X) 1) #f) should be able to typecheck
against (or integer boolean) and here we would have an equality of the
type (= (validated integer) (res A)) and then A=integer in the rest of the
equations in the or.

Example:
(let x 1 (if (integer? x) "a" 2))
=================================
(= integer x)
 (or ((=  x (validated integer)) (= string Texp))
     ((=  x (validated (not integer)))
      (=  integer Texp))))



So maybe it's an unessesary step but at least I appriciate this little 
transformation to get an understanding the subject. I'll will now work
a little with solving the equations. 

And yes, all tree-il is not included, but I fix the complexity at this level
and move over to solving the equations.

Play around and have fun
/Stefan
















[-- Attachment #2: equationalize.scm --]
[-- Type: text/x-scheme, Size: 9222 bytes --]

(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))

;; the main function is equationalize, which takes a format that should be derived from 
;; tree-il representation with suitable tags to be able to communicate to the compiler
;; about type-checking conclusions. For know it's just a toy translator. The idea is to 
;; translate this code to a set of equations that later on is fed into the typechecker and
;; is a good starting point to see the type structure
;;
;; (equationalize Bindings Equations Code Outer-type)
;; To get the equations of (if 1 1 1) you would write 
;; (recieve (Bind Eq) (equationalize '() '() '(if 1 1 1) 'T-outer) ...)
;;
;; the language have just a few functions implemented for illustration
;; (number? X),(integer? X), (symbol? X), (char? X), (string? X)., (boolean? X).
;; plain simple (if X Y Z) (let Var Val Code) (lambda (x ...) code) is available as 
;; well. functions application should be written as (apply symbol? X).
;; and or and not is supported as is because they are special
;; 
;; So currently not that exciting but it is very instructive to play with a few expressions
;; an look att the corresponding equations that results. esiest is to use the check function
;; like (check Code) e.g. (check `(if 1 1 1)) which produces the type equation,

;;(if 1 1 1)
;;((or ((= 1 boolean) (= integer Texp))
;;     ((not (= 1 boolean)) (= integer Texp))))

;;Have a play!

(define (pp X)       (begin (pretty-print X) X))
(define union  (lambda (x y) (lset-union eq? x y)))

;;**************************** PRELUDE TO TYPECHECKING ***********************  

                            
;;This is just to kill of receive nesting buitifies the code alot

(define-syntax rlet
  (syntax-rules ()
    ((_ (((a ...) c) . l) code ...)
     (receive (a ...) c 
              (rlet l code ...)))
    ((_ ((a c) . l) code ...)
     (let ((a c)) 
       (rlet l code ...)))
    ((_ () code ...) (begin code ...))))


(define (compute-type Const Code)  
  (define (type? X) (and (symbol? X) (char-upper-case? (car (string->list (symbol->string X))))))
  (define (gen-map Code Bind Lam)
    (match Code
           ([X . L]     (gen-map X Bind (lambda (Bind) (gen-map L Bind Lam))))
           ((? type? X) (if (member X Bind)
                            (Lam Bind)
                            (let ((T (Const)))
                              (Lam (cons (cons X T) Bind)))))
           (_           (Lam Bind))))

  (define (make-rep X Bind)
    (match X
           ([X . L]  (cons (make-rep X Bind) (make-rep L Bind)))
           ([]       '[])
           (X        (let ((R (assoc-ref Bind X)))
                       (if R R X)))))
           
  (make-rep Code (gen-map Code '() (lambda (x) x))))

;;typecheck will create a list of equation that defines the rules for the predicates, the rules are
;; [= A B]           A and B should unify
;; [and A B] [A B]   A holds and B holds
;; [or A B]          A holds or B holds
;; [not A]           A is not true
;; [arg A]           A is an argument variable
;; [res A]           A is the result of a function
;;  e                Accepts everything
(define (equationalize Bind Eq Expr Tp)
  ;;(pp Expr)
  (match Expr
         (['let X V Code]   (rlet (((Bind Eq) (equationalize Bind Eq V X)))
                                  (equationalize (cons X Bind) Eq Code Tp  )))

         (['lambda V Code]  (rlet (( Tlam              (gensym "Tlam"))
                                   ((Bind-lam Eq-lam)  (equationalize (append V Bind) '() Code Tlam)))
                              (values Bind (cons `(= (lambda ,V ,Tlam ,Eq-lam) ,Tp) Eq))))
                               
         (['if P X Y]       (rlet ((F           (equationalize-bool Bind '() P))
                                   ((Bind1 Eq1) (F #t))
                                   ((Bind0 Eq0) (F #f))
                                   ((Bind1 Eq1) (equationalize Bind1 Eq1 X Tp))
                                   ((Bind0 Eq0) (equationalize Bind0 Eq0 Y Tp)))
                                (values (union Bind0 Bind1) (append `((or ,(reverse Eq1) ,(reverse Eq0))) Eq))))

         (['apply F A]      (rlet ((Ta        (map (lambda x (gensym "Targ")) A))
                                   (Tr        (gensym "Tres"))
                                   ((Bind Eq) (equationalize Bind Eq F `[lambda ,Ta ,Tr]))
                                   ((Bind Eq) (equationalize-arg Bind Eq A Ta)))
                               (values Bind (cons `[= [res ,Tr] ,Tp] Eq))))
         
         (['begin A]        (equationalize Bind Eq A Tp))
         (['begin A . L]    (rlet (((Bind Eq)  (equationalize Bind Eq A 'e)))
                                  (equationalize Bind Eq (cons 'begin L) Tp)))

         ((? symbol? X)     (if (member X Bind)
                                (values Bind (cons `(= ,X ,Tp) Eq))
                                (let ((Ts (symbol-property X ':type)))
                                  (if Ts
                                      (values Bind (cons `(= ,(compute-type (lambda () (gensym "T")) Ts) ,Tp) Eq))
                                      (values Bind (cons `(=  e ,Tp) Eq))))))
         
         (('quote (? symbol?))  (values Bind (cons `(= symbol    ,Tp) Eq)))
         ((? integer?)          (values Bind (cons `(= integer   ,Tp) Eq)))
         ((? boolean?)          (values Bind (cons `(= boolean   ,Tp) Eq)))
         ((? number? )          (values Bind (cons `(= number    ,Tp) Eq)))
         ((? char?   )          (values Bind (cons `(= character ,Tp) Eq)))
         ((? string? )          (values Bind (cons `(= string    ,Tp) Eq)))))

(define (check X)
  (rlet ((A          X)
         ((Ba Ea)   (equationalize '() '() A 'Texp)))
        (pp A)
        (pp (reverse Ea)))
  #t)

(define typemap  '((+ (lambda (number number) number))
                   (id (lam (A) A))
                   (- (lambda (number number) number))))

(map (lambda (x) (match x ((Sym T)  (set-symbol-property! Sym ':type T))))
     typemap)


(define (equationalize-arg Bind Eq Xs Tps)
  (match `(,Xs ,Tps)
         (([X . Xs] [Tp . Tps])   (rlet (((Bind Eq)  (equationalize Bind Eq X (list 'arg Tp))))
                                      (equationalize-arg Bind Eq Xs Tps)))
         (([]       []        )   (values Bind Eq))))


(define *predtypes*
  '((string?  string  )
    (symbol?  symbol  )
    (integer? integer )
    (number?  number  )
    (boolean? boolean )
    (char?    char    )))
  

(define (equationalize-bool Bind Eq Expr)
  (define (pred? X)
    (define (f L)
      (if (pair? L)
          (if (eq? X (caar L))
              #t
              (f (cdr L)))
          #f))
    (f *predtypes*))

  (define (type-of-pred X)
    (define (f L)
      (if (pair? L)
          (if (eq? X (caar L))
              (cadar L)
              (f (cdr L)))
          #f))
    (f *predtypes*))

  ;;(pk Expr)
  (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)))
                         (lambda (X) 
                           (if X 
                               (rlet (((Bind1 Eq1) (F1 #t))
                                      ((Bind2 Eq2) (F2 #t)))
                                  (values (union Bind1 Bind2) `(or ,Eq1 ,Eq2)))
                               (rlet (((Bind1 Eq1) (F1 #f))
                                      ((Bind2 Eq2) (F2 #f)))
                                  (values (union Bind1 Bind2) `(and  ,Eq1 ,Eq2)))))))

         (['not  X ]   (let ((F (equationalize-bool Bind Eq X)))
                         (lambda (X)
                           (if X (F #f) (F #t)))))

         ([(? pred? String?) X] (lambda (P)
                                  (if P 
                                      (equationalize Bind Eq X `(validated ,(type-of-pred String?)))
                                      (equationalize Bind Eq X `(validated (not ,(type-of-pred String?)))))))
         (X                     (lambda (P)
                                  (if P
                                      (values Bind (cons `[= ,X boolean] Eq))
                                      (values Bind (cons `[not [= ,X boolean]] Eq)))))))
                                                                                                                           






         




   
          
          

Re: Typechecking I

[Andy Wingo]

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/

Re: The progress of hacking guile and prolog

[Andy Wingo]

Hi Noah,

On Thu 04 Nov 2010 03:40, Noah Lavine <noah.b.lavine@gmail.com> writes:

> I think that Guile should offer optional static checking - not just of
> types, but of everything that we can check.

It seems like you're really asking for *dynamic* checking -- not only
checking properties that can be proved statically, without running the
program, but also runtime properties.

In this regard, I have a positive impression of the work that people are
doing on "contracts", especially the Racket folks.

    http://docs.racket-lang.org/reference/contracts.html

Happy reading,

Andy
-- 
http://wingolog.org/

Re: The progress of hacking guile and prolog

[Noah Lavine]

Hello,

That might make sense. The documentation certainly looks interesting.

What I'm thinking of is like racket contracts, but with the idea of
"trusted modules", which might involve static checking. For instance,
if the contract is that map's second parameter is a list, you'd
normally want to check that. But if a module that used map could
guarantee that it would always pass a list as the second argument,
then you'd arrange things so the second module could skip the type
check.

I'm curious in general though whether it would be possible and
worthwhile to statically check programmer-defined ideas, as long as
the interface is easy enough to use. For instance, what if you could
ask Guile to check that your tree structure always remained a binary
tree? Or better, what if you wrote a GUI program and checked that the
callbacks you passed to the GUI library would always return? (I know
it's not possible in general, but I think it will work for a subset of
procedures that will include some interesting ones.)

Noah

On Sat, Nov 20, 2010 at 6:25 AM, Andy Wingo <wingo@pobox.com> wrote:
> Hi Noah,
>
> On Thu 04 Nov 2010 03:40, Noah Lavine <noah.b.lavine@gmail.com> writes:
>
>> I think that Guile should offer optional static checking - not just of
>> types, but of everything that we can check.
>
> It seems like you're really asking for *dynamic* checking -- not only
> checking properties that can be proved statically, without running the
> program, but also runtime properties.
>
> In this regard, I have a positive impression of the work that people are
> doing on "contracts", especially the Racket folks.
>
>    http://docs.racket-lang.org/reference/contracts.html
>
> Happy reading,
>
> Andy
> --
> http://wingolog.org/
>

Re: The progress of hacking guile and prolog

[Stefan Israelsson Tampe]

Hi Noah,

On Wednesday, November 24, 2010 02:54:37 am Noah Lavine wrote:
> Hello,
> 
> That might make sense. The documentation certainly looks interesting.
> 
> What I'm thinking of is like racket contracts, but with the idea of
> "trusted modules", which might involve static checking. For instance,
> if the contract is that map's second parameter is a list, you'd
> normally want to check that. But if a module that used map could
> guarantee that it would always pass a list as the second argument,
> then you'd arrange things so the second module could skip the type
> check.

Sure static typechecking can save some time, but also note that it can bring
in applications that would not be on a scheme platform without static 
typechecking/proofing due to code safety reason imaginable or not 
(again static versus dynamic). An intersting note, one here stories about 
codebases around a popular dynamically p.l. where the test harness grow out 
of bounds and where the major part of it is test that the static typechecker 
would have been performed by default in both a much faster manner and also
more rigourusly. Personally I prefere dynamic - but that is from my usage 
pattern which is mainly smaller programs that automate. Form this I'm 
wondering if the people in this hersay really take advantage 
of testing only the relevant parts of the code in light of done changes. 

> I'm curious in general though whether it would be possible and
> worthwhile to statically check programmer-defined ideas, as long as
> the interface is easy enough to use. For instance, what if you could
> ask Guile to check that your tree structure always remained a binary
> tree? Or better, what if you wrote a GUI program and checked that the
> callbacks you passed to the GUI library would always return? (I know
> it's not possible in general, but I think it will work for a subset of
> procedures that will include some interesting ones.)

Yep I agree with you here.

Here is an idea:
You can try to say something like this function argument will never be 
returned or kept in a closure etc. Then you might allocate that object from
the stack. Again it is not always ways to proove this but sometimes you
can. So the function argument could be of a proved not proved and don't know
and you can make sure to use the safe way. Then you can guide a user to prove
that it is indeed so or let the user say it is so or just take the safe path 
and allocate from the heap. There is a nice pattern here that one could employ
when there is a compiler for guile (without compiler the speedup is not that
exiting on a relative scale). Process the code and builed up the result using
a tail call paraadigm, e.g. there is a parameter res that is constructed. Then 
at the end return (heapify (revers ret)) and transfere the constructed ret 
object to the heap by trying to fill a continuous segment on the heap by cons 
cells that is linked appropriated. That way you get some work to align objects
on the heap, allocate a big chunk at the time and the overall performance
scale and is performat. I would say that 99% of the code I write that use or
could use this pattern can be typechecked to proove that res could be builed
up from stack elements. The typical usage scenario here is to speed up 
functional (no mutating) code transformations. 

Have fun
Stefan

piper schemigan

[Stefan Israelsson Tampe]

Hi,

I'm very used to take the standart output and pipe it to grep and friends.
So I searched for this feature and I think scsh is the correct way to make 
this happen. But it have been bitrotted.

So I've hacked the sorces to.

Use guile syntax-define and cut out defmacro and friends
Use guile modules whenever possible keeping the interface as 
intact as possible, e.g use,

(ice-9 optargs)
(ice-9 regexp)
(srfi srfi-9)
(srfi srfi-9 gnu)

In stead of the scsh bag of software for these cases.

There are a few issues that I found
1. the macro run uses unquote out of a visble backquote and guile barfs
2. I was not able to use the | symbol.

Any useful comments?

Regards
Stefan

Re: piper schemigan

[Andreas Rottmann]

Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> Hi,
>
> I'm very used to take the standart output and pipe it to grep and friends.
> So I searched for this feature and I think scsh is the correct way to make 
> this happen. But it have been bitrotted.
>
> So I've hacked the sorces to.
>
> Use guile syntax-define and cut out defmacro and friends
>
Yay for getting rid of defmacro!

> Use guile modules whenever possible keeping the interface as 
> intact as possible, e.g use,
>
> (ice-9 optargs)
> (ice-9 regexp)
> (srfi srfi-9)
> (srfi srfi-9 gnu)
>
> In stead of the scsh bag of software for these cases.
>
> There are a few issues that I found
> 1. the macro run uses unquote out of a visble backquote and guile
> barfs
>
Please provide a more detailed explanation -- what exactly did you try
and what was the exact error did message you did get?  It is indeed
possible to write macros that behave as its input was implicitly
backquoted, e.g.:

(define-syntax run
  (syntax-rules ()
    ((_ command args ...)
     (begin
       (display (cons `command `(args ...)))
       (newline)))))

scheme@(guile-user)> (run "echo" ,(+ 1 2))
(echo 3)

> 2. I was not able to use the | symbol.
>
I just checked, and on both Guile HEAD (from recent git) and Guile
1.8.7, `|' is a valid symbol, although it is not valid according to R5RS
and R6RS.  What difficulties are you experiencing exactly?

Regards, Rotty
-- 
Andreas Rottmann -- <http://rotty.yi.org/>

Re: piper schemigan

[Ludovic Courtès]

+1 for reviving Guile-SCSH!

Ludo’.

Re: piper schemigan

[Stefan Israelsson Tampe]

On Thursday, November 25, 2010 10:17:44 pm Ludovic Courtès wrote:
> +1 for reviving Guile-SCSH!
> 
> Ludo’.

yay,

Well all this stems from me littering development code with printf or pk's
or pretty-pk's and then add tags to it. Then I usually work in bash and
mongle the output at my will. So now I have this is guile and are so pleased
that I can do
(use-modules (scsh syntax))

and then write
(run (| (begin (the-schem-fun)) '(grep abc) '(tee debug.log)))

Oh well, actually, I would probably make a macro and/or mod the reader
and add the autoquoting as in the original scsh, to be able to do

(the-schem-fun) | (grep abc) (tee debug.log)

So from my personal view I'm sort of very close to the goal.

But all of scsh have not been imported (yet) the reason is that I want to get 
a core that is stable. you can easilly with a little misstake make guile and 
actually the whole shell session go down. So, the core has to be worked on for 
some time. I've just made it work I do not understand the codebase and tests
has to be made. I do not, personally, like the idea to incorporate all of scsh
in one go. I would divede the package into a base where the basic
functionality is in and that sit's closer to the guile core. Then as time goes
we can add the SRE regexps, and so on. to another package, further away. 
Maybe I need to put in some more packages I don't now, but my sense tells me 
that it it wise to startup small and solid in stead of fat and ugly :-).

Anyhow, I just checked in the current scsh in module/scsh in 
http://gitorious.org/guile-unify if there is a package you would like thean
give me a hint.

A note, you need to quote a lot of things explicitly and there are bugs and
debug  outputs - e.g. a bit premature, but I would like you to have a
possibility to express ideas, ok if none, great if some.

Actually I noticed that the codebase seem to be needing to include all
packages into the namespace before e.g. using defmacro's and then need to 
have the symbols generated by the macro in the namespace. As small as it
sounds, the imporvemnet on  this is soo great, I can now just ask for the 
run macro from the (scsh syntax) package and it should work. This is far
better then all of scsh working in my book.

Your milage may vary, keep up the good work and a happy weekend to you.

/stefan

Guile-SCSH

[Ludovic Courtès]

Hi!

Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> Anyhow, I just checked in the current scsh in module/scsh in 
> http://gitorious.org/guile-unify if there is a package you would like thean
> give me a hint.

How about keeping it separate from your other work?

I noticed that Gary Houston’s Guile-SCSH page at
<http://arglist.com/guile/> vanished, but you might want to get in touch
with him...

Thanks,
Ludo’.

Re: Guile-SCSH

[Stefan Israelsson Tampe]

On Sunday, November 28, 2010 11:30:05 pm Ludovic Courtès wrote:
> Hi!
> 
> Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:
> > Anyhow, I just checked in the current scsh in module/scsh in
> > http://gitorious.org/guile-unify if there is a package you would like
> > thean give me a hint.
> 
> How about keeping it separate from your other work?

Yea, 

I think I understand your point.

I was a bit lazy and post it on the repo that I already had.

Hmm, the thing is that I do a small change in (system repl) due to
exit capturing, I do not want to clone the whole repo. SO untill that is 
fixed in a good way I will keep it on the repo.

> I noticed that Gary Houston’s Guile-SCSH page at
> <http://arglist.com/guile/> vanished, but you might want to get in touch
> with him...

I will try.

> Thanks,
> Ludo’.

Re: Guile-SCSH

[Jose A. Ortega Ruiz]

On Mon, Nov 29 2010, Stefan Israelsson Tampe wrote:

[...]

>> I noticed that Gary Houston’s Guile-SCSH page at
>> <http://arglist.com/guile/> vanished, but you might want to get in touch
>> with him...
>
> I will try.

I wrote him back in the day and he sent me a tar with guile-scsh source
code. Let me know if you'd like me to sent it to you, or if it'd be
better to post it here.

Cheers,
jao

Re: Guile-SCSH

[Stefan Israelsson Tampe]

Hi Jao,

You can send it to me, that's fine. I'll put a repo on gitorious and
add that code there together with my suggested alternatives.

Regards
Stefan

On Monday, November 29, 2010 12:24:28 am Jose A. Ortega Ruiz wrote:
> On Mon, Nov 29 2010, Stefan Israelsson Tampe wrote:
> 
> [...]
> 
> >> I noticed that Gary Houston’s Guile-SCSH page at
> >> <http://arglist.com/guile/> vanished, but you might want to get in touch
> >> with him...
> > 
> > I will try.
> 
> I wrote him back in the day and he sent me a tar with guile-scsh source
> code. Let me know if you'd like me to sent it to you, or if it'd be
> better to post it here.
> 
> Cheers,
> jao

http://gitorious.org/guile-scsh/guile-scsh

[Stefan Israelsson Tampe]

Ok I put the code in a repo of it's own.

So now this thingie is isolated.

I don't now what to do about the licesning, I kept
the COPYING as I should though.

To use it, store it in a %load-path directory

try
(use-modules (scsh syntax))

and then
(run (| (begin (pk 'wow) (pk 'vov)) (grep o)))


So, a slight improvement on system :-)

should behave acording to spec.

Have fun
Stefan

Guile-Facade

[Ludovic Courtès]

Hi!

Thanks for setting up the repo!

I also realized that Clinton once mentioned Guile-Facade on IRC, which
is a Guile-SCSH revival, AIUI:

  http://unknownlamer.org/darcsweb/browse?r=guile-facade;a=summary

Perhaps he can comment.  :-)

Ludo’.

Re: The progress of hacking guile and prolog

[Ludovic Courtès]

Hi!

Noah Lavine <noah.b.lavine@gmail.com> writes:

> What I'm thinking of is like racket contracts, but with the idea of
> "trusted modules", which might involve static checking. For instance,
> if the contract is that map's second parameter is a list, you'd
> normally want to check that. But if a module that used map could
> guarantee that it would always pass a list as the second argument,
> then you'd arrange things so the second module could skip the type
> check.

In Guile, modules are dynamic by nature: they are assembled at run-time
(everything is “dynamically linked”).  My feeling is that cross-module
static analysis doesn’t fit well in this framework.

> I'm curious in general though whether it would be possible and
> worthwhile to statically check programmer-defined ideas, as long as
> the interface is easy enough to use. For instance, what if you could
> ask Guile to check that your tree structure always remained a binary
> tree?

I think you’ll be interested in dependent types:

  https://secure.wikimedia.org/wikipedia/en/wiki/Dependent_types

Though I’d recommend working on JIT for Guile before you get stuck in a
meta-circular Curry-Howardish enlightenment period.  :-)

Thanks,
Ludo’.

Re: The progress of hacking guile and prolog

[Noah Lavine]

Hello,

> Though I’d recommend working on JIT for Guile before you get stuck in a
> meta-circular Curry-Howardish enlightenment period.  :-)

I agree. :-)

Noah

Re: The progress of hacking guile and prolog

[Andy Wingo]

Hi Noah,

On Wed 24 Nov 2010 02:54, Noah Lavine <noah.b.lavine@gmail.com> writes:

> What I'm thinking of is like racket contracts, but with the idea of
> "trusted modules", which might involve static checking.

Yeah, definitely. Like the interface between typed and untyped code in
racket, also. I don't know very much about the relationship between
types and contracts, though.

> I'm curious in general though whether it would be possible and
> worthwhile to statically check programmer-defined ideas, as long as
> the interface is easy enough to use. For instance, what if you could
> ask Guile to check that your tree structure always remained a binary
> tree? Or better, what if you wrote a GUI program and checked that the
> callbacks you passed to the GUI library would always return? (I know
> it's not possible in general, but I think it will work for a subset of
> procedures that will include some interesting ones.)

It's certainly interesting! As I understand things (which is not very
far), Racket allows for this via other "languages". Guile could do that
too. We might need some more generic support for this kind of thing in
the compiler infrastructure or in tree-il or whatever, but I would like
to make it possible to experiment with these linguistic ideas, with the
kind of isolation provided by modules.

Cheers,

Andy
-- 
http://wingolog.org/

Re: The progress of hacking guile and prolog

[Andy Wingo]

Hi again,

The more apropos link to Racket's contracts would probably be:

   http://docs.racket-lang.org/guide/contracts.html

Cheers,

Andy
-- 
http://wingolog.org/

Re: The progress of hacking guile and prolog

[Stefan Israelsson Tampe]

On Thursday, November 04, 2010 12:43:54 am Ludovic Courtès wrote:
> Hi Stefan,
> 
> Lots of stuff here, which is why I took the time to read it.  :-)
> 
> Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:
> > 1. The theorem prover (leanCop) is a nice exercise
> 
> [...]
> 
> > 2. Kanren is a nice way to program like with prolog,
> 
> Great that you’re mentioning them.  It looks like there’s a lot of
> interesting work that’s been done around Kanren, such as the “toy” type
> inference engine and, better, αleanTAP.  I don’t grok it all I’m glad
> you’re looking at it from a Guile perspective.  :-)

Yes, but I would like to be more true to it then I am right now. So is it 
enough to reproduce minikanren? Also I've reading in on racklog so I guess
what I have right now is correct conceptually but not syntactically. But of
cause this can be fixed. So If you think it is worthwhile I will download the
minikanren sorce hack on.

> > 4. The umatch hackity hack was turned into a much more hygienic creature.
> 
> Funny sentence.  :-)

Well I have two versions one based on the match-phd and is not touching guiles 
internals and is based on passing continuations closures and has the property 
that all calls are tail calls for basic prolog usage patterns. Also note that
this principle is not as expensive that one may think if you take into acount 
a system that inline functions acording to findings from profiling. So in 
principle all this pushing parameters to the heap could be mitigated. The 
other
one is the hackety hack that tend to be fast on the vm.

> > 5) Typechecking is for safty and optimisation, in the end it can be cool
> > to have and I'm working to understand all sides of this and have a
> > pretty good idea what is needed. It will be a goos testcase for the
> > code.
> 
> Yes, if the type inference engine that comes with Kanren could somehow
> be hooked into Guile’s compiler, so that it can emit type-mismatch
> warnings or determine whether type-checks can be optimized away (which
> would require changes in the VM), that’d be great.

Notes.
	1. It's when compilers start to work you will gain from removing 
	type checks. It's probably not worth it in vm land

	2. If a function is used like (f 0.1) in function g and you recompile
 	function f to just allow only fixnums you may end up with havoc. So 
	either function dependencies is tracked or you use the racket way of 
	executing code if going down this optimizing path in a safe way.

	3. Of cause local entities can be tracked and optimized away and maybe
	we should stick to only that.

> What’s amazing is that Kanren + type-inference.scm weigh in at “only”
> ~3,500 SLOC.

Hence is a powerful concept :-)
Hmm I'm also keen to match what typed racket does. I will look into this.


> > 6) I copied the  glil->assembly compiler and modded the code to spit out
> > c-code in stead of assembly. For functions which does not call other
> > scheme functions except in tail call manner this should be quite fast to
> > adapt. And of cause loops becomes wickedly fast when compiling this way.
> > Wingo:s example without consing tok 7ns for each loop on my machine.
> 
> Interesting.  Is it a sufficiently isolated change that you could point
> us to?

Uhmm, I was just curious to se what the overhead of dispatching 
instructions in a goto-loop would give when I did it. But just think of it
as a tool that just inline the c-code behind some simple vm instructions in 
stead of the actual vm-instructions. Actually all prolog vanilla prolog 
code should be able to be compiled quite effectively this way cause it's 
all tail calls. I'm not sure my code is that interesting though Probably the 
idea is more interesting and should be discussed. The basic idea is to pair
the c-code generation with the glil->assembly code so that the compiling
function and all it's internal lambda get's corresponding c-function quite
automagically and then be gcc:d into linkable code and hooked int these 
functions vm part that now just act like a trampoline into C land. 
Do you see it?

Have fun
Stefan

Re: The progress of hacking guile and prolog

[Stefan Israelsson Tampe]

[-- Attachment #1: Type: Text/Plain, Size: 2387 bytes --]

Ok, for the c generator, here are some code attached. I would 
just study this there is bit's still missing and you need to wait for me to
dig up the details. My point is to suggest  ideas for what can be done. 
I don't assume that this is it. But it's a nice playing ground.

So it is a hack, here is what I do.

(use modules (language glil compile-assembly))
(set! *compile-to-c* #t)
(define (f N) 
	(set! <c-dummy> '<c-code-tag>)   ;; This tagg!! initiate the compiler 
	                                 ;; and c-fkn will use the
                 		         ;; <c-code-tag> slot :-)
 
	(let loop ((I N) (X 0)) 
	(if (eq? I 0) 
	X  (loop 
	(- I 1) (+ X 1)))))
(generate-c-fkns "fkn")

Then in a sub-directory called cboost from the starting directory you find
fkn.c and a makefile. e.g.

Makefile:
=========
libguile-fkn.so : fkn.c
	gcc -shared -O2 -o libguile-fkn.so -fPIC fkn.c

fkn.c:
======
#include "cfkn.h"
#define LOCAL_REF(i)     fp[i]
#define LOCAL_SET(i,v)   fp[i] = (v)
void cfkn3676(SCM *fp, SCM **spp)
{
 /* setup of environment */
 SCM *objects, *free, program, *sp, sss[100];
 sp = sss;
 program = fp[-1];
 objects = SCM_I_VECTOR_WELTS (SCM_PROGRAM_OBJTABLE (program));    
 free    = SCM_PROGRAM_FREE_VARIABLES(program);
 /* compiled section */
 LCASE3666:


goto L3668;
LCASE3665:
sp++; *sp = LOCAL_REF(1);
sp++; *sp = SCM_I_MAKINUM(0);
sp-=2; if(!scm_is_eq(sp[1],sp[2])) goto L3669;
sp++; *sp = LOCAL_REF(2);
RETURN;
L3669:
sp++; *sp = LOCAL_REF(1);
SUB1;
sp++; *sp = LOCAL_REF(2);
ADD1;
LOCAL_SET(2,*sp)              ; sp--;
LOCAL_SET(1,*sp)              ; sp--;
goto LCASE3665;
L3668:
sp++; *sp = LOCAL_REF(0);
sp++; *sp = SCM_I_MAKINUM(0);
LOCAL_SET(2,*sp)              ; sp--;
LOCAL_SET(1,*sp)              ; sp--;
goto LCASE3665;

}

void init_fkn.c()
{
   SCM cfkn3676_sym;
   

   cfkn3676_sym = scm_from_locale_symbol("cfkn3676");
   

   printf("loading fkn %s as adres %x.\n","cfkn3676",&cfkn3676);
   

   scm_define(cfkn3676_sym,SCM_PACK(((scm_t_bits) &cfkn3676) | 2));
   
}


So compileing and loading the shared library into guile you should be able 
to issue (f 1000000) and get a correct and fast result. 

I'm did not find my cfkn.h file but I'll send you the stuff I have. I modify
glil->assembly and add offload some bit's into an extra file into the same
directory also a vm-instruction is added to be able to start the c-code.

Have fun
Stefan


[-- Attachment #2: compile2c.tar.gz --]
[-- Type: application/x-compressed-tar, Size: 9983 bytes --]

GLIL->C compilation

[Ludovic Courtès]

Hi,

Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> #include "cfkn.h"
> #define LOCAL_REF(i)     fp[i]
> #define LOCAL_SET(i,v)   fp[i] = (v)
> void cfkn3676(SCM *fp, SCM **spp)
> {
>  /* setup of environment */
>  SCM *objects, *free, program, *sp, sss[100];
>  sp = sss;
>  program = fp[-1];
>  objects = SCM_I_VECTOR_WELTS (SCM_PROGRAM_OBJTABLE (program));    
>  free    = SCM_PROGRAM_FREE_VARIABLES(program);
>  /* compiled section */
>  LCASE3666:
>
>
> goto L3668;
> LCASE3665:
> sp++; *sp = LOCAL_REF(1);
> sp++; *sp = SCM_I_MAKINUM(0);
> sp-=2; if(!scm_is_eq(sp[1],sp[2])) goto L3669;
> sp++; *sp = LOCAL_REF(2);

[...]

Comparing this to the VM’s bytecode interpreter should show the overhead
incurred by instruction dispatch.

Did you try to measure this?  That’d be interesting.

Thanks,
Ludo’.

Re: GLIL->C compilation

[Stefan Israelsson Tampe]

On Saturday, November 20, 2010 12:11:16 am Ludovic Courtès wrote:
> Hi,
> 
> Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:
> > #include "cfkn.h"
> > #define LOCAL_REF(i)     fp[i]
> > #define LOCAL_SET(i,v)   fp[i] = (v)
> > void cfkn3676(SCM *fp, SCM **spp)
> > {
> > 
> >  /* setup of environment */
> >  SCM *objects, *free, program, *sp, sss[100];
> >  sp = sss;
> >  program = fp[-1];
> >  objects = SCM_I_VECTOR_WELTS (SCM_PROGRAM_OBJTABLE (program));
> >  free    = SCM_PROGRAM_FREE_VARIABLES(program);
> >  /* compiled section */
> > 
> >  LCASE3666:
> > goto L3668;
> > LCASE3665:
> > sp++; *sp = LOCAL_REF(1);
> > sp++; *sp = SCM_I_MAKINUM(0);
> > sp-=2; if(!scm_is_eq(sp[1],sp[2])) goto L3669;
> > sp++; *sp = LOCAL_REF(2);
> 
> [...]
> 
> Comparing this to the VM’s bytecode interpreter should show the overhead
> incurred by instruction dispatch.
> 
> Did you try to measure this?  That’d be interesting.
> 
> Thanks,
> Ludo’.

Yes on one of my machine one loop takes about 6ns for the compiled one and 
about 50ns for the bytcode, say a factor of 7-10 for simple tasks, but 
remember
this is for rather trivial work.

Re: GLIL->C compilation

[Ludovic Courtès]

Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:

> On Saturday, November 20, 2010 12:11:16 am Ludovic Courtès wrote:
>> Hi,
>> 
>> Stefan Israelsson Tampe <stefan.itampe@gmail.com> writes:
>> > #include "cfkn.h"
>> > #define LOCAL_REF(i)     fp[i]
>> > #define LOCAL_SET(i,v)   fp[i] = (v)
>> > void cfkn3676(SCM *fp, SCM **spp)
>> > {
>> > 
>> >  /* setup of environment */
>> >  SCM *objects, *free, program, *sp, sss[100];
>> >  sp = sss;
>> >  program = fp[-1];
>> >  objects = SCM_I_VECTOR_WELTS (SCM_PROGRAM_OBJTABLE (program));
>> >  free    = SCM_PROGRAM_FREE_VARIABLES(program);
>> >  /* compiled section */
>> > 
>> >  LCASE3666:
>> > goto L3668;
>> > LCASE3665:
>> > sp++; *sp = LOCAL_REF(1);
>> > sp++; *sp = SCM_I_MAKINUM(0);
>> > sp-=2; if(!scm_is_eq(sp[1],sp[2])) goto L3669;
>> > sp++; *sp = LOCAL_REF(2);
>> 
>> [...]
>> 
>> Comparing this to the VM’s bytecode interpreter should show the overhead
>> incurred by instruction dispatch.
>> 
>> Did you try to measure this?  That’d be interesting.
>> 
>> Thanks,
>> Ludo’.
>
> Yes on one of my machine one loop takes about 6ns for the compiled one and 
> about 50ns for the bytcode, say a factor of 7-10 for simple tasks, but 
> remember
> this is for rather trivial work.

Woow, I didn’t expect so much.

Ludo’.

Re: GLIL->C compilation

[Andy Wingo]

On Sat 20 Nov 2010 00:56, ludo@gnu.org (Ludovic Courtès) writes:

>> Yes on one of my machine one loop takes about 6ns for the compiled one and 
>> about 50ns for the bytcode, say a factor of 7-10 for simple tasks, but 
>> remember
>> this is for rather trivial work.
>
> Woow, I didn’t expect so much.

I would expect it, yes. Something aroung 5x for dispatch, with more if
the compiler decided to inline more things across "instruction"
boundaries.

Andy
-- 
http://wingolog.org/