type secure Shen-YACC

[Mark Tarver]

An experimental Shen-YACC is producing type secure code which checks under vanilla Shen.  I worked on this a few years ago, but my approach required effectively redoing the proofs in TBoS and rewriting part of T *.  The unanswered question is if there is a performance hit and so it will remain experimental until I am happy that there is not a downside.  A good start though.

Mark

[Mark Tarver]

Still testing this; it uses what I call 'big arrow' notation which is a shorthand expanded by a macro to conventional 'small arrow' notation.

(49+) (defcc <sent>

 {(list symbol) ==> (list symbol)}

<np> <vp>;)

warning: <np> <vp> has no semantics.

<sent> : (((list symbol) * (list symbol)) --> ((list symbol) * (list symbol)))

(50+)(defcc <det>

{(list symbol) ==> (list symbol)}

the; a;)

warning: the has no semantics.

warning: a has no semantics.

<det> : (((list symbol) * (list symbol)) --> ((list symbol) * (list symbol)))

(51+)(defcc <np>

{(list symbol) ==> (list symbol)}

<det> <n>;

<name1>;)

warning: <det> <n> has no semantics.

warning: <name1> has no semantics.

<np> : (((list symbol) * (list symbol)) --> ((list symbol) * (list symbol)))

(52+)(defcc <n>

 {(list symbol) ==> (list symbol)}

cat; dog;)

warning: cat has no semantics.

warning: dog has no semantics.

<n> : (((list symbol) * (list symbol)) --> ((list symbol) * (list symbol)))

(53+)(defcc <name1>

{(list symbol) ==> (list symbol)}

 X := [X]       where (element? X [bill ben]);)

<name1> : (((list symbol) * (list symbol)) --> ((list symbol) * (list symbol)))

(54+) (defcc <vp>

{(list symbol) ==> (list symbol)}

<vtrans> <np>;)

warning: <vtrans> <np> has no semantics.

<vp> : (((list symbol) * (list symbol)) --> ((list symbol) * (list symbol)))

(55+) (defcc <vtrans>

{(list symbol) ==> (list symbol)}

likes; chases;)

warning: likes has no semantics.

warning: chases has no semantics.

<vtrans> : (((list symbol) * (list symbol)) --> ((list symbol) * (list symbol)))

(56+) (compile (function <sent>) [bill likes ben]) 

[bill likes ben] : (list symbol)

A slight performance hit but not major - probably not humanly noticeable in early all cases.  10^5 iterations of the last expression.

0.2180004119873047 secs  \\ typed Shen-YACC

0.14000000804662704 sec \\untyped Shen-YACC

I think though that the benefits of being able to have type secure Shen-YACC probably merit developing this.  Expect in SP.

Mark