Laurel parsing

.github/workflows/ci.yml

@@ -116,7 +116,7 @@ jobs:
         run: .github/scripts/checkLeanImport.sh
 
   build_doc:
-    name: Build Documentation
+    name: Build documentation
     runs-on: ubuntu-latest
     permissions:
       contents: read
@@ -126,10 +126,10 @@ jobs:
         uses: leanprover/lean-action@v1
         with:
           build-args: '--wfail'
-          lake-package-directory: 'docs/ddm'
-      - name: Build Documentation
-        run: lake exe docs 
-        working-directory: docs/ddm
+          lake-package-directory: 'docs/verso'
+      - name: Build documentation
+        run: ./generate.sh
+        working-directory: docs/verso
 
   build_python:
     name: Build and test Python

Examples/dialects/Arith.dialect.st

@@ -8,7 +8,7 @@ fn sub_expr (a : Int, b : Int) : Int => @[prec(25), leftassoc] a " - " b;
 fn mul_expr (a : Int, b : Int) : Int => @[prec(30), leftassoc] a " * " b;
 fn exp_expr (a : Int, b : Int) : Int => @[prec(32), rightassoc] a " ^ " b;
 
-fn le (a : Int, b : Int) : Bool => @[prec(15)] a " <= " b;
-fn lt (a : Int, b : Int) : Bool => @[prec(15)] a " < " b;
-fn ge (a : Int, b : Int) : Bool => @[prec(15)] a " >= " b;
-fn gt (a : Int, b : Int) : Bool => @[prec(15)] a " > " b;
+fn le (a : Int, b : Int) : BoolType => @[prec(15)] a " <= " b;
+fn lt (a : Int, b : Int) : BoolType => @[prec(15)] a " < " b;
+fn ge (a : Int, b : Int) : BoolType => @[prec(15)] a " >= " b;
+fn gt (a : Int, b : Int) : BoolType => @[prec(15)] a " > " b;

Examples/dialects/Bool.dialect.st

@@ -1,18 +1,18 @@
 dialect Bool;
-// Introduce Boolean type
-type Bool;
 
-// Introduce literals as constants.
-fn true_lit : Bool => "true";
-fn false_lit : Bool => "false";
+// BoolType for use in function signatures
+type BoolType;
+
+// Function to lift Init.Bool literals to expressions
+fn boolLit (b : Bool) : BoolType => b;
 
 // Introduce basic Boolean operations.
 fn not_expr (tp : Type, a : tp) : tp => "-" a;
-fn and (a : Bool, b : Bool) : Bool => @[prec(10), leftassoc] a " && " b;
-fn or (a : Bool, b : Bool) : Bool => @[prec(8), leftassoc] a " || " b;
-fn imp (a : Bool, b : Bool) : Bool => @[prec(8), leftassoc] a " ==> " b;
+fn and (a : BoolType, b : BoolType) : BoolType => @[prec(10), leftassoc] a " && " b;
+fn or (a : BoolType, b : BoolType) : BoolType => @[prec(8), leftassoc] a " || " b;
+fn imp (a : BoolType, b : BoolType) : BoolType => @[prec(8), leftassoc] a " ==> " b;
 
 // Introduce equality operations that work for arbitrary types.
 // The type is inferred.
-fn equal (tp : Type, a : tp, b : tp) : Bool => @[prec(15)] a " == " b;
-fn not_equal (tp : Type, a : tp, b : tp) : Bool => @[prec(15)] a " != " b;
+fn equal (tp : Type, a : tp, b : tp) : BoolType => @[prec(15)] a " == " b;
+fn not_equal (tp : Type, a : tp, b : tp) : BoolType => @[prec(15)] a " != " b;

Strata.lean

@@ -16,16 +16,8 @@ import Strata.DL.Lambda.Lambda
 import Strata.DL.Imperative.Imperative
 
 /- Boogie -/
-import Strata.Languages.Boogie.Examples.Examples
 import Strata.Languages.Boogie.StatementSemantics
 
