Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

maps -> records

  • Loading branch information...
commit 9f1a521575e18e3f3191b687461d4bdea15b4b11 1 parent 8e1e41c
@frenchy64 authored
Showing with 132 additions and 55 deletions.
  1. +2 −1  project.clj
  2. +130 −54 src/typed/new.clj
View
3  project.clj
@@ -1,5 +1,6 @@
(defproject typed "0.1-alpha3-SNAPSHOT"
:description "Optional static type system"
:dependencies [[org.clojure/clojure "1.4.0"]
- [analyze "0.1.7-SNAPSHOT"]]
+ [analyze "0.1.7-SNAPSHOT"]
+ [trammel "0.7.0"]]
:dev-dependencies [[org.clojure/tools.trace "0.7.3"]])
View
184 src/typed/new.clj
@@ -1,74 +1,126 @@
(ns typed.new
+ (:refer-clojure :exclude [defrecord])
(:require [analyze.core :as analyze]
+ [clojure.set :as set]
+ [trammel.core :as contracts]
[clojure.tools.trace :refer [trace trace-ns]]))
+(defmacro defrecord [name slots inv-description invariants & etc]
+ `(contracts/defconstrainedrecord ~name ~slots ~inv-description ~invariants ~@etc))
+
(declare abstract-many)
+(defn- comp-mm [mm disps]
+ (set/difference disps (set (keys (.getMethodTable mm)))))
+
+;(comp-mm replace-image (disj kinds :scope))
+;(comp-mm replace-image (disj kinds :scope))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Types
+
(def nat? (every-pred (complement neg?) integer?))
-(def kinds #{:b :f :rclass :poly :scope})
-(defn kind-inst? [k]
- (boolean (kinds (:kind k))))
+(def kinds #{:B :F :RClass :Poly :Mu :Union :intersection
+ :Top})
-(defn B [i]
- {:pre [(nat? i)]}
- {:kind :b
- :idx i})
+(def Type ::Type)
-(defn F [name]
- {:pre [(symbol? name)]}
- {:kind :f
- :name name})
+(defn Type? [a]
+ (isa? a Type))
-(defn F? [a]
- (= (:kind a) :f))
+(defn declare-type [a]
+ (derive a Type))
-(defn RClass [the-class replacements]
- {:pre [(class? the-class)
- (every? class? (keys replacements))
- (every? kind-inst? (vals replacements))]}
+(defrecord Top []
+ "The top type"
+ [])
- {:kind :rclass
- :the-class the-class
- :replacements replacements})
+(declare-type Top)
-(declare Scope?)
+(defrecord Union [types]
+ "An unordered union of types"
+ [(every? Type? types)])
-(defn make-Poly [n scope]
- {:pre [(nat? n)
- (Scope? scope)]}
- {:kind :poly
- :nbound n
- :scope scope})
+(declare-type Union)
+
+(defn Bottom []
+ (->Union []))
+
+(defrecord Intersection [types]
+ "An ordered intersection of types"
+ [(sequential? types)
+ (every? Type? types)])
+
+(declare-type Intersection)
+
+(defrecord B [idx]
+ "A bound variable. Should not appear outside this file"
+ [(nat? idx)])
+
+(declare-type B)
+
+(defrecord F [name]
+ "A named free variable"
+ [(symbol? name)])
+
+(declare-type F)
+
+(defrecord RClass [the-class replacements]
+ "A restricted class, where ancestors are
+ (replace replacements (ancestors the-class))"
+ [(class? the-class)
+ (every? class? (keys replacements))
+ (every? Type? (vals replacements))])
+
+(declare-type RClass)
+
+(defrecord Scope [body]
+ "A scope that contains bound variables. Not used directly"
+ [(Type? body)])
+
+(defrecord Poly [n scope]
+ "A polymorphic type containing n bound variables"
+ [(nat? n)
+ (Scope? scope)])
+
+(declare-type Poly)
;smart constructor
-(defn Poly [names body]
+(defn Poly* [names body]
{:pre [(every? symbol names)
- (kind-inst? body)]}
+ (Type? body)]}
(if (empty? names)
body
- (make-Poly (count names) (abstract-many names body))))
+ (->Poly (count names) (abstract-many names body))))
-(defn Scope [body]
- {:pre [(kind-inst? body)]}
+(defrecord Mu [scope]
+ "A recursive type containing one bound variable, itself"
+ [(Scope? scope)])
- {:kind :scope
- :body body})
+(declare-type Mu)
+
+(declare abstract)
+
+;smart constructor
+(defn Mu* [name body]
+ (->Mu (abstract name body)))
-(defn Scope? [a]
- (= (:kind a) :scope))
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Variable rep
(defn add-scopes [n t]
"Wrap type in n Scopes"
{:pre [(nat? n)
- (kind-inst? t)]}
+ (Type? t)]}
(last
(take (inc n) (iterate Scope t))))
(defn remove-scopes [n sc]
"Unwrap n Scopes"
{:pre [(nat? n)
- (kind-inst? sc)]}
+ (Type? sc)]}
(last
(take (inc n) (iterate (fn [{body :body :as t}]
(assert (Scope? t) "Tried to remove too many Scopes")
@@ -80,28 +132,28 @@
where n is the position in the current binder, and outer is the
number of indices previously bound"
(fn [ty name res]
- {:pre [(kind-inst? ty)
+ {:pre [(Type? ty)
(symbol? name)
(nat? res)]}
(:kind ty)))
-(defmethod name-to :b [ty name res] ty)
+(defmethod name-to B [ty name res] ty)
-(defmethod name-to :f
+(defmethod name-to F
[{name* :name :as ty} name res]
(if (= name name*)
- (B res)
+ (->B res)
ty))
-(defmethod name-to :rclass
+(defmethod name-to RClass
[{:keys [the-class replacements]} name res]
- (RClass the-class (into {} (for [[k v] replacements]
- [k (name-to v name res)]))))
+ (->RClass the-class (into {} (for [[k v] replacements]
+ [k (name-to v name res)]))))
-(defmethod name-to :poly
+(defmethod name-to Poly
[{n :nbound scope :scope} name res]
(let [body (remove-scopes n scope)]
- (make-Poly n (add-scopes n (name-to body name (+ n res))))))
+ (->Poly n (add-scopes n (name-to body name (+ n res))))))
(defn- rev-indexed
"'(a b c) -> '([2 a] [1 b] [0 c])"
@@ -112,7 +164,7 @@
"Names Type -> Scope^n where n is (count names)"
[names ty]
{:pre [(every? symbol? names)
- (kind-inst? ty)]}
+ (Type? ty)]}
(let [n (count names)]
(->>
;convert each given name to a bound de Bruijn index
@@ -125,20 +177,20 @@
(defmulti replace-image
(fn [type image target]
- {:pre [(kind-inst? type)
+ {:pre [(Type? type)
(F? image)
(nat? target)]}
(:kind type)))
-(defmethod replace-image :f [ty image target] ty)
+(defmethod replace-image F [ty image target] ty)
-(defmethod replace-image :b
+(defmethod replace-image B
[{idx :idx :as ty} image target]
(if (= idx target)
image
ty))
-(defmethod replace-image :poly
+(defmethod replace-image Poly
[{scope :scope n :nbound :as ty} image target]
(let [body (remove-scopes n scope)]
(assoc ty :scope (add-scopes n (replace-image body image (+ target n))))))
@@ -159,7 +211,7 @@
(defn abstract [name ty]
"Make free name bound"
{:pre [(symbol? name)
- (kind-inst? ty)]}
+ (Type? ty)]}
(abstract-many [name] ty))
(defn instantiate [f sc]
@@ -168,7 +220,31 @@
(Scope? sc)]}
(instantiate-many [f] sc))
-(defmulti subtype (fn [A s t] [(:kind s) (:kind t)]))
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Subtypes
+
+(def ^:dynamic *A*)
+(def ^:dynamic *A0*)
+
+(defmulti subtype* (fn [s t] [(:kind s) (:kind t)]))
+
+(defn subtypeA* [A s t]
+ (cond
+ (or (contains? A [s t])
+ (= s t))
+ A
+
+ :else
+ (binding [*A* A
+ *A0* (conj A [s t])]
+ (subtype* s t))))
+
+(defn subtype [s t]
+ (subtypeA* #{} s t))
+
+(defmethod subtype* [Type Top]
+ [s t]
+ )
(defmulti check :op)
Please sign in to comment.
Something went wrong with that request. Please try again.