Better and simpler test for violations of the split condition in `u…

…nify`.

README.md

@@ -28,6 +28,7 @@ Version 2.0 goals -- version targets may be reassigned:
 - [_] 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. (v1.4)
 - [_] Optimize, paying attention to the speed of the update mode. (v1.4)
 - [_] Support OCaml-style records, with some desambiguation roughly as in OCaml. (v1.4)
+- [_] Or-patterns `p1 | p2` expanded for inference but preserved in exported code. (v1.4)
 - [_] Syntax for numeric multiplication. (v2.0)
 - [_] Add a new "promising" sort. Candidates: integer numbers, partial orders, ring of polynomials... (v2.0)
 

TODO.md

@@ -7,3 +7,4 @@ Place for TODOs/FIXMEs, especially if not expressed in other places. See README.
 * TODO: more parsimonious use of parentheses in printing expressions and types.
 * TODO: 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. In update mode, if typechecking fails, retry without type annotation. In verify mode, check that the resulting type matches the interface type from `.gadti` -- is not less general. In update mode, regenerate the `.gadti` file.
 * FIXME: when checking discarded in term abduction, in iteration 0 (only?), check modulo renaming of alien sort variables.
+* FIXME: missing "assert false" branches in exported code?

doc/invargent.tm

@@ -484,7 +484,10 @@
   In fact, when performing unification, we check more than
   <math|\<b-U\><rsub|<wide|\<alpha\>|\<bar\>><wide|\<beta\>|\<bar\>>><around*|(|\<cal-Q\>.A|)>>
   requires. We also ensure that the use of parameters will not cause problems
-  in the <verbatim|split> phase of the main algorithm.
+  in the <verbatim|split> phase of the main algorithm. To this effect, we
+  forbid substitution of a variable from <math|<wide|\<beta\>|\<bar\>>> with
+  a term containing a universally quantified variable that is not in
+  <math|<wide|\<beta\>|\<bar\>>>.
 
   In implementing <cite|AbductionSolvMaher> p. 13, we follow top-down
   approach where bigger subterms are abstracted first -- replaced by fresh
@@ -1762,7 +1765,7 @@
     <associate|auto-5|<tuple|2.2|5>>
     <associate|auto-6|<tuple|3|5>>
     <associate|auto-7|<tuple|3.1|6>>
-    <associate|auto-8|<tuple|3.1.1|7>>
+    <associate|auto-8|<tuple|3.1.1|8>>
     <associate|auto-9|<tuple|3.2|8>>
     <associate|bib-AbductionSolvMaher|<tuple|3|20>>
     <associate|bib-AntiUnifAlg|<tuple|9|20>>

examples/non_pointwise_avl.gadti.target

@@ -1,18 +1,30 @@
 (** Normally we would use [num], but this is a stress test for [type]. *)
 newtype Z
-Newtype S : type
+
+newtype S : type
+
 newtype Balance : type * type * type
+
 newcons Less : ∀a. Balance (a, S a, S a)
-newcons Same : ∀a. Balance (a, a, a)
+
+newcons Same : ∀b. Balance (b, b, b)
+
 newcons More : ∀a. Balance (S a, a, S a)
+
 newtype AVL : type
+
 newcons Leaf : AVL Z
-newcons Node :
-  ∀a, b, c. Balance (a, b, c) * AVL a * Int * AVL b ⟶ AVL (S c)
+
+newcons Node : ∀a, b, c.Balance (a, b, c) * AVL a * Int * AVL b ⟶
+   AVL (S c)
 
 newtype Choice : type * type
-newcons Left : ∀a, b. a ⟶ Choice (a, b)
-newcons Right : ∀a, b. b ⟶ Choice (a, b)
+
+newcons Left : ∀a, b.a ⟶ Choice (a, b)
+
+newcons Right : ∀a, b.b ⟶ Choice (a, b)
 
 val rotr :
-  ∀a. Int → AVL a → AVL (S (S a)) → Choice (AVL (S (S a)), AVL (S (S (S a))))
+   ∀a.
+   Int → AVL a → AVL (S (S a)) →
+     Choice (AVL (S (S a)), AVL (S (S (S a))))

src/InvarGenTTest.ml

