subtyping.tr

let interleave_pairs (l: term list) =
  let rec loop (l: term list) : (term, term) tuple list =
    match l with
    | [] -> []
    | x :: y :: rest -> (x, y) :: loop(y :: rest)
    | x :: [] -> []
  in
  loop(l)
in

let seek
    (h: string)
    (key: string)
    (data: term list)
    (tag: string) =
  match assoc(key, hint(h)) with
  | none -> []
  | some(m) ->
    zip(m, data)[`(x, t)` when x = tag]: t
in

let rec extract_variance (t: term) (v: string) : term list =
  match t with
  | (c ts) ->
    let vs = seek("variance", c, ts, v) in
    vars(vs) @ concat(diff(ts, vs)[`_`]: extract_variance(self, v))
  | _ -> []
in

let filter_ts (ts: term list) =
  ts[`t` when var?(t) && var_kind?(t, "Type")]: self
in

(* modify all typing rules *)
(Rule[`_`]:
  let typ_prems = Premises[`&("typeof" _)`]: self in
  if empty?(typ_prems) then self else (
    (* uniquify all type variables in the outputs;
     * this will return a list of modified premises
     * and a map from the original types to a list of
     * their uniquified counterparts *)
    let (new_premises, tmap) =
      let ignored = Premises[`_`]:
        match self with
        | _ |- _ : _{_/x} -> some(self)
        | _ -> none
      in
      uniquify(Premises, ignored, hint("mode"), "out")
    in
    let name = rule_name(self) in

    (* replace the premises with the uniquified ones *)
    [name] {
      new_premises
      ------------------
      conclusion
    };
    
    (* grab all types in contravariant positions *)
    let contra_types = concat(Premises[`_ |- _ : t`]: extract_variance(t, "contra")) in
   
    (* grab all types in invariant positions *)
    let inv_types = concat(Premises[`p`]:
      match p with
      | gamma |- e : t -> extract_variance(t, "inv")
      | &member t _ -> filter_ts(vars(t))
      | _ -> [])
    in
    
    (* create a map from the original types (before uniquify)
     * to the "final type" that should appear in the conclusion *)
    let concl = conclusion in
    let final_type = concat(tmap[`(tk, tv)`]:
      match concl with
      | gamma |- e : t ->
        let t_types = filter_ts(vars(t)) in
        if empty?(t_types) then none else
          some(vars(e)[`v`]:
            match assoc(v, tmap) with
            | some(_) -> (tk, v)
            | none ->
               let ov = var_overlap(tv, contra_types) in
               if length(ov) = 1 then (tk, head(ov)) else (tk, tk))
      | _ -> none)
    in
   
    (* for each type we uniquified, get their uniquified
     * counterparts and interleave them in a list of pairs,
     * then use these pairs to append new subtyping premises *) 
    let tpairs = concat(tmap[`(_, ts)`]: interleave_pairs(ts)) in
    [name] {
      Premises,
      tpairs[`(t1, t2)`]: t1 <: t2
      ----------------------------
      conclusion
    };
   
    (* reorder the generated subtyping premises according
     * to their variance (i.e. did they appear in a
     * contravariant/invariant position in the premises?) *) 
    let prems = Premises in
    [name] {
      prems(keep)[`t1 <: t2`]:
        let p = self in
        let ps = prems[`gamma |- e : (c ts)`]:
          match assoc(c, hint("variance")) with
          | none -> none
          | some(variance) ->
            let vmap = zip(ts, variance) in
            match assoc(t1, vmap) with
            | some("contra") -> some(t2 <: t1)
            | some("inv") ->
              (match assoc(t2, vmap) with
               | some("inv") -> some(&(t1 = t2))
               | _ -> some(t2 <: t1))
            | _ -> none
        in if empty?(ps) then p else head(ps)
      ---------------------------------------
      conclusion
    };
    
    (* check for types that are peers, and if so, add a join for them.
     * additionally, multiple contravariant types require a meet *) 
    [name] {
      Premises,
      tmap[`(tk, tv)`]:
        match var_overlap(tv, contra_types) with
        | _ :: [] -> none
        | [] ->
          let ov = var_overlap(tv, inv_types) in
          if empty?(ov)
          then some(&("join" (tv @ [tk.])))
          else
            let final_type_range = final_type[`(_, v)`]: v in
            if member?(tk, final_type_range)
            then some(&("join" (tv @ [tk.])))
            else none
        | _ -> some(&("meet" (tv @ [tk.])))
      -------------------------------------
      conclusion
    };
    
    (* substitute the final type in the rule *)
    substitute(self, final_type);
    
    (* eliminate subtyping premises that are subsumed by a join or meet *)
    let prems = Premises in
    [name] {
      prems(keep)[`t1 <: t2`]:
        let joins = prems[`&(pred ts)` when ((pred = "join") || (pred = "meet"))]:
          let ov1 = var_overlap([t1.], ts) in
          let ov2 = var_overlap([t2.], ts) in
          if empty?(ov1) || empty?(ov2) then none else some(self)
        in
        if empty?(joins) then some(self) else none
      --------------------------------------------
      conclusion
    })
);

