diff --git a/Strata/DL/Bounded/BExpr.lean b/Strata/DL/Bounded/BExpr.lean new file mode 100644 index 00000000..c515cc4c --- /dev/null +++ b/Strata/DL/Bounded/BExpr.lean @@ -0,0 +1,418 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.DL.Lambda.LTy +import Strata.DL.Lambda.LExprT +import Strata.DL.Lambda.IntBoolFactory + +/-! ## Lambda Expressions with Bounded Ints + +Here, we desugar LExprTs with bounded int types into regular Lambda expressions by performing two steps: +1. Translating the term, keeping track of assumptions implicit in the bounded types. +2. Generating well-formedness conditions e.g. for function calls. +Most bounds must be explicitly stated; the only inferred/checked ones occur when calling a function requiring a bounded argument on a int-typed argument. +-/ + +/- +The process of keeping track of assumptions and constraints is complicated. Here we give the key ideas (using the type nat = {x | 0 ≤ x} as an example): +1. There are two kinds of assumptions: context-dependent (e.g. for ∀ (x: nat). e, we assume 0 ≤ x when translating e) and context-independent (e.g. for external operator foo: int → nat, we are always free to assume 0 ≤ foo 1). +2. The context-dependent assumptions must be propagated top-down (when recursively translating the body of a quantifier or lambda), while the context-independent assumptions must be propagated bottom-up (as we do not know which external symbols appear in a subterm without inspecting it). +3. Assumptions can only be added to boolean-valued terms. Therefore, the basic algorithm is as follows: maintain a set of the top-down assumptions and recursively traverse the term, removing bounded types. Whenever a bool-valued expression is reached, recursively translate the body and collect the bottom-up assumptions. Then add all assumptions to the translated body. +4. However, we cannot freely add assumptions in non-strictly-positive positions without changing the semantics. Therefore, if in such a position, we do not add the bottom-up assumptions but rather keep propagating upward until we reach a strictly positive position (which must exist at least at the outer layer). Since it is not possible to always determine whether a position is positive without β-reduction, we are conservative and assume all unknown positions are non-positive. +5. We must be careful about binders and quantify bottom-up assumptions that escape the scope of a quantified variable due to the above positivity restriction. For example, (∃ (x: int). foo x < 0) → False is translated to (∀ (x: int). 0 ≤ foo' x) → ((∃ (x: int). foo' x < 0) → False) where foo' has type int → int + +Generating well-formedness conditions is somewhat simpler. The main rules are: +1. Constants that claim to have a bounded type are checked (e.g. 3: nat) +2. For application e₁e₂ where e₁ has type b → T, we check that b holds of the translated e₂ +3. For application e₁e₂ : b where e₁ has type T -> int, we check that the translated application satisfies b. (Note: we cannot just check bounded types in general because some bounds are assumed e.g. for external operators) +4. For λ (x : T). e : T -> b, we check that e satisfies bound b (possibly assuming any bounds for x) +Proving these well-formedness conditions may require both the top-down and bottom-up assumptions, so we compute all at the same time. + +See StrataTest/DL/Bounded/BExprTest.lean for test cases that further illustrate the expected translations and well-formedness conditions. + +-/ + +namespace Bounded +open Std (ToFormat Format format) +open Lambda + +variable {Identifier : Type} [ToString Identifier] [DecidableEq Identifier] [ToFormat Identifier] [HasGen Identifier] + +/-- +Translate bounded integer expression b to LExprT with holes filled by e +-/ +def boundValToLExprT (b: BoundVal) (e: LExprT Identifier) : LExprT Identifier := + match b with + | .bvar => e + | .bconst val => .const (val.repr) LMonoTy.int + +/- +Utilities to construct common operators on common int and bool functions from IntBoolFactory.lean +-/ + +-- Adapted for LExprT from Factory.lean +def LFunc.opExprT (f: LFunc Identifier) : LExprT Identifier := + let input_tys := f.inputs.values + let output_tys := Lambda.LMonoTy.destructArrow f.output + let ty := match input_tys with + | [] => f.output + | ity :: irest => Lambda.LMonoTy.mkArrow ity (irest ++ output_tys) + .op f.name ty + +/-- +Constructs the LExprT (.op o) e1 e2, where o has type bool -> bool -> bool +-/ +def boolBinopExprT (o: LFunc Identifier) (e1 e2: LExprT Identifier) : LExprT Identifier := + .app (.app (LFunc.opExprT o) e1 (.arrow .bool .bool)) e2 .bool + +/-- +Constructs the LExprT (.op o) e1 e2, where o has type int -> int -> bool +-/ +def intCompBinopExprT (o: LFunc Identifier) (e1 e2: LExprT Identifier) : LExprT Identifier := + .app (.app (LFunc.opExprT o) e1 (.arrow .int .bool)) e2 .bool + +def andExprT [Coe String Identifier] (e1 e2: LExprT Identifier) : LExprT Identifier := + boolBinopExprT boolAndFunc e1 e2 + +def implExprT [Coe String Identifier] (e1 e2: LExprT Identifier) : LExprT Identifier := + boolBinopExprT boolImpliesFunc e1 e2 + +def notExprT [Coe String Identifier] (e: LExprT Identifier) : LExprT Identifier := + .app (LFunc.opExprT boolNotFunc) e .bool + +def intLtExprT [Coe String Identifier] (e1 e2: LExprT Identifier) : LExprT Identifier := + intCompBinopExprT intLtFunc e1 e2 + +def intLeExprT [Coe String Identifier] (e1 e2: LExprT Identifier) : LExprT Identifier := + intCompBinopExprT intLeFunc e1 e2 + +/-- +Translate BoundExpr b to corresponding Lambda expression +-/ +def boundExprToLExprT [Coe String Identifier] (b: BoundExpr) (e: LExprT Identifier) : +LExprT Identifier := + match b with + | .beq b1 b2 => + .eq (boundValToLExprT b1 e) (boundValToLExprT b2 e) LMonoTy.bool + | .blt b1 b2 => intLtExprT (boundValToLExprT b1 e) (boundValToLExprT b2 e) + | .ble b1 b2 => intLeExprT (boundValToLExprT b1 e) (boundValToLExprT b2 e) + | .band e1 e2 => andExprT (boundExprToLExprT e1 e) (boundExprToLExprT e2 e) + | .bnot e1 => notExprT (boundExprToLExprT e1 e) + +-- Auxilliary functions for translation + +/-- +Add list of assumptions l to boolean-valued e +-/ +private def addAssumptions [Coe String Identifier] (l: List (LExprT Identifier)) (e: LExprT Identifier) : LExprT Identifier := + List.foldr implExprT e l + +/-- +Produce l₁ ∧ ... ∧ lₙ ∧ e +-/ +private def addAndExprs [Coe String Identifier] (l: List (LExprT Identifier)) (e: LExprT Identifier) : LExprT Identifier := + List.foldr andExprT e l + +/- +An inefficient method of maintaining a list with no duplicates. Should be replaced with a HashSet or similar +-/ +def ListSet α := List α + +def ListSet.contains {α} [DecidableEq α] (l: ListSet α) (x: α) : Bool := + List.foldr (fun y acc => x == y || acc) false l + +def ListSet.insert {α} [DecidableEq α] (l: ListSet α) (x: α) : ListSet α := + if ListSet.contains l x then l else x :: l + +def ListSet.insertAll {α} [DecidableEq α] (l: ListSet α) (xs: List α) : ListSet α := + List.foldr (fun x acc => ListSet.insert acc x) l xs + +def ListSet.union {α} [DecidableEq α] (l: List (ListSet α)) : ListSet α := + List.foldr ListSet.insertAll [] l + +-- Auxiliary functions for producing bounds/assumptions + +/- +All top-down assumptions initially start as expressions over (.bvar 0 .int). As we pass through binders, these bvars must be increased. We only care about expressions consisting of bvar, eq, app (output of boundExprToLExprT) +-/ +private def increaseBVar (e: LExprT Identifier) : LExprT Identifier := + match e with + | .bvar b ty => .bvar (b+1) ty + | .eq e1 e2 ty => .eq (increaseBVar e1) (increaseBVar e2) ty + | .app e1 e2 ty => .app (increaseBVar e1) (increaseBVar e2) ty + | _ => e + +private def increaseBVars (l: List (LExprT Identifier)) : List (LExprT Identifier) := + List.map increaseBVar l + +private def isBounded (t: LMonoTy) : Option BoundExpr := + match t with + | LMonoTy.bounded b => .some b + | _ => .none + +private def removeTyBound (t: LMonoTy) : LMonoTy := + match t with + | LMonoTy.bounded _ => LMonoTy.int + | .tcons name args m => .tcons name (List.map removeTyBound args) m + | _ => t + +/-- +If ty is .bounded b, produces expression b(e) +-/ +private def boundExprIfType [Coe String Identifier] (ty: LMonoTy) (e: LExprT Identifier) : List (LExprT Identifier) := + ((isBounded ty).map (fun b => boundExprToLExprT b e)).toList + +/-- +If ty is .bounded b, produces expression b(.bvar 0 .int) +-/ +def makeBoundAssumption [Coe String Identifier] (ty : LMonoTy) : List (LExprT Identifier) := boundExprIfType ty (.bvar 0 .int) + +/-- +Generates WF condition for calling e1 with argument e2 if bounded type expected +-/ +def wfCallCondition [Coe String Identifier] (assume : List (LExprT Identifier)) (e1 e2: LExprT Identifier) := + match LExprT.toLMonoTy e1 with + | .arrow (.bounded b) _ => + -- check that translated e2 satisfies precondition under assumptions + [addAssumptions assume (boundExprToLExprT b e2)] + | _ => [] + +/-- + Universally quantifies all expressions in lists l1 and l2, additionally adding assumptions in "assume" to l1. These quantifiers will eventually be removed in a postprocessing step +-/ +private def addBoundedWf [Coe String Identifier] (assume: List (LExprT Identifier)) (l1 l2: List (LExprT Identifier)) : List (LExprT Identifier) := + List.map (fun e => .quant .all .int (.bvar 0 .int) (addAssumptions assume e)) l1 ++ List.map (.quant .all .int (.bvar 0 .int)) l2 + +/-- + Universally quantifies all expressions in list l with additional assumptions in "assume" +-/ +private def addBoundedWfAssume [Coe String Identifier] (assume: List (LExprT Identifier)) (l: List (LExprT Identifier)) := + addBoundedWf assume l [] + +/-- +Determines if a term uses a particular bound variable at the top level +-/ +private def hasBvar (e: LExprT Identifier) (n: Nat) : Bool := + match e with + | .bvar m _ => n == m + | .app e1 e2 _ => hasBvar e1 n || hasBvar e2 n + | .abs e _ => hasBvar e (n + 1) + | .quant _ _ _ e => hasBvar e (n + 1) + | .eq e1 e2 _ => hasBvar e1 n || hasBvar e2 n + | .mdata _ e => hasBvar e n + | .ite e1 e2 e3 _ => hasBvar e1 n || hasBvar e2 n || hasBvar e3 n + | _ => false + +/-- +When passing an assumption through a binder, we need to quantify the bound variable if used. +-/ +private def quantifyAssumptions (ty: LMonoTy) (e: LExprT Identifier): LExprT Identifier := + --TODO: triggers? + if hasBvar e 0 then .quant .all ty (.bvar 0 ty) e else e + +/-- +Add extra to base iff b holds +-/ +def conditionalAdd (b : Bool) (base extra : List α) : List α := + if b then base ++ extra else base + +def conditionalReturn (pos : Bool) (value : List α) : List α := + if pos then [] else value + +/-- +A "clean" translation that only removes types; used for triggers +-/ +private def translateClean [Coe String Identifier] (e: LExprT Identifier) : LExprT Identifier := + match e with + | .const c ty => .const c (removeTyBound ty) + | .op o ty => .op o (removeTyBound ty) + | .bvar b ty => .bvar b (removeTyBound ty) + | .fvar f ty => .fvar f (removeTyBound ty) + | .app e1 e2 ty => .app (translateClean e1) (translateClean e2) (removeTyBound ty) + | .abs e ty => .abs (translateClean e) (removeTyBound ty) + | .quant qk ty tr e' => .quant qk (removeTyBound ty) (translateClean tr) (translateClean e') + | .ite c t f ty => .ite (translateClean c) (translateClean t) (translateClean f) (removeTyBound ty) + | .eq e1 e2 ty => .eq (translateClean e1) (translateClean e2) (removeTyBound ty) + | .mdata m e => .mdata m (translateClean e) + +structure translationRes Identifier where +(translate : LExprT Identifier) +(wfCond : ListSet (LExprT Identifier)) +(assume : List (LExprT Identifier)) + +/-- + Under top-down assumptions "assume" and positivity "pos", produce the translation, well-formedness conditions, and bottom-up assumptions for expression e +-/ +def translateBounded [Coe String Identifier] [DecidableEq Identifier] (e: LExprT Identifier) (assume: List (LExprT Identifier)) (pos : Bool) : translationRes Identifier := + match e with + -- constants do not need assumptions; they produce a wf goal if bounded + | .const c ty => + let res := .const c (removeTyBound ty); + ⟨res, boundExprIfType ty res, []⟩ + -- an op adds a bottom-up assumption if it has bounded type; its wf is assumed + | .op o ty => + let res := .op o (removeTyBound ty); + ⟨if ty == .bool then addAssumptions assume res else res, [], boundExprIfType ty res⟩ + -- bvars are handled when bound + | .bvar b ty => ⟨ .bvar b (removeTyBound ty), [], [] ⟩ + -- fvars generate bottom-up assumptions if bounded + | .fvar f ty => + let res := .fvar f (removeTyBound ty); + ⟨res, [], boundExprIfType ty res⟩ + /- + Application has several cases: + 1. If the entire application has boolean type, assumptions can be added subject to positivity. + 2. Otherwise, if the application has bounded type, it produces a bottom-up assumption. There is a subtle case. If the function has type (t -> int), then we must generate a wf condition. Otherwise, the bound will be assumed (for external operators) or checked (for abstraction/if-then-else/etc) + 3. In either case, we produce a wf condition if the argument should have bounded type. + -/ + | .app (.op o ty1) e2 .bool => + let notCase := o == boolNotFunc.name; + -- inside "not" - not positive + let e2' := translateBounded e2 [] (not notCase && pos); + let all_assumes := conditionalAdd pos assume e2'.assume; + let res := addAssumptions all_assumes (.app (.op o (removeTyBound ty1)) e2'.translate .bool); + ⟨res, ListSet.union [wfCallCondition (assume ++ e2'.assume) (.op o ty1) e2'.translate, e2'.wfCond], conditionalReturn pos e2'.assume⟩ + | .app (.app (.op o ty1) e1 ty2) e2 .bool => + -- The first argument has positivity pos if the operator is "and" or "or" otherwise false + let first := (o == boolAndFunc.name || o == boolOrFunc.name) && pos; + -- The second also includes the RHS of implication + let second := (o == boolAndFunc.name || o == boolOrFunc.name || o == boolImpliesFunc.name) && pos; + let e1' := translateBounded e1 [] first; + let e2' := translateBounded e2 [] second; + let all_assumes := conditionalAdd pos assume (e1'.assume ++ e2'.assume); + let res := addAssumptions all_assumes (.app (.app (.op o (removeTyBound ty1)) e1'.translate (removeTyBound ty2)) e2'.translate .bool); + ⟨res, ListSet.union [wfCallCondition (assume ++ e2'.assume) e1 e2'.translate, e1'.wfCond, e2'.wfCond], conditionalReturn pos (e1'.assume ++ e2'.assume)⟩ + | .app e1 e2 .bool => + --Anything else we cannot assume is positive + let e1' := translateBounded e1 [] false; + let e2' := translateBounded e2 [] false; + let all_assumes := conditionalAdd pos assume (e1'.assume ++ e2'.assume); + let res := addAssumptions all_assumes (.app e1'.translate e2'.translate .bool); + ⟨res, ListSet.union [wfCallCondition (assume ++ e2'.assume) e1 e2'.translate, e1'.wfCond, e2'.wfCond], conditionalReturn pos (e1'.assume ++ e2'.assume)⟩ + | .app e1 e2 ty => + let e1' := translateBounded e1 assume pos; + let e2' := translateBounded e2 assume pos; + let res := .app e1'.translate e2'.translate (removeTyBound ty); + -- If we have application f x where f : _ -> int and f x has bounded type, need wf condition that application result is bounded + let extraWf := + match LExprT.toLMonoTy e1, ty with + | .arrow _ .int, .bounded _ => + boundExprIfType ty res + | _, _ => []; + ⟨res, ListSet.union [wfCallCondition (assume ++ e2'.assume) e1 e2'.translate, extraWf, e1'.wfCond, e2'.wfCond], boundExprIfType ty res ++ e1'.assume ++ e2'.assume⟩ + /- + Lambda abstraction: + 1. If the argument is bounded, add as top-down assumption + 2. If the body has type bool, add assumptions and translate + 3. Otherwise, add assumptions and increase bvars of all in "assume" list, as they are passing through a binder + 4. WF: if body bounded, prove body satisfies bound with same assumptions (but without new binder) + -/ + | .abs e (.arrow ty .bool) => + let e' := translateBounded e [] pos; + let all_assume := conditionalAdd pos (makeBoundAssumption ty ++ (increaseBVars assume)) e'.assume; + ⟨.abs (addAssumptions all_assume e'.translate) (removeTyBound (.arrow ty .bool)), addBoundedWfAssume all_assume e'.wfCond, conditionalReturn pos (List.map (quantifyAssumptions (removeTyBound ty)) e'.assume)⟩ + | .abs e (.arrow ty1 ty2) => + let all_assume := makeBoundAssumption ty1 ++ (increaseBVars assume); + let e' := translateBounded e all_assume pos; + let res := .abs e'.translate (removeTyBound (.arrow ty1 ty2)); + -- Note: don't add assumptions to e'.wfCond, already included + ⟨res, addBoundedWf all_assume (boundExprIfType ty2 e'.translate) e'.wfCond, List.map (quantifyAssumptions (removeTyBound ty1)) e'.assume⟩ + | .abs _ _ => ⟨.const "0" .int, [], []⟩ -- error case + /- + Quantifiers are simpler because they are boolean-valued. ∀ (x : nat). e adds an assumption x >= 0 -> ..., while ∃ (x: nat). e results in x >= 0 ∧ .. + -/ + | .quant .all ty tr e => + let e' := translateBounded e [] pos; + let tr' := translateClean tr; + let all_assume := conditionalAdd pos (makeBoundAssumption ty ++ (increaseBVars assume)) e'.assume; + ⟨.quant .all (removeTyBound ty) tr' (addAssumptions all_assume e'.translate), addBoundedWfAssume all_assume e'.wfCond, conditionalReturn pos (List.map (quantifyAssumptions (removeTyBound ty)) e'.assume)⟩ + | .quant .exist ty tr e => + let newAssumption := makeBoundAssumption ty; + let e' := translateBounded e [] pos; + let tr' := translateClean tr; + let all_assume := conditionalAdd pos (increaseBVars assume) e'.assume; + ⟨.quant .exist (removeTyBound ty) tr' (addAssumptions all_assume (addAndExprs newAssumption e'.translate)), addBoundedWfAssume (newAssumption ++ all_assume) e'.wfCond, conditionalReturn pos (List.map (quantifyAssumptions (removeTyBound ty)) e'.assume)⟩ + /- + For if-then-else, add assumptions to the condition, which is always bool-valued. For a bool-valued result, can add the conditions freely. For a bounded-valued term, produce a wf condition proving this. + -/ + | .ite c t f .bool => + -- c is NOT positive; equivalent to c -> t /\ ~c -> f + let c' := translateBounded c [] false; + let t' := translateBounded t [] pos; + let f' := translateBounded f [] pos; + let res := .ite (addAssumptions assume c'.translate) (addAssumptions (conditionalAdd pos assume t'.assume) t'.translate) (addAssumptions (conditionalAdd pos assume f'.assume) f'.translate) .bool; + ⟨(if pos then addAssumptions c'.assume else id) res, ListSet.union [c'.wfCond, t'.wfCond, f'.wfCond], c'.assume ++ conditionalReturn pos (t'.assume ++ f'.assume)⟩ + | .ite c t f ty => + let c' := translateBounded c [] pos; + let t' := translateBounded t assume pos; + let f' := translateBounded f assume pos; + -- here can add inside if positive, never add outside + let res := .ite (addAssumptions (conditionalAdd pos assume c'.assume) c'.translate) t'.translate f'.translate (removeTyBound ty); + ⟨res, ListSet.union [boundExprIfType ty res, c'.wfCond, t'.wfCond, f'.wfCond], conditionalReturn pos (c'.assume ++ t'.assume ++ f'.assume)⟩ + /- + Equality is always bool-valued, so can add assumptions + Equality/iff are equivalent, NOT positive + -/ + | .eq e1 e2 ty => + let e1' := translateBounded e1 [] false; + let e2' := translateBounded e2 [] false; + ⟨addAssumptions (conditionalAdd pos assume (e1'.assume ++ e2'.assume)) (.eq e1'.translate e2'.translate (removeTyBound ty)), ListSet.union [e1'.wfCond, e2'.wfCond], conditionalReturn pos (e1'.assume ++ e2'.assume)⟩ + | .mdata m e => + let e' := translateBounded e assume pos; + ⟨.mdata m e'.translate, e'.wfCond, e'.assume⟩ + +/-- +Translated an expression with bounded types to one without, preserving semantics of bool-valued terms by adding assumptions +-/ +def translateBoundedExpr [Coe String Identifier] (e: LExprT Identifier) : LExprT Identifier := + (translateBounded e [] true).translate + +/- +Many of the wf conditions have the form: forall x, f(x). We remove the quantifiers to make the SMT formulas easier to solve. +Must be stateful because we need to generate fresh variables +-/ + +-- temporary until LExpr/LExprT are unified +private def LExprT.substK (k : Nat) (s : LExprT Identifier) (e : LExprT Identifier) : LExprT Identifier := + match e with + | .const c ty => .const c ty + | .op o ty => .op o ty + | .bvar i ty => if (i == k) then s else .bvar i ty + | .fvar y ty => .fvar y ty + | .mdata info e' => .mdata info (substK k s e') + | .abs e' ty => .abs (substK (k + 1) s e') ty + | .quant qk ty tr' e' => .quant qk ty (substK (k + 1) s tr') (substK (k + 1) s e') + | .app e1 e2 ty => .app (substK k s e1) (substK k s e2) ty + | .ite c t e ty => .ite (substK k s c) (substK k s t) (substK k s e) ty + | .eq e1 e2 ty => .eq (substK k s e1) (substK k s e2) ty + +def LExprT.varOpen (k : Nat) (x : Identifier × LMonoTy) (e : LExprT Identifier) : LExprT Identifier := + LExprT.substK k (.fvar x.fst x.snd) e + +/-- +Remove leading "forall" quantifiers statefully +-/ +private def removeLeadingForall (T : TEnv Identifier) (e: LExprT Identifier) : Except Format (LExprT Identifier × TEnv Identifier) := + match e with + | .quant .all ty _ e => do + let (xv, xty, T) ← Lambda.LExprT.typeBoundVar T ty; + .ok (LExprT.varOpen 0 (xv, xty) e, T) + | _ => .ok (e, T) + +private def removeLeadingForalls (T : TEnv Identifier) (l: List (LExprT Identifier)) : Except Format (List (LExprT Identifier) × TEnv Identifier) := + List.foldlM (fun (l, T) e => + do + let (e, T') ← removeLeadingForall T e; + .ok (e :: l, T')) ([], T) l + +-- Functional version with extra quantifiers +def boundedWfConditionsQuant [Coe String Identifier] (e: LExprT Identifier) : List (LExprT Identifier) := + (translateBounded e [] true).wfCond + +-- Stateful version without extra quantifiers +def boundedWfConditions [Coe String Identifier] (T : TEnv Identifier) (e: LExprT Identifier) : Except Format (List (LExprT Identifier) × TEnv Identifier) := removeLeadingForalls T (boundedWfConditionsQuant e) + +end Bounded diff --git a/Strata/DL/Lambda/LExpr.lean b/Strata/DL/Lambda/LExpr.lean index 1d45f06a..ff5e61bb 100644 --- a/Strata/DL/Lambda/LExpr.lean +++ b/Strata/DL/Lambda/LExpr.lean @@ -322,51 +322,51 @@ scoped syntax lconstmono : lexprmono def elabLConstMono (Identifier : Type) [MkIdent Identifier] : Lean.Syntax → MetaM Expr | `(lconstmono| #$n:num) => do - let none ← mkNone (mkConst ``LMonoTy) - let typeTypeExpr := mkConst ``LMonoTy + let none ← mkNone (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit (toString n.getNat), none] | `(lconstmono| (#$n:num : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty - let typeTypeExpr := mkConst ``LMonoTy + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit (toString n.getNat), lmonoty] | `(lconstmono| #-$n:num) => do - let none ← mkNone (mkConst ``LMonoTy) - let typeTypeExpr := mkConst ``LMonoTy + let none ← mkNone (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit ("-" ++ (toString n.getNat)), none] | `(lconstmono| (#-$n:num : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty - let typeTypeExpr := mkConst ``LMonoTy + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit ("-" ++ (toString n.getNat)), lmonoty] | `(lconstmono| #true) => do - let none ← mkNone (mkConst ``LMonoTy) - let typeTypeExpr := mkConst ``LMonoTy + let none ← mkNone (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit "true", none] | `(lconstmono| (#true : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty - let typeTypeExpr := mkConst ``LMonoTy + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit "true", lmonoty] | `(lconstmono| #false) => do - let none ← mkNone (mkConst ``LMonoTy) - let typeTypeExpr := mkConst ``LMonoTy + let none ← mkNone (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit "false", none] | `(lconstmono| (#false : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty - let typeTypeExpr := mkConst ``LMonoTy + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit "false", lmonoty] | `(lconstmono| #$s:ident) => do - let none ← mkNone (mkConst ``LMonoTy) + let none ← mkNone (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) let s := toString s.getId - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit s, none] | `(lconstmono| (#$s:ident : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty let s := toString s.getId - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.const []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkStrLit s, lmonoty] | _ => throwUnsupportedSyntax @@ -377,13 +377,13 @@ scoped syntax lopmono : lexprmono def elabLOpMono (Identifier : Type) [MkIdent Identifier] : Lean.Syntax → MetaM Expr | `(lopmono| ~$s:lidentmono) => do - let none ← mkNone (mkConst ``LMonoTy) + let none ← mkNone (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) let ident ← MkIdent.elabIdent Identifier s - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.op []) #[typeTypeExpr, MkIdent.toExpr Identifier, ident, none] | `(lopmono| (~$s:lidentmono : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty mkAppM ``LExpr.op #[← MkIdent.elabIdent Identifier s, lmonoty] | _ => throwUnsupportedSyntax @@ -391,7 +391,7 @@ declare_syntax_cat lbvarmono scoped syntax "%" noWs num : lbvarmono def elabLBVarMono (Identifier : Type) [MkIdent Identifier] : Lean.Syntax → MetaM Expr | `(lbvarmono| %$n:num) => - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.bvar []) #[typeTypeExpr, MkIdent.toExpr Identifier, mkNatLit n.getNat] | _ => throwUnsupportedSyntax scoped syntax lbvarmono : lexprmono @@ -402,11 +402,11 @@ scoped syntax "(" lidentmono ":" lmonoty ")" : lfvarmono def elabLFVarMono (Identifier : Type) [MkIdent Identifier] : Lean.Syntax → MetaM Expr | `(lfvarmono| $i:lidentmono) => do - let none ← mkNone (mkConst ``LMonoTy) + let none ← mkNone (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) mkAppM ``LExpr.fvar #[← MkIdent.elabIdent Identifier i, none] | `(lfvarmono| ($i:lidentmono : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty mkAppM ``LExpr.fvar #[← MkIdent.elabIdent Identifier i, lmonoty] | _ => throwUnsupportedSyntax scoped syntax lfvarmono : lexprmono @@ -455,48 +455,48 @@ partial def elabLExprMono (Identifier : Type) [MkIdent Identifier] : Lean.Syntax | `(lexprmono| $f:lfvarmono) => elabLFVarMono Identifier f | `(lexprmono| λ $e:lexprmono) => do let e' ← elabLExprMono Identifier e - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.absUntyped []) #[typeTypeExpr, MkIdent.toExpr Identifier, e'] | `(lexprmono| λ ($mty:lmonoty): $e:lexprmono) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty let e' ← elabLExprMono Identifier e - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.abs []) #[typeTypeExpr, MkIdent.toExpr Identifier, lmonoty, e'] | `(lexprmono| ∀ $e:lexprmono) => do let e' ← elabLExprMono Identifier e - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.allUntyped []) #[typeTypeExpr, MkIdent.toExpr Identifier, e'] | `(lexprmono| ∀ {$tr}$e:lexprmono) => do let e' ← elabLExprMono Identifier e let tr' ← elabLExprMono Identifier tr - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.allUntypedTr []) #[typeTypeExpr, MkIdent.toExpr Identifier, tr', e'] | `(lexprmono| ∀ ($mty:lmonoty): $e:lexprmono) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty let e' ← elabLExprMono Identifier e - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.all []) #[typeTypeExpr, MkIdent.toExpr Identifier, lmonoty, e'] | `(lexprmono| ∀ ($mty:lmonoty):{$tr} $e:lexprmono) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty let e' ← elabLExprMono Identifier e let tr' ← elabLExprMono Identifier tr - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.allTr []) #[typeTypeExpr, MkIdent.toExpr Identifier, lmonoty, tr', e'] | `(lexprmono| ∃ ($mty:lmonoty): $e:lexprmono) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty let e' ← elabLExprMono Identifier e - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.exist []) #[typeTypeExpr, MkIdent.toExpr Identifier, lmonoty, e'] | `(lexprmono| ∃ ($mty:lmonoty):{$tr} $e:lexprmono) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty - let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty + let lmonoty ← mkSome (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) lmonoty let e' ← elabLExprMono Identifier e let tr' ← elabLExprMono Identifier tr - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.existTr []) #[typeTypeExpr, MkIdent.toExpr Identifier, lmonoty, tr', e'] | `(lexprmono| ∃ $e:lexprmono) => do let e' ← elabLExprMono Identifier e @@ -508,18 +508,18 @@ partial def elabLExprMono (Identifier : Type) [MkIdent Identifier] : Lean.Syntax | `(lexprmono| ($e1:lexprmono $e2:lexprmono)) => do let e1' ← elabLExprMono Identifier e1 let e2' ← elabLExprMono Identifier e2 - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.app []) #[typeTypeExpr, MkIdent.toExpr Identifier, e1', e2'] | `(lexprmono| $e1:lexprmono == $e2:lexprmono) => do let e1' ← elabLExprMono Identifier e1 let e2' ← elabLExprMono Identifier e2 - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.eq []) #[typeTypeExpr, MkIdent.toExpr Identifier, e1', e2'] | `(lexprmono| if $e1:lexprmono then $e2:lexprmono else $e3:lexprmono) => do let e1' ← elabLExprMono Identifier e1 let e2' ← elabLExprMono Identifier e2 let e3' ← elabLExprMono Identifier e3 - let typeTypeExpr := mkConst ``LMonoTy + let typeTypeExpr := (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) return mkAppN (.const ``LExpr.ite []) #[typeTypeExpr, MkIdent.toExpr Identifier, e1', e2', e3'] | `(lexprmono| ($e:lexprmono)) => elabLExprMono Identifier e | _ => throwUnsupportedSyntax @@ -544,7 +544,8 @@ open LTy.Syntax #guard_msgs in #check esM[((λ %0) #5)] -/-- info: (abs (some (LMonoTy.tcons "bool" [])) (bvar 0)).app (const "true" none) : LExpr LMonoTy String -/ +/-- info: (abs (some (LMonoTy.tcons BoundTyRestrict "bool" [] LTyRestrict.nodata)) (bvar 0)).app + (const "true" none) : LExpr LMonoTy String -/ #guard_msgs in #check esM[((λ (bool): %0) #true)] @@ -556,36 +557,51 @@ open LTy.Syntax #guard_msgs in #check esM[(∃ %0 == #5)] -/-- info: exist (some (LMonoTy.tcons "int" [])) ((bvar 0).eq (const "5" none)) : LExpr LMonoTy String -/ +/-- info: exist (some (LMonoTy.tcons BoundTyRestrict "int" [] LTyRestrict.nodata)) + ((bvar 0).eq (const "5" none)) : LExpr LMonoTy String-/ #guard_msgs in #check esM[(∃ (int): %0 == #5)] -/-- info: fvar "x" (some (LMonoTy.tcons "bool" [])) : LExpr LMonoTy String -/ +/-- info: fvar "x" (some (LMonoTy.tcons BoundTyRestrict "bool" [] LTyRestrict.nodata)) : LExpr LMonoTy String -/ #guard_msgs in #check esM[(x : bool)] -- axiom [updateSelect]: forall m: Map k v, kk: k, vv: v :: m[kk := vv][kk] == vv; /-- -info: all (some (LMonoTy.tcons "Map" [LMonoTy.ftvar "k", LMonoTy.ftvar "v"])) - (all (some (LMonoTy.ftvar "k")) - (all (some (LMonoTy.ftvar "v")) +info: all + (some + (LMonoTy.tcons BoundTyRestrict "Map" [LMonoTy.ftvar BoundTyRestrict "k", LMonoTy.ftvar BoundTyRestrict "v"] + LTyRestrict.nodata)) + (all (some (LMonoTy.ftvar BoundTyRestrict "k")) + (all (some (LMonoTy.ftvar BoundTyRestrict "v")) ((((op "select" (some - (LMonoTy.tcons "Map" - [LMonoTy.ftvar "k", - LMonoTy.tcons "arrow" - [LMonoTy.ftvar "v", LMonoTy.tcons "arrow" [LMonoTy.ftvar "k", LMonoTy.ftvar "v"]]]))).app + (LMonoTy.tcons BoundTyRestrict "Map" + [LMonoTy.ftvar BoundTyRestrict "k", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "v", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "k", LMonoTy.ftvar BoundTyRestrict "v"] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata))).app ((((op "update" (some - (LMonoTy.tcons "Map" - [LMonoTy.ftvar "k", - LMonoTy.tcons "arrow" - [LMonoTy.ftvar "v", - LMonoTy.tcons "arrow" - [LMonoTy.ftvar "k", - LMonoTy.tcons "arrow" - [LMonoTy.ftvar "v", - LMonoTy.tcons "Map" [LMonoTy.ftvar "k", LMonoTy.ftvar "v"]]]]]))).app + (LMonoTy.tcons BoundTyRestrict "Map" + [LMonoTy.ftvar BoundTyRestrict "k", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "v", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "k", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "v", + LMonoTy.tcons BoundTyRestrict "Map" + [LMonoTy.ftvar BoundTyRestrict "k", LMonoTy.ftvar BoundTyRestrict "v"] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata))).app (bvar 2)).app (bvar 1)).app (bvar 0))).app @@ -858,7 +874,8 @@ open LTy.Syntax #guard_msgs in #check es[((λ %0) #5)] -/-- info: (abs (some (LTy.forAll [] (LMonoTy.tcons "bool" []))) (bvar 0)).app (const "true" none) : LExpr LTy String -/ +/-- info: (abs (some (LTy.forAll [] (LMonoTy.tcons BoundTyRestrict "bool" [] LTyRestrict.nodata))) (bvar 0)).app + (const "true" none) : LExpr LTy String -/ #guard_msgs in #check es[((λ (bool): %0) #true)] @@ -870,38 +887,55 @@ open LTy.Syntax #guard_msgs in #check es[(∃ %0 == #5)] -/-- info: exist (some (LTy.forAll [] (LMonoTy.tcons "int" []))) ((bvar 0).eq (const "5" none)) : LExpr LTy String -/ +/-- info: exist (some (LTy.forAll [] (LMonoTy.tcons BoundTyRestrict "int" [] LTyRestrict.nodata))) + ((bvar 0).eq (const "5" none)) : LExpr LTy String -/ #guard_msgs in #check es[(∃ (int): %0 == #5)] -/-- info: fvar "x" (some (LTy.forAll [] (LMonoTy.tcons "bool" []))) : LExpr LTy String -/ +/-- info: fvar "x" (some (LTy.forAll [] (LMonoTy.tcons BoundTyRestrict "bool" [] LTyRestrict.nodata))) : LExpr LTy String -/ #guard_msgs in #check es[(x : bool)] -- axiom [updateSelect]: forall m: Map k v, kk: k, vv: v :: m[kk := vv][kk] == vv; /-- -info: all (some (LTy.forAll [] (LMonoTy.tcons "Map" [LMonoTy.ftvar "k", LMonoTy.ftvar "v"]))) - (all (some (LTy.forAll [] (LMonoTy.ftvar "k"))) - (all (some (LTy.forAll [] (LMonoTy.ftvar "v"))) +info: all + (some + (LTy.forAll [] + (LMonoTy.tcons BoundTyRestrict "Map" [LMonoTy.ftvar BoundTyRestrict "k", LMonoTy.ftvar BoundTyRestrict "v"] + LTyRestrict.nodata))) + (all (some (LTy.forAll [] (LMonoTy.ftvar BoundTyRestrict "k"))) + (all (some (LTy.forAll [] (LMonoTy.ftvar BoundTyRestrict "v"))) ((((op "select" (some (LTy.forAll [] - (LMonoTy.tcons "Map" - [LMonoTy.ftvar "k", - LMonoTy.tcons "arrow" - [LMonoTy.ftvar "v", LMonoTy.tcons "arrow" [LMonoTy.ftvar "k", LMonoTy.ftvar "v"]]])))).app + (LMonoTy.tcons BoundTyRestrict "Map" + [LMonoTy.ftvar BoundTyRestrict "k", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "v", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "k", LMonoTy.ftvar BoundTyRestrict "v"] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata)))).app ((((op "update" (some (LTy.forAll [] - (LMonoTy.tcons "Map" - [LMonoTy.ftvar "k", - LMonoTy.tcons "arrow" - [LMonoTy.ftvar "v", - LMonoTy.tcons "arrow" - [LMonoTy.ftvar "k", - LMonoTy.tcons "arrow" - [LMonoTy.ftvar "v", - LMonoTy.tcons "Map" [LMonoTy.ftvar "k", LMonoTy.ftvar "v"]]]]])))).app + (LMonoTy.tcons BoundTyRestrict "Map" + [LMonoTy.ftvar BoundTyRestrict "k", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "v", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "k", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "v", + LMonoTy.tcons BoundTyRestrict "Map" + [LMonoTy.ftvar BoundTyRestrict "k", + LMonoTy.ftvar BoundTyRestrict "v"] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata)))).app (bvar 2)).app (bvar 1)).app (bvar 0))).app diff --git a/Strata/DL/Lambda/LExprTypeEnv.lean b/Strata/DL/Lambda/LExprTypeEnv.lean index 717229c6..75724987 100644 --- a/Strata/DL/Lambda/LExprTypeEnv.lean +++ b/Strata/DL/Lambda/LExprTypeEnv.lean @@ -454,7 +454,7 @@ def LMonoTy.aliasDef? (mty : LMonoTy) (T : (TEnv Identifier)) : (Option LMonoTy | .bitvec _ => -- A bitvector cannot be a type alias. (none, T) - | .tcons name args => + | .tcons name args r => match T.context.aliases.find? (fun a => a.name == name && a.typeArgs.length == args.length) with | none => (none, T) | some alias => @@ -568,11 +568,11 @@ partial def LMonoTy.resolveAliases (mty : LMonoTy) (T : TEnv Identifier) : (Opti match mty with | .ftvar _ => (some mty, T) | .bitvec _ => (some mty, T) - | .tcons name mtys => + | .tcons name mtys r => let (maybe_mtys, T) := LMonoTys.resolveAliases mtys T.context.aliases T match maybe_mtys with | none => (none, T) - | some mtys' => (some (.tcons name mtys'), T) + | some mtys' => (some (.tcons name mtys' r), T) /-- De-alias `mtys`, including at the subtrees. @@ -637,7 +637,7 @@ de-aliased. def LMonoTy.knownInstance (ty : LMonoTy) (ks : KnownTypes) : Bool := match ty with | .ftvar _ | .bitvec _ => true - | .tcons name args => + | .tcons name args _ => (ks.contains { name := name, arity := args.length }) && LMonoTys.knownInstances args ks diff --git a/Strata/DL/Lambda/LTy.lean b/Strata/DL/Lambda/LTy.lean index f033f8c2..90842bbe 100644 --- a/Strata/DL/Lambda/LTy.lean +++ b/Strata/DL/Lambda/LTy.lean @@ -25,21 +25,62 @@ abbrev TyIdentifier := String instance : Coe String TyIdentifier where coe := id +/-- +Bounded integer expressions: the grammar allows expressions like +a <= b /\ b < c, where a, b, and c are integer constants or a (single) variable. This lets us express types like {x | 0 <= x < 2^32} +-/ +inductive BoundVal : Type where + /-- The bounded variable -/ + | bvar + /-- Integer constants -/ + | bconst (val: Int) +deriving Inhabited, Repr, DecidableEq + +inductive BoundExpr : Type where + /-- b1 = b2 -/ + | beq (b1 b2: BoundVal) + /-- b1 < b2 -/ + | blt (e1 e2: BoundVal) + /-- b1 <= b2 -/ + | ble (e1 e2: BoundVal) + /-- e1 /\ e2 -/ + | band (e1 e2: BoundExpr) + /-- not e -/ + | bnot (e: BoundExpr) +deriving Inhabited, Repr, DecidableEq + +/- +An additional parameter that restricts the values of a type +or attaches additional metadata to a type. +-/ +inductive BoundTyRestrict : Type where + /-- Bounded integers -/ + | bounddata (b: BoundExpr) +deriving Inhabited, Repr, DecidableEq + +inductive LTyRestrict (ExtraRestrict : Type) : Type where + /-- Special support for bitvector types of every size. -/ + | bitvecdata (size: Nat) + | extradata (e: ExtraRestrict) + | nodata +deriving Inhabited, Repr, DecidableEq + /-- Types in Lambda: these are mono-types. Note that all free type variables (`.ftvar`) are implicitly universally quantified. -/ -inductive LMonoTy : Type where +inductive LMonoTy (ExtraRestrict: Type := BoundTyRestrict) : Type where /-- Type variable. -/ | ftvar (name : TyIdentifier) /-- Type constructor. -/ - | tcons (name : String) (args : List LMonoTy) - /-- Special support for bitvector types of every size. -/ - | bitvec (size : Nat) + | tcons (name : String) (args : List (LMonoTy ExtraRestrict)) (r: LTyRestrict ExtraRestrict := by exact .nodata) deriving Inhabited, Repr abbrev LMonoTys := List LMonoTy +@[match_pattern] +def LMonoTy.bitvec (n: Nat) : LMonoTy := LMonoTy.tcons "bitvec" [] (LTyRestrict.bitvecdata n) + @[match_pattern] def LMonoTy.bool : LMonoTy := .tcons "bool" [] @@ -52,6 +93,10 @@ def LMonoTy.int : LMonoTy := def LMonoTy.real : LMonoTy := .tcons "real" [] +@[match_pattern] +def LMonoTy.bounded (b: BoundExpr) : LMonoTy := + .tcons "int" [] (.extradata (.bounddata b)) + @[match_pattern] def LMonoTy.bv1 : LMonoTy := .bitvec 1 @@ -124,10 +169,9 @@ Lean's default `induction` tactic does not support nested or mutual inductive types. So we define our own induction principle below. -/ @[induction_eliminator] -theorem LMonoTy.induct {P : LMonoTy → Prop} +theorem LMonoTy.induct {R: Type} {P : LMonoTy R → Prop} (ftvar : ∀f, P (.ftvar f)) - (bitvec : ∀n, P (.bitvec n)) - (tcons : ∀name args, (∀ ty ∈ args, P ty) → P (.tcons name args)) : + (tcons : ∀name args r, (∀ ty ∈ args, P ty) → P (.tcons name args r)) : ∀ ty, P ty := by intro n apply LMonoTy.rec <;> try assumption @@ -144,8 +188,7 @@ Compute the size of `ty` as a tree. def LMonoTy.size (ty : LMonoTy) : Nat := match ty with | .ftvar _ => 1 - | .tcons _ args => 1 + LMonoTys.size args - | .bitvec _ => 1 + | .tcons _ args _ => 1 + LMonoTys.size args def LMonoTys.size (args : LMonoTys) : Nat := match args with @@ -165,9 +208,8 @@ Boolean equality for `LMonoTy`. def LMonoTy.BEq (x y : LMonoTy) : Bool := match x, y with | .ftvar i, .ftvar j => i == j - | .bitvec i, .bitvec j => i == j - | .tcons i1 j1, .tcons i2 j2 => - i1 == i2 && j1.length == j2.length && go j1 j2 + | .tcons i1 j1 r1, .tcons i2 j2 r2 => + i1 == i2 && j1.length == j2.length && r1 == r2 && go j1 j2 | _, _ => false where go j1 j2 := match j1, j2 with @@ -179,7 +221,7 @@ def LMonoTy.BEq (x y : LMonoTy) : Bool := @[simp] theorem LMonoTy.BEq_refl : LMonoTy.BEq ty ty := by induction ty <;> simp_all [LMonoTy.BEq] - rename_i name args ih + rename_i name args r ih induction args case tcons.nil => simp [LMonoTy.BEq.go] case tcons.cons => @@ -194,13 +236,11 @@ instance : DecidableEq LMonoTy := induction x generalizing y case ftvar => unfold LMonoTy.BEq at h <;> split at h <;> try simp_all - case bitvec => - unfold LMonoTy.BEq at h <;> split at h <;> try simp_all case tcons => - rename_i name args ih + rename_i name args r ih cases y <;> try simp_all [LMonoTy.BEq] - rename_i name' args' - obtain ⟨⟨h1, h2⟩, h3⟩ := h + rename_i name' args' r' + obtain ⟨⟨⟨h1, h2⟩, _⟩, h3⟩ := h induction args generalizing args' case nil => unfold List.length at h2; split at h2 <;> simp_all case cons head' tail' ih' => @@ -213,11 +253,9 @@ instance : DecidableEq LMonoTy := isFalse (by induction x generalizing y case ftvar => cases y <;> try simp_all [LMonoTy.BEq] - case bitvec n => + case tcons name args r ih => cases y <;> try simp_all [LMonoTy.BEq] - case tcons name args ih => - cases y <;> try simp_all [LMonoTy.BEq] - rename_i name' args' + rename_i name' args' r' intro hname; simp [hname] at h induction args generalizing args' case tcons.nil => @@ -244,8 +282,7 @@ it. def LMonoTy.freeVars (mty : LMonoTy) : List TyIdentifier := match mty with | .ftvar x => [x] - | .bitvec _ => [] - | .tcons _ ltys => LMonoTys.freeVars ltys + | .tcons _ ltys _ => LMonoTys.freeVars ltys /-- Get the free type variables in monotypes `mtys`, which are simply the `.ftvar`s @@ -268,7 +305,7 @@ def LMonoTy.getTyConstructors (mty : LMonoTy) : List LMonoTy := match mty with | .ftvar _ => [] | .bitvec _ => [] - | .tcons name mtys => + | .tcons name mtys _ => let typeargs := List.replicate mtys.length "_dummy" let args := typeargs.mapIdx (fun i elem => LMonoTy.ftvar (elem ++ toString i)) let mty := .tcons name args @@ -279,10 +316,13 @@ def LMonoTy.getTyConstructors (mty : LMonoTy) : List LMonoTy := | [] => [] | m :: mrest => LMonoTy.getTyConstructors m ++ go mrest /-- -info: [Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.ftvar "_dummy0", Lambda.LMonoTy.ftvar "_dummy1"], - Lambda.LMonoTy.tcons "bool" [], - Lambda.LMonoTy.tcons "foo" [Lambda.LMonoTy.ftvar "_dummy0"], - Lambda.LMonoTy.tcons "a" [Lambda.LMonoTy.ftvar "_dummy0", Lambda.LMonoTy.ftvar "_dummy1"]] +info: [Lambda.LMonoTy.tcons + "arrow" + [Lambda.LMonoTy.ftvar "_dummy0", Lambda.LMonoTy.ftvar "_dummy1"] + (Lambda.LTyRestrict.nodata), + Lambda.LMonoTy.tcons "bool" [] (Lambda.LTyRestrict.nodata), + Lambda.LMonoTy.tcons "foo" [Lambda.LMonoTy.ftvar "_dummy0"] (Lambda.LTyRestrict.nodata), + Lambda.LMonoTy.tcons "a" [Lambda.LMonoTy.ftvar "_dummy0", Lambda.LMonoTy.ftvar "_dummy1"] (Lambda.LTyRestrict.nodata)] -/ #guard_msgs in #eval LMonoTy.getTyConstructors @@ -356,7 +396,7 @@ private def formatLMonoTy (lmonoty : LMonoTy) : Format := match lmonoty with | .ftvar x => toString x | .bitvec n => f!"bv{n}" - | .tcons name tys => + | .tcons name tys _ => if tys.isEmpty then f!"{name}" else @@ -408,18 +448,18 @@ scoped syntax "(" lmonoty ")" : lmonoty open Lean Elab Meta in partial def elabLMonoTy : Lean.Syntax → MetaM Expr | `(lmonoty| %$f:ident) => do - mkAppM ``LMonoTy.ftvar #[mkStrLit (toString f.getId)] + mkAppOptM ``LMonoTy.ftvar #[mkConst `Lambda.BoundTyRestrict, mkStrLit (toString f.getId)] | `(lmonoty| $ty1:lmonoty → $ty2:lmonoty) => do let ty1' ← elabLMonoTy ty1 let ty2' ← elabLMonoTy ty2 - let tys ← mkListLit (mkConst ``LMonoTy) [ty1', ty2'] - mkAppM ``LMonoTy.tcons #[(mkStrLit "arrow"), tys] + let tys ← mkListLit (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) [ty1', ty2'] + mkAppM ``LMonoTy.tcons #[(mkStrLit "arrow"), tys, (.app (mkConst `Lambda.LTyRestrict.nodata) (mkConst `Lambda.BoundTyRestrict))] | `(lmonoty| int) => do - let argslist ← mkListLit (mkConst ``LMonoTy) [] - mkAppM ``LMonoTy.tcons #[(mkStrLit "int"), argslist] + let argslist ← mkListLit (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) [] + mkAppM ``LMonoTy.tcons #[(mkStrLit "int"), argslist, (.app (mkConst `Lambda.LTyRestrict.nodata) (mkConst `Lambda.BoundTyRestrict))] | `(lmonoty| bool) => do - let argslist ← mkListLit (mkConst ``LMonoTy) [] - mkAppM ``LMonoTy.tcons #[(mkStrLit "bool"), argslist] + let argslist ← mkListLit (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) [] + mkAppM ``LMonoTy.tcons #[(mkStrLit "bool"), argslist, (.app (mkConst `Lambda.LTyRestrict.nodata) (mkConst `Lambda.BoundTyRestrict))] | `(lmonoty| bv1) => mkAppM ``LMonoTy.bv1 #[] | `(lmonoty| bv8) => mkAppM ``LMonoTy.bv8 #[] | `(lmonoty| bv16) => mkAppM ``LMonoTy.bv16 #[] @@ -427,8 +467,8 @@ partial def elabLMonoTy : Lean.Syntax → MetaM Expr | `(lmonoty| bv64) => mkAppM ``LMonoTy.bv64 #[] | `(lmonoty| $i:ident $args:lmonoty*) => do let args' ← go args - let argslist ← mkListLit (mkConst ``LMonoTy) args'.toList - mkAppM ``LMonoTy.tcons #[(mkStrLit (toString i.getId)), argslist] + let argslist ← mkListLit (.app (mkConst ``LMonoTy) (mkConst `Lambda.BoundTyRestrict)) args'.toList + mkAppM ``LMonoTy.tcons #[(mkStrLit (toString i.getId)), argslist, (.app (mkConst `Lambda.LTyRestrict.nodata) (mkConst `Lambda.BoundTyRestrict))] | `(lmonoty| ($ty:lmonoty)) => elabLMonoTy ty | _ => throwUnsupportedSyntax where go (args : TSyntaxArray `lmonoty) : MetaM (Array Expr) := do @@ -440,26 +480,38 @@ partial def elabLMonoTy : Lean.Syntax → MetaM Expr elab "mty[" ty:lmonoty "]" : term => elabLMonoTy ty -/-- info: LMonoTy.tcons "list" [LMonoTy.tcons "int" []] : LMonoTy -/ +/-- info: LMonoTy.tcons BoundTyRestrict "list" [LMonoTy.tcons BoundTyRestrict "int" [] LTyRestrict.nodata] + LTyRestrict.nodata : LMonoTy -/ #guard_msgs in #check mty[list int] -/-- info: LMonoTy.tcons "pair" [LMonoTy.tcons "int" [], LMonoTy.tcons "bool" []] : LMonoTy -/ +/-- info: LMonoTy.tcons BoundTyRestrict "pair" + [LMonoTy.tcons BoundTyRestrict "int" [] LTyRestrict.nodata, + LMonoTy.tcons BoundTyRestrict "bool" [] LTyRestrict.nodata] + LTyRestrict.nodata : LMonoTy -/ #guard_msgs in #check mty[pair int bool] /-- -info: LMonoTy.tcons "arrow" - [LMonoTy.tcons "Map" [LMonoTy.ftvar "k", LMonoTy.ftvar "v"], - LMonoTy.tcons "arrow" [LMonoTy.ftvar "k", LMonoTy.ftvar "v"]] : LMonoTy +info: LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.tcons BoundTyRestrict "Map" [LMonoTy.ftvar BoundTyRestrict "k", LMonoTy.ftvar BoundTyRestrict "v"] + LTyRestrict.nodata, + LMonoTy.tcons BoundTyRestrict "arrow" [LMonoTy.ftvar BoundTyRestrict "k", LMonoTy.ftvar BoundTyRestrict "v"] + LTyRestrict.nodata] + LTyRestrict.nodata : LMonoTy -/ #guard_msgs in #check mty[(Map %k %v) → %k → %v] /-- -info: LMonoTy.tcons "arrow" - [LMonoTy.ftvar "a", - LMonoTy.tcons "arrow" [LMonoTy.ftvar "b", LMonoTy.tcons "arrow" [LMonoTy.ftvar "c", LMonoTy.ftvar "d"]]] : LMonoTy +info: LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "a", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "b", + LMonoTy.tcons BoundTyRestrict "arrow" [LMonoTy.ftvar BoundTyRestrict "c", LMonoTy.ftvar BoundTyRestrict "d"] + LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata : LMonoTy -/ #guard_msgs in #check mty[%a → %b → %c → %d] @@ -485,13 +537,18 @@ partial def elabLTy : Lean.Syntax → MetaM Expr elab "t[" lsch:lty "]" : term => elabLTy lsch -/-- info: forAll ["α"] (LMonoTy.tcons "myType" [LMonoTy.ftvar "α"]) : LTy -/ +/-- info: forAll ["α"] (LMonoTy.tcons BoundTyRestrict "myType" [LMonoTy.ftvar BoundTyRestrict "α"] LTyRestrict.nodata) : LTy -/ #guard_msgs in #check t[∀α. myType %α] /-- info: forAll ["α"] - (LMonoTy.tcons "arrow" [LMonoTy.ftvar "α", LMonoTy.tcons "arrow" [LMonoTy.ftvar "α", LMonoTy.tcons "int" []]]) : LTy + (LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "α", + LMonoTy.tcons BoundTyRestrict "arrow" + [LMonoTy.ftvar BoundTyRestrict "α", LMonoTy.tcons BoundTyRestrict "int" [] LTyRestrict.nodata] + LTyRestrict.nodata] + LTyRestrict.nodata) : LTy -/ #guard_msgs in #check t[∀α. %α → %α → int] diff --git a/Strata/DL/Lambda/LTyUnify.lean b/Strata/DL/Lambda/LTyUnify.lean index 07a4081d..9d8a3783 100644 --- a/Strata/DL/Lambda/LTyUnify.lean +++ b/Strata/DL/Lambda/LTyUnify.lean @@ -160,9 +160,8 @@ def LMonoTy.subst (S : Subst) (mty : LMonoTy) : LMonoTy := match mty with | .ftvar x => match S.find? x with | some sty => sty | none => mty - | .bitvec _ => mty - | .tcons name ltys => - .tcons name (LMonoTys.subst S ltys) + | .tcons name ltys r => + .tcons name (LMonoTys.subst S ltys) r /-- Apply substitution `S` to monotypes `mtys`. -/ @@ -249,11 +248,7 @@ theorem LMonoTy.subst_keys_not_in_substituted_type (h : SubstWF S) : have := @Maps.find?_of_not_mem_values _ _ i _ S simp_all exact ne_of_mem_of_not_mem hid this - case bitvec n => - simp_all [LMonoTy.subst] - unfold LMonoTy.freeVars - simp - case tcons name args h1 => + case tcons name args r h1 => simp_all simp [subst] induction args @@ -292,9 +287,7 @@ theorem LMonoTy.freeVars_of_subst_subset (S : Subst) (mty : LMonoTy) : apply @Maps.find?_mem_values _ _ x sty _ S h_find · -- Case: S.find? x = none simp [freeVars] - case bitvec n => - simp [subst] - case tcons name args ih => + case tcons name args r ih => simp [LMonoTy.subst, LMonoTy.freeVars] induction args case nil => @@ -1065,20 +1058,20 @@ def Constraint.unifyOne (c : Constraint) (S : SubstInfo) : .ok { newS := SubstInfo.mk [] (by simp [SubstWF]), goodSubset := by grind } else .error f!"Cannot unify differently sized bitvector types {t1} and {t2}!" - | .tcons name1 args1, .tcons name2 args2 => do + | .bitvec _, .tcons _ _ _ => + .error f!"Cannot unify bv type {t1} and type constructor {t2}!" + | .tcons _ _ _, .bitvec _ => + .error f!"Cannot unify type constructor {t1} and bv type {t2}!" + | .tcons name1 args1 r1, .tcons name2 args2 r2 => do if _h6 : name1 == name2 && args1.length == args2.length then let new_constraints := List.zip args1 args2 let relS ← Constraints.unifyCore new_constraints S have h_sub : Subst.freeVars_subset_prop - [(LMonoTy.tcons name1 args1, LMonoTy.tcons name2 args2)] relS.newS S := by + [(LMonoTy.tcons name1 args1 r1, LMonoTy.tcons name2 args2 r2)] relS.newS S := by exact Subst.freeVars_subset_prop_of_tcons S name1 name2 args1 args2 rfl relS .ok { newS := relS.newS, goodSubset := by simp [h_sub] } else .error f!"Cannot unify differently named type constructors {t1} and {t2}!" - | .bitvec _, .tcons _ _ => - .error f!"Cannot unify bv type {t1} and type constructor {t2}!" - | .tcons _ _, .bitvec _ => - .error f!"Cannot unify type constructor {t1} and bv type {t2}!" termination_by ((((Constraints.freeVars [c]) ++ S.subst.freeVars).dedup.length), Constraints.size [c], 0) diff --git a/Strata/Languages/Boogie/Examples/DDMAxiomsExtraction.lean b/Strata/Languages/Boogie/Examples/DDMAxiomsExtraction.lean index bd17a8ca..9ac2f236 100644 --- a/Strata/Languages/Boogie/Examples/DDMAxiomsExtraction.lean +++ b/Strata/Languages/Boogie/Examples/DDMAxiomsExtraction.lean @@ -239,7 +239,7 @@ info: #[{ name := { dialect := "Boogie", name := "command_typedecl" }, /-- info: [Lambda.LExpr.quant (Lambda.QuantifierKind.all) - (some (Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"])) + (some (Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] (Lambda.LTyRestrict.nodata))) (Lambda.LExpr.bvar 0) (Lambda.LExpr.quant (Lambda.QuantifierKind.all) @@ -256,8 +256,15 @@ info: [Lambda.LExpr.quant u:select (some (Lambda.LMonoTy.tcons "arrow" - [Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"], - Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"]]))) + [Lambda.LMonoTy.tcons + "Map" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata), + Lambda.LMonoTy.tcons + "arrow" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)))) (Lambda.LExpr.app (Lambda.LExpr.app (Lambda.LExpr.app @@ -265,14 +272,23 @@ info: [Lambda.LExpr.quant u:update (some (Lambda.LMonoTy.tcons "arrow" - [Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"], + [Lambda.LMonoTy.tcons + "Map" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata), Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.ftvar "v", - Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"]]]]))) + Lambda.LMonoTy.tcons + "Map" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)))) (Lambda.LExpr.bvar 2)) (Lambda.LExpr.bvar 1)) (Lambda.LExpr.bvar 0))) @@ -280,7 +296,7 @@ info: [Lambda.LExpr.quant (Lambda.LExpr.bvar 0)))), Lambda.LExpr.quant (Lambda.QuantifierKind.all) - (some (Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"])) + (some (Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] (Lambda.LTyRestrict.nodata))) (Lambda.LExpr.bvar 0) (Lambda.LExpr.quant (Lambda.QuantifierKind.all) @@ -301,8 +317,15 @@ info: [Lambda.LExpr.quant u:select (some (Lambda.LMonoTy.tcons "arrow" - [Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"], - Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"]]))) + [Lambda.LMonoTy.tcons + "Map" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata), + Lambda.LMonoTy.tcons + "arrow" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)))) (Lambda.LExpr.app (Lambda.LExpr.app (Lambda.LExpr.app @@ -310,14 +333,23 @@ info: [Lambda.LExpr.quant u:update (some (Lambda.LMonoTy.tcons "arrow" - [Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"], + [Lambda.LMonoTy.tcons + "Map" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata), Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.ftvar "v", - Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"]]]]))) + Lambda.LMonoTy.tcons + "Map" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)))) (Lambda.LExpr.bvar 3)) (Lambda.LExpr.bvar 1)) (Lambda.LExpr.bvar 0))) @@ -328,8 +360,15 @@ info: [Lambda.LExpr.quant u:select (some (Lambda.LMonoTy.tcons "arrow" - [Lambda.LMonoTy.tcons "Map" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"], - Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"]]))) + [Lambda.LMonoTy.tcons + "Map" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata), + Lambda.LMonoTy.tcons + "arrow" + [Lambda.LMonoTy.ftvar "k", Lambda.LMonoTy.ftvar "v"] + (Lambda.LTyRestrict.nodata)] + (Lambda.LTyRestrict.nodata)))) (Lambda.LExpr.bvar 3)) (Lambda.LExpr.bvar 2))))))] -/ diff --git a/Strata/Languages/Boogie/Identifiers.lean b/Strata/Languages/Boogie/Identifiers.lean index 298edd68..a2517fc9 100644 --- a/Strata/Languages/Boogie/Identifiers.lean +++ b/Strata/Languages/Boogie/Identifiers.lean @@ -141,7 +141,9 @@ info: (Lambda.LExpr.op (BoogieIdent.unres "old") none).app open Lambda.LTy.Syntax in /-- info: Lambda.LExpr.fvar (BoogieIdent.unres "x") - (some (Lambda.LMonoTy.tcons "bool" [])) : Lambda.LExpr Lambda.LMonoTy (Visibility × String) -/ + (some + (Lambda.LMonoTy.tcons Lambda.BoundTyRestrict "bool" [] + Lambda.LTyRestrict.nodata)) : Lambda.LExpr Lambda.LMonoTy (Visibility × String) -/ #guard_msgs in #check eb[(x : bool)] diff --git a/Strata/Languages/Boogie/SMTEncoder.lean b/Strata/Languages/Boogie/SMTEncoder.lean index 8c25cd5d..887d9a4b 100644 --- a/Strata/Languages/Boogie/SMTEncoder.lean +++ b/Strata/Languages/Boogie/SMTEncoder.lean @@ -87,12 +87,12 @@ mutual def LMonoTy.toSMTType (ty : LMonoTy) (ctx : SMT.Context) : Except Format (TermType × SMT.Context) := do match ty with - | .bitvec n => .ok (.bitvec n, ctx) - | .tcons "bool" [] => .ok (.bool, ctx) - | .tcons "int" [] => .ok (.int, ctx) - | .tcons "real" [] => .ok (.real, ctx) - | .tcons "string" [] => .ok (.string, ctx) - | .tcons id args => + | .bitvec n => .ok (TermType.bitvec n, ctx) + | .tcons "bool" [] _ => .ok (.bool, ctx) + | .tcons "int" [] _ => .ok (.int, ctx) + | .tcons "real" [] _ => .ok (.real, ctx) + | .tcons "string" [] _ => .ok (.string, ctx) + | .tcons id args _ => let ctx := ctx.addSort { name := id, arity := args.length } let (args', ctx) ← LMonoTys.toSMTType args ctx .ok ((.constr id args'), ctx) diff --git a/StrataTest/DL/Bounded/BExprTest.lean b/StrataTest/DL/Bounded/BExprTest.lean new file mode 100644 index 00000000..f887e84b --- /dev/null +++ b/StrataTest/DL/Bounded/BExprTest.lean @@ -0,0 +1,1074 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.DL.Bounded.BExpr +import Strata.DL.Lambda.LExprT +import Strata.DL.Lambda.LTy + +-- Tests for Bounded Expressions + +namespace Test +open Std (ToFormat Format format) +open Lambda +open Bounded + +def natTy : LMonoTy := LMonoTy.bounded (.ble (.bconst 0) .bvar) + +def leOp (e1 e2: LExprT String) : LExprT String := .app (.app (LFunc.opExprT intLeFunc) e1 (.arrow .int .bool)) e2 .bool + +def geOp (e1 e2: LExprT String) : LExprT String := .app (.app (LFunc.opExprT intGeFunc) e1 (.arrow .int .bool)) e2 .bool + +def addOp (e1 e2: LExprT String) : LExprT String := .app (.app (LFunc.opExprT intAddFunc) e1 (.arrow .int .int)) e2 .int + +def mulOp (e1 e2: LExprT String) : LExprT String := .app (.app (LFunc.opExprT intMulFunc) e1 (.arrow .int .int)) e2 .int + +def notOp (e: LExprT String) : LExprT String := .app (LFunc.opExprT boolNotFunc) e .bool + +-- easier to read without huge type ASTs +def eraseTy (x: LExprT String) := + LExpr.eraseTypes (LExprT.toLExpr x) + +def eraseTys l := List.map eraseTy l + +namespace TranslateTest + +-- 1. ∀ (x: Nat), 0 <= x (quantified assumption) +-- Expected: ∀ (x: int), 0 <= x -> 0 <= x + +def testQuantAssume := (@LExprT.quant String .all natTy (.bvar 0 natTy) (leOp (.const "0" .int) (.bvar 0 .int))) + +/-- info: Lambda.LExpr.quant + (Lambda.QuantifierKind.all) + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.bvar 0) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0))) + -/ +#guard_msgs in +#eval (eraseTy (translateBoundedExpr testQuantAssume) ) + +-- 2. λ(x: Nat), if 0 <= x then 1 else 2 (assumption inside ite) +-- Expected: λ (x: int), if 0 <= x -> 0 <= x then 1 else 2 + +def testAssumeIte : LExprT String := .abs (.ite (leOp (.const "0" .int) (.bvar 0 .int)) (.const "1" .int) (.const "2" .int) .int) (.arrow natTy .int) + +/-- info: Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.ite + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "1" none) + (Lambda.LExpr.const "2" none))-/ +#guard_msgs in +#eval (eraseTy (translateBoundedExpr testAssumeIte)) + +-- 3. λ(x: int), if foo x >= 0 then 1 else 0 (for foo: int -> Nat) (propagate op/application information) +-- Expected: λ (x: int), if 0 <= foo x -> foo x >= 0 then 1 else 0 + +def testAppAssume : LExprT String := .abs (.ite (geOp (.app (.op "foo" (.arrow .int natTy)) (.bvar 0 .int) natTy) (.const "0" .int)) (.const "1" .int) (.const "0" .int) .int) (.arrow .int .int) + +/-- info: Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.ite + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Ge" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "0" none))) + (Lambda.LExpr.const "1" none) + (Lambda.LExpr.const "0" none))-/ +#guard_msgs in +#eval (eraseTy (translateBoundedExpr testAppAssume)) + +-- 4. (x: Nat) + (y: Nat) >= 0 (free variable bounds) +-- Expected: 0 <= (x: int) -> 0 <= (y : int) -> x + y >= 0 + +def testFreeVar : LExprT String := geOp (addOp (.fvar "x" natTy) (.fvar "y" natTy)) (.const "0" .int) + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "x" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "y" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Ge" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Add" none) (Lambda.LExpr.fvar "x" none)) + (Lambda.LExpr.fvar "y" none))) + (Lambda.LExpr.const "0" none)))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testFreeVar) + +-- 5. λ (x: Nat). λ (y: Nat). x + y >= 0 (multiple bound vars) +-- Expected: λ (x: int). λ (y: int). 0 <= y -> 0 <= x -> x + y >= 0 + +def testMultiBvar : LExprT String := .abs (.abs (geOp (addOp (.bvar 1 .int) (.bvar 0 .int)) (.const "0" .int)) (.arrow natTy .bool)) (.arrow natTy (.arrow natTy .bool)) + +/-- info: Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 1))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Ge" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Add" none) (Lambda.LExpr.bvar 1)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "0" none)))))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testMultiBvar) + +-- 6. λ (x: Nat), if foo then λ (y: Nat). not (x = -1) else λ (y: Nat). x + y >= 0 (propagate inside branches of if-then-else) +--Expected: λ (x: int), if 0 <= x -> foo then λ (y: int), 0 <= y -> 0 <= x -> not (x = -1) else λ (y: int). 0 <= y -> 0 <= x -> x + y >= 0 + +def testBranchIte : LExprT String := .abs (.ite (.op "foo" .bool) (.abs (notOp (.eq (.bvar 1 .int) (.const "-1" .int) .bool)) (.arrow natTy .bool)) (.abs (geOp (addOp (.bvar 1 .int) (.bvar 0 .int)) (.const "0" .int)) (.arrow natTy .bool)) (.arrow natTy .bool)) (.arrow natTy (.arrow natTy .bool)) + +/-- info: Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.ite + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.op "foo" none)) + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 1))) + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Not" none) + (Lambda.LExpr.eq (Lambda.LExpr.bvar 1) (Lambda.LExpr.const "-1" none)))))) + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 1))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Ge" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Add" none) (Lambda.LExpr.bvar 1)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "0" none))))))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testBranchIte) + +end TranslateTest + +-- Tests for wf conditions + +-- For these tests, we initialize with an empty TEnv +def runWFTest (e: LExprT String) := do + let (l, _) ← boundedWfConditions TEnv.default e; + .ok (eraseTys l) + +namespace WFTest + +-- 1. constant: (1: Nat) +-- Expected: 0 <= 1 + +def testWfConst : LExprT String := .const "1" natTy + +/--info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.const "1" none)] + -/ +#guard_msgs in +#eval runWFTest testWfConst + +-- 2. application: (λ x: Nat. x) 1 +-- Expected: 0 <= 1 + +def testWfApp : LExprT String := .app (.abs (.bvar 0 .int) (.arrow natTy .int)) (.const "1" .int) .int + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.const "1" none)]-/ +#guard_msgs in +#eval runWFTest testWfApp + +-- 3. application with assumption (bottom up): (λ x: Nat. x) (foo : Nat) +-- Expected: 0 <= foo -> 0 <= foo + +def testWfAppAssume1 : LExprT String := .app (.abs (.bvar 0 .int) (.arrow natTy .int)) (.op "foo" natTy) .int + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.op "foo" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.op "foo" none))]-/ +#guard_msgs in +#eval runWFTest testWfAppAssume1 + +-- 4. application with assumption (top down): (λ x: Nat. (λ y: Nat. y) x) +-- Expected: 0 <= x -> 0 <= x (no quantifiers) + +def testWfAppAssume2 : LExprT String := .abs (.app (.abs (.bvar 0 .int) (.arrow natTy .int)) (.bvar 0 .int) .int) (.arrow natTy .int) + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var0" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var0" none))]-/ +#guard_msgs in +#eval runWFTest testWfAppAssume2 + +-- 5. abstraction with assumption: (λ x: Nat. foo (x + 1)) (foo: Nat -> int) +-- Expected: 0 <= x -> 0 <= x + 1 + +def testWfAbs : LExprT String := .abs (.app (.op "foo" (.arrow natTy .int)) (addOp (.bvar 0 .int) (.const "1" .int)) .int) (.arrow natTy .int) + +/--info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var0" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Add" none) (Lambda.LExpr.fvar "$__var0" none)) + (Lambda.LExpr.const "1" none)))]-/ +#guard_msgs in +#eval runWFTest testWfAbs + +-- 6. quantified assumption: (∃ x: Nat. foo x) where (foo: Nat -> int) +-- Expected: 0 <= x -> 0 <= x + +def testWfQuantAssume : LExprT String := .quant .exist natTy (.bvar 0 .int) (.app (.op "foo" (.arrow natTy .int)) (.bvar 0 .int) .int) + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var0" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var0" none))]-/ +#guard_msgs in +#eval runWFTest testWfQuantAssume + +-- 7. Lambda with bounded body (λ x: Nat. (x + 1: Nat)) +-- Expected: 0 <= x -> 0 <= x + 1 + +def testWfAbsBody : LExprT String := .abs (addOp (.bvar 0 .int) (.const "1" .int)) (.arrow natTy natTy) + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var0" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Add" none) (Lambda.LExpr.fvar "$__var0" none)) + (Lambda.LExpr.const "1" none)))]-/ +#guard_msgs in +#eval runWFTest testWfAbsBody + + +-- 8. Application with bounded body: (foo x) : Nat where foo: int -> Nat +-- Expected: [] (foo assumed) + +def testWfBoundBody : LExprT String := .app (.op "foo" (.arrow .int natTy)) (.fvar "x" .int) natTy + +/-- info: ok: []-/ +#guard_msgs in +#eval runWFTest testWfBoundBody + +-- 9. Application with bounded body, no assumption: (λ (x: int) . x * x) 1 : Nat +-- Expected: 0 <= (λ (x: int) . x * x) 1 + +def testWfBoundBodyNoAssume : LExprT String := .app (.abs (mulOp (.bvar 0 .int) (.bvar 0 .int)) (.arrow .int .int)) (.const "1" .int) natTy + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Mul" none) (Lambda.LExpr.bvar 0)) + (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "1" none))]-/ +#guard_msgs in +#eval runWFTest testWfBoundBodyNoAssume + +-- 10. If-then-else with bounded body: if b then 1 else 0 : Nat +-- Expected: 0 <= if b then 1 else 0 + +def testWfIteBoundBody : LExprT String := .ite (.const "b" .bool) (.const "1" .int) (.const "0" .int) natTy + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.ite (Lambda.LExpr.const "b" none) (Lambda.LExpr.const "1" none) (Lambda.LExpr.const "0" none))]-/ +#guard_msgs in +#eval runWFTest testWfIteBoundBody + +-- 11. If-then-else with bound functions: if b then λ (x: int). x * x : Nat else λ (y: int). 0 : Nat (whole type int -> Nat) +-- Expected: 0 <= x * x; 0 <= 0 + +def testWfIteBoundAbs : LExprT String := .ite (.const "b" .bool) (.abs (mulOp (.bvar 0 .int) (.bvar 0 .int)) (.arrow .int natTy)) (.abs (.const "0" .int) (.arrow .int natTy)) (.arrow .int natTy) + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Mul" none) (Lambda.LExpr.fvar "$__var1" none)) + (Lambda.LExpr.fvar "$__var1" none)), Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.const "0" none)]-/ +#guard_msgs in +#eval runWFTest testWfIteBoundAbs + +end WFTest + +--Tests with more sophisticated bounded types (mostly AI generated) + +namespace MoreBoundTests + +-- Test 1: Nested bounded function applications +-- Input: add : {x < 10} → {y < 5} → {z < 15}, applied to (3 : {x < 10}) and (2 : {x < 5}) +-- Expected: translate = add 3 2, wfCond = [3 < 10, 2 < 5] + +def testNestedBoundedApps : LExprT String := + .app (.app (.op "add" (.arrow (.bounded (.blt (.bvar) (.bconst 10))) + (.arrow (.bounded (.blt (.bvar) (.bconst 5))) + (.bounded (.blt (.bvar) (.bconst 15)))))) + (.const "3" (.bounded (.blt (.bvar) (.bconst 10)))) + (.arrow (.bounded (.blt (.bvar) (.bconst 5))) (.bounded (.blt (.bvar) (.bconst 15))))) + (.const "2" (.bounded (.blt (.bvar) (.bconst 5)))) + (.bounded (.blt (.bvar) (.bconst 15))) + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.const "2" none)) + (Lambda.LExpr.const "5" none), Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.const "3" none)) + (Lambda.LExpr.const "10" none)]-/ +#guard_msgs in +#eval runWFTest testNestedBoundedApps + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "add" none) (Lambda.LExpr.const "3" none)) + (Lambda.LExpr.const "2" none)-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testNestedBoundedApps) + +-- Test 2: Bounded variable in quantifier with complex bound expression +-- Input: ∀ (x : {x < 100 ∧ 0 ≤ x}). x = 42 +-- Expected: translate = ∀ x:int. (x < 100 ∧ 0 ≤ x) → (x = 42), wfCond = [] + +def testComplexBoundInQuantifier : LExprT String := + .quant .all (.bounded (.band (.blt (.bvar) (.bconst 100)) + (.ble (.bconst 0) (.bvar)))) + (.bvar 0 (.bounded (.band (.blt (.bvar) (.bconst 100)) + (.ble (.bconst 0) (.bvar))))) + (.eq (.bvar 0 (.bounded (.band (.blt (.bvar) (.bconst 100)) + (.ble (.bconst 0) (.bvar))))) + (.const "42" .int) .bool) + +/-- info: ok: []-/ +#guard_msgs in +#eval runWFTest testComplexBoundInQuantifier + +/-- info: Lambda.LExpr.quant + (Lambda.QuantifierKind.all) + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.bvar 0) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.And" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.bvar 0)) + (Lambda.LExpr.const "100" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.bvar 0)))) + (Lambda.LExpr.eq (Lambda.LExpr.bvar 0) (Lambda.LExpr.const "42" none))) +-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testComplexBoundInQuantifier) + +-- Test 3: If-then-else with bounded branches and boolean condition +-- Input: if (0 < (getValue 5 : {0 ≤ x})) then (1 : {x < 10}) else (0 : {x < 10}) : {x < 10} +-- Expected: translate = if (0 ≤ getValue 5) → (0 < getValue 5) then 1 else 0, wfCond = [1 < 10, 0 < 10, (if (getValue 5) then 1 else 0) < 10] +def testBoundedIte : LExprT String := + .ite (.app (.app (LFunc.opExprT intLtFunc) + (.const "0" .int) + (.arrow .int .bool)) + (.app (.op "getValue" (.arrow .int (.bounded (.ble (.bconst 0) (.bvar))))) + (.const "5" .int) + (.bounded (.ble (.bconst 0) (.bvar)))) + .bool) + (.const "1" (.bounded (.blt (.bvar) (.bconst 10)))) + (.const "0" (.bounded (.blt (.bvar) (.bconst 10)))) + (.bounded (.blt (.bvar) (.bconst 10))) + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.ite + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "getValue" none) (Lambda.LExpr.const "5" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "getValue" none) (Lambda.LExpr.const "5" none)))) + (Lambda.LExpr.const "1" none) + (Lambda.LExpr.const "0" none))) + (Lambda.LExpr.const "10" none), Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.const "1" none)) + (Lambda.LExpr.const "10" none), Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.const "10" none)]-/ +#guard_msgs in +#eval runWFTest testBoundedIte + +/-- info: Lambda.LExpr.ite + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "getValue" none) (Lambda.LExpr.const "5" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "getValue" none) (Lambda.LExpr.const "5" none)))) + (Lambda.LExpr.const "1" none) + (Lambda.LExpr.const "0" none)-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testBoundedIte) + +-- Test 4: Lambda with bounded parameter and bounded return type +-- Input: λ (x : {0 ≤ x}). increment x : {y < 100} +-- Expected: translate = λ x:int. increment x, wfCond = [0 ≤ x → increment x < 100; 0 <= x -> 0 <= x] +def testBoundedLambda : LExprT String := + .abs (.app (.op "increment" (.arrow (.bounded (.ble (.bconst 0) (.bvar))) + (.bounded (.blt (.bvar) (.bconst 100))))) + (.bvar 0 (.bounded (.ble (.bconst 0) (.bvar)))) + (.bounded (.blt (.bvar) (.bconst 100)))) + (.arrow (.bounded (.ble (.bconst 0) (.bvar))) + (.bounded (.blt (.bvar) (.bconst 100)))) + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var1" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var1" none)), Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "$__var0" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "increment" none) (Lambda.LExpr.fvar "$__var0" none))) + (Lambda.LExpr.const "100" none))]-/ +#guard_msgs in +#eval runWFTest testBoundedLambda + +/-- info: Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app (Lambda.LExpr.op "increment" none) (Lambda.LExpr.bvar 0))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testBoundedLambda) + +-- Test 5: Equality between bounded expressions +-- Input: (square (3 : {-10 ≤ x ≤ 10}) : {0 ≤ y}) = (9 : {0 ≤ z}) +-- Expected: translate = 0 <= square 3 -> square 3 = 9, wfCond = [-10 ≤ 3 ≤ 10, 0 ≤ 9] +def testBoundedEquality : LExprT String := + .eq (.app (.op "square" (.arrow (.bounded (.band (.ble (.bconst (-10)) (.bvar)) + (.ble (.bvar) (.bconst 10)))) + (.bounded (.ble (.bconst 0) (.bvar))))) + (.const "3" (.bounded (.band (.ble (.bconst (-10)) (.bvar)) + (.ble (.bvar) (.bconst 10))))) + (.bounded (.ble (.bconst 0) (.bvar)))) + (.const "9" (.bounded (.ble (.bconst 0) (.bvar)))) + .bool + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.And" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "-10" none)) + (Lambda.LExpr.const "3" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "3" none)) + (Lambda.LExpr.const "10" none)), Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.const "9" none)]-/ +#guard_msgs in +#eval runWFTest testBoundedEquality + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "square" none) (Lambda.LExpr.const "3" none)))) + (Lambda.LExpr.eq + (Lambda.LExpr.app (Lambda.LExpr.op "square" none) (Lambda.LExpr.const "3" none)) + (Lambda.LExpr.const "9" none))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testBoundedEquality) + +-- Test 6: Free variable with bounded type in assumptions +-- Input: compare (x : {x < 50}) 25, with assumption [x < 50] +-- Expected: translate = (x < 50) → compare x 25, wfCond = [] +def testFreeVarWithAssumptions : LExprT String := + .app (.app (.op "compare" (.arrow .int (.arrow .int .bool))) + (.fvar "x" (.bounded (.blt (.bvar) (.bconst 50)))) + (.arrow .int .bool)) + (.const "25" .int) + .bool + +/-- info: ok: []-/ +#guard_msgs in +#eval runWFTest testFreeVarWithAssumptions + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.fvar "x" none)) + (Lambda.LExpr.const "50" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "compare" none) (Lambda.LExpr.fvar "x" none)) + (Lambda.LExpr.const "25" none))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testFreeVarWithAssumptions) + +-- Test 7: Metadata preservation with bounded types +-- Input: @metadata(42 : {0 ≤ x < 100}) +-- Expected: translate = @metadata(42), wfCond = [0 ≤ 42 < 100] +def testMetadataWithBounds : LExprT String := + .mdata (Info.mk "test_info") + (.const "42" (.bounded (.band (.ble (.bconst 0) (.bvar)) + (.blt (.bvar) (.bconst 100))))) + +/-- info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.And" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.const "42" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Lt" none) (Lambda.LExpr.const "42" none)) + (Lambda.LExpr.const "100" none))]-/ +#guard_msgs in +#eval runWFTest testMetadataWithBounds + +/-- info: Lambda.LExpr.mdata { value := "test_info" } (Lambda.LExpr.const "42" none)-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testMetadataWithBounds) + +-- Test 8: Chain of bounded function applications +-- Input: f3 (f2 (f1 5 : {x < 10}) : {x < 20}) : {x < 30} +-- Expected: translate = f3 (f2 (f1 5)), wfCond = [f2 (f1 5) < 20 -> f1 5 < 10 → f2 (f1 5) < 20, f1 5 < 10 -> f1 5 < 10] +def testBoundedChain : LExprT String := + .app (.op "f3" (.arrow (.bounded (.blt (.bvar) (.bconst 20))) + (.bounded (.blt (.bvar) (.bconst 30))))) + (.app (.op "f2" (.arrow (.bounded (.blt (.bvar) (.bconst 10))) + (.bounded (.blt (.bvar) (.bconst 20))))) + (.app (.op "f1" (.arrow .int (.bounded (.blt (.bvar) (.bconst 10))))) + (.const "5" .int) + (.bounded (.blt (.bvar) (.bconst 10)))) + (.bounded (.blt (.bvar) (.bconst 20)))) + (.bounded (.blt (.bvar) (.bconst 30))) + +/--info: ok: [Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app + (Lambda.LExpr.op "f2" none) + (Lambda.LExpr.app (Lambda.LExpr.op "f1" none) (Lambda.LExpr.const "5" none)))) + (Lambda.LExpr.const "20" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "f1" none) (Lambda.LExpr.const "5" none))) + (Lambda.LExpr.const "10" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app + (Lambda.LExpr.op "f2" none) + (Lambda.LExpr.app (Lambda.LExpr.op "f1" none) (Lambda.LExpr.const "5" none)))) + (Lambda.LExpr.const "20" none))), Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "f1" none) (Lambda.LExpr.const "5" none))) + (Lambda.LExpr.const "10" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "f1" none) (Lambda.LExpr.const "5" none))) + (Lambda.LExpr.const "10" none))]-/ +#guard_msgs in +#eval runWFTest testBoundedChain + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.op "f3" none) + (Lambda.LExpr.app + (Lambda.LExpr.op "f2" none) + (Lambda.LExpr.app (Lambda.LExpr.op "f1" none) (Lambda.LExpr.const "5" none)))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testBoundedChain) + +end MoreBoundTests + +-- Tests relating to positivity + +/- +Here we have several tests for positivity. For many, we have the main test as well as an auxilliary test showing the ordinary (i.e. no positivity complications) version. This demonstrates that we can create better translations when we know that there are no positivity restrictions. +-/ + +namespace PositiveTest + +def ltOp (e1 e2: LExprT String) : LExprT String := .app (.app (LFunc.opExprT intLtFunc) e1 (.arrow .int .bool)) e2 .bool +def impliesOp (e1 e2: LExprT String) : LExprT String := .app (.app (LFunc.opExprT boolImpliesFunc) e1 (.arrow .bool .bool)) e2 .bool + +-- 1. not (foo 1 < 0) where foo: int -> nat +-- Expected: 0 <= foo 1 -> not (foo 1 < 0) +def testPosNot : LExprT String := + notOp (ltOp (.app (.op "foo" (.arrow .int natTy)) (.const "1" .int) natTy) (.const "0" .int)) + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.const "1" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Not" none) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.const "1" none))) + (Lambda.LExpr.const "0" none))) -/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosNot) + +-- 1a. (foo 1 < 0) where foo: int -> nat +-- Expected: 0 <= foo 1 -> foo 1 < 0 +def testPosNotAux : LExprT String := + ltOp (.app (.op "foo" (.arrow .int natTy)) (.const "1" .int) natTy) (.const "0" .int) + +/-- +info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.const "1" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.const "1" none))) + (Lambda.LExpr.const "0" none))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosNotAux) + + +-- 2. not (forall (x: int), foo x < 0) for foo of same type +-- Expected: (forall (x: int), 0 <= foo x) -> not (forall (x: int), foo x < 0) +def testPosQuant : LExprT String := + notOp (.quant .all .int (.bvar 0 .int) + (ltOp (.app (.op "foo" (.arrow .int natTy)) (.bvar 0 .int) natTy) (.const "0" .int))) + + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.quant + (Lambda.QuantifierKind.all) + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.bvar 0) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))))) + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Not" none) + (Lambda.LExpr.quant + (Lambda.QuantifierKind.all) + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.bvar 0) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "0" none)))) -/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosQuant) + +-- 2a. (forall (x: int), foo x < 0) for foo: int -> nat +-- Expected: forall (x: int), 0 <= foo x -> foo x < 0 +def testPosQuantAux : LExprT String := + .quant .all .int (.bvar 0 .int) + (ltOp (.app (.op "foo" (.arrow .int natTy)) (.bvar 0 .int) natTy) (.const "0" .int)) + +/-- info: Lambda.LExpr.quant + (Lambda.QuantifierKind.all) + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.bvar 0) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "0" none)))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosQuantAux) + +-- 3. (foo 1 < 0 -> false) +-- Expected: 0 <= foo 1 -> (foo 1 < 0 -> false) +def testPosImpl : LExprT String := + impliesOp (ltOp (.app (.op "foo" (.arrow .int natTy)) (.const "1" .int) natTy) (.const "0" .int)) + (.const "false" .bool) + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.const "1" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.const "1" none))) + (Lambda.LExpr.const "0" none))) + (Lambda.LExpr.const "false" none))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosImpl) + +-- 3a. (b -> foo 1 < 0) for boolean constant b where foo: int -> nat +-- Expected: b -> 0 <= foo 1 -> foo 1 < 0 +def testPosImplAux : LExprT String := + impliesOp (.const "b" .bool) + (ltOp (.app (.op "foo" (.arrow .int natTy)) (.const "1" .int) natTy) (.const "0" .int)) + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Bool.Implies" none) (Lambda.LExpr.const "b" none)) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.const "1" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.const "1" none))) + (Lambda.LExpr.const "0" none)))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosImplAux) + + +-- 4. (\x y. x -> y) (foo x < 0) false +-- Expected: (forall x, 0 <= foo x) -> (\x y: bool. x -> y) (foo x < 0) false +def testPosImplApp : LExprT String := + .app (.app (.abs (.abs (impliesOp (.bvar 1 .bool) (.bvar 0 .bool)) (.arrow .bool .bool)) (.arrow .bool (.arrow .bool .bool))) + (ltOp (.app (.op "foo" (.arrow .int natTy)) (.fvar "x" .int) natTy) (.const "0" .int)) + (.arrow .bool .bool)) + (.const "false" .bool) + .bool + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.fvar "x" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "bool" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "bool" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Bool.Implies" none) (Lambda.LExpr.bvar 1)) + (Lambda.LExpr.bvar 0)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.fvar "x" none))) + (Lambda.LExpr.const "0" none))) + (Lambda.LExpr.const "false" none))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosImplApp) + +-- 5. (\x. foo x < 0) 1 +-- Expected: (forall x, 0 <= foo x) -> (\x. foo x < 0) 1 +def testPosApp : LExprT String := + .app (.abs (ltOp (.app (.op "foo" (.arrow .int natTy)) (.bvar 0 .int) natTy) (.const "0" .int)) (.arrow .int .bool)) + (.const "1" .int) + .bool + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.quant + (Lambda.QuantifierKind.all) + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.bvar 0) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))))) + (Lambda.LExpr.app + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "0" none))) + (Lambda.LExpr.const "1" none)) -/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosApp) + +-- 5a. (\x. foo y < 0) 1 where foo: int -> nat and y is a free variable +-- Expected: 0 <= foo y -> (\x. foo y < 0) 1 +def testPosAppAux : LExprT String := + .app (.abs (ltOp (.app (.op "foo" (.arrow .int natTy)) (.fvar "y" .int) natTy) (.const "0" .int)) (.arrow .int .bool)) + (.const "1" .int) + .bool + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.fvar "y" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.fvar "y" none))) + (Lambda.LExpr.const "0" none))) + (Lambda.LExpr.const "1" none))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosAppAux) + + +-- 6. (\x. foo x) 1 >= 0 +-- Expected: 0 <= (\x. foo x) 1 -> (forall x, 0 <= foo x) -> (\x. foo x) 1 >= 0 +def testAbsQuant : LExprT String := + geOp (.app (.abs (.app (.op "foo" (.arrow .int natTy)) (.bvar 0 .int) natTy) (.arrow .int natTy)) + (.const "1" .int) + natTy) + (.const "0" .int) + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "1" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.quant + (Lambda.QuantifierKind.all) + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.bvar 0) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Ge" none) + (Lambda.LExpr.app + (Lambda.LExpr.abs + (some (Lambda.LMonoTy.tcons "int" [] (Lambda.LTyRestrict.nodata))) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.bvar 0))) + (Lambda.LExpr.const "1" none))) + (Lambda.LExpr.const "0" none)))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testAbsQuant) + +-- 7. (if foo x < 0 then bar == 1 else baz > 0) where bar and baz have type nat +-- Expected: 0 <= foo x -> if foo x < 0 then 0 <= bar -> bar == 1 else 0 <= baz -> baz > 0 +def testPosIte : LExprT String := + .ite (ltOp (.app (.op "foo" (.arrow .int natTy)) (.fvar "x" .int) natTy) (.const "0" .int)) + (.eq (.fvar "bar" natTy) (.const "1" .int) .bool) + (.app (.app (LFunc.opExprT intGtFunc) (.fvar "baz" natTy) (.arrow .int .bool)) (.const "0" .int) .bool) + .bool + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.fvar "x" none)))) + (Lambda.LExpr.ite + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Lt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.fvar "x" none))) + (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "bar" none))) + (Lambda.LExpr.eq (Lambda.LExpr.fvar "bar" none) (Lambda.LExpr.const "1" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.fvar "baz" none))) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Gt" none) (Lambda.LExpr.fvar "baz" none)) + (Lambda.LExpr.const "0" none))))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosIte) + +-- 8. (foo x >= 0) && (bar y > 0) where foo: int -> nat and bar: int -> nat +-- Expected: (0 <= foo x -> foo x >= 0) && (0 <= bar y -> bar y > 0) +def andOp (e1 e2: LExprT String) : LExprT String := .app (.app (LFunc.opExprT boolAndFunc) e1 (.arrow .bool .bool)) e2 .bool +def gtOp (e1 e2: LExprT String) : LExprT String := .app (.app (LFunc.opExprT intGtFunc) e1 (.arrow .int .bool)) e2 .bool + +def testPosAnd : LExprT String := + andOp (geOp (.app (.op "foo" (.arrow .int natTy)) (.fvar "x" .int) natTy) (.const "0" .int)) + (gtOp (.app (.op "bar" (.arrow .int natTy)) (.fvar "y" .int) natTy) (.const "0" .int)) + +/-- info: Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.And" none) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.fvar "x" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Ge" none) + (Lambda.LExpr.app (Lambda.LExpr.op "foo" none) (Lambda.LExpr.fvar "x" none))) + (Lambda.LExpr.const "0" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Bool.Implies" none) + (Lambda.LExpr.app + (Lambda.LExpr.app (Lambda.LExpr.op "Int.Le" none) (Lambda.LExpr.const "0" none)) + (Lambda.LExpr.app (Lambda.LExpr.op "bar" none) (Lambda.LExpr.fvar "y" none)))) + (Lambda.LExpr.app + (Lambda.LExpr.app + (Lambda.LExpr.op "Int.Gt" none) + (Lambda.LExpr.app (Lambda.LExpr.op "bar" none) (Lambda.LExpr.fvar "y" none))) + (Lambda.LExpr.const "0" none)))-/ +#guard_msgs in +#eval eraseTy (translateBoundedExpr testPosAnd) + + +end PositiveTest + +end Test