From 0085798a86a35e2430a97289e894724f688db435 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 23 Jun 2021 16:26:23 +0100
Subject: 1. Put universe level parameters first in automatic term definitions.
 2. Add debugging to typechecker

---
 mltt/core/MLTT.thy |  3 ---
 mltt/core/goals.ML |  9 +++++----
 mltt/core/lib.ML   | 14 ++++++++++++++
 mltt/core/types.ML |  6 +++---
 4 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy
index cd8ae42..5888a90 100644
--- a/mltt/core/MLTT.thy
+++ b/mltt/core/MLTT.thy
@@ -137,9 +137,6 @@ translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (fn x. B)"
 abbreviation Prod (infixl "\<times>" 60)
   where "A \<times> B \<equiv> \<Sum>_: A. B"
 
-abbreviation "and" (infixl "\<and>" 60)
-  where "A \<and> B \<equiv> A \<times> B"
-
 axiomatization where
   SigF: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and
 
diff --git a/mltt/core/goals.ML b/mltt/core/goals.ML
index 7d52495..d69c800 100644
--- a/mltt/core/goals.ML
+++ b/mltt/core/goals.ML
@@ -82,7 +82,7 @@ fun define_proof_term name (local_name, [th]) lthy =
           val concl_vars = Lib.collect_subterms is_Var
             (Lib.term_of_typing concl)
 
-          val params = inter Term.aconv concl_vars prems_vars
+          val params = sort (uncurry Lib.lvl_order) (inter Term.aconv concl_vars prems_vars)
 
           val prf_tm = fold_rev lambda params (Lib.term_of_typing concl)
 
@@ -197,10 +197,11 @@ fun theorem spec descr =
             long descr NONE (K I) binding includes elems concl))
 
 fun definition spec descr =
-  Outer_Syntax.local_theory_to_proof' spec "definition via proof"
+  Outer_Syntax.local_theory_to_proof' spec "definition with explicit type checking obligation"
     ((long_statement || short_statement) >>
-      (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd
-        true long descr NONE (K I) binding includes elems concl))
+      (fn (long, binding, includes, elems, concl) =>
+        schematic_theorem_cmd
+          true long descr NONE (K I) binding includes elems concl))
 
 in
 
diff --git a/mltt/core/lib.ML b/mltt/core/lib.ML
index e43ad98..f15daf6 100644
--- a/mltt/core/lib.ML
+++ b/mltt/core/lib.ML
@@ -39,6 +39,7 @@ val collect_subterms: (term -> bool) -> term -> term list
 
 (*Orderings*)
 val subterm_order: term -> term -> order
+val lvl_order: term -> term -> order
 val cond_order: order -> order -> order
 
 end = struct
@@ -187,6 +188,19 @@ fun subterm_order t1 t2 =
   else if has_subterm [t2] t1 then GREATER
   else EQUAL
 
+fun lvl_order t1 t2 =
+  let val _ = @{print} (fastype_of t1) in
+  case fastype_of t1 of
+    Type (\<^type_name>\<open>lvl\<close>, _) => (case fastype_of t2 of
+                          Type (\<^type_name>\<open>lvl\<close>, _) => EQUAL
+                        | Type (_, _) => LESS
+                        | _ => EQUAL)
+  | Type (_, _)     => (case fastype_of t2 of
+                          Type (\<^type_name>\<open>lvl\<close>, _) => GREATER
+                        | _ => EQUAL)
+  | _ => EQUAL
+  end
+
 fun cond_order o1 o2 = case o1 of EQUAL => o2 | _ => o1
 
 
diff --git a/mltt/core/types.ML b/mltt/core/types.ML
index 5e0d484..d0b1137 100644
--- a/mltt/core/types.ML
+++ b/mltt/core/types.ML
@@ -83,9 +83,9 @@ fun check_infer_step facts i (ctxt, st) =
     val ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*)
   in
     TACTIC_CONTEXT ctxt' (
-      (NO_CONTEXT_TACTIC ctxt' o known_ctac facts
-      ORELSE' refine_tac
-      ORELSE' sub_tac) i st)
+      ((NO_CONTEXT_TACTIC ctxt' o known_ctac facts THEN' K (debug_tac ctxt' "after `known`"))
+      ORELSE' (refine_tac THEN' K (debug_tac ctxt' "after `refine`"))
+      ORELSE' (sub_tac THEN' K (debug_tac ctxt' "after `sub`"))) i st)
   end
 
 and check_infer facts i (cst as (_, st)) =
-- 
cgit v1.2.3