Add CoreMatch dialect: surface pattern matching for Strata Core

Examples/pattern_matching/01_option.coreMatch.st

@@ -0,0 +1,21 @@
+program CoreMatch;
+
+// Option-like enum: non-recursive datatype, simplest possible match.
+
+datatype OptInt () { None(), Some(val : int) };
+
+function getOr(o : OptInt, dflt : int) : int
+{
+  match o {
+    arm None()              => dflt;
+    arm Some(val : int)     => val;
+  }
+};
+
+function isSome(o : OptInt) : bool
+{
+  match o {
+    arm None()              => false;
+    arm Some(val : int)     => true;
+  }
+};

Examples/pattern_matching/02_color.coreMatch.st

@@ -0,0 +1,34 @@
+program CoreMatch;
+
+// Pure enum with wildcard arms covering uncovered constructors.
+
+datatype Color () { Red(), Green(), Blue(), Yellow() };
+
+function isWarm(c : Color) : bool
+{
+  match c {
+    arm Red()    => true;
+    arm Yellow() => true;
+    arm _        => false;
+  }
+};
+
+function isPrimary(c : Color) : bool
+{
+  match c {
+    arm Red()   => true;
+    arm Green() => true;
+    arm Blue()  => true;
+    arm _       => false;
+  }
+};
+
+function rank(c : Color) : int
+{
+  match c {
+    arm Red()    => 1;
+    arm Green()  => 2;
+    arm Blue()   => 3;
+    arm Yellow() => 4;
+  }
+};

Examples/pattern_matching/03_peano.coreMatch.st

@@ -0,0 +1,29 @@
+program CoreMatch;
+
+// Peano naturals: natural-style recursion on the `pred` field.
+
+datatype Nat () { Zero(), Succ(pred : Nat) };
+
+rec function toInt(n : Nat) : int
+{
+  match n {
+    arm Zero()           => 0;
+    arm Succ(pred : Nat) => 1 + toInt(pred);
+  }
+};
+
+rec function isZero(n : Nat) : bool
+{
+  match n {
+    arm Zero()           => true;
+    arm Succ(pred : Nat) => false;
+  }
+};
+
+rec function double(n : Nat) : Nat
+{
+  match n {
+    arm Zero()           => Zero();
+    arm Succ(pred : Nat) => Succ(Succ(double(pred)));
+  }
+};

Examples/pattern_matching/04_list.coreMatch.st

@@ -0,0 +1,37 @@
+program CoreMatch;
+
+// Monomorphic List of int: natural-style recursion on `tl`.
+
+datatype List () { Nil(), Cons(hd : int, tl : List) };
+
+rec function length(xs : List) : int
+{
+  match xs {
+    arm Nil() => 0;
+    arm Cons(hd : int, tl : List) => 1 + length(tl);
+  }
+};
+
+rec function sum(xs : List) : int
+{
+  match xs {
+    arm Nil() => 0;
+    arm Cons(hd : int, tl : List) => hd + sum(tl);
+  }
+};
+
+rec function allPositive(xs : List) : bool
+{
+  match xs {
+    arm Nil() => true;
+    arm Cons(hd : int, tl : List) => hd > 0 && allPositive(tl);
+  }
+};
+
+rec function containsZero(xs : List) : bool
+{
+  match xs {
+    arm Nil() => false;
+    arm Cons(hd : int, tl : List) => hd == 0 || containsZero(tl);
+  }
+};

Examples/pattern_matching/05_tree_dfs.coreMatch.st

