syndicate-lang
/
syndicate-2017
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

start on for loops

This commit is contained in:
Sam Caldwell 2019-04-30 17:42:03 -04:00
parent 899d8c460d
commit 1b2527920e
6 changed files with 204 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
racket/typed/core-types.rkt
View File

@ -717,7 +717,7 @@
(free-identifier=? #'X #'Y)]
[((~∀ (X:id ...) τ1) (~∀ (Y:id ...) τ2))
#:when (stx-length=? #'(X ...) #'(Y ...))
#:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2)
#:with τ2-X/Y (substs #'(Y ...) #'(X ...) #'τ2)
(<: #'τ1 #'τ2-X/Y)]
[((~Base τ1:id) (~Base τ2:id))
(free-identifier=? #'τ1 #'τ2)]

125
racket/typed/for-loops.rkt Normal file
View File

@ -0,0 +1,125 @@
#lang turnstile
(provide for/fold)
(require "core-types.rkt")
(require "sequence.rkt")
(require (only-in "list.rkt" List ~List))
(require (only-in "set.rkt" Set ~Set))
(require (only-in "hash.rkt" Hash ~Hash))
(begin-for-syntax
(define-splicing-syntax-class iter-clause
#:attributes (parend)
#:datum-literals (:)
(pattern [x:id seq:expr]
#:attr parend #'[x seq])
(pattern [x:id : τ:type seq:expr]
#:attr parend #'[x : τ seq])
(pattern [(k:id v:id) hash-seq:expr]
#:attr parend #'[(k v) hash-seq])
(pattern (~seq #:when pred:expr)
#:attr parend #'(#:when pred))
(pattern (~seq #:unless pred:expr)
#:attr parend #'(#:unless pred))
(pattern (~seq #:break pred:expr)
#:attr parend #'(#:break pred))))
(begin-for-syntax
(struct loop-clause (exp bindings) #:transparent)
(struct directive (kw exp) #:transparent))
(define-for-syntax (analyze-for-clauses clauses)
(define-values (br binds)
(for/fold ([body-rev '()]
[bindings '()])
([clause (in-syntax clauses)])
(match (analyze-for-clause clause)
[(loop-clause exp bs)
(values (cons exp body-rev)
(append bindings bs))]
[(directive kw exp)
(values (list* exp kw body-rev)
bindings)])))
#`(#,(reverse br)
#,binds))
;; iter-clause -> (U iter-clause directive)
(define-for-syntax (analyze-for-clause clause)
(syntax-parse clause
#:datum-literals (:)
[[x:id seq:expr]
#:and (~typecheck
[⊢ seq ≫ seq- (⇒ : τ-seq)])
#:fail-unless (pure? #'seq-) "pure"
#:do [(define-values (seq-- τ-elems) (make-sequence #'seq- #'τ-seq))]
(loop-clause #`[x #,seq--]
(list #`(x #,τ-elems)))]
[[x:id : τ:type seq:expr]
#:do [(match-define (list seq- (list (list y τ-elems)))
(analyze-for-clause (syntax/loc clause [x seq])))]
#:fail-unless (<: τ-elems #'τ.norm) "unexpected type"
(loop-clause #`[#,y #,seq-]
(list #`(#,y τ.norm)))]
[[(k:id v:id) hash-seq:expr]
#:and (~typecheck
[⊢ hash-seq ≫ hash-seq- (⇒ : (~Hash K V))])
#:fail-unless (pure? #'hash-seq-) "pure"
(loop-clause #`[(k v) (in-hash- hash-seq-)]
(list #'(k K) #'(v V)))]
[(dir:keyword pred)
#:and (~typecheck
[⊢ pred ≫ pred- (⇐ : Bool)])
#:fail-unless (pure? #'pred-) "pure"
(directive #'dir #'pred-)]))
;; Expression Type -> (Values Expression Type)
;; Determine what kind of sequence we're dealing with;
;; if it's not already in Sequence form, wrap the expression in the appropriate in-* form
;; also figure out what the type of elements are to associate with the loop variable
;; hashes handled separately
(define-for-syntax (make-sequence e τ)
(syntax-parse τ
[(~Sequence t)
(values e #'t)]
[(~List t)
(values #`(in-list- #,e) #'t)]
[(~Set t)
(values #`(in-set- #,e) #'t)]
[_
(type-error #:src e
#:msg "not an iterable type: " τ)]))
(define-typed-syntax for/fold
[(for/fold ([acc:id (~optional (~datum :)) τ-acc init])
(clause:iter-clause
...)
e-body ...+) ≫
[⊢ init ≫ init- (⇐ : τ-acc)]
#:fail-unless (pure? #'init-) "expression must be pure"
#:with (clauses- ([x τ] ...)) (analyze-for-clauses #'(clause.parend ...))
[[x ≫ x- : τ] ...
[acc ≫ acc- : τ-acc] ⊢ (begin e-body ...) ≫ e-body-
(⇐ : τ-acc)
(⇒ ν-ep (~effs τ-ep ...))
(⇒ ν-s (~effs τ-s ...))
(⇒ ν-f (~effs τ-f ...))]
#:with clauses-- (substs #'(x- ...) #'(x ...) #'clauses-)
-------------------------------------------------------
[⊢ (for/fold- ([acc- init-])
(#,@#'clauses--)
e-body-)
(⇒ : τ-acc)
(⇒ ν-ep (τ-ep ...))
(⇒ ν-s (τ-s ...))
(⇒ ν-f (τ-f ...))]]
[(for/fold ([acc:id init])
clauses
e-body ...+) ≫
[⊢ init ≫ _ (⇒ : τ-acc)]
---------------------------------------------------
[≻ (for/fold ([acc τ-acc init])
clauses
e-body ...)]])

38
racket/typed/list.rkt
View File

@ -8,8 +8,7 @@
rest
member?
empty?
for
for/fold)
reverse)
(require "core-types.rkt")
(require (postfix-in - racket/list))
@ -35,38 +34,6 @@
----------------------------------------
[⊢ (cons- e1- e2-) ⇒ τ-l])
(define-typed-syntax (for/fold [acc:id e-acc]
[x:id e-list]
e-body ...+) ≫
[⊢ e-list ≫ e-list- ⇒ (~List τ-l)]
#:fail-unless (pure? #'e-list-) "expression must be pure"
[⊢ e-acc ≫ e-acc- ⇒ τ-a]
#:fail-unless (pure? #'e-acc-) "expression must be pure"
[[x ≫ x- : τ-l] [acc ≫ acc- : τ-a] ⊢ (begin e-body ...) ≫ e-body- ⇒ τ-b]
#:fail-unless (pure? #'e-body-) "body must be pure"
#:fail-unless (<: #'τ-b #'τ-a)
"loop body doesn't match accumulator"
-------------------------------------------------------
[⊢ (for/fold- ([acc- e-acc-])
([x- (in-list- e-list-)])
e-body-)
⇒ τ-b])
(define-typed-syntax (for ([x:id e-list] ...)
e-body ...+) ≫
[⊢ e-list ≫ e-list- ⇒ (~List τ-l)] ...
#:fail-unless (all-pure? #'(e-list- ...)) "expressions must be pure"
[[x ≫ x- : τ-l] ... ⊢ (begin e-body ...) ≫ e-body- (⇒ : τ-b)
(⇒ ν-ep (~effs eps ...))
(⇒ ν-f (~effs fs ...))
(⇒ ν-s (~effs ss ...))]
-------------------------------------------------------
[⊢ (for- ([x- (in-list- e-list-)] ...)
e-body-) (⇒ : ★/t)
(⇒ ν-ep (eps ...))
(⇒ ν-f (fs ...))
(⇒ ν-s (ss ...))])
(define-typed-syntax (empty? e) ≫
[⊢ e ≫ e- ⇒ (~List _)]
#:fail-unless (pure? #'e-) "expression must be pure"
@ -96,3 +63,6 @@
(define- (member?- v l)
(and- (member- v l) #t))
(require/typed racket/base
[reverse : (∀ (X) (→fn (List X) (List X)))])

2
racket/typed/prim.rkt
View File

@ -22,6 +22,8 @@
(define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(define-primop even? (→fn Int Bool))
(define-primop odd? (→fn Int Bool))
(define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns))))
(define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns))))

3
racket/typed/roles.rkt
View File

@ -41,6 +41,8 @@
(all-from-out "sequence.rkt")
;; hash tables
(all-from-out "hash.rkt")
;; for loops
(all-from-out "for-loops.rkt")
;; DEBUG and utilities
print-type print-role
;; Extensions
@ -57,6 +59,7 @@
(require "prim.rkt")
(require "sequence.rkt")
(require "hash.rkt")
(require "for-loops.rkt")
(require (prefix-in syndicate: syndicate/actor-lang))

69
racket/typed/tests/for-loops.rkt Normal file
View File

@ -0,0 +1,69 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type (for/fold ([x 0])
([y (list 1 2 3)])
x)
: Int
⇒ 0)
(check-type (for/fold ([x 0])
([y (list 1 2 3)])
y)
: Int
⇒ 3)
(define-type-alias Inventory (List (Tuple String Int)))
(define inventory0 (list (tuple "The Wind in the Willows" 5)
(tuple "Catch 22" 2)
(tuple "Candide" 33)))
(check-type (for/fold ([stock 0])
([item inventory0])
(select 1 item))
: Int
⇒ 33)
(check-type (for/fold ([stock 0])
([item inventory0])
(if (equal? "Catch 22" (select 0 item))
(select 1 item)
stock))
: Int
⇒ 2)
(define (lookup [title : String]
[inv : Inventory] -> Int)
(for/fold ([stock 0])
([item inv])
(if (equal? title (select 0 item))
(select 1 item)
stock)))
(check-type lookup : (→fn String Inventory Int))
(define (zip [xs : (List Int)]
[ys : (List Int)])
((inst reverse (Tuple Int Int))
(for/fold ([acc : (List (Tuple Int Int))
(list)])
([x xs]
[y ys])
(cons (tuple x y) acc))))
(check-type (zip (list 1 2 3) (list 4 5 6))
: (List (Tuple Int Int))
⇒ (list (tuple 1 4) (tuple 2 5) (tuple 3 6)))
(define (zip-even [xs : (List Int)]
[ys : (List Int)])
((inst reverse (Tuple Int Int))
(for/fold ([acc : (List (Tuple Int Int))
(list)])
([x xs]
#:when (even? x)
[y ys]
#:when (even? y))
(cons (tuple x y) acc))))