-/- CSimp -/
-import Strata.Languages.C_Simp.Examples.Examples
-
-/- Dyn -/
-import Strata.Languages.Dyn.Examples.Examples
-
-
 /- Code Transforms -/
 import Strata.Transform.CallElimCorrect
 import Strata.Transform.DetToNondetCorrect

Strata/Backends/CBMC/BoogieToCBMC.lean

@@ -173,7 +173,7 @@ partial def blockToJson {P : Imperative.PureExpr} (I : Lambda.LExprParams) [Iden
       ("statement", Json.mkObj [("id", "block")]),
       ("type", emptyType)
     ]),
-    ("sub", Json.arr (b.ss.map (stmtToJson (I:=I) · loc)).toArray)
+    ("sub", Json.arr (b.map (stmtToJson (I:=I) · loc)).toArray)
   ]
 
 partial def stmtToJson {P : Imperative.PureExpr} (I : Lambda.LExprParams) [IdentToStr (Lambda.Identifier I.IDMeta)] [HasLExpr P I]

Strata/Backends/CBMC/StrataToCBMC.lean

@@ -299,7 +299,7 @@ partial def blockToJson (b: Imperative.Block Strata.C_Simp.Expression Strata.C_S
       ("statement", Json.mkObj [("id", "block")]),
       ("type", emptyType)
     ]),
-    ("sub", Json.arr (b.ss.map (stmtToJson · loc)).toArray)
+    ("sub", Json.arr (b.map (stmtToJson · loc)).toArray)
   ]
 
 partial def stmtToJson (e : Strata.C_Simp.Statement) (loc: SourceLoc) : Json :=

Strata/DDM/AST.lean

@@ -8,9 +8,23 @@ import Std.Data.HashMap
 import Strata.DDM.Util.Array
 import Strata.DDM.Util.ByteArray
 import Strata.DDM.Util.Decimal
+import Std.Data.HashMap.Lemmas
 
 set_option autoImplicit false
 
+namespace Strata.Array
+
+theorem mem_iff_back_or_pop {α} (a : α) {as : Array α} (p : as.size > 0 := by get_elem_tactic) :
+  a ∈ as ↔ (a = as.back ∨ a ∈ as.pop) := by
+  simp [Array.mem_iff_getElem]
+  grind
+
+theorem of_mem_pop {α} {a : α} {as : Array α} : a ∈ as.pop → a ∈ as := by
+  simp [Array.mem_iff_getElem]
+  grind
+
+end Strata.Array
+
 namespace Strata
 
 abbrev DialectName := String
@@ -175,7 +189,7 @@ inductive ArgF (α : Type) : Type where
 | expr (e : ExprF α)
 | type (e : TypeExprF α)
 | ident (ann : α) (i : String)
-| num (ann : α)(v : Nat)
+| num (ann : α) (v : Nat)
 | decimal (ann : α) (v : Decimal)
 | strlit (ann : α) (i : String)
 | bytes (ann : α) (a : ByteArray)
@@ -303,9 +317,9 @@ As an example, in the string `"123abc\ndef"`, the string
 -/
 structure SourceRange where
   /-- The starting offset of the source range. -/
-  start : String.Pos
+  start : String.Pos.Raw
   /-- One past the end of the range. -/
-  stop : String.Pos
+  stop : String.Pos.Raw
 deriving BEq, Inhabited, Repr
 
 namespace SourceRange
@@ -587,7 +601,8 @@ inductive SyntaxDefAtom
 -- Surround with parenthesis if the precedence of the argument is less than `prec`.
 -- Note. If `prec` is zero, then parenthesis will never be added (even with pp.parens is true).
 -- This is to avoid parens in categories that do not support them.
-| ident (level : Nat) (prec : Nat)
+-- The unwrap parameter specifies if the value should be unwrapped to a raw type.
+| ident (level : Nat) (prec : Nat) (unwrap : Bool := false)
 | str (lit : String)
 | indent (n : Nat) (args : Array SyntaxDefAtom)
 deriving BEq, Inhabited, Repr
