Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 78d09859ce
Fetching contributors…

Cannot retrieve contributors at this time

file 242 lines (220 sloc) 9.561 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
(in-ns 'clojure.core.typed)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Variable rep

(defn add-scopes [n t]
  "Wrap type in n Scopes"
  {:pre [(nat? n)
         (Type? t)]}
  (doall
    (last
      (take (inc n) (iterate ->Scope t)))))

(defn remove-scopes
  "Unwrap n Scopes"
  [n sc]
  {:pre [(nat? n)
         (or (zero? n)
             (Scope? sc))]
   :post [(or (Scope? %) (Type? %))]}
  (doall
    (last
      (take (inc n) (iterate (fn [t]
                               (assert (Scope? t) "Tried to remove too many Scopes")
                               (:body t))
                             sc)))))

(defn- rev-indexed
  "'(a b c) -> '([2 a] [1 b] [0 c])"
  [c]
  (map vector (iterate dec (dec (count c))) c))

(derive ::abstract-many fold-rhs-default)

(add-fold-case ::abstract-many
               F
               (fn [{name* :name :as t} {{:keys [name count outer sb]} :locals}]
                 (if (= name name*)
                   (->B (+ count outer))
                   t)))

(add-fold-case ::abstract-many
               Function
               (fn [{:keys [dom rng rest drest kws]} {{:keys [name count outer sb]} :locals}]
                 (assert (not kws))
                 (->Function (map sb dom)
                             (sb rng)
                             (when rest (sb rest))
                             (when drest
                               (->DottedPretype (sb (:pre-type drest))
                                                (if (= (:name drest) name)
                                                  (+ count outer)
                                                  (:name drest))))
                             nil)))

(add-fold-case ::abstract-many
               Mu
               (fn [{:keys [scope]} {{:keys [name count type outer name-to]} :locals}]
                 (let [body (remove-scopes 1 scope)]
                   (->Mu (->Scope (name-to name count type (inc outer) body))))))

(add-fold-case ::abstract-many
               PolyDots
               (fn [{bbnds* :bbnds n :nbound body* :scope} {{:keys [name count type outer name-to]} :locals}]
                 (let [rs #(remove-scopes n %)
                       body (rs body*)
                       bbnds (mapv #(visit-bounds % rs) bbnds*)
                       as #(add-scopes n (name-to name count type (+ n outer) %))]
                   (->PolyDots n
                               (mapv #(visit-bounds % rs) bbnds)
                               (as body)))))

(add-fold-case ::abstract-many
               Poly
               (fn [{bbnds* :bbnds n :nbound body* :scope :as poly} {{:keys [name count type outer name-to]} :locals}]
                 (let [rs #(remove-scopes n %)
                       body (rs body*)
                       bbnds (mapv #(visit-bounds % rs) bbnds*)
                       as #(add-scopes n (name-to name count type (+ n outer) %))]
                   (->Poly n
                           (mapv #(visit-bounds % as) bbnds)
                           (as body)
                           (Poly-free-names* poly)))))

(add-fold-case ::abstract-many
               TypeFn
               (fn [{bbnds* :bbnds n :nbound body* :scope :keys [variances]} {{:keys [name count type outer name-to]} :locals}]
                 (let [rs #(remove-scopes n %)
                       body (rs body*)
                       bbnds (mapv #(visit-bounds % rs) bbnds*)
                       as #(add-scopes n (name-to name count type (+ n outer) %))]
                   (->TypeFn n
                             variances
                             (mapv #(visit-bounds % as) bbnds)
                             (as body)))))

(defn abstract-many
  "Names Type -> Scope^n where n is (count names)"
  [names ty]
  {:pre [(every? symbol? names)
         ((some-fn Type? TypeFn?) ty)]}
  (letfn [(name-to
            ([name count type] (name-to name count type 0 type))
            ([name count type outer ty]
             (letfn [(sb [t] (name-to name count type outer t))]
               (fold-rhs ::abstract-many
                 {:type-rec sb
                  :filter-rec (sub-f sb ::abstract-many)
                  :object-rec (sub-o sb ::abstract-many)
                  :locals {:name name
                           :count count
                           :outer outer
                           :sb sb
                           :name-to name-to}}
                 ty))))]
    (if (empty? names)
      ty
      (let [n (count names)]
        (loop [ty ty
               names names
               count (dec n)]
          (if (zero? count)
            (add-scopes n (name-to (first names) 0 ty))
            (recur (name-to (first names) count ty)
                   (next names)
                   (dec count))))))))

(derive ::instantiate-many fold-rhs-default)

(add-fold-case ::instantiate-many
               B
               (fn [{:keys [idx] :as t} {{:keys [count outer image sb]} :locals}]
                 (if (= (+ count outer) idx)
                   (->F image)
                   t)))

(add-fold-case ::instantiate-many
               Function
               (fn [{:keys [dom rng rest drest kws]} {{:keys [count outer image sb]} :locals}]
                 (assert (not kws))
                 (->Function (map sb dom)
                             (sb rng)
                             (when rest
                               (sb rest))
                             (when drest
                               (->DottedPretype (sb (:pre-type drest))
                                                (let [{:keys [name]} drest]
                                                  (assert (nat? name))
                                                  (if (= (+ count outer) name)
                                                    image
                                                    name))))
                             nil)))

(add-fold-case ::instantiate-many
               Mu
               (fn [{:keys [scope]} {{:keys [replace count outer image sb type]} :locals}]
                 (let [body (remove-scopes 1 scope)]
                   (->Mu (->Scope (replace image count type (inc outer) body))))))

(add-fold-case ::instantiate-many
               PolyDots
               (fn [{bbnds* :bbnds n :nbound body* :scope} {{:keys [replace count outer image sb type]} :locals}]
                 (let [rs #(remove-scopes n %)
                       body (rs body*)
                       bbnds (mapv #(visit-bounds % rs) bbnds*)
                       as #(add-scopes n (replace image count type (+ n outer) %))]
                   (->PolyDots n
                               (mapv #(visit-bounds % as) bbnds)
                               (as body)))))

(add-fold-case ::instantiate-many
               Poly
               (fn [{bbnds* :bbnds n :nbound body* :scope :as poly} {{:keys [replace count outer image sb type]} :locals}]
                 (let [rs #(remove-scopes n %)
                       body (rs body*)
                       bbnds (mapv #(visit-bounds % rs) bbnds*)
                       as #(add-scopes n (replace image count type (+ n outer) %))]
                   (->Poly n
                           (mapv #(visit-bounds % as) bbnds)
                           (as body)
                           (Poly-free-names* poly)))))

(add-fold-case ::instantiate-many
               TypeFn
               (fn [{bbnds* :bbnds n :nbound body* :scope :keys [variances]} {{:keys [replace count outer image sb type]} :locals}]
                 (let [rs #(remove-scopes n %)
                       body (rs body*)
                       bbnds (mapv #(visit-bounds % rs) bbnds*)
                       as #(add-scopes n (replace image count type (+ n outer) %))]
                   (->TypeFn n
                             variances
                             (mapv #(visit-bounds % as) bbnds)
                             (as body)))))

(defn instantiate-many
  "instantiate-many : List[Symbols] Scope^n -> Type
Instantiate de Bruijn indices in sc to frees named by
images, preserving upper/lower bounds"
  [images sc]
  {:pre [(every? symbol? images)
         (or (Scope? sc)
             (empty? images))]
   :post [((some-fn Type? TypeFn?) %)]}
  (letfn [(replace
            ([image count type] (replace image count type 0 type))
            ([image count type outer ty]
             (letfn [(sb [t] (replace image count type outer t))]
               (let [sf (sub-f sb ::instantiate-many)]
                 (fold-rhs ::instantiate-many
                   {:type-rec sb
                    :filter-rec sf
                    :object-rec (sub-o sb ::instantiate-many)
                    :locals {:count count
                             :outer outer
                             :image image
                             :sb sb
                             :type type
                             :replace replace}}
                   ty)))))]
    (if (empty? images)
      sc
      (let [n (count images)]
        (loop [ty (remove-scopes n sc)
               images images
               count (dec n)]
          (if (zero? count)
            (replace (first images) 0 ty)
            (recur (replace (first images) count ty)
                   (next images)
                   (dec count))))))))

(defn abstract [name ty]
  "Make free name bound"
  {:pre [(symbol? name)
         (Type? ty)]}
  (abstract-many [name] ty))

(defn instantiate [f sc]
  "Instantiate bound name to free"
  {:pre [(symbol? f)
         (Scope? sc)]}
  (instantiate-many [f] sc))
Something went wrong with that request. Please try again.