Basic experiments adding reduction to the type checker

3 files changed, 88 insertions, 45 deletions

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 10caa30..6b2ed58 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -181,18 +181,16 @@ axiomatization where
     \<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x"
 
 
-section \<open>Infrastructure\<close>
+section \<open>Type checking & inference\<close>
 
 ML_file \<open>lib.ML\<close>
 ML_file \<open>context_facts.ML\<close>
 ML_file \<open>context_tactical.ML\<close>
 
-subsection \<open>Type-checking/inference\<close>
-
-\<comment> \<open>Rule attributes for the type-checker\<close>
+\<comment> \<open>Rule attributes for the typechecker\<close>
 named_theorems form and intr and comp
 
-\<comment> \<open>Defines elimination automation and the `elim` attribute\<close>
+\<comment> \<open>Elimination/induction automation and the `elim` attribute\<close>
 ML_file \<open>elimination.ML\<close>
 
 lemmas
@@ -203,7 +201,20 @@ lemmas
   [comp] = beta Sig_comp and
   [cong] = Pi_cong lam_cong Sig_cong
 
-\<comment> \<open>Type-checking\<close>
+\<comment> \<open>Subsumption rule\<close>
+lemma sub:
+  assumes "a: A" "A \<equiv> A'"
+  shows "a: A'"
+  using assms by simp
+
+\<comment> \<open>Basic substitution of definitional equalities\<close>
+ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
+ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
+
+\<comment> \<open>Term normalization, type checking & inference\<close>
 ML_file \<open>types.ML\<close>
 
 method_setup typechk =
@@ -214,14 +225,26 @@ method_setup known =
   \<open>Scan.succeed (K (CONTEXT_METHOD (
     CHEADGOAL o Types.known_ctac)))\<close>
 
-subsection \<open>Statement commands\<close>
+setup \<open>
+let val typechk = fn ctxt =>
+  NO_CONTEXT_TACTIC ctxt o Types.check_infer
+    (Simplifier.prems_of ctxt @ Context_Facts.known ctxt)
+in
+  map_theory_simpset (fn ctxt => ctxt
+    addSolver (mk_solver "" typechk))
+end
+\<close>
+
+
+section \<open>Statements and goals\<close>
 
 ML_file \<open>focus.ML\<close>
 ML_file \<open>elaboration.ML\<close>
 ML_file \<open>elaborated_statement.ML\<close>
 ML_file \<open>goals.ML\<close>
 
-subsection \<open>Proof methods\<close>
+
+section \<open>Proof methods\<close>
 
 named_theorems intro \<comment> \<open>Logical introduction rules\<close>
 
@@ -270,6 +293,7 @@ subsection \<open>Reflexivity\<close>
 named_theorems refl
 method refl = (rule refl)
 
+
 subsection \<open>Trivial proofs (modulo automatic discharge of side conditions)\<close>
 
 method_setup this =
@@ -278,16 +302,9 @@ method_setup this =
       (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts))
       facts))))\<close>
 
-subsection \<open>Rewriting\<close>
 
-\<comment> \<open>\<open>subst\<close> method\<close>
-ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
-ML_file \<open>eqsubst.ML\<close>
+subsection \<open>Rewriting\<close>
 
-\<comment> \<open>\<open>rewrite\<close> method\<close>
 consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
 
 lemma eta_expand:
@@ -315,20 +332,18 @@ ML_file \<open>~~/src/HOL/Library/cconv.ML\<close>
 ML_file \<open>rewrite.ML\<close>
 
 \<comment> \<open>\<open>reduce\<close> computes terms via judgmental equalities\<close>
-setup \<open>map_theory_simpset (fn ctxt =>
-  ctxt addSolver (mk_solver "" (fn ctxt' =>
-    NO_CONTEXT_TACTIC ctxt' o Types.check_infer (Simplifier.prems_of ctxt'))))\<close>
-
 method reduce uses add =
-  changed \<open>repeat_new \<open>(simp add: comp add | sub comp); typechk?\<close>\<close>
+  changed \<open>repeat_new \<open>(simp add: comp add | subst comp); typechk?\<close>\<close>
 
-subsection \<open>Congruence automation\<close>
+
+subsection \<open>Congruence relations\<close>
 
 consts "rhs" :: \<open>'a\<close> ("..")
 
 ML_file \<open>congruence.ML\<close>
 
-subsection \<open>Implicits\<close>
+
+section \<open>Implicits\<close>
 
 text \<open>
   \<open>?\<close> is used to mark implicit arguments in definitions, while \<open>{}\<close> is expanded
@@ -364,7 +379,8 @@ translations
 
 translations "\<lambda>x. b" \<leftharpoondown> "\<lambda>x: A. b"
 
-subsection \<open>Lambda coercion\<close>
+
+section \<open>Lambda coercion\<close>
 
 \<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
 abbreviation (input) lambda :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close>
@@ -389,7 +405,7 @@ Lemma refine_codomain:
     "f: \<Prod>x: A. B x"
     "\<And>x. x: A \<Longrightarrow> f `x: C x"
   shows "f: \<Prod>x: A. C x"
-  by (subst eta_exp)
+  by (rewrite eta_exp)
 
 Lemma lift_universe_codomain:
   assumes "A: U i" "f: A \<rightarrow> U j"