@@ -1160,12 +1175,18 @@ instance {α β} [BEq α] [Hashable α] [BEq β]: BEq (Std.HashMap α β) where
 
 structure DialectMap where
   map : Std.HashMap DialectName Dialect
-deriving BEq, Inhabited
+  closed : ∀(d : DialectName) (p: d ∈ map), map[d].imports.all (· ∈ map)
 
 namespace DialectMap
 
+instance : BEq DialectMap where
+  beq x y := x.map == y.map
+
 instance : EmptyCollection DialectMap where
-  emptyCollection := .mk {}
+  emptyCollection := { map := {}, closed := by simp }
+
+instance : Inhabited DialectMap where
+  default := {}
 
 instance : Membership DialectName DialectMap where
   mem m d := d ∈ m.map
@@ -1178,23 +1199,61 @@ instance : GetElem? DialectMap DialectName Dialect (fun m d => d ∈ m) where
   getElem? m d := m.map[d]?
   getElem! m d := m.map[d]!
 
+/--
+This inserts a new dialect into the dialect map.
+
+This requires propositions to ensure we do not change the semantics
+of dialects and imports are already in dialect.
+-/
+def insert (m : DialectMap) (d : Dialect) (_d_new : d.name ∉ m) (d_imports_ok : d.imports.all (· ∈ m)) : DialectMap :=
+  { map := m.map.insert d.name d
+    closed := by
+      intro name mem
+      if eq : d.name = name then
+        simp at d_imports_ok
+        simp [eq]
+        intro i lt
+        exact Or.inr (d_imports_ok i lt)
+      else
+        simp only [Std.HashMap.mem_insert, eq, beq_iff_eq, false_or] at mem
+        have cl := m.closed name mem
+        simp at cl
+        simp [Std.HashMap.getElem_insert, eq]
+        intro i lt
+        exact Or.inr (cl i lt)
+  }
+
 /--
 This inserts a dialect in to the dialect map.
 
 It panics if a dialect with the same name is already in the map
 or if the dialect imports a dialect not already in the map.
 -/
 def insert! (m : DialectMap) (d : Dialect) : DialectMap :=
-  assert! d.name ∉ m
-  assert! d.imports.all (· ∈ m)
-  { map := m.map.insert d.name d }
+  if d_new : d.name ∈ m then
+    panic! s!"{d.name} already in map."
+  else
+    if d_imports_ok : d.imports.all (· ∈ m) then
+      m.insert d d_new d_imports_ok
+    else
+      panic! s!"Missing import."
 
 def ofList! (l : List Dialect) : DialectMap :=
-  let m := l.foldl (init := {}) fun m d =>
-    assert! d.name ∉ m;
-    m.insert d.name d
-  assert! l.all fun d => d.imports.all (· ∈ m)
-  { map := m }
+  let map : Std.HashMap DialectName Dialect :=
+        l.foldl (init := .emptyWithCapacity l.length) fun m d =>
+          m.insert d.name d
+  let check := map.toArray.all fun (nm, d) => d.imports.all (· ∈ map)
+  if p : check then
+    { map := map,
+      closed := by
+        intro name name_mem
+        simp only [check, Array.all_eq_true_iff_forall_mem (xs := map.toArray)] at p
+        have mem : (name, map[name]) ∈ map.toArray := by
+          simp [Std.HashMap.mem_toArray_iff_getElem?_eq_some]
+        exact p (name, map[name]) mem
+    }
+  else
+    panic! "Invalid list"
 
 def toList (m : DialectMap) : List Dialect := m.map.values
 
@@ -1216,24 +1275,60 @@ Return set of all dialects that are imported by `dialect`.
 
 This includes transitive imports.
 -/
