# Generic Refinements

b ::=
    % keys are u32, values are String
    | HashMap[valid: u32 -> bool]
    % values are String
    | OptionString[is_some: bool]

let if<a>        : forall b: Bool. forall x: a. forall y: a.
                   Bool[b] -> ({() | b = true} -> a[x]) -> ({() | b = false} -> a[y]) -> a[if b then x else y]

let new          : () -> HashMap[\k: u32. false];
let lookup       : forall valid: (u32 -> Bool).
                   HashMap[valid] -> {k. String[k] | valid(k)} -> String;
let contains_key : forall valid: (u32 -> Bool). forall key: u32.
                   HashMap[valid] -> String[key] -> bool[valid(key)];
let insert       : forall valid: (u32 -> Bool). forall key: u32. forall value: String.
                   HashMap[valid] -> {String[key] | !valid(key)} -> String[value] -> HashMap[\k -> valid(k) || k == key];

let get : forall valid: (u32 -> Bool). forall key: u32.
          HashMap[valid] -> String[key] -> OptionString[valid(key)]
        = \m : HashMap[valid]. \k : String[key]. if<Option>(
            contains_key(m, k),
            \(): {() | contains_key(m, k) = true}. Some(index(m, k)),
            \(): {() | contains_key(m, k) = false}. None);

let test : () -> () =
  let zero: u32 = 0 in
  let one:  u32 = 1 in
  let two:  u32 = 2 in
  let m: HashMap[\k: u32. false] = new() in
  let m: HashMap[\k: u32. false || k = 0] = insert(m, zero, "cat") in
  let m: HashMap[\k: u32. false || k = 0 || k = 1] = insert(m, one, "dog") in
  let _: String       = lookup(m, zero) in
  let _: OptionString[(\k: u32. false || k = 0 || k = 1) 1] = m.get(two) in
  ()

       Φ; Γ ⊢ e1: bool[b] 
      Φ,b=true; Γ ⊢ e2 <= t
     Φ,b=false; Γ ⊢ e3 <= t
      Φ,b=true; Γ ⊢ e2 : {t | r1}
     Φ,b=false; Γ ⊢ e3 : {t | r2}
----------------------------------
   Φ;Γ ⊢ if e1 then e2 else e3 : {t | if b then r1 else r2}

       Φ; Γ ⊢ e1: bool[b] 
      Φ,b=true; Γ ⊢ e2 : t1   t1 <: t
     Φ,b=false; Γ ⊢ e3 : t2   t2 <: t
----------------------------------
   Φ;Γ ⊢ if e1 then e2 else e3 : t

       Φ; Γ ⊢ e1: bool[b] 
      Φ,b=true; Γ ⊢ e1 : {v. int[v] | v >= 10}   int[1 + 1] <: {v. int[v] | b => v >= 10 && !b => v >= 4}
     Φ,b=false; Γ ⊢ 2 + 2 : int[2 + 2]           int[2 + 2] <: {v. int[v] | v >= 4}
----------------------------------
   Φ;Γ ⊢ if b then 1 + 1 else 2 + 2 : int[if b then 1 + 1 else 2 + 2]

let if<a>        : forall b: Bool.
                   Bool[b] -> ({() | b = true} -> a) -> ({() | b = false} -> a) -> a

λx: {v. int[v] | v > 0}. x + 1

λx: {v. int[v] | v > 0}. 
  // Γ= x: {v. int[v] | v > 0}
  // Γ = x: int[a], Φ = a:Z, a > 0 
  x + 1 : int[a + 1]
  
{v. int[v] | v > 0} -> {a. int[a + 1] | a > 0 }


(λx. x + 1 : ∀a.int[a] -> int[a + 1])
(λx. x + 1 : {v. int[v] | v > 0} -> {v. int[v] | v > 1})


+: ∀a,b. int[a] -> int[b] -> int[a + b]