@@ -0,0 +1,50 @@
+program CoreMatch;
+
+// Binary tree DFS: natural-style recursion on `left` and `right`.
+
+datatype Tree () { Leaf(), Node(value : int, left : Tree, right : Tree) };
+
+rec function treeSum(t : Tree) : int
+{
+  match t {
+    arm Leaf() => 0;
+    arm Node(value : int, left : Tree, right : Tree) =>
+      value + treeSum(left) + treeSum(right);
+  }
+};
+
+rec function nodeCount(t : Tree) : int
+{
+  match t {
+    arm Leaf() => 0;
+    arm Node(value : int, left : Tree, right : Tree) =>
+      1 + nodeCount(left) + nodeCount(right);
+  }
+};
+
+rec function depth(t : Tree) : int
+{
+  match t {
+    arm Leaf() => 0;
+    arm Node(value : int, left : Tree, right : Tree) =>
+      1 + (if depth(left) >= depth(right) then depth(left) else depth(right));
+  }
+};
+
+rec function allNonNeg(t : Tree) : bool
+{
+  match t {
+    arm Leaf() => true;
+    arm Node(value : int, left : Tree, right : Tree) =>
+      value >= 0 && allNonNeg(left) && allNonNeg(right);
+  }
+};
+
+rec function containsZero(t : Tree) : bool
+{
+  match t {
+    arm Leaf() => false;
+    arm Node(value : int, left : Tree, right : Tree) =>
+      value == 0 || containsZero(left) || containsZero(right);
+  }
+};

Examples/pattern_matching/06_either.coreMatch.st

@@ -0,0 +1,29 @@
+program CoreMatch;
+
+// Either with heterogeneously-typed constructor fields.
+
+datatype Either () { LeftI(v : int), RightB(b : bool) };
+
+function isError(e : Either) : bool
+{
+  match e {
+    arm LeftI(v : int)   => v < 0;
+    arm RightB(b : bool) => !b;
+  }
+};
+
+function describeKind(e : Either) : int
+{
+  match e {
+    arm LeftI(v : int)   => 1;
+    arm RightB(b : bool) => 2;
+  }
+};
+
+function unwrapOr(e : Either, dflt : int) : int
+{
+  match e {
+    arm LeftI(v : int)   => v;
+    arm RightB(b : bool) => dflt;
+  }
+};

Examples/pattern_matching/07_nested_match.coreMatch.st

@@ -0,0 +1,24 @@
+program CoreMatch;
+
+// Nested non-recursive matches: outer on `m`, inner on `s`.
+
+datatype Shape () { Circle(radius : int), Square(side : int), Triangle(base : int, height : int) };
+datatype Mode  () { Area(), Perimeter() };
+
+function compute(s : Shape, m : Mode) : int
+{
+  match m {
+    arm Area() =>
+      match s {
+        arm Circle(radius : int)               => 3 * radius * radius;
+        arm Square(side : int)                 => side * side;
+        arm Triangle(base : int, height : int) => base * height;
+      };
+    arm Perimeter() =>
+      match s {
+        arm Circle(radius : int)               => 6 * radius;
+        arm Square(side : int)                 => 4 * side;
+        arm Triangle(base : int, height : int) => base + base + height;
+      };
+  }
+};

Examples/pattern_matching/08_expr_eval.coreMatch.st

@@ -0,0 +1,35 @@
+program CoreMatch;
+
+// Expression-tree evaluator: natural-style recursion on `l` and `r`.
+
+datatype Op   () { Plus(), Times(), Minus() };
+datatype Tree () { Lit(v : int), Bin(op : Op, l : Tree, r : Tree) };
+
+rec function eval(t : Tree) : int
+{
+  match t {
+    arm Lit(v : int) => v;
+    arm Bin(op : Op, l : Tree, r : Tree) =>
+      match op {
+        arm Plus()  => eval(l) + eval(r);
+        arm Times() => eval(l) * eval(r);
+        arm Minus() => eval(l) - eval(r);
+      };
+  }
+};
+
+rec function size(t : Tree) : int
+{
+  match t {
+    arm Lit(v : int) => 1;
+    arm Bin(op : Op, l : Tree, r : Tree) => 1 + size(l) + size(r);
+  }
+};
+
+rec function constantsOnly(t : Tree) : bool
+{
+  match t {
+    arm Lit(v : int) => true;
+    arm Bin(op : Op, l : Tree, r : Tree) => constantsOnly(l) && constantsOnly(r);
+  }
+};

Examples/pattern_matching/09_constructor_calls.coreMatch.st

