|
| 1 | + |
| 2 | + signature module SubstitutionSig2 { |
| 3 | + class TypeAbstraction { |
| 4 | + predicate typeVariable(TypeParameter tp); |
| 5 | + |
| 6 | + /** Gets a textual representation of this type abstraction. */ |
| 7 | + string toString(); |
| 8 | + |
| 9 | + /** Gets the location of this type mention. */ |
| 10 | + Location getLocation(); |
| 11 | + } |
| 12 | + |
| 13 | + class TypeApplication { |
| 14 | + TypeAbstraction getTarget(); |
| 15 | + |
| 16 | + Type getType(TypeParameter tp, TypePath path); |
| 17 | + |
| 18 | + /** Gets a textual representation of this type application. */ |
| 19 | + string toString(); |
| 20 | + |
| 21 | + /** Gets the location of this type application. */ |
| 22 | + Location getLocation(); |
| 23 | + } |
| 24 | + |
| 25 | + class TypeUnderAbstraction { |
| 26 | + TypeAbstraction getAbstraction(); |
| 27 | + |
| 28 | + Type getType(TypePath path); |
| 29 | + |
| 30 | + /** Gets a textual representation of this type under abstraction. */ |
| 31 | + string toString(); |
| 32 | + |
| 33 | + /** Gets the location of this type mention. */ |
| 34 | + Location getLocation(); |
| 35 | + } |
| 36 | + } |
| 37 | + |
| 38 | + module Substitution2<SubstitutionSig2 Input> { |
| 39 | + private import Input |
| 40 | + |
| 41 | + Type substitution( |
| 42 | + TypeAbstraction abs, TypeApplication app, TypeUnderAbstraction subj, TypePath path |
| 43 | + ) { |
| 44 | + app.getTarget() = abs and |
| 45 | + subj.getAbstraction() = abs and |
| 46 | + ( |
| 47 | + result = subj.getType(path) and not abs.typeVariable(result) |
| 48 | + or |
| 49 | + exists(TypePath prefix, TypePath suffix, TypeParameter tp | |
| 50 | + path = prefix.append(suffix) and |
| 51 | + tp = subj.getType(prefix) and |
| 52 | + abs.typeVariable(tp) and |
| 53 | + result = app.getType(tp, suffix) |
| 54 | + ) |
| 55 | + ) |
| 56 | + } |
| 57 | + } |
| 58 | + |
| 59 | + |
| 60 | + signature module SubstitutionSig { |
| 61 | + predicate substitution(TypeParameter tp, TypePath path, Type t); |
| 62 | + |
| 63 | + Type subject(TypePath path); |
| 64 | + |
| 65 | + default predicate freeVariable(TypeParameter tp) { substitution(tp, _, _) } |
| 66 | + } |
| 67 | + |
| 68 | + module Substitution<SubstitutionSig Input> { |
| 69 | + private import Input |
| 70 | + |
| 71 | + Type substituted(TypePath path) { |
| 72 | + result = subject(path) and not freeVariable(result) |
| 73 | + or |
| 74 | + exists(TypePath prefix, TypePath suffix, TypeParameter tp | |
| 75 | + path = prefix.append(suffix) and |
| 76 | + tp = subject(prefix) and |
| 77 | + freeVariable(tp) and |
| 78 | + substitution(tp, suffix, result) |
| 79 | + ) |
| 80 | + } |
| 81 | + } |
| 82 | + |
| 83 | + ## Signature with type abstraction |
| 84 | + |
| 85 | + ```java |
| 86 | + signature module SubstitutionSig { |
| 87 | + class TypeAbstraction; |
| 88 | + |
| 89 | + class TypeApplication; |
| 90 | + |
| 91 | + class TypeTerm; |
| 92 | + |
| 93 | + predicate typeVariable(TypeAbstraction abs, TypeParameter tp); |
| 94 | + |
| 95 | + TypeAbstraction applicationGetTarget(TypeApplication app); |
| 96 | + |
| 97 | + Type applicationGetType(TypeApplication app, TypeParameter tp, TypePath path); |
| 98 | + |
| 99 | + TypeAbstraction termGetAbstraction(TypeTerm subj); |
| 100 | + |
| 101 | + Type termGetType(TypeTerm subj, TypePath path); |
| 102 | + } |
| 103 | + |
| 104 | + module Substitution<SubstitutionSig Input> { |
| 105 | + private import Input |
| 106 | + |
| 107 | + Type substitution(TypeAbstraction abs, TypeApplication app, TypeTerm subj, TypePath path) { |
| 108 | + abs = applicationGetTarget(app) and |
| 109 | + abs = termGetAbstraction(subj) and |
| 110 | + ( |
| 111 | + result = termGetType(subj, path) and not typeVariable(abs, result) |
| 112 | + or |
| 113 | + exists(TypePath prefix, TypePath suffix, TypeParameter tp | |
| 114 | + path = prefix.append(suffix) and |
| 115 | + tp = termGetType(subj, prefix) and |
| 116 | + typeVariable(abs, tp) and |
| 117 | + result = applicationGetType(app, tp, suffix) |
| 118 | + ) |
| 119 | + ) |
| 120 | + } |
| 121 | + } |
| 122 | + |
| 123 | + signature module SatisfiesConstraintSig<HasTypeTreeSig Term> { |
| 124 | + predicate desiredConstraint(Term term, Constraint Type); |
| 125 | + } |
| 126 | + |
| 127 | + module SatisfiesConstraint<HasTypeTreeSig Term, SatisfiesConstraintSig<Term> Input> { |
| 128 | + predicate termSatisfiesConstraintTypeAt( |
| 129 | + Term term, TypePath prefix, Type constraint, TypePath path, Type t |
| 130 | + ) { |
| 131 | + } |
| 132 | + } |
| 133 | + |
| 134 | +``` |
0 commit comments