From 3bcaf5d1c40b513f8e4590f7d38d3eef8393092e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 16 Jul 2020 16:46:09 +0200
Subject: Checkpoint. THIS BUILD WILL FAIL

---
 spartan/core/typechecking.ML | 67 +++++++++++++++++++++++++++++++++++---------
 1 file changed, 53 insertions(+), 14 deletions(-)

(limited to 'spartan/core/typechecking.ML')

diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
index 437a2dc..13ca440 100644
--- a/spartan/core/typechecking.ML
+++ b/spartan/core/typechecking.ML
@@ -1,7 +1,7 @@
 (*  Title:      typechecking.ML
     Author:     Joshua Chen
 
-Type information and typechecking infrastructure.
+Type information and type-checking infrastructure.
 *)
 
 structure Types: sig
@@ -11,11 +11,12 @@ val types: Proof.context -> term -> thm list
 val put_type: thm -> Proof.context -> Proof.context
 val put_types: thm list -> Proof.context -> Proof.context
 
-val check: Proof.context -> thm -> int -> tactic
-val infer: Proof.context -> thm -> int -> tactic
+val known_ctac: thm list -> int -> context_tactic
+val check_infer: thm list -> int -> context_tactic
 
 end = struct
 
+
 (* Context data *)
 
 structure Data = Generic_Data (
@@ -32,22 +33,60 @@ fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing))
 fun put_types typings = foldr1 (op o) (map put_type typings)
 
 
-(* Checking and inference *)
-
-local
+(* Context tactics for type-checking *)
 
-fun checkable prop = Lib.is_typing prop
-  andalso not (exists_subterm is_Var (Lib.type_of_typing prop))
+(*For debugging*)
+structure Probe = Proof_Data (
+  type T = int
+  val init = K 0
+)
 
+(*Solves goals without metavariables and type inference problems by resolving
+  with facts or assumption from inline premises.*)
+fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
+  TACTIC_CONTEXT ctxt
+    let val concl = Logic.strip_assums_concl goal in
+      if Lib.no_vars concl orelse
+        (Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl))
+      then
+        let val ths = facts
+          (*FIXME: Shouldn't pull nameless facts directly from context*)
+          @ map fst (Facts.props (Proof_Context.facts_of ctxt))
+        in (resolve_tac ctxt ths i ORELSE assume_tac ctxt i) st end
+      else Seq.empty
+    end)
+
+(*Simple bidirectional typing tactic, with some nondeterminism from backtracking
+  search over arbitrary `typechk` rules. The current implementation does not
+  perform any normalization.*)
+local
+  fun check_infer_step facts i (ctxt, st) =
+    let
+      val tac = SUBGOAL (fn (goal, i) =>
+        if Lib.rigid_typing_concl goal
+        then
+          let val net = Tactic.build_net (facts
+            (*MAYBE FIXME: Remove `typechk` from this list, and instead perform
+              definitional unfolding to (w?)hnf.*)
+            @(Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>)
+            @(Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>)
+            @(map #1 (Elim.rules ctxt)))
+          in (resolve_from_net_tac ctxt net) i end
+        else no_tac)
+      val ctxt' = Probe.map (fn i => i + 1) ctxt
+    in
+      TACTIC_CONTEXT ctxt' (tac i st)
+    end
 in
 
-fun check ctxt rule = Subgoal.FOCUS_PREMS (
-  fn {context = goal_ctxt, prems, concl, ...} => no_tac) ctxt
-
-fun infer ctxt rule = Subgoal.FOCUS_PREMS (
-  fn {context = goal_ctxt, prems, concl, ...} => no_tac) ctxt
+fun check_infer facts =
+  let val probe = K (print_ctac (Int.toString o Probe.get))
+  in
+    CREPEAT_ALL_NEW_FWD (
+      probe CTHEN' known_ctac facts
+      CORELSE' probe CTHEN' check_infer_step facts)
+  end
 
 end
 
-
 end
-- 
cgit v1.2.3