diff --git a/Strata/Backends/CBMC/CoreToCBMC.lean b/Strata/Backends/CBMC/CoreToCBMC.lean index 04617c385c..9894b83c4c 100644 --- a/Strata/Backends/CBMC/CoreToCBMC.lean +++ b/Strata/Backends/CBMC/CoreToCBMC.lean @@ -215,7 +215,7 @@ end def listToExpr (l: ListMap CoreLabel Core.Procedure.Check) : Core.Expression.Expr := match l with - | _ => .true () + | _ => Core.true def createContractSymbolFromAST (func : Core.Procedure) : Except String CBMCSymbol := do let location : Location := { diff --git a/Strata/DDM/Util/SourceRange.lean b/Strata/DDM/Util/SourceRange.lean index dc602ea181..9e7e7fd856 100644 --- a/Strata/DDM/Util/SourceRange.lean +++ b/Strata/DDM/Util/SourceRange.lean @@ -25,10 +25,11 @@ structure SourceRange where start : String.Pos.Raw /-- One past the end of the range. -/ stop : String.Pos.Raw -deriving DecidableEq, Inhabited, Repr +deriving Inhabited, Repr, DecidableEq, BEq namespace SourceRange +@[expose] def none : SourceRange := { start := 0, stop := 0 } def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0 diff --git a/Strata/DL/Imperative/PureExpr.lean b/Strata/DL/Imperative/PureExpr.lean index aeb3cff286..15eeb0e01b 100644 --- a/Strata/DL/Imperative/PureExpr.lean +++ b/Strata/DL/Imperative/PureExpr.lean @@ -49,6 +49,9 @@ class HasBool (P : PureExpr) where ff : P.Expr tt_is_not_ff: tt ≠ ff boolTy : P.Ty + /-- Check if an expression represents `true`. Defaults to `e == tt` but + implementations may override to ignore metadata. -/ + isTt : [BEq P.Expr] → P.Expr → Bool := fun e => e == tt class HasNot (P : PureExpr) extends HasBool P where not : P.Expr → P.Expr diff --git a/Strata/DL/Imperative/StmtEval.lean b/Strata/DL/Imperative/StmtEval.lean index f09895a74c..65d529c24e 100644 --- a/Strata/DL/Imperative/StmtEval.lean +++ b/Strata/DL/Imperative/StmtEval.lean @@ -61,7 +61,7 @@ def runStep [BEq P.Expr] [HasBool P] | .det e => match ops.evalExpr ρ e with | some v => - if v == HasBool.tt then .stmts tss ρ + if HasBool.isTt v then .stmts tss ρ else .stmts ess ρ | none => .terminal (ops.addError ρ "ITE condition did not reduce to bool") @@ -71,7 +71,7 @@ def runStep [BEq P.Expr] [HasBool P] | .det g => match ops.evalExpr ρ g with | some v => - if v == HasBool.tt then .stmts (body ++ [s]) ρ + if HasBool.isTt v then .stmts (body ++ [s]) ρ else .terminal ρ | none => .terminal (ops.addError ρ "Loop guard did not reduce to bool") diff --git a/Strata/DL/Lambda/LExpr.lean b/Strata/DL/Lambda/LExpr.lean index 2eacf83523..689185ed40 100644 --- a/Strata/DL/Lambda/LExpr.lean +++ b/Strata/DL/Lambda/LExpr.lean @@ -231,6 +231,21 @@ instance {T: LExprParamsT} [DecidableEq T.base.Metadata] [DecidableEq T.TypeType else isFalse (fun heq => h (LExpr.beq_eq e1 e2 |>.mpr heq)) +/-- Structural equality ignoring metadata fields. Does not allocate intermediate expressions. -/ +def LExpr.beqIgnoringMetadata [BEq T.TypeType] [BEq (Identifier T.base.IDMeta)] : LExpr T → LExpr T → Bool + | .const _ c1, .const _ c2 => c1 == c2 + | .op _ o1 ty1, .op _ o2 ty2 => o1 == o2 && ty1 == ty2 + | .bvar _ i1, .bvar _ i2 => i1 == i2 + | .fvar _ n1 ty1, .fvar _ n2 ty2 => n1 == n2 && ty1 == ty2 + | .abs _ name1 ty1 e1, .abs _ name2 ty2 e2 => name1 == name2 && ty1 == ty2 && beqIgnoringMetadata e1 e2 + | .quant _ k1 name1 ty1 tr1 e1, .quant _ k2 name2 ty2 tr2 e2 => + k1 == k2 && name1 == name2 && ty1 == ty2 && beqIgnoringMetadata tr1 tr2 && beqIgnoringMetadata e1 e2 + | .app _ fn1 e1, .app _ fn2 e2 => beqIgnoringMetadata fn1 fn2 && beqIgnoringMetadata e1 e2 + | .ite _ c1 t1 f1, .ite _ c2 t2 f2 => + beqIgnoringMetadata c1 c2 && beqIgnoringMetadata t1 t2 && beqIgnoringMetadata f1 f2 + | .eq _ e1a e1b, .eq _ e2a e2b => beqIgnoringMetadata e1a e2a && beqIgnoringMetadata e1b e2b + | _, _ => false + def LExpr.noTrigger {T : LExprParamsT} (m : T.base.Metadata) : LExpr T := .bvar m 0 def LExpr.allTr {T : LExprParamsT} (m : T.base.Metadata) (name : String) (ty : Option T.TypeType) := @LExpr.quant T m .all name ty def LExpr.all {T : LExprParamsT} (m : T.base.Metadata) (name : String) (ty : Option T.TypeType) := @LExpr.quant T m .all name ty (LExpr.noTrigger m) @@ -694,6 +709,7 @@ open Lean Elab Meta meta class MkLExprParams (T: LExprParams) where elabIdent : Lean.Syntax → MetaM Expr toExpr : Expr + defaultMetadata : MetaM Expr := mkAppM ``Unit.unit #[] declare_syntax_cat lidentmono @@ -720,30 +736,30 @@ meta def mkNegLit (n: NumLit) := Expr.app (.const ``Int.neg []) (mkIntLit n) meta def elabLConstMono [MkLExprParams T] : Lean.Syntax → MetaM Expr | `(lconstmono| #$n:num) => do - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] let intVal := mkIntLit n let lconstVal ← mkAppM ``LConst.intConst #[intVal] return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal] | `(lconstmono| #-$n:num) => do - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] let intVal := mkNegLit n let lconstVal ← mkAppM ``LConst.intConst #[intVal] return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal] | `(lconstmono| #true) => do - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] let lconstVal ← mkAppM ``LConst.boolConst #[toExpr true] return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal] | `(lconstmono| #false) => do - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] let lconstVal ← mkAppM ``LConst.boolConst #[toExpr false] return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal] | `(lconstmono| #$s:ident) => do let s := toString s.getId - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] let lconstVal ← mkAppM ``LConst.strConst #[mkStrLit s] return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal] @@ -757,13 +773,13 @@ scoped syntax lopmono : lexprmono meta def elabLOpMono [MkLExprParams T] : Lean.Syntax → MetaM Expr | `(lopmono| ~$s:lidentmono) => do let none ← mkNone (mkConst ``LMonoTy) - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.op []) #[tMono, metadata, ← MkLExprParams.elabIdent T s, none] | `(lopmono| (~$s:lidentmono : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.op []) #[tMono, metadata, ← MkLExprParams.elabIdent T s, lmonoty] | _ => throwUnsupportedSyntax @@ -772,7 +788,7 @@ declare_syntax_cat lbvarmono scoped syntax "%" noWs num : lbvarmono meta def elabLBVarMono [MkLExprParams T] : Lean.Syntax → MetaM Expr | `(lbvarmono| %$n:num) => do - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.bvar []) #[tMono, metadata, mkNatLit n.getNat] | _ => throwUnsupportedSyntax @@ -785,13 +801,13 @@ scoped syntax "(" lidentmono ":" lmonoty ")" : lfvarmono meta def elabLFVarMono [MkLExprParams T] : Lean.Syntax → MetaM Expr | `(lfvarmono| $i:lidentmono) => do let none ← mkNone (mkConst ``LMonoTy) - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.fvar []) #[tMono, metadata, ← MkLExprParams.elabIdent T i, none] | `(lfvarmono| ($i:lidentmono : $ty:lmonoty)) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.fvar []) #[tMono, metadata, ← MkLExprParams.elabIdent T i, lmonoty] | _ => throwUnsupportedSyntax @@ -842,32 +858,32 @@ meta partial def elabLExprMono [MkLExprParams T] : Lean.Syntax → MetaM Expr | `(lexprmono| λ $e:lexprmono) => do let e' ← elabLExprMono (T:=T) e let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T return mkAppN (.const ``LExpr.absUntyped []) #[tMono, metadata, e'] | `(lexprmono| λ ($mty:lmonoty): $e:lexprmono) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty let e' ← elabLExprMono (T:=T) e let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T return mkAppN (.const ``LExpr.abs []) #[tMono, metadata, mkStrLit "", lmonoty, e'] | `(lexprmono| ∀ $e:lexprmono) => do let e' ← elabLExprMono (T:=T) e let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T return mkAppN (.const ``LExpr.allUntyped []) #[tMono, metadata, e'] | `(lexprmono| ∀ {$tr}$e:lexprmono) => do let e' ← elabLExprMono (T:=T) e let tr' ← elabLExprMono (T:=T) tr let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T return mkAppN (.const ``LExpr.allUntypedTr []) #[tMono, metadata, tr', e'] | `(lexprmono| ∀ ($mty:lmonoty): $e:lexprmono) => do let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty let e' ← elabLExprMono (T:=T) e let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let emptyName := mkStrLit "" return mkAppN (.const ``LExpr.all []) #[tMono, metadata, emptyName, lmonoty, e'] | `(lexprmono| ∀ ($mty:lmonoty):{$tr} $e:lexprmono) => do @@ -876,7 +892,7 @@ meta partial def elabLExprMono [MkLExprParams T] : Lean.Syntax → MetaM Expr let e' ← elabLExprMono (T:=T) e let tr' ← elabLExprMono (T:=T) tr let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let emptyName := mkStrLit "" return mkAppN (.const ``LExpr.allTr []) #[tMono, metadata, emptyName, lmonoty, tr', e'] | `(lexprmono| ∃ ($mty:lmonoty): $e:lexprmono) => do @@ -884,7 +900,7 @@ meta partial def elabLExprMono [MkLExprParams T] : Lean.Syntax → MetaM Expr let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty let e' ← elabLExprMono (T:=T) e let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let emptyName := mkStrLit "" return mkAppN (.const ``LExpr.exist []) #[tMono, metadata, emptyName, lmonoty, e'] | `(lexprmono| ∃ ($mty:lmonoty):{$tr} $e:lexprmono) => do @@ -893,37 +909,37 @@ meta partial def elabLExprMono [MkLExprParams T] : Lean.Syntax → MetaM Expr let e' ← elabLExprMono (T:=T) e let tr' ← elabLExprMono (T:=T) tr let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let emptyName := mkStrLit "" return mkAppN (.const ``LExpr.existTr []) #[tMono, metadata, emptyName, lmonoty, tr', e'] | `(lexprmono| ∃ $e:lexprmono) => do let e' ← elabLExprMono (T:=T) e - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.existUntyped []) #[tMono, metadata, e'] | `(lexprmono| ∃{$tr} $e:lexprmono) => do let e' ← elabLExprMono (T:=T) e let tr' ← elabLExprMono (T:=T) tr - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.existUntypedTr []) #[tMono, metadata, tr', e'] | `(lexprmono| ($e1:lexprmono $e2:lexprmono)) => do let e1' ← elabLExprMono (T:=T) e1 let e2' ← elabLExprMono (T:=T) e2 - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.app []) #[tMono, metadata, e1', e2'] | `(lexprmono| $e1:lexprmono == $e2:lexprmono) => do let e1' ← elabLExprMono (T:=T) e1 let e2' ← elabLExprMono (T:=T) e2 - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.eq []) #[tMono, metadata, e1', e2'] | `(lexprmono| if $e1:lexprmono then $e2:lexprmono else $e3:lexprmono) => do let e1' ← elabLExprMono (T:=T) e1 let e2' ← elabLExprMono (T:=T) e2 let e3' ← elabLExprMono (T:=T) e3 - let metadata ← mkAppM ``Unit.unit #[] + let metadata ← MkLExprParams.defaultMetadata T let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T] return mkAppN (.const ``LExpr.ite []) #[tMono, metadata, e1', e2', e3'] | `(lexprmono| ($e:lexprmono)) => elabLExprMono (T:=T) e diff --git a/Strata/DL/Lambda/Scopes.lean b/Strata/DL/Lambda/Scopes.lean index d30fdbf126..ade444f899 100644 --- a/Strata/DL/Lambda/Scopes.lean +++ b/Strata/DL/Lambda/Scopes.lean @@ -74,7 +74,7 @@ def Scope.merge (cond : LExpr T.mono) (m1 m2 : Scope T) : Scope T := (k, (ty1, mkIte cond e1 e2)) :: Scope.merge cond rest (m2.erase k) where mkIte (cond tru fals : LExpr T.mono) : LExpr T.mono := - if tru == fals then tru + if tru.beqIgnoringMetadata fals then tru else (LExpr.ite (default : T.Metadata) cond tru fals) diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index 5240629436..f37b57fc0f 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -82,7 +82,7 @@ private def withTypeBVars (xs : List String) (k : TranslateM α) : TranslateM α private def withBVars (xs : List String) (k : TranslateM α) : TranslateM α := do let old := (← get).bvars - let fresh := xs.toArray.map (fun n => (.fvar () (mkIdent n) none : Core.Expression.Expr)) + let fresh := xs.toArray.map (fun n => (.fvar (ExprSourceLoc.synthesized "boole") (mkIdent n) none : Core.Expression.Expr)) modify fun s => { s with bvars := old ++ fresh } try let out ← k @@ -173,7 +173,7 @@ private def getBVarExpr (m : SourceRange) (i : Nat) : TranslateM Core.Expression let xs := (← get).bvars if i < xs.size then match xs[(xs.size - i - 1)]? with - | some (.bvar _ _) => return (.bvar () i) + | some (.bvar _ _) => return (.bvar m i) | some e => return e | none => throwAt m s!"Unknown bound variable with index {i}" else @@ -212,8 +212,8 @@ private def toCoreMetaData (sr : SourceRange) : TranslateM (Imperative.MetaData let file := (← get).fileName return Imperative.MetaData.ofSourceRange (.file file) sr -private def mkCoreApp (op : Core.Expression.Expr) (args : List Core.Expression.Expr) : Core.Expression.Expr := - Lambda.LExpr.mkApp () op args +private def mkCoreApp (m : SourceRange) (op : Core.Expression.Expr) (args : List Core.Expression.Expr) : Core.Expression.Expr := + Lambda.LExpr.mkApp m op args private def typeRange : Boole.Type → SourceRange | .bvar m _ => m @@ -281,6 +281,7 @@ private def toCoreMonoBind (b : BooleDDM.MonoBind SourceRange) : TranslateM (Cor match b with | .mono_bind_mk _ ⟨_, n⟩ ty => return (mkIdent n, ← toCoreMonoType ty) + private def bvWidth (m : SourceRange) (ty : Boole.Type) : TranslateM Nat := match ty with | .bv1 _ => return 1 @@ -292,17 +293,17 @@ private def bvWidth (m : SourceRange) (ty : Boole.Type) : TranslateM Nat := private def toCoreBvUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do let n ← bvWidth m ty - return .app () (.op () ⟨s!"Bv{n}.{op}", ()⟩ none) a + return .app m (.op m ⟨s!"Bv{n}.{op}", ()⟩ none) a private def toCoreBvBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do let n ← bvWidth m ty - return mkCoreApp (.op () ⟨s!"Bv{n}.{op}", ()⟩ none) [a, b] + return mkCoreApp m (.op m ⟨s!"Bv{n}.{op}", ()⟩ none) [a, b] def toCoreTypedUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do match ty with | .int _ => - let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none - return .app () iop a + let iop : Core.Expression.Expr := .op m ⟨s!"Int.{op}", ()⟩ none + return .app m iop a | _ => toCoreBvUn m ty op a -- Bitvector comparison operators use unsigned variants by default (Le→ULe, etc.). @@ -315,8 +316,8 @@ private def toBvCmpOp (op : String) : String := def toCoreTypedBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do match ty with | .int _ => - let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none - return mkCoreApp iop [a, b] + let iop : Core.Expression.Expr := .op m ⟨s!"Int.{op}", ()⟩ none + return mkCoreApp m iop [a, b] | _ => toCoreBvBin m ty (toBvCmpOp op) a b private def toCoreExtensionalEq @@ -326,13 +327,13 @@ private def toCoreExtensionalEq match ty with | .Map _ _ keyTy => let keyTy' ← toCoreMonoType keyTy - let idx : Core.Expression.Expr := .bvar () 0 + let idx : Core.Expression.Expr := .bvar m 0 let a := Lambda.LExpr.liftBVars 1 a let b := Lambda.LExpr.liftBVars 1 b - let lhs := mkCoreApp Core.mapSelectOp [a, idx] - let rhs := mkCoreApp Core.mapSelectOp [b, idx] + let lhs := mkCoreApp m Core.mapSelectOp [a, idx] + let rhs := mkCoreApp m Core.mapSelectOp [b, idx] let trigger := lhs - return .quant () .all "" (some keyTy') trigger (.eq () lhs rhs) + return .quant m .all "" (some keyTy') trigger (.eq m lhs rhs) | _ => throwAt m s!"Extensional equality is currently only supported for Map types, got: {repr ty}" @@ -351,15 +352,16 @@ private def oldifyExpr (inoutNames : List String) : Core.Expression.Expr → Cor mutual partial def toCoreQuant + (m : SourceRange) (isForall : Bool) (ds : BooleDDM.DeclList SourceRange) (body : Boole.Expr) : TranslateM Core.Expression.Expr := do let decls := declListToList ds let tys ← decls.mapM fun (.bind_mk _ _ _ ty) => toCoreMonoType ty - let qBVars : Array Core.Expression.Expr := (decls.toArray.mapIdx fun i _ => .bvar () i) + let qBVars : Array Core.Expression.Expr := (decls.toArray.mapIdx fun i _ => .bvar m i) let body' ← withBVarExprs qBVars (toCoreExpr body) let q := if isForall then Lambda.QuantifierKind.all else Lambda.QuantifierKind.exist - return tys.foldr (fun ty acc => .quant () q "" (some ty) (.bvar () 0) acc) body' + return tys.foldr (fun ty acc => .quant m q "" (some ty) (.bvar m 0) acc) body' /-- Normalize Boole quantifier surface-syntax variants to a single lowering path. @@ -373,16 +375,16 @@ constructor variants. -/ private partial def toCoreQuantExpr? (e : Boole.Expr) : Option (TranslateM Core.Expression.Expr) := match e with - | .forall _ ds body - | .forall_unicode _ ds body - | .forallT _ ds _ body - | .forall_unicodeT _ ds _ body => - some (toCoreQuant true ds body) - | .exists _ ds body - | .exists_unicode _ ds body - | .existsT _ ds _ body - | .exists_unicodeT _ ds _ body => - some (toCoreQuant false ds body) + | .forall m ds body + | .forall_unicode m ds body + | .forallT m ds _ body + | .forall_unicodeT m ds _ body => + some (toCoreQuant m true ds body) + | .exists m ds body + | .exists_unicode m ds body + | .existsT m ds _ body + | .exists_unicodeT m ds _ body => + some (toCoreQuant m false ds body) | _ => none partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do @@ -392,9 +394,9 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do | .fvar m i => let id := mkIdent (← getFVarName m i) if (← getFVarIsOp m i) then - return .op () id none + return .op m id none else - return .fvar () id none + return .fvar m id none | .bvar m i => getBVarExpr m i | .let_in_expr _ _bind value body => -- Assumption: `value` contains no free variables that share names with @@ -402,26 +404,26 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do -- are pure arithmetic with no name collisions. let value' ← toCoreExpr value withBVarExprs #[value'] (toCoreExpr body) - | .app _ f a => return .app () (← toCoreExpr f) (← toCoreExpr a) - | .not _ a => return .app () Core.boolNotOp (← toCoreExpr a) - | .bv1Lit _ ⟨_, n⟩ => return .bitvecConst () 1 n - | .bv8Lit _ ⟨_, n⟩ => return .bitvecConst () 8 n - | .bv16Lit _ ⟨_, n⟩ => return .bitvecConst () 16 n - | .bv32Lit _ ⟨_, n⟩ => return .bitvecConst () 32 n - | .bv64Lit _ ⟨_, n⟩ => return .bitvecConst () 64 n - | .natToInt _ ⟨_, n⟩ => return .intConst () (Int.ofNat n) - | .if _ _ c t f => return .ite () (← toCoreExpr c) (← toCoreExpr t) (← toCoreExpr f) - | .map_get _ _ _ a i => return mkCoreApp Core.mapSelectOp [← toCoreExpr a, ← toCoreExpr i] - | .map_set _ _ _ a i v => return mkCoreApp Core.mapUpdateOp [← toCoreExpr a, ← toCoreExpr i, ← toCoreExpr v] - | .btrue _ => return .true () - | .bfalse _ => return .false () - | .and _ a b => return mkCoreApp Core.boolAndOp [← toCoreExpr a, ← toCoreExpr b] - | .or _ a b => return mkCoreApp Core.boolOrOp [← toCoreExpr a, ← toCoreExpr b] - | .equiv _ a b => return mkCoreApp Core.boolEquivOp [← toCoreExpr a, ← toCoreExpr b] - | .implies _ a b => return mkCoreApp Core.boolImpliesOp [← toCoreExpr a, ← toCoreExpr b] + | .app m f a => return .app m (← toCoreExpr f) (← toCoreExpr a) + | .not m a => return .app m Core.boolNotOp (← toCoreExpr a) + | .bv1Lit m ⟨_, n⟩ => return .bitvecConst m 1 n + | .bv8Lit m ⟨_, n⟩ => return .bitvecConst m 8 n + | .bv16Lit m ⟨_, n⟩ => return .bitvecConst m 16 n + | .bv32Lit m ⟨_, n⟩ => return .bitvecConst m 32 n + | .bv64Lit m ⟨_, n⟩ => return .bitvecConst m 64 n + | .natToInt m ⟨_, n⟩ => return .intConst m (Int.ofNat n) + | .if m _ c t f => return .ite m (← toCoreExpr c) (← toCoreExpr t) (← toCoreExpr f) + | .map_get m _ _ a i => return mkCoreApp m Core.mapSelectOp [← toCoreExpr a, ← toCoreExpr i] + | .map_set m _ _ a i v => return mkCoreApp m Core.mapUpdateOp [← toCoreExpr a, ← toCoreExpr i, ← toCoreExpr v] + | .btrue m => return .true m + | .bfalse m => return .false m + | .and m a b => return mkCoreApp m Core.boolAndOp [← toCoreExpr a, ← toCoreExpr b] + | .or m a b => return mkCoreApp m Core.boolOrOp [← toCoreExpr a, ← toCoreExpr b] + | .equiv m a b => return mkCoreApp m Core.boolEquivOp [← toCoreExpr a, ← toCoreExpr b] + | .implies m a b => return mkCoreApp m Core.boolImpliesOp [← toCoreExpr a, ← toCoreExpr b] | .ext_equal m ty a b => return ← toCoreExtensionalEq m ty (← toCoreExpr a) (← toCoreExpr b) - | .equal _ _ a b => return .eq () (← toCoreExpr a) (← toCoreExpr b) - | .not_equal _ _ a b => return .app () Core.boolNotOp (.eq () (← toCoreExpr a) (← toCoreExpr b)) + | .equal m _ a b => return .eq m (← toCoreExpr a) (← toCoreExpr b) + | .not_equal m _ a b => return .app m Core.boolNotOp (.eq m (← toCoreExpr a) (← toCoreExpr b)) | .le m ty a b => toCoreTypedBin m ty "Le" (← toCoreExpr a) (← toCoreExpr b) | .lt m ty a b => toCoreTypedBin m ty "Lt" (← toCoreExpr a) (← toCoreExpr b) | .ge m ty a b => toCoreTypedBin m ty "Ge" (← toCoreExpr a) (← toCoreExpr b) @@ -448,27 +450,27 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do | .old _ _ a => return oldifyExpr (← get).currentInoutNames (← toCoreExpr a) -- Sequence operations (Core Grammar, inherited by Boole) - | .seq_length _ _ s => return mkCoreApp Core.seqLengthOp [← toCoreExpr s] - | .seq_select _ _ s i => return mkCoreApp Core.seqSelectOp [← toCoreExpr s, ← toCoreExpr i] - | .seq_take _ _ s n => return mkCoreApp Core.seqTakeOp [← toCoreExpr s, ← toCoreExpr n] - | .seq_drop _ _ s n => return mkCoreApp Core.seqDropOp [← toCoreExpr s, ← toCoreExpr n] - | .seq_append _ _ s1 s2 => return mkCoreApp Core.seqAppendOp [← toCoreExpr s1, ← toCoreExpr s2] - | .seq_build _ _ s v => return mkCoreApp Core.seqBuildOp [← toCoreExpr s, ← toCoreExpr v] - | .seq_update _ _ s i v => return mkCoreApp Core.seqUpdateOp [← toCoreExpr s, ← toCoreExpr i, ← toCoreExpr v] - | .seq_contains _ _ s v => return mkCoreApp Core.seqContainsOp [← toCoreExpr s, ← toCoreExpr v] + | .seq_length m _ s => return mkCoreApp m Core.seqLengthOp [← toCoreExpr s] + | .seq_select m _ s i => return mkCoreApp m Core.seqSelectOp [← toCoreExpr s, ← toCoreExpr i] + | .seq_take m _ s n => return mkCoreApp m Core.seqTakeOp [← toCoreExpr s, ← toCoreExpr n] + | .seq_drop m _ s n => return mkCoreApp m Core.seqDropOp [← toCoreExpr s, ← toCoreExpr n] + | .seq_append m _ s1 s2 => return mkCoreApp m Core.seqAppendOp [← toCoreExpr s1, ← toCoreExpr s2] + | .seq_build m _ s v => return mkCoreApp m Core.seqBuildOp [← toCoreExpr s, ← toCoreExpr v] + | .seq_update m _ s i v => return mkCoreApp m Core.seqUpdateOp [← toCoreExpr s, ← toCoreExpr i, ← toCoreExpr v] + | .seq_contains m _ s v => return mkCoreApp m Core.seqContainsOp [← toCoreExpr s, ← toCoreExpr v] -- Sequence operations (Boole Verus-style additions — not in Core Grammar) -- Sequence.skip(s, n) = drop first n elements -- Sequence.dropFirst(s) = drop first element -- Sequence.subrange(s,lo,hi) = take(drop(s,lo), hi-lo) - | .seq_skip _ _ s n => return mkCoreApp Core.seqDropOp [← toCoreExpr s, ← toCoreExpr n] - | .seq_drop_first _ _ s => return mkCoreApp Core.seqDropOp [← toCoreExpr s, .intConst () 1] - | .seq_subrange _ _ s lo hi => do + | .seq_skip m _ s n => return mkCoreApp m Core.seqDropOp [← toCoreExpr s, ← toCoreExpr n] + | .seq_drop_first m _ s => return mkCoreApp m Core.seqDropOp [← toCoreExpr s, .intConst m 1] + | .seq_subrange m _ s lo hi => do let s' ← toCoreExpr s let lo' ← toCoreExpr lo let hi' ← toCoreExpr hi - let intSub : Core.Expression.Expr := .op () ⟨"Int.Sub", ()⟩ none - return mkCoreApp Core.seqTakeOp - [mkCoreApp Core.seqDropOp [s', lo'], mkCoreApp intSub [hi', lo']] + let intSub : Core.Expression.Expr := .op m ⟨"Int.Sub", ()⟩ none + return mkCoreApp m Core.seqTakeOp + [mkCoreApp m Core.seqDropOp [s', lo'], mkCoreApp m intSub [hi', lo']] | .seq_empty_bv8 _ => return Core.seqEmptyOp (some (.bitvec 8)) | .seq_empty_bv16 _ => return Core.seqEmptyOp (some (.bitvec 16)) | .seq_empty_bv32 _ => return Core.seqEmptyOp (some (.bitvec 32)) @@ -476,31 +478,31 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do | .seq_empty_int _ => return Core.seqEmptyOp (some .int) -- Sequence literals: Sequence.of_bv32[v0, v1, ..., vn] -- Lowers to a left-fold of seq_build over seq_empty. - | .seq_of_bv8 _ ⟨_, vs⟩ | .seq_of_bv16 _ ⟨_, vs⟩ | .seq_of_bv32 _ ⟨_, vs⟩ - | .seq_of_bv64 _ ⟨_, vs⟩ | .seq_of_int _ ⟨_, vs⟩ => do + | .seq_of_bv8 m ⟨_, vs⟩ | .seq_of_bv16 m ⟨_, vs⟩ | .seq_of_bv32 m ⟨_, vs⟩ + | .seq_of_bv64 m ⟨_, vs⟩ | .seq_of_int m ⟨_, vs⟩ => do let vals ← vs.toList.mapM toCoreExpr - return vals.foldl (fun acc v => mkCoreApp Core.seqBuildOp [acc, v]) Core.seqEmptyOp + return vals.foldl (fun acc v => mkCoreApp m Core.seqBuildOp [acc, v]) Core.seqEmptyOp -- Lambda abstraction: `fun x : T => body` → Core .abs - | .lambda _ _ decls body => do + | .lambda m _ decls body => do let declsList := declListToList decls let tys ← declsList.mapM fun (.bind_mk _ _ _ ty) => toCoreMonoType ty - let bvars : Array Core.Expression.Expr := declsList.toArray.mapIdx fun i _ => .bvar () i + let bvars : Array Core.Expression.Expr := declsList.toArray.mapIdx fun i _ => .bvar m i let body' ← withBVarExprs bvars (toCoreExpr body) - return tys.foldr (fun ty acc => .abs () "" (some ty) acc) body' + return tys.foldr (fun ty acc => .abs m "" (some ty) acc) body' -- Function application: `(f)(x)` → Core .app - | .apply_expr _ _ _ f x => return .app () (← toCoreExpr f) (← toCoreExpr x) + | .apply_expr m _ _ f x => return .app m (← toCoreExpr f) (← toCoreExpr x) | _ => throw (.fromMessage s!"Unsupported expression: {repr e}") end -def nestMapSet (base : Core.Expression.Expr) (idxs : List Core.Expression.Expr) (rhs : Core.Expression.Expr) : Core.Expression.Expr := +def nestMapSet (m : SourceRange) (base : Core.Expression.Expr) (idxs : List Core.Expression.Expr) (rhs : Core.Expression.Expr) : Core.Expression.Expr := match idxs with | [] => rhs - | [i] => mkCoreApp Core.mapUpdateOp [base, i, rhs] + | [i] => mkCoreApp m Core.mapUpdateOp [base, i, rhs] | i :: rest => - let innerMap := mkCoreApp Core.mapSelectOp [base, i] - let updatedInner := nestMapSet innerMap rest rhs - mkCoreApp Core.mapUpdateOp [base, i, updatedInner] + let innerMap := mkCoreApp m Core.mapSelectOp [base, i] + let updatedInner := nestMapSet m innerMap rest rhs + mkCoreApp m Core.mapUpdateOp [base, i, updatedInner] def toCoreInvariants (is : BooleDDM.Invariants SourceRange) : TranslateM (List (String × Core.Expression.Expr)) := do @@ -525,11 +527,11 @@ private def forArithOps (ty : Lambda.LMonoTy) : Core.Expression.Expr × Core.Expression.Expr × Core.Expression.Expr × Core.Expression.Expr := match ty with | .bitvec n => - (.op () ⟨s!"Bv{n}.ULe", ()⟩ none, - .op () ⟨s!"Bv{n}.Add", ()⟩ none, - .op () ⟨s!"Bv{n}.Sub", ()⟩ none, - .bitvecConst () n 1) - | _ => (Core.intLeOp, Core.intAddOp, Core.intSubOp, .intConst () 1) + (.op default ⟨s!"Bv{n}.ULe", ()⟩ none, + .op default ⟨s!"Bv{n}.Add", ()⟩ none, + .op default ⟨s!"Bv{n}.Sub", ()⟩ none, + .bitvecConst default n 1) + | _ => (Core.intLeOp, Core.intAddOp, Core.intSubOp, .intConst default 1) def lowerFor (m : SourceRange) @@ -553,8 +555,8 @@ private def lowerVarStatement (m : SourceRange) (ds : BooleDDM.DeclList SourceRa let n := (← get).globalVarCounter modify fun st => { st with globalVarCounter := n + 1 } let initName := mkIdent s!"init_{id.name}_{n}" - newBVarsRev := (.fvar () id none : Core.Expression.Expr) :: newBVarsRev - outRev := Core.Statement.init id ty (.det (.fvar () initName none)) (← toCoreMetaData m) :: outRev + newBVarsRev := (.fvar m id none : Core.Expression.Expr) :: newBVarsRev + outRev := Core.Statement.init id ty (.det (.fvar m initName none)) (← toCoreMetaData m) :: outRev modify fun st => { st with bvars := st.bvars ++ newBVarsRev.reverse.toArray } return outRev.reverse @@ -591,8 +593,9 @@ private def constructProcArgsPrefix (n : String) : TranslateM (List (Core.CallArg Core.Expression)) := do let (modifiesTyped, readOnlyGlobals) ← getGlobalParamPrefix n let modifiesArgs := modifiesTyped.map fun (id, _) => Core.CallArg.inoutArg id + -- Synthesized variable reference for read-only global let readOnlyArgs := readOnlyGlobals.map - fun (id, _) => Core.CallArg.inArg (Lambda.LExpr.fvar () id none : Core.Expression.Expr) + fun (id, _) => Core.CallArg.inArg (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "boole") id none : Core.Expression.Expr) return modifiesArgs ++ readOnlyArgs def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement := do @@ -606,7 +609,7 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement | _ => return .block "var" out (← toCoreMetaData m) | .initStatement m ty ⟨_, n⟩ e => let rhs ← toCoreExpr e - modify fun st => { st with bvars := st.bvars.push (.fvar () (mkIdent n) none) } + modify fun st => { st with bvars := st.bvars.push (.fvar m (mkIdent n) none) } return Core.Statement.init (mkIdent n) (← toCoreType ty) (.det rhs) (← toCoreMetaData m) | .assign m _ lhs rhs => let rec lhsParts (lhs : BooleDDM.Lhs SourceRange) : TranslateM (String × List Core.Expression.Expr) := do @@ -617,8 +620,8 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement return (n, (← toCoreExpr i) :: isRev) let (n, idxsRev) ← lhsParts lhs let idxs := idxsRev.reverse - let base := .fvar () (mkIdent n) none - return Core.Statement.set (mkIdent n) (nestMapSet base idxs (← toCoreExpr rhs)) (← toCoreMetaData m) + let base := .fvar m (mkIdent n) none + return Core.Statement.set (mkIdent n) (nestMapSet m base idxs (← toCoreExpr rhs)) (← toCoreMetaData m) | .assume m ⟨_, l?⟩ e => return Core.Statement.assume (← defaultLabel m "assume" l?) (← toCoreExpr e) (← toCoreMetaData m) | .assert m rc? ⟨_, l?⟩ e => @@ -639,7 +642,7 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement | .condNondet _ => pure .nondet return .ite cond thenb elseb (← toCoreMetaData m) | .choose_assign m ⟨_, lhs⟩ v pred => - let lhsExpr : Core.Expression.Expr := .fvar () (mkIdent lhs) none + let lhsExpr : Core.Expression.Expr := .fvar m (mkIdent lhs) none let predExpr ← withBVarExprs #[lhsExpr] (toCoreExpr pred) let md ← toCoreMetaData m let label ← defaultLabel m "choose" none @@ -649,9 +652,9 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement -- obligation verify as a false positive. let .mono_bind_mk _ _ vTy := v let vMonoTy ← toCoreMonoType vTy - let existsBody ← withBVarExprs #[.bvar () 0] (toCoreExpr pred) + let existsBody ← withBVarExprs #[.bvar m 0] (toCoreExpr pred) let existsExpr : Core.Expression.Expr := - .quant () .exist "" (some vMonoTy) (.bvar () 0) existsBody + .quant m .exist "" (some vMonoTy) (.bvar m 0) existsBody let existenceAssert := Core.Statement.assert s!"{label}_exists" existsExpr md let havocStmt := Core.Statement.havoc (mkIdent lhs) md let assumeStmt := Core.Statement.assume label predExpr md @@ -706,14 +709,14 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement inputsMono.map (fun (id, mty) => (id, .forAll [] mty)) let inputNames := bsList.map bindingName let pair ← (withBVars inputNames do - let mut precondsRev : List (DL.Util.FuncPrecondition Core.Expression.Expr Unit) := [] + let mut precondsRev : List (DL.Util.FuncPrecondition Core.Expression.Expr Core.Expression.ExprMetadata) := [] for p in pres.toList do match p with - | .requires_spec _ _ _ cond => - precondsRev := { expr := ← toCoreExpr cond, md := () } :: precondsRev + | .requires_spec sm _ _ cond => + precondsRev := { expr := ← toCoreExpr cond, md := sm } :: precondsRev | _ => pure () let bodyExpr ← toCoreExpr body - return (precondsRev.reverse, bodyExpr) : TranslateM (List (DL.Util.FuncPrecondition Core.Expression.Expr Unit) × Core.Expression.Expr)) + return (precondsRev.reverse, bodyExpr) : TranslateM (List (DL.Util.FuncPrecondition Core.Expression.Expr Core.Expression.ExprMetadata) × Core.Expression.Expr)) let (preconds, bodyExpr) := pair let funcTy := Lambda.LMonoTy.mkArrow outputMono ((inputsMono.map (·.2)).reverse) let decl : Imperative.PureFunc Core.Expression := { @@ -727,7 +730,7 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement preconditions := preconds } -- Keep function name in local scope for subsequent statements. - modify fun st => { st with bvars := st.bvars.push (.op () (mkIdent n) (some funcTy)) } + modify fun st => { st with bvars := st.bvars.push (.op m (mkIdent n) (some funcTy)) } return .funcDecl decl (← toCoreMetaData m) | .for_statement m v init guard step invs body => let (id, ty) ← toCoreMonoBind v @@ -747,7 +750,7 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement let limitExpr ← toCoreExpr limit withBVars [id.name] do let initExpr ← toCoreExpr init - let guard := mkCoreApp leOp [.fvar () id none, limitExpr] + let guard := mkCoreApp m leOp [.fvar m id none, limitExpr] let stepExpr ← ((match step? with | none => pure one | some (.step _ e) => toCoreExpr e) : TranslateM Core.Expression.Expr) @@ -756,7 +759,7 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement | some (.measure_mk _ e) => return some (← toCoreExpr e)) let body ← withBVars [] (toCoreBlock body) lowerFor m id ty initExpr guard - (mkCoreApp addOp [.fvar () id none, stepExpr]) + (mkCoreApp m addOp [.fvar m id none, stepExpr]) measureExpr (← toCoreInvariants invs) body | .for_down_to_by_statement m v init limit ⟨_, step?⟩ ⟨_, decr?⟩ invs body => let (id, ty) ← toCoreMonoBind v @@ -764,7 +767,7 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement let limitExpr ← toCoreExpr limit withBVars [id.name] do let initExpr ← toCoreExpr init - let guard := mkCoreApp leOp [limitExpr, .fvar () id none] + let guard := mkCoreApp m leOp [limitExpr, .fvar m id none] let stepExpr ← ((match step? with | none => pure one | some (.step _ e) => toCoreExpr e) : TranslateM Core.Expression.Expr) @@ -773,7 +776,7 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement | some (.measure_mk _ e) => return some (← toCoreExpr e)) let body ← withBVars [] (toCoreBlock body) lowerFor m id ty initExpr guard - (mkCoreApp subOp [.fvar () id none, stepExpr]) + (mkCoreApp m subOp [.fvar m id none, stepExpr]) measureExpr (← toCoreInvariants invs) body termination_by SizeOf.sizeOf s @@ -862,7 +865,11 @@ private def lowerPureFuncDef | .casesBinding _ _ _ => true | _ => false let pres ← withBVars inputNames (toCoreSpecElts m n pres) - let pres := pres.preconditions.map (fun (_, c) => ⟨c.expr, ()⟩) + let pres := pres.preconditions.map (fun (_, c) => + let sr := match Imperative.getFileRange c.md with + | some fr => fr.range + | none => ExprSourceLoc.synthesized "boole" + ⟨c.expr, sr⟩) let body ← withBVars inputNames (toCoreExpr body) let measure ← withBVars inputNames (measure?.mapM toCoreExpr) let attr := @@ -992,7 +999,7 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec | some (.measure_mk _ e) => some e | _ => none let siblingBvars := prevNames.map fun sn => - (.op () (mkIdent sn) none : Core.Expression.Expr) + (.op m (mkIdent sn) none : Core.Expression.Expr) let f ← withBVarExprs siblingBvars.toArray (lowerPureFuncDef m n tys bs ret pres body false measureExpr?) return ({ f with isRecursive := true } :: acc, prevNames ++ [n]) diff --git a/Strata/Languages/C_Simp/Verify.lean b/Strata/Languages/C_Simp/Verify.lean index b04c557882..3a003de29b 100644 --- a/Strata/Languages/C_Simp/Verify.lean +++ b/Strata/Languages/C_Simp/Verify.lean @@ -24,17 +24,22 @@ namespace Strata -- 2. Running SymExec of Lambda and Imp +-- C_Simp expressions carry Unit metadata, so translated expressions use synthesized provenance +private abbrev cSimpLoc : ExprSourceLoc := ExprSourceLoc.synthesized "c-simp" + +/-- Translate a C_Simp expression to a Core expression. + C_Simp expressions carry `Unit` metadata, so translated expressions use synthesized provenance. -/ def translate_expr (e : C_Simp.Expression.Expr) : Lambda.LExpr Core.CoreLParams.mono := match e with - | .const m c => .const m c - | .op m o ty => .op m ⟨o.name, ()⟩ ty - | .bvar m n => .bvar m n - | .fvar m n ty => .fvar m ⟨n.name, ()⟩ ty - | .abs m name ty e => .abs m name ty (translate_expr e) - | .quant m k name ty tr e => .quant m k name ty (translate_expr tr) (translate_expr e) - | .app m fn e => .app m (translate_expr fn) (translate_expr e) - | .ite m c t e => .ite m (translate_expr c) (translate_expr t) (translate_expr e) - | .eq m e1 e2 => .eq m (translate_expr e1) (translate_expr e2) + | .const _ c => .const cSimpLoc c + | .op _ o ty => .op cSimpLoc ⟨o.name, ()⟩ ty + | .bvar _ n => .bvar cSimpLoc n + | .fvar _ n ty => .fvar cSimpLoc ⟨n.name, ()⟩ ty + | .abs _ name ty e => .abs cSimpLoc name ty (translate_expr e) + | .quant _ k name ty tr e => .quant cSimpLoc k name ty (translate_expr tr) (translate_expr e) + | .app _ fn e => .app cSimpLoc (translate_expr fn) (translate_expr e) + | .ite _ c t e => .ite cSimpLoc (translate_expr c) (translate_expr t) (translate_expr e) + | .eq _ e1 e2 => .eq cSimpLoc (translate_expr e1) (translate_expr e2) def translate_opt_expr (e : Option C_Simp.Expression.Expr) : Option (Lambda.LExpr Core.CoreLParams.mono) := match e with @@ -85,6 +90,9 @@ Assumption that invariant holds on exit This is suitable for Symbolic Execution, but may not be suitable for other analyses. + +Synthesized expressions (measure checks, guard negations) use `ExprSourceLoc.synthesized "c-simp"` +because they have no corresponding source location. -/ def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement := match s with @@ -94,7 +102,7 @@ def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement := let assigned_vars := (Imperative.Block.modifiedVars body).map (λ s => ⟨s.name, ()⟩) let havocd : Core.Statement := .block "loop havoc" (assigned_vars.map (λ n => Core.Statement.havoc n {})) {} - let measure_pos := (.app () (.app () (coreOpExpr (.numeric ⟨.int, .Ge⟩)) (translate_expr measure)) (.intConst () 0)) + let measure_pos := (.app cSimpLoc (.app cSimpLoc (coreOpExpr (.numeric ⟨.int, .Ge⟩)) (translate_expr measure)) (.intConst cSimpLoc 0)) let entry_invariants : List Core.Statement := invList.mapIdx fun i (_, inv) => .assert s!"entry_invariant_{i}" (translate_expr inv) {} @@ -107,8 +115,8 @@ def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement := ([Core.Statement.assume "assume_guard" (translate_expr guard_expr) {}] ++ inv_assumes ++ [Core.Statement.assume "assume_measure_pos" measure_pos {}]) {} let measure_old_value_assign : Core.Statement := .init "special-name-for-old-measure-value" (.forAll [] (.tcons "int" [])) (.det (translate_expr measure)) {} - let measure_decreases : Core.Statement := .assert "measure_decreases" (.app () (.app () (coreOpExpr (.numeric ⟨.int, .Lt⟩)) (translate_expr measure)) (.fvar () "special-name-for-old-measure-value" none)) {} - let measure_imp_not_guard : Core.Statement := .assert "measure_imp_not_guard" (.ite () (.app () (.app () (coreOpExpr (.numeric ⟨.int, .Le⟩)) (translate_expr measure)) (.intConst () 0)) (.app () (coreOpExpr (.bool .Not)) (translate_expr guard_expr)) (.true ())) {} + let measure_decreases : Core.Statement := .assert "measure_decreases" (.app cSimpLoc (.app cSimpLoc (coreOpExpr (.numeric ⟨.int, .Lt⟩)) (translate_expr measure)) (.fvar cSimpLoc "special-name-for-old-measure-value" none)) {} + let measure_imp_not_guard : Core.Statement := .assert "measure_imp_not_guard" (.ite cSimpLoc (.app cSimpLoc (.app cSimpLoc (coreOpExpr (.numeric ⟨.int, .Le⟩)) (translate_expr measure)) (.intConst cSimpLoc 0)) (.app cSimpLoc (coreOpExpr (.bool .Not)) (translate_expr guard_expr)) Core.true) {} let maintain_invariants : List Core.Statement := invList.mapIdx fun i (_, inv) => .assert s!"arbitrary_iter_maintain_invariant_{i}" (translate_expr inv) {} let body_statements : List Core.Statement := body.map translate_stmt @@ -116,7 +124,7 @@ def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement := ([havocd, arbitrary_iter_assumes, measure_old_value_assign] ++ body_statements ++ [measure_decreases, measure_imp_not_guard] ++ maintain_invariants) {} - let not_guard : Core.Statement := .assume "not_guard" (.app () (coreOpExpr (.bool .Not)) (translate_expr guard_expr)) {} + let not_guard : Core.Statement := .assume "not_guard" (.app cSimpLoc (coreOpExpr (.bool .Not)) (translate_expr guard_expr)) {} let invariant_assumes : List Core.Statement := invList.mapIdx fun i (_, inv) => .assume s!"invariant_{i}" (translate_expr inv) {} @@ -136,7 +144,7 @@ def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement := let body_statements : List Core.Statement := body.map translate_stmt let arbitrary_iter_facts : Core.Statement := .block "arbitrary iter facts" ([havocd, arbitrary_iter_assumes] ++ body_statements ++ maintain_invariants) {} - let not_guard : Core.Statement := .assume "not_guard" (.app () (coreOpExpr (.bool .Not)) (translate_expr guard_expr)) {} + let not_guard : Core.Statement := .assume "not_guard" (.app cSimpLoc (coreOpExpr (.bool .Not)) (translate_expr guard_expr)) {} let invariant_assumes : List Core.Statement := invList.mapIdx fun i (_, inv) => .assume s!"invariant_{i}" (translate_expr inv) {} .ite (.det (translate_expr guard_expr)) ([first_iter_facts, arbitrary_iter_facts, havocd, not_guard] ++ invariant_assumes) [] {} diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index 860e36a841..72ca073917 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -722,6 +722,10 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres | _, q`Core.re_none => return Core.reNoneOp | _, _ => TransM.error s!"translateFn: Unknown/unimplemented function {repr q} at type {repr ty?}" +/-- Build the URI for the current translation unit. -/ +private def getUri : TransM Uri := do + return .file (← StateT.get).inputCtx.fileName + mutual /-- Shared binding setup for lambdas and quantifiers: translates the declaration list, @@ -733,7 +737,8 @@ def withScopedBindings TransM (ListMap Core.Expression.Ident Core.Expression.Ty × TransBindings × Core.Expression.Expr) := do let xsArray ← translateDeclList bindings xsa let n := xsArray.size - let newBoundVars := List.toArray (xsArray.mapIdx (fun i _ => LExpr.bvar () (n - 1 - i))) + let m := ExprSourceLoc.ofUriRange (← getUri) xsa.ann + let newBoundVars := List.toArray (xsArray.mapIdx (fun i _ => LExpr.bvar m (n - 1 - i))) let boundVars' := bindings.boundVars ++ newBoundVars let xbindings := { bindings with boundVars := boundVars' } let b ← translateExpr p xbindings bodya @@ -745,10 +750,11 @@ def translateLambda (bindings : TransBindings) (xsa : Arg) (bodya : Arg) : TransM Core.Expression.Expr := do let (xsArray, _, b) ← withScopedBindings p bindings xsa bodya + let m := ExprSourceLoc.ofUriRange (← getUri) xsa.ann let buildLambda := fun (name, ty) e => match ty with | .forAll [] mty => - .abs () name.name (.some mty) e + .abs m name.name (.some mty) e | _ => panic! s!"Expected monomorphic type in lambda, got: {ty}" -- nopanic:ok return xsArray.foldr buildLambda (init := b) @@ -759,10 +765,11 @@ def translateQuantifier (bindings : TransBindings) (xsa : Arg) (triggersa: Option Arg) (bodya: Arg) : TransM Core.Expression.Expr := do let (xsArray, xbindings, b) ← withScopedBindings p bindings xsa bodya + let m := ExprSourceLoc.ofUriRange (← getUri) xsa.ann -- Handle triggers if present let triggers ← match triggersa with - | none => pure (LExpr.noTrigger ()) + | none => pure (LExpr.noTrigger m) | some tsa => translateTriggers p xbindings tsa -- Create one quantifier constructor per variable @@ -773,8 +780,8 @@ def translateQuantifier let triggers := if first then triggers else - LExpr.noTrigger () - (.quant () qk name.name (.some mty) triggers e, false) + LExpr.noTrigger m + (.quant m qk name.name (.some mty) triggers e, false) | _ => panic! s!"Expected monomorphic type in quantifier, got: {ty}" return xsArray.foldr buildQuantifier (init := (b, true)) |>.1 @@ -784,10 +791,11 @@ def translateTriggerGroup (p: Program) (bindings : TransBindings) (arg : Arg) : TransM Core.Expression.Expr := do let .op op := arg | TransM.error s!"translateTriggerGroup expected op, got {repr arg}" + let m := ExprSourceLoc.ofUriRange (← getUri) op.ann match op.name, op.args with | q`Core.trigger, #[tsa] => do let ts ← translateCommaSep (fun t => translateExpr p bindings t) tsa - return ts.foldl (fun g t => .app () (.app () Core.addTriggerOp t) g) Core.emptyTriggerGroupOp + return ts.foldl (fun g t => .app m (.app m Core.addTriggerOp t) g) Core.emptyTriggerGroupOp | _, _ => panic! s!"Unexpected operator in trigger group" partial @@ -795,14 +803,15 @@ def translateTriggers (p: Program) (bindings : TransBindings) (arg : Arg) : TransM Core.Expression.Expr := do let .op op := arg | TransM.error s!"translateTriggers expected op, got: {repr arg}" + let m := ExprSourceLoc.ofUriRange (← getUri) op.ann match op.name, op.args with | q`Core.triggersAtom, #[group] => let g ← translateTriggerGroup p bindings group - return .app () (.app () Core.addTriggerGroupOp g) Core.emptyTriggersOp + return .app m (.app m Core.addTriggerGroupOp g) Core.emptyTriggersOp | q`Core.triggersPush, #[triggers, group] => do let ts ← translateTriggers p bindings triggers let g ← translateTriggerGroup p bindings group - return .app () (.app () Core.addTriggerGroupOp g) ts + return .app m (.app m Core.addTriggerGroupOp g) ts | _, _ => panic! s!"Unexpected operator in trigger" /-- Resolve a function from a `recFuncBlock` by its global-context index. -/ @@ -819,58 +828,60 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : TransM Core.Expression.Expr := do let .expr expr := arg | TransM.error s!"translateExpr expected expr {repr arg}" + let uri ← getUri + let loc (sr : SourceRange) : ExprSourceLoc := ExprSourceLoc.ofUriRange uri sr let (op, args) := expr.flatten match op, args with -- Constants/Literals - | .fn _ q`Core.btrue, [] => - return .true () - | .fn _ q`Core.bfalse, [] => - return .false () - | .fn _ q`Core.natToInt, [xa] => + | .fn m q`Core.btrue, [] => + return .boolConst (loc m) true + | .fn m q`Core.bfalse, [] => + return .boolConst (loc m) false + | .fn m q`Core.natToInt, [xa] => let n ← translateNat xa - return .intConst () n - | .fn _ q`Core.bv1Lit, [xa] => + return .intConst (loc m) n + | .fn m q`Core.bv1Lit, [xa] => let n ← translateBitVec 1 xa - return .bitvecConst () 1 n - | .fn _ q`Core.bv8Lit, [xa] => + return .bitvecConst (loc m) 1 n + | .fn m q`Core.bv8Lit, [xa] => let n ← translateBitVec 8 xa - return .bitvecConst () 8 n - | .fn _ q`Core.bv16Lit, [xa] => + return .bitvecConst (loc m) 8 n + | .fn m q`Core.bv16Lit, [xa] => let n ← translateBitVec 16 xa - return .bitvecConst () 16 n - | .fn _ q`Core.bv32Lit, [xa] => + return .bitvecConst (loc m) 16 n + | .fn m q`Core.bv32Lit, [xa] => let n ← translateBitVec 32 xa - return .bitvecConst () 32 n - | .fn _ q`Core.bv64Lit, [xa] => + return .bitvecConst (loc m) 32 n + | .fn m q`Core.bv64Lit, [xa] => let n ← translateBitVec 64 xa - return .bitvecConst () 64 n - | .fn _ q`Core.strLit, [xa] => + return .bitvecConst (loc m) 64 n + | .fn m q`Core.strLit, [xa] => let x ← translateStr xa - return .strConst () x - | .fn _ q`Core.realLit, [xa] => + return .strConst (loc m) x + | .fn m q`Core.realLit, [xa] => let x ← translateReal xa - return .realConst () (Strata.Decimal.toRat x) + return .realConst (loc m) (Strata.Decimal.toRat x) -- Equality - | .fn _ q`Core.equal, [_tpa, xa, ya] => + | .fn m q`Core.equal, [_tpa, xa, ya] => let x ← translateExpr p bindings xa let y ← translateExpr p bindings ya - return .eq () x y - | .fn _ q`Core.not_equal, [_tpa, xa, ya] => + return .eq (loc m) x y + | .fn m q`Core.not_equal, [_tpa, xa, ya] => let x ← translateExpr p bindings xa let y ← translateExpr p bindings ya - return (.app () Core.boolNotOp (.eq () x y)) - | .fn _ q`Core.bvnot, [tpa, xa] => + return (.app (loc m) Core.boolNotOp (.eq (loc m) x y)) + | .fn m q`Core.bvnot, [tpa, xa] => let tp ← translateLMonoTy bindings (dealiasTypeArg p tpa) let x ← translateExpr p bindings xa let fn : LExpr Core.CoreLParams.mono ← translateFn (.some tp) q`Core.bvnot - return (.app () fn x) + return (.app (loc m) fn x) -- If-then-else expression - | .fn _ q`Core.if, [_tpa, ca, ta, fa] => + | .fn m q`Core.if, [_tpa, ca, ta, fa] => let c ← translateExpr p bindings ca let t ← translateExpr p bindings ta let f ← translateExpr p bindings fa - return .ite () c t f + return .ite (loc m) c t f -- Re.AllChar | .fn _ q`Core.re_allchar, [] => let fn ← translateFn .none q`Core.re_allchar @@ -891,7 +902,7 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : (.some (Core.seqTy ety)) return fn -- Unary function applications - | .fn _ fni, [xa] => + | .fn m fni, [xa] => match fni with | q`Core.not | q`Core.bvextract_7_7 @@ -910,77 +921,77 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : | q`Core.re_comp => do let fn ← translateFn .none fni let x ← translateExpr p bindings xa - return .mkApp () fn [x] + return .mkApp (loc m) fn [x] | _ => TransM.error s!"translateExpr unimplemented {repr op} {repr args}" - | .fn _ q`Core.neg_expr, [tpa, xa] => + | .fn m q`Core.neg_expr, [tpa, xa] => let ty ← translateLMonoTy bindings (dealiasTypeArg p tpa) let fn ← translateFn ty q`Core.neg_expr let x ← translateExpr p bindings xa - return .mkApp () fn [x] - | .fn _ q`Core.safeneg_expr, [tpa, xa] => + return .mkApp (loc m) fn [x] + | .fn m q`Core.safeneg_expr, [tpa, xa] => let ty ← translateLMonoTy bindings (dealiasTypeArg p tpa) let fn ← translateFn ty q`Core.safeneg_expr let x ← translateExpr p bindings xa - return .mkApp () fn [x] - | .fn _ q`Core.bv_neg_overflow, [tpa, xa] => + return .mkApp (loc m) fn [x] + | .fn m q`Core.bv_neg_overflow, [tpa, xa] => let ty ← translateLMonoTy bindings (dealiasTypeArg p tpa) let fn ← translateFn ty q`Core.bv_neg_overflow let x ← translateExpr p bindings xa - return .mkApp () fn [x] - | .fn _ q`Core.bv_uneg_overflow, [tpa, xa] => + return .mkApp (loc m) fn [x] + | .fn m q`Core.bv_uneg_overflow, [tpa, xa] => let ty ← translateLMonoTy bindings (dealiasTypeArg p tpa) let fn ← translateFn ty q`Core.bv_uneg_overflow let x ← translateExpr p bindings xa - return .mkApp () fn [x] + return .mkApp (loc m) fn [x] -- Strings - | .fn _ q`Core.str_concat, [xa, ya] => + | .fn m q`Core.str_concat, [xa, ya] => let x ← translateExpr p bindings xa let y ← translateExpr p bindings ya - return .mkApp () Core.strConcatOp [x, y] - | .fn _ q`Core.str_substr, [xa, ia, na] => + return .mkApp (loc m) Core.strConcatOp [x, y] + | .fn m q`Core.str_substr, [xa, ia, na] => let x ← translateExpr p bindings xa let i ← translateExpr p bindings ia let n ← translateExpr p bindings na - return .mkApp () Core.strSubstrOp [x, i, n] + return .mkApp (loc m) Core.strSubstrOp [x, i, n] | .fn _ q`Core.old, [_tp, xa] => let x ← translateExpr p bindings xa match x with - | .fvar m ident ty => return .fvar m (Core.CoreIdent.mkOld ident.name) ty + | .fvar m' ident ty => return .fvar m' (Core.CoreIdent.mkOld ident.name) ty | _ => TransM.error s!"old: expected an identifier, got {x}" - | .fn _ q`Core.map_get, [_ktp, _vtp, ma, ia] => + | .fn m q`Core.map_get, [_ktp, _vtp, ma, ia] => let kty ← translateLMonoTy bindings _ktp let vty ← translateLMonoTy bindings _vtp -- TODO: use Core.mapSelectOp, but specialized let fn : LExpr Core.CoreLParams.mono := (Core.coreOpExpr (.map .Select) (.some (LMonoTy.mkArrow (Core.mapTy kty vty) [kty, vty]))) - let m ← translateExpr p bindings ma + let mv ← translateExpr p bindings ma let i ← translateExpr p bindings ia - return .mkApp () fn [m, i] - | .fn _ q`Core.map_set, [_ktp, _vtp, ma, ia, xa] => + return .mkApp (loc m) fn [mv, i] + | .fn m q`Core.map_set, [_ktp, _vtp, ma, ia, xa] => let kty ← translateLMonoTy bindings _ktp let vty ← translateLMonoTy bindings _vtp -- TODO: use Core.mapUpdateOp, but specialized let fn : LExpr Core.CoreLParams.mono := (Core.coreOpExpr (.map .Update) (.some (LMonoTy.mkArrow (Core.mapTy kty vty) [kty, vty, Core.mapTy kty vty]))) - let m ← translateExpr p bindings ma + let mv ← translateExpr p bindings ma let i ← translateExpr p bindings ia let x ← translateExpr p bindings xa - return .mkApp () fn [m, i, x] + return .mkApp (loc m) fn [mv, i, x] -- Seq operations - | .fn _ q`Core.seq_length, [_atp, sa] => + | .fn m q`Core.seq_length, [_atp, sa] => let ety ← translateLMonoTy bindings _atp let fn : LExpr Core.CoreLParams.mono := Core.coreOpExpr (.seq .Length) (.some (LMonoTy.mkArrow (Core.seqTy ety) [.int])) let s ← translateExpr p bindings sa - return .mkApp () fn [s] - | .fn _ q`Core.seq_select, [_atp, sa, ia] => + return .mkApp (loc m) fn [s] + | .fn m q`Core.seq_select, [_atp, sa, ia] => let ety ← translateLMonoTy bindings _atp let fn : LExpr Core.CoreLParams.mono := Core.coreOpExpr (.seq .Select) (.some (LMonoTy.mkArrow (Core.seqTy ety) [.int, ety])) let s ← translateExpr p bindings sa let i ← translateExpr p bindings ia - return .mkApp () fn [s, i] - | .fn _ q`Core.seq_append, [_atp, s1a, s2a] => + return .mkApp (loc m) fn [s, i] + | .fn m q`Core.seq_append, [_atp, s1a, s2a] => let ety ← translateLMonoTy bindings _atp let fn : LExpr Core.CoreLParams.mono := Core.coreOpExpr (.seq .Append) @@ -988,16 +999,16 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : [Core.seqTy ety, Core.seqTy ety])) let s1 ← translateExpr p bindings s1a let s2 ← translateExpr p bindings s2a - return .mkApp () fn [s1, s2] - | .fn _ q`Core.seq_build, [_atp, sa, va] => + return .mkApp (loc m) fn [s1, s2] + | .fn m q`Core.seq_build, [_atp, sa, va] => let ety ← translateLMonoTy bindings _atp let fn : LExpr Core.CoreLParams.mono := Core.coreOpExpr (.seq .Build) (.some (LMonoTy.mkArrow (Core.seqTy ety) [ety, Core.seqTy ety])) let s ← translateExpr p bindings sa let v ← translateExpr p bindings va - return .mkApp () fn [s, v] - | .fn _ q`Core.seq_update, [_atp, sa, ia, va] => + return .mkApp (loc m) fn [s, v] + | .fn m q`Core.seq_update, [_atp, sa, ia, va] => let ety ← translateLMonoTy bindings _atp let fn : LExpr Core.CoreLParams.mono := Core.coreOpExpr (.seq .Update) @@ -1006,16 +1017,16 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : let s ← translateExpr p bindings sa let i ← translateExpr p bindings ia let v ← translateExpr p bindings va - return .mkApp () fn [s, i, v] - | .fn _ q`Core.seq_contains, [_atp, sa, va] => + return .mkApp (loc m) fn [s, i, v] + | .fn m q`Core.seq_contains, [_atp, sa, va] => let ety ← translateLMonoTy bindings _atp let fn : LExpr Core.CoreLParams.mono := Core.coreOpExpr (.seq .Contains) (.some (LMonoTy.mkArrow (Core.seqTy ety) [ety, .bool])) let s ← translateExpr p bindings sa let v ← translateExpr p bindings va - return .mkApp () fn [s, v] - | .fn _ q`Core.seq_take, [_atp, sa, na] => + return .mkApp (loc m) fn [s, v] + | .fn m q`Core.seq_take, [_atp, sa, na] => let ety ← translateLMonoTy bindings _atp let fn : LExpr Core.CoreLParams.mono := Core.coreOpExpr (.seq .Take) @@ -1023,8 +1034,8 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : [.int, Core.seqTy ety])) let s ← translateExpr p bindings sa let n ← translateExpr p bindings na - return .mkApp () fn [s, n] - | .fn _ q`Core.seq_drop, [_atp, sa, na] => + return .mkApp (loc m) fn [s, n] + | .fn m q`Core.seq_drop, [_atp, sa, na] => let ety ← translateLMonoTy bindings _atp let fn : LExpr Core.CoreLParams.mono := Core.coreOpExpr (.seq .Drop) @@ -1032,15 +1043,15 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : [.int, Core.seqTy ety])) let s ← translateExpr p bindings sa let n ← translateExpr p bindings na - return .mkApp () fn [s, n] + return .mkApp (loc m) fn [s, n] -- Lambda abstraction | .fn _ q`Core.lambda, [_, xsa, ba] => translateLambda p bindings xsa ba -- Expression application: (f)(x) - | .fn _ q`Core.apply_expr, [_, _, fa, xa] => do + | .fn m q`Core.apply_expr, [_, _, fa, xa] => do let f ← translateExpr p bindings fa let x ← translateExpr p bindings xa - return .app () f x + return .app (loc m) f x -- Quantifiers | .fn _ q`Core.forall, [xsa, ba] => translateQuantifier .all p bindings xsa .none ba @@ -1051,19 +1062,19 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : | .fn _ q`Core.existsT, [xsa, tsa, ba] => translateQuantifier .exist p bindings xsa (.some tsa) ba -- Binary function applications (monomorphic) - | .fn _ fni, [xa, ya] => + | .fn m fni, [xa, ya] => let fn ← translateFn .none fni let x ← translateExpr p bindings xa let y ← translateExpr p bindings ya - return .mkApp () fn [x, y] - | .fn _ q`Core.re_loop, [xa, ya, za] => + return .mkApp (loc m) fn [x, y] + | .fn m q`Core.re_loop, [xa, ya, za] => let fn ← translateFn .none q`Core.re_loop let x ← translateExpr p bindings xa let y ← translateExpr p bindings ya let z ← translateExpr p bindings za - return .mkApp () fn [x, y, z] + return .mkApp (loc m) fn [x, y, z] -- Binary function applications (polymorphic) - | .fn _ fni, [tpa, xa, ya] => + | .fn m fni, [tpa, xa, ya] => match fni with | q`Core.add_expr | q`Core.sub_expr @@ -1111,21 +1122,21 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : let fn ← translateFn (.some ty) fni let x ← translateExpr p bindings xa let y ← translateExpr p bindings ya - return .mkApp () fn [x, y] + return .mkApp (loc m) fn [x, y] | _ => TransM.error s!"translateExpr unimplemented {repr op} {repr args}" -- NOTE: Bound and free variables are numbered differently. Bound variables -- ascending order (so closer to deBrujin levels). - | .bvar _ i, argsa => do + | .bvar m i, argsa => do if i < bindings.boundVars.size then let expr := bindings.boundVars[bindings.boundVars.size - (i+1)]! match argsa with | [] => match expr with - | .bvar m _ => return .bvar m i + | .bvar _ _ => return .bvar (loc m) i | _ => return expr | _ => let args ← translateExprs p bindings argsa.toArray - return .mkApp () expr args.toList + return .mkApp (loc m) expr args.toList else -- Bound variable index exceeds boundVars - check if it's a local function let funcIndex := i - bindings.boundVars.size @@ -1137,18 +1148,18 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : | [] => return func.opExpr | _ => let args ← translateExprs p bindings argsa.toArray - return .mkApp () func.opExpr args.toList + return .mkApp (loc m) func.opExpr args.toList | .recFuncBlock funcs _md => let func ← resolveRecFunc funcs funcIndex match argsa with | [] => return func.opExpr | _ => let args ← translateExprs p bindings argsa.toArray - return .mkApp () func.opExpr args.toList + return .mkApp (loc m) func.opExpr args.toList | _ => TransM.error s!"translateExpr out-of-range bound variable: {i}" else TransM.error s!"translateExpr out-of-range bound variable: {i}" - | .fvar _ i, [] => + | .fvar m i, [] => assert! i < bindings.freeVars.size let decl := bindings.freeVars[i]! let ty? ← match p.globalContext.kindOf! i with @@ -1157,24 +1168,24 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : match decl with | .func func _md => -- 0-ary Function - return (.op () func.name ty?) + return (.op (loc m) func.name ty?) | .recFuncBlock funcs _md => let func ← resolveRecFunc funcs i - return (.op () func.name ty?) + return (.op (loc m) func.name ty?) | _ => TransM.error s!"translateExpr unimplemented fvar decl (no args): {format decl}" - | .fvar _ i, argsa => + | .fvar m i, argsa => -- Call of a function declared/defined in Core. assert! i < bindings.freeVars.size let decl := bindings.freeVars[i]! match decl with | .func func _md => let args ← translateExprs p bindings argsa.toArray - return .mkApp () func.opExpr args.toList + return .mkApp (loc m) func.opExpr args.toList | .recFuncBlock funcs _md => let func ← resolveRecFunc funcs i let args ← translateExprs p bindings argsa.toArray - return .mkApp () func.opExpr args.toList + return .mkApp (loc m) func.opExpr args.toList | _ => TransM.error s!"translateExpr unimplemented fvar decl: {format decl} \nargs:{repr argsa}" | op, args => @@ -1238,7 +1249,7 @@ def initVarStmts (tpids : ListMap Core.Expression.Ident LTy) (bindings : TransBi return ((s :: stmts), bindings) def translateVarStatement (bindings : TransBindings) (decls : Array Arg) - (md : MetaData Core.Expression): + (md : MetaData Core.Expression) (sr : SourceRange): TransM ((List Core.Statement) × TransBindings) := do if decls.size != 1 then TransM.error s!"translateVarStatement unexpected decls length {repr decls}" @@ -1247,14 +1258,14 @@ def translateVarStatement (bindings : TransBindings) (decls : Array Arg) let (stmts, bindings) ← initVarStmts tpids bindings md let newVars ← tpids.mapM (fun (id, ty) => if h: ty.isMonoType then - return ((LExpr.fvar () id (ty.toMonoType h)): LExpr Core.CoreLParams.mono) + return ((LExpr.fvar sr id (ty.toMonoType h)): LExpr Core.CoreLParams.mono) else TransM.error s!"translateVarStatement requires {id} to have a monomorphic type, but it has type {ty}") let bbindings := bindings.boundVars ++ newVars return (stmts, { bindings with boundVars := bbindings }) def translateInitStatement (p : Program) (bindings : TransBindings) (args : Array Arg) - (md : MetaData Core.Expression): + (md : MetaData Core.Expression) (sr : SourceRange): TransM ((List Core.Statement) × TransBindings) := do if args.size != 3 then TransM.error "translateInitStatement unexpected arg length {repr decls}" @@ -1263,7 +1274,7 @@ def translateInitStatement (p : Program) (bindings : TransBindings) (args : Arra let lhs ← translateIdent Core.CoreIdent args[1]! let val ← translateExpr p bindings args[2]! let ty := (.forAll [] mty) - let newBinding: LExpr Core.CoreLParams.mono := LExpr.fvar () lhs mty + let newBinding: LExpr Core.CoreLParams.mono := LExpr.fvar sr lhs mty let bbindings := bindings.boundVars ++ [newBinding] return ([.init lhs ty (.det val) md], { bindings with boundVars := bbindings }) @@ -1288,17 +1299,17 @@ private def translateCondBool (p : Program) (bindings : TransBindings) (a : Arg) /-- Build a nested map-update expression: `nestMapUpdate base [i1, i2] v` produces `map_update(base, i1, map_update(map_select(base, i1), i2, v))`. -/ -private def nestMapUpdate (base : Core.Expression.Expr) (idxs : List Core.Expression.Expr) +private def nestMapUpdate (m : Core.ExpressionMetadata) (base : Core.Expression.Expr) (idxs : List Core.Expression.Expr) (rhs : Core.Expression.Expr) : Core.Expression.Expr := let selectOp := Core.coreOpExpr (.map .Select) let updateOp := Core.coreOpExpr (.map .Update) match idxs with | [] => rhs - | [i] => .mkApp () updateOp [base, i, rhs] + | [i] => .mkApp m updateOp [base, i, rhs] | i :: rest => - let inner := .mkApp () selectOp [base, i] - let updatedInner := nestMapUpdate inner rest rhs - .mkApp () updateOp [base, i, updatedInner] + let inner := .mkApp m selectOp [base, i] + let updatedInner := nestMapUpdate m inner rest rhs + .mkApp m updateOp [base, i, updatedInner] /-- Decompose an LHS into a base identifier and a (reversed) list of index expressions. For `m[k1][k2]`, returns `(m, [k2, k1])`. -/ @@ -1331,7 +1342,7 @@ partial def translateFnPreconds (p : Program) (name : Core.CoreIdent) (bindings let args ← checkOpArg specElt q`Core.requires_spec 3 let _l ← translateOptionLabel s!"{name.name}_requires_{count}" args[0]! let e ← translateExpr p bindings args[2]! - return (acc ++ [⟨e, ()⟩], count + 1) + return (acc ++ [⟨e, ExprSourceLoc.ofUriRange (← getUri) op.ann⟩], count + 1) | _ => TransM.error s!"translateFnPreconds: only requires allowed, got {repr op.name}" return preconds.1 @@ -1342,16 +1353,16 @@ partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) : match op.name, op.args with | q`Core.varStatement, declsa => - translateVarStatement bindings declsa (← getOpMetaData op) + translateVarStatement bindings declsa (← getOpMetaData op) op.ann | q`Core.initStatement, args => - translateInitStatement p bindings args (← getOpMetaData op) + translateInitStatement p bindings args (← getOpMetaData op) op.ann | q`Core.assign, #[_tpa, lhsa, ea] => let (lhs, idxsRev) ← translateLhsParts p bindings lhsa let val ← translateExpr p bindings ea let md ← getOpMetaData op let rhs := match idxsRev.reverse with | [] => val - | idxs => nestMapUpdate (.fvar () lhs none) idxs val + | idxs => nestMapUpdate op.ann (.fvar op.ann lhs none) idxs val return ([.set lhs rhs md], bindings) | q`Core.havoc_statement, #[ida] => let id ← translateIdent Core.CoreIdent ida @@ -1439,8 +1450,8 @@ partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) : -- The function name is NOT in scope inside the body (declareFn adds it -- for subsequent statements only). So body bindings = outer + parameters. let funcType := Lambda.LMonoTy.mkArrow outputMono (inputs.values.reverse) - let funcBinding : LExpr Core.CoreLParams.mono := .op () name (some funcType) - let in_bindings := (inputs.map (fun (v, ty) => (LExpr.fvar () v ty))).toArray + let funcBinding : LExpr Core.CoreLParams.mono := .op op.ann name (some funcType) + let in_bindings := (inputs.map (fun (v, ty) => (LExpr.fvar op.ann v ty))).toArray let bodyBindings := { bindings with boundVars := bindings.boundVars ++ in_bindings } -- Translate preconditions @@ -1649,9 +1660,9 @@ def translateProcedure (p : Program) (bindings : TransBindings) (op : Operation) let pname ← translateIdent Core.CoreIdent op.args[0]! let typeArgs ← translateTypeArgs op.args[1]! let (sig, ret) ← translateBindingsPartitioned bindings op.args[2]! - let in_bindings := (sig.map (fun (v, ty) => (LExpr.fvar () v ty))).toArray + let in_bindings := (sig.map (fun (v, ty) => (LExpr.fvar op.ann v ty))).toArray let out_bindings_only := (ret.filter (fun (v, _) => !sig.any (fun (iv, _) => iv == v))).map - (fun (v, ty) => (LExpr.fvar () v ty)) + (fun (v, ty) => (LExpr.fvar op.ann v ty)) let out_bindings := out_bindings_only.toArray let origBindings := bindings let bbindings := bindings.boundVars ++ in_bindings ++ out_bindings @@ -1762,7 +1773,7 @@ def translateFunction (status : FnInterp) (p : Program) (bindings : TransBinding let typeArgs ← translateTypeArgs op.args[1]! let sig ← translateBindings bindings op.args[2]! let ret ← translateLMonoTy bindings op.args[3]! - let in_bindings := (sig.map (fun (v, ty) => (LExpr.fvar () v ty))).toArray + let in_bindings := (sig.map (fun (v, ty) => (LExpr.fvar op.ann v ty))).toArray let orig_bbindings := bindings.boundVars let bbindings := bindings.boundVars ++ in_bindings let bindings := { bindings with boundVars := bbindings } @@ -1809,12 +1820,12 @@ partial def translateRecFnDecl (p : Program) (preBindings : TransBindings) let typeArgs ← translateTypeArgs fnOp.args[1]! let (sig, casesIdx) ← translateBindingsWithCases preBindings fnOp.args[2]! let ret ← translateLMonoTy preBindings fnOp.args[3]! - let in_bindings := (sig.map (fun (v, ty) => (LExpr.fvar () v ty))).toArray + let in_bindings := (sig.map (fun (v, ty) => (LExpr.fvar fnOp.ann v ty))).toArray -- Build boundVars matching the DDM elaborator's typing context. -- @[declareFn] accumulates sibling bvars across NewlineSepBy children. -- Self-reference goes through fvar (from @[preRegisterFunctions]), not bvar. let tyArgPlaceholders := typeArgs.map fun (ta : TyIdentifier) => - LExpr.op () (ta : Core.CoreIdent) .none + LExpr.op fnOp.ann (ta : Core.CoreIdent) .none let bbindings := preBindings.boundVars ++ siblingExprs ++ tyArgPlaceholders ++ in_bindings let bodyBindings := { preBindings with boundVars := bbindings } let casesAttr := match casesIdx with diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean index 3bf5f082e9..c1cb268dd6 100644 --- a/Strata/Languages/Core/Env.lean +++ b/Strata/Languages/Core/Env.lean @@ -3,6 +3,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +-- Synthesized expressions for environment operations and path conditions module public import Strata.Languages.Core.Program @@ -17,7 +18,7 @@ open Imperative open Strata instance : ToFormat ExpressionMetadata := - show ToFormat Unit from inferInstance + show ToFormat ExprSourceLoc from inferInstance -- ToFormat instance for Expression.Expr instance : ToFormat Expression.Expr := by @@ -40,13 +41,35 @@ instance : ToFormat (Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr)) w format := formatScope instance : Inhabited ExpressionMetadata := - show Inhabited Unit from inferInstance + show Inhabited ExprSourceLoc from inferInstance +-- When combining provenance during evaluation, use the Original expression's +-- source location as primary and collect other non-none locations as related, +-- so that both the original expression and the substituted argument can be reported. instance : Lambda.Traceable Lambda.LExpr.EvalProvenance ExpressionMetadata where - combine _ := () + combine reasons := + let findLoc (prov : Lambda.LExpr.EvalProvenance) : Option ExprSourceLoc := + reasons.find? (fun p => match p.1, prov with + | .Original, .Original | .ReplacementVar, .ReplacementVar + | .Abstraction, .Abstraction => true + | _, _ => false) |>.map (·.2) + -- Pick the primary location: prefer Original > ReplacementVar > Abstraction + let priority := [.Original, .ReplacementVar, .Abstraction] + match priority.findSome? findLoc with + | none => ExprSourceLoc.synthesized "env" + | some primaryLoc => + -- Collect related locations from all other non-none provenance entries, + -- including their own relatedLocs. + let related := priority.foldl (init := primaryLoc.relatedLocs) fun acc prov => + match findLoc prov with + | some loc => + if loc == primaryLoc then acc + else (loc.uri, loc.range) :: (loc.relatedLocs ++ acc) + | none => acc + { primaryLoc with relatedLocs := related } instance : Inhabited (Lambda.LExpr ⟨⟨ExpressionMetadata, CoreIdent⟩, LMonoTy⟩) := - show Inhabited (Lambda.LExpr ⟨⟨Unit, CoreIdent⟩, LMonoTy⟩) from inferInstance + show Inhabited (Lambda.LExpr ⟨⟨ExprSourceLoc, CoreIdent⟩, LMonoTy⟩) from inferInstance --------------------------------------------------------------------- @@ -292,14 +315,14 @@ def Env.genVars (xs : List String) (σ : Lambda.LState CoreLParams) : (List Core /-- Generate a fresh variable using the base name and pre-existing type, if any, -from `xt`. +from `xt`. Synthesized variable references carry no source location. -/ def Env.genFVar (E : Env) (xt : (Lambda.IdentT Lambda.LMonoTy Unit)) : Expression.Expr × Env := let (xid, E) := E.genVar xt.ident let xe := match xt.ty? with - | none => .fvar () xid none - | some xty => .fvar () xid (some xty) + | none => .fvar (ExprSourceLoc.synthesized "env") xid none + | some xty => .fvar (ExprSourceLoc.synthesized "env") xid (some xty) (xe, E) /-- @@ -321,28 +344,31 @@ def Env.genFVars (E : Env) (xs : List (Lambda.IdentT Lambda.LMonoTy Unit)) : /-- Insert `(xi, .fvar xi)`, for each `xi` in `xs`, in the _oldest_ scope in `ss`, only if `xi` is the identifier of a free variable, i.e., it is not in `ss`. +Synthesized variable references carry no source location. -/ def Env.insertFreeVarsInOldestScope (xs : List (Lambda.IdentT Lambda.LMonoTy Unit)) (E : Env) : Env := let (xis, xtyei) := xs.foldl (fun (acc_ids, acc_pairs) x => - (x.fst :: acc_ids, (x.snd, .fvar () x.fst x.snd) :: acc_pairs)) + (x.fst :: acc_ids, (x.snd, .fvar (ExprSourceLoc.synthesized "env") x.fst x.snd) :: acc_pairs)) ([], []) let state' := Maps.addInOldest E.exprEnv.state xis xtyei { E with exprEnv := { E.exprEnv with state := state' }} +-- Synthesized path condition logic open Imperative Lambda in def PathCondition.merge (cond : Expression.Expr) (pc1 pc2 : PathCondition Expression) : PathCondition Expression := let wrapAssumption (ant : Expression.Expr) : PathConditionEntry Expression → PathConditionEntry Expression | .assumption label e => .assumption label (mkImplies ant e) | entry => entry - let negCond := LExpr.ite () cond (LExpr.false ()) (LExpr.true ()) + let envLoc := ExprSourceLoc.synthesized "env" + let negCond := LExpr.ite envLoc cond (LExpr.boolConst envLoc false) (LExpr.boolConst envLoc true) let pc1' := pc1.map (wrapAssumption cond) let pc2' := pc2.map (wrapAssumption negCond) pc1' ++ pc2' where mkImplies (ant con : Expression.Expr) : Expression.Expr := - LExpr.ite () ant con (LExpr.true ()) + LExpr.ite (ExprSourceLoc.synthesized "env") ant con (LExpr.boolConst (ExprSourceLoc.synthesized "env") true) def Env.performMerge (cond : Expression.Expr) (E1 E2 : Env) (_h1 : E1.error.isNone) (_h2 : E2.error.isNone) : Env := diff --git a/Strata/Languages/Core/Expressions.lean b/Strata/Languages/Core/Expressions.lean index 0a25a77bbf..5cc9380fe8 100644 --- a/Strata/Languages/Core/Expressions.lean +++ b/Strata/Languages/Core/Expressions.lean @@ -3,6 +3,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +-- Default instances and operator constructors use synthesized provenance module public import Strata.DL.Lambda.Lambda @@ -10,6 +11,7 @@ public import Strata.DL.Imperative.PureExpr public import Strata.Languages.Core.Identifiers public import Strata.Languages.Core.CoreOp public import Strata.DL.Imperative.HasVars +public import Strata.DDM.Util.SourceRange namespace Core open Std (ToFormat Format format) @@ -17,7 +19,7 @@ open Std (ToFormat Format format) public section -@[expose] abbrev ExpressionMetadata := Unit +@[expose] abbrev ExpressionMetadata := ExprSourceLoc @[expose] abbrev Expression : Imperative.PureExpr := @@ -33,12 +35,14 @@ abbrev Expression : Imperative.PureExpr := instance : Imperative.HasVarsPure Expression Expression.Expr where getVars := Lambda.LExpr.LExpr.getVars +-- Inhabited default uses synthesized "core" provenance instance : Inhabited Expression.Expr where - default := .intConst () 0 + default := .intConst (ExprSourceLoc.synthesized "core") 0 -/-- Build an `LExpr.op` node from a structured `CoreOp`. -/ +/-- Build an `LExpr.op` node from a structured `CoreOp`. + `CoreOp` values are language-level operators with synthesized provenance. -/ def coreOpExpr (op : CoreOp) (ty : Option Lambda.LMonoTy := none) : Expression.Expr := - .op () op.toString ty + .op (ExprSourceLoc.synthesized "core") op.toString ty --------------------------------------------------------------------- diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean index a5ea88df7a..bda48c4a52 100644 --- a/Strata/Languages/Core/Factory.lean +++ b/Strata/Languages/Core/Factory.lean @@ -21,12 +21,13 @@ import all Strata.DL.Lambda.FactoryWF import Strata.DL.Util.BitVec --------------------------------------------------------------------- +-- Operator constructors and factory helpers use ExprSourceLoc.synthesized "factory" because +-- they build expressions programmatically, not from parsed source. + namespace Core -open Lambda LTy.Syntax LExpr.SyntaxMono +open Lambda LTy.Syntax LExpr.SyntaxMono Core.Syntax public section - -@[expose, match_pattern] def mapTy (keyTy : LMonoTy) (valTy : LMonoTy) : LMonoTy := .tcons "Map" [keyTy, valTy] @@ -372,7 +373,7 @@ def mapConstFunc : WFLFunc CoreLParams := [("d", mty[%v])] (mapTy mty[%k] mty[%v]) (axioms := [ - esM[∀ (%v): -- %1 d + eb[∀ (%v): -- %1 d (∀ (%k): -- %0 kk {(((~select : (Map %k %v) → %k → %v) ((~const : %v → (Map %k %v)) %1)) %0)} @@ -392,7 +393,7 @@ def mapUpdateFunc : WFLFunc CoreLParams := (mapTy mty[%k] mty[%v]) (axioms := [ -- updateSelect: forall m: Map k v, kk: k, vv: v :: m[kk := vv][kk] == vv - esM[∀(Map %k %v): + eb[∀(Map %k %v): (∀ (%k): (∀ (%v):{ (((~select : (Map %k %v) → %k → %v) @@ -400,7 +401,7 @@ def mapUpdateFunc : WFLFunc CoreLParams := (((~select : (Map %k %v) → %k → %v) ((((~update : (Map %k %v) → %k → %v → (Map %k %v)) %2) %1) %0)) %1) == %0))], -- updatePreserve: forall m: Map k v, okk: k, kk: k, vv: v :: okk != kk ==> m[kk := vv][okk] == m[okk] - esM[∀ (Map %k %v): -- %3 m + eb[∀ (Map %k %v): -- %3 m (∀ (%k): -- %2 okk (∀ (%k): -- %1 kk (∀ (%v): -- %0 vv @@ -424,7 +425,7 @@ def seqLengthFunc : WFLFunc CoreLParams := [("s", seqTy mty[%a])] mty[int] (axioms := [ -- length(s) >= 0 - esM[∀ (Sequence %a): -- %0 s + eb[∀ (Sequence %a): -- %0 s {((~Sequence.length : (Sequence %a) → int) %0)} (((~Int.Ge : int → int → bool) ((~Sequence.length : (Sequence %a) → int) %0)) @@ -439,7 +440,7 @@ def seqEmptyFunc : WFLFunc CoreLParams := polyUneval "Sequence.empty" ["a"] [] (seqTy mty[%a]) (axioms := [ -- length(empty()) == 0 - esM[((~Sequence.length : (Sequence %a) → int) + eb[((~Sequence.length : (Sequence %a) → int) (~Sequence.empty : (Sequence %a))) == #0] ]) @@ -450,7 +451,7 @@ def seqAppendFunc : WFLFunc CoreLParams := (seqTy mty[%a]) (axioms := [ -- length(append(s0, s1)) == length(s0) + length(s1) - esM[∀ (Sequence %a): -- %1 s0 + eb[∀ (Sequence %a): -- %1 s0 (∀ (Sequence %a): -- %0 s1 {((~Sequence.length : (Sequence %a) → int) (((~Sequence.append : (Sequence %a) → (Sequence %a) → (Sequence %a)) %1) %0))} @@ -462,7 +463,7 @@ def seqAppendFunc : WFLFunc CoreLParams := ((~Sequence.length : (Sequence %a) → int) %0)))], -- select(append(s0, s1), n): -- 0 <= n < length(s0) ==> select(append(s0,s1), n) == select(s0, n) - esM[∀ (Sequence %a): -- %2 s0 + eb[∀ (Sequence %a): -- %2 s0 (∀ (Sequence %a): -- %1 s1 (∀ (int): -- %0 n {(((~Sequence.select : (Sequence %a) → int → %a) @@ -479,7 +480,7 @@ def seqAppendFunc : WFLFunc CoreLParams := -- select(append(s0, s1), n): -- n >= length(s0) && n < length(s0) + length(s1) -- ==> select(append(s0,s1), n) == select(s1, n - length(s0)) - esM[∀ (Sequence %a): -- %2 s0 + eb[∀ (Sequence %a): -- %2 s0 (∀ (Sequence %a): -- %1 s1 (∀ (int): -- %0 n {(((~Sequence.select : (Sequence %a) → int → %a) @@ -559,7 +560,7 @@ def seqBuildFunc : WFLFunc CoreLParams := (seqTy mty[%a]) (axioms := [ -- length(build(s, v)) == 1 + length(s) - esM[∀ (Sequence %a): -- %1 s + eb[∀ (Sequence %a): -- %1 s (∀ (%a): -- %0 v {((~Sequence.length : (Sequence %a) → int) (((~Sequence.build : (Sequence %a) → %a → (Sequence %a)) %1) %0))} @@ -571,7 +572,7 @@ def seqBuildFunc : WFLFunc CoreLParams := ((~Sequence.length : (Sequence %a) → int) %1)))], -- select(build(s, v), i): -- i == length(s) ==> select(build(s,v), i) == v - esM[∀ (Sequence %a): -- %2 s + eb[∀ (Sequence %a): -- %2 s (∀ (%a): -- %1 v (∀ (int): -- %0 i {(((~Sequence.select : (Sequence %a) → int → %a) @@ -584,7 +585,7 @@ def seqBuildFunc : WFLFunc CoreLParams := else #true))], -- select(build(s, v), i): -- 0 <= i < length(s) ==> select(build(s,v), i) == select(s, i) - esM[∀ (Sequence %a): -- %2 s + eb[∀ (Sequence %a): -- %2 s (∀ (%a): -- %1 v (∀ (int): -- %0 i {(((~Sequence.select : (Sequence %a) → int → %a) @@ -610,7 +611,7 @@ def seqUpdateFunc : WFLFunc CoreLParams := (seqTy mty[%a]) (axioms := [ -- length(update(s, i, v)) == length(s) - esM[∀ (Sequence %a): -- %2 s + eb[∀ (Sequence %a): -- %2 s (∀ (int): -- %1 i (∀ (%a): -- %0 v {((~Sequence.length : (Sequence %a) → int) @@ -620,7 +621,7 @@ def seqUpdateFunc : WFLFunc CoreLParams := == ((~Sequence.length : (Sequence %a) → int) %2)))], -- 0 <= i < length(s) ==> select(update(s, i, v), i) == v (same index) - esM[∀ (Sequence %a): -- %2 s + eb[∀ (Sequence %a): -- %2 s (∀ (int): -- %1 i (∀ (%a): -- %0 v {(((~Sequence.select : (Sequence %a) → int → %a) @@ -635,7 +636,7 @@ def seqUpdateFunc : WFLFunc CoreLParams := == %0 else #true))], -- 0 <= n < length(s) && n != i ==> select(update(s, i, v), n) == select(s, n) - esM[∀ (Sequence %a): -- %3 s + eb[∀ (Sequence %a): -- %3 s (∀ (int): -- %2 i (∀ (%a): -- %1 v (∀ (int): -- %0 n @@ -663,7 +664,7 @@ def seqContainsFunc : WFLFunc CoreLParams := [("s", seqTy mty[%a]), ("v", mty[%a])] mty[bool] (axioms := [ -- contains(s, v) <==> exists i :: 0 <= i < length(s) && select(s, i) == v - esM[∀ (Sequence %a): -- %1 s + eb[∀ (Sequence %a): -- %1 s (∀ (%a): -- %0 v {(((~Sequence.contains : (Sequence %a) → %a → bool) %1) %0)} (((~Sequence.contains : (Sequence %a) → %a → bool) %1) %0) @@ -685,7 +686,7 @@ def seqTakeFunc : WFLFunc CoreLParams := (seqTy mty[%a]) (axioms := [ -- 0 <= n <= length(s) ==> length(take(s, n)) == n - esM[∀ (Sequence %a): -- %1 s + eb[∀ (Sequence %a): -- %1 s (∀ (int): -- %0 n {((~Sequence.length : (Sequence %a) → int) (((~Sequence.take : (Sequence %a) → int → (Sequence %a)) %1) %0))} @@ -699,7 +700,7 @@ def seqTakeFunc : WFLFunc CoreLParams := == %0 else #true)], -- select(take(s, n), j) == select(s, j) (when 0 <= j < n) - esM[∀ (Sequence %a): -- %2 s + eb[∀ (Sequence %a): -- %2 s (∀ (int): -- %1 n (∀ (int): -- %0 j {(((~Sequence.select : (Sequence %a) → int → %a) @@ -725,7 +726,7 @@ def seqDropFunc : WFLFunc CoreLParams := (seqTy mty[%a]) (axioms := [ -- 0 <= n <= length(s) ==> length(drop(s, n)) == length(s) - n - esM[∀ (Sequence %a): -- %1 s + eb[∀ (Sequence %a): -- %1 s (∀ (int): -- %0 n {((~Sequence.length : (Sequence %a) → int) (((~Sequence.drop : (Sequence %a) → int → (Sequence %a)) %1) %0))} @@ -742,7 +743,7 @@ def seqDropFunc : WFLFunc CoreLParams := %0) else #true)], -- 0 <= j < length(s) - n ==> select(drop(s, n), j) == select(s, j + n) - esM[∀ (Sequence %a): -- %2 s + eb[∀ (Sequence %a): -- %2 s (∀ (int): -- %1 n (∀ (int): -- %0 j {(((~Sequence.select : (Sequence %a) → int → %a) @@ -968,8 +969,9 @@ end -- public meta section public section +-- Inhabited defaults use synthesized "factory" provenance instance : Inhabited CoreLParams.Metadata where - default := () + default := ExprSourceLoc.synthesized "factory" DefBVOpFuncExprs [1, 8, 16, 32, 64] DefBVSafeOpFuncExprs [1, 8, 16, 32, 64] @@ -994,8 +996,9 @@ def addTriggerGroupOp : Expression.Expr := addTriggerGroupFunc.opExpr def emptyTriggerGroupOp : Expression.Expr := emptyTriggerGroupFunc.opExpr def addTriggerOp : Expression.Expr := addTriggerFunc.opExpr +-- Inhabited default uses synthesized "factory" provenance instance : Inhabited (⟨ExpressionMetadata, CoreIdent⟩: LExprParams).Metadata where - default := () + default := ExprSourceLoc.synthesized "factory" def intAddOp : Expression.Expr := (@intAddFunc CoreLParams _).opExpr def intSubOp : Expression.Expr := (@intSubFunc CoreLParams _).opExpr @@ -1062,12 +1065,14 @@ def seqContainsOp : Expression.Expr := seqContainsFunc.opExpr def seqTakeOp : Expression.Expr := seqTakeFunc.opExpr def seqDropOp : Expression.Expr := seqDropFunc.opExpr +/-- Build a trigger group expression. Trigger infrastructure is synthesized programmatically. -/ def mkTriggerGroup (ts : List Expression.Expr) : Expression.Expr := - ts.foldl (fun g t => .app () (.app () addTriggerOp t) g) emptyTriggerGroupOp + ts.foldl (fun g t => .app (ExprSourceLoc.synthesized "factory") (.app (ExprSourceLoc.synthesized "factory") addTriggerOp t) g) emptyTriggerGroupOp +/-- Build a triggers expression from groups. Trigger infrastructure is synthesized programmatically. -/ def mkTriggerExpr (ts : List (List Expression.Expr)) : Expression.Expr := let groups := ts.map mkTriggerGroup - groups.foldl (fun gs g => .app () (.app () addTriggerGroupOp g) gs) emptyTriggersOp + groups.foldl (fun gs g => .app (ExprSourceLoc.synthesized "factory") (.app (ExprSourceLoc.synthesized "factory") addTriggerGroupOp g) gs) emptyTriggersOp /-- Get all the built-in functions supported by Strata Core. diff --git a/Strata/Languages/Core/Identifiers.lean b/Strata/Languages/Core/Identifiers.lean index 196ac5ddb7..b7e55655d9 100644 --- a/Strata/Languages/Core/Identifiers.lean +++ b/Strata/Languages/Core/Identifiers.lean @@ -3,11 +3,68 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +-- Defines ExprSourceLoc and its elaborator/test infrastructure module public import Strata.DL.Lambda.LExprTypeEnv public import Strata.DL.Lambda.Factory public meta import Strata.DL.Lambda.LExpr +public import Strata.DDM.Util.SourceRange + +public section + +/-- Lightweight source location for Core expressions: a byte range plus an optional file URI. + The URI is needed because inlining can move expressions across files. + `relatedLocs` accumulates additional source locations from substitution so that + both the original expression and the substituted argument can be reported. -/ +structure ExprSourceLoc where + /-- The file this expression originates from, if known. -/ + uri : Option Strata.Uri := none + /-- Byte-offset range within the file. -/ + range : Strata.SourceRange + /-- Additional source locations accumulated during substitution (e.g. call-site arguments). -/ + relatedLocs : List (Option Strata.Uri × Strata.SourceRange) := [] +deriving Inhabited, Repr, DecidableEq, BEq + +namespace ExprSourceLoc + +/-- Marker for expressions synthesized programmatically. The `origin` string identifies + the synthesis context (e.g. "smt-model", "anf", "transform", "test"). -/ +@[expose] +def synthesized (origin : String) : ExprSourceLoc := + { uri := some (.file s!""), range := Strata.SourceRange.none } + +/-- Default metadata for elaborated expressions from syntax (e.g. `eb[...]` notation). -/ +@[expose] +def elabDefault : ExprSourceLoc := synthesized "elab" + +/-- Build from a `SourceRange` with no URI. -/ +def ofRange (sr : Strata.SourceRange) : ExprSourceLoc := { uri := .none, range := sr } + +/-- Build from a URI and a `SourceRange`. -/ +def ofUriRange (uri : Strata.Uri) (sr : Strata.SourceRange) : ExprSourceLoc := + { uri := some uri, range := sr } + +instance : Std.ToFormat ExprSourceLoc where + format loc := + let primary := match loc.uri with + | some u => f!"{u}:{loc.range}" + | .none => f!"{loc.range}" + if loc.relatedLocs.isEmpty then primary + else + let related := loc.relatedLocs.map fun (u, r) => + match u with | some u => f!"{u}:{r}" | .none => f!"{r}" + f!"{primary} (related: {related})" + +end ExprSourceLoc + +/-- Coercion from `SourceRange` to `ExprSourceLoc` (with no URI). + Translators that have a URI available should use `ExprSourceLoc.ofUriRange` instead. -/ +instance : Coe Strata.SourceRange ExprSourceLoc where + coe sr := ExprSourceLoc.ofRange sr + +end -- public section + namespace Core public section @@ -18,7 +75,7 @@ open Std abbrev CoreIdent := Lambda.Identifier Unit @[expose] -abbrev CoreExprMetadata := Unit +abbrev CoreExprMetadata := ExprSourceLoc @[expose] abbrev CoreLParams: Lambda.LExprParams := {Metadata := CoreExprMetadata, IDMeta := Unit} @[expose] @@ -105,19 +162,22 @@ meta def elabCoreIdent : Syntax → MetaM Expr meta instance : MkLExprParams ⟨CoreExprMetadata, Unit⟩ where elabIdent := elabCoreIdent toExpr := mkApp2 (mkConst ``Lambda.LExprParams.mk) (mkConst ``CoreExprMetadata) (mkConst ``Unit) + -- Elaborated expressions from syntax carry "elab" provenance + defaultMetadata := return mkConst ``ExprSourceLoc.elabDefault elab "eb[" e:lexprmono "]" : term => elabLExprMono (T:=⟨CoreExprMetadata, Unit⟩) e /-- -info: Lambda.LExpr.op () { name := "old", metadata := () } +info: Lambda.LExpr.op ExprSourceLoc.elabDefault { name := "old", metadata := () } none : Lambda.LExpr { Metadata := CoreExprMetadata, IDMeta := Unit }.mono -/ #guard_msgs in #check eb[~old] /-- -info: Lambda.LExpr.app () (Lambda.LExpr.op () { name := "old", metadata := () } none) - (Lambda.LExpr.fvar () { name := "a", metadata := () } +info: Lambda.LExpr.app ExprSourceLoc.elabDefault + (Lambda.LExpr.op ExprSourceLoc.elabDefault { name := "old", metadata := () } none) + (Lambda.LExpr.fvar ExprSourceLoc.elabDefault { name := "a", metadata := () } none) : Lambda.LExpr { Metadata := CoreExprMetadata, IDMeta := Unit }.mono -/ #guard_msgs in @@ -126,7 +186,7 @@ info: Lambda.LExpr.app () (Lambda.LExpr.op () { name := "old", metadata := () } open Lambda.LTy.Syntax in /-- -info: Lambda.LExpr.fvar () { name := "x", metadata := () } +info: Lambda.LExpr.fvar ExprSourceLoc.elabDefault { name := "x", metadata := () } (some (Lambda.LMonoTy.tcons "bool" [])) : Lambda.LExpr { Metadata := CoreExprMetadata, IDMeta := Unit }.mono -/ #guard_msgs in diff --git a/Strata/Languages/Core/Procedure.lean b/Strata/Languages/Core/Procedure.lean index 90b00cce92..a3c425178d 100644 --- a/Strata/Languages/Core/Procedure.lean +++ b/Strata/Languages/Core/Procedure.lean @@ -20,10 +20,10 @@ open Std.Format -- Type class instances to enable deriving for structures containing Expression.Expr instance : DecidableEq ExpressionMetadata := - show DecidableEq Unit from inferInstance + show DecidableEq ExprSourceLoc from inferInstance instance : Repr ExpressionMetadata := - show Repr Unit from inferInstance + show Repr ExprSourceLoc from inferInstance instance : DecidableEq (⟨⟨ExpressionMetadata, CoreIdent⟩, LMonoTy⟩ : LExprParamsT).base.Metadata := show DecidableEq ExpressionMetadata from inferInstance diff --git a/Strata/Languages/Core/ProcedureEval.lean b/Strata/Languages/Core/ProcedureEval.lean index 9ea328f41b..1bcee26e0f 100644 --- a/Strata/Languages/Core/ProcedureEval.lean +++ b/Strata/Languages/Core/ProcedureEval.lean @@ -99,7 +99,7 @@ def eval (E : Env) (p : Procedure) : Env × Statistics := -- that hides the expression from the evaluator, allowing us -- to retain the postcondition body instead of replacing it -- with "true". - (.assert label (.true ()) + (.assert label (Core.true) ((Imperative.MetaData.pushElem #[] (.label label) diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean index 20907ceea2..32da7aebd6 100644 --- a/Strata/Languages/Core/SMTEncoder.lean +++ b/Strata/Languages/Core/SMTEncoder.lean @@ -641,7 +641,9 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte | some body => -- Substitute the formals in the function body with appropriate -- `.bvar`s. Use substFvarsLifting to properly lift indices under binders. - let bvars := (List.range formals.length).map (fun i => LExpr.bvar () i) + -- Synthesized bound variables for substitution; no source location + let smtEnc := ExprSourceLoc.synthesized "smt-encoding" + let bvars := (List.range formals.length).map (fun i => LExpr.bvar smtEnc i) let body := LExpr.substFvarsLifting body (formals.zip bvars) let (term, ctx) ← toSMTTerm E bvs body ctx useArrayTheory .ok (ctx.addIF uf term, !ctx.ifs.contains ({ uf := uf, body := term })) @@ -649,7 +651,7 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte -- Int-recursive functions (no @[cases]) are pure UFs with no axioms. let recAxioms ← if func.isRecursive && isNew && (Strata.DL.Util.FuncAttr.findInlineIfConstr func.attr).isSome then - Lambda.genRecursiveAxioms func ctx.typeFactory E.exprEval () + Lambda.genRecursiveAxioms func ctx.typeFactory E.exprEval (ExprSourceLoc.synthesized "smt-encoding") else .ok [] let allAxioms := func.axioms ++ recAxioms if isNew then @@ -783,8 +785,9 @@ def toSMTCommandsWithAssert (e : LExpr CoreLParams.mono) (E : Env := Env.init) ( then return String.fromUTF8 contents.data h else return "Converting SMT Term to bytes produced an invalid UTF-8 sequence." -/-- -Convert an `SMT.Term` back to a Core `LExpr` (best-effort, partial inverse of `toSMTTerm`). +/-- Convert an SMT term back to a Core `LExpr` for counterexample display. +Uses `ExprSourceLoc.synthesized "smt-model"` to indicate these expressions +originate from an SMT solver model, not from parsed source. Handles: - Primitives: bool, int, real, bitvec, string @@ -800,45 +803,47 @@ such as `Nil`), the result uses `.op` instead of `.fvar` so that the counterexample formatter can distinguish constructors from plain variables and render them with the correct Core data structure. -/ +private abbrev smtModelLoc : ExprSourceLoc := ExprSourceLoc.synthesized "smt-model" + def smtTermToLExpr (t : Strata.SMT.Term) (constructorNames : Std.HashSet String := {}) : LExpr CoreLParams.mono := match t with - | .prim (.bool b) => .boolConst () b - | .prim (.int i) => .intConst () i - | .prim (.real d) => .realConst () d.toRat - | .prim (.bitvec b) => .bitvecConst () _ b - | .prim (.string s) => .strConst () s + | .prim (.bool b) => .boolConst smtModelLoc b + | .prim (.int i) => .intConst smtModelLoc i + | .prim (.real d) => .realConst smtModelLoc d.toRat + | .prim (.bitvec b) => .bitvecConst smtModelLoc _ b + | .prim (.string s) => .strConst smtModelLoc s | .var v => -- Zero-arg constructors arrive as plain variables from the SMT solver. -- Mark them with `.op` so the formatter can emit `Name()`. if constructorNames.contains v.id then - .op () v.id none + .op smtModelLoc v.id none else - .fvar () v.id none + .fvar smtModelLoc v.id none | .app (.core (.uf uf)) args _retTy => -- Constructor names use `.op` so the formatter can distinguish them -- from plain variables (e.g., `Nil` constructor must not be .fvar) let fnExpr : LExpr CoreLParams.mono := if constructorNames.contains uf.id then - .op () uf.id none + .op smtModelLoc uf.id none else - .fvar () uf.id none - args.foldl (fun acc arg => .app () acc (smtTermToLExpr arg constructorNames)) fnExpr + .fvar smtModelLoc uf.id none + args.foldl (fun acc arg => .app smtModelLoc acc (smtTermToLExpr arg constructorNames)) fnExpr | .app (.datatype_op _kind name) args _retTy => - let fnExpr : LExpr CoreLParams.mono := .op () name none - args.foldl (fun acc arg => .app () acc (smtTermToLExpr arg constructorNames)) fnExpr + let fnExpr : LExpr CoreLParams.mono := .op smtModelLoc name none + args.foldl (fun acc arg => .app smtModelLoc acc (smtTermToLExpr arg constructorNames)) fnExpr | .app op args _ => -- Generic fallback for other ops: render as op name applied to args let opName := op.mkName - let fnExpr : LExpr CoreLParams.mono := .op () opName none - args.foldl (fun acc arg => .app () acc (smtTermToLExpr arg constructorNames)) fnExpr - | .none _ty => .op () "none" none - | .some inner => .app () (.op () "some" none) (smtTermToLExpr inner constructorNames) + let fnExpr : LExpr CoreLParams.mono := .op smtModelLoc opName none + args.foldl (fun acc arg => .app smtModelLoc acc (smtTermToLExpr arg constructorNames)) fnExpr + | .none _ty => .op smtModelLoc "none" none + | .some inner => .app smtModelLoc (.op smtModelLoc "some" none) (smtTermToLExpr inner constructorNames) | .quant _ _ _ _ => -- Quantifiers in model values are unusual; fall back to string repr let s := match Strata.SMTDDM.termToString t with | .ok s => s | .error _ => repr t |>.pretty - .fvar () s none + .fvar smtModelLoc s none /-- Extract the set of datatype constructor names from an `SMT.Context`. diff --git a/Strata/Languages/Core/Statement.lean b/Strata/Languages/Core/Statement.lean index d221db67d6..330d77d969 100644 --- a/Strata/Languages/Core/Statement.lean +++ b/Strata/Languages/Core/Statement.lean @@ -105,7 +105,8 @@ theorem replaceInArgs_length (args : List (CallArg P)) (newExprs : List P.Expr) def getInputExprs (args : List (CallArg Expression)) : List Expression.Expr := args.filterMap fun | .inArg e => some e - | .inoutArg id => some (Lambda.LExpr.fvar () id none) + -- Synthesized variable reference from an identifier + | .inoutArg id => some (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "statement") id none) | .outArg _ => none end CallArg diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean index 57f800544d..35741ff1dd 100644 --- a/Strata/Languages/Core/StatementEval.lean +++ b/Strata/Languages/Core/StatementEval.lean @@ -29,6 +29,9 @@ namespace Statement open Std (ToFormat Format format) open Lambda +/-- Metadata for expressions synthesized during statement evaluation. -/ +private abbrev evalSynthLoc : ExprSourceLoc := ExprSourceLoc.synthesized "eval" + --------------------------------------------------------------------- inductive CondType where @@ -85,7 +88,7 @@ LHS mapping: `[("x", fresh_var)]` -/ private def mkReturnSubst (proc : Procedure) (lhs : List Expression.Ident) (E : Env) : VarSubst × VarSubst × Env := - let lhs_tys := lhs.map (fun l => (E.exprEnv.state.findD l (none, .fvar () l none)).fst) + let lhs_tys := lhs.map (fun l => (E.exprEnv.state.findD l (none, .fvar evalSynthLoc l none)).fst) let lhs_typed := lhs.zip lhs_tys let (lhs_fvars, E') := E.genFVars lhs_typed let return_tys := proc.header.outputs.keys.map @@ -94,7 +97,6 @@ private def mkReturnSubst (proc : Procedure) (lhs : List Expression.Ident) (E : let lhs_post_subst := List.zip lhs_typed lhs_fvars (return_lhs_subst, lhs_post_subst, E') - /-- Extract the type from an expression that has already been typechecked (so e.g. `.fvar` and `.op` nodes have their types stored in the `Option LMonoTy` field). @@ -129,7 +131,7 @@ private def computeTypeSubst (input_tys output_tys: List LMonoTy) Subst := let actual_tys := args.filterMap getExprType let lhs_tys := lhs.filterMap (fun l => - (E.exprEnv.state.findD l (none, .fvar () l none)).fst) + (E.exprEnv.state.findD l (none, .fvar evalSynthLoc l none)).fst) let input_constraints := actual_tys.zip input_tys let output_constraints := lhs_tys.zip output_tys let constraints := input_constraints ++ output_constraints @@ -307,7 +309,7 @@ private def createUnreachableCoverObligations Imperative.ProofObligations Expression := covers.toArray.map (fun (label, md) => - (Imperative.ProofObligation.mk label .cover pathConditions (LExpr.false ()) md)) + (Imperative.ProofObligation.mk label .cover pathConditions (LExpr.boolConst evalSynthLoc false) md)) /-- Create assert obligations for asserts in an unreachable (dead) branch, including @@ -321,7 +323,7 @@ private def createUnreachableAssertObligations asserts.toArray.map (fun (label, md) => let propType := Imperative.convertMetaDataPropertyType md - (Imperative.ProofObligation.mk label propType pathConditions (LExpr.true ()) md)) + (Imperative.ProofObligation.mk label propType pathConditions (LExpr.boolConst evalSynthLoc true) md)) /-- Substitute free variables in an expression with their current values from the environment, @@ -376,7 +378,7 @@ private def collectDeadBranchDeferred Imperative.ProofObligations Expression := if Statements.containsCovers ss_f || Statements.containsAsserts ss_f then let deadLabel := toString (f!"") - let deadPathConds := pathConditions.push [.assumption deadLabel (LExpr.false ())] + let deadPathConds := pathConditions.push [.assumption deadLabel (LExpr.boolConst evalSynthLoc false)] createUnreachableCoverObligations deadPathConds (Statements.collectCovers ss_f) ++ createUnreachableAssertObligations deadPathConds (Statements.collectAsserts ss_f) else @@ -580,7 +582,7 @@ private def evalOneStmt (old_var_subst : SubstMap) match cond with | .nondet => let freshName : CoreIdent := ⟨s!"$__nondet_cond_{Ewn.env.pathConditions.length}", ()⟩ - let freshVar : Expression.Expr := .fvar () freshName none + let freshVar : Expression.Expr := .fvar evalSynthLoc freshName none let initStmt := Statement.init freshName (.forAll [] (.tcons "bool" [])) .nondet (Imperative.MetaData.ofProvenance (.synthesized .nondetIte)) let iteStmt := Imperative.Stmt.ite (.det freshVar) then_ss else_ss (Imperative.MetaData.ofProvenance (.synthesized .nondetIte)) evalSub Ewn [initStmt, iteStmt] nextSplitId @@ -675,7 +677,7 @@ def processIteBranches (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNe let label_false := toString (f!"") let path_conds_true := Ewn.env.pathConditions.push [.assumption label_true cond'] let path_conds_false := Ewn.env.pathConditions.push - [.assumption label_false (Lambda.LExpr.ite () cond' (LExpr.false ()) (LExpr.true ()))] + [.assumption label_false (Lambda.LExpr.ite evalSynthLoc cond' (LExpr.boolConst evalSynthLoc false) (LExpr.boolConst evalSynthLoc true))] have : 1 <= Imperative.Block.sizeOf then_ss := by unfold Imperative.Block.sizeOf; split <;> omega have : 1 <= Imperative.Block.sizeOf else_ss := by @@ -781,7 +783,7 @@ def Command.runCall (lhs : List Expression.Ident) (procName : String) (args : Li else let outputBindings : List (CoreIdent × (Option LMonoTy × Expression.Expr)) := proc.header.outputs.keys.zip proc.header.outputs.values - |>.map fun (name, ty) => (name, (some ty, LExpr.fvar () name none)) + |>.map fun (name, ty) => (name, (some ty, LExpr.fvar evalSynthLoc name none)) let callEnv : Env := { E with exprEnv := { E.exprEnv with state := [formalBindings ++ outputBindings] } } @@ -820,7 +822,7 @@ def Command.runCall (lhs : List Expression.Ident) (procName : String) (args : Li CmdEval.updateError E (.Misc s!"procedure '{procName}': expected {proc.header.outputs.keys.length} output arguments, got {lhs.length}") else let outputVals := proc.header.outputs.keys.map fun name => - (callEnv'.exprEnv.state.findD name (none, LExpr.fvar () name none)).snd + (callEnv'.exprEnv.state.findD name (none, LExpr.fvar evalSynthLoc name none)).snd lhs.zip outputVals |>.foldl (fun env (name, val) => env.insertInContext (name, none) val) E | _ => CmdEval.updateError E (.Misc "failed to terminate") diff --git a/Strata/Languages/Core/StatementSemantics.lean b/Strata/Languages/Core/StatementSemantics.lean index 233cffd42d..b198b49ac5 100644 --- a/Strata/Languages/Core/StatementSemantics.lean +++ b/Strata/Languages/Core/StatementSemantics.lean @@ -17,19 +17,29 @@ public section namespace Core -/-- expressions that can't be reduced when evaluating -/ +-- Proof terms and semantic definitions use semLoc provenance +-- (canonical forms represent abstract values, not parsed source terms). + +abbrev semLoc : ExprSourceLoc := + { uri := some (.file ""), range := Strata.SourceRange.none } + +/-- Expressions that can't be reduced when evaluating. + These are canonical forms used in semantic definitions; they carry synthesized provenance + because they represent abstract values, not parsed source terms. -/ inductive Value : Core.Expression.Expr → Prop where - | const : Value (.const () _) - | bvar : Value (.bvar () _) - | op : Value (.op () _ _) - | abs : Value (.abs () _ _ _) + | const : Value (.const semLoc _) + | bvar : Value (.bvar semLoc _) + | op : Value (.op semLoc _ _) + | abs : Value (.abs semLoc _ _ _) open Imperative instance : HasVal Core.Expression where value := Value +-- Semantic typeclass instances construct canonical expressions with synthesized provenance. + instance : HasFvar Core.Expression where - mkFvar := (.fvar () · none) + mkFvar := (.fvar semLoc · none) getFvar | .fvar _ v _ => some v | _ => none @@ -39,30 +49,31 @@ instance : HasSubstFvar Core.Expression where substFvars := Lambda.LExpr.substFvars instance : HasIntOrder Core.Expression where - eq e1 e2 := .eq () e1 e2 - lt e1 e2 := .app () (.app () Core.intLtOp e1) e2 - zero := .intConst () 0 + eq e1 e2 := .eq semLoc e1 e2 + lt e1 e2 := .app semLoc (.app semLoc Core.intLtOp e1) e2 + zero := .intConst semLoc 0 intTy := .forAll [] (.tcons "int" []) instance : HasIdent Core.Expression where ident s := ⟨s, ()⟩ @[expose, match_pattern] -def Core.true : Core.Expression.Expr := .boolConst () Bool.true +def Core.true : Core.Expression.Expr := .boolConst semLoc Bool.true @[expose, match_pattern] -def Core.false : Core.Expression.Expr := .boolConst () Bool.false +def Core.false : Core.Expression.Expr := .boolConst semLoc Bool.false instance : HasBool Core.Expression where tt := Core.true ff := Core.false tt_is_not_ff := by unfold Core.true Core.false; unfold Lambda.LExpr.boolConst; simp boolTy := .forAll [] (.tcons "bool" []) + isTt := fun e => match e with | .const _ (.boolConst true) => true | _ => false instance : HasNot Core.Expression where not | Core.true => Core.false | Core.false => Core.true - | e => Lambda.LExpr.app () (Lambda.boolNotFunc (T:=CoreLParams)).opExpr e + | e => Lambda.LExpr.app semLoc (Lambda.boolNotFunc (T:=CoreLParams)).opExpr e @[expose] abbrev CoreEval := SemanticEval Expression @[expose] abbrev CoreStore := SemanticStore Expression @@ -187,12 +198,12 @@ def updatedStates : SemanticStore P := updatedStates' σ $ idents.zip vals -/-- The evaluator handles old expressions correctly --- It should specify the exact expression form that would map to the old store --- This can be used to implement more general two-state functions, as in Dafny --- https://dafny.org/latest/DafnyRef/DafnyRef#sec-two-state --- where this condition will be asserted at procedures utilizing those two-state functions --/ +/-- The evaluator handles old expressions correctly. +It should specify the exact expression form that would map to the old store. +This can be used to implement more general two-state functions, as in Dafny +https://dafny.org/latest/DafnyRef/DafnyRef#sec-two-state +where this condition will be asserted at procedures utilizing those two-state functions. +Synthesized `old` variable references carry no source location. -/ def WellFormedCoreEvalTwoState (δ : CoreEval) (σ₀ σ : CoreStore) : Prop := (∃ vs vs' σ₁, HavocVars σ₀ vs σ₁ ∧ InitVars σ₁ vs' σ) ∧ (∀ vs vs' σ₀ σ₁ σ, @@ -200,10 +211,10 @@ def WellFormedCoreEvalTwoState (δ : CoreEval) (σ₀ σ : CoreStore) : Prop := ∀ v, -- "old g" in the post-state holds the pre-state value of g (v ∈ vs → - δ σ (.fvar () (CoreIdent.mkOld v.name) none) = σ₀ v) ∧ + δ σ (.fvar semLoc (CoreIdent.mkOld v.name) none) = σ₀ v) ∧ -- if the variable is not modified, "old g" is the same as g (¬ v ∈ vs → - δ σ (.fvar () (CoreIdent.mkOld v.name) none) = σ v)) + δ σ (.fvar semLoc (CoreIdent.mkOld v.name) none) = σ v)) /-! ### Closure Capture for Function Declarations -/ diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 9e02d9a825..4566828bcf 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -47,6 +47,13 @@ public section private def mdWithUnknownLoc : Imperative.MetaData Core.Expression := Imperative.MetaData.ofProvenance (.synthesized .laurelToCore) +/-- Extract source location from an `AstNode` as an `ExprSourceLoc`, + preserving the URI when available. -/ +private def exprSourceLocOf (node : AstNode α) : ExprSourceLoc := + match node.source with + | some fr => ExprSourceLoc.ofUriRange fr.file fr.range + | none => ExprSourceLoc.synthesized "laurel" + def isFieldName (fieldNames : List Identifier) (name : Identifier) : Bool := fieldNames.contains name @@ -128,12 +135,13 @@ private def freshId : TranslateM Nat := do set { s with nextId := id + 1 } return id -/-- Throw a hard diagnostic error, aborting the current translation -/ +/-- Throw a hard diagnostic error, aborting the current translation. + The dummy variable has no source range because it is synthesized for error recovery. -/ def throwExprDiagnostic (d : DiagnosticModel): TranslateM Core.Expression.Expr := do emitDiagnostic d modify fun s => { s with coreProgramHasSuperfluousErrors := true } let id ← freshId - return LExpr.fvar () (⟨s!"DUMMY_VAR_{id}", ()⟩) none + return LExpr.fvar (ExprSourceLoc.synthesized "laurel") (⟨s!"DUMMY_VAR_{id}", ()⟩) none /-- Translate Laurel StmtExpr to Core Expression using the `TranslateM` monad. @@ -154,6 +162,7 @@ def translateExpr (expr : StmtExprMd) let s ← get let model := s.model let md := astNodeToCoreMd expr + let sr := exprSourceLocOf expr let disallowed (source : Option FileRange) (msg : String) : TranslateM Core.Expression.Expr := do if isPureContext then throwExprDiagnostic $ diagnosticFromSource source msg @@ -161,52 +170,52 @@ def translateExpr (expr : StmtExprMd) throwExprDiagnostic $ diagnosticFromSource source s!"{msg} (should have been lifted)" DiagnosticType.StrataBug match h: expr.val with - | .LiteralBool b => return .const () (.boolConst b) - | .LiteralInt i => return .const () (.intConst i) - | .LiteralString s => return .const () (.strConst s) - | .LiteralDecimal d => return .const () (.realConst (Strata.Decimal.toRat d)) + | .LiteralBool b => return .const sr (.boolConst b) + | .LiteralInt i => return .const sr (.intConst i) + | .LiteralString s => return .const sr (.strConst s) + | .LiteralDecimal d => return .const sr (.realConst (Strata.Decimal.toRat d)) | .Var (.Local name) => -- First check if this name is bound by an enclosing quantifier match boundVars.findIdx? (· == name) with | some idx => -- Bound variable: use de Bruijn index - return .bvar () idx + return .bvar sr idx | none => match model.get name with | .field _ f => - return .op () ⟨f.name.text, ()⟩ none + return .op sr ⟨f.name.text, ()⟩ none | astNode => - return .fvar () ⟨name.text, ()⟩ (some (← translateType astNode.getType)) + return .fvar sr ⟨name.text, ()⟩ (some (← translateType astNode.getType)) | .Var (.Declare _) => throwExprDiagnostic $ md.toDiagnostic "variable declaration in expression context should have been lowered" DiagnosticType.StrataBug | .PrimitiveOp op [e] => match op with | .Not => let re ← translateExpr e boundVars isPureContext - return .app () boolNotOp re + return .app sr boolNotOp re | .Neg => let re ← translateExpr e boundVars isPureContext let isReal := match (computeExprType model e).val with | .TReal => true | _ => false - return .app () (if isReal then realNegOp else intNegOp) re + return .app sr (if isReal then realNegOp else intNegOp) re | _ => throwExprDiagnostic $ diagnosticFromSource expr.source s!"translateExpr: Invalid unary op: {repr op}" DiagnosticType.StrataBug | .PrimitiveOp op [e1, e2] => let re1 ← translateExpr e1 boundVars isPureContext let re2 ← translateExpr e2 boundVars isPureContext let binOp (bop : Core.Expression.Expr) : Core.Expression.Expr := - LExpr.mkApp () bop [re1, re2] + LExpr.mkApp sr bop [re1, re2] let isReal := match (computeExprType model e1).val, (computeExprType model e2).val with | .TReal, _ | _, .TReal => true | _, _ => false match op with - | .Eq => return .eq () re1 re2 - | .Neq => return .app () boolNotOp (.eq () re1 re2) + | .Eq => return .eq sr re1 re2 + | .Neq => return .app sr boolNotOp (.eq sr re1 re2) | .And => return binOp boolAndOp | .Or => return binOp boolOrOp - | .AndThen => return .ite () re1 re2 (.boolConst () false) - | .OrElse => return .ite () re1 (.boolConst () true) re2 - | .Implies => return .ite () re1 re2 (.boolConst () true) + | .AndThen => return .ite sr re1 re2 (.boolConst sr false) + | .OrElse => return .ite sr re1 (.boolConst sr true) re2 + | .Implies => return .ite sr re1 re2 (.boolConst sr true) | .Add => return binOp (if isReal then realAddOp else intAddOp) | .Sub => return binOp (if isReal then realSubOp else intSubOp) | .Mul => return binOp (if isReal then realMulOp else intMulOp) @@ -234,16 +243,16 @@ def translateExpr (expr : StmtExprMd) have := AstNode.sizeOf_val_lt expr cases expr; simp_all; omega translateExpr e boundVars isPureContext - return .ite () bcond bthen belse + return .ite sr bcond bthen belse | .StaticCall callee args => -- In a pure context, only Core functions (not procedures) are allowed if isPureContext && !model.isFunction callee then disallowed expr.source "calls to procedures are not supported in functions or contracts" else - let fnOp : Core.Expression.Expr := .op () ⟨callee.text, ()⟩ none + let fnOp : Core.Expression.Expr := .op sr ⟨callee.text, ()⟩ none args.attach.foldlM (fun acc ⟨arg, _⟩ => do let re ← translateExpr arg boundVars isPureContext - return .app () acc re) fnOp + return .app sr acc re) fnOp | .Block [single] _ => translateExpr single boundVars isPureContext | .Quantifier mode ⟨ name, ty ⟩ trigger body => let coreTy ← translateType ty @@ -252,19 +261,19 @@ def translateExpr (expr : StmtExprMd) | some trig => let coreTrig ← translateExpr trig (name :: boundVars) isPureContext match mode with - | .Forall => return LExpr.allTr () name.text (some coreTy) coreTrig coreBody - | .Exists => return LExpr.existTr () name.text (some coreTy) coreTrig coreBody + | .Forall => return LExpr.allTr sr name.text (some coreTy) coreTrig coreBody + | .Exists => return LExpr.existTr sr name.text (some coreTy) coreTrig coreBody | none => match mode with - | .Forall => return LExpr.all () name.text (some coreTy) coreBody - | .Exists => return LExpr.exist () name.text (some coreTy) coreBody + | .Forall => return LExpr.all sr name.text (some coreTy) coreBody + | .Exists => return LExpr.exist sr name.text (some coreTy) coreBody | .Hole _ _ => -- Holes should have been eliminated before translation. disallowed expr.source "holes should have been eliminated before translation" | .ReferenceEquals e1 e2 => let re1 ← translateExpr e1 boundVars isPureContext let re2 ← translateExpr e2 boundVars isPureContext - return .eq () re1 re2 + return .eq sr re1 re2 | .Assign _ _ => disallowed expr.source "destructive assignments are not supported in functions or contracts" | .While _ _ _ _ => @@ -281,7 +290,7 @@ def translateExpr (expr : StmtExprMd) let valueExpr ← translateExpr initializer boundVars isPureContext let bodyExpr ← translateExpr { val := StmtExpr.Block rest label, source := innerSrc } (name :: boundVars) isPureContext let coreMonoType ← translateType ty - return .app () (.abs () name.text (some coreMonoType) bodyExpr) valueExpr + return .app sr (.abs sr name.text (some coreMonoType) bodyExpr) valueExpr | .Block (⟨ .Var (.Declare _), innerSrc⟩ :: rest) label => do _ ← disallowed innerSrc "local variables in functions must have initializers" translateExpr { val := StmtExpr.Block rest label, source := innerSrc } boundVars isPureContext @@ -323,16 +332,17 @@ def getNameFromMd (md : Imperative.MetaData Core.Expression): String := | none => "(unknown)" def defaultExprForType (ty : HighTypeMd) : TranslateM Core.Expression.Expr := do + let sr := exprSourceLocOf ty match ty.val with - | .TInt => return .const () (.intConst 0) - | .TBool => return .const () (.boolConst false) - | .TString => return .const () (.strConst "") + | .TInt => return .const sr (.intConst 0) + | .TBool => return .const sr (.boolConst false) + | .TString => return .const sr (.strConst "") | _ => -- For types without a natural default (arrays, composites, etc.), -- use a fresh free variable. This is only used when the value is -- immediately overwritten by a procedure call. let coreTy ← translateType ty - return .fvar () (⟨"$default", ()⟩) (some coreTy) + return .fvar sr (⟨"$default", ()⟩) (some coreTy) /-- Translate an expression in statement position into a `var $unused_N := expr` init. @@ -599,9 +609,10 @@ def translateInvokeOnAxiom (proc : Procedure) (trigger : StmtExprMd) -- Translate postconditions and trigger with the full bound-var context let postcondExprs ← postconds.mapM (fun pc => translateExpr pc.condition boundVars (isPureContext := true)) let bodyExpr : Core.Expression.Expr := match postcondExprs with - | [] => .const () (.boolConst true) + -- Synthesized conjunction of postconditions + | [] => .const (ExprSourceLoc.synthesized "laurel") (.boolConst true) | [e] => e - | e :: rest => rest.foldl (fun acc x => LExpr.mkApp () boolAndOp [acc, x]) e + | e :: rest => rest.foldl (fun acc x => LExpr.mkApp (ExprSourceLoc.synthesized "laurel") boolAndOp [acc, x]) e let triggerExpr ← translateExpr trigger boundVars (isPureContext := true) -- Wrap in ∀ from outermost (first param) to innermost (last param). -- The trigger is placed on the innermost quantifier. @@ -615,10 +626,16 @@ where match params with | [] => return body | [p] => - return LExpr.allTr () p.name.text (some (← translateType p.type)) trigger body + let sr := match p.name.source with + | some fr => ExprSourceLoc.ofUriRange fr.file fr.range + | none => ExprSourceLoc.synthesized "laurel" + return LExpr.allTr sr p.name.text (some (← translateType p.type)) trigger body | p :: rest => do let inner ← buildQuants rest body trigger - return LExpr.all () p.name.text (some (← translateType p.type)) inner + let sr := match p.name.source with + | some fr => ExprSourceLoc.ofUriRange fr.file fr.range + | none => ExprSourceLoc.synthesized "laurel" + return LExpr.all sr p.name.text (some (← translateType p.type)) inner structure LaurelTranslateOptions where emitResolutionErrors : Bool := true @@ -648,7 +665,7 @@ def translateProcedureToFunction (options: LaurelTranslateOptions) (isRecursive: -- Translate precondition to FuncPrecondition (skip trivial `true`) let preconditions ← proc.preconditions.mapM (fun precondition => do let checkExpr ← translateExpr precondition.condition [] true - return { expr := checkExpr, md := () }) + return { expr := checkExpr, md := exprSourceLocOf precondition.condition }) -- For recursive functions, infer the @[cases] parameter index: the first input -- whose type is a user-defined datatype (has constructors). This is the argument diff --git a/Strata/Languages/Python/FunctionSignatures.lean b/Strata/Languages/Python/FunctionSignatures.lean index 53eeab9e88..be5157dd4c 100644 --- a/Strata/Languages/Python/FunctionSignatures.lean +++ b/Strata/Languages/Python/FunctionSignatures.lean @@ -149,18 +149,23 @@ def addCoreDecls : SignatureM Unit := do end +/-- Build a `None` value expression for a given `OrNone` type. + Synthesized expression for default parameter values. -/ def TypeStrToCoreExpr (ty: String) : Core.Expression.Expr := if !ty.endsWith "OrNone" then panic! s!"Should only be called for possibly None types. Called for: {ty}" else + let loc := ExprSourceLoc.synthesized "python-default-value" + let mkNoneExpr (ty : String) : Core.Expression.Expr := + .app loc (.op loc (ty ++ "_mk_none") none) (.op loc "None_none" none) match ty with - | "StrOrNone" => .app () (.op () "StrOrNone_mk_none" none) (.op () "None_none" none) - | "BoolOrNone" => .app () (.op () "BoolOrNone_mk_none" none) (.op () "None_none" none) - | "BoolOrStrOrNone" => .app () (.op () "BoolOrStrOrNone_mk_none" none) (.op () "None_none" none) - | "AnyOrNone" => .app () (.op () "AnyOrNone_mk_none" none) (.op () "None_none" none) - | "IntOrNone" => .app () (.op () "IntOrNone_mk_none" none) (.op () "None_none" none) - | "BytesOrStrOrNone" => .app () (.op () "BytesOrStrOrNone_mk_none" none) (.op () "None_none" none) - | "DictStrStrOrNone" => .app () (.op () "DictStrStrOrNone_mk_none" none) (.op () "None_none" none) + | "StrOrNone" => mkNoneExpr "StrOrNone" + | "BoolOrNone" => mkNoneExpr "BoolOrNone" + | "BoolOrStrOrNone" => mkNoneExpr "BoolOrStrOrNone" + | "AnyOrNone" => mkNoneExpr "AnyOrNone" + | "IntOrNone" => mkNoneExpr "IntOrNone" + | "BytesOrStrOrNone" => mkNoneExpr "BytesOrStrOrNone" + | "DictStrStrOrNone" => mkNoneExpr "DictStrStrOrNone" | _ => panic! s!"unsupported type: {ty}" end -- public section diff --git a/Strata/Languages/Python/PyFactory.lean b/Strata/Languages/Python/PyFactory.lean index f058b50293..518e84515f 100644 --- a/Strata/Languages/Python/PyFactory.lean +++ b/Strata/Languages/Python/PyFactory.lean @@ -15,6 +15,9 @@ public section ------------------------------------------------------------------------------- +/-- Metadata for Python factory synthesized expressions. -/ +private abbrev pyFactoryLoc : ExprSourceLoc := ExprSourceLoc.synthesized "python-factory" + /- ## Python regex verification — factory functions @@ -80,10 +83,10 @@ private def mkModeBoolFunc (name : String) (mode : MatchMode) : attr := #[.evalIfCanonical 0], concreteEval := some (fun _ args => match args with - | [LExpr.strConst () pattern, sExpr] => + | [LExpr.strConst _ pattern, sExpr] => let (regexExpr, maybe_err) := pythonRegexToCore pattern mode match maybe_err with - | none => .some (LExpr.mkApp () (.op () "Str.InRegEx" (some mty[string → (regex → bool)])) [sExpr, regexExpr]) + | none => .some (LExpr.mkApp pyFactoryLoc (.op pyFactoryLoc "Str.InRegEx" (some mty[string → (regex → bool)])) [sExpr, regexExpr]) | some _ => .none | _ => .none) } @@ -103,16 +106,16 @@ def rePatternErrorFunc : LFunc Core.CoreLParams := attr := #[.evalIfCanonical 0], concreteEval := some (fun _ args => match args with - | [LExpr.strConst () s] => + | [LExpr.strConst _ s] => let (_, maybe_err) := pythonRegexToCore s .fullmatch -- mode irrelevant: errors come from parseTop before mode-specific compilation match maybe_err with | none => - .some (LExpr.mkApp () (.op () "NoError" (some mty[Error])) []) + .some (LExpr.mkApp pyFactoryLoc (.op pyFactoryLoc "NoError" (some mty[Error])) []) | some (ParseError.unimplemented ..) => - .some (LExpr.mkApp () (.op () "NoError" (some mty[Error])) []) + .some (LExpr.mkApp pyFactoryLoc (.op pyFactoryLoc "NoError" (some mty[Error])) []) | some (ParseError.patternError msg ..) => - .some (LExpr.mkApp () (.op () "RePatternError" (some mty[string → Error])) - [.strConst () (toString msg)]) + .some (LExpr.mkApp pyFactoryLoc (.op pyFactoryLoc "RePatternError" (some mty[string → Error])) + [.strConst pyFactoryLoc (toString msg)]) | _ => .none) } diff --git a/Strata/Languages/Python/PythonToCore.lean b/Strata/Languages/Python/PythonToCore.lean index 5641277d32..8ccaafae0b 100644 --- a/Strata/Languages/Python/PythonToCore.lean +++ b/Strata/Languages/Python/PythonToCore.lean @@ -23,28 +23,37 @@ open Lambda.LTy.Syntax public section +/-- Source location for intermediate sub-expressions synthesized during Python-to-Core + translation (e.g. operator wrappers, curried applications) that do not correspond + to a single Python AST node. -/ +private abbrev pySynthLoc : ExprSourceLoc := ExprSourceLoc.synthesized "python-to-core" + +/-- Build an `ExprSourceLoc` that carries the actual Python source position. -/ +private def pyLoc (filePath : String) (sr : SourceRange) : ExprSourceLoc := + ExprSourceLoc.ofUriRange (.file filePath) sr + -- Some hard-coded things we'll need to fix later: def clientType : Core.Expression.Ty := .forAll [] (.tcons "Client" []) -def dummyClient : Core.Expression.Expr := .fvar () "DUMMY_CLIENT" none +def dummyClient : Core.Expression.Expr := .fvar pySynthLoc "DUMMY_CLIENT" none def dictStrAnyType : Core.Expression.Ty := .forAll [] (.tcons "DictStrAny" []) -def dummyDictStrAny : Core.Expression.Expr := .fvar () "DUMMY_DICT_STR_ANY" none +def dummyDictStrAny : Core.Expression.Expr := .fvar pySynthLoc "DUMMY_DICT_STR_ANY" none def strType : Core.Expression.Ty := .forAll [] (.tcons "string" []) -def dummyStr : Core.Expression.Expr := .fvar () "DUMMY_STR" none +def dummyStr : Core.Expression.Expr := .fvar pySynthLoc "DUMMY_STR" none def listStrType : Core.Expression.Ty := .forAll [] (.tcons "ListStr" []) -def dummyListStr : Core.Expression.Expr := .fvar () "DUMMY_LIST_STR" none +def dummyListStr : Core.Expression.Expr := .fvar pySynthLoc "DUMMY_LIST_STR" none def datetimeType : Core.Expression.Ty := .forAll [] (.tcons "Datetime" []) -def dummyDatetime : Core.Expression.Expr := .fvar () "DUMMY_DATETIME" none +def dummyDatetime : Core.Expression.Expr := .fvar pySynthLoc "DUMMY_DATETIME" none def dateType : Core.Expression.Ty := .forAll [] (.tcons "Date" []) -def dummyDate : Core.Expression.Expr := .fvar () "DUMMY_DATE" none +def dummyDate : Core.Expression.Expr := .fvar pySynthLoc "DUMMY_DATE" none def timedeltaType : Core.Expression.Ty := .forAll [] (.tcons "int" []) -def dummyTimedelta : Core.Expression.Expr := .fvar () "DUMMY_Timedelta" none +def dummyTimedelta : Core.Expression.Expr := .fvar pySynthLoc "DUMMY_Timedelta" none ------------------------------------------------------------------------------- @@ -106,114 +115,114 @@ def sourceRangeToMetaData (filePath : String) (sr : SourceRange) : Imperative.Me ------------------------------------------------------------------------------- def strToCoreExpr (s: String) : Core.Expression.Expr := - .strConst () s + .strConst pySynthLoc s def intToCoreExpr (i: Int) : Core.Expression.Expr := - .intConst () i + .intConst pySynthLoc i def PyIntToInt (i : Python.int SourceRange) : Int := match i with | .IntPos _ n => n.val | .IntNeg _ n => -n.val -def PyConstToCore (c: Python.constant SourceRange) : Core.Expression.Expr := +def PyConstToCore (loc : ExprSourceLoc) (c: Python.constant SourceRange) : Core.Expression.Expr := match c with - | .ConString _ s => .strConst () s.val - | .ConPos _ i => .intConst () i.val - | .ConNeg _ i => .intConst () (-i.val) - | .ConBytes _ _b => .const () (.strConst "") -- TODO: fix - | .ConFloat _ f => .strConst () (f.val) + | .ConString _ s => .strConst loc s.val + | .ConPos _ i => .intConst loc i.val + | .ConNeg _ i => .intConst loc (-i.val) + | .ConBytes _ _b => .const loc (.strConst "") -- TODO: fix + | .ConFloat _ f => .strConst loc (f.val) | _ => panic! s!"Unhandled Constant: {repr c}" def PyAliasToCoreExpr (a : Python.alias SourceRange) : Core.Expression.Expr := match a with | .mk_alias _ n as_n => assert! as_n.val.isNone - .strConst () n.val + .strConst pySynthLoc n.val def handleAdd (translation_ctx: TranslationContext) (lhs rhs: Core.Expression.Expr) : Core.Expression.Expr := match lhs, rhs with - | .intConst () l, .intConst () r => .intConst () (l + r) - | .fvar () l _, .fvar () r _ => + | .intConst _ l, .intConst _ r => .intConst pySynthLoc (l + r) + | .fvar _ l _, .fvar _ r _ => let l_ty := translation_ctx.variableTypes.find? (λ p => p.fst == l.name) let r_ty := translation_ctx.variableTypes.find? (λ p => p.fst == r.name) match l_ty, r_ty with | some (_, .tcons "int" []), some (_, .tcons "int" []) => - .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Add⟩) (some mty[int → (int → int)])) lhs) rhs + .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Add⟩) (some mty[int → (int → int)])) lhs) rhs | some (_, .tcons "string" []), some (_, .tcons "string" []) => - .app () (.app () (.op () "Str.Concat" mty[string → (string → string)]) lhs) rhs + .app pySynthLoc (.app pySynthLoc (.op pySynthLoc "Str.Concat" mty[string → (string → string)]) lhs) rhs | _, _ => panic! s!"Unsupported types for +. Exprs: {lhs} and {rhs}" - | _, _ => .app () (.app () (.op () "Str.Concat" mty[string → (string → string)]) lhs) rhs + | _, _ => .app pySynthLoc (.app pySynthLoc (.op pySynthLoc "Str.Concat" mty[string → (string → string)]) lhs) rhs def handleSub (translation_ctx: TranslationContext) (lhs rhs: Core.Expression.Expr) : Core.Expression.Expr := match lhs, rhs with - | .intConst () l, .intConst () r => .intConst () (l - r) - | .fvar () l _, .fvar () r _ => + | .intConst _ l, .intConst _ r => .intConst pySynthLoc (l - r) + | .fvar _ l _, .fvar _ r _ => let l_ty := translation_ctx.variableTypes.find? (λ p => p.fst == l.name) let r_ty := translation_ctx.variableTypes.find? (λ p => p.fst == r.name) match l_ty, r_ty with | some (_, .tcons "int" []), some (_, .tcons "int" []) => - .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Sub⟩) (some mty[int → (int → int)])) lhs) rhs + .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Sub⟩) (some mty[int → (int → int)])) lhs) rhs | some (_, .tcons "Datetime" []), some (_, .tcons "int" []) => - .app () (.app () (.op () "Datetime_sub" none) lhs) rhs + .app pySynthLoc (.app pySynthLoc (.op pySynthLoc "Datetime_sub" none) lhs) rhs | some (_, .tcons "Datetime" []), some (_, .tcons "Timedelta" []) => - .app () (.app () (.op () "Datetime_sub" none) lhs) rhs + .app pySynthLoc (.app pySynthLoc (.op pySynthLoc "Datetime_sub" none) lhs) rhs | _, _ => panic! s!"Unsupported types for -. Exprs: {lhs} and {rhs}" | _, _ => panic! s!"Unsupported args for -. Got: {lhs} and {rhs}" def handleMult (translation_ctx: TranslationContext) (lhs rhs: Core.Expression.Expr) : Core.Expression.Expr := match lhs, rhs with - | .strConst () s, .intConst () i => .strConst () (String.join (List.replicate i.toNat s)) - | .intConst () l, .intConst () r => .intConst () (l * r) - | .fvar () l _, .fvar () r _ => + | .strConst _ s, .intConst _ i => .strConst pySynthLoc (String.join (List.replicate i.toNat s)) + | .intConst _ l, .intConst _ r => .intConst pySynthLoc (l * r) + | .fvar _ l _, .fvar _ r _ => let l := translation_ctx.variableTypes.find? (λ p => p.fst == l.name) let r := translation_ctx.variableTypes.find? (λ p => p.fst == r.name) match l, r with | .some lty, .some rty => match lty.snd, rty.snd with - | .tcons "int" [], .tcons "int" [] => .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Mul⟩) (some mty[int → (int → int)])) lhs) rhs + | .tcons "int" [], .tcons "int" [] => .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Mul⟩) (some mty[int → (int → int)])) lhs) rhs | _, _ => panic! s!"Unsupported types for fvar *. Types: {lty} and {rty}" | _, _ => panic! s!"Missing needed type information for *. Exprs: {lhs} and {rhs}" | _ , _ => panic! s!"Unsupported args for * . Got: {lhs} and {rhs}" def handleFloorDiv (_translation_ctx: TranslationContext) (lhs rhs: Core.Expression.Expr) : Core.Expression.Expr := - .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Div⟩) (some mty[int → (int → int)])) lhs) rhs + .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Div⟩) (some mty[int → (int → int)])) lhs) rhs def handleNot (arg: Core.Expression.Expr) : Core.Expression.Expr := let ty : Lambda.LMonoTy := (.tcons "ListStr" []) match ty with - | (.tcons "ListStr" []) => .eq () arg (.op () "ListStr_nil" none) + | (.tcons "ListStr" []) => .eq pySynthLoc arg (.op pySynthLoc "ListStr_nil" none) | _ => panic! s!"Unimplemented not op for {arg}" def handleLt (translation_ctx: TranslationContext) (lhs rhs: Core.Expression.Expr) : Core.Expression.Expr := match lhs, rhs with - | .fvar () l _, .fvar () r _ => + | .fvar _ l _, .fvar _ r _ => let l_ty := translation_ctx.variableTypes.find? (λ p => p.fst == l.name) let r_ty := translation_ctx.variableTypes.find? (λ p => p.fst == r.name) match l_ty, r_ty with | some (_, .tcons "Datetime" []), some (_, .tcons "Datetime" []) => - .app () (.app () (.op () "Datetime_lt" none) lhs) rhs - | _, _ => .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Lt⟩) (some mty[int → (int → bool)])) lhs) rhs - | _, _ => .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Lt⟩) (some mty[int → (int → bool)])) lhs) rhs + .app pySynthLoc (.app pySynthLoc (.op pySynthLoc "Datetime_lt" none) lhs) rhs + | _, _ => .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Lt⟩) (some mty[int → (int → bool)])) lhs) rhs + | _, _ => .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Lt⟩) (some mty[int → (int → bool)])) lhs) rhs def handleLtE (translation_ctx: TranslationContext) (lhs rhs: Core.Expression.Expr) : Core.Expression.Expr := match lhs, rhs with - | .fvar () l _, .fvar () r _ => + | .fvar _ l _, .fvar _ r _ => let l_ty := translation_ctx.variableTypes.find? (λ p => p.fst == l.name) let r_ty := translation_ctx.variableTypes.find? (λ p => p.fst == r.name) match l_ty, r_ty with | some (_, .tcons "Datetime" []), some (_, .tcons "Datetime" []) => - let eq := (.eq () lhs rhs) - let lt := (.app () (.app () (.op () "Datetime_lt" none) lhs) rhs) - (.app () (.app () (Core.coreOpExpr (.bool .Or)) eq) lt) - | _, _ => .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Le⟩) (some mty[int → (int → bool)])) lhs) rhs - | _, _ => .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Le⟩) (some mty[int → (int → bool)])) lhs) rhs + let eq := (.eq pySynthLoc lhs rhs) + let lt := (.app pySynthLoc (.app pySynthLoc (.op pySynthLoc "Datetime_lt" none) lhs) rhs) + (.app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.bool .Or)) eq) lt) + | _, _ => .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Le⟩) (some mty[int → (int → bool)])) lhs) rhs + | _, _ => .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Le⟩) (some mty[int → (int → bool)])) lhs) rhs def handleGt (lhs rhs: Core.Expression.Expr) : Core.Expression.Expr := - .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Gt⟩) (some mty[int → (int → bool)])) lhs) rhs + .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Gt⟩) (some mty[int → (int → bool)])) lhs) rhs def handleGtE (lhs rhs: Core.Expression.Expr) : Core.Expression.Expr := - .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Ge⟩) (some mty[int → (int → bool)])) lhs) rhs + .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Ge⟩) (some mty[int → (int → bool)])) lhs) rhs structure SubstitutionRecord where pyExpr : Python.expr SourceRange @@ -231,13 +240,13 @@ def PyExprIdent (e1 e2: Python.expr SourceRange) : Bool := -- TODO: handle rest of names def PyListStrToCore (names : Array (Python.alias SourceRange)) : Core.Expression.Expr := - .app () (.app () (.op () "ListStr_cons" mty[string → (ListStr → ListStr)]) (PyAliasToCoreExpr names[0]!)) - (.op () "ListStr_nil" mty[ListStr]) + .app pySynthLoc (.app pySynthLoc (.op pySynthLoc "ListStr_cons" mty[string → (ListStr → ListStr)]) (PyAliasToCoreExpr names[0]!)) + (.op pySynthLoc "ListStr_nil" mty[ListStr]) def handleList (_elmts: Array (Python.expr SourceRange)) (expected_type : Lambda.LMonoTy): PyExprTranslated := match expected_type with - | (.tcons "ListStr" _) => {stmts := [], expr := (.op () "ListStr_nil" expected_type)} - | (.tcons "ListDictStrAny" _) => {stmts := [], expr := (.op () "ListDictStrAny_nil" expected_type)} + | (.tcons "ListStr" _) => {stmts := [], expr := (.op pySynthLoc "ListStr_nil" expected_type)} + | (.tcons "ListDictStrAny" _) => {stmts := [], expr := (.op pySynthLoc "ListDictStrAny_nil" expected_type)} | _ => panic! s!"Unexpected type : {expected_type}" def PyOptExprToString (e : Python.opt_expr SourceRange) : String := @@ -307,15 +316,15 @@ def noneOrExpr (translation_ctx : TranslationContext) (fname n : String) (e: Cor if type_str.endsWith "OrNone" then -- Optional param. Need to wrap e.g., string into StrOrNone match type_str with - | "IntOrNone" => .app () (.op () "IntOrNone_mk_int" none) e - | "StrOrNone" => .app () (.op () "StrOrNone_mk_str" none) e - | "BytesOrStrOrNone" => .app () (.op () "BytesOrStrOrNone_mk_str" none) e + | "IntOrNone" => .app pySynthLoc (.op pySynthLoc "IntOrNone_mk_int" none) e + | "StrOrNone" => .app pySynthLoc (.op pySynthLoc "StrOrNone_mk_str" none) e + | "BytesOrStrOrNone" => .app pySynthLoc (.op pySynthLoc "BytesOrStrOrNone_mk_str" none) e | _ => panic! "Unsupported type_str: "++ type_str else e def handleCallThrow (jmp_target : String) : Core.Statement := - let cond := .app () (.op () "ExceptOrNone..isExceptOrNone_mk_code" none) (.fvar () "maybe_except" none) + let cond := .app pySynthLoc (.op pySynthLoc "ExceptOrNone..isExceptOrNone_mk_code" none) (.fvar pySynthLoc "maybe_except" none) .ite (.det cond) [.exit jmp_target .empty] [] .empty def deduplicateTypeAnnotations (l : List (String × Option String)) : List (String × String) := Id.run do @@ -355,11 +364,11 @@ partial def collectVarDecls (translation_ctx : TranslationContext) (stmts: Array let name := p.fst let ty_name := p.snd match ty_name with - | "bool" => [(.init name t[bool] (.det (.boolConst () false)) .empty), (.havoc name .empty)] - | "str" => [(.init name t[string] (.det (.strConst () "")) .empty), (.havoc name .empty)] - | "int" => [(.init name t[int] (.det (.intConst () 0)) .empty), (.havoc name .empty)] - | "float" => [(.init name t[string] (.det (.strConst () "0.0")) .empty), (.havoc name .empty)] -- Floats as strs for now - | "bytes" => [(.init name t[string] (.det (.strConst () "")) .empty), (.havoc name .empty)] + | "bool" => [(.init name t[bool] (.det (.boolConst pySynthLoc false)) .empty), (.havoc name .empty)] + | "str" => [(.init name t[string] (.det (.strConst pySynthLoc "")) .empty), (.havoc name .empty)] + | "int" => [(.init name t[int] (.det (.intConst pySynthLoc 0)) .empty), (.havoc name .empty)] + | "float" => [(.init name t[string] (.det (.strConst pySynthLoc "0.0")) .empty), (.havoc name .empty)] -- Floats as strs for now + | "bytes" => [(.init name t[string] (.det (.strConst pySynthLoc "")) .empty), (.havoc name .empty)] | "Client" => [(.init name clientType (.det dummyClient) .empty), (.havoc name .empty)] | "Dict[str Any]" => [(.init name dictStrAnyType (.det dummyDictStrAny) .empty), (.havoc name .empty)] | "List[str]" => [(.init name listStrType (.det dummyListStr) .empty), (.havoc name .empty)] @@ -371,7 +380,7 @@ partial def collectVarDecls (translation_ctx : TranslationContext) (stmts: Array match user_defined_class with | .some i => let user_defined_class_ty := .forAll [] (.tcons i.name []) - let user_defined_class_dummy := .fvar () ("DUMMY_" ++ i.name) none + let user_defined_class_dummy := .fvar pySynthLoc ("DUMMY_" ++ i.name) none [(.init name user_defined_class_ty (.det user_defined_class_dummy) .empty), (.havoc name .empty)] | .none => panic! s!"Unsupported type annotation: `{ty_name}`" let foo := dedup.map toCore @@ -469,29 +478,30 @@ partial def argsAndKWordsToCanonicalList (translation_ctx : TranslationContext) partial def handleDict (translation_ctx: TranslationContext) (sr : SourceRange) (keys: Array (Python.opt_expr SourceRange)) (values: Array (Python.expr SourceRange)) : PyExprTranslated := let md := sourceRangeToMetaData translation_ctx.filePath sr - let dict := .app () (.op () "DictStrAny_mk" none) (.strConst () "DefaultDict") -- TODO: need to generate unique dict arg + let dict := .app pySynthLoc (.op pySynthLoc "DictStrAny_mk" none) (.strConst pySynthLoc "DefaultDict") -- TODO: need to generate unique dict arg assert! keys.size == values.size let zipped := Array.zip keys values let res := zipped.toList.flatMap (λ (k, v) => let n := PyOptExprToString k - let in_dict := (.assume s!"assume_{n}_in_dict" (.app () (.app () (.op () "str_in_dict_str_any" none) (.strConst () n)) dict) md) + let in_dict := (.assume s!"assume_{n}_in_dict" (.app pySynthLoc (.app pySynthLoc (.op pySynthLoc "str_in_dict_str_any" none) (.strConst pySynthLoc n)) dict) md) match v with | .Call _ f args _ => match f with | .Name _ {ann := _ , val := "str"} _ => assert! args.val.size == 1 - let dt := (.app () (.op () "datetime_to_str" none) ((PyExprToCore default args.val[0]!).expr)) - let dict_of_v_is_k := (.assume s!"assume_{n}_key" (.eq () (.app () (.app () (.op () "dict_str_any_get_str" none) dict) (.strConst () n)) dt) md) + let dt := (.app pySynthLoc (.op pySynthLoc "datetime_to_str" none) ((PyExprToCore default args.val[0]!).expr)) + let dict_of_v_is_k := (.assume s!"assume_{n}_key" (.eq pySynthLoc (.app pySynthLoc (.app pySynthLoc (.op pySynthLoc "dict_str_any_get_str" none) dict) (.strConst pySynthLoc n)) dt) md) [in_dict, dict_of_v_is_k] | _ => panic! "Unsupported function when constructing map" | _ => - let dict_of_v_is_k := (.assume s!"assume_{n}_key" (.eq () (.app () (.app () (.op () "dict_str_any_get_str" none) dict) (.strConst () n)) (.strConst () "DummyVal")) md) + let dict_of_v_is_k := (.assume s!"assume_{n}_key" (.eq pySynthLoc (.app pySynthLoc (.app pySynthLoc (.op pySynthLoc "dict_str_any_get_str" none) dict) (.strConst pySynthLoc n)) (.strConst pySynthLoc "DummyVal")) md) [in_dict, dict_of_v_is_k]) {stmts := res , expr := dict, post_stmts := []} partial def PyExprToCore (translation_ctx : TranslationContext) (e : Python.expr SourceRange) (substitution_records : Option (List SubstitutionRecord) := none) : PyExprTranslated := + let loc := pyLoc translation_ctx.filePath e.toAst.ann if h : substitution_records.isSome && (substitution_records.get!.find? (λ r => PyExprIdent r.pyExpr e)).isSome then have hr : (List.find? (fun r => PyExprIdent r.pyExpr e) substitution_records.get!).isSome = true := by rw [Bool.and_eq_true] at h; exact h.2 let record := (substitution_records.get!.find? (λ r => PyExprIdent r.pyExpr e)).get hr @@ -500,20 +510,20 @@ partial def PyExprToCore (translation_ctx : TranslationContext) (e : Python.expr match e with | .Call _ f args kwords => panic! s!"Call should be handled at stmt level: \n(func: {repr f}) \n(Records: {repr substitution_records}) \n(AST: {repr e.toAst})" - | .Constant _ c _ => {stmts := [], expr := PyConstToCore c} + | .Constant _ c _ => {stmts := [], expr := PyConstToCore loc c} | .Name _ n _ => match n.val with - | "AssertionError" | "Exception" => {stmts := [], expr := .strConst () n.val} + | "AssertionError" | "Exception" => {stmts := [], expr := .strConst loc n.val} | s => match translation_ctx.variableTypes.find? (λ p => p.fst == s) with | .some p => if translation_ctx.expectedType == some (.tcons "bool" []) && p.snd == (.tcons "DictStrAny" []) then - let a := .fvar () n.val none - let e := .app () (Core.coreOpExpr (.bool .Not)) (.eq () (.app () (.op () "dict_str_any_length" none) a) (.intConst () 0)) + let a := .fvar loc n.val none + let e := .app loc (Core.coreOpExpr (.bool .Not)) (.eq loc (.app loc (.op pySynthLoc "dict_str_any_length" none) a) (.intConst loc 0)) {stmts := [], expr := e} else - {stmts := [], expr := .fvar () n.val none} - | .none => {stmts := [], expr := .fvar () n.val none} + {stmts := [], expr := .fvar loc n.val none} + | .none => {stmts := [], expr := .fvar loc n.val none} | .JoinedStr _ ss => PyExprToCore translation_ctx ss.val[0]! -- TODO: need to actually join strings | .BinOp _ lhs op rhs => let lhs := (PyExprToCore translation_ctx lhs) @@ -535,9 +545,9 @@ partial def PyExprToCore (translation_ctx : TranslationContext) (e : Python.expr match op.val with | #[v] => match v with | Strata.Python.cmpop.Eq _ => - {stmts := lhs.stmts ++ rhs.stmts, expr := (.eq () lhs.expr rhs.expr)} + {stmts := lhs.stmts ++ rhs.stmts, expr := (.eq loc lhs.expr rhs.expr)} | Strata.Python.cmpop.In _ => - {stmts := lhs.stmts ++ rhs.stmts, expr := .app () (.app () (.op () "str_in_dict_str_any" none) lhs.expr) rhs.expr} + {stmts := lhs.stmts ++ rhs.stmts, expr := .app loc (.app pySynthLoc (.op pySynthLoc "str_in_dict_str_any" none) lhs.expr) rhs.expr} | Strata.Python.cmpop.Lt _ => {stmts := lhs.stmts ++ rhs.stmts, expr := handleLt translation_ctx lhs.expr rhs.expr} | Strata.Python.cmpop.LtE _ => @@ -557,24 +567,23 @@ partial def PyExprToCore (translation_ctx : TranslationContext) (e : Python.expr | _ => panic! "Unsupported UnaryOp: {repr e}" | .Subscript sr_sub v slice _ => let sub_md := sourceRangeToMetaData translation_ctx.filePath sr_sub + let sub_loc := pyLoc translation_ctx.filePath sr_sub let l := PyExprToCore translation_ctx v let k := PyExprToCore translation_ctx slice -- TODO: we need to plumb the type of `v` here - match s!"{repr l.expr}" with - | "LExpr.fvar () { name := \"keys\", metadata := () } none" => - -- let access_check : Core.Statement := .assert "subscript_bounds_check" (.app () (.app () (.op () "str_in_dict_str_any" none) k.expr) l.expr) - {stmts := l.stmts ++ k.stmts, expr := .app () (.app () (.op () "list_str_get" none) l.expr) k.expr} - | "LExpr.fvar () { name := \"blended_cost\", metadata := () } none" => - -- let access_check : Core.Statement := .assert "subscript_bounds_check" (.app () (.app () (.op () "str_in_dict_str_any" none) k.expr) l.expr) - {stmts := l.stmts ++ k.stmts, expr := .app () (.app () (.op () "dict_str_any_get_str" none) l.expr) k.expr} + match l.expr with + | .fvar _ ⟨"keys", _⟩ _ => + {stmts := l.stmts ++ k.stmts, expr := .app sub_loc (.app pySynthLoc (.op pySynthLoc "list_str_get" none) l.expr) k.expr} + | .fvar _ ⟨"blended_cost", _⟩ _ => + {stmts := l.stmts ++ k.stmts, expr := .app sub_loc (.app pySynthLoc (.op pySynthLoc "dict_str_any_get_str" none) l.expr) k.expr} | _ => match translation_ctx.expectedType with | .some (.tcons "ListStr" []) => - let access_check : Core.Statement := .assert "subscript_bounds_check" (.app () (.app () (.op () "str_in_dict_str_any" none) k.expr) l.expr) sub_md - {stmts := l.stmts ++ k.stmts ++ [access_check], expr := .app () (.app () (.op () "dict_str_any_get_list_str" none) l.expr) k.expr} + let access_check : Core.Statement := .assert "subscript_bounds_check" (.app sub_loc (.app pySynthLoc (.op pySynthLoc "str_in_dict_str_any" none) k.expr) l.expr) sub_md + {stmts := l.stmts ++ k.stmts ++ [access_check], expr := .app sub_loc (.app pySynthLoc (.op pySynthLoc "dict_str_any_get_list_str" none) l.expr) k.expr} | _ => - let access_check : Core.Statement := .assert "subscript_bounds_check" (.app () (.app () (.op () "str_in_dict_str_any" none) k.expr) l.expr) sub_md - {stmts := l.stmts ++ k.stmts ++ [access_check], expr := .app () (.app () (.op () "dict_str_any_get" none) l.expr) k.expr} + let access_check : Core.Statement := .assert "subscript_bounds_check" (.app sub_loc (.app pySynthLoc (.op pySynthLoc "str_in_dict_str_any" none) k.expr) l.expr) sub_md + {stmts := l.stmts ++ k.stmts ++ [access_check], expr := .app sub_loc (.app pySynthLoc (.op pySynthLoc "dict_str_any_get" none) l.expr) k.expr} | .List _ elmts _ => match elmts.val[0]! with | .Constant _ expr _ => match expr with @@ -594,11 +603,11 @@ partial def initTmpParam (translation_ctx: TranslationContext) (p: Python.expr S match f with | .Name _ n _ => match n.val with - | "json_dumps" => [(.init p.snd t[string] (.det (.strConst () "")) md), .call "json_dumps" ([.inArg (.app () (.op () "DictStrAny_mk" none) (.strConst () "DefaultDict")), .inArg (Strata.Python.TypeStrToCoreExpr "IntOrNone")] ++ [.outArg p.snd, .outArg "maybe_except"]) md] + | "json_dumps" => [(.init p.snd t[string] (.det (.strConst pySynthLoc "")) md), .call "json_dumps" ([.inArg (.app pySynthLoc (.op pySynthLoc "DictStrAny_mk" none) (.strConst pySynthLoc "DefaultDict")), .inArg (Strata.Python.TypeStrToCoreExpr "IntOrNone")] ++ [.outArg p.snd, .outArg "maybe_except"]) md] | "str" => assert! args.val.size == 1 - [(.init p.snd t[string] (.det (.strConst () "")) md), .set p.snd (.app () (.op () "datetime_to_str" none) ((PyExprToCore default args.val[0]!).expr)) md] - | "int" => [(.init p.snd t[int] (.det (.intConst () 0)) md), .set p.snd (.op () "datetime_to_int" none) md] + [(.init p.snd t[string] (.det (.strConst pySynthLoc "")) md), .set p.snd (.app pySynthLoc (.op pySynthLoc "datetime_to_str" none) ((PyExprToCore default args.val[0]!).expr)) md] + | "int" => [(.init p.snd t[int] (.det (.intConst pySynthLoc 0)) md), .set p.snd (.op pySynthLoc "datetime_to_int" none) md] | _ => panic! s!"Unsupported name {n.val}" | _ => panic! s!"Unsupported tmp param init call: {repr f}" | _ => panic! "Expected Call" @@ -612,15 +621,15 @@ partial def exceptHandlersToCore (jmp_targets: List String) (translation_ctx: Tr | .some ex_ty => let inherits_from : Core.CoreIdent := "inheritsFrom" let get_ex_tag : Core.CoreIdent := "ExceptOrNone..code_val!" - let exception_ty : Core.Expression.Expr := .app () (.op () get_ex_tag none) (.fvar () "maybe_except" none) - let rhs_curried : Core.Expression.Expr := .app () (.op () inherits_from none) exception_ty + let exception_ty : Core.Expression.Expr := .app pySynthLoc (.op pySynthLoc get_ex_tag none) (.fvar pySynthLoc "maybe_except" none) + let rhs_curried : Core.Expression.Expr := .app pySynthLoc (.op pySynthLoc inherits_from none) exception_ty let res := PyExprToCore translation_ctx ex_ty - let rhs : Core.Expression.Expr := .app () rhs_curried (res.expr) + let rhs : Core.Expression.Expr := .app pySynthLoc rhs_curried (res.expr) let call := .set "exception_ty_matches" rhs md res.stmts ++ [call] | .none => - [.set "exception_ty_matches" (.boolConst () false) md] - let cond := .fvar () "exception_ty_matches" none + [.set "exception_ty_matches" (.boolConst pySynthLoc false) md] + let cond := .fvar pySynthLoc "exception_ty_matches" none let body_if_matches := body.val.toList.flatMap (λ s => (PyStmtToCore jmp_targets.tail! translation_ctx s).fst) ++ [.exit jmp_targets[1]! md] set_ex_ty_matches ++ [.ite (.det cond) body_if_matches [] md] @@ -647,8 +656,8 @@ partial def handleFunctionCall (lhs: List Core.Expression.Ident) if isCall arg then some arg else none) let kwords_calls_to_tmps := nested_kwords_calls.map (λ a => (a, s!"call_kword_tmp_{a.toAst.ann.start}")) - let substitution_records : List SubstitutionRecord := args_calls_to_tmps.toList.map (λ p => {pyExpr := p.fst, coreExpr := .fvar () p.snd none}) ++ - kwords_calls_to_tmps.toList.map (λ p => {pyExpr := p.fst, coreExpr := .fvar () p.snd none}) + let substitution_records : List SubstitutionRecord := args_calls_to_tmps.toList.map (λ p => {pyExpr := p.fst, coreExpr := .fvar pySynthLoc p.snd none}) ++ + kwords_calls_to_tmps.toList.map (λ p => {pyExpr := p.fst, coreExpr := .fvar pySynthLoc p.snd none}) let md := sourceRangeToMetaData translation_ctx.filePath s.toAst.ann let res := argsAndKWordsToCanonicalList translation_ctx fname args.val kwords.val substitution_records @@ -662,9 +671,9 @@ partial def handleComprehension (translation_ctx: TranslationContext) (lhs: Pyth | .mk_comprehension sr _ itr _ _ => let md := sourceRangeToMetaData translation_ctx.filePath sr let res := PyExprToCore default itr - let guard := .app () (Core.coreOpExpr (.bool .Not)) (.eq () (.app () (.op () "dict_str_any_length" none) res.expr) (.intConst () 0)) + let guard := .app pySynthLoc (Core.coreOpExpr (.bool .Not)) (.eq pySynthLoc (.app pySynthLoc (.op pySynthLoc "dict_str_any_length" none) res.expr) (.intConst pySynthLoc 0)) let then_ss: List Core.Statement := [.havoc (PyExprToString lhs) md] - let else_ss: List Core.Statement := [.set (PyExprToString lhs) (.op () "ListStr_nil" none) md] + let else_ss: List Core.Statement := [.set (PyExprToString lhs) (.op pySynthLoc "ListStr_nil" none) md] res.stmts ++ [.ite (.det guard) then_ss else_ss md] partial def PyStmtToCore (jmp_targets: List String) (translation_ctx : TranslationContext) (s : Python.stmt SourceRange) : List Core.Statement × TranslationContext := @@ -725,7 +734,7 @@ partial def PyStmtToCore (jmp_targets: List String) (translation_ctx : Translati | .none => ([.exit jmp_targets[0]! md], none) | .For _ tgt itr body _ _ => -- Do one unrolling: - let guard := .app () (Core.coreOpExpr (.bool .Not)) (.eq () (.app () (.op () "dict_str_any_length" none) (PyExprToCore default itr).expr) (.intConst () 0)) + let guard := .app pySynthLoc (Core.coreOpExpr (.bool .Not)) (.eq pySynthLoc (.app pySynthLoc (.op pySynthLoc "dict_str_any_length" none) (PyExprToCore default itr).expr) (.intConst pySynthLoc 0)) match tgt with | .Name _ n _ => let assign_tgt := [(.init n.val dictStrAnyType (.det dummyDictStrAny) md)] @@ -734,7 +743,7 @@ partial def PyStmtToCore (jmp_targets: List String) (translation_ctx : Translati -- TODO: missing havoc | .While _ test body _ => -- Do one unrolling: - let guard := .app () (Core.coreOpExpr (.bool .Not)) (.eq () (.app () (.op () "dict_str_any_length" none) (PyExprToCore default test).expr) (.intConst () 0)) + let guard := .app pySynthLoc (Core.coreOpExpr (.bool .Not)) (.eq pySynthLoc (.app pySynthLoc (.op pySynthLoc "dict_str_any_length" none) (PyExprToCore default test).expr) (.intConst pySynthLoc 0)) ([.ite (.det guard) (ArrPyStmtToCore translation_ctx body.val).fst [] md], none) -- TODO: missing havoc | .Assert sr a _ => @@ -747,7 +756,7 @@ partial def PyStmtToCore (jmp_targets: List String) (translation_ctx : Translati match lhs with | .Name _ n _ => let rhs := PyExprToCore translation_ctx rhs - let new_lhs := (.strConst () "DUMMY_FLOAT") + let new_lhs := (.strConst pySynthLoc "DUMMY_FLOAT") (rhs.stmts ++ [.set n.val new_lhs md], none) | _ => panic! s!"Expected lhs to be name: {repr lhs}" | .FloorDiv _ => @@ -755,7 +764,7 @@ partial def PyStmtToCore (jmp_targets: List String) (translation_ctx : Translati | .Name _ n _ => let lhs := PyExprToCore translation_ctx lhs let rhs := PyExprToCore translation_ctx rhs - let new_lhs := .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Div⟩) (some mty[int → (int → int)])) lhs.expr) rhs.expr + let new_lhs := .app pySynthLoc (.app pySynthLoc (Core.coreOpExpr (.numeric ⟨.int, .Div⟩) (some mty[int → (int → int)])) lhs.expr) rhs.expr (rhs.stmts ++ [.set n.val new_lhs md], none) | _ => panic! s!"Expected lhs to be name: {repr lhs}" | _ => panic! s!"Unsupported AugAssign op: {repr op}" @@ -804,7 +813,7 @@ def pyTyStrToLMonoTy (ty_str: String) : Lambda.LMonoTy := def pythonFuncToCore (name : String) (args: List (String × String)) (body: Array (Python.stmt SourceRange)) (ret : Option (Python.expr SourceRange)) (spec : Core.Procedure.Spec) (translation_ctx : TranslationContext) : Core.Procedure := let inputs : List (Lambda.Identifier Unit × Lambda.LMonoTy) := args.map (λ p => (p.fst, pyTyStrToLMonoTy p.snd)) - let varDecls := collectVarDecls translation_ctx body ++ [(.init "exception_ty_matches" t[bool] (.det (.boolConst () false)) .empty), (.havoc "exception_ty_matches" .empty)] + let varDecls := collectVarDecls translation_ctx body ++ [(.init "exception_ty_matches" t[bool] (.det (.boolConst pySynthLoc false)) .empty), (.havoc "exception_ty_matches" .empty)] let stmts := (ArrPyStmtToCore translation_ctx body).fst let body := varDecls ++ [.block "end" stmts .empty] let constructor := name.endsWith "___init__" diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 0c1a030899..506e07a444 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1761,7 +1761,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang let typeAssert := match target with | .Name _ n _ => if !typeAssertSafe then [] - else if s.toAst.ann == default then [] -- compiler-generated statement, no source location + else if s.toAst.ann.isNone then [] -- compiler-generated statement, no source location else let annStr := pyExprToString annotation match typeTester? annStr with diff --git a/Strata/Languages/Python/Regex/ReToCore.lean b/Strata/Languages/Python/Regex/ReToCore.lean index c889b3f09d..35877141b1 100644 --- a/Strata/Languages/Python/Regex/ReToCore.lean +++ b/Strata/Languages/Python/Regex/ReToCore.lean @@ -115,39 +115,42 @@ private def rr2r := mty[regex → (regex → regex)] private def ss2r := mty[string → (string → regex)] private def rii2r := mty[regex → (int → (int → regex))] +/-- Metadata for regex-to-Core synthesized expressions. -/ +private abbrev regexSynthLoc : ExprSourceLoc := ExprSourceLoc.synthesized "regex" + /-- Empty regex pattern; matches an empty string. -/ private def Core.emptyRegex : Expression.Expr := - mkApp () (.op () strToRegexFunc.name (some s2r)) [strConst () ""] + mkApp regexSynthLoc (.op regexSynthLoc strToRegexFunc.name (some s2r)) [strConst regexSynthLoc ""] /-- Unmatchable regex pattern. -/ private def Core.unmatchableRegex : Expression.Expr := - mkApp () (.op () reNoneFunc.name (some reTy)) [] + mkApp regexSynthLoc (.op regexSynthLoc reNoneFunc.name (some reTy)) [] -- Core regex expression builders. private abbrev mkReFromStr (s : String) : Expression.Expr := - mkApp () (.op () strToRegexFunc.name (some s2r)) [strConst () s] + mkApp regexSynthLoc (.op regexSynthLoc strToRegexFunc.name (some s2r)) [strConst regexSynthLoc s] private abbrev mkReRange (c1 c2 : Char) : Expression.Expr := - mkApp () (.op () reRangeFunc.name (some ss2r)) [strConst () (toString c1), strConst () (toString c2)] + mkApp regexSynthLoc (.op regexSynthLoc reRangeFunc.name (some ss2r)) [strConst regexSynthLoc (toString c1), strConst regexSynthLoc (toString c2)] private abbrev mkReAllChar : Expression.Expr := - .op () reAllCharFunc.name (some reTy) + .op regexSynthLoc reAllCharFunc.name (some reTy) private abbrev mkReComp (r : Expression.Expr) : Expression.Expr := - mkApp () (.op () reCompFunc.name (some r2r)) [r] + mkApp regexSynthLoc (.op regexSynthLoc reCompFunc.name (some r2r)) [r] private abbrev mkReUnion (a b : Expression.Expr) : Expression.Expr := - mkApp () (.op () reUnionFunc.name (some rr2r)) [a, b] + mkApp regexSynthLoc (.op regexSynthLoc reUnionFunc.name (some rr2r)) [a, b] private abbrev mkReConcat (a b : Expression.Expr) : Expression.Expr := - mkApp () (.op () reConcatFunc.name (some rr2r)) [a, b] + mkApp regexSynthLoc (.op regexSynthLoc reConcatFunc.name (some rr2r)) [a, b] private abbrev mkReInter (a b : Expression.Expr) : Expression.Expr := - mkApp () (.op () reInterFunc.name (some rr2r)) [a, b] + mkApp regexSynthLoc (.op regexSynthLoc reInterFunc.name (some rr2r)) [a, b] private abbrev mkReStar (r : Expression.Expr) : Expression.Expr := - mkApp () (.op () reStarFunc.name (some r2r)) [r] + mkApp regexSynthLoc (.op regexSynthLoc reStarFunc.name (some r2r)) [r] private abbrev mkRePlus (r : Expression.Expr) : Expression.Expr := - mkApp () (.op () rePlusFunc.name (some r2r)) [r] + mkApp regexSynthLoc (.op regexSynthLoc rePlusFunc.name (some r2r)) [r] private abbrev mkReLoop (r : Expression.Expr) (lo hi : Nat) : Expression.Expr := - mkApp () (.op () reLoopFunc.name (some rii2r)) [r, intConst () lo, intConst () hi] + mkApp regexSynthLoc (.op regexSynthLoc reLoopFunc.name (some rii2r)) [r, intConst regexSynthLoc lo, intConst regexSynthLoc hi] /-- Shared body for `star` and `loop {0, m}` (m ≥ 2): @@ -313,7 +316,7 @@ private def RegexAST.toCore (r : RegexAST) (atStart atEnd : Bool) : def pythonRegexToCore (pyRegex : String) (mode : MatchMode := .fullmatch) : Core.Expression.Expr × Option ParseError := match parseTop pyRegex with - | .error err => (mkApp () (.op () reAllFunc.name (some reTy)) [], some err) + | .error err => (mkApp regexSynthLoc (.op regexSynthLoc reAllFunc.name (some reTy)) [], some err) | .ok ast => -- `dotStar`: passed with `atStart=false`, `atEnd=false` since `anychar` -- ignores both. diff --git a/Strata/MetaVerifier.lean b/Strata/MetaVerifier.lean index c841f4c107..ed82122eda 100644 --- a/Strata/MetaVerifier.lean +++ b/Strata/MetaVerifier.lean @@ -207,7 +207,14 @@ deriving instance ToExpr for SMT.Term deriving instance ToExpr for Core.SMT.Sort deriving instance ToExpr for Core.SMT.IF deriving instance ToExpr for SanitizedContext -deriving instance ToExpr for Core.CoreExprMetadata +meta instance : ToExpr Strata.Uri where + toTypeExpr := mkConst ``Strata.Uri + toExpr + | .file p => mkApp (mkConst ``Strata.Uri.file) (toExpr p) + +meta instance : ToExpr ExprSourceLoc where + toTypeExpr := mkConst ``ExprSourceLoc + toExpr e := mkApp3 (mkConst ``ExprSourceLoc.mk) (toExpr e.uri) (toExpr e.range) (toExpr e.relatedLocs) deriving instance ToExpr for Lambda.LMonoTy instance [ToExpr α] : ToExpr (Lambda.Identifier α) where diff --git a/Strata/Transform/ANFEncoder.lean b/Strata/Transform/ANFEncoder.lean index 6f30267052..9f8d10b571 100644 --- a/Strata/Transform/ANFEncoder.lean +++ b/Strata/Transform/ANFEncoder.lean @@ -29,6 +29,8 @@ The pass walks procedure bodies via `anfEncodeProgram`, hoisting duplicated subexpressions into `var` declarations prepended to the body. -/ +-- ANF-synthesized fresh variables carry the source location of the expression they replace. + public section namespace Core.ANFEncoder @@ -71,7 +73,7 @@ private structure ExprKey where expr : Expression.Expr private instance : BEq ExprKey where - beq a b := a.expr == b.expr + beq a b := a.expr.eqModuloMeta b.expr private instance : Hashable ExprKey where hash k := LExpr.hashExpr k.expr @@ -139,7 +141,7 @@ where check (h : UInt64) (e : Expression.Expr) : UInt64 × Expression.Expr := match replacements[h]? with | some pairs => - match pairs.find? (fun (t, _) => e == t) with + match pairs.find? (fun (t, _) => e.eqModuloMeta t) with | some (_, replacement) => (h, replacement) | none => (h, e) | none => (h, e) @@ -251,7 +253,7 @@ where let (revDecls, replacements, nextIdx) := targets.foldl (fun (decls, repMap, idx) dup => let freshName : CoreIdent := ⟨s!"{anfVarPrefix}{idx}", ()⟩ let freshTy := dup.typeOf - let freshVar : Expression.Expr := .fvar () freshName freshTy + let freshVar : Expression.Expr := .fvar dup.metadata freshName freshTy let ty : Expression.Ty := match freshTy with | some mty => LTy.forAll [] mty | none => LTy.forAll ["α"] (.ftvar "α") diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean index 5b7c165ca7..51e6ebe55c 100644 --- a/Strata/Transform/CallElimCorrect.lean +++ b/Strata/Transform/CallElimCorrect.lean @@ -26,6 +26,9 @@ import Strata.DL.Util.ListUtils `Stmt`. This proof will be re-done with a new small-step semantics in the near future. + Variable references in these proofs use `ExprSourceLoc.synthesized "transform"` to match the + synthesized expressions produced by the call elimination transform. + This file contains the main proof that the call elimination transformation is semantics preserving (see `callElimStatementCorrect`). Additionally, `callElimBlockNoExcept` shows that the call elimination @@ -513,7 +516,7 @@ theorem EvalStatementContractInitVar : constructor constructor . apply Imperative.EvalCmd.eval_init <;> try assumption - have Hwfv := Hwf (Lambda.LExpr.fvar () v none) v σ + have Hwfv := Hwf (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") v none) v σ rw [Hwfv]; assumption simp [Imperative.HasFvar.getFvar] apply Imperative.InitState.init Hnone @@ -1043,8 +1046,8 @@ theorem Lambda.LExpr.substFvarCorrect : simp [Imperative.HasFvar.getFvar] case abs m ty e ih => specialize ih Hinv - have e2 := (e.substFvar fro (Lambda.LExpr.fvar () to none)) - have Hwfc := Hwfc.1 σ σ' e ((e.substFvar fro (Lambda.LExpr.fvar () to none))) + have e2 := (e.substFvar fro (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") to none)) + have Hwfc := Hwfc.1 σ σ' e ((e.substFvar fro (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") to none))) grind case quant m k ty tr e trih eih => simp [Imperative.invStores, Imperative.substStores, @@ -1929,7 +1932,7 @@ NormalizedOldExpr e → rename_i md tyy id v have HH2 := HH md tyy () id v simp_all - have Hnold' : ¬ IsOldPred (substOld h (Lambda.LExpr.fvar () h' none) fn) := by + have Hnold' : ¬ IsOldPred (substOld h (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") h' none) fn) := by intros Hold apply Hnold apply substOldIsOldPred' ?_ Hold @@ -1982,8 +1985,8 @@ theorem substOldExpr_cons: split <;> simp [*] simp_all [createOldVarsSubst, createFvar] rename_i _ fn e _ _ H - generalize H1: (OldExpressions.substOld h.snd (Lambda.LExpr.fvar () h.fst.fst none) fn) = fn' - generalize H2: (OldExpressions.substOld h.snd (Lambda.LExpr.fvar () h.fst.fst none) e) = e' + generalize H1: (OldExpressions.substOld h.snd (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") h.fst.fst none) fn) = fn' + generalize H2: (OldExpressions.substOld h.snd (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") h.fst.fst none) e) = e' rw (occs := [3]) [Core.OldExpressions.substsOldExpr.eq_def] simp; split simp_all [Map.isEmpty]; rename_i H; split at H <;> simp_all @@ -3155,7 +3158,7 @@ theorem substsOldPostSubset: have ih := @ih post Hdisj have : (Imperative.HasVarsPure.getVars - (substsOldExpr ((h.snd, Lambda.LExpr.fvar () h.1.fst none) :: List.map createOldVarsSubst.go t) post)).Subset + (substsOldExpr ((h.snd, Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") h.1.fst none) :: List.map createOldVarsSubst.go t) post)).Subset ((Imperative.HasVarsPure.getVars (substsOldExpr (List.map createOldVarsSubst.go t) post)) ++ [h.1.fst]) := by apply substOldExprPostSubset apply List.Subset.trans this diff --git a/Strata/Transform/CoreTransform.lean b/Strata/Transform/CoreTransform.lean index d621676ee0..806bc9dd6a 100644 --- a/Strata/Transform/CoreTransform.lean +++ b/Strata/Transform/CoreTransform.lean @@ -13,6 +13,8 @@ public import Strata.Util.Statistics /-! # Utility functions for program transformation in Strata Core -/ +-- Synthesized expressions from transforms carry ExprSourceLoc.synthesized provenance. + public section namespace Core @@ -31,9 +33,11 @@ def createHavoc (ident : Expression.Ident) def createHavocs (ident : List Expression.Ident) (md : (Imperative.MetaData Expression)) : List Statement := ident.map (createHavoc · md) +/-- Create a free variable reference from an identifier. + Synthesized during transforms; carries provenance via ExprSourceLoc.synthesized. -/ def createFvar (ident : Expression.Ident) : Expression.Expr - := Lambda.LExpr.fvar ((): ExpressionMetadata) ident none + := Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") ident none @[expose] def createFvars (ident : List Expression.Ident) @@ -211,13 +215,14 @@ def createInits (trips : List ((Expression.Ident × Expression.Ty) × Expression trips.map (createInit · md) /-- -Generate an init statement with rhs as a free variable reference +Generate an init statement with rhs as a free variable reference. +Synthesized during transforms; carries provenance via ExprSourceLoc.synthesized. -/ def createInitVar (trip : (Expression.Ident × Expression.Ty) × Expression.Ident) (md:Imperative.MetaData Expression) : Statement := match trip with - | ((v', ty), v) => Statement.init v' ty (.det (Lambda.LExpr.fvar () v none)) md + | ((v', ty), v) => Statement.init v' ty (.det (Lambda.LExpr.fvar (ExprSourceLoc.synthesized "transform") v none)) md def createInitVars (trips : List ((Expression.Ident × Expression.Ty) × Expression.Ident)) (md : (Imperative.MetaData Expression)) diff --git a/Strata/Transform/ProcBodyVerify.lean b/Strata/Transform/ProcBodyVerify.lean index aa68c38a96..8afb94739d 100644 --- a/Strata/Transform/ProcBodyVerify.lean +++ b/Strata/Transform/ProcBodyVerify.lean @@ -49,6 +49,8 @@ block "verify_P" { ``` -/ +-- Synthesized expressions carry ExprSourceLoc.synthesized "proc-body-verify" provenance. + namespace Core.ProcBodyVerify open Core Imperative Transform @@ -82,7 +84,8 @@ open Core Imperative Transform -- Initialize old variables of in-out parameters (those in both inputs and outputs). let oldInoutInits ← proc.header.getInoutParams.mapM fun (id,ty) => do let oldG := CoreIdent.mkOld id.name - let e : Core.Expression.Expr := .fvar () id none + -- Synthesized variable reference for old-value initialization + let e : Core.Expression.Expr := .fvar (ExprSourceLoc.synthesized "proc-body-verify") id none return (Statement.init oldG (Lambda.LTy.forAll [] ty) (.det e) #[]) -- Convert preconditions to assumes diff --git a/Strata/Transform/ProcBodyVerifyCorrect.lean b/Strata/Transform/ProcBodyVerifyCorrect.lean index 515f44dee2..f40c811811 100644 --- a/Strata/Transform/ProcBodyVerifyCorrect.lean +++ b/Strata/Transform/ProcBodyVerifyCorrect.lean @@ -300,7 +300,8 @@ private theorem PrefixStepsOK_nondet_init_map exact h_nodup.1 (heq ▸ List.mem_map_of_mem (f := Prod.fst) hmem) /-- For a deterministic init `init oldG ty (.det (fvar id))`, if `id` has a value - in the pre-state, `oldG` is none, and `oldG ≠ id`, then it steps correctly. -/ + in the pre-state, `oldG` is none, and `oldG ≠ id`, then it steps correctly. + The `fvar` uses `ExprSourceLoc.synthesized` to match the synthesized init from `ProcBodyVerify`. -/ private theorem PrefixStepsOK_det_init_cons (π : String → Option Procedure) (φ : CoreEval → PureFunc Expression → CoreEval) (id : Expression.Ident) (oldG : Expression.Ident) (ty : Expression.Ty) (rest : List Statement) @@ -312,21 +313,21 @@ private theorem PrefixStepsOK_det_init_cons (h_id_eq_old : (prefixInitEnv rest ρ).store id = (prefixInitEnv rest ρ).store oldG) (h_ne : oldG ≠ id) : PrefixStepsOK π φ - (Statement.init oldG ty (.det (LExpr.fvar () id none)) #[] :: rest) ρ := by + (Statement.init oldG ty (.det (LExpr.fvar (ExprSourceLoc.synthesized "proc-body-verify") id none)) #[] :: rest) ρ := by constructor · exact h_rest · refine ⟨_, rfl, (prefixInitEnv rest ρ).store, ?_, rfl⟩ - have h_none : (prefixInitEnv (Statement.init oldG ty (.det (LExpr.fvar () id none)) #[] :: rest) ρ).store oldG = none := + have h_none : (prefixInitEnv (Statement.init oldG ty (.det (LExpr.fvar (ExprSourceLoc.synthesized "proc-body-verify") id none)) #[] :: rest) ρ).store oldG = none := prefixInitEnv_store_init _ _ _ _ rfl - have h_id_val : (prefixInitEnv (Statement.init oldG ty (.det (LExpr.fvar () id none)) #[] :: rest) ρ).store id = + have h_id_val : (prefixInitEnv (Statement.init oldG ty (.det (LExpr.fvar (ExprSourceLoc.synthesized "proc-body-verify") id none)) #[] :: rest) ρ).store id = (prefixInitEnv rest ρ).store id := by rw [prefixInitEnv_store_other _ _ _ id oldG rfl h_ne] rw [Option.isSome_iff_exists] at h_old_some obtain ⟨v, hv⟩ := h_old_some - have h_getFvar : HasFvar.getFvar (LExpr.fvar () id none : Expression.Expr) = some id := by + have h_getFvar : HasFvar.getFvar (LExpr.fvar (ExprSourceLoc.synthesized "proc-body-verify") id none : Expression.Expr) = some id := by simp [HasFvar.getFvar] - have h_eval : ρ.eval (prefixInitEnv (Statement.init oldG ty (.det (LExpr.fvar () id none)) #[] :: rest) ρ).store - (LExpr.fvar () id none) = some v := by + have h_eval : ρ.eval (prefixInitEnv (Statement.init oldG ty (.det (LExpr.fvar (ExprSourceLoc.synthesized "proc-body-verify") id none)) #[] :: rest) ρ).store + (LExpr.fvar (ExprSourceLoc.synthesized "proc-body-verify") id none) = some v := by rw [h_wfVar _ _ _ h_getFvar, h_id_val, h_id_eq_old, hv] exact EvalCommand.cmd_sem (EvalCmd.eval_init h_eval (InitState.init h_none hv (fun y hne => by @@ -351,7 +352,7 @@ private theorem PrefixStepsOK_det_init_map : PrefixStepsOK π φ (entries.map fun (id, ty) => Statement.init (CoreIdent.mkOld id.name) (Lambda.LTy.forAll [] ty) - (.det (LExpr.fvar () id none)) #[]) ρ := by + (.det (LExpr.fvar (ExprSourceLoc.synthesized "proc-body-verify") id none)) #[]) ρ := by induction entries with | nil => exact trivial | cons e rest ih => @@ -480,7 +481,7 @@ theorem procToVerifyStmt_structure Statement.init id (Lambda.LTy.forAll [] ty) .nondet #[] let oldInoutInits := proc.header.getInoutParams.toList.map fun (id, ty) => Statement.init (CoreIdent.mkOld id.name) (Lambda.LTy.forAll [] ty) - (.det (LExpr.fvar () id none)) #[] + (.det (LExpr.fvar (ExprSourceLoc.synthesized "proc-body-verify") id none)) #[] let assumes := requiresToAssumes proc.spec.preconditions let prefixStmts := inputInits ++ outputOnlyInits ++ oldInoutInits ++ assumes refine ⟨prefixStmts, h_eq.symm, ?_, ?_⟩ diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean index 752e626aa6..c631e4eea2 100644 --- a/Strata/Transform/ProcedureInlining.lean +++ b/Strata/Transform/ProcedureInlining.lean @@ -15,7 +15,10 @@ public import Strata.Transform.CoreTransform public import Strata.Languages.Core.PipelinePhase import Strata.Util.Tactics -/-! # Procedure Inlining Transformation -/ +/-! # Procedure Inlining Transformation + +-- Variable references synthesized during inlining carry ExprSourceLoc.synthesized "inlining" provenance. +-/ public section @@ -114,7 +117,7 @@ private def renameAllLocalNames (c:Procedure) -- renames LHS variables and labels. let new_body := List.map (fun (s0:Statement) => var_map.foldl (fun (s:Statement) (old_id,new_id) => - let s := Statement.substFvar s old_id (.fvar () new_id .none) + let s := Statement.substFvar s old_id (.fvar (ExprSourceLoc.synthesized "inlining") new_id .none) let s := Statement.renameLhs s old_id new_id Statement.replaceLabels s label_map) s0) c.body @@ -266,7 +269,7 @@ def inlineCallCmd let outs_lhs_and_sig := List.zip lhs out_vars List.map (fun (lhs_var,out_var) => - Statement.set lhs_var (.fvar () out_var (.none)) md) + Statement.set lhs_var (.fvar (ExprSourceLoc.synthesized "inlining") out_var (.none)) md) outs_lhs_and_sig let stmts:List (Imperative.Stmt Core.Expression Core.Command) diff --git a/Strata/Transform/TerminationCheck.lean b/Strata/Transform/TerminationCheck.lean index f0de27d583..bd3d7b55c1 100644 --- a/Strata/Transform/TerminationCheck.lean +++ b/Strata/Transform/TerminationCheck.lean @@ -55,6 +55,9 @@ inductive DecreasesKind where | structural (paramIdx : Nat) (dtName : String) | intValued (measure : Expression.Expr) +/-- Synthesized metadata for expressions generated by termination checking. -/ +private abbrev termMeta : ExpressionMetadata := ExprSourceLoc.synthesized "termination-check" + /-- Validate that a parameter index refers to a known ADT type, returning `.structural`. -/ private def validateStructuralParam (func : Function) (tf : @TypeFactory Unit) (idx : Nat) @@ -79,7 +82,7 @@ private def getDecreasesKind (func : Function) (tf : @TypeFactory Unit) match func.measure with | some (.fvar _ id _) => match func.inputs.findWithIdx? id with - | some (_, .int) => .ok (.intValued (.fvar () id (.some .int))) + | some (_, .int) => .ok (.intValued (.fvar termMeta id (.some .int))) | some (idx, _) => validateStructuralParam func tf idx | none => .error s!"recursive function '{func.name.name}': decreases variable '{id}' is not a parameter" @@ -125,15 +128,15 @@ private def extractTermObligations : Except String (List Expression.Expr) := go body [] where - go (e : Expression.Expr) (implications : List (Unit × Expression.Expr)) + go (e : Expression.Expr) (implications : List (ExpressionMetadata × Expression.Expr)) : Except String (List Expression.Expr) := match _he: e with | .ite _ c t f => do let cObs ← go c implications - let tObs ← go t (((), c) :: implications) + let tObs ← go t ((termMeta, c) :: implications) let notC : Expression.Expr := - LExpr.mkApp () (@boolNotFunc CoreLParams).opExpr [c] - let fObs ← go f (((), notC) :: implications) + LExpr.mkApp termMeta (@boolNotFunc CoreLParams).opExpr [c] + let fObs ← go f ((termMeta, notC) :: implications) return cObs ++ tObs ++ fObs | .app _ fn arg => match _h : getLFuncCall e with @@ -196,7 +199,7 @@ private def computeCallMeasure | .structural calleeIdx calleeDtName => match callArgs[calleeIdx]?, calleeInputTys[calleeIdx]? with | some arg, some calleeAdtTy => - .ok (LExpr.mkApp () (.op () (adtRankFuncName calleeDtName) (.some (.arrow calleeAdtTy .int))) [arg]) + .ok (LExpr.mkApp termMeta (.op termMeta (adtRankFuncName calleeDtName) (.some (.arrow calleeAdtTy .int))) [arg]) | _, _ => .error s!"termination checking '{calleeName}': decreasing parameter index {calleeIdx} is out of range at call site" | .intValued calleeMeasure => if calleeFormals.length != callArgs.length then @@ -211,8 +214,8 @@ private def computeCallerMeasure (func : Function) (kind : DecreasesKind) | .structural idx dtName => match func.inputs.keys[idx]?, func.inputs.values[idx]? with | some param, some adtTy => - .ok (LExpr.mkApp () (.op () (adtRankFuncName dtName) (.some (.arrow adtTy .int))) - [.fvar () param (.some adtTy)]) + .ok (LExpr.mkApp termMeta (.op termMeta (adtRankFuncName dtName) (.some (.arrow adtTy .int))) + [.fvar termMeta param (.some adtTy)]) | _, _ => .error s!"termination checking '{func.name.name}': decreasing parameter index {idx} is out of range" | .intValued m => .ok m @@ -250,11 +253,11 @@ private def mkTermCheckProc else if containsOpCall callMeasure recFuncNames then .error s!"termination checking '{func.name.name}': decreasing argument contains a recursive call" else - let decrease := LExpr.mkApp () (@intLtFunc CoreLParams).opExpr + let decrease := LExpr.mkApp termMeta (@intLtFunc CoreLParams).opExpr [callMeasure, callerMeasure] if needsNonNeg then - let nonNeg := LExpr.mkApp () (@intLeFunc CoreLParams).opExpr - [LExpr.intConst () 0, callMeasure] + let nonNeg := LExpr.mkApp termMeta (@intLeFunc CoreLParams).opExpr + [LExpr.intConst termMeta 0, callMeasure] .ok [nonNeg, decrease] else .ok [decrease] @@ -319,7 +322,7 @@ private def mkAdtRankDecls { namedDecls := block.map fun dt => (dt.name, Decl.func (mkAdtRankFunc (T := CoreLParams) dt) md) axioms := block.flatMap fun dt => - let axioms := mkAdtRankAxioms (T := CoreLParams) dt block () + let axioms := mkAdtRankAxioms (T := CoreLParams) dt block termMeta axioms.mapIdx fun i ax => (s!"{adtRankFuncName dt.name}_{i}", ax) } diff --git a/StrataTest/DL/Imperative/FormatStmtTest.lean b/StrataTest/DL/Imperative/FormatStmtTest.lean index 3b4062c932..48a0b9bfe6 100644 --- a/StrataTest/DL/Imperative/FormatStmtTest.lean +++ b/StrataTest/DL/Imperative/FormatStmtTest.lean @@ -5,6 +5,7 @@ -/ import Strata.Languages.Core.Statement import Strata.Languages.Core.DDMTransform.FormatCore +-- Test fixtures build Core expressions directly with synthesized provenance namespace FormatStmtTest open Core @@ -17,16 +18,16 @@ private abbrev Ss := List S private abbrev E := Expression.Expr private def intTy : Expression.Ty := .forAll [] .int -private def x : E := .fvar () (⟨"x", ()⟩) (some .int) -private def y : E := .fvar () (⟨"y", ()⟩) (some .int) -private def tt : E := .boolConst () true -private def int0 : E := .intConst () 0 -private def int1 : E := .intConst () 1 -private def int2 : E := .intConst () 2 -private def int42 : E := .intConst () 42 -private def xEq0 : E := .eq () x int0 -private def xEq5 : E := .eq () x (.intConst () 5) -private def xEq1 : E := .eq () x int1 +private def x : E := .fvar (ExprSourceLoc.synthesized "test") (⟨"x", ()⟩) (some .int) +private def y : E := .fvar (ExprSourceLoc.synthesized "test") (⟨"y", ()⟩) (some .int) +private def tt : E := .boolConst (ExprSourceLoc.synthesized "test") true +private def int0 : E := .intConst (ExprSourceLoc.synthesized "test") 0 +private def int1 : E := .intConst (ExprSourceLoc.synthesized "test") 1 +private def int2 : E := .intConst (ExprSourceLoc.synthesized "test") 2 +private def int42 : E := .intConst (ExprSourceLoc.synthesized "test") 42 +private def xEq0 : E := .eq (ExprSourceLoc.synthesized "test") x int0 +private def xEq5 : E := .eq (ExprSourceLoc.synthesized "test") x (.intConst (ExprSourceLoc.synthesized "test") 5) +private def xEq1 : E := .eq (ExprSourceLoc.synthesized "test") x int1 -- 1. cmd: init /-- info: var x : int := 0; -/ diff --git a/StrataTest/Languages/Boole/FeatureRequests/map_extensionality.lean b/StrataTest/Languages/Boole/FeatureRequests/map_extensionality.lean index 29f3ec9cfd..19194c115e 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/map_extensionality.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/map_extensionality.lean @@ -6,6 +6,7 @@ import Strata.MetaVerifier import Strata.Languages.Boole.Verify +-- Test fixtures build Core expressions directly with synthesized provenance open Strata open Lambda @@ -39,11 +40,11 @@ spec { #end /-- info: -Obligation: assert_2_986 +Obligation: assert_2_1063 Property: assert Result: ✅ pass -Obligation: map_extensionality_seed_ensures_1_963 +Obligation: map_extensionality_seed_ensures_1_1040 Property: assert Result: ✅ pass-/ #guard_msgs in @@ -78,7 +79,7 @@ spec { private def mkExprApp (f : Core.Expression.Expr) (args : List Core.Expression.Expr) : Core.Expression.Expr := - Lambda.LExpr.mkApp () f args + Lambda.LExpr.mkApp (ExprSourceLoc.synthesized "test") f args private def loweredQuantifiedMapExtensionalityCapture? : Option Core.Expression.Expr := do let booleProg <- (Strata.Boole.getProgram quantifiedMapExtensionalityCaptureSeed).toOption @@ -95,10 +96,10 @@ private def loweredQuantifiedMapExtensionalityCapture? : Option Core.Expression. private def expectedQuantifiedMapExtensionalityCapture : Core.Expression.Expr := let mapIntInt := Core.mapTy .int .int - let lhs := mkExprApp Core.mapSelectOp [.bvar () 2, .bvar () 0] - let rhs := mkExprApp Core.mapSelectOp [.bvar () 1, .bvar () 0] - .quant () .all "" (some mapIntInt) (.bvar () 0) - (.quant () .all "" (some mapIntInt) (.bvar () 0) - (.quant () .all "" (some .int) lhs (.eq () lhs rhs))) + let lhs := mkExprApp Core.mapSelectOp [.bvar (ExprSourceLoc.synthesized "test") 2, .bvar (ExprSourceLoc.synthesized "test") 0] + let rhs := mkExprApp Core.mapSelectOp [.bvar (ExprSourceLoc.synthesized "test") 1, .bvar (ExprSourceLoc.synthesized "test") 0] + .quant (ExprSourceLoc.synthesized "test") .all "" (some mapIntInt) (.bvar (ExprSourceLoc.synthesized "test") 0) + (.quant (ExprSourceLoc.synthesized "test") .all "" (some mapIntInt) (.bvar (ExprSourceLoc.synthesized "test") 0) + (.quant (ExprSourceLoc.synthesized "test") .all "" (some .int) lhs (.eq (ExprSourceLoc.synthesized "test") lhs rhs))) -#guard loweredQuantifiedMapExtensionalityCapture? == some expectedQuantifiedMapExtensionalityCapture +#guard (loweredQuantifiedMapExtensionalityCapture?.map (·.eraseMetadata)) == some expectedQuantifiedMapExtensionalityCapture.eraseMetadata diff --git a/StrataTest/Languages/C_Simp/Examples/LoopElimTests.lean b/StrataTest/Languages/C_Simp/Examples/LoopElimTests.lean index 61cc0f3a28..94805ba020 100644 --- a/StrataTest/Languages/C_Simp/Examples/LoopElimTests.lean +++ b/StrataTest/Languages/C_Simp/Examples/LoopElimTests.lean @@ -81,6 +81,11 @@ C_Simp function with a nondet loop programmatically and pass it through `to_core` to test the nondet loop elimination path. -/ +open Strata in +open Strata.C_Simp in +private def csimpOpExpr (op : Core.CoreOp) : Expression.Expr := + .op () op.toString none + open Strata in open Strata.C_Simp in private def nondetLoopProgram : C_Simp.Program := @@ -92,11 +97,11 @@ private def nondetLoopProgram : C_Simp.Program := let zero : Expression.Expr := .intConst () 0 let one : Expression.Expr := .intConst () 1 let intTy : Lambda.LTy := .forAll [] (.tcons "int" []) - let iLeN : Expression.Expr := .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Le⟩)) iExpr) nExpr - let iAddOne : Expression.Expr := .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Add⟩)) iExpr) one + let iLeN : Expression.Expr := .app () (.app () (csimpOpExpr (.numeric ⟨.int, .Le⟩)) iExpr) nExpr + let iAddOne : Expression.Expr := .app () (.app () (csimpOpExpr (.numeric ⟨.int, .Add⟩)) iExpr) one { funcs := [{ name := ⟨"nondetLoop", ()⟩, - pre := .app () (.app () (Core.coreOpExpr (.numeric ⟨.int, .Ge⟩)) nExpr) zero, + pre := .app () (.app () (csimpOpExpr (.numeric ⟨.int, .Ge⟩)) nExpr) zero, post := .true (), ret_ty := .tcons "int" [], inputs := ListMap.ofList [(n, .tcons "int" [])], diff --git a/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean b/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean index d6ebf385b1..f091c4ab03 100644 --- a/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean +++ b/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean @@ -395,72 +395,9 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, #eval examplePgm.commands /-- -info: [LExpr.quant () QuantifierKind.all "m" (some Lambda.LMonoTy.tcons - "Map" - [Lambda.LMonoTy.ftvar "k", - Lambda.LMonoTy.ftvar - "v"]) (LExpr.bvar () 0) (LExpr.quant () QuantifierKind.all "kk" (some Lambda.LMonoTy.ftvar - "k") (LExpr.bvar () 0) (LExpr.quant () QuantifierKind.all "vv" (some Lambda.LMonoTy.ftvar - "v") (LExpr.bvar () 0) (LExpr.eq () (LExpr.app () (LExpr.app () (LExpr.op () { name := "select", - metadata := () } (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"]])) (LExpr.app () (LExpr.app () (LExpr.app () (LExpr.op () { name := "update", - metadata := () } (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.tcons - "arrow" - [Lambda.LMonoTy.ftvar "v", - Lambda.LMonoTy.tcons - "Map" - [Lambda.LMonoTy.ftvar "k", - Lambda.LMonoTy.ftvar - "v"]]]])) (LExpr.bvar () 2)) (LExpr.bvar () 1)) (LExpr.bvar () 0))) (LExpr.bvar () 1)) (LExpr.bvar () 0)))), - LExpr.quant () QuantifierKind.all "m" (some Lambda.LMonoTy.tcons - "Map" - [Lambda.LMonoTy.ftvar "k", - Lambda.LMonoTy.ftvar - "v"]) (LExpr.bvar () 0) (LExpr.quant () QuantifierKind.all "okk" (some Lambda.LMonoTy.ftvar - "k") (LExpr.bvar () 0) (LExpr.quant () QuantifierKind.all "kk" (some Lambda.LMonoTy.ftvar - "k") (LExpr.bvar () 0) (LExpr.quant () QuantifierKind.all "vv" (some Lambda.LMonoTy.ftvar - "v") (LExpr.bvar () 0) (LExpr.eq () (LExpr.app () (LExpr.app () (LExpr.op () { name := "select", - metadata := () } (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"]])) (LExpr.app () (LExpr.app () (LExpr.app () (LExpr.op () { name := "update", - metadata := () } (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.tcons - "arrow" - [Lambda.LMonoTy.ftvar "v", - Lambda.LMonoTy.tcons - "Map" - [Lambda.LMonoTy.ftvar "k", - Lambda.LMonoTy.ftvar - "v"]]]])) (LExpr.bvar () 3)) (LExpr.bvar () 1)) (LExpr.bvar () 0))) (LExpr.bvar () 2)) (LExpr.app () (LExpr.app () (LExpr.op () { name := "select", - metadata := () } (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"]])) (LExpr.bvar () 3)) (LExpr.bvar () 2))))))] +info: forall m : (Map k v) :: forall kk : (k) :: forall vv : (v) :: (m[kk:=vv])[kk] == vv, forall m : (Map k v) :: forall okk : (k) :: forall kk : (k) :: forall vv : (v) :: (m[kk:=vv])[okk] == m[okk] -/ #guard_msgs in -#eval - extractAxiomsWithFreeTypeVars examplePgm ["k", "v"] +#eval do + let exprs := extractAxiomsWithFreeTypeVars examplePgm ["k", "v"] + IO.println s!"{Core.formatExprs exprs}" diff --git a/StrataTest/Languages/Core/Examples/SubstFvarsCaptureTests.lean b/StrataTest/Languages/Core/Examples/SubstFvarsCaptureTests.lean index 03e9b3e795..2a1fe0f82c 100644 --- a/StrataTest/Languages/Core/Examples/SubstFvarsCaptureTests.lean +++ b/StrataTest/Languages/Core/Examples/SubstFvarsCaptureTests.lean @@ -5,6 +5,7 @@ -/ import Strata.Languages.Core.Verifier +-- Test fixtures build Core expressions directly with synthesized provenance /-! # Simultaneous substitution tests (Issue 653) @@ -84,13 +85,13 @@ namespace Core open Lambda private def precond : LExpr CoreLParams.mono := - .eq () (.fvar () ⟨"x", ()⟩ (some .int)) (.fvar () ⟨"y", ()⟩ (some .int)) + .eq (ExprSourceLoc.synthesized "test") (.fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some .int)) (.fvar (ExprSourceLoc.synthesized "test") ⟨"y", ()⟩ (some .int)) private def formals : List (Identifier Unit × LMonoTy) := [(⟨"x", ()⟩, .int), (⟨"y", ()⟩, .int)] private def actuals : List (LExpr CoreLParams.mono) := - [.fvar () ⟨"y", ()⟩ (some .int), .intConst () 0] + [.fvar (ExprSourceLoc.synthesized "test") ⟨"y", ()⟩ (some .int), .intConst (ExprSourceLoc.synthesized "test") 0] -- f(y,0): iterated [x↦y][y↦0] on `x==y` produces `0==0`. Correct: `y==0`. /-- info: y == 0 -/ @@ -101,12 +102,12 @@ private def actuals : List (LExpr CoreLParams.mono) := /-! ## substitutePrecondition: bvar capture under quantifier -/ private def precondBvar : LExpr CoreLParams.mono := - .quant () .all "z" (some .int) (.bvar () 0) - (.app () (.app () (.op () ⟨"Int.Gt", ()⟩ (some (.arrow .int (.arrow .int .bool)))) - (.fvar () ⟨"x", ()⟩ (some .int))) (.bvar () 0)) + .quant (ExprSourceLoc.synthesized "test") .all "z" (some .int) (.bvar (ExprSourceLoc.synthesized "test") 0) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") ⟨"Int.Gt", ()⟩ (some (.arrow .int (.arrow .int .bool)))) + (.fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some .int))) (.bvar (ExprSourceLoc.synthesized "test") 0)) private def formalsBvar : List (Identifier Unit × LMonoTy) := [(⟨"x", ()⟩, .int)] -private def actualsBvar : List (LExpr CoreLParams.mono) := [.bvar () 0] +private def actualsBvar : List (LExpr CoreLParams.mono) := [.bvar (ExprSourceLoc.synthesized "test") 0] -- bvar!1 refers to an outer binder not present in this subexpression -- (collectWFObligations wraps it in a quantifier). @@ -132,10 +133,10 @@ namespace Core.Statement open Lambda private def mkId (s : String) : Identifier Unit := ⟨s, ()⟩ -private def mkFv (s : String) : LExpr CoreLParams.mono := .fvar () (mkId s) (some .int) -private def mkInt (n : Int) : LExpr CoreLParams.mono := .intConst () n +private def mkFv (s : String) : LExpr CoreLParams.mono := .fvar (ExprSourceLoc.synthesized "test") (mkId s) (some .int) +private def mkInt (n : Int) : LExpr CoreLParams.mono := .intConst (ExprSourceLoc.synthesized "test") n private def mkAdd (a b : LExpr CoreLParams.mono) : LExpr CoreLParams.mono := - .app () (.app () (.op () (mkId "Int.Add") (some (.arrow .int (.arrow .int .int)))) a) b + .app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (mkId "Int.Add") (some (.arrow .int (.arrow .int .int)))) a) b private def testEnv : Env := let e := Env.init diff --git a/StrataTest/Languages/Core/Tests/ExprEvalTest.lean b/StrataTest/Languages/Core/Tests/ExprEvalTest.lean index 7bdd7092c0..a1dd034c89 100644 --- a/StrataTest/Languages/Core/Tests/ExprEvalTest.lean +++ b/StrataTest/Languages/Core/Tests/ExprEvalTest.lean @@ -18,6 +18,7 @@ import Strata.Languages.Core.SMTEncoder import Strata.Languages.Core.Verifier import StrataTest.DL.Lambda.TestGen import StrataTest.DL.Lambda.PlausibleHelpers +-- Test fixtures build Core expressions directly with synthesized provenance import Plausible.Gen /-! This file does random testing of Strata Core operations registered in factory, by @@ -112,27 +113,27 @@ private def mkRandConst (ty:LMonoTy): IO (Option (LExpr CoreLParams.mono)) match ty with | .tcons "int" [] => let i <- pickInterestingValue 1 [0,1,-1] (pickRandInt 2147483648) - return (.some (.intConst () i)) + return (.some (.intConst (ExprSourceLoc.synthesized "test") i)) | .tcons "bool" [] => let rand_flag <- IO.rand 0 1 let rand_flag := rand_flag == 0 - return (.some (.boolConst () rand_flag)) + return (.some (.boolConst (ExprSourceLoc.synthesized "test") rand_flag)) | .tcons "real" [] => let i <- pickInterestingValue 1 [0,1,-1] (pickRandInt 2147483648) let n <- IO.rand 1 2147483648 - return (.some (.realConst () (mkRat i n))) + return (.some (.realConst (ExprSourceLoc.synthesized "test") (mkRat i n))) | .tcons "string" [] => -- TODO: random string generator - return (.some (.strConst () "a")) + return (.some (.strConst (ExprSourceLoc.synthesized "test") "a")) | .tcons "regex" [] => -- TODO: random regex generator - return (.some (.app () - (.op () (⟨"Str.ToRegEx", ()⟩) .none) (.strConst () ".*"))) + return (.some (.app (ExprSourceLoc.synthesized "test") + (.op (ExprSourceLoc.synthesized "test") (⟨"Str.ToRegEx", ()⟩) .none) (.strConst (ExprSourceLoc.synthesized "test") ".*"))) | .bitvec n => let specialvals := [0, 1, -1, Int.ofNat n, (Int.pow 2 (n-1)) - 1, -(Int.pow 2 (n-1))] let i <- pickInterestingValue 3 specialvals (IO.rand 0 ((Nat.pow 2 n) - 1)) - return (.some (.bitvecConst () n (BitVec.ofInt n i))) + return (.some (.bitvecConst (ExprSourceLoc.synthesized "test") n (BitVec.ofInt n i))) | _ => return .none @@ -164,8 +165,8 @@ def checkFactoryOps (verbose:Bool): IO Unit := do break else let args := List.map (Option.get!) args - let expr := List.foldl (fun e arg => (.app () e arg)) - (LExpr.op () (⟨e.name.name, ()⟩) .none) args + let expr := List.foldl (fun e arg => (.app (ExprSourceLoc.synthesized "test") e arg)) + (LExpr.op (ExprSourceLoc.synthesized "test") (⟨e.name.name, ()⟩) .none) args let res <- checkValid expr if ¬ res then if cnt_skipped = 0 then @@ -191,7 +192,7 @@ open Lambda.LTy.Syntax #guard_msgs in #eval (checkValid eb[if #1 == #2 then #false else #true]) /-- info: true -/ #guard_msgs in #eval (checkValid - (.app () (.app () (.op () (⟨"Int.Add", ()⟩) .none) eb[#100]) eb[#50])) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"Int.Add", ()⟩) .none) eb[#100]) eb[#50])) -- This may take a while diff --git a/StrataTest/Languages/Core/Tests/FunctionTests.lean b/StrataTest/Languages/Core/Tests/FunctionTests.lean index 11a51e21f8..1cf702a368 100644 --- a/StrataTest/Languages/Core/Tests/FunctionTests.lean +++ b/StrataTest/Languages/Core/Tests/FunctionTests.lean @@ -5,6 +5,7 @@ -/ import Strata.Languages.Core.Function +-- Test fixtures build Core expressions directly with synthesized provenance /-! ## Tests for Core Function -/ @@ -20,7 +21,7 @@ open LTy.Syntax LExpr.SyntaxMono typeArgs := ["a", "b"], inputs := [(⟨"w", ()⟩, mty[int]), (⟨"x", ()⟩, mty[%a]), (⟨"y", ()⟩, mty[%b]), (⟨"z", ()⟩, mty[%a])], output := mty[%a], - body := some (LExpr.fvar () (⟨"x", ()⟩) none) } : Function) + body := some (LExpr.fvar (ExprSourceLoc.synthesized "test") (⟨"x", ()⟩) none) } : Function) return format type end Core diff --git a/StrataTest/Languages/Core/Tests/GenericCallFallbackTest.lean b/StrataTest/Languages/Core/Tests/GenericCallFallbackTest.lean index c3491396f7..383212cd21 100644 --- a/StrataTest/Languages/Core/Tests/GenericCallFallbackTest.lean +++ b/StrataTest/Languages/Core/Tests/GenericCallFallbackTest.lean @@ -5,6 +5,7 @@ -/ import Strata.Languages.Core.DDMTransform.ASTtoCST +-- Test fixtures build Core expressions directly with synthesized provenance /-! Tests for the generic call fallback in ASTtoCST. @@ -23,16 +24,16 @@ namespace Strata.Test.GenericCallFallback open Strata Core Lambda private def mkOp (name : String) : Core.Expression.Expr := - LExpr.op () ⟨name, ()⟩ none + LExpr.op (ExprSourceLoc.synthesized "test") ⟨name, ()⟩ none private def mkFvar (name : String) : Core.Expression.Expr := - LExpr.fvar () ⟨name, ()⟩ none + LExpr.fvar (ExprSourceLoc.synthesized "test") ⟨name, ()⟩ none private def mkApp (fn arg : Core.Expression.Expr) : Core.Expression.Expr := - LExpr.app () fn arg + LExpr.app (ExprSourceLoc.synthesized "test") fn arg private def mkStrConst (s : String) : Core.Expression.Expr := - LExpr.const () (.strConst s) + LExpr.const (ExprSourceLoc.synthesized "test") (.strConst s) private def mkCall1 (opName : String) (a : Core.Expression.Expr) : Core.Expression.Expr := mkApp (mkOp opName) a diff --git a/StrataTest/Languages/Core/Tests/OverflowCheckTest.lean b/StrataTest/Languages/Core/Tests/OverflowCheckTest.lean index 8beb89023d..01cb748e3a 100644 --- a/StrataTest/Languages/Core/Tests/OverflowCheckTest.lean +++ b/StrataTest/Languages/Core/Tests/OverflowCheckTest.lean @@ -7,6 +7,7 @@ import Strata.Languages.Core.Factory import Strata.DL.Lambda.Preconditions import Strata.Transform.PrecondElim +-- Test fixtures build Core expressions directly with synthesized provenance /-! # Tests: overflow safe operators @@ -32,26 +33,26 @@ example := Core.bv32SNegOverflowOp -- Verify WF obligations are generated for safe add (1 precondition) #guard (collectWFObligations Core.Factory - (LExpr.mkApp () Core.bv32SafeAddOp [ - .fvar () ⟨"x", ()⟩ (some (.bitvec 32)), - .fvar () ⟨"y", ()⟩ (some (.bitvec 32))])).length == 1 + (LExpr.mkApp (ExprSourceLoc.synthesized "test") Core.bv32SafeAddOp [ + .fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some (.bitvec 32)), + .fvar (ExprSourceLoc.synthesized "test") ⟨"y", ()⟩ (some (.bitvec 32))])).length == 1 -- Verify WF obligations are generated for safe neg (1 precondition) #guard (collectWFObligations Core.Factory - (.app () Core.bv8SafeNegOp - (.fvar () ⟨"x", ()⟩ (some (.bitvec 8))))).length == 1 + (.app (ExprSourceLoc.synthesized "test") Core.bv8SafeNegOp + (.fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some (.bitvec 8))))).length == 1 -- Verify no WF obligations for unsafe add (no precondition) #guard (collectWFObligations Core.Factory - (LExpr.mkApp () Core.bv32AddOp [ - .fvar () ⟨"x", ()⟩ (some (.bitvec 32)), - .fvar () ⟨"y", ()⟩ (some (.bitvec 32))])).length == 0 + (LExpr.mkApp (ExprSourceLoc.synthesized "test") Core.bv32AddOp [ + .fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some (.bitvec 32)), + .fvar (ExprSourceLoc.synthesized "test") ⟨"y", ()⟩ (some (.bitvec 32))])).length == 0 -- Verify SafeSDiv has 2 preconditions (div-by-zero + overflow) #guard (collectWFObligations Core.Factory - (LExpr.mkApp () Core.bv32SafeSDivOp [ - .fvar () ⟨"x", ()⟩ (some (.bitvec 32)), - .fvar () ⟨"y", ()⟩ (some (.bitvec 32))])).length == 2 + (LExpr.mkApp (ExprSourceLoc.synthesized "test") Core.bv32SafeSDivOp [ + .fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some (.bitvec 32)), + .fvar (ExprSourceLoc.synthesized "test") ⟨"y", ()⟩ (some (.bitvec 32))])).length == 2 -- Verify SDivOverflow predicate and SafeSDiv/SafeSMod exist example := Core.bv32SDivOverflowOp @@ -60,9 +61,9 @@ example := Core.bv32SafeSModOp -- Verify SafeUAdd has 1 precondition (unsigned overflow) #guard (collectWFObligations Core.Factory - (LExpr.mkApp () Core.bv8SafeUAddOp [ - .fvar () ⟨"x", ()⟩ (some (.bitvec 8)), - .fvar () ⟨"y", ()⟩ (some (.bitvec 8))])).length == 1 + (LExpr.mkApp (ExprSourceLoc.synthesized "test") Core.bv8SafeUAddOp [ + .fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some (.bitvec 8)), + .fvar (ExprSourceLoc.synthesized "test") ⟨"y", ()⟩ (some (.bitvec 8))])).length == 1 -- Verify unsigned overflow predicates and safe ops exist example := Core.bv32UAddOverflowOp @@ -77,9 +78,9 @@ example := Core.bv32SafeUNegOp -- Verify SafeSDiv precondition classification: precond 0 = divisionByZero, precond 1 = arithmeticOverflow open Strata Core Lambda Core.PrecondElim Imperative in #eval do - let expr := LExpr.mkApp () Core.bv32SafeSDivOp [ - .fvar () ⟨"x", ()⟩ (some (.bitvec 32)), - .fvar () ⟨"y", ()⟩ (some (.bitvec 32))] + let expr := LExpr.mkApp (ExprSourceLoc.synthesized "test") Core.bv32SafeSDivOp [ + .fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some (.bitvec 32)), + .fvar (ExprSourceLoc.synthesized "test") ⟨"y", ()⟩ (some (.bitvec 32))] let stmts := collectPrecondAsserts Core.Factory expr "test" #[] assert! stmts.length == 2 -- First should be divisionByZero @@ -92,12 +93,12 @@ open Strata Core Lambda Core.PrecondElim Imperative in -- Verify nested SafeSDiv: both inner and outer calls get correct classification open Strata Core Lambda Core.PrecondElim Imperative in #eval do - let innerDiv := LExpr.mkApp () Core.bv32SafeSDivOp [ - .fvar () ⟨"x", ()⟩ (some (.bitvec 32)), - .fvar () ⟨"y", ()⟩ (some (.bitvec 32))] - let outerDiv := LExpr.mkApp () Core.bv32SafeSDivOp [ + let innerDiv := LExpr.mkApp (ExprSourceLoc.synthesized "test") Core.bv32SafeSDivOp [ + .fvar (ExprSourceLoc.synthesized "test") ⟨"x", ()⟩ (some (.bitvec 32)), + .fvar (ExprSourceLoc.synthesized "test") ⟨"y", ()⟩ (some (.bitvec 32))] + let outerDiv := LExpr.mkApp (ExprSourceLoc.synthesized "test") Core.bv32SafeSDivOp [ innerDiv, - .fvar () ⟨"z", ()⟩ (some (.bitvec 32))] + .fvar (ExprSourceLoc.synthesized "test") ⟨"z", ()⟩ (some (.bitvec 32))] let stmts := collectPrecondAsserts Core.Factory outerDiv "test" #[] assert! stmts.length == 4 -- Inner call: precond 0 = divisionByZero, precond 1 = arithmeticOverflow diff --git a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean index a415360eeb..d556e8bca3 100644 --- a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean +++ b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean @@ -6,6 +6,7 @@ import Strata.Languages.Core.Verifier import Strata.Languages.Core.StatementEval +-- Test fixtures build Core expressions directly with synthesized provenance namespace Core @@ -480,7 +481,7 @@ procedure Test(x : int, out y : int) /-- info: y = (some 10) -/ #guard_msgs in -#eval runProc arithPgm "Test" [.intConst () 5] +#eval runProc arithPgm "Test" [.intConst (ExprSourceLoc.synthesized "test") 5] -- If-then-else private def itePgm : Strata.Program := @@ -498,11 +499,11 @@ procedure Test(x : int, out y : int) /-- info: y = (some 7) -/ #guard_msgs in -#eval runProc itePgm "Test" [.intConst () 7] +#eval runProc itePgm "Test" [.intConst (ExprSourceLoc.synthesized "test") 7] /-- info: y = (some 3) -/ #guard_msgs in -#eval runProc itePgm "Test" [.intConst () (-3)] +#eval runProc itePgm "Test" [.intConst (ExprSourceLoc.synthesized "test") (-3)] -- Procedure call private def callPgm : Strata.Program := @@ -520,7 +521,7 @@ procedure Test(x : int, out y : int) /-- info: y = (some 20) -/ #guard_msgs in -#eval runProc callPgm "Test" [.intConst () 10] +#eval runProc callPgm "Test" [.intConst (ExprSourceLoc.synthesized "test") 10] -- Chained procedure calls (DoubleTwice) private def chainedCallPgm : Strata.Program := @@ -539,7 +540,7 @@ procedure Test(x : int, out output : int) /-- info: output = (some 20) -/ #guard_msgs in -#eval runProc chainedCallPgm "Test" [.intConst () 5] +#eval runProc chainedCallPgm "Test" [.intConst (ExprSourceLoc.synthesized "test") 5] -- Loop (sum of 0..n-1) private def loopPgm : Strata.Program := @@ -560,7 +561,7 @@ procedure Test(n : int, out sum : int) /-- info: sum = (some 15) -/ #guard_msgs in -#eval runProc loopPgm "Test" [.intConst () 5] +#eval runProc loopPgm "Test" [.intConst (ExprSourceLoc.synthesized "test") 5] -- Assertion success private def assertSuccessPgm : Strata.Program := diff --git a/StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean b/StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean index 0f1d023365..313232c4ab 100644 --- a/StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean +++ b/StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean @@ -17,6 +17,7 @@ import Strata.Languages.Core.Identifiers import Strata.Languages.Core.Options import Strata.Languages.Core.SMTEncoder import Strata.Languages.Core.Verifier +-- Test fixtures build Core expressions directly with synthesized provenance /-! This file contains unit tests for SMT datatype encoding. @@ -117,7 +118,7 @@ info: (declare-datatype TestOption (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"x", ()⟩) (.some (.tcons "TestOption" [.int]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"x", ()⟩) (.some (.tcons "TestOption" [.int]))) [optionDatatype] -- Test 2: Recursive datatype (List) - using List type @@ -130,7 +131,7 @@ info: (declare-datatype TestList (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"xs", ()⟩) (.some (.tcons "TestList" [.int]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"xs", ()⟩) (.some (.tcons "TestList" [.int]))) [listDatatype] -- Test 3: Multiple constructors - Tree with Leaf and Node @@ -143,7 +144,7 @@ info: (declare-datatype TestTree (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"tree", ()⟩) (.some (.tcons "TestTree" [.bool]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"tree", ()⟩) (.some (.tcons "TestTree" [.bool]))) [treeDatatype] -- Test 4: Parametric datatype instantiation - List Int @@ -156,7 +157,7 @@ info: (declare-datatype TestList (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"intList", ()⟩) (.some (.tcons "TestList" [.int]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"intList", ()⟩) (.some (.tcons "TestList" [.int]))) [listDatatype] -- Test 5: Parametric datatype instantiation - List Bool (should reuse same datatype) @@ -169,7 +170,7 @@ info: (declare-datatype TestList (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"boolList", ()⟩) (.some (.tcons "TestList" [.bool]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"boolList", ()⟩) (.some (.tcons "TestList" [.bool]))) [listDatatype] -- Test 6: Multi-field constructor - Tree with 3 fields @@ -182,7 +183,7 @@ info: (declare-datatype TestTree (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"intTree", ()⟩) (.some (.tcons "TestTree" [.int]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"intTree", ()⟩) (.some (.tcons "TestTree" [.int]))) [treeDatatype] -- Test 7: Nested parametric types - List of Option (should declare both datatypes) @@ -198,7 +199,7 @@ info: (declare-datatype TestOption (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"listOfOption", ()⟩) (.some (.tcons "TestList" [.tcons "TestOption" [.int]]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"listOfOption", ()⟩) (.some (.tcons "TestList" [.tcons "TestOption" [.int]]))) [optionDatatype, listDatatype] /-! ## Constructor Application Tests -/ @@ -211,7 +212,7 @@ info: (declare-datatype TestOption (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.op () (⟨"None", ()⟩) (.some (.tcons "TestOption" [.int]))) + (.op (ExprSourceLoc.synthesized "test") (⟨"None", ()⟩) (.some (.tcons "TestOption" [.int]))) [optionDatatype] -- Test 9: Some constructor (single-argument) @@ -222,7 +223,7 @@ info: (declare-datatype TestOption (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () (.op () (⟨"Some", ()⟩) (.some (.arrow .int (.tcons "TestOption" [.int])))) (.intConst () 42)) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"Some", ()⟩) (.some (.arrow .int (.tcons "TestOption" [.int])))) (.intConst (ExprSourceLoc.synthesized "test") 42)) [optionDatatype] -- Test 10: Cons constructor (multi-argument) @@ -233,10 +234,10 @@ info: (declare-datatype TestList (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () - (.app () (.op () (⟨"Cons", ()⟩) (.some (.arrow .int (.arrow (.tcons "TestList" [.int]) (.tcons "TestList" [.int]))))) - (.intConst () 1)) - (.op () (⟨"Nil", ()⟩) (.some (.tcons "TestList" [.int])))) + (.app (ExprSourceLoc.synthesized "test") + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"Cons", ()⟩) (.some (.arrow .int (.arrow (.tcons "TestList" [.int]) (.tcons "TestList" [.int]))))) + (.intConst (ExprSourceLoc.synthesized "test") 1)) + (.op (ExprSourceLoc.synthesized "test") (⟨"Nil", ()⟩) (.some (.tcons "TestList" [.int])))) [listDatatype] /-! ## Tester Function Tests -/ @@ -251,8 +252,8 @@ info: (declare-datatype TestOption (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () (.op () (⟨"TestOption..isNone", ()⟩) (.some (.arrow (.tcons "TestOption" [.int]) .bool))) - (.fvar () (⟨"x", ()⟩) (.some (.tcons "TestOption" [.int])))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"TestOption..isNone", ()⟩) (.some (.arrow (.tcons "TestOption" [.int]) .bool))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"x", ()⟩) (.some (.tcons "TestOption" [.int])))) [optionDatatype] -- Test 12: isCons tester @@ -265,8 +266,8 @@ info: (declare-datatype TestList (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () (.op () (⟨"TestList..isCons", ()⟩) (.some (.arrow (.tcons "TestList" [.int]) .bool))) - (.fvar () (⟨"xs", ()⟩) (.some (.tcons "TestList" [.int])))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"TestList..isCons", ()⟩) (.some (.arrow (.tcons "TestList" [.int]) .bool))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"xs", ()⟩) (.some (.tcons "TestList" [.int])))) [listDatatype] /-! ## Destructor Function Tests -/ @@ -281,8 +282,8 @@ info: (declare-datatype TestOption (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () (.op () (⟨"TestOption..val", ()⟩) (.some (.arrow (.tcons "TestOption" [.int]) .int))) - (.fvar () (⟨"x", ()⟩) (.some (.tcons "TestOption" [.int])))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"TestOption..val", ()⟩) (.some (.arrow (.tcons "TestOption" [.int]) .int))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"x", ()⟩) (.some (.tcons "TestOption" [.int])))) [optionDatatype] -- Test 14: Cons head destructor @@ -295,8 +296,8 @@ info: (declare-datatype TestList (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () (.op () (⟨"TestList..head", ()⟩) (.some (.arrow (.tcons "TestList" [.int]) .int))) - (.fvar () (⟨"xs", ()⟩) (.some (.tcons "TestList" [.int])))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"TestList..head", ()⟩) (.some (.arrow (.tcons "TestList" [.int]) .int))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"xs", ()⟩) (.some (.tcons "TestList" [.int])))) [listDatatype] -- Test 15: Cons tail destructor @@ -309,8 +310,8 @@ info: (declare-datatype TestList (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () (.op () (⟨"TestList..tail", ()⟩) (.some (.arrow (.tcons "TestList" [.int]) (.tcons "TestList" [.int])))) - (.fvar () (⟨"xs", ()⟩) (.some (.tcons "TestList" [.int])))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"TestList..tail", ()⟩) (.some (.arrow (.tcons "TestList" [.int]) (.tcons "TestList" [.int])))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"xs", ()⟩) (.some (.tcons "TestList" [.int])))) [listDatatype] /-! ## Dependency Order Tests -/ @@ -373,7 +374,7 @@ info: (declare-datatype Root ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"diamondVar", ()⟩) (.some (.tcons "Diamond" []))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"diamondVar", ()⟩) (.some (.tcons "Diamond" []))) [rootDatatype, rightDatatype, leftDatatype, diamondDatatype] -- Test 17: Mutually recursive datatypes (RoseTree/Forest) @@ -413,7 +414,7 @@ info: (declare-datatypes ((RoseTree 1) (Forest 1)) -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypeBlocks - (.fvar () (⟨"tree", ()⟩) (.some (.tcons "RoseTree" [.int]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"tree", ()⟩) (.some (.tcons "RoseTree" [.int]))) [[roseTreeDatatype, forestDatatype]] -- Test 19: Mix of mutual and non-mutual datatypes @@ -430,7 +431,7 @@ info: (declare-datatype TestOption (par (α) ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypeBlocks - (.fvar () (⟨"optionTree", ()⟩) (.some (.tcons "TestOption" [.tcons "RoseTree" [.int]]))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"optionTree", ()⟩) (.some (.tcons "TestOption" [.tcons "RoseTree" [.int]]))) [[optionDatatype], [roseTreeDatatype, forestDatatype]] /-! ## Recursive Function Axiom Tests -/ @@ -448,12 +449,12 @@ def intListDatatype : LDatatype Unit := private def intListTy := LMonoTy.tcons "IntList" [] private def listLenBody : LExpr CoreLParams.mono := - let xs := LExpr.fvar () ⟨"xs", ()⟩ (.some intListTy) - let isNil_xs := LExpr.app () (LExpr.op () ⟨"isNil", ()⟩ (.some (LMonoTy.arrow intListTy .bool))) xs - let tl_xs := LExpr.app () (LExpr.op () ⟨"IntList..tl", ()⟩ (.some (LMonoTy.arrow intListTy intListTy))) xs - let listLen_tl := LExpr.app () (LExpr.op () ⟨"listLen", ()⟩ (.some (LMonoTy.arrow intListTy .int))) tl_xs - let one_plus := LExpr.app () (LExpr.app () (LExpr.op () ⟨"Int.Add", ()⟩ (.some (LMonoTy.arrow .int (LMonoTy.arrow .int .int)))) (LExpr.intConst () 1)) listLen_tl - LExpr.ite () isNil_xs (LExpr.intConst () 0) one_plus + let xs := LExpr.fvar (ExprSourceLoc.synthesized "test") ⟨"xs", ()⟩ (.some intListTy) + let isNil_xs := LExpr.app (ExprSourceLoc.synthesized "test") (LExpr.op (ExprSourceLoc.synthesized "test") ⟨"isNil", ()⟩ (.some (LMonoTy.arrow intListTy .bool))) xs + let tl_xs := LExpr.app (ExprSourceLoc.synthesized "test") (LExpr.op (ExprSourceLoc.synthesized "test") ⟨"IntList..tl", ()⟩ (.some (LMonoTy.arrow intListTy intListTy))) xs + let listLen_tl := LExpr.app (ExprSourceLoc.synthesized "test") (LExpr.op (ExprSourceLoc.synthesized "test") ⟨"listLen", ()⟩ (.some (LMonoTy.arrow intListTy .int))) tl_xs + let one_plus := LExpr.app (ExprSourceLoc.synthesized "test") (LExpr.app (ExprSourceLoc.synthesized "test") (LExpr.op (ExprSourceLoc.synthesized "test") ⟨"Int.Add", ()⟩ (.some (LMonoTy.arrow .int (LMonoTy.arrow .int .int)))) (LExpr.intConst (ExprSourceLoc.synthesized "test") 1)) listLen_tl + LExpr.ite (ExprSourceLoc.synthesized "test") isNil_xs (LExpr.intConst (ExprSourceLoc.synthesized "test") 0) one_plus private def listLenFunc : Lambda.LFunc CoreLParams := { name := "listLen", @@ -506,8 +507,8 @@ info: (declare-datatype IntList ( -/ #guard_msgs in #eval format <$> toSMTStringWithRecFunc - (.app () (.op () "listLen" (.some (LMonoTy.arrow intListTy .int))) - (.op () "Nil" (.some intListTy))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") "listLen" (.some (LMonoTy.arrow intListTy .int))) + (.op (ExprSourceLoc.synthesized "test") "Nil" (.some intListTy))) [[intListDatatype]] listLenFunc @@ -531,7 +532,7 @@ info: (declare-datatype Container ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"c", ()⟩) (.some (.tcons "Container" []))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"c", ()⟩) (.some (.tcons "Container" []))) [containerWithMapDatatype] true -- Test: Same datatype without useArrayTheory should keep Map @@ -543,7 +544,7 @@ info: (declare-datatype Container ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.fvar () (⟨"c", ()⟩) (.some (.tcons "Container" []))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"c", ()⟩) (.some (.tcons "Container" []))) [containerWithMapDatatype] -- Test: ADT testers with Map type should emit Array when useArrayTheory=true @@ -555,8 +556,8 @@ info: (declare-datatype Container ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () (.op () (⟨"Container..isMkContainer", ()⟩) (.some (.arrow (.tcons "Container" []) .bool))) - (.fvar () (⟨"xs", ()⟩) (.some (.tcons "Container" [])))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"Container..isMkContainer", ()⟩) (.some (.arrow (.tcons "Container" []) .bool))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"xs", ()⟩) (.some (.tcons "Container" [])))) [containerWithMapDatatype] true -- Test: ADT destructors with Map type should emit Array when useArrayTheory=true @@ -568,8 +569,8 @@ info: (declare-datatype Container ( -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes - (.app () (.op () (⟨"Container..data", ()⟩) (.some (.arrow (.tcons "Container" []) (.tcons "Map" [.int, .int])))) - (.fvar () (⟨"xs", ()⟩) (.some (.tcons "Container" [])))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"Container..data", ()⟩) (.some (.arrow (.tcons "Container" []) (.tcons "Map" [.int, .int])))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"xs", ()⟩) (.some (.tcons "Container" [])))) [containerWithMapDatatype] true diff --git a/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean b/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean index 5ce57a9ecc..5672dbe18d 100644 --- a/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean +++ b/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean @@ -6,6 +6,7 @@ import Strata.Languages.Core.SMTEncoder import Strata.Languages.Core.Verifier +-- Test fixtures build Core expressions directly with synthesized provenance /-! ## Tests for SMTEncoder -/ @@ -18,25 +19,25 @@ info: "(assert (forall ((n Int)) (exists ((m Int)) (= n m))))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .all "n" (.some .int) (LExpr.noTrigger ()) - (.quant () .exist "m" (.some .int) (LExpr.noTrigger ()) - (.eq () (.bvar () 1) (.bvar () 0)))) + (.quant (ExprSourceLoc.synthesized "test") .all "n" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.quant (ExprSourceLoc.synthesized "test") .exist "m" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.eq (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 1) (.bvar (ExprSourceLoc.synthesized "test") 0)))) /-- info: "; x\n(declare-const x Int)\n(assert (exists ((i Int)) (= i x)))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .exist "i" (.some .int) (LExpr.noTrigger ()) - (.eq () (.bvar () 0) (.fvar () "x" (.some .int)))) + (.quant (ExprSourceLoc.synthesized "test") .exist "i" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.eq (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 0) (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .int)))) /-- info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(assert (exists ((i Int)) (! (= i x) :pattern ((f i)))))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .exist "i" (.some .int) (.app () (.fvar () "f" (.some (.arrow .int .int))) (.bvar () 0)) - (.eq () (.bvar () 0) (.fvar () "x" (.some .int)))) + (.quant (ExprSourceLoc.synthesized "test") .exist "i" (.some .int) (.app (ExprSourceLoc.synthesized "test") (.fvar (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int .int))) (.bvar (ExprSourceLoc.synthesized "test") 0)) + (.eq (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 0) (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .int)))) /-- @@ -44,23 +45,23 @@ info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(assert (exis -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .exist "i" (.some .int) (.app () (.fvar () "f" (.some (.arrow .int .int))) (.bvar () 0)) - (.eq () (.app () (.fvar () "f" (.some (.arrow .int .int))) (.bvar () 0)) (.fvar () "x" (.some .int)))) + (.quant (ExprSourceLoc.synthesized "test") .exist "i" (.some .int) (.app (ExprSourceLoc.synthesized "test") (.fvar (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int .int))) (.bvar (ExprSourceLoc.synthesized "test") 0)) + (.eq (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.fvar (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int .int))) (.bvar (ExprSourceLoc.synthesized "test") 0)) (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .int)))) /-- info: "Cannot encode expression f(bvar!0)\n-- Errors: Unsupported construct in lexprToExpr: bvar index out of bounds: 0\nContext: Global scope:\n freeVars: [f]" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .exist "i" (.some .int) (.app () (.fvar () "f" (.none)) (.bvar () 0)) - (.eq () (.app () (.fvar () "f" (.some (.arrow .int .int))) (.bvar () 0)) (.fvar () "x" (.some .int)))) + (.quant (ExprSourceLoc.synthesized "test") .exist "i" (.some .int) (.app (ExprSourceLoc.synthesized "test") (.fvar (ExprSourceLoc.synthesized "test") "f" (.none)) (.bvar (ExprSourceLoc.synthesized "test") 0)) + (.eq (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.fvar (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int .int))) (.bvar (ExprSourceLoc.synthesized "test") 0)) (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .int)))) /-- info: "; f\n(declare-const f (arrow Int Int))\n; f\n(declare-fun f@1 (Int) Int)\n; x\n(declare-const x Int)\n(assert (exists ((i Int)) (! (= (f@1 i) x) :pattern (f))))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .exist "i" (.some .int) - (mkTriggerExpr [[.fvar () "f" (.some (.arrow .int .int))]]) - (.eq () (.app () (.fvar () "f" (.some (.arrow .int .int))) (.bvar () 0)) (.fvar () "x" (.some .int)))) + (.quant (ExprSourceLoc.synthesized "test") .exist "i" (.some .int) + (mkTriggerExpr [[.fvar (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int .int))]]) + (.eq (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.fvar (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int .int))) (.bvar (ExprSourceLoc.synthesized "test") 0)) (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .int)))) (ctx := SMT.Context.default) (E := {Env.init with exprEnv := { Env.init.exprEnv with @@ -74,8 +75,8 @@ info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(assert ( -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .all "m" (.some .int) (.bvar () 0) (.quant () .all "n" (.some .int) (.app () (.app () (.op () "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar () 0)) (.bvar () 1)) - (.eq () (.app () (.app () (.op () "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar () 0)) (.bvar () 1)) (.fvar () "x" (.some .int))))) + (.quant (ExprSourceLoc.synthesized "test") .all "m" (.some .int) (.bvar (ExprSourceLoc.synthesized "test") 0) (.quant (ExprSourceLoc.synthesized "test") .all "n" (.some .int) (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar (ExprSourceLoc.synthesized "test") 0)) (.bvar (ExprSourceLoc.synthesized "test") 1)) + (.eq (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar (ExprSourceLoc.synthesized "test") 0)) (.bvar (ExprSourceLoc.synthesized "test") 1)) (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .int))))) (ctx := SMT.Context.mk #[] #[UF.mk "f" ((TermVar.mk "m" TermType.int) ::(TermVar.mk "n" TermType.int) :: []) TermType.int] #[] #[] [] #[] {} [] 0 false) (E := {Env.init with exprEnv := { Env.init.exprEnv with @@ -92,8 +93,8 @@ info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(assert ( -/ #guard_msgs in -- No valid trigger #eval toSMTCommandsWithAssert - (.quant () .all "m" (.some .int) (.bvar () 0) (.quant () .all "n" (.some .int) (.bvar () 0) - (.eq () (.app () (.app () (.op () "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar () 0)) (.bvar () 1)) (.fvar () "x" (.some .int))))) + (.quant (ExprSourceLoc.synthesized "test") .all "m" (.some .int) (.bvar (ExprSourceLoc.synthesized "test") 0) (.quant (ExprSourceLoc.synthesized "test") .all "n" (.some .int) (.bvar (ExprSourceLoc.synthesized "test") 0) + (.eq (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar (ExprSourceLoc.synthesized "test") 0)) (.bvar (ExprSourceLoc.synthesized "test") 1)) (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .int))))) (ctx := SMT.Context.mk #[] #[UF.mk "f" ((TermVar.mk "m" TermType.int) ::(TermVar.mk "n" TermType.int) :: []) TermType.int] #[] #[] [] #[] {} [] 0 false) (E := {Env.init with exprEnv := { Env.init.exprEnv with @@ -114,9 +115,9 @@ info: "; m\n(declare-const m (Array Int Int))\n; i\n(declare-const i Int)\n(asse -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.app () (.app () (.op () "select" (.some (.arrow (mapTy .int .int) (.arrow .int .int)))) - (.fvar () "m" (.some (mapTy .int .int)))) - (.fvar () "i" (.some .int))) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") "select" (.some (.arrow (mapTy .int .int) (.arrow .int .int)))) + (.fvar (ExprSourceLoc.synthesized "test") "m" (.some (mapTy .int .int)))) + (.fvar (ExprSourceLoc.synthesized "test") "i" (.some .int))) (useArrayTheory := true) (E := {Env.init with exprEnv := { Env.init.exprEnv with @@ -131,10 +132,10 @@ info: "; m\n(declare-const m (Array Int Int))\n; i\n(declare-const i Int)\n; v\n -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.app () (.app () (.app () (.op () "update" (.some (.arrow (mapTy .int .int) (.arrow .int (.arrow .int (mapTy .int .int)))))) - (.fvar () "m" (.some (mapTy .int .int)))) - (.fvar () "i" (.some .int))) - (.fvar () "v" (.some .int))) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") "update" (.some (.arrow (mapTy .int .int) (.arrow .int (.arrow .int (mapTy .int .int)))))) + (.fvar (ExprSourceLoc.synthesized "test") "m" (.some (mapTy .int .int)))) + (.fvar (ExprSourceLoc.synthesized "test") "i" (.some .int))) + (.fvar (ExprSourceLoc.synthesized "test") "v" (.some .int))) (useArrayTheory := true) (E := {Env.init with exprEnv := { Env.init.exprEnv with @@ -149,12 +150,12 @@ info: "; m\n(declare-const m (Array Int Int))\n; i\n(declare-const i Int)\n; v\n -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.app () (.app () (.op () "select" (.some (.arrow (mapTy .int .int) (.arrow .int .int)))) - (.app () (.app () (.app () (.op () "update" (.some (.arrow (mapTy .int .int) (.arrow .int (.arrow .int (mapTy .int .int)))))) - (.fvar () "m" (.some (mapTy .int .int)))) - (.fvar () "i" (.some .int))) - (.fvar () "v" (.some .int)))) - (.fvar () "j" (.some .int))) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") "select" (.some (.arrow (mapTy .int .int) (.arrow .int .int)))) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") "update" (.some (.arrow (mapTy .int .int) (.arrow .int (.arrow .int (mapTy .int .int)))))) + (.fvar (ExprSourceLoc.synthesized "test") "m" (.some (mapTy .int .int)))) + (.fvar (ExprSourceLoc.synthesized "test") "i" (.some .int))) + (.fvar (ExprSourceLoc.synthesized "test") "v" (.some .int)))) + (.fvar (ExprSourceLoc.synthesized "test") "j" (.some .int))) (useArrayTheory := true) (E := {Env.init with exprEnv := { Env.init.exprEnv with @@ -169,8 +170,8 @@ info: "; m\n(declare-const m (Array Int Int))\n; getFirst\n(declare-fun getFirst -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.app () (.op () (⟨"getFirst", ()⟩) (.some (.arrow (mapTy .int .int) .int))) - (.fvar () (⟨"m", ()⟩) (.some (mapTy .int .int)))) + (.app (ExprSourceLoc.synthesized "test") (.op (ExprSourceLoc.synthesized "test") (⟨"getFirst", ()⟩) (.some (.arrow (mapTy .int .int) .int))) + (.fvar (ExprSourceLoc.synthesized "test") (⟨"m", ()⟩) (.some (mapTy .int .int)))) (useArrayTheory := true) (E := {Env.init with exprEnv := { Env.init.exprEnv with @@ -186,9 +187,9 @@ info: "; m\n(declare-const m (Array Int Int))\n; getFirst\n(declare-fun getFirst /-- info: "(assert (forall (($__bv0 Int)) (exists (($__bv1 Int)) (= $__bv0 $__bv1))))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .all "" (.some .int) (LExpr.noTrigger ()) - (.quant () .exist "" (.some .int) (LExpr.noTrigger ()) - (.eq () (.bvar () 1) (.bvar () 0)))) + (.quant (ExprSourceLoc.synthesized "test") .all "" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.quant (ExprSourceLoc.synthesized "test") .exist "" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.eq (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 1) (.bvar (ExprSourceLoc.synthesized "test") 0)))) -- Test nested quantifiers with same user name get disambiguated human-readable names /-- @@ -196,9 +197,9 @@ info: "(assert (forall ((x Int)) (exists ((x@1 Int)) (= x x@1))))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .all "x" (.some .int) (LExpr.noTrigger ()) - (.quant () .exist "x" (.some .int) (LExpr.noTrigger ()) - (.eq () (.bvar () 1) (.bvar () 0)))) + (.quant (ExprSourceLoc.synthesized "test") .all "x" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.quant (ExprSourceLoc.synthesized "test") .exist "x" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.eq (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 1) (.bvar (ExprSourceLoc.synthesized "test") 0)))) -- Test triply nested quantifiers all get distinct disambiguated human-readable names /-- @@ -206,10 +207,10 @@ info: "(assert (forall ((x Int) (x@1 Int) (x@2 Int)) (= x@2 x)))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .all "x" (.some .int) (LExpr.noTrigger ()) - (.quant () .all "x" (.some .int) (LExpr.noTrigger ()) - (.quant () .all "x@1" (.some .int) (LExpr.noTrigger ()) - (.eq () (.bvar () 0) (.bvar () 2))))) + (.quant (ExprSourceLoc.synthesized "test") .all "x" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.quant (ExprSourceLoc.synthesized "test") .all "x" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.quant (ExprSourceLoc.synthesized "test") .all "x@1" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.eq (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 0) (.bvar (ExprSourceLoc.synthesized "test") 2))))) /-- @@ -217,19 +218,19 @@ info: "; x\n(declare-const x Int)\n(assert (forall ((x@1 Int)) (= x@1 x)))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.quant () .all "x" (.some .int) (LExpr.noTrigger ()) - (.eq () (.bvar () 0) (.fvar () "x" (.some .int)))) + (.quant (ExprSourceLoc.synthesized "test") .all "x" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.eq (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 0) (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .int)))) -- Test that bound variable names are globally unique across multiple terms. -- Two independent forall terms with empty names encoded via toSMTTerms should get distinct $__bv names. #guard match toSMTTerms Env.init [ -- Term 1: ∀ x:Int. x = x - (.quant () .all "" (.some .int) (LExpr.noTrigger ()) - (.eq () (.bvar () 0) (.bvar () 0))), + (.quant (ExprSourceLoc.synthesized "test") .all "" (.some .int) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.eq (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 0) (.bvar (ExprSourceLoc.synthesized "test") 0))), -- Term 2: ∀ y:Bool. y - (.quant () .all "" (.some .bool) (LExpr.noTrigger ()) - (.bvar () 0)) + (.quant (ExprSourceLoc.synthesized "test") .all "" (.some .bool) (LExpr.noTrigger (ExprSourceLoc.synthesized "test")) + (.bvar (ExprSourceLoc.synthesized "test") 0)) ] SMT.Context.default with | .ok ([t1, t2], _) => match Strata.SMTDDM.termToString t1, Strata.SMTDDM.termToString t2 with @@ -246,7 +247,7 @@ info: "; x\n(declare-const x String)\n(assert (= x \"{\"\"key\"\":\"\"val\"\"}\" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.eq () (.fvar () "x" (.some .string)) (.strConst () "{\"key\":\"val\"}")) + (.eq (ExprSourceLoc.synthesized "test") (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .string)) (.strConst (ExprSourceLoc.synthesized "test") "{\"key\":\"val\"}")) -- Test that negative integer constants are lowered to (- N) form /-- info: Except.ok "(- 1)" -/ @@ -259,11 +260,11 @@ info: "; x\n(declare-const x Real)\n; y\n(declare-const y Real)\n(assert (|/| x -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.app () - (.app () - (.op () "Real.Div" (.some (.arrow .real (.arrow .real .real)))) - (.fvar () "x" (.some .real))) - (.fvar () "y" (.some .real))) + (.app (ExprSourceLoc.synthesized "test") + (.app (ExprSourceLoc.synthesized "test") + (.op (ExprSourceLoc.synthesized "test") "Real.Div" (.some (.arrow .real (.arrow .real .real)))) + (.fvar (ExprSourceLoc.synthesized "test") "x" (.some .real))) + (.fvar (ExprSourceLoc.synthesized "test") "y" (.some .real))) (E := {Env.init with exprEnv := { Env.init.exprEnv with config := { Env.init.exprEnv.config with @@ -469,16 +470,16 @@ info: "; s1\n(declare-const s1 String)\n; s2\n(declare-const s2 String)\n(assert -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.app () (.app () strPrefixOfOp (.fvar () "s1" (.some .string))) - (.fvar () "s2" (.some .string))) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") strPrefixOfOp (.fvar (ExprSourceLoc.synthesized "test") "s1" (.some .string))) + (.fvar (ExprSourceLoc.synthesized "test") "s2" (.some .string))) /-- info: "; s1\n(declare-const s1 String)\n; s2\n(declare-const s2 String)\n(assert (str.suffixof s1 s2))\n" -/ #guard_msgs in #eval toSMTCommandsWithAssert - (.app () (.app () strSuffixOfOp (.fvar () "s1" (.some .string))) - (.fvar () "s2" (.some .string))) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") strSuffixOfOp (.fvar (ExprSourceLoc.synthesized "test") "s1" (.some .string))) + (.fvar (ExprSourceLoc.synthesized "test") "s2" (.some .string))) end Core diff --git a/StrataTest/Languages/Core/Tests/SarifOutputTests.lean b/StrataTest/Languages/Core/Tests/SarifOutputTests.lean index ad488d023c..8f15c03128 100644 --- a/StrataTest/Languages/Core/Tests/SarifOutputTests.lean +++ b/StrataTest/Languages/Core/Tests/SarifOutputTests.lean @@ -7,6 +7,7 @@ import Strata.Languages.Core.SarifOutput import Strata.Languages.Core.Verifier import Lean.Data.Json +-- Test fixtures build Core expressions directly with synthesized provenance /-! # SARIF Output Tests @@ -60,7 +61,7 @@ def makeObligation (label : String) (md : MetaData Expression := #[]) { label := label property := property assumptions := [] - obligation := Lambda.LExpr.boolConst () true + obligation := Lambda.LExpr.boolConst (ExprSourceLoc.synthesized "test") true metadata := md } /-- Create a VCResult for testing -/ @@ -260,7 +261,7 @@ def makeVCResult (label : String) (outcome : VCOutcome) let cex : List (Core.Expression.Ident × Strata.SMT.Term) := [({ name := "x", metadata := () }, .prim (.int 42))] let lexprCex : LExprModel := - [({ name := "x", metadata := () }, .intConst () 42)] + [({ name := "x", metadata := () }, .intConst (ExprSourceLoc.synthesized "test") 42)] let md := makeMetadata "/test/cex.st" 25 3 let files := makeFilesMap "/test/cex.st" let vcr := makeVCResult "cex_obligation" (mkOutcome .unsat (.sat cex)) md lexprCex diff --git a/StrataTest/Languages/Core/Tests/TestASTtoCST.lean b/StrataTest/Languages/Core/Tests/TestASTtoCST.lean index 981a7fc688..b98348d8d7 100644 --- a/StrataTest/Languages/Core/Tests/TestASTtoCST.lean +++ b/StrataTest/Languages/Core/Tests/TestASTtoCST.lean @@ -6,6 +6,7 @@ import Strata.Languages.Core.DDMTransform.ASTtoCST import Strata.Languages.Core.DDMTransform.Translate +-- Test fixtures build Core expressions directly with synthesized provenance -- Tests for Core.Program → CST Conversion -- This file tests one-direction conversion: AST → CST using the old @@ -645,7 +646,7 @@ private def formatCore (p : Core.Program) : IO Unit := private def lambdaIdentityPgm : Core.Program := { decls := [ .func { name := "intID", typeArgs := [], inputs := [], output := .arrow .int .int, - body := some (.abs () "" (.some .int) (.bvar () 0)) } .empty + body := some (.abs (ExprSourceLoc.synthesized "test") "" (.some .int) (.bvar (ExprSourceLoc.synthesized "test") 0)) } .empty ]} /-- @@ -661,8 +662,8 @@ function intID () : int -> int { private def lambdaNestedPgm : Core.Program := { decls := [ .func { name := "constFn", typeArgs := [], inputs := [], output := .arrow .int (.arrow .int .int), - body := some (.abs () "" (.some .int) - (.abs () "" (.some .int) (.bvar () 1))) } .empty + body := some (.abs (ExprSourceLoc.synthesized "test") "" (.some .int) + (.abs (ExprSourceLoc.synthesized "test") "" (.some .int) (.bvar (ExprSourceLoc.synthesized "test") 1))) } .empty ]} /-- @@ -678,7 +679,7 @@ function constFn () : int -> int -> int { private def lambdaNamedPgm : Core.Program := { decls := [ .func { name := "namedLam", typeArgs := [], inputs := [], output := .arrow .int .int, - body := some (.abs () "x" (.some .int) (.bvar () 0)) } .empty + body := some (.abs (ExprSourceLoc.synthesized "test") "x" (.some .int) (.bvar (ExprSourceLoc.synthesized "test") 0)) } .empty ]} /-- @@ -695,7 +696,7 @@ function namedLam () : int -> int { private def lambdaAppliedPgm : Core.Program := { decls := [ .func { name := "test", typeArgs := [], inputs := [], output := .int, - body := some (.app () (.abs () "x" (.some .int) (.bvar () 0)) (.intConst () 5)) } .empty + body := some (.app (ExprSourceLoc.synthesized "test") (.abs (ExprSourceLoc.synthesized "test") "x" (.some .int) (.bvar (ExprSourceLoc.synthesized "test") 0)) (.intConst (ExprSourceLoc.synthesized "test") 5)) } .empty ]} /-- @@ -712,9 +713,9 @@ function test () : int { private def lambdaMultiBindPgm : Core.Program := { decls := [ .func { name := "add", typeArgs := [], inputs := [], output := .arrow .int (.arrow .int .int), - body := some (.abs () "x" (.some .int) - (.abs () "y" (.some .int) - (.app () (.app () Core.intAddOp (.bvar () 1)) (.bvar () 0)))) } .empty + body := some (.abs (ExprSourceLoc.synthesized "test") "x" (.some .int) + (.abs (ExprSourceLoc.synthesized "test") "y" (.some .int) + (.app (ExprSourceLoc.synthesized "test") (.app (ExprSourceLoc.synthesized "test") Core.intAddOp (.bvar (ExprSourceLoc.synthesized "test") 1)) (.bvar (ExprSourceLoc.synthesized "test") 0)))) } .empty ]} /-- @@ -731,9 +732,9 @@ function add () : int -> int -> int { private def lambdaHigherOrderPgm : Core.Program := { decls := [ .func { name := "applyFn", typeArgs := [], inputs := [], output := .arrow (.arrow .int .int) (.arrow .int .int), - body := some (.abs () "f" (.some (.arrow .int .int)) - (.abs () "x" (.some .int) - (.app () (.bvar () 1) (.bvar () 0)))) } .empty + body := some (.abs (ExprSourceLoc.synthesized "test") "f" (.some (.arrow .int .int)) + (.abs (ExprSourceLoc.synthesized "test") "x" (.some .int) + (.app (ExprSourceLoc.synthesized "test") (.bvar (ExprSourceLoc.synthesized "test") 1) (.bvar (ExprSourceLoc.synthesized "test") 0)))) } .empty ]} /-- info: program Core; diff --git a/StrataTest/Languages/Core/VCOutcomeTests.lean b/StrataTest/Languages/Core/VCOutcomeTests.lean index c4a2b5374c..64180149a6 100644 --- a/StrataTest/Languages/Core/VCOutcomeTests.lean +++ b/StrataTest/Languages/Core/VCOutcomeTests.lean @@ -205,7 +205,7 @@ private def unknownResult : Result := .unknown (some []) /-- A dummy obligation for testing phase validation. -/ private def dummyObligation : Imperative.ProofObligation Core.Expression := - { label := "test", property := .assert, assumptions := [], obligation := .true (), metadata := {} } + { label := "test", property := .assert, assumptions := [], obligation := Core.true, metadata := {} } /-- info: false -/ #guard_msgs in #eval needsValidation [preservingPhase] dummyObligation @@ -258,14 +258,14 @@ private def dummyObligation : Imperative.ProofObligation Core.Expression := /-- Obligation with call-elimination labels in path conditions. -/ private def callElimObligation : Imperative.ProofObligation Core.Expression := { label := "test_callElim", property := .assert, - assumptions := [[.assumption "callElimAssume_post" (.true ())]], - obligation := .true (), metadata := {} } + assumptions := [[.assumption "callElimAssume_post" Core.true]], + obligation := Core.true, metadata := {} } /-- Obligation with no abstraction labels — models are sound. -/ private def cleanObligation : Imperative.ProofObligation Core.Expression := { label := "test_clean", property := .assert, - assumptions := [[.assumption "precond_x_positive" (.true ())]], - obligation := .true (), metadata := {} } + assumptions := [[.assumption "precond_x_positive" Core.true]], + obligation := Core.true, metadata := {} } -- Combined Core phases: clean obligation preserves sat #guard (satResult.adjustForPhases [callElimPipelinePhase.phase, loopElimPipelinePhase.phase] cleanObligation).1 == satResult diff --git a/StrataTest/Languages/Python/expected_interpret/test_param_reassign_cross_module.expected b/StrataTest/Languages/Python/expected_interpret/test_param_reassign_cross_module.expected index e5bfdd2c78..e08d8d6b3a 100644 --- a/StrataTest/Languages/Python/expected_interpret/test_param_reassign_cross_module.expected +++ b/StrataTest/Languages/Python/expected_interpret/test_param_reassign_cross_module.expected @@ -1 +1 @@ -\[ERROR\] assert \(assert\(59\)\) condition did not reduce to bool +\[ERROR\] assert \(assert\([0-9]+\)\) condition did not reduce to bool diff --git a/StrataTest/Transform/CallElim.lean b/StrataTest/Transform/CallElim.lean index c950d3cf27..856f882028 100644 --- a/StrataTest/Transform/CallElim.lean +++ b/StrataTest/Transform/CallElim.lean @@ -222,14 +222,14 @@ private def unknownResult : Result := .unknown (some []) /-- Obligation with call-elimination labels in path conditions. -/ private def callElimObligation : Imperative.ProofObligation Core.Expression := { label := "test_callElim", property := .assert, - assumptions := [[.assumption "callElimAssume_post" (.true ())]], - obligation := .true (), metadata := {} } + assumptions := [[.assumption "callElimAssume_post" Core.true]], + obligation := Core.true, metadata := {} } /-- Obligation with no abstraction labels — models are sound. -/ private def cleanObligation : Imperative.ProofObligation Core.Expression := { label := "test_clean", property := .assert, - assumptions := [[.assumption "precond_x_positive" (.true ())]], - obligation := .true (), metadata := {} } + assumptions := [[.assumption "precond_x_positive" Core.true]], + obligation := Core.true, metadata := {} } -- callElimPipelinePhase: rejects sat when obligation has call-elim labels #guard (satResult.adjustForPhases [callElimPipelinePhase.phase] callElimObligation).1 == unknownResult diff --git a/StrataTest/Transform/LoopElim.lean b/StrataTest/Transform/LoopElim.lean index 7753452085..50b8132790 100644 --- a/StrataTest/Transform/LoopElim.lean +++ b/StrataTest/Transform/LoopElim.lean @@ -19,14 +19,14 @@ private def unknownResult : Result := .unknown (some []) /-- Obligation with loop-elimination labels in path conditions. -/ private def loopElimObligation : Imperative.ProofObligation Core.Expression := { label := "test_loopElim", property := .assert, - assumptions := [[.assumption "assume_invariant_0_0" (.true ()), .assumption "assume_guard_0" (.true ())]], - obligation := .true (), metadata := {} } + assumptions := [[.assumption "assume_invariant_0_0" Core.true, .assumption "assume_guard_0" Core.true]], + obligation := Core.true, metadata := {} } /-- Obligation with no abstraction labels — models are sound. -/ private def cleanObligation : Imperative.ProofObligation Core.Expression := { label := "test_clean", property := .assert, - assumptions := [[.assumption "precond_x_positive" (.true ())]], - obligation := .true (), metadata := {} } + assumptions := [[.assumption "precond_x_positive" Core.true]], + obligation := Core.true, metadata := {} } -- loopElimPipelinePhase: rejects sat when obligation has loop-elim labels #guard (satResult.adjustForPhases [loopElimPipelinePhase.phase] loopElimObligation).1 == unknownResult diff --git a/StrataTest/Transform/PrecondElim.lean b/StrataTest/Transform/PrecondElim.lean index 3242d25afa..38aefa0c6a 100644 --- a/StrataTest/Transform/PrecondElim.lean +++ b/StrataTest/Transform/PrecondElim.lean @@ -429,11 +429,11 @@ section SeqBoundsObligations open Strata Core Lambda Core.PrecondElim Imperative /-- Shared fvar fixtures so each per-op case below is a one-liner. -/ -private def fxS : Core.Expression.Expr := .fvar () ⟨"s", ()⟩ (some (Core.seqTy .int)) -private def fxI : Core.Expression.Expr := .fvar () ⟨"i", ()⟩ (some .int) -private def fxV : Core.Expression.Expr := .fvar () ⟨"v", ()⟩ (some .int) -private def fxN : Core.Expression.Expr := .fvar () ⟨"n", ()⟩ (some .int) -private def fxJ : Core.Expression.Expr := .fvar () ⟨"j", ()⟩ (some .int) +private def fxS : Core.Expression.Expr := .fvar default ⟨"s", ()⟩ (some (Core.seqTy .int)) +private def fxI : Core.Expression.Expr := .fvar default ⟨"i", ()⟩ (some .int) +private def fxV : Core.Expression.Expr := .fvar default ⟨"v", ()⟩ (some .int) +private def fxN : Core.Expression.Expr := .fvar default ⟨"n", ()⟩ (some .int) +private def fxJ : Core.Expression.Expr := .fvar default ⟨"j", ()⟩ (some .int) /-- Check that `collectPrecondAsserts` produces exactly `expectedCount` obligations from `expr`, each tagged with `outOfBoundsAccess`. -/ @@ -447,20 +447,20 @@ private def assertOutOfBoundsObligations assert! md.getPropertyType == some MetaData.outOfBoundsAccess -- Sequence.select / update / take / drop each emit one out-of-bounds obligation. -#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqSelectOp [fxS, fxI]) 1 -#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqUpdateOp [fxS, fxI, fxV]) 1 -#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqTakeOp [fxS, fxN]) 1 -#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqDropOp [fxS, fxN]) 1 +#eval assertOutOfBoundsObligations (LExpr.mkApp default Core.seqSelectOp [fxS, fxI]) 1 +#eval assertOutOfBoundsObligations (LExpr.mkApp default Core.seqUpdateOp [fxS, fxI, fxV]) 1 +#eval assertOutOfBoundsObligations (LExpr.mkApp default Core.seqTakeOp [fxS, fxN]) 1 +#eval assertOutOfBoundsObligations (LExpr.mkApp default Core.seqDropOp [fxS, fxN]) 1 -- Nested: `Sequence.select(Sequence.update(s, i, v), j)` emits two -- obligations (one per partial call), both tagged `outOfBoundsAccess`. #eval assertOutOfBoundsObligations - (LExpr.mkApp () Core.seqSelectOp [LExpr.mkApp () Core.seqUpdateOp [fxS, fxI, fxV], fxJ]) 2 + (LExpr.mkApp default Core.seqSelectOp [LExpr.mkApp default Core.seqUpdateOp [fxS, fxI, fxV], fxJ]) 2 -- Sequence.length is total: no precondition obligations generated. #eval do let stmts := collectPrecondAsserts Core.Factory - (LExpr.mkApp () Core.seqLengthOp [fxS]) "test" #[] + (LExpr.mkApp default Core.seqLengthOp [fxS]) "test" #[] assert! stmts.isEmpty /-! #### Test 10a: Pretty-printed obligation shape per partial op @@ -478,19 +478,19 @@ private def printFirstObligation (expr : Core.Expression.Expr) : IO Unit := do /-- info: 0 <= i && i < Sequence.length(s) -/ #guard_msgs in -#eval printFirstObligation (LExpr.mkApp () Core.seqSelectOp [fxS, fxI]) +#eval printFirstObligation (LExpr.mkApp default Core.seqSelectOp [fxS, fxI]) /-- info: 0 <= i && i < Sequence.length(s) -/ #guard_msgs in -#eval printFirstObligation (LExpr.mkApp () Core.seqUpdateOp [fxS, fxI, fxV]) +#eval printFirstObligation (LExpr.mkApp default Core.seqUpdateOp [fxS, fxI, fxV]) /-- info: 0 <= n && n <= Sequence.length(s) -/ #guard_msgs in -#eval printFirstObligation (LExpr.mkApp () Core.seqTakeOp [fxS, fxN]) +#eval printFirstObligation (LExpr.mkApp default Core.seqTakeOp [fxS, fxN]) /-- info: 0 <= n && n <= Sequence.length(s) -/ #guard_msgs in -#eval printFirstObligation (LExpr.mkApp () Core.seqDropOp [fxS, fxN]) +#eval printFirstObligation (LExpr.mkApp default Core.seqDropOp [fxS, fxN]) end SeqBoundsObligations diff --git a/StrataTest/Transform/ProcedureInlining.lean b/StrataTest/Transform/ProcedureInlining.lean index a7c7c08f4a..36da231b71 100644 --- a/StrataTest/Transform/ProcedureInlining.lean +++ b/StrataTest/Transform/ProcedureInlining.lean @@ -14,6 +14,7 @@ import Strata.Languages.Core.ProgramWF import Strata.Transform.CoreTransform import Strata.Transform.ProcedureInlining import Strata.Util.Tactics +-- Test fixtures build Core expressions directly with synthesized provenance open Core open Core.Transform @@ -68,14 +69,14 @@ private def substExpr (e1:Expression.Expr) (map:Map String String) := -- created by CoreGenM. -- All variables now have Unit metadata; we substitute by name. let old_id : Expression.Ident := { name := i1, metadata := () } - let new_expr : Expression.Expr := .fvar () { name := i2, metadata := () } .none + let new_expr : Expression.Expr := .fvar (ExprSourceLoc.synthesized "test") { name := i2, metadata := () } .none e.substFvar old_id new_expr) e1 private def alphaEquivExprs (e1 e2: Expression.Expr) (map:IdMap) : Bool := - (substExpr e1 (map.vars.fst)).eraseTypes == e2.eraseTypes && - (substExpr e2 (map.vars.snd)).eraseTypes == e1.eraseTypes + (substExpr e1 (map.vars.fst)).eraseTypes.eraseMetadata == e2.eraseTypes.eraseMetadata && + (substExpr e2 (map.vars.snd)).eraseTypes.eraseMetadata == e1.eraseTypes.eraseMetadata private def alphaEquivExprsOpt (e1 e2: Option Expression.Expr) (map:IdMap) : Except Format Bool :=