@@ -463,12 +479,12 @@ lemma
 Lemma id_left [comp]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f"
-  by (subst eta_exp[of f]) (reduce, rule eta)
+  by (rewrite eta_exp[of f]) (reduce, rule eta)
 
 Lemma id_right [comp]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
-  by (subst eta_exp[of f]) (reduce, rule eta)
+  by (rewrite eta_exp[of f]) (reduce, rule eta)
 
 lemma id_U [type]:
   "id (U i): U i \<rightarrow> U i"
@@ -494,7 +510,7 @@ Lemma fst_comp [comp]:
 Lemma snd_type [type]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
   shows "snd A B: \<Prod>p: \<Sum>x: A. B x. B (fst A B p)"
-  unfolding snd_def by typechk reduce
+  unfolding snd_def by typechk
 
 Lemma snd_comp [comp]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML
index 31d5126..5ae8c73 100644
--- a/spartan/core/eqsubst.ML
+++ b/spartan/core/eqsubst.ML
@@ -430,12 +430,12 @@ val _ =
       Method.setup \<^binding>\<open>sub\<close>
         (parser >> (fn ((asm, occs), inthms) => fn ctxt => SIMPLE_METHOD' (
           (if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
-        "single-step substitution" #>
+        "single-step substitution" (* #>
       Method.setup \<^binding>\<open>subst\<close>
         (parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD (
           CHEADGOAL o SIDE_CONDS 0
             ((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms)))))
-        "single-step substitution with automatic discharge of side conditions"
+        "single-step substitution with automatic discharge of side conditions" *)
     )
   end
 
diff --git a/spartan/core/types.ML b/spartan/core/types.ML
index 70e5057..67918b9 100644
--- a/spartan/core/types.ML
+++ b/spartan/core/types.ML
@@ -43,42 +43,69 @@ fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
       if Lib.no_vars concl orelse
         (Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl))
       then
-        let val ths = known ctxt @ map (Simplifier.norm_hhf ctxt) facts
+        let val ths = known ctxt @ facts
         in st |>
           (assume_tac ctxt ORELSE' resolve_tac ctxt ths THEN_ALL_NEW K no_tac) i
         end
       else Seq.empty
     end)
 
-(*Simple bidirectional typing tactic, with some nondeterminism from backtracking
-  search over input facts. The current implementation does not perform any
-  normalization.*)
+(*Simple bidirectional typing tactic with some backtracking search over input
+  facts.*)
 fun check_infer_step facts i (ctxt, st) =
   let
-    val tac = SUBGOAL (fn (goal, i) =>
+    val refine_tac = SUBGOAL (fn (goal, i) =>
       if Lib.rigid_typing_concl goal
       then
-        let val net = Tactic.build_net (
-          map (Simplifier.norm_hhf ctxt) facts
-          @(cond ctxt)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>)
-          @(map #1 (Elim.rules ctxt)))
-        in (resolve_from_net_tac ctxt net) i end
+        let
+          val net = Tactic.build_net (
+            map (Simplifier.norm_hhf ctxt) facts
+            @(cond ctxt)
+            @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)
+            @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>)
+            @(map #1 (Elim.rules ctxt)))
+        in resolve_from_net_tac ctxt net i end
       else no_tac)
 
+    val sub_tac = SUBGOAL (fn (goal, i) =>
+      let val concl = Logic.strip_assums_concl goal in
+      if Lib.is_typing concl
+        andalso Lib.is_rigid (Lib.term_of_typing concl)
+        andalso Lib.no_vars (Lib.type_of_typing concl)
+      then
+        (resolve_tac ctxt @{thms sub}
+        THEN' SUBGOAL (fn (_, i) =>
+          NO_CONTEXT_TACTIC ctxt (check_infer facts i))
+        THEN' compute_tac ctxt facts
+        THEN_ALL_NEW K no_tac) i
+      else no_tac end)
+
     val ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*)
   in
-    TACTIC_CONTEXT ctxt' (tac i st)
+    TACTIC_CONTEXT ctxt' (
+      (NO_CONTEXT_TACTIC ctxt' o known_ctac facts
+      ORELSE' refine_tac
+      ORELSE' sub_tac) i st)
   end
 
-fun check_infer facts i (cst as (_, st)) =
+and check_infer facts i (cst as (_, st)) =
   let
-    val ctac = known_ctac facts CORELSE' check_infer_step facts
+    val ctac = check_infer_step facts
   in
     cst |> (ctac i CTHEN
       CREPEAT_IN_RANGE i (Thm.nprems_of st - i) (CTRY o CREPEAT_ALL_NEW_FWD ctac))
   end
 
+and compute_tac ctxt facts =
+  let
+    val comps = Named_Theorems.get ctxt \<^named_theorems>\<open>comp\<close>
+    val ctxt' = ctxt addsimps comps
+  in
+    SUBGOAL (fn (_, i) =>
+      ((CHANGED o asm_simp_tac ctxt' ORELSE' EqSubst.eqsubst_tac ctxt [0] comps)
+      THEN_ALL_NEW SUBGOAL (fn (_, i) =>
+        NO_CONTEXT_TACTIC ctxt (check_infer facts i))) i)
+  end
+
 
 end