new Shen-YACC works

[Mark Tarver]

This is due for SP 20 and hopefully (if my funding drive succeeds) in OS Shen; it really restores the symmetry in Shen in that having typed Shen-YACC now means that we can write type secure compilers in Shen.  In fact it would be possible, with suitable datatype declarations, to typecheck the Shen kernel itself now.

I've rebuilt the Kl kernel using the new YACC and it works fine.  I'm testing it out on a compiler for a fragment of C, which involves parsing C code into a list representation.   Here is the code which uses big arrow type notation.

(datatype declaration

  Type : type; Variables : (list symbol);

  =============================================

  [declare Type Variables] : declaration;

  Type : type; Variable : symbol; Dim : integer;

  ===================================================

  [declare [vector Type] Variable Dim] : declaration;)

(defcc <declaration>

  {(list string) ==> declaration} 

  <ws> <type> <space> <ws> <variables> := [declare <type> <variables>];

  <ws> <type> <space> <ws> <variable> <ws> <dim> 

  := [declare [vector <type>] <variable> <dim>];)

            

(datatype integer

  if (integer? N)

   ____________

  N : integer;

  if (element? Op [+ - *])

  M : integer; N : integer;

  ___________________________ 

  (Op M N) : integer;

   

  N : integer;

  _____________________

  N : number;)

   

(defcc <dim>

 {(list string) ==> integer}

"[" <ws> <int> <ws> "]" := <int>;)

(defcc <int>

  {(list string) ==> integer}

  <int-h> := (compute-int <int-h>);)

(defcc <int-h> 

  {(list string) ==> (list integer)}

  <numeric> <int-h> := [(digit <numeric>) | <int-h>];

  <numeric> := [(digit <numeric>)];)

(defcc <numeric> 

  {(list string) ==> string}

  X := X where (element? X ["0" "1" "2""3""4""5" "6" "7" "8" "9"]);)

   

(define digit

  {string --> integer}

  "0" -> 0

  "1" -> 1

  "2" -> 2

  "3" -> 3

  "4" -> 4

  "5" -> 5

  "6" -> 6

  "7" -> 7

  "8" -> 8

  "9" -> 9)

(define compute-int

  {(list integer) --> integer}

  [] -> 0

  [N | Ns] -> (+ (* N (expt 10 (intlength Ns))) (compute-int Ns)))

(define expt

  {integer --> integer --> integer}

  _ 0 -> 1

  M N -> (* M (expt M (- N 1)))) 

(define intlength

  {(list A) --> integer}

  [] -> 0

  [_ | Y] -> (+ 1 (intlength Y)))

 

(datatype type

 if (element? T [int char float])

 ________________________

 T : type;)

(defcc <type>

 {(list string) ==> type}

  ($ int) := int;

  ($ char) := char;

  ($ float) := float;) 

(defcc <variables>

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

 <variable> <ws> "," <ws> <variables> := [<variable> | <variables>];

 <variable> := [<variable>];)

 

(defcc <variable>

 {(list string) ==> symbol}

 <alphanumeric> := (string->symbol <alphanumeric>);)

(defcc <alphanumeric>

  {(list string) ==> string}

  <alpha> <alphanumeric-h> := (@s <alpha> <alphanumeric-h>);)

(defcc <alphanumeric-h>

  {(list string) ==> string}

  <alpha> <alphanumeric-h> := (@s <alpha> <alphanumeric-h>);

  <numeric> <alphanumeric-h> := (@s <numeric> <alphanumeric-h>);

  <e> := "";)

(defcc <alpha>

  {(list string) ==> string}

  "a" := "a"; "A" := "A"; "b" := "b";"B" := "B";

  "c" := "c";"C" :="C";"d" := "d";"D" := "D";

  "e" := "e";"E" := "E";"f" := "f";"F" := "F";

  "g" := "g"; "G" := "G";"h" := "h"; "H" := "H";

  "i" := "i";"I" := "I";"j" := "j";"J" := "J";

  "k" := "k"; "K" := "K";"l" := "l";"L" := "L";

  "m" := "m"; "M" := "M"; "n" := "n";"N" := "N";

  "o" := "o";"O" := "O"; "p" := "p";"P" := "P";

  "q" := "q";"Q" :="Q"; "r" := "r";"R" := "R";

  "s" := "s";"S" := "S"; "t" := "t";"T" := "T";

  "u" := "u"; "U" := "U"; "v" := "v"; "V" := "V";

  "w" := "w";"W" := "W"; "x" := "x";"X" := "X";

  "y" := "y"; "Y" := "Y"; "z" := "z";"Z" := "Z";

  "_" := "_";) 

