diff options
author | Josh Chen | 2021-06-23 16:26:23 +0100 |
---|---|---|
committer | Josh Chen | 2021-06-23 16:26:23 +0100 |
commit | 0085798a86a35e2430a97289e894724f688db435 (patch) | |
tree | db1662a5805917c6627963578f074dc226b4b06a /mltt/core/lib.ML | |
parent | 1928649fd490d50d1e05fef6cbb22ca38d81cbe5 (diff) |
1. Put universe level parameters first in automatic term definitions. 2. Add debugging to typechecker
Diffstat (limited to 'mltt/core/lib.ML')
-rw-r--r-- | mltt/core/lib.ML | 14 |
1 files changed, 14 insertions, 0 deletions
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 |