@@ -152,7 +152,7 @@ let tests = "InvarGenT" >::: [
            test_case ~richer_answers:true "non_pointwise_avl_small" ());
       "non_pointwise_avl" >::
         (fun () ->
-           todo "harder test";
+           skip_if !debug "debug";
            test_case ~richer_answers:true "non_pointwise_avl" ());
       "non_pointwise_vary" >::
         (fun () ->

src/Invariants.ml

@@ -611,6 +611,7 @@ let solve q_ops new_ex_types exty_res_chi brs =
                 brs) in
          more @ prem, concl)
       neg_brs in
+  (*[* Format.printf "solve: pos_brs=@ %a@\n%!" Infer.pr_rbrs pos_brs; *]*)
   (*[* Format.printf "solve: neg_brs=@ %a@\n%!" Infer.pr_rbrs neg_brs; *]*)
   let neg_cns = List.map
       (fun (prem, concl) ->

src/InvariantsTest.ml

@@ -772,6 +772,7 @@ let rec walk = fun x ->
   "existential with param" >::
     (fun () ->
        skip_if !debug "debug";
+       todo "make no abduction for postconditions & not in bvs on iter=0";
        test_case "existential with param"
 "newtype Place : type
 newtype Nearby : type * type

src/NumS.ml

@@ -238,6 +238,8 @@ let eqineq_loc_union (eqn, ineqn) =
 let un_ans (eqs, ineqs) = unsubst eqs, unsolve ineqs
 
 (* Assumption: [v] is downstream of all [vars] *)
+(* TODO: understand why the equivalent of [Terms.quant_viol] utterly
+   fails here. *)
 let quant_viol uni_v bvs v vars =
   let res = uni_v v && not (VarSet.mem v bvs) in
   (*[* if res then

src/Terms.ml

@@ -1218,37 +1218,31 @@ let connected ?(validate=fun _ -> ()) target (vs, phi) =
 let var_not_left_of q v t =
   VarSet.for_all (fun w -> q.cmp_v v w <> Left_of) (fvs_typ t)
 
-(* If there are no [bvs] parameters, the LHS variable has to be
+(* If [v] is not a [bvs] parameter, the LHS variable has to be
    existential and not upstream (i.e. left of) of any RHS variable
    that is not in [pms].
 
-   If [v] is a [bvs] parameter, every universal variable must be
-   left of some [bv] parameter. (Note that a [bv] parameter that
-   is sufficiently downstream is a "savior".) Existential variables
-   are not constrained: do not need to be same as or to the left of [v]. *)
+   If [v] is a [bvs] parameter, the RHS must not contain a universal
+   non-[bvs] variable. Existential variables are not constrained: do not
+   need to be same as or to the left of [v]. *)
 let quant_viol q bvs pms v t =
-  let uv = q.uni_v v in
-  let pvs, npvs = List.partition (fun v->VarSet.mem v bvs)
+  let uv = q.uni_v v and bv = VarSet.mem v bvs in
+  let npvs = List.filter (fun v-> not (VarSet.mem v bvs))
     (VarSet.elements (fvs_typ t)) in
-  let pvs = if VarSet.mem v bvs then v::pvs else pvs in
   let uni_vs =
-    List.filter q.uni_v (if VarSet.mem v bvs then npvs else v::npvs) in
+    List.filter q.uni_v (if bv then npvs else v::npvs) in
   (*[* Format.printf "quant_viol: vrels %!"; *]*)
   let res =
-  if not (VarSet.mem v bvs) then uv ||
+  if not bv then
+    uv ||
     List.exists
     (fun v2 ->
       (*[* Format.printf "%s %s %s; " (var_str v)
         (var_scope_str (q.cmp_v v v2)) (var_str v2); *]*)
       not (VarSet.mem v2 pms) && q.cmp_v v v2 = Left_of) npvs
-  else
-    not
-      (List.for_all
-         (fun uv -> q.cmp_v v uv = Same_quant ||
-                    List.exists (fun pv -> q.cmp_v uv pv = Left_of) pvs)
-         uni_vs) in
+  else uni_vs <> [] in
   (*[* Format.printf
-    "@\nquant_viol: %b; v=%s; uv=%b;@ t=%a;@ bvs=%a;@ pms=%a;@ pvs=%a;@
+    "@\nquant_viol: %b; v=%s; uv=%b;@ t=%a;@ bvs=%a;@ pms=%a;@ \
    uni_vs=%a; npvs=%a@\n%!"
     res (var_str v) uv (pr_ty false) t
     pr_vars bvs pr_vars pms pr_vars (vars_of_list pvs)