-partial def importedDialects! (map : DialectMap) (dialect : DialectName) : DialectMap := aux (.ofList [(d.name, d)]) [d]
-  where d :=
-          match map[dialect]? with
-          | none => panic! s!"Unknown dialect {dialect}"
-          | some d => d
-        aux (all : Std.HashMap DialectName Dialect) (next : List Dialect) : DialectMap :=
-          match next with
-          | d :: next =>
-            let (all, next) := d.imports.foldl (init := (all, next)) fun (all, next) i =>
-              if i ∈ all then
-                (all, next)
-              else
-                let d := match map[i]? with
-                          | none => panic! s!"Unknown dialect {i}"
-                          | some d => d
-               (all.insert i d, d :: next)
-            aux all next
-          | [] => DialectMap.mk all
+partial def importedDialects (dm : DialectMap) (dialect : DialectName) (p : dialect ∈ dm) : DialectMap :=
+    aux {} #[dialect] (by simp; exact p) (by simp)
+  where aux (map : Std.HashMap DialectName Dialect)
+            (next : Array DialectName)
+            (nextp : ∀name, name ∈ next → name ∈ dm)
+            (inv : ∀name (mem : name ∈ map), map[name].imports.all (fun i => i ∈ map ∨ i ∈ next))
+            : DialectMap :=
+          if emptyP : next.isEmpty then
+            { map := map,
+              closed := by intro d mem; grind
+            }
+          else
+            have next_size_pos : next.size > 0 := by
+              simp only [Array.isEmpty_iff] at emptyP
+              grind
+            let name  := next.back (h := next_size_pos)
+            if name_mem : name ∈ map then
+              aux map next.pop
+                (by
+                  intro d p
+                  exact nextp _ (Array.of_mem_pop p))
+                (by
+                  simp only [Array.all_eq_true']
+                  intro d d_mem e e_mem
+                  simp only [Array.all_eq_true'] at inv
+                  have inv2 := inv d d_mem e e_mem
+                  simp only [Array.mem_iff_back_or_pop e next_size_pos] at inv2
+                  grind)
+            else
+              have name_in_dm : name ∈ dm := nextp name (by grind)
+              let d := dm[name]
+              aux (map.insert name d) (next.pop ++ d.imports)
+                (by
+                  intro nm nm_mem
+                  simp at nm_mem
+                  match nm_mem with
+                  | .inl nm_mem =>
+                    exact nextp _ (Array.of_mem_pop nm_mem)
+                  | .inr nm_mem =>
+                    have inv := dm.closed name name_in_dm
+                    simp only [Array.all_eq_true'] at inv
+                    have inv2 := inv nm nm_mem
+                    simp at inv2
+                    exact inv2)
+                (by
+                  intro n n_mem
+                  if n_eq : name = n then
+                    simp [n_eq]
+                  else
+                    simp [n_eq] at n_mem
+                    simp [n_eq, Std.HashMap.getElem_insert]
+                    intro i lt
+                    have mem := Array.mem_iff_back_or_pop (map[n].imports[i]) next_size_pos
+                    grind)
 
 end DialectMap
 

Strata/DDM/BuiltinDialects/Init.lean

@@ -26,6 +26,20 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   declareAtomicCat q`Init.Decimal
   declareAtomicCat q`Init.Str
 
+  declareCat q`Init.Bool
+  declareOp {
+    name := "boolTrue",
+    argDecls := .empty,
+    category := q`Init.Bool,
+    syntaxDef := .ofList [.str "true"],
+  }
+  declareOp {
+    name := "boolFalse",
+    argDecls := .empty,
+    category := q`Init.Bool,
+    syntaxDef := .ofList [.str "false"],
+  }
+
   declareCat q`Init.Option #["a"]
 
   declareCat q`Init.Seq #["a"]

Strata/DDM/BuiltinDialects/StrataDDL.lean

@@ -151,6 +151,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   declareMetadata { name := "rightassoc", args := #[] }
 
   declareMetadata { name := "scope", args := #[.mk "scope" .ident] }
+  declareMetadata { name := "unwrap", args := #[] }
   declareMetadata { name := "declareType", args := #[.mk "name" .ident, .mk "args" (.opt .ident)] }
   declareMetadata { name := "aliasType",   args := #[.mk "name" .ident, .mk "args" (.opt .ident), .mk "def" .ident] }
   declareMetadata { name := "declare",     args := #[.mk "name" .ident, .mk "type" .ident] }