diff --git a/README.md b/README.md index d6aa6a3..391469f 100644 --- a/README.md +++ b/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) diff --git a/TODO.md b/TODO.md index 8fffb8d..0eb7a05 100644 --- a/TODO.md +++ b/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? diff --git a/doc/invargent.pdf b/doc/invargent.pdf index db04b8f..a5d0e8c 100644 Binary files a/doc/invargent.pdf and b/doc/invargent.pdf differ diff --git a/doc/invargent.tm b/doc/invargent.tm index 895ce6b..6586af1 100644 --- a/doc/invargent.tm +++ b/doc/invargent.tm @@ -484,7 +484,10 @@ In fact, when performing unification, we check more than |\>|\>>.A|)>> requires. We also ensure that the use of parameters will not cause problems - in the phase of the main algorithm. + in the phase of the main algorithm. To this effect, we + forbid substitution of a variable from |\>> with + a term containing a universally quantified variable that is not in + |\>>. In implementing p. 13, we follow top-down approach where bigger subterms are abstracted first -- replaced by fresh @@ -1762,7 +1765,7 @@ > > > - > + > > > > diff --git a/examples/non_pointwise_avl.gadti.target b/examples/non_pointwise_avl.gadti.target index 0aa023a..90d6786 100644 --- a/examples/non_pointwise_avl.gadti.target +++ b/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)))) diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index df2482e..241677f 100644 --- a/src/InvarGenTTest.ml +++ b/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 () -> diff --git a/src/Invariants.ml b/src/Invariants.ml index d581b4e..7ab174e 100644 --- a/src/Invariants.ml +++ b/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) -> diff --git a/src/InvariantsTest.ml b/src/InvariantsTest.ml index 3fb4bff..2c37f5d 100644 --- a/src/InvariantsTest.ml +++ b/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 diff --git a/src/NumS.ml b/src/NumS.ml index 1cfb0bc..ccb14f0 100644 --- a/src/NumS.ml +++ b/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 diff --git a/src/Terms.ml b/src/Terms.ml index 54d414d..dc2a70a 100644 --- a/src/Terms.ml +++ b/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)