(defcc <numeric> 

  {(list string) ==> string}

  X := X          where (element? X ["0" "1" "2""3""4""5""6""7""8""9"]);)

(defcc <ws>

  {(list string) ==> A}

  <comment> <ws> := skip!;

  <space> <ws> := skip!;

  <tab> <ws> := skip!;

  <newline> <ws> := skip!;

  <e> := skip!;) 

(defcc <space>

  {(list string) ==> A}

  X := skip!      where (= (string->n X) 32);)

(defcc <tab>

  {(list string) ==> A}

  X := skip!      where (= (string->n X) 9);)

(defcc <newline>

  {(list string) ==> A}

  X := skip!      where (element? (string->n X) [10 13]);)

(defcc <comment>

  {(list string) ==> A}

  "/" "*" <comment-body> := skip!;)

(defcc <comment-body>

  {(list string) ==> A}

  "/" "*" := skip!;

  _ <comment-body> := skip!;)

Here we test the program

(1+) (load "C:\Users\User\Desktop\hum")

type#declaration : symbol

<declaration> : (((list string) * A) --> ((list string) * declaration))

type#integer : symbol

<dim> : (((list string) * A) --> ((list string) * integer))

<int> : (((list string) * A) --> ((list string) * integer))

<int-h> : (((list string) * A) --> ((list string) * (list integer)))

<numeric> : (((list string) * A) --> ((list string) * string))

digit : (string --> integer)

compute-int : ((list integer) --> integer)

expt : (integer --> (integer --> integer))

intlength : ((list A) --> integer)

type#type : symbol

<type> : (((list string) * A) --> ((list string) * type))

<variables> : (((list string) * A) --> ((list string) * (list symbol)))

<variable> : (((list string) * A) --> ((list string) * symbol))

<alphanumeric> : (((list string) * A) --> ((list string) * string))

<alphanumeric-h> : (((list string) * A) --> ((list string) * string))

<alpha> : (((list string) * A) --> ((list string) * string))

<numeric> : (((list string) * A) --> ((list string) * string))

<ws> : (((list string) * A) --> ((list string) * A))

<space> : (((list string) * A) --> ((list string) * A))

<tab> : (((list string) * A) --> ((list string) * A))

<newline> : (((list string) * A) --> ((list string) * A))

<comment> : (((list string) * A) --> ((list string) * A))

<comment-body> : (((list string) * A) --> ((list string) * A))

run time: 3.7439999617636204 secs

typechecked in 82968 inferences

loaded : symbol

(2+) (compile (function <declaration>) (explode "int a,b,c"))

[declare int [a b c]] : declaration

Mark

[Mark Tarver]

The entire C compiler front end type checks.

Mark

(47+) (load "C:\Users\User\Desktop\hum")

warning: <expr> has no semantics.

warning: <expr> has no semantics.

warning: <vector-ref> has no semantics.

warning: <complex> has no semantics.

warning: <variable> has no semantics.

warning: <constant> has no semantics.

warning: <statement> has no semantics.

warning: <statement> has no semantics.

warning: <declaration> has no semantics.

warning: <print> has no semantics.

warning: <assignment> has no semantics.

warning: <conditional> has no semantics.

warning: <while> has no semantics.

warning: <return> has no semantics.

warning: <atomic-statement> has no semantics.

warning: <compound-statement> has no semantics.

warning: <statements> has no semantics.

type#program : symbol

type#preamble : symbol

type#main : symbol

c-minus : (string --> program)

read-file-as-unit-strings : (string --> (list string))

<program> : (((list string) * A) --> ((list string) * program))

