From d70ec302e58462beffa991695edd8c41692f2671 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?favonia=20=28Sai-hong=20=E3=82=B5=E3=82=A4=E3=83=9B?= =?UTF-8?q?=E3=83=B3=29?= Date: Sun, 19 Nov 2017 09:49:54 -0500 Subject: [PATCH] Match on values only. (#462) * Reduce and unfold terms before resolving match judgments. * Tweak pretty printer of judgments. * Remove now unnecessary unfolding in examples. --- src/redprl/refiner.fun | 22 +++++++++++++++++++--- src/redprl/refiner_misc.fun | 19 ++++++++++++++++--- src/redprl/sequent.sml | 2 +- test/success/hlevels.prl | 20 ++++++++++++-------- test/success/pushout.prl | 1 - 5 files changed, 48 insertions(+), 16 deletions(-) diff --git a/src/redprl/refiner.fun b/src/redprl/refiner.fun index adca7fe96..c991ce693 100644 --- a/src/redprl/refiner.fun +++ b/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: diff --git a/src/redprl/refiner_misc.fun b/src/redprl/refiner_misc.fun index e38ade93b..106e2db95 100644 --- a/src/redprl/refiner_misc.fun +++ b/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) diff --git a/src/redprl/sequent.sml b/src/redprl/sequent.sml index 7325f8df9..57c9b5c10 100644 --- a/src/redprl/sequent.sml +++ b/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) => diff --git a/test/success/hlevels.prl b/test/success/hlevels.prl index f6d111ec9..b8d09c035 100644 --- a/test/success/hlevels.prl +++ b/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. - lam x. `(@ ($ h x ($ f x) ($ g x)) i) + lam tyA, tyB, h, f, g. 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. `(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? - ( lam a, b. + 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. lam a, b. `(@ ($ (PropSet #l) tyA h1 a b ($ h1 a b) ($ h2 a b)) i) ]. // // This should be exactly like the one above: diff --git a/test/success/pushout.prl b/test/success/pushout.prl index eb82d4326..6ec57a23a 100644 --- a/test/success/pushout.prl +++ b/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 ];