Forth Type Checker by Jürgen Pfitzenmaier pfitzen@web.de ---------------------------------------- Abstract Forth engine <---> Type Checker ---------------------------------------- Installation & next version monolithic --> library + ocaml runtime pforth ---------------------------------------- Reading input from file --- from keyboard automatic testing ---------------------------------------- Declaring Types much like in the current standard \T Execution: (u -- x n) \ \T Compilation: (x -- ) Runtime: ( -- x) \T Assume: Execution: (x -- x) \T Cast: Execution: (n -- ) (F: -- r) ---------------------------------------- Standard Types xd __ x _______________________ /\ / / \ \ \ \ \ \ / \ | | | | \ \ \ \ ud d xt u n flag wid ior fam fileid \ / /\ / | \/ / +n state +d / | c-addr char | __ a-addr ___ / | \ | | | f-addr sf-addr df-addr colon-sys do-sys case-sys of-sys orig dest ---------------------------------------- Finer types for loops loop-sys / \ loop-sys-u loop-sys-n ---------------------------------------- Exit as Forward Connection nest-sys like-nest-sys ---------------------------------------- How to empty the Stack i*x j*x k*x empty ---------------------------------------- Special Types state recurse ---------------------------------------- Reserved for future use obj class frame ---------------------------------------- Full Declaration prevents internal shifting Compilation: ( -- ) Runtime: ( x -- x ) is NOT equal to Runtime: ( x -- x ) ---------------------------------------- Delay type check for one token RESTRICT IMMEDIATE IMMEDIATERESTRICT ---------------------------------------- Example 1 : bad1 \ T ( u -- u) -1 + ; \ end of bad1 : bad1b \T ( u -- u) -1 + ; \ end of bad1b : good1 \T ( n -- n) -1 + ; \ end of good1 ---------------------------------------- Example 2 Constant as a simple constraint : good2 \T ( -- n) 4 ; \ end of good2 : good2b \T ( -- 4) 4 ; \ end of good2b ---------------------------------------- Example 3 IF ELSE THEN and dependent types : bad3 \T (x true -- x x) | (x false -- char.addr) IF DUP DUP ELSE PAD THEN ; \ end of bad3 : bad3b \T (x true -- x x x) | (x false -- char.addr) IF DUP DUP ELSE PAD THEN ; \ end of bad3b : good3 \T (x true -- x x x) | (false -- char.addr) IF DUP DUP ELSE PAD THEN ; \ end of good3 : good3b \T (x_{1} true -- x_{1} x_{1} x_{1}) | (false -- char.addr) IF DUP DUP ELSE PAD THEN ; \ end of good3b ---------------------------------------- Example 4 Casting Types : FLOATSTACK? \T ( -- flag) S" FLOATING-STACK" environment? \T Cast: (false -- false) | (i*x true -- n true) if 0<> else false then ; ---------------------------------------- Example 5 Floating Point Stack : float1 [ floatstack? ] [IF] \T (F: r r -- r) [ELSE] \T (r r -- r) [THEN] F+ ; \ end of float1 ---------------------------------------- : local1 \T Cast: ( n n -- n n) ; DOKU warum cast vor local-def { m n -- } \T ( n n -- n n) n dup m * dup n * ; \ end of local1 : local2 \T Cast: (n n -- n n) { v1 v2 | l1 l2 -- } \T ( n n -- ) v1 . v2 . cr v1 v2 + -> l1 l1 . l2 . cr ; \ end of local2 ---------------------------------------- : exit1 \T (false -- +n) | (true -- +n +n) IF 1 THEN 2 ; \ end of exit1 : exit2 \T (false -- +n) | (true -- +n) IF 1 EXIT THEN 2 ; \ end of exit2 ---------------------------------------- Example with ABORT and CASE : POSTPONE \T ( -- ) ; CORE 6.1.2033 bl word find CASE 0 OF ." Postpone could not find " count type cr ABORT ENDOF 1 OF compile, ENDOF \ immediate -1 OF (compile) ENDOF \ normal ENDCASE ; immediaterestrict ---------------------------------------- Problem with matching types : abort2 \T (+n -- n) CASE 1 OF 1 ENDOF 2 OF 2 2 ENDOF ENDCASE ; \ end of abort2 : abort3 \T ( empty -- ) (R: empty -- ) \ \T | ( k*x -- -1) (R: k*x -- ) -1 throw ; \ end of abort3 ---------------------------------------- RECURSE in action : rec1 \T (n -- n) DUP 2 > IF DUP 1 - * RECURSE THEN ; \ end of rec1 ---------------------------------------- Using CREATE and DOES> : 2VARIABLE \T ( -- ) nameExecution: ( -- d.a-addr ) ; DOUBLE 8.6.1.0440 create 0 , 0 , \T AllowRebind: (-- d.a-addr) ; \ end of 2variable : CONSTANT \T (x_{1} -- ) nameExecution: (-- x_{1}) ; CORE 6.1.0950 XXX im ANS fehlt der index 1 CREATE , \T AllowRebind: (x -- ) DOES> \T ( x_{1}.a-addr -- x_{1} ) @ ; \ end of constant ---------------------------------------- : loop1 \T (n --) 5 do cr loop ; \ end of loop1 : loop2 \T (n --) 5 do J 4 = if LEAVE then loop ; \ end of loop2 ---------------------------------------- Dirty Failures : dirtyloop \T (n --) 5 do if LEAVE then loop ; \ end of dirtyloop : dirty \T ( -- ) R> DROP ; \ end of dirty : ?EXIT \T Compilation: ( -- ) Runtime: (x --) Runtime: (R: nest-sys --) \ \T | Compilation: ( -- ) Runtime: (x -- ) postpone IF postpone EXIT postpone THEN ; immediate ----------------------------------------