Strata/StrataTest/DL/Imperative/Arith.lean at main · keyboardDrummer/Strata · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
/-
  Copyright Strata Contributors

  SPDX-License-Identifier: Apache-2.0 OR MIT
-/
module

meta import all StrataTest.DL.Imperative.ArithExpr
meta import all StrataTest.DL.Imperative.ArithEval
meta import all StrataTest.DL.Imperative.ArithType

meta section

---------------------------------------------------------------------
namespace Arith
open Std (ToFormat Format format)

def typeCheckAndPartialEval (cmds : Commands) : Except Format (Commands × Eval.State) := do
  let (cmds, _T) ← Imperative.Cmds.typeCheck () TEnv.init cmds
    |>.mapError (fun dm => dm.message)
  let (cmds, S) := Imperative.Cmds.eval Eval.State.init cmds
  return (cmds, S)

private def testProgram1 : Commands :=
  [.init "x" .Num (.det (.Var "y" (.some .Num))) .empty,
   .set "x" .nondet .empty,
   .assert "x_value_eq" (.Eq (.Var "x" .none) (.Var "y" none)) .empty]

/--
info: ok: Commands:
init (x : Num) := (y : Num)
havoc x
assert [x_value_eq] ($__x0 : Num) = (y : Num)

State:
error: none
warnings: []
deferred: #[Label: x_value_eq
 Property : assert
 Assumptions: ⏎
 Obligation: ($__x0 : Num) = (y : Num)
 Metadata: ⏎
 ]
pathConditions: ⏎
env: (y, (Num, (y : Num))) (x, (Num, ($__x0 : Num)))
genNum: 1
-/
#guard_msgs in
#eval do let (cmds, S) ← typeCheckAndPartialEval testProgram1
         return format (cmds, S)


private def testProgram2 : Commands :=
  [.init "x" .Num (.det (.Num 0)) .empty,
   .set "x" (.det (.Plus (.Var "x" .none) (.Num 100))) .empty,
   .assert "x_value_eq" (.Eq (.Var "x" .none) (.Num 100)) .empty]

/--
info: ok: Commands:
init (x : Num) := 0
x := 100
assert [x_value_eq] true

State:
error: none
warnings: []
deferred: #[Label: x_value_eq
 Property : assert
 Assumptions: ⏎
 Obligation: true
 Metadata: ⏎
 ]
pathConditions: ⏎
env: (x, (Num, 100))
genNum: 0
-/
#guard_msgs in
#eval do let (cmds, S) ← typeCheckAndPartialEval testProgram2
         return format (cmds, S)

end Arith
---------------------------------------------------------------------
end