diff options
| -rw-r--r-- | mltt/core/MLTT.thy | 3 | ||||
| -rw-r--r-- | mltt/core/goals.ML | 9 | ||||
| -rw-r--r-- | mltt/core/lib.ML | 14 | ||||
| -rw-r--r-- | 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)) = |