Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

solveA

  • Loading branch information...
commit a6709452ec8a94519b1fff78836c44d4e1853f09 1 parent 90cbe15
@samth authored
Showing with 23 additions and 7 deletions.
  1. +23 −7 constraints.rkt
View
30 constraints.rkt
@@ -161,11 +161,27 @@
;; solving constraints
-
-
-
-
-
-
-
+;; constraints on signatures
+(define-metafunction js
+ solveA : (:= α hσ) -> (:= α hσ) or bot
+ [(solveA (:= α ((γ ... (γ_1 ... (: x σ))) x)))
+ (:= α σ)]
+ [(solveA (:= α ((γ ... (((: x σ) *))) x)))
+ (:= α σ)]
+ [(solveA (:= α ((γ ... (γ_1 ... ((: x σ_1) *) ((: x σ) *))) x)))
+ bot] ;; could allow this
+ [(solveA (:= α ((γ ... (γ_1 ... (: x_1 σ))) x)))
+ (:= α ((γ ... (γ_1 ...)) x))
+ (side-condition (not (equal? (term x) (term x_1))))]
+ [(solveA (:= α ((γ ... (γ_1 ... ((: x_1 σ) *))) x)))
+ (:= α ((γ ... (γ_1 ...)) x))
+ (side-condition (not (equal? (term x) (term x_1))))]
+ [(solveA (:= α ((γ ... ()) x)))
+ (:= α ((γ ...) x))]
+ [(solveA (:= α (() x)))
+ bot]
+ [(solveA (:= α (dot (module ρ) x)))
+ (:= α ((ρ) x))]
+ [(solveA (:= α (dot V x)))
+ (:= α V)])
Please sign in to comment.
Something went wrong with that request. Please try again.