Skip to content
This repository has been archived by the owner on Mar 5, 2024. It is now read-only.

Commit

Permalink
Shen 8
Browse files Browse the repository at this point in the history
  • Loading branch information
Hakan Raberg committed Jan 23, 2013
1 parent a1d9a54 commit 6dd1d88
Show file tree
Hide file tree
Showing 9 changed files with 1,454 additions and 1,218 deletions.
440 changes: 223 additions & 217 deletions shen/klambda/declarations.kl

Large diffs are not rendered by default.

4 changes: 4 additions & 0 deletions shen/klambda/reader.kl
Expand Up @@ -1056,3 +1056,7 @@ For an explication of this license see http://www.lambdassociates.org/News/june1
(concat V1078 V1080))
(true V1080)))

(defun read-from-string (V466)
(let Ns (map (lambda V465 (string->n V465)) (explode V466))
(compile shen-<st_input> Ns shen-read-error)))

2,132 changes: 1,171 additions & 961 deletions shen/klambda/t-star.kl

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion shen/klambda/toplevel.kl
Expand Up @@ -27,7 +27,7 @@ For an explication of this license see http://www.lambdassociates.org/News/june1

(defun version (V568) (set *version* V568))

(version "version 7.1")
(version "version 8")

(defun shen-credits ()
(do (intoutput "~%Shen 2010, copyright (C) 2010 Mark Tarver~%" ())
Expand Down
76 changes: 41 additions & 35 deletions shen/klambda/types.kl
Expand Up @@ -15,12 +15,12 @@

For an explication of this license see http://www.lambdassociates.org/News/june11/license.htm which explains this license in full."

(defun declare (V1681 V1682)
(let Record (set shen-*signedfuncs* (adjoin V1681 (value shen-*signedfuncs*)))
(defun declare (V1679 V1680)
(let Record (set shen-*signedfuncs* (adjoin V1679 (value shen-*signedfuncs*)))
(let Variancy
(trap-error (shen-variancy-test V1681 V1682) (lambda E shen-skip))
(let Type (shen-rcons_form (shen-normalise-type V1682))
(let F* (concat shen-type-signature-of- V1681)
(trap-error (shen-variancy-test V1679 V1680) (lambda E shen-skip))
(let Type (shen-rcons_form (shen-normalise-type V1680))
(let F* (concat shen-type-signature-of- V1679)
(let Parameters (shen-parameters 1)
(let Clause
(cons (cons F* (cons X ()))
Expand All @@ -33,43 +33,43 @@ For an explication of this license see http://www.lambdassociates.org/News/june1
(append Parameters
(append (cons ProcessN (cons Continuation ()))
(cons -> (cons Code ()))))))
(let Eval (shen-eval-without-macros ShenDef) V1681)))))))))))
(let Eval (shen-eval-without-macros ShenDef) V1679)))))))))))

(defun shen-normalise-type (V1683)
(fix (lambda V1684 (shen-normalise-type-help V1684)) V1683))
(defun shen-normalise-type (V1681)
(fix (lambda V1682 (shen-normalise-type-help V1682)) V1681))

(defun shen-normalise-type-help (V1685)
(defun shen-normalise-type-help (V1683)
(cond
((cons? V1685)
((cons? V1683)
(shen-normalise-X
(map (lambda V1686 (shen-normalise-type-help V1686)) V1685)))
(true (shen-normalise-X V1685))))
(map (lambda V1684 (shen-normalise-type-help V1684)) V1683)))
(true (shen-normalise-X V1683))))

(defun shen-normalise-X (V1687)
(let Val (assoc V1687 (value shen-*synonyms*))
(if (empty? Val) V1687 (tl Val))))
(defun shen-normalise-X (V1685)
(let Val (assoc V1685 (value shen-*synonyms*))
(if (empty? Val) V1685 (tl Val))))

(defun shen-variancy-test (V1688 V1689)
(let TypeF (shen-typecheck V1688 B)
(defun shen-variancy-test (V1686 V1687)
(let TypeF (shen-typecheck V1686 B)
(let Check
(if (= symbol TypeF) shen-skip
(if (shen-variant? TypeF V1689) shen-skip
(if (shen-variant? TypeF V1687) shen-skip
(intoutput "warning: changing the type of ~A may create errors~%"
(@p V1688 ()))))
(@p V1686 ()))))
shen-skip)))