<preamble> : (((list string) * A) --> ((list string) * (list statement)))

<main> : (((list string) * A) --> ((list string) * main))

type#statement : symbol

<statement> : (((list string) * A) --> ((list string) * statement))

<compound-statement> : (((list string) * A) --> ((list string) * statement)

<statements> : (((list string) * A) --> ((list string) * (list statement)))

<atomic-statement> : (((list string) * A) --> ((list string) * statement))

type#assignment : symbol

<assignment> : (((list string) * A) --> ((list string) * statement))

type#expr : symbol

type#op : symbol

type#conditional : symbol

<return> : (((list string) * A) --> ((list string) * statement))

<conditional> : (((list string) * A) --> ((list string) * statement))

<statement1> : (((list string) * A) --> ((list string) * statement))

<statement2> : (((list string) * A) --> ((list string) * statement))

<exprs> : (((list string) * A) --> ((list string) * (list expr)))

<expr> : (((list string) * A) --> ((list string) * expr))

<vector-ref> : (((list string) * A) --> ((list string) * expr))

<index> : (((list string) * A) --> ((list string) * expr))

<complex> : (((list string) * A) --> ((list string) * expr))

<expr1> : (((list string) * A) --> ((list string) * expr))

<expr2> : (((list string) * A) --> ((list string) * expr))

<prefix> : (((list string) * A) --> ((list string) * symbol))

<infix> : (((list string) * A) --> ((list string) * infix))

type#constant : symbol

<constant> : (((list string) * A) --> ((list string) * constant))

<float> : (((list string) * A) --> ((list string) * number))

<pre> : (((list string) * A) --> ((list string) * (list integer)))

<post> : (((list string) * A) --> ((list string) * (list integer)))

compute-float : ((list integer) --> ((list integer) --> number))

compute-fractional : ((list integer) --> number)

compute-fractional-h : ((list integer) --> (integer --> number))

<char> : (((list string) * A) --> ((list string) * string))

type#integer : symbol

<int> : (((list string) * A) --> ((list string) * integer))

<int-h> : (((list string) * A) --> ((list string) * (list integer)))

<numeric> : (((list string) * A) --> ((list string) * string))

digit : (string --> integer)

compute-int : ((list integer) --> integer)

expt : (integer --> (integer --> integer))

intlength : ((list A) --> integer)

type#print : symbol

<print> : (((list string) * A) --> ((list string) * statement))

<string> : (((list string) * A) --> ((list string) * string))

<stringstuff> : (((list string) * A) --> ((list string) * string))

<ndq> : (((list string) * A) --> ((list string) * string))

type#while : symbol

<while> : (((list string) * A) --> ((list string) * statement))

type#parameters : symbol

<params> : (((list string) * A) --> ((list string) * parameters))

type#declaration : symbol

<declaration> : (((list string) * A) --> ((list string) * statement))

<dim> : (((list string) * A) --> ((list string) * integer))

type#type : symbol

<type> : (((list string) * A) --> ((list string) * type))

<variables> : (((list string) * A) --> ((list string) * (list symbol)))

<variable> : (((list string) * A) --> ((list string) * symbol))

<alphanumeric> : (((list string) * A) --> ((list string) * string))

<alphanumeric-h> : (((list string) * A) --> ((list string) * string))

<alpha> : (((list string) * A) --> ((list string) * string))

<numeric> : (((list string) * A) --> ((list string) * string))

type#procedure : symbol

type#parameters : symbol

<procedure> : (((list string) * A) --> ((list string) * procedure))

<procname> : (((list string) * A) --> ((list string) * symbol))

<params> : (((list string) * A) --> ((list string) * parameters))

<ws> : (((list string) * A) --> ((list string) * A))

<space> : (((list string) * A) --> ((list string) * A))

<tab> : (((list string) * A) --> ((list string) * A))

<newline> : (((list string) * A) --> ((list string) * A))

<comment> : (((list string) * A) --> ((list string) * A))

<comment-body> : (((list string) * A) --> ((list string) * A))

run time: 6.1620025634765625 secs

typechecked in 156778 inferences

loaded : symbol