mzacho/refinement-types

A refinement type checker for simply typed lamda calculus with inductive data-types and well-founded recursive functions

refinement-types's Issues

sumT fails

The test sumT: recursion on multiple parameters terminates fails. Dunno what's wrong. Cleaned up constraints:

(∀zero:ℤ. zero=0 ⇒
    (∀one:ℤ. one=1 ⇒
    (∀ten:ℤ. ten=10 ⇒
      (∀total:ℤ. (∀x:ℤ.
        (∀v:ℤ. x=v ) ∧
        (∀v:ℤ. v=1 ∧ one=v ) ∧
        (∀y:𝔹. ¬y ∨ x<one ∧ ¬x<one ∨ y ⇒
          (∀z:𝔹. ¬z ∨ x<one ∧ ¬x<one ∨ z ∧ y=z ) ∧
          (∀fr0:ℤ. y ⇒ (∀v:ℤ. v=0 )) ∧
          (∀fr0:ℤ. ¬y ⇒ (∀v:ℤ. total=v ) ∧
            (∀v:ℤ. v=1 ∧ one=v ) ∧
            (∀newtotal:ℤ. newtotal=total+one ⇒
               (∀v:ℤ. x=v) ∧
               (∀v:ℤ. v=1 ∧ one=v ⇒ True) ∧
               (∀newx:ℤ. newx=x-one ⇒
                 (∀z:ℤ. z=total+one ∧ newtotal=z ⇒ 0<=x ∧ x<x) ∧
                 (∀z:ℤ. z=x-one ∧ newx=z ))))))) ∧
                   (∀v:ℤ. v=0 ∧ zero=v) ∧
                   (∀v:ℤ. v=10 ∧ ten=v))))

on the termination branch

lookup codomain of uninterpreted function in `metric_wf`

When checking let rec expressions with a metric that's a call to an uninterpreted function (such as "length reflects len" whose metric is len(xs)), we're currently assume that any function has as result that's int-sorted.

See the P_FunApp case in check_sort:

let rec check_sort (g : logic_env) (p : L.pred) (s : L.sort) : bool =
  match s with
  | L.S_Int -> (
      match p with
      | L.P_Int _ -> true
      (* check that both predicates are int-sorted *)
      | L.P_Op (_, p1, p2) -> check_sort g p1 s && check_sort g p2 s
      | L.P_Var x -> (
          try
            let _, s' = List.find (fun (y, _) -> String.equal y x) g in
            s' = L.S_Int
          with Not_found -> true)
      | P_FunApp (_, _) -> true (* TODO: lookup codomain of uninterpreted fun *)
      | _ -> false
  )
  | L.S_Bool -> failwith "unimplemented"
  | L.S_TyCtor _ -> failwith "unimplemented"

on the termination branch

parsing: precedence of negation wrt. conj/ disj is wrong

so the type of lt is currently parsed incorrectly

substitute type can capture variables under refinement binder

Consider checking if the application f x synthesizes to bool in the environment where f:y:int -> bool{x: (y = y) = x} and x:bool. Then substitute_type will produce a constraint similar to forall x:int. (x = x) = x

Fix:

Add something like

if String.equal v z then
         let fv = fresh_var () in
         T_Refined (b, fv, L.substitute_pred y z @@ L.substitute_pred v fv p)

in substitute_type, as well as for the case with arrow types. We have the same issue in subst_constraint.

checking "append reflects len" fails

On the termination branch.

This is the generated contraint:

(∀xs:list. True
    ⇒ True ∧
      (∀hd:ℤ. True
        ⇒ (∀tl:list. True
          ⇒ (∀xs:list. True ∧ len(xs)=1+len(tl)
            ⇒ True ∧
              True ∧
              (∀v:list. True ∧ tl=v ⇒ True ∧ 0<=len(v) ∧ len(v)<len(xs))
              ∧ (∀lengthtail:ℤ. lengthtail=len(tl)
                 ⇒ True ∧
                   (∀one:ℤ. one=1
                   ⇒ True ∧
                     True ∧
                     (∀v:ℤ. v=len(tl) ∧ lengthtail=v ⇒ True) ∧
                     True ∧
                     (∀v:ℤ. v=1 ∧ one=v ⇒ True) ∧
                     (∀z:ℤ. z=lengthtail+one ⇒ z=len(xs))))))) ∧
    (∀xs:list. True ∧ len(xs)=0 ⇒ True ∧ (∀v:ℤ. v=0 ⇒ v=len(xs)))) ∧
True ∧
(∀v:list. True ⇒ True) ∧
(∀xs:list. True ⇒ (∀v:ℤ. v=len(xs) ⇒ v=len(xs)))

The type of the length function is limited in the ty env when checking the body of the let expression:

length:fr0:list{fr0:True ∧ 0<=len(fr0) ∧ len(fr0)<len(xs)}->int{v:v=len(fr0)}

which is also reflected in the contraint above.

enforce exhaustive switch alternatives

This allows proving false in the sense of Curry-Howard:

val f : list -> int:{x:False}
let rec f =
  (fn l. match l with end)

in ...

SUB-BASE can capture free variables with the binder

Found a bug in our implementation of SUB-BASE: Consider checking if int{x: True} is a subtype of int{v: x > v} in the environment where x:int. Then the x in the predicate, that refers to the x from the environment is incorrectly captured by the binder: Forall x:int: True => x > x. So v1 should be a fresh var in the rule

enforce that we don't add vars twice to env Gamma

Currently, we don't check if a var is already in Gamma before adding it. We could check and throw an error if it is already present.