@@ -0,0 +1,31 @@
+program CoreMatch;
+
+// Constructor calls in arm bodies plus natural-style recursion.
+
+datatype List () { Nil(), Cons(hd : int, tl : List) };
+datatype Pair () { MkPair(first : int, second : List) };
+
+rec function map_inc(xs : List) : List
+{
+  match xs {
+    arm Nil() => Nil();
+    arm Cons(hd : int, tl : List) => Cons(hd + 1, map_inc(tl));
+  }
+};
+
+rec function filter_pos(xs : List) : List
+{
+  match xs {
+    arm Nil() => Nil();
+    arm Cons(hd : int, tl : List) =>
+      if hd > 0 then Cons(hd, filter_pos(tl)) else filter_pos(tl);
+  }
+};
+
+function head_or_zero_with_rest(xs : List) : Pair
+{
+  match xs {
+    arm Nil()                       => MkPair(0, Nil());
+    arm Cons(hd : int, tl : List)   => MkPair(hd, tl);
+  }
+};

Scripts/CoreMatchCheck.lean

@@ -0,0 +1,72 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import Strata.Languages.CoreMatch.Verify
+import Strata.Languages.CoreMatch.DDMTransform.StrataGen
+import Strata.DDM.Elab
+
+/-!
+Per-file iteration helper for the CoreMatch dialect. Invoked as
+`lake exe coreMatchCheck <file.coreMatch.st> [--show-decls]`; prints
+`OK: <N> decls` on success or `ERR: <message>` on failure.
+-/
+
+open Strata
+open Lambda
+
+private def declSummary (d : Core.Decl) : String :=
+  match d with
+  | .type t _ =>
+    match t with
+    | .data block =>
+      let names := block.map (·.name)
+      s!"  type (data) {names}"
+    | .con tc => s!"  type {tc.name}"
+    | .syn ts => s!"  type {ts.name} (synonym)"
+  | .ax a _ => s!"  axiom {a.name}"
+  | .distinct n _ _ => s!"  distinct {n.name}"
+  | .proc p _ => s!"  procedure {p.header.name.name}"
+  | .func f _ =>
+    let kind := if f.isRecursive then "rec function" else "function"
+    s!"  {kind} {f.name.name}"
+  | .recFuncBlock fs _ =>
+    let names := fs.map (·.name.name)
+    s!"  rec block {names}"
+
+private def runOnFile (path : System.FilePath) (showDecls : Bool) : IO UInt32 := do
+  let content ← IO.FS.readFile path
+  let input := Strata.Parser.stringInputContext path content
+  let dialects :=
+    Strata.Elab.LoadedDialects.ofDialects!
+      #[Strata.initDialect, Strata.Core, Strata.CoreMatch]
+  let leanEnv ← Lean.mkEmptyEnvironment 0
+  let prog ←
+    match Strata.Elab.elabProgram dialects leanEnv input with
+    | .ok p => pure p
+    | .error errors =>
+      let mut msg : String := "ERR: parse failed:"
+      for e in errors do
+        msg := msg ++ s!"\n  {e.pos.line}:{e.pos.column}: {← e.data.toString}"
+      IO.eprintln msg
+      return (1 : UInt32)
+  match Strata.CoreMatch.Verify.parseToCore prog path.toString with
+  | .error e =>
+    IO.eprintln s!"ERR: lowering failed: {e.format none}"
+    return (1 : UInt32)
+  | .ok cp =>
+    IO.println s!"OK: {cp.decls.length} decls"
+    if showDecls then
+      for d in cp.decls do
+        IO.println (declSummary d)
+    return (0 : UInt32)
+
+def main (args : List String) : IO UInt32 := do
+  match args with
+  | [] | ["--help"] =>
+    IO.println "Usage: lake exe coreMatchCheck <file.coreMatch.st> [--show-decls]"
+    return (0 : UInt32)
+  | path :: rest =>
+    let showDecls := rest.contains "--show-decls"
+    runOnFile path showDecls

Strata.lean

@@ -40,6 +40,11 @@ import Strata.Languages.Boole.Boole
 import Strata.Languages.Boole.Verify
 import Strata.Languages.C_Simp.C_Simp
 import Strata.Languages.C_Simp.Verify
+import Strata.Languages.CoreMatch.CoreMatch
+import Strata.Languages.CoreMatch.ToCore
+import Strata.Languages.CoreMatch.Verify
+import Strata.Languages.CoreMatch.DDMTransform.StrataGen
+import Strata.Languages.CoreMatch.DDMTransform.Translate
 import Strata.Languages.Core.EntryPoint
 import Strata.Languages.Core.VerifierProofs
 import Strata.Languages.Dyn.Dyn