Carp/lisp/infer_types.carp

412 lines
19 KiB
Plaintext

;; The type env is bindings from variable names to types or variables, i.e. {:x :int, :y "t10"}
(defn type-env-extend (type-env args)
(let [new-env (copy type-env)]
(do (reduce (fn (_ pair) (dict-set! new-env (nth pair 0) (nth pair 1)))
nil
(map2 list (map :name args) (map :type args)))
new-env)))
(defn is-self-recursive? (type-env app-f-name)
(let [x (get-maybe type-env app-f-name)]
(do
;;(println (str "app-f: " app-f-name ", x: " x))
(= x :self))))
(defn get-type-of-symbol (type-env symbol)
(let [lookup (get-maybe type-env symbol)]
(if (nil? lookup)
(let [global-lookup (eval symbol)
t (type global-lookup)]
(match t
:lambda (if (meta-get global-lookup :generic)
(let [signature (meta-get global-lookup :signature)]
(do ;;(println (str "'" symbol "' is generic with signature "))
signature))
(error (str "Found non-baked symbol '" symbol "'.")))
:macro (error (str "Found non-expanded macro '" symbol "'."))
:foreign (signature global-lookup)
:primop (let [s (signature global-lookup)]
(if (nil? s)
(error (str "No signature set for primop " symbol " (maybe it isn't allowed to be baked?)"))
s))
_ t))
lookup)))
(defn math-op? (op)
(contains? '(+ - * /) op))
(def log-chaining false)
(defn generate-constraints-internal (constraints ast type-env)
(do
;;(println "gen constrs: \n" ast)
(match (get ast :node)
:function (let [extended-type-env (type-env-extend type-env (get ast :args))
extended-type-env-2 (let [fn-name (get-maybe ast :name)]
(if (string? fn-name)
(assoc extended-type-env fn-name :self)
extended-type-env))
new-constraints (generate-constraints-internal constraints (:body ast) extended-type-env-2)
func-ret-constr {:a (get-in ast '(:type 2)) ;; the return type of the fn type
:b (get-in ast '(:body :type))
:doc (str "func-ret-constr")}
func-arg-constrs (map2 (fn (a b) {:a a :b b :doc "func-arg"})
(map :type (:args ast))
(get-in ast '(:type 1)))]
(concat func-arg-constrs (cons func-ret-constr new-constraints)))
:app (let [ret-constr {:a (get ast :type) :b (get-in ast '(:head :type 2)) :doc "ret-constr for :app"}
arg-constrs (map2 (fn (a b) {:a a :b b :doc "app-arg"}) (get-in ast '(:head :type 1)) (map :type (:tail ast)))
head-constrs (generate-constraints-internal '() (:head ast) type-env)
tail-constrs (reduce (fn (constrs tail-form) (generate-constraints-internal constrs tail-form type-env))
'() (:tail ast))
new-constraints (concat tail-constrs head-constrs (cons ret-constr arg-constrs))]
(concat new-constraints constraints))
:literal constraints ;; literals don't need constraints
:ref (let [expr (:expr ast)
x0 (generate-constraints-internal constraints expr type-env)
inner-type (match (:type ast)
(:ref t) t
_ (error "Not a ref type"))
expr-constr {:a inner-type :b (:type expr) :doc "ref-constr"}]
(cons expr-constr x0))
:reset (let [expr (:expr ast)
symbol (:symbol ast)
x0 (generate-constraints-internal constraints expr type-env)
t (get-type-of-symbol type-env symbol)
expr-constr {:a t
:b (:type expr)
:doc "reset!-constr"}]
(cons expr-constr x0))
:lookup (if (has-key? ast :self-recursive)
constraints
(if (has-key? ast :constructor)
(let [member-types (array-to-list (:member-types ast))
t (:type ast)
constructor-return-constr {:a (keyword (:struct-name ast)) :b (nth t 2) :doc "constructor-return-value"}
constructor-arg-constrs (map2 (fn [a b] {:a a :b b :doc "constructor-arg"})
member-types
(nth t 1))]
(cons constructor-return-constr constructor-arg-constrs))
(let [val (:value ast)
;;_ (println (str "not self-recursive: \n" ast))
t (get-type-of-symbol type-env val)
;;_ (println (str "type of lookup '" val "': " t))
]
(if (nil? t)
(error (str "Can't create constraint for lookup of '" val "', it's type is nil."))
(cons {:a (:type ast)
:b t
:doc (str "lookup " val)} constraints)))))
:binop (let [x0 (generate-constraints-internal constraints (get ast :left) type-env)
x1 (generate-constraints-internal x0 (get ast :right) type-env)
;;tvar (gen-typevar)
;;left-arg-constr {:a tvar :b (get-in ast '(:a :type)) :doc "left-arg-constr"}
;;right-arg-constr {:a tvar :b (get-in ast '(:b :type)) :doc "right-arg-constr"}
;;ret-constr {:a tvar :b (:type ast)}
same-arg-type-constr {:a (get-in ast '(:left :type)) :b (get-in ast '(:right :type)) :doc "same-arg-type-constr"}
maybe-constr (if (math-op? (:op ast))
(list {:a (get-in ast '(:left :type)) :b (:type ast)})
())
]
;;(concat x1 (list left-arg-constr right-arg-constr ret-constr)))
(concat maybe-constr (cons same-arg-type-constr x1)))
:if (let [x0 (generate-constraints-internal constraints (get ast :if-true) type-env)
x1 (generate-constraints-internal x0 (get ast :if-false) type-env)
x2 (generate-constraints-internal x1 (get ast :expr) type-env)
left-result-constr {:a (get-in ast '(:if-true :type)) :b (:type ast)}
right-result-constr {:a (get-in ast '(:if-false :type)) :b (:type ast)}
expr-must-be-bool {:a :bool :b (get-in ast '(:expr :type))}]
(concat x2 (list
expr-must-be-bool
left-result-constr
right-result-constr)))
:do (let [x0 (reduce (fn (constrs form) (generate-constraints-internal constrs form type-env))
constraints (:forms ast))
;;_ (log "count: " (count x0))
n (count (:forms ast))
_ (when (= 0 n) (error (str "do-form must have at least one statement.")))
ret-constr {:a (:type ast) :b (get-in ast (list :forms (- n 1) :type)) :doc "do-ret-constr"}]
(cons ret-constr x0))
:let (let [bindings (:bindings ast)
extended-type-env (reduce (fn (e b) (assoc e (:name b) (get-in b '(:value :type)))) type-env bindings)
;;_ (println "Extended type env: " extended-type-env)
let-constr {:a (:type ast) :b (get-in ast '(:body :type)) :doc "let-constr"}
bindings-constr (mapcat (fn (binding) (let [bind-constr {:a (:type binding) :b (get-in binding '(:value :type))}
value-constrs (generate-constraints-internal constraints (:value binding) extended-type-env)]
(cons bind-constr value-constrs)))
bindings)
body-constrs (generate-constraints-internal constraints (:body ast) extended-type-env)]
(cons let-constr (concat bindings-constr body-constrs)))
:while (let [x0 (generate-constraints-internal constraints (get ast :body) type-env)
x1 (generate-constraints-internal x0 (get ast :expr) type-env)
body-result-constr {:a (get-in ast '(:body :type)) :b (:type ast)}
expr-must-be-bool {:a :bool :b (get-in ast '(:expr :type))}]
(concat x1 (list expr-must-be-bool )))
:null constraints
_ constraints
)))
;; This function will generate a list with two kinds of constraints: type-constraints and func-deps
;;
;; 1. Type constraints have three keys called :a, :b & :doc.
;; The a and b keys hold types that should get unified.
;; The doc key is just a string telling you in what form the constraint was generated.
;;
;; 2. Func deps only have one key (:func-dep) and it holds the symbol
;; refering to a particular function that this function is dependant on
;; It could be better to generate the func deps in a separate step before generating
;; the constraints, keeping things more separated, but this works too.
(defn generate-constraints (ast)
(let [constraints '()]
(generate-constraints-internal constraints ast {})))
;; A shorter name:
(def gencon generate-constraints)
(defn lookup (substs b)
(if (list? b)
(map (fn [x] (lookup substs x)) b)
(let [val (get-maybe substs b)]
(if (= () val)
b
(if (= b val)
val
(if (= :string (type val))
(lookup substs val) ; keep looking
val))) ; found the actual type
)))
;; Replacement function for replacing "from the right" in an associative map
;; Example usage:
;; (replace-subst-from-right {:a :b, :c :d} :d :e)
;; =>
;; {:c :e,
;; :a :b}
(defn replace-in-list (l replace-this with-this)
(do
;;(println (str "replace-in-list " l ", replace: " replace-this ", with: " with-this))
(match l
() ()
(x & xs) (if (= x replace-this)
(cons with-this (replace-in-list xs replace-this with-this))
(if (list? x)
(cons (replace-in-list x replace-this with-this) (replace-in-list xs replace-this with-this))
(cons x (replace-in-list xs replace-this with-this)))))))
(defn maybe-replace-binding (key value replace-this with-this)
(do
;;(println (str "maybe-replace-binding key: " key ", value: " value ", replace: " replace-this ", with: " with-this))
(if (list? value)
{:key key :value (replace-in-list value replace-this with-this)}
(if (= replace-this value)
{:key key :value with-this}
{:key key :value value}))))
(defn replace-subst-from-right (substs existing b)
(do
;;(println (str "replace-substs-from-right " substs existing b))
(reduce (fn (new-substs pair) (assoc new-substs (:key pair) (:value pair)))
{}
(map2 (fn (k v)
(maybe-replace-binding k v existing b))
(keys substs)
(values substs)))))
(defn typevar? (x) (string? x))
(defn types-exactly-eq? (a b)
(if (and (list? a) (list? b))
(all? true? (map2 types-exactly-eq? a b))
(if (= :any a)
true
(if (= :any b)
true
(= a b)))))
(def log-substs false)
(defn extend-substitutions (substs lhs value)
(do
(when log-substs (do
(println (str "\nSubsts:\n" substs))
(println (str "Try extend " lhs " => " value))))
(let [value-lookup (lookup substs value)]
(if (typevar? lhs)
(let [existing (get-maybe substs lhs)]
(if (= nil existing)
(let [new-substs (assoc substs lhs value-lookup)
;;_ (println (str "new-substs:\n" new-substs))
substs-replaced-from-right (replace-subst-from-right new-substs lhs value-lookup)
;;_ (println (str "substs-replaced-from-right:\n" substs-replaced-from-right))
]
(do (when log-substs (println (str "No existing binding, set " lhs " to " value-lookup
", substs-replaced-from-right:\n" substs-replaced-from-right)))
substs-replaced-from-right))
(do (when log-substs (println (str "Existing binding: " existing)))
(if (list? existing)
(if (list? value-lookup)
(let [_ (when log-substs (println "The existing binding is a list"))
new-substs (reduce (fn (s m2) (extend-substitutions substs (:e m2) (:l m2)))
substs
(map2 (fn (e l) {:e e :l l}) existing value-lookup))
_ (when log-substs (println (str "\nBack from list, new substs: " new-substs)))]
new-substs)
(do
substs))
(if (typevar? existing)
(do (when log-substs (println "The existing binding is a typevar, will replace from right"))
(replace-subst-from-right substs existing value-lookup))
(do (when log-substs (println "The existing binding is not a typevar"))
(if (types-exactly-eq? existing value-lookup)
(do (when log-substs (println "Current binding matches new value"))
substs)
(do (when log-substs (println "Current binding do not match new value"))
(if (or (= :any lhs) (typevar? value-lookup))
substs
(error (str "Can't unify typevar \n" existing " with \n" value-lookup)))))))))))
;; Not a typevar:
(if (list? lhs)
(let [value-lookup (lookup substs value)]
(if (list? value-lookup)
(do
;;(println (str "Both lhs and value-lookup are lists: " lhs ", " value-lookup))
(reduce (fn (s m2) (let [s1 (extend-substitutions s (:t m2) (:v m2))]
(extend-substitutions s1 (:v m2) (:t m2))))
substs (map2 (fn (t v) {:t t :v v}) lhs value-lookup)))
(do
;;(println (str "value lookup must be a list when lhs is a list: " lhs))
substs)))
(do (when log-substs (println (str "lhs " lhs " is not a tvar or list.")))
(if (or (= :any lhs) (= :any value-lookup) (= lhs value-lookup) (typevar? value-lookup))
substs
(error (str "Can't unify \n" lhs " with \n" value-lookup)))))))))
(defn solve-list (substs a-list b-list)
(match (list a-list b-list)
(() ()) substs
((a & as) (b & bs)) (solve (solve substs a b) as bs)
_ (error (str "Lists not matching: " a-list " - vs - " b-list ", substs: \n" substs))))
(defn solve (substs a b)
(if (and (list? a) (list? b))
(solve-list substs a b)
(extend-substitutions substs a b)))
(defn solve-contraint-internal (substs constraint)
(let [a (:a constraint)
b (:b constraint)]
(solve (solve substs a b) b a))) ; Solving from both directions!
;; Returns a substitution map from type variables to actual types
(defn solve-constraints (constraints)
(reduce solve-contraint-internal {} constraints))
(defn make-type-list (substs typevars)
(map (fn (t) (if (string? t) (get-type substs t)
(if (list? t)
(make-type-list substs t)
t)))
typevars))
(defn get-type (substs typevar)
(if (list? typevar)
(make-type-list substs typevar)
(let [maybe-type (get-maybe substs typevar)]
(if (= maybe-type ())
typevar ;; lookup failed, there is no substitution for this type variable (= it's generic)
maybe-type))))
(defn assign-types-to-list (asts substs)
(map (fn (x) (assign-types x substs)) asts))
(defn assign-types-to-binding (b substs)
(let [x0 (assoc b :type (get-type substs (:type b)))
x1 (assoc x0 :value (assign-types (:value b) substs))]
x1))
(defn assign-types (ast substs)
(match (:node ast)
:function (let [a (assoc ast :type (get-type substs (:type ast)))
b (assoc a :body (assign-types (:body ast) substs))
c (assoc b :args (assign-types-to-list (:args ast) substs))]
c)
:app (let [app-ret-type (get-type substs (:type ast))]
(assoc (assoc (assoc ast :type app-ret-type)
:head (assign-types (:head ast) substs))
:tail (map (fn (x) (assign-types x substs)) (:tail ast))))
:literal ast
:lookup (assoc ast :type (get-type substs (:type ast)))
:arg (assoc ast :type (get-type substs (:type ast)))
:ref (let [x0 (assoc ast :type (get-type substs (:type ast)))
x1 (assoc x0 :expr (assign-types (:expr x0) substs))]
x1)
:reset (let [x0 (assoc ast :expr (assign-types (:expr ast) substs))]
x0)
:binop (let [x0 (assoc ast :type (get-type substs (:type ast)))
x1 (assoc x0 :left (assign-types (:left ast) substs))
x2 (assoc x1 :right (assign-types (:right ast) substs))]
x2)
:if (let [x0 (assoc ast :type (get-type substs (:type ast)))
x1 (assoc x0 :if-true (assign-types (:if-true ast) substs))
x2 (assoc x1 :if-false (assign-types (:if-false ast) substs))
x3 (assoc x2 :expr (assign-types (:expr ast) substs))]
x3)
:do (let [x0 (assoc ast :forms (map (fn (x) (assign-types x substs)) (:forms ast)))
x1 (assoc x0 :type (get-type substs (:type ast)))]
x1)
:let (let [x0 (assoc ast :bindings (map (fn (b) (assign-types-to-binding b substs)) (:bindings ast)))
x1 (assoc x0 :body (assign-types (:body x0) substs))
x2 (assoc x1 :type (get-type substs (:type ast)))]
x2)
:while (let [x0 (assoc ast :type (get-type substs (:type ast)))
x1 (assoc x0 :body (assign-types (:body ast) substs))
x2 (assoc x1 :expr (assign-types (:expr ast) substs))]
x2)
:null ast
:c-code (assoc ast :type (get-type substs (:type ast)))
_ (error (str "Can't assign types to ast node " ast))))
;; x1 (assoc-in x0 '(:body :type) (get-type substs (get-in x0 '(:body :type))))
(defn func-dep? (constraint) (has-key? constraint :func-dep))
(defn infer-types (ast func-signature-if-generic)
(let [type-constraints (generate-constraints ast)
func-signature-constraint (if (nil? func-signature-if-generic) '() (list {:a func-signature-if-generic :b (:type ast) :doc "generic-constr"}))
substs (solve-constraints (concat func-signature-constraint type-constraints))
ast-typed (assign-types ast substs)]
ast-typed))