Add constraints' method to Expr and refactor toSuperscript usage; create TutorialSheet5 example

Author: HEIGE-PCloud

ProgramAnalysis/ControlFlowAnalysis/Analysis.lean

@@ -98,6 +98,8 @@ public def Expr.constraints : Expr → ReaderM (List FnTerm) (Set Constraint)
         .ofList (fns.map (fun t => Constraint.conditional t (.cache t1.label) (.cache t2.label) (.env t.var))) ∪
         .ofList (fns.map (fun t => Constraint.conditional t (.cache t1.label) (.cache t.body.label) (.cache label)))
 
+public def Expr.constraints' : Expr → (Set Constraint) := fun expr => expr.constraints.run (expr.allFns)
+
 public abbrev Constraint.Node := ConcreteDomain
 
 public def Constraint.nodes : Constraint → List Node

ProgramAnalysis/ControlFlowAnalysis/Basic.lean

@@ -3,21 +3,6 @@ module
 public import Std.Data.TreeSet
 public import Std.Data.TreeMap
 
-public def Char.toSuperScript : Char → Char
-  | '0' => '⁰'
-  | '1' => '¹'
-  | '2' => '²'
-  | '3' => '³'
-  | '4' => '⁴'
-  | '5' => '⁵'
-  | '6' => '⁶'
-  | '7' => '⁷'
-  | '8' => '⁸'
-  | '9' => '⁹'
-  | c => c
-
-public def Nat.toSuperscript (n : Nat) : String := (toString n).map Char.toSuperScript
-
 public def Std.TreeSet.subset (s1 s2 : Std.TreeSet α cmp) : Bool :=
   s1.all s2.contains
 

ProgramAnalysis/ControlFlowAnalysis/Fun.lean

@@ -78,7 +78,7 @@ public def Term.toString : Term → String
   | .letin x e1 e2 => s!"(let {x} = {e1.toString} in {e2.toString})"
 
 public def Expr.toString : Expr → String
-  | .e t l => s!"{t.toString}{l.toSuperscript}"
+  | .e t l => s!"{t.toString}{l.toSuperscriptString}"
 end
 end
 

ProgramAnalysis/Example.lean

@@ -1,3 +1,4 @@
 module
 
 import ProgramAnalysis.Example.Exam2425
+import ProgramAnalysis.Example.TutorialSheet5

ProgramAnalysis/Example/TutorialSheet5.lean

@@ -0,0 +1,73 @@
+module
+import ProgramAnalysis.DataFlowAnalysis
+meta import ProgramAnalysis.DataFlowAnalysis
+import ProgramAnalysis.ControlFlowAnalysis
+meta import ProgramAnalysis.ControlFlowAnalysis
+
+namespace ProgramAnalysis.Example
+
+section Exercise2
+
+open ControlFlowAnalysis
+
+def expr : Expr := [Fun|
+(let g = (fn f => (if (f 3) then 10 else 5))
+in (g (fn y => (y > 2))))
+]
+
+/--
+info: (let g = (fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶)⁷ in (g⁸ (fn y => (y⁹ > 2¹⁰)¹¹)¹²)¹³)¹⁴
+-/
+#guard_msgs in
+#eval IO.println expr
+
+def constraints := expr.constraints'
+
+/--
+info: C(4) ⊆ C(6)
+C(5) ⊆ C(6)
+C(7) ⊆ r(g)
+C(13) ⊆ C(14)
+r(f) ⊆ C(1)
+r(g) ⊆ C(8)
+r(y) ⊆ C(9)
+fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶ ⊆ C(7)
+fn y => (y⁹ > 2¹⁰)¹¹ ⊆ C(12)
+fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶ ⊆ C(1) => C(2) ⊆ r(f)
+fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶ ⊆ C(1) => C(6) ⊆ C(3)
+fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶ ⊆ C(8) => C(6) ⊆ C(13)
+fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶ ⊆ C(8) => C(12) ⊆ r(f)
+fn y => (y⁹ > 2¹⁰)¹¹ ⊆ C(1) => C(2) ⊆ r(y)
+fn y => (y⁹ > 2¹⁰)¹¹ ⊆ C(1) => C(11) ⊆ C(3)
+fn y => (y⁹ > 2¹⁰)¹¹ ⊆ C(8) => C(11) ⊆ C(13)
+fn y => (y⁹ > 2¹⁰)¹¹ ⊆ C(8) => C(12) ⊆ r(y)
+-/
+#guard_msgs in
+#eval constraints.forM IO.println
+
+def solution := Constraint.solve constraints.toList
+
+/--
+info: C(1) ↦ [fn y => (y⁹ > 2¹⁰)¹¹]
+C(2) ↦ []
+C(3) ↦ []
+C(4) ↦ []
+C(5) ↦ []
+C(6) ↦ []
+C(7) ↦ [fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶]
+C(8) ↦ [fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶]
+C(9) ↦ []
+C(11) ↦ []
+C(12) ↦ [fn y => (y⁹ > 2¹⁰)¹¹]
+C(13) ↦ []
+C(14) ↦ []
+r(f) ↦ [fn y => (y⁹ > 2¹⁰)¹¹]
+r(g) ↦ [fn f => (if (f¹ 3²)³ then 10⁴ else 5⁵)⁶]
+r(y) ↦ []
+-/
+#guard_msgs in
+#eval solution.toList.forM (fun (node, value) => IO.println s!"{node} ↦ {value.toList.map (fun t: FnTerm => t)}")
+
+end Exercise2
+
+end ProgramAnalysis.Example