Skip to content
This repository
Browse code

Move type rep

  • Loading branch information...
commit 109fbaf3d0fbb01587319e6a0f7c62cccd891bc4 1 parent 49af16f
Ambrose Bonnaire-Sergeant authored November 17, 2012
782  src/typed/core.clj
@@ -268,790 +268,10 @@
268 268
 
269 269
 (declare abstract-many instantiate-many)
270 270
 
271  
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
272  
-;; Types
273  
-
274  
-(def nat? (every-pred integer? (complement neg?)))
275  
-
276  
-(def Type ::Type)
277  
-
278  
-(defn Type? [a]
279  
-  (isa? (class a) Type))
280  
-
281  
-(declare TCResult? Result? Function? DottedPretype? TypeFn?)
282  
-
283  
-(def AnyType ::AnyType)
284  
-
285  
-(defn AnyType? [a]
286  
-  (isa? (class a) AnyType))
287  
-
288  
-(derive Type AnyType)
289  
-
290  
-(defn declare-type [a]
291  
-  (derive a Type))
292  
-
293  
-(defn declare-AnyType [a]
294  
-  (derive a AnyType))
295  
-
296  
-(defrecord Top []
297  
-  "The top type"
298  
-  [])
299  
-
300  
-(def -any (->Top))
301  
-
302  
-(declare-type Top)
303  
-
304  
-;FIXME proper union maker, with sorted types
305  
-(defrecord Union [types]
306  
-  "An flattened, unordered union of types"
307  
-  [(set? types)
308  
-   (every? Type? types)
309  
-   (not (some Union? types))])
310  
-
311  
-(declare-type Union)
312  
-
313  
-(declare ->HeterogeneousMap HeterogeneousMap? Bottom)
314  
-
315  
-(def empty-union (->Union #{}))
316  
-
317  
-(defn -hmap [types]
318  
-  (if (some #(= (Bottom) %) (concat (keys types) (vals types)))
319  
-    (Bottom)
320  
-    (->HeterogeneousMap types)))
321  
-
322  
-#_(defn simplify-HMap-Un [hmaps]
323  
-  {:pre [(every? HeterogeneousMap? hmaps)]
324  
-   :post [(Type? %)]}
325  
-  (let [mss (vals
326  
-              (group-by #(-> % :types keys set) (set hmaps)))
327  
-        ;union the vals of maps with exactly the same keys
328  
-        flat (set
329  
-               (for [ms mss]
330  
-                 (-hmap
331  
-                   (apply merge-with Un
332  
-                          (map :types ms)))))]
333  
-    (if (= 1 (count flat))
334  
-      (first flat)
335  
-      (->Union flat))))
336  
-
337  
-(defn Un [& types]
338  
-  (let [types (disj (set types) empty-union)]
339  
-    (cond
340  
-      (empty? types) empty-union
341  
-      (= 1 (count types)) (first types)
342  
-      :else (->Union (set (apply concat
343  
-                                 (for [t (set types)]
344  
-                                   (if (Union? t)
345  
-                                     (:types t)
346  
-                                     [t]))))))))
347  
-
348  
-(defn Bottom []
349  
-  empty-union)
350  
-
351  
-(def -nothing (Bottom))
352  
-
353  
-(defn Bottom? [a]
354  
-  (= empty-union a))
355  
-
356  
-(declare Function? Poly? PolyDots?)
357  
-
358  
-;should probably be ordered
359  
-(defrecord Intersection [types]
360  
-  "An unordered intersection of types."
361  
-  [(seq types)
362  
-   (every? Type? types)])
363  
-
364  
-(defrecord FnIntersection [types]
365  
-  "An ordered intersection of Functions."
366  
-  [(seq types)
367  
-   (sequential? types)
368  
-   (every? Function? types)])
369  
-
370  
-(declare-type FnIntersection)
371  
-
372  
-(declare In HeterogeneousMap? ->HeterogeneousMap overlap)
373  
-
374  
-(defn In [& types]
375  
-  {:pre [(every? Type? types)]
376  
-   :post [(Type? %)]}
377  
-           ;flatten intersections
378  
-  (let [ts (set (apply concat
379  
-                       (for [t (set types)]
380  
-                         (if (Intersection? t)
381  
-                           (:types t)
382  
-                           [t]))))]
383  
-    (cond
384  
-      (or (empty? ts)
385  
-          (ts (Un))) (Bottom)
386  
-
387  
-      (= 1 (count ts)) (first ts)
388  
-
389  
-      ; if there no overlap
390  
-      (and (<= (count ts) 2)
391  
-           (some (fn [[t1 t2]] (not (overlap t1 t2))) (comb/combinations ts 2))) (Bottom)
392  
-
393  
-      (some Union? ts) (let [flat (set (mapcat #(if (Union? %)
394  
-                                                  (:types %)
395  
-                                                  [%])
396  
-                                               ts))]
397  
-                         (apply Un
398  
-                                (set
399  
-                                  (for [[t1 t2] (comb/combinations flat 2)]
400  
-                                    (In t1 t2)))))
401  
-
402  
-      (ts -any) (apply In (disj ts -any))
403  
-      :else (->Intersection ts))))
404  
-
405  
-(declare-type Intersection)
406  
-
407  
-(def variances #{:constant :covariant :contravariant :invariant :dotted})
408  
-
409  
-(defn variance? [v]
410  
-  (contains? variances v))
411  
-
412  
-(declare Scope? TypeFn?)
413  
-
414  
-(defrecord Bounds [upper-bound lower-bound higher-kind]
415  
-  "A type bound or higher-kind bound on a variable"
416  
-  [(some-fn (and (every? (some-fn Type? Scope?) [upper-bound lower-bound])
417  
-                 (nil? higher-kind))
418  
-            (and (every? nil? [upper-bound lower-bound])
419  
-                 (TypeFn? higher-kind)))])
420  
-
421  
-(defrecord B [idx]
422  
-  "A bound variable. Should not appear outside this file"
423  
-  [(nat? idx)])
424  
-
425  
-(declare-type B)
426  
-
427  
-(defrecord F [name]
428  
-  "A named free variable"
429  
-  [(symbol? name)])
430  
-
431  
-(defn make-F
432  
-  "Make a free variable "
433  
-  [name] (->F name))
434  
-
435  
-(declare-type F)
436  
-
437  
-(declare Scope?)
438  
-
439  
-(defrecord Scope [body]
440  
-  "A scope that contains one bound variable, can be nested. Not used directly"
441  
-  [((some-fn Type? Scope?) body)])
442  
-
443  
-(defn scope-depth? 
444  
-  "True if scope is has depth number of scopes nested"
445  
-  [scope depth]
446  
-  {:pre [(Scope? scope)
447  
-         (nat? depth)]}
448  
-  (Type? (last (take (inc depth) (iterate #(and (Scope? %)
449  
-                                                (:body %))
450  
-                                          scope)))))
451  
-
452  
-(defrecord Projection [afn ts]
453  
-  "Projects type variables as arguments to afn"
454  
-  [(fn? afn)
455  
-   (every? AnyType? ts)])
456  
-
457  
-(declare-type Projection)
458  
-
459  
-(defrecord RClass [variances poly? the-class replacements]
460  
-  "A restricted class, where ancestors are
461  
-  (replace replacements (ancestors the-class))"
462  
-  [(or (nil? variances)
463  
-       (and (seq variances)
464  
-            (sequential? variances)
465  
-            (every? variance? variances)))
466  
-   (or (nil? poly?)
467  
-       (and (seq poly?)
468  
-            (sequential? poly?)
469  
-            (every? Type? poly?)))
470  
-   (symbol? the-class)
471  
-   ((hash-c? symbol? (some-fn Type? Scope?)) replacements)])
472  
-
473  
-(declare-type RClass)
474  
-
475  
-(defn RClass->Class [rcls]
476  
-  (Class/forName (str (.the-class rcls))))
477  
-
478  
-(declare RESTRICTED-CLASS instantiate-poly Class->symbol)
479  
-
480  
-(defn RClass-of 
481  
-  ([sym-or-cls] (RClass-of sym-or-cls nil))
482  
-  ([sym-or-cls args]
483  
-   {:pre [((some-fn class? symbol?) sym-or-cls)
484  
-          (every? Type? args)]
485  
-    :post [(RClass? %)]}
486  
-   (let [sym (if (class? sym-or-cls)
487  
-               (Class->symbol sym-or-cls)
488  
-               sym-or-cls)
489  
-         rc (@RESTRICTED-CLASS sym)]
490  
-     (assert ((some-fn Poly? RClass? nil?) rc))
491  
-     (assert (or (Poly? rc) (not args)) (str "Cannot instantiate non-polymorphic RClass " sym))
492  
-     (cond 
493  
-       (Poly? rc) (instantiate-poly rc args)
494  
-       (RClass? rc) rc
495  
-       :else (->RClass nil nil sym {})))))
496  
-
497  
-(declare Poly* no-bounds)
498  
-
499  
-;smart constructor
500  
-(defn RClass* [names variances poly? the-class replacements]
501  
-  {:pre [(every? symbol? names)
502  
-         (every? variance? variances)
503  
-         (= (count variances) (count poly?))
504  
-         (every? Type? poly?)
505  
-         (symbol? the-class)]}
506  
-  (if (seq variances)
507  
-    (Poly* names (repeat (count names) no-bounds) (->RClass variances poly? the-class replacements) names)
508  
-    (->RClass nil nil the-class replacements)))
509  
-
510  
-(declare poly-RClass-from)
511  
-
512  
-(declare substitute-many unparse-type Class->symbol symbol->Class)
513  
-
514  
-(defn RClass-supers* 
515  
-  "Return a set of ancestors to the RClass"
516  
-  [{:keys [poly? replacements the-class] :as rcls}]
517  
-  {:pre [(RClass? rcls)]
518  
-   :post [(set? %)
519  
-          (every? Type? %)
520  
-          (<= (count (filter (some-fn FnIntersection? Poly? PolyDots?) %))
521  
-              1)]}
522  
-  (let [;set of symbols of Classes we haven't explicitly replaced
523  
-        not-replaced (set/difference (set (map Class->symbol (-> the-class symbol->Class supers)))
524  
-                                     (set (keys replacements)))]
525  
-    (set/union (set (for [csym not-replaced]
526  
-                      (RClass-of csym nil)))
527  
-               (set (vals replacements))
528  
-               #{(RClass-of Object)})))
529  
-
530  
-(defrecord Record [the-class fields]
531  
-  "A record"
532  
-  [(class? the-class)
533  
-   ((array-map-c? symbol? Type?) fields)])
534  
-
535  
-(declare-type Record)
536  
-
537  
-(defrecord DataType [the-class variances poly? fields]
538  
-  "A Clojure datatype"
539  
-  [(or (nil? variances)
540  
-       (and (seq variances)
541  
-            (every? variance? variances)))
542  
-   (or (nil? poly?)
543  
-       (and (seq poly?)
544  
-            (every? Type? poly?)))
545  
-   (symbol? the-class)
546  
-   ((array-map-c? symbol? (some-fn Scope? Type?)) fields)])
547  
-
548  
-(declare-type DataType)
549  
-
550  
-(defrecord Protocol [the-var variances poly? on-class methods]
551  
-  "A Clojure Protocol"
552  
-  [(symbol? the-var)
553  
-   (or (nil? variances)
554  
-       (and (seq variances)
555  
-            (every? variance? variances)))
556  
-   (or (nil? poly?)
557  
-       (and (seq poly?)
558  
-            (every? Type? poly?)))
559  
-   (= (count poly?) (count variances))
560  
-   (symbol? on-class)
561  
-   ((hash-c? (every-pred symbol? (complement namespace)) Type?) methods)])
562  
-
563  
-(declare-type Protocol)
564  
-
565  
-(defrecord TypeFn [nbound variances bbnds scope]
566  
-  "A type function containing n bound variables with variances.
567  
-  It is of a higher kind"
568  
-  [(nat? nbound)
569  
-   (every? variance? variances)
570  
-   (every? Bounds? bbnds)
571  
-   (apply = nbound (map count [variances bbnds]))
572  
-   (scope-depth? scope nbound)
573  
-   (Scope? scope)])
574  
-
575  
-(declare-type TypeFn)
576  
-
577  
-(defn tfn-bound [tfn]
578  
-  (->Bounds nil nil tfn))
579  
-
580  
-(declare visit-bounds)
581  
-
582  
-;smart constructor
583  
-(defn TypeFn* [names variances bbnds body]
584  
-  {:pre [(every? symbol names)
585  
-         (every? variance? variances)
586  
-         (every? Bounds? bbnds)
587  
-         (apply = (map count [names variances bbnds]))
588  
-         ((some-fn TypeFn? Type?) body)]}
589  
-  (if (empty? names)
590  
-    body
591  
-    (->TypeFn (count names) 
592  
-              variances
593  
-              (vec
594  
-                (for [bnd bbnds]
595  
-                  (visit-bounds bnd #(abstract-many names %))))
596  
-              (abstract-many names body))))
597  
-
598  
-;smart destructor
599  
-(defn TypeFn-body* [names typefn]
600  
-  {:pre [(every? symbol? names)
601  
-         (TypeFn? typefn)]}
602  
-  (assert (= (.nbound typefn) (count names)) "Wrong number of names")
603  
-  (instantiate-many names (.scope typefn)))
604  
-
605  
-(defn TypeFn-bbnds* [names typefn]
606  
-  {:pre [(every? symbol? names)
607  
-         (TypeFn? typefn)]
608  
-   :post [(every? Bounds? %)]}
609  
-  (assert (= (.nbound typefn) (count names)) "Wrong number of names")
610  
-  (mapv (fn [b]
611  
-          (visit-bounds b #(instantiate-many names %)))
612  
-        (.bbnds typefn)))
613  
-
614  
-(defrecord Poly [nbound bbnds scope actual-frees]
615  
-  "A polymorphic type containing n bound variables, with display names actual-frees"
616  
-  [(nat? nbound)
617  
-   (every? Bounds? bbnds)
618  
-   (every? symbol? actual-frees)
619  
-   (apply = nbound (map count [bbnds actual-frees]))
620  
-   (scope-depth? scope nbound)
621  
-   (Scope? scope)])
622  
-
623  
-(declare-type Poly)
624  
-
625  
-;smart constructor
626  
-(defn Poly* [names bbnds body free-names]
627  
-  {:pre [(every? symbol names)
628  
-         (every? Bounds? bbnds)
629  
-         (Type? body)
630  
-         (every? symbol? free-names)
631  
-         (apply = (map count [names bbnds free-names]))]}
632  
-  (if (empty? names)
633  
-    body
634  
-    (->Poly (count names) 
635  
-            (vec
636  
-              (for [bnd bbnds]
637  
-                (visit-bounds bnd #(abstract-many names %))))
638  
-            (abstract-many names body)
639  
-            free-names)))
640  
-
641  
-(defn Poly-free-names* [poly]
642  
-  {:pre [(Poly? poly)]
643  
-   :post [((every-pred seq (every-c? symbol?)) %)]}
644  
-  (.actual-frees poly))
645  
-
646  
-;smart destructor
647  
-(defn Poly-body* [names poly]
648  
-  {:pre [(every? symbol? names)
649  
-         (Poly? poly)]}
650  
-  (assert (= (.nbound poly) (count names)) "Wrong number of names")
651  
-  (instantiate-many names (.scope poly)))
652  
-
653  
-(defn Poly-bbnds* [names poly]
654  
-  {:pre [(every? symbol? names)
655  
-         (Poly? poly)]}
656  
-  (assert (= (.nbound poly) (count names)) "Wrong number of names")
657  
-  (mapv (fn [b]
658  
-          (visit-bounds b #(instantiate-many names %)))
659  
-        (.bbnds poly)))
660  
-
661  
-(defrecord PolyDots [nbound bbnds scope]
662  
-  "A polymorphic type containing n-1 bound variables and 1 ... variable"
663  
-  [(nat? nbound)
664  
-   (every? Bounds? bbnds)
665  
-   (= nbound (count bbnds))
666  
-   (scope-depth? scope nbound)
667  
-   (Scope? scope)])
668  
-
669  
-(declare-type PolyDots)
670  
-
671  
-;smart constructor
672  
-(defn PolyDots* [names bbnds body]
673  
-  {:pre [(every? symbol names)
674  
-         (every? Bounds? bbnds)
675  
-         (Type? body)]}
676  
-  (assert (= (count names) (count bbnds)) "Wrong number of names")
677  
-  (if (empty? names)
678  
-    body
679  
-    (->PolyDots (count names) 
680  
-                (vec
681  
-                  (for [bnd bbnds]
682  
-                    (-> bnd
683  
-                      (update-in [:upper-bound] #(abstract-many names %))
684  
-                      (update-in [:lower-bound] #(abstract-many names %)))))
685  
-                (abstract-many names body))))
686  
-
687  
-;smart destructor
688  
-(defn PolyDots-body* [names poly]
689  
-  {:pre [(every? symbol? names)
690  
-         (PolyDots? poly)]}
691  
-  (assert (= (:nbound poly) (count names)) "Wrong number of names")
692  
-  (instantiate-many names (:scope poly)))
693  
-
694  
-(defn PolyDots-bbnds* [names poly]
695  
-  {:pre [(every? symbol? names)
696  
-         (PolyDots? poly)]}
697  
-  (assert (= (:nbound poly) (count names)) "Wrong number of names")
698  
-  (mapv (fn [b]
699  
-          (-> b
700  
-            (update-in [:upper-bound] #(instantiate-many names %))
701  
-            (update-in [:lower-bound] #(instantiate-many names %))))
702  
-        (:bbnds poly)))
703  
-
704  
-(defrecord Name [id]
705  
-  "A late bound name"
706  
-  [((every-pred (some-fn namespace (fn [a] (some (fn [c] (= \. c)) (str a))))
707  
-                symbol?) 
708  
-     id)])
709  
-
710  
-(defrecord TApp [rator rands]
711  
-  "An application of a type function to arguments."
712  
-  [((some-fn Name? TypeFn? F? B?) rator)
713  
-   (every? (some-fn TypeFn? Type?) rands)])
714  
-
715  
-(declare-type TApp) ;not always a type
716  
-
717  
-(defrecord App [rator rands]
718  
-  "An application of a polymorphic type to type arguments"
719  
-  [(Type? rator)
720  
-   (every? Type? rands)])
721  
-
722  
-(declare -resolve)
723  
-
724  
-(declare ->t-subst subst-all Mu? unfold)
725  
-
726  
-(defn make-simple-substitution [vs ts]
727  
-  {:pre [(every? symbol? vs)
728  
-         (every? Type? ts)
729  
-         (= (count vs)
730  
-            (count ts))]}
731  
-  (into {} (for [[v t] (map vector vs ts)]
732  
-             [v (->t-subst t no-bounds)])))
733  
-
734  
-(declare error-msg)
735  
-
736  
-(defn instantiate-typefn [t types]
737  
-  (assert (TypeFn? t) (unparse-type t))
738  
-  (do (assert (= (.nbound t) (count types)) (error-msg "Wrong number of arguments passed to type function: "
739  
-                                                       (unparse-type t) (mapv unparse-type types)))
740  
-    (let [nms (repeatedly (.nbound t) gensym)
741  
-          body (TypeFn-body* nms t)]
742  
-      (subst-all (make-simple-substitution nms types) body))))
743  
-
744  
-(defn instantiate-poly [t types]
745  
-  (cond
746  
-    (Poly? t) (do (assert (= (:nbound t) (count types)) (error-msg "Wrong number of arguments passed to polymorphic type: "
747  
-                                                             (unparse-type t) (mapv unparse-type types)))
748  
-                (let [nms (repeatedly (:nbound t) gensym)
749  
-                      body (Poly-body* nms t)]
750  
-                  (subst-all (make-simple-substitution nms types) body)))
751  
-    ;PolyDots NYI
752  
-    :else (throw (Exception. "instantiate-poly: requires Poly, and PolyDots NYI"))))
753  
-
754  
-(declare ^:dynamic *current-env* resolve-app*)
755  
-
756  
-(declare resolve-tapp*)
757  
-
758  
-(defn resolve-TApp [app]
759  
-  {:pre [(TApp? app)]}
760  
-  (resolve-tapp* (.rator app) (.rands app)))
761  
-
762  
-(defn resolve-tapp* [rator rands]
763  
-  (let [rator (-resolve rator)
764  
-        _ (assert (TypeFn? rator) (unparse-type rator))]
765  
-    (assert (= (count rands) (.nbound rator))
766  
-            (error-msg "Wrong number of arguments provided to type function"
767  
-                       (unparse-type rator)))
768  
-    (instantiate-typefn rator rands)))
769  
-
770  
-(defn resolve-App [app]
771  
-  {:pre [(App? app)]}
772  
-  (resolve-app* (.rator app) (.rands app)))
773  
-
774  
-(defn resolve-app* [rator rands]
775  
-  (let [rator (-resolve rator)]
776  
-    (cond
777  
-      (Poly? rator) (do (assert (= (count rands) (.nbound rator))
778  
-                                (error-msg "Wrong number of arguments provided to polymorphic type"
779  
-                                     (unparse-type rator)))
780  
-                      (instantiate-poly rator rands))
781  
-      ;PolyDots NYI
782  
-      :else (throw (Exception. (str (when *current-env*
783  
-                                      (str (:line *current-env*) ": "))
784  
-                                    "Cannot apply non-polymorphic type " (unparse-type rator)))))))
785  
-
786  
-(declare-type App)
787  
-
788  
-(declare resolve-name* resolve-Name)
789  
-
790  
-(defn -resolve [ty]
791  
-  {:pre [(AnyType? ty)]}
792  
-  (cond 
793  
-    (Name? ty) (resolve-Name ty)
794  
-    (Mu? ty) (unfold ty)
795  
-    (App? ty) (resolve-App ty)
796  
-    (TApp? ty) (resolve-TApp ty)
797  
-    :else ty))
798  
-
799  
-(defn requires-resolving? [ty]
800  
-  (or (Name? ty)
801  
-      (App? ty)
802  
-      (and (TApp? ty)
803  
-           (not (F? (.rator ty))))
804  
-      (Mu? ty)))
805  
-
806  
-(defn resolve-Name [nme]
807  
-  {:pre [(Name? nme)]}
808  
-  (resolve-name* (:id nme)))
809  
-
810  
-(declare-type Name)
811  
-
812  
-(defrecord Mu [scope]
813  
-  "A recursive type containing one bound variable, itself"
814  
-  [(Scope? scope)])
815  
-
816  
-(declare instantiate substitute remove-scopes subtype? abstract)
817  
-
818  
-;smart constructor
819  
-(defn Mu* [name body]
820  
-  (->Mu (abstract name body)))
821  
-
822  
-;smart destructor
823  
-(defn Mu-body* [name t]
824  
-  {:pre [(Mu? t)
825  
-         (symbol? name)]}
826  
-  (instantiate name (:scope t)))
827  
-
828  
-(defn unfold [t]
829  
-  {:pre [(Mu? t)]
830  
-   :post [(Type? %)]}
831  
-  (let [sym (gensym)
832  
-        body (Mu-body* sym t)]
833  
-    (substitute t sym body)))
834  
-
835  
-(declare-type Mu)
836  
-
837  
-(defrecord Value [val]
838  
-  "A Clojure value"
839  
-  [])
840  
-
841  
-(defrecord AnyValue []
842  
-  "Any Value"
843  
-  [])
844  
-
845  
-(def -val ->Value)
846  
-
847  
-(declare-type Value)
848  
-(declare-type AnyValue)
849  
-
850  
-(defrecord HeterogeneousMap [types]
851  
-  "A constant map, clojure.lang.IPersistentMap"
852  
-  [((hash-c? Value? (some-fn Type? Result?))
853  
-     types)])
854  
-
855  
-(defn make-HMap [mandatory optional]
856  
-  (assert (= #{}
857  
-             (set/intersection (-> mandatory keys set)
858  
-                               (-> optional keys set))))
859  
-  (apply Un
860  
-         (for [ss (map #(into {} %) (comb/subsets optional))]
861  
-           (-hmap (merge mandatory ss)))))
862  
-
863  
-(declare-type HeterogeneousMap)
864  
-
865  
-(defrecord HeterogeneousVector [types]
866  
-  "A constant vector, clojure.lang.IPersistentVector"
867  
-  [(vector? types)
868  
-   (every? (some-fn Type? Result?) types)])
869  
-
870  
-(defn -hvec [types]
871  
-  (if (some Bottom? types)
872  
-    (Bottom)
873  
-    (->HeterogeneousVector types)))
874  
-
875  
-(declare-type HeterogeneousVector)
876  
-
877  
-(defrecord HeterogeneousList [types]
878  
-  "A constant list, clojure.lang.IPersistentList"
879  
-  [(sequential? types)
880  
-   (every? Type? types)])
881  
-
882  
-(declare-type HeterogeneousList)
883  
-
884  
-(defrecord HeterogeneousSeq [types]
885  
-  "A constant seq, clojure.lang.ISeq"
886  
-  [(sequential? types)
887  
-   (every? Type? types)])
888  
-
889  
-(declare-type HeterogeneousSeq)
890  
-
891  
-(defrecord PrimitiveArray [jtype input-type output-type]
892  
-  "A Java Primitive array"
893  
-  [(class? jtype)
894  
-   (Type? input-type)
895  
-   (Type? output-type)])
896  
-
897  
-(declare-type PrimitiveArray)
898  
-
899  
-(declare Result?)
900  
-
901  
-(defrecord DottedPretype [pre-type name]
902  
-  "A dotted pre-type. Not a type"
903  
-  [(Type? pre-type)
904  
-   ((some-fn symbol? nat?) name)])
905  
-
906  
-(declare-AnyType DottedPretype)
907  
-
908  
-(defrecord KwArgs [mandatory optional]
909  
-  "A set of mandatory and optional keywords"
910  
-  [(map? mandatory)
911  
-   (map? optional)
912  
-   (every? Value? (map keys [mandatory optional]))
913  
-   (every? Type? (map vals [mandatory optional]))])
914  
-
915  
-(defrecord Function [dom rng rest drest kws]
916  
-  "A function arity, must be part of an intersection"
917  
-  [(or (nil? dom)
918  
-       (sequential? dom))
919  
-   (every? Type? dom)
920  
-   (Result? rng)
921  
-   (<= (count (filter identity [rest drest kws])) 1)
922  
-   (or (nil? rest)
923  
-       (Type? rest))
924  
-   (or (nil? drest)
925  
-       (DottedPretype? drest))
926  
-   (or (nil? kws)
927  
-       (KwArgs? kws))])
928  
-
929  
-(declare-AnyType Function)
930  
-
931  
-(defrecord TopFunction []
932  
-  "Supertype to all functions"
933  
-  [])
934  
-
935  
-(defrecord CountRange [lower upper]
936  
-  "A sequence of count between lower and upper.
937  
-  If upper is nil, between lower and infinity."
938  
-  [(nat? lower)
939  
-   (or (nil? upper)
940  
-       (and (nat? upper)
941  
-            (<= lower upper)))])
942  
-
943  
-(defrecord GTRange [n]
944  
-  "The type of all numbers greater than n"
945  
-  [(number? n)])
946  
-
947  
-(defrecord LTRange [n]
948  
-  "The type of all numbers less than n"
949  
-  [(number? n)])
950  
-
951  
-(declare-type CountRange)
952  
-(declare-type GTRange)
953  
-(declare-type LTRange)
954  
-
955  
-(defn make-CountRange
956  
-  ([lower] (make-CountRange lower nil))
957  
-  ([lower upper] (->CountRange lower upper)))
958  
-
959  
-(defn make-ExactCountRange [c]
960  
-  {:pre [(nat? c)]}
961  
-  (make-CountRange c c))
962  
-
963  
-(declare ->EmptyObject ->Result -FS -top)
964  
-
965  
-(defn make-Result
966  
-  "Make a result. ie. the range of a Function"
967  
-  ([t] (make-Result t nil nil))
968  
-  ([t f] (make-Result t f nil))
969  
-  ([t f o] (->Result t (or f (-FS -top -top)) (or o (->EmptyObject)))))
970  
-
971  
-(declare ret-t ret-f ret-o)
972  
-
973  
-(defn make-Function
974  
-  "Make a function, wrap range type in a Result.
975  
-  Accepts optional :filter and :object parameters that default to the most general filter
976  
-  and EmptyObject"
977  
-  ([dom rng] (make-Function dom rng nil nil))
978  
-  ([dom rng rest] (make-Function dom rng rest nil))
979  
-  ([dom rng rest drest & {:keys [filter object kws]}]
980  
-   (->Function dom (->Result rng (or filter (-FS -top -top)) (or object (->EmptyObject))) rest drest kws)))
981  
-
982  
-(defn make-FnIntersection [& fns]
983  
-  {:pre [(every? Function? fns)]}
984  
-  (->FnIntersection fns))
985  
-
986  
-(defrecord NotType [type]
987  
-  "A type that does not include type"
988  
-  [(Type? type)])
989  
-
990  
-(declare-type NotType)
991  
-
992  
-(defrecord ListDots [pre-type bound]
993  
-  "A dotted list"
994  
-  [(Type? pre-type)
995  
-   ((some-fn F? B?) bound)])
996  
-
997  
-(declare-type ListDots)
998  
-
999  
-(declare abstract)
1000  
-
1001  
-(declare Filter? RObject? ret)
1002  
-
1003  
-(defrecord Result [t fl o]
1004  
-  "A result type with filter f and object o. NOT a type."
1005  
-  [(Type? t)
1006  
-   (Filter? fl)
1007  
-   (RObject? o)])
1008  
-
1009  
-(declare-AnyType Result)
1010  
-
1011  
-(defn Result->TCResult [{:keys [t fl o] :as r}]
1012  
-  {:pre [(Result? r)]
1013  
-   :post [(TCResult? %)]}
1014  
-  (ret t fl o))
1015  
-
1016  
-(defn Result-type* [r]
1017  
-  {:pre [(Result? r)]
1018  
-   :post [(Type? %)]}
1019  
-  (:t r))
1020  
-
1021  
-(defn Result-filter* [r]
1022  
-  {:pre [(Result? r)]
1023  
-   :post [(Filter? %)]}
1024  
-  (:fl r))
1025  
-
1026  
-(defn Result-object* [r]
1027  
-  {:pre [(Result? r)]
1028  
-   :post [(RObject? %)]}
1029  
-  (:o r))
1030  
-
1031  
-(def no-bounds (->Bounds (->Top) (Un) nil))
1032  
-
1033  
-
1034  
-(declare unparse-path-elem)
1035  
-
1036  
-(declare TypeFilter? NotTypeFilter? type-of TCResult? ret-t Nil? False? True? unparse-type)
1037  
-
1038  
-(def ^:dynamic *mutated-bindings* #{})
1039  
-
1040  
-(defn is-var-mutated? [id]
1041  
-  (contains? *mutated-bindings* id))
1042  
-
  271
+(load "type_rep")
1043 272
 (load "type_ops")
1044 273
 (load "filter_rep")
1045 274
 (load "filter_ops")
1046  
-
1047  
-(defrecord TCResult [t fl o]
1048  
-  "This record represents the result of typechecking an expression"
1049  
-  [(AnyType? t)
1050  
-   (FilterSet? fl)
1051  
-   (RObject? o)])
1052  
-
1053  
-(declare-AnyType TCResult)
1054  
-
1055 275
 (load "path_rep")
1056 276
 (load "object_rep")
1057 277
 
780  type_rep.clj
... ...
@@ -0,0 +1,780 @@
  1
+
  2
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  3
+;; Types
  4
+
  5
+(def nat? (every-pred integer? (complement neg?)))
  6
+
  7
+(def Type ::Type)
  8
+
  9
+(defn Type? [a]
  10
+  (isa? (class a) Type))
  11
+
  12
+(declare TCResult? Result? Function? DottedPretype? TypeFn?)
  13
+
  14
+(def AnyType ::AnyType)
  15
+
  16
+(defn AnyType? [a]
  17
+  (isa? (class a) AnyType))
  18
+
  19
+(derive Type AnyType)
  20
+
  21
+(defn declare-type [a]
  22
+  (derive a Type))
  23
+
  24
+(defn declare-AnyType [a]
  25
+  (derive a AnyType))
  26
+
  27
+(defrecord Top []
  28
+  "The top type"
  29
+  [])
  30
+
  31
+(def -any (->Top))
  32
+
  33
+(declare-type Top)
  34
+
  35
+;FIXME proper union maker, with sorted types
  36
+(defrecord Union [types]
  37
+  "An flattened, unordered union of types"
  38
+  [(set? types)
  39
+   (every? Type? types)
  40
+   (not (some Union? types))])
  41
+
  42
+(declare-type Union)
  43
+
  44
+(declare ->HeterogeneousMap HeterogeneousMap? Bottom)
  45
+
  46
+(def empty-union (->Union #{}))
  47
+
  48
+(defn -hmap [types]
  49
+  (if (some #(= (Bottom) %) (concat (keys types) (vals types)))
  50
+    (Bottom)
  51
+    (->HeterogeneousMap types)))
  52
+
  53
+#_(defn simplify-HMap-Un [hmaps]
  54
+  {:pre [(every? HeterogeneousMap? hmaps)]
  55
+   :post [(Type? %)]}
  56
+  (let [mss (vals
  57
+              (group-by #(-> % :types keys set) (set hmaps)))
  58
+        ;union the vals of maps with exactly the same keys
  59
+        flat (set
  60
+               (for [ms mss]
  61
+                 (-hmap
  62
+                   (apply merge-with Un
  63
+                          (map :types ms)))))]
  64
+    (if (= 1 (count flat))
  65
+      (first flat)
  66
+      (->Union flat))))
  67
+
  68
+(defn Un [& types]
  69
+  (let [types (disj (set types) empty-union)]
  70
+    (cond
  71
+      (empty? types) empty-union
  72
+      (= 1 (count types)) (first types)
  73
+      :else (->Union (set (apply concat
  74
+                                 (for [t (set types)]
  75
+                                   (if (Union? t)
  76
+                                     (:types t)
  77
+                                     [t]))))))))
  78
+
  79
+(defn Bottom []
  80
+  empty-union)
  81
+
  82
+(def -nothing (Bottom))
  83
+
  84
+(defn Bottom? [a]
  85
+  (= empty-union a))
  86
+
  87
+(declare Function? Poly? PolyDots?)
  88
+
  89
+;should probably be ordered
  90
+(defrecord Intersection [types]
  91
+  "An unordered intersection of types."
  92
+  [(seq types)
  93
+   (every? Type? types)])
  94
+
  95
+(defrecord FnIntersection [types]
  96
+  "An ordered intersection of Functions."
  97
+  [(seq types)
  98
+   (sequential? types)
  99
+   (every? Function? types)])
  100
+
  101
+(declare-type FnIntersection)
  102
+
  103
+(declare In HeterogeneousMap? ->HeterogeneousMap overlap)
  104
+
  105
+(defn In [& types]
  106
+  {:pre [(every? Type? types)]
  107
+   :post [(Type? %)]}
  108
+           ;flatten intersections
  109
+  (let [ts (set (apply concat
  110
+                       (for [t (set types)]
  111
+                         (if (Intersection? t)
  112
+                           (:types t)
  113
+                           [t]))))]
  114
+    (cond
  115
+      (or (empty? ts)
  116
+          (ts (Un))) (Bottom)
  117
+
  118
+      (= 1 (count ts)) (first ts)
  119
+
  120
+      ; if there no overlap
  121
+      (and (<= (count ts) 2)
  122
+           (some (fn [[t1 t2]] (not (overlap t1 t2))) (comb/combinations ts 2))) (Bottom)
  123
+
  124
+      (some Union? ts) (let [flat (set (mapcat #(if (Union? %)
  125
+                                                  (:types %)
  126
+                                                  [%])
  127
+                                               ts))]
  128
+                         (apply Un
  129
+                                (set
  130
+                                  (for [[t1 t2] (comb/combinations flat 2)]
  131
+                                    (In t1 t2)))))
  132
+
  133
+      (ts -any) (apply In (disj ts -any))
  134
+      :else (->Intersection ts))))
  135
+
  136
+(declare-type Intersection)
  137
+
  138
+(def variances #{:constant :covariant :contravariant :invariant :dotted})
  139
+
  140
+(defn variance? [v]
  141
+  (contains? variances v))
  142
+
  143
+(declare Scope? TypeFn?)
  144
+
  145
+(defrecord Bounds [upper-bound lower-bound higher-kind]
  146
+  "A type bound or higher-kind bound on a variable"
  147
+  [(some-fn (and (every? (some-fn Type? Scope?) [upper-bound lower-bound])
  148
+                 (nil? higher-kind))
  149
+            (and (every? nil? [upper-bound lower-bound])
  150
+                 (TypeFn? higher-kind)))])
  151
+
  152
+(defrecord B [idx]
  153
+  "A bound variable. Should not appear outside this file"
  154
+  [(nat? idx)])
  155
+
  156
+(declare-type B)
  157
+
  158
+(defrecord F [name]
  159
+  "A named free variable"
  160
+  [(symbol? name)])
  161
+
  162
+(defn make-F
  163
+  "Make a free variable "
  164
+  [name] (->F name))
  165
+
  166
+(declare-type F)
  167
+
  168
+(declare Scope?)
  169
+
  170
+(defrecord Scope [body]
  171
+  "A scope that contains one bound variable, can be nested. Not used directly"
  172
+  [((some-fn Type? Scope?) body)])
  173
+
  174
+(defn scope-depth? 
  175
+  "True if scope is has depth number of scopes nested"
  176
+  [scope depth]
  177
+  {:pre [(Scope? scope)
  178
+         (nat? depth)]}
  179
+  (Type? (last (take (inc depth) (iterate #(and (Scope? %)
  180
+                                                (:body %))
  181
+                                          scope)))))
  182
+
  183
+(defrecord Projection [afn ts]
  184
+  "Projects type variables as arguments to afn"
  185
+  [(fn? afn)
  186
+   (every? AnyType? ts)])
  187
+
  188
+(declare-type Projection)
  189
+
  190
+(defrecord RClass [variances poly? the-class replacements]
  191
+  "A restricted class, where ancestors are
  192
+  (replace replacements (ancestors the-class))"
  193
+  [(or (nil? variances)
  194
+       (and (seq variances)
  195
+            (sequential? variances)
  196
+            (every? variance? variances)))
  197
+   (or (nil? poly?)
  198
+       (and (seq poly?)
  199
+            (sequential? poly?)
  200
+            (every? Type? poly?)))
  201
+   (symbol? the-class)
  202
+   ((hash-c? symbol? (some-fn Type? Scope?)) replacements)])
  203
+
  204
+(declare-type RClass)
  205
+
  206
+(defn RClass->Class [rcls]
  207
+  (Class/forName (str (.the-class rcls))))
  208
+
  209
+(declare RESTRICTED-CLASS instantiate-poly Class->symbol)
  210
+
  211
+(defn RClass-of 
  212
+  ([sym-or-cls] (RClass-of sym-or-cls nil))
  213
+  ([sym-or-cls args]
  214
+   {:pre [((some-fn class? symbol?) sym-or-cls)
  215
+          (every? Type? args)]
  216
+    :post [(RClass? %)]}
  217
+   (let [sym (if (class? sym-or-cls)
  218
+               (Class->symbol sym-or-cls)
  219
+               sym-or-cls)
  220
+         rc (@RESTRICTED-CLASS sym)]
  221
+     (assert ((some-fn Poly? RClass? nil?) rc))
  222
+     (assert (or (Poly? rc) (not args)) (str "Cannot instantiate non-polymorphic RClass " sym))
  223
+     (cond 
  224
+       (Poly? rc) (instantiate-poly rc args)
  225
+       (RClass? rc) rc
  226
+       :else (->RClass nil nil sym {})))))
  227
+
  228
+(declare Poly* no-bounds)
  229
+
  230
+;smart constructor
  231
+(defn RClass* [names variances poly? the-class replacements]
  232
+  {:pre [(every? symbol? names)
  233
+         (every? variance? variances)
  234
+         (= (count variances) (count poly?))
  235
+         (every? Type? poly?)
  236
+         (symbol? the-class)]}
  237
+  (if (seq variances)
  238
+    (Poly* names (repeat (count names) no-bounds) (->RClass variances poly? the-class replacements) names)
  239
+    (->RClass nil nil the-class replacements)))
  240
+
  241
+(declare poly-RClass-from)
  242
+
  243
+(declare substitute-many unparse-type Class->symbol symbol->Class)
  244
+
  245
+(defn RClass-supers* 
  246
+  "Return a set of ancestors to the RClass"
  247
+  [{:keys [poly? replacements the-class] :as rcls}]
  248
+  {:pre [(RClass? rcls)]
  249
+   :post [(set? %)
  250
+          (every? Type? %)
  251
+          (<= (count (filter (some-fn FnIntersection? Poly? PolyDots?) %))
  252
+              1)]}
  253
+  (let [;set of symbols of Classes we haven't explicitly replaced
  254
+        not-replaced (set/difference (set (map Class->symbol (-> the-class symbol->Class supers)))
  255
+                                     (set (keys replacements)))]
  256
+    (set/union (set (for [csym not-replaced]
  257
+                      (RClass-of csym nil)))
  258
+               (set (vals replacements))
  259
+               #{(RClass-of Object)})))
  260
+
  261
+(defrecord Record [the-class fields]
  262
+  "A record"
  263
+  [(class? the-class)
  264
+   ((array-map-c? symbol? Type?) fields)])
  265
+
  266
+(declare-type Record)
  267
+
  268
+(defrecord DataType [the-class variances poly? fields]
  269
+  "A Clojure datatype"
  270
+  [(or (nil? variances)
  271
+       (and (seq variances)
  272
+            (every? variance? variances)))
  273
+   (or (nil? poly?)
  274
+       (and (seq poly?)
  275
+            (every? Type? poly?)))
  276
+   (symbol? the-class)
  277
+   ((array-map-c? symbol? (some-fn Scope? Type?)) fields)])
  278
+
  279
+(declare-type DataType)
  280
+
  281
+(defrecord Protocol [the-var variances poly? on-class methods]
  282
+  "A Clojure Protocol"
  283
+  [(symbol? the-var)
  284
+   (or (nil? variances)
  285
+       (and (seq variances)
  286
+            (every? variance? variances)))
  287
+   (or (nil? poly?)
  288
+       (and (seq poly?)
  289
+            (every? Type? poly?)))
  290
+   (= (count poly?) (count variances))
  291
+   (symbol? on-class)
  292
+   ((hash-c? (every-pred symbol? (complement namespace)) Type?) methods)])
  293
+
  294
+(declare-type Protocol)
  295
+
  296
+(defrecord TypeFn [nbound variances bbnds scope]
  297
+  "A type function containing n bound variables with variances.
  298
+  It is of a higher kind"
  299
+  [(nat? nbound)
  300
+   (every? variance? variances)
  301
+   (every? Bounds? bbnds)
  302
+   (apply = nbound (map count [variances bbnds]))
  303
+   (scope-depth? scope nbound)
  304
+   (Scope? scope)])
  305
+
  306
+(declare-type TypeFn)
  307
+
  308
+(defn tfn-bound [tfn]
  309
+  (->Bounds nil nil tfn))
  310
+
  311
+(declare visit-bounds)
  312
+
  313
+;smart constructor
  314
+(defn TypeFn* [names variances bbnds body]
  315
+  {:pre [(every? symbol names)
  316
+         (every? variance? variances)
  317
+         (every? Bounds? bbnds)
  318
+         (apply = (map count [names variances bbnds]))
  319
+         ((some-fn TypeFn? Type?) body)]}
  320
+  (if (empty? names)
  321
+    body
  322
+    (->TypeFn (count names) 
  323
+              variances
  324
+              (vec
  325
+                (for [bnd bbnds]
  326
+                  (visit-bounds bnd #(abstract-many names %))))
  327
+              (abstract-many names body))))
  328
+
  329
+;smart destructor
  330
+(defn TypeFn-body* [names typefn]
  331
+  {:pre [(every? symbol? names)
  332
+         (TypeFn? typefn)]}
  333
+  (assert (= (.nbound typefn) (count names)) "Wrong number of names")
  334
+  (instantiate-many names (.scope typefn)))
  335
+
  336
+(defn TypeFn-bbnds* [names typefn]
  337
+  {:pre [(every? symbol? names)
  338
+         (TypeFn? typefn)]
  339
+   :post [(every? Bounds? %)]}
  340
+  (assert (= (.nbound typefn) (count names)) "Wrong number of names")
  341
+  (mapv (fn [b]
  342
+          (visit-bounds b #(instantiate-many names %)))
  343
+        (.bbnds typefn)))
  344
+
  345
+(defrecord Poly [nbound bbnds scope actual-frees]
  346
+  "A polymorphic type containing n bound variables, with display names actual-frees"
  347
+  [(nat? nbound)
  348
+   (every? Bounds? bbnds)
  349
+   (every? symbol? actual-frees)
  350
+   (apply = nbound (map count [bbnds actual-frees]))
  351
+   (scope-depth? scope nbound)
  352
+   (Scope? scope)])
  353
+
  354
+(declare-type Poly)
  355
+
  356
+;smart constructor
  357
+(defn Poly* [names bbnds body free-names]
  358
+  {:pre [(every? symbol names)
  359
+         (every? Bounds? bbnds)
  360
+         (Type? body)
  361
+         (every? symbol? free-names)
  362
+         (apply = (map count [names bbnds free-names]))]}
  363
+  (if (empty? names)
  364
+    body
  365
+    (->Poly (count names) 
  366
+            (vec
  367
+              (for [bnd bbnds]
  368
+                (visit-bounds bnd #(abstract-many names %))))
  369
+            (abstract-many names body)
  370
+            free-names)))
  371
+
  372
+(defn Poly-free-names* [poly]
  373
+  {:pre [(Poly? poly)]
  374
+   :post [((every-pred seq (every-c? symbol?)) %)]}
  375
+  (.actual-frees poly))
  376
+
  377
+;smart destructor
  378
+(defn Poly-body* [names poly]
  379
+  {:pre [(every? symbol? names)
  380
+         (Poly? poly)]}
  381
+  (assert (= (.nbound poly) (count names)) "Wrong number of names")
  382
+  (instantiate-many names (.scope poly)))
  383
+
  384
+(defn Poly-bbnds* [names poly]
  385
+  {:pre [(every? symbol? names)
  386
+         (Poly? poly)]}
  387
+  (assert (= (.nbound poly) (count names)) "Wrong number of names")
  388
+  (mapv (fn [b]
  389
+          (visit-bounds b #(instantiate-many names %)))
  390
+        (.bbnds poly)))
  391
+
  392
+(defrecord PolyDots [nbound bbnds scope]
  393
+  "A polymorphic type containing n-1 bound variables and 1 ... variable"
  394
+  [(nat? nbound)
  395
+   (every? Bounds? bbnds)
  396
+   (= nbound (count bbnds))
  397
+   (scope-depth? scope nbound)
  398
+   (Scope? scope)])
  399
+
  400
+(declare-type PolyDots)
  401
+
  402
+;smart constructor
  403
+(defn PolyDots* [names bbnds body]
  404
+  {:pre [(every? symbol names)
  405
+         (every? Bounds? bbnds)
  406
+         (Type? body)]}
  407
+  (assert (= (count names) (count bbnds)) "Wrong number of names")
  408
+  (if (empty? names)
  409
+    body
  410
+    (->PolyDots (count names) 
  411
+                (vec
  412
+                  (for [bnd bbnds]
  413
+                    (-> bnd
  414
+                      (update-in [:upper-bound] #(abstract-many names %))
  415
+                      (update-in [:lower-bound] #(abstract-many names %)))))
  416
+                (abstract-many names body))))