(defun shen-variant? (V1698 V1699)
(cond ((= V1699 V1698) true)
((and (cons? V1698) (and (cons? V1699) (= (hd V1699) (hd V1698))))
(shen-variant? (tl V1698) (tl V1699)))
((and (cons? V1698)
(and (cons? V1699) (and (shen-pvar? (hd V1698)) (variable? (hd V1699)))))
(shen-variant? (subst shen-a (hd V1698) (tl V1698))
(subst shen-a (hd V1699) (tl V1699))))
((and (cons? V1698)
(and (cons? (hd V1698)) (and (cons? V1699) (cons? (hd V1699)))))
(shen-variant? (append (hd V1698) (tl V1698))
(append (hd V1699) (tl V1699))))
(defun shen-variant? (V1696 V1697)
(cond ((= V1697 V1696) true)
((and (cons? V1696) (and (cons? V1697) (= (hd V1697) (hd V1696))))
(shen-variant? (tl V1696) (tl V1697)))
((and (cons? V1696)
(and (cons? V1697) (and (shen-pvar? (hd V1696)) (variable? (hd V1697)))))
(shen-variant? (subst shen-a (hd V1696) (tl V1696))
(subst shen-a (hd V1697) (tl V1697))))
((and (cons? V1696)
(and (cons? (hd V1696)) (and (cons? V1697) (cons? (hd V1697)))))
(shen-variant? (append (hd V1696) (tl V1696))
(append (hd V1697) (tl V1697))))
(true false)))

(declare absvector? (cons A (cons --> (cons boolean ()))))
Expand Down Expand Up @@ -313,13 +313,17 @@ For an explication of this license see http://www.lambdassociates.org/News/june1
(declare read-byte
(cons (cons stream (cons in ())) (cons --> (cons number ()))))

(declare read-file
(cons string (cons --> (cons (cons list (cons unit ())) ()))))

(declare read-file-as-bytelist
(cons string (cons --> (cons (cons list (cons number ())) ()))))

(declare read-file-as-string (cons string (cons --> (cons string ()))))
(declare read-file-as-string
(cons string (cons --> (cons string ()))))

(declare read-file
(cons string (cons --> (cons (cons list (cons unit ())) ()))))

(declare read-from-string
(cons string (cons --> (cons (cons list (cons unit ())) ()))))

(declare remove
(cons A
Expand Down Expand Up @@ -388,6 +392,8 @@ For an explication of this license see http://www.lambdassociates.org/News/june1

(declare tuple? (cons A (cons --> (cons boolean ()))))

(declare shen-undefmacro (cons symbol (cons --> (cons symbol ()))))

(declare union
(cons (cons list (cons A ()))
(cons -->
Expand Down
4 changes: 2 additions & 2 deletions shen/src/declarations.shen
Expand Up @@ -47,7 +47,7 @@
>= 2 = 2 hd 1 hdv 1 hdstr 1 head 1 if 3 integer? 1 identical 4 inferences 1 intoutput 2 make-string 2
intersection 2 length 1 lineread 0 load 1 < 2 <= 2 vector 1 macroexpand 1 map 2 mapcan 2 intmake-string 2
maxinferences 1 not 1 nth 2 n->string 1 number? 1 output 2 occurs-check 1 occurrences 2 occurs-check 1 or 2
package 3 pos 2 print 1 profile 1 profile-results 1 ps 1 preclude 1 preclude-all-but 1 protect 1 address-> 3 put 4 reassemble 2 read-file-as-string 1 read-file 1 read-byte 1 remove 2 reverse 1 set 2 simple-error 1 snd 1 specialise 1
package 3 pos 2 print 1 profile 1 profile-results 1 ps 1 preclude 1 preclude-all-but 1 protect 1 address-> 3 put 4 reassemble 2 read-file-as-string 1 read-file 1 read-byte 1 read-from-string 1 remove 2 reverse 1 set 2 simple-error 1 snd 1 specialise 1
spy 1 step 1 stinput 1 stoutput 1 string->n 1 string? 1 strong-warning 1 subst 3 symbol? 1 tail 1 tl 1 tc 1 tc? 1 thaw 1
track 1 trap-error 2 tuple? 1 type 1 return 3 undefmacro 1 unprofile 1 unify 4 unify! 4 union 2 untrack 1 unspecialise 1 vector 1
vector-> 3 value 1 variable? 1 version 1 warn 1 write-to-file 2 y-or-n? 1 + 2 * 2 / 2 - 2 == 2 <1> 1 <e> 1
Expand All @@ -66,7 +66,7 @@
variable? value vector-> <-vector vector vector? unspecialise untrack unix union unify unify! unprofile undefmacro
return type tuple? true trap-error track time thaw tc? tc tl tlstr tlv tail systemf synonyms symbol symbol?
subst string? string->n stream string stinput stoutput step spy specialise snd simple-error set save str run
reverse remove read read-file read-file-as-bytelist read-file-as-string read-byte quit put preclude
reverse remove read read-file read-file-as-bytelist read-file-as-string read-byte read-from-string quit put preclude
preclude-all-but ps prolog? protect profile-results profile print pr pos package output out or open occurrences
occurs-check n->string number? number null nth not nl mode macro macroexpand maxinferences mapcan map make-string
load loaded list lineread limit length let lazy lambda is intersection inferences intern integer? input input+
Expand Down
8 changes: 7 additions & 1 deletion shen/src/reader.shen
Expand Up @@ -383,4 +383,10 @@
(doubleunderline? X) (singleunderline? X))
PackageName Exceptions X -> (concat PackageName X)
where (and (symbol? X) (not (prefix? ["s" "h" "e" "n" "-"] (explode X))))
_ _ X -> X)
_ _ X -> X)

(define read-from-string
S -> (let Ns (map (function string->n) (explode S))
(compile (function shen-<st_input>)
Ns
(function shen-read-error))))
5 changes: 4 additions & 1 deletion shen/src/t-star.shen
Expand Up @@ -52,6 +52,7 @@
X A _ <-- (fwhen (typedf? X)) (bind F (sigf X)) (call [F A]);
X A _ <-- (base X A);
X A Hyp <-- (by_hypothesis X A Hyp);
(mode [F] -) A Hyp <-- (th* F [--> A] Hyp);
(mode [F X] -) A Hyp <-- (th* F [B --> A] Hyp) (th* X B Hyp);
(mode [cons X Y] -) [list A] Hyp <-- (th* X A Hyp) (th* Y [list A] Hyp);
(mode [@p X Y] -) [A * B] Hyp <-- (th* X A Hyp) (th* Y B Hyp);
Expand All @@ -65,7 +66,8 @@
(bind X&& (placeholder))
(bind W (ebr X&& X Z))
(th* W A [[X&& : B] | Hyp]);
(mode [open file FileName Direction] -) [stream Direction] Hyp <-- ! (th* FileName string Hyp);
(mode [open file FileName Direction] -) [stream Direction] Hyp
<-- ! (th* FileName string Hyp);
(mode [type X A] -) B Hyp <-- ! (unify A B) (th* X A Hyp);
(mode [input+ : A] -) B Hyp <-- (bind C (normalise-type A)) (unify B C);
(mode [where P X] -) A Hyp <-- ! (th* P boolean Hyp) ! (th* X A [[P : verified] | Hyp]);
Expand Down Expand Up @@ -236,6 +238,7 @@
_ _ N F _ <-- (bind Error (type-insecure-rule-error-message N F));)

(defprolog t*-ruleh
(mode [[] Result] -) [--> A] Hyp <-- ! (th* Result A Hyp);
(mode [Patterns Result] -) A Hyp <-- (t*-patterns Patterns A NewHyp B)
!
(conc NewHyp Hyp AllHyp)
Expand Down
1 change: 1 addition & 0 deletions shen/src/types.shen
Expand Up @@ -109,6 +109,7 @@
(declare read-file-as-bytelist [string --> [list number]])
(declare read-file-as-bytelist [string --> [list number]])
(declare read-file [string --> [list unit]])
(declare read-from-string [string --> [list unit]])
(declare remove [A --> [[list A] --> [list A]]])
(declare reverse [[list A] --> [list A]])
(declare simple-error [string --> A])
Expand Down

0 comments on commit 6dd1d88

Please sign in to comment.