(* add the relation for the join of types *)
(Type[`(c ts)`]:
  let vmap = match assoc(c, hint("variance")) with  
    | none -> []
    | some(variance) -> zip(ts, variance)
  in
  let ts2 = ts[`t`]:
    let new_t = fresh_var("T") in
    if binding?(t) then $(bound(t))new_t else new_t
  in
  let ts3 = ts[`t`]:
    let new_t = fresh_var("T") in
    if binding?(t) then $(bound(t))new_t else new_t
  in
  let m2 = zip(ts, ts2) in
  let m3 = zip(ts, ts3) in
  ["JOIN-" ^ uppercase(c)] {
    concat(ts[`t`]:
      let t2 = assoc!(t, m2) in
      let t3 = assoc!(t, m3) in
      let tu = unbind(t) in
      let tu2 = unbind(t2) in
      let tu3 = unbind(t3) in
      match assoc(t, vmap) with
      | some("contra") -> [&("meet" [tu, tu2, tu3]).]
      | some("inv") -> [&(tu = tu2), &(tu3 = tu)]
      | _ -> [&("join" [tu, tu2, tu3]).])
    ---------------------------------------
    &("join" [(c ts), (c ts2), (c ts3)])
  }
);

(* add the relation for the meet of types *)
(Type[`(c ts)`]:
  let vmap = match assoc(c, hint("variance")) with  
    | none -> []
    | some(variance) -> zip(ts, variance)
  in
  let ts2 = ts[`t`]:
    let new_t = fresh_var("T") in
    if binding?(t) then $(bound(t))new_t else new_t
  in
  let ts3 = ts[`t`]:
    let new_t = fresh_var("T") in
    if binding?(t) then $(bound(t))new_t else new_t
  in
  let m2 = zip(ts, ts2) in
  let m3 = zip(ts, ts3) in
  ["MEET-" ^ uppercase(c)] {
    concat(ts[`t`]:
      let t2 = assoc!(t, m2) in
      let t3 = assoc!(t, m3) in
      let tu = unbind(t) in
      let tu2 = unbind(t2) in
      let tu3 = unbind(t3) in
      match assoc(t, vmap) with
      | some("contra") -> [&("join" [tu, tu2, tu3]).]
      | some("inv") -> [&(tu = tu2), &(tu3 = tu)]
      | _ -> [&("meet" [tu, tu2, tu3]).])
    ---------------------------------------
    &("meet" [(c ts), (c ts2), (c ts3)])
  }
);

(* add the relation for subtyping *)
(Type[`(c ts)`]:
  let vmap = match assoc(c, hint("variance")) with  
    | none -> []
    | some(variance) -> zip(ts, variance)
  in
  let ts2 = ts[`t`]:
    let new_t = fresh_var("T") in
    if binding?(t) then $(bound(t))new_t else new_t
  in
  let m2 = zip(ts, ts2) in
  ["S-" ^ uppercase(c)] {
    ts[`t`]:
      let t2 = assoc!(t, m2) in
      let tu = unbind(t) in
      let tu2 = unbind(t2) in
      match assoc(t, vmap) with
      | some("contra") -> tu2 <: tu
      | some("inv") -> &(tu = tu2)
      | _ -> tu <: tu2
    ----------------------------
    (c ts) <: (c ts2)
  }
);

add_relation("join", [$T, $T, $T]);
add_relation("meet", [$T, $T, $T]);
add_relation($T <: $T);

# mode: ... | join => inp inp out | meet => inp inp out | subtype => inp inp;
# principal: ... | join => yes yes no | meet => yes yes no | subtype => yes yes;

(* add the cast operator to the grammar for expressions, contexts *)
Expression e ::= ... | ("cast" [$e, $T]).;
Context E ::= ... | ("cast" [$E, $T]).;

(* add the typing rule for casts *)
let assume = head(relations[`("typeof", a :: _)`]: a) in
["T-CAST"] {
  assume |- $e : $T1,
  $T1 <: $T2
  ----------------------------------
  assume |- ("cast" [$e, $T2]) : $T2
};

(* add the reduction rule for casts *)
let config = head(relations[`("step", a :: _)`]: a) in
let do_config (t: term) = match config with
  | <_ :: ts> -> <t :: ts>
  | $!_ -> t
in

["R-CAST"] {
  ----------------------------------------------
  do_config(("cast" [$v, $T])) --> do_config($v)
}