Match on values only. (RedPRL#462)

* Reduce and unfold terms before resolving match judgments.
* Tweak pretty printer of judgments.
* Remove now unnecessary unfolding in examples.

src/redprl/refiner.fun

@@ -426,7 +426,9 @@ struct
   struct
     open Computation
     fun Reduce sign = SequentReduce sign
-    fun ReduceAll sign = Lcf.rule o SequentReduceAll sign orelse_ Lcf.rule o MatchRecordReduce sign
+    fun ReduceAll sign = Lcf.rule o SequentReduceAll sign
+      orelse_ Lcf.rule o MatchReduce sign
+      orelse_ Lcf.rule o MatchRecordReduce sign
   end
 
   local
@@ -796,14 +798,28 @@ struct
          | (_, Machine.NEUTRAL blocker) => StepSubUniverseNeuExpand sign u blocker
          | _ => fail @@ E.NOT_APPLICABLE (Fpp.text "StepSubUniverse", TermPrinter.ppTerm u)
 
+      fun StepMatch sign u =
+        case canonicity sign u of
+           Machine.REDEX => Lcf.rule o Computation.MatchReduce sign
+         | Machine.CANONICAL => Lcf.rule o Misc.MatchOperator
+         | Machine.NEUTRAL (Machine.VAR x) => fail @@ E.NOT_APPLICABLE (Fpp.text "match", TermPrinter.ppTerm u)
+         | Machine.NEUTRAL (Machine.OPERATOR theta) => Lcf.rule o Custom.UnfoldAll sign [theta]
+
+      fun StepMatchRecord sign u =
+        case canonicity sign u of
+           Machine.REDEX => Lcf.rule o Computation.MatchRecordReduce sign
+         | Machine.CANONICAL => Lcf.rule o Record.MatchRecord
+         | Machine.NEUTRAL (Machine.VAR x) => fail @@ E.NOT_APPLICABLE (Fpp.text "match-record", TermPrinter.ppTerm u)
+         | Machine.NEUTRAL (Machine.OPERATOR theta) => Lcf.rule o Custom.UnfoldAll sign [theta]
+
       fun StepJdg sign = matchGoal
         (fn _ >> AJ.EQ_TYPE (tys, _, _) => StepEqType sign tys
           | _ >> AJ.EQ ((m, n), (ty, _, _)) => StepEq sign ((m, n), ty)
           | _ >> AJ.TRUE (ty, _, _) => StepTrue sign ty
           | _ >> AJ.SYNTH (m, _, _) => StepSynth sign m
           | _ >> AJ.SUB_UNIVERSE (univ, _, _) => StepSubUniverse sign univ
-          | MATCH _ => Lcf.rule o Misc.MatchOperator
-          | MATCH_RECORD _ => Lcf.rule o Record.MatchRecord orelse_ Lcf.rule o Computation.MatchRecordReduce sign then_ Lcf.rule o Record.MatchRecord
+          | MATCH (_, _, m, _) => StepMatch sign m
+          | MATCH_RECORD (_, m, _) => StepMatchRecord sign m
           | _ >> jdg => fail @@ E.NOT_APPLICABLE (Fpp.text "AutoStep", AJ.pretty jdg))
 
       (* favonia:

src/redprl/refiner_misc.fun

@@ -86,11 +86,20 @@ struct
         |>: goal #> (H, hole)
       end
 
+    fun MatchReduce sign _ jdg =
+      let
+        val _ = RedPrlLog.trace "Computation.MatchReduce"
+        val MATCH (th, k, a, ms) = jdg
+        val (goal, hole) = makeGoal @@ MATCH (th, k, reduce sign a, ms)
+      in
+        |>: goal #> (Hyps.empty, hole)
+      end
+
     fun MatchRecordReduce sign _ jdg = 
       let
         val _ = RedPrlLog.trace "Computation.MatchRecordReduce"
-        val MATCH_RECORD _ = jdg
-        val (goal, hole) = makeGoal @@ Seq.map (reduce sign) jdg
+        val MATCH_RECORD (lbl, tm, tuple) = jdg
+        val (goal, hole) = makeGoal @@ MATCH_RECORD (lbl, reduce sign tm, tuple)
       in
         |>: goal #> (Hyps.empty, hole)
       end
@@ -124,7 +133,11 @@ struct
     fun UnfoldAll sign opids _ jdg =
       let
         val _ = RedPrlLog.trace "Custom.UnfoldAll"
-        val H >> _ = jdg
+        val H =
+          case jdg of
+            H >> _ => H
+          | MATCH _ => Hyps.empty
+          | MATCH_RECORD _ => Hyps.empty
         val (goal, hole) = makeGoal @@ Seq.map (unfold sign opids) jdg
       in
         |>: goal #> (H, hole)

src/redprl/sequent.sml

@@ -59,7 +59,7 @@ struct
        else
          Fpp.seq [prettyHyps AJ.pretty H, Fpp.newline, Fpp.hsep [Fpp.text ">>", AJ.pretty catjdg]]
      | MATCH (th, k, a, _) => Fpp.hsep [TP.ppTerm a, Fpp.text "match", TP.ppOperator th, Fpp.text "@", Fpp.text (Int.toString k)]
-     | MATCH_RECORD (lbl, a, m) => Fpp.hsep [TP.ppTerm a, Fpp.text "match_record", Fpp.text lbl, Fpp.text "with tuple", TP.ppTerm m]
+     | MATCH_RECORD (lbl, a, m) => Fpp.hsep [TP.ppTerm a, Fpp.text "match-record", Fpp.text lbl, Fpp.text "with tuple", TP.ppTerm m]
 
   val rec eq =
     fn (H1 >> catjdg1, H2 >> catjdg2) =>

test/success/hlevels.prl

@@ -10,7 +10,6 @@ Thm InhPropIsContr(#l:lvl) : [
   [a : ty]
   (IsContr ty))
 ] by [
-  unfold IsProp;
   lam ty, h, a. {use a,lam x. `($ h x a)}
 ].
 
@@ -21,8 +20,7 @@ Thm PropPi(#l:lvl) : [
   [h : (-> [x : tyA] (IsProp ($ tyB x)))]
   (IsProp (-> [x : tyA] ($ tyB x))))
 ] by [
-  unfold IsProp; lam tyA, tyB, h, f, g.
-  <i> lam x. `(@ ($ h x ($ f x) ($ g x)) i)
+  lam tyA, tyB, h, f, g. <i> lam x. `(@ ($ h x ($ f x) ($ g x)) i)
 ].
 
 Thm PropSet(#l:lvl) : [
@@ -32,7 +30,6 @@ Thm PropSet(#l:lvl) : [
    (IsSet tyA)
   )
 ] by [
-  unfold [IsSet, IsProp];
   lam tyA, h, a, b, p, q.
   <j i> `(hcom 0~>1 tyA a
                [i=0 [k] (@ ($ h a a) k)]
@@ -48,13 +45,20 @@ Thm IsPropIsProp(#l:lvl) : [
    (IsProp (IsProp tyA))
   )
 ] by [
-  unfold IsProp; // If I don't unfold here I get a ton of obligations...
   lam tyA, h1, h2. // why is 1 and 2 blue?
-  (<i> lam a, b.
+  <i> lam a, b.
     let foo = (PropSet #l) [`tyA, `h1].
     unfold [IsSet, IsProp];
-    use foo [`a, `b, use h1 [`a, `b], use h2 [`a, `b], `i]);
-  unfold PropSet; auto
+    use foo [`a, `b, use h1 [`a, `b], use h2 [`a, `b], `i]
+].
+
+Thm IsPropIsProp'(#l:lvl) : [
+  (->
+   [tyA : (U #l kan)]
+   (IsProp (IsProp tyA))
+  )
+] by [
+  lam tyA, h1, h2. <i> lam a, b. `(@ ($ (PropSet #l) tyA h1 a b ($ h1 a b) ($ h2 a b)) i)
 ].
 
 // // This should be exactly like the one above:

test/success/pushout.prl

@@ -37,7 +37,6 @@ Thm PushoutToS1/Test0 : [
   (= (-> S1' S1) PushoutToS1 PushoutToS1)
 ] by [
   unfold PushoutToS1; // otherwise too easy
-  unfold S1'; // can be omitted once the great auto-unfolding is done
   refine eq/intro;
   fresh s1 -> refine fun/eq/lam;
   [ refine pushout/eq/pushout-rec ];