aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--HoTT_Base.thy38
-rw-r--r--Prod.thy58
-rw-r--r--typing.ML205
3 files changed, 237 insertions, 64 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index e74ef31..ed8c18b 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,11 +1,11 @@
(********
Isabelle/HoTT: Foundational definitions and notation
-Jan 2019
+Feb 2019
This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
Among other things, it:
-* Sets up object-level type inference functionality (via typing.ML).
+* Calls the setup of object-level type inference functionality.
* Defines the universe hierarchy and its governing rules.
* Defines named theorems for later use by proof methods.
@@ -13,19 +13,49 @@ Among other things, it:
theory HoTT_Base
imports Pure
+keywords "assume_type" "assume_types" :: thy_decl
begin
section \<open>Terms and typing\<close>
-declare[[eta_contract=false]]
-
typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
judgment has_type :: "[t, t] \<Rightarrow> prop" ("(3_:/ _)")
+section \<open>Setup non-core logic functionality\<close>
+
+declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
+
+text \<open>The following file sets up type assumption and inference functionality.\<close>
+
ML_file "typing.ML"
+ML \<open>
+val _ =
+ let
+ fun store_typing ctxt = Typing.put_declared_typing o (Syntax.read_prop ctxt)
+ in
+ Outer_Syntax.local_theory
+ @{command_keyword "assume_type"}
+ "Declare typing assumptions"
+ (Parse.prop >>
+ (fn prop => fn lthy => Local_Theory.background_theory (store_typing lthy prop) lthy))
+ end
+
+val _ =
+ let
+ val parser = Parse.and_list (Parse.prop)
+ fun store_typings ctxt = fold (Typing.put_declared_typing o (Syntax.read_prop ctxt))
+ in
+ Outer_Syntax.local_theory
+ @{command_keyword "assume_types"}
+ "Declare typing assumptions"
+ (parser >>
+ (fn props => fn lthy => Local_Theory.background_theory (store_typings lthy props) lthy))
+ end
+\<close>
+
section \<open>Universes\<close>
typedecl ord \<comment> \<open>Type of meta-numerals\<close>
diff --git a/Prod.thy b/Prod.thy
index 0de7d89..ce785d6 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -1,6 +1,6 @@
(********
Isabelle/HoTT: Dependent product (dependent function)
-Jan 2019
+Feb 2019
********)
@@ -20,13 +20,13 @@ axiomatization
syntax
"_Prod" :: "[idt, t, t] \<Rightarrow> t" ("(3TT '(_: _')./ _)" 30)
"_Prod'" :: "[idt, t, t] \<Rightarrow> t" ("(3TT _: _./ _)" 30)
- "_lam" :: "[idt, t, t] \<Rightarrow> t" ("(3,\\ '(_: _')./ _)" 30)
- "_lam'" :: "[idt, t, t] \<Rightarrow> t" ("(3,\\ _: _./ _)" 30)
+ "_lam" :: "[idt, t, t] \<Rightarrow> t" ("(3\<lambda>'(_: _')./ _)" 30)
+ "_lam'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<lambda>_: _./ _)" 30)
translations
- "TT(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
- "TT x: A. B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
- ",\\(x: A). b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)"
- ",\\x: A. b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)"
+ "TT(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
+ "TT x: A. B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
+ "\<lambda>(x: A). b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)"
+ "\<lambda>x: A. b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)"
text \<open>
The syntax translations above bind the variable @{term x} in the expressions @{term B} and @{term b}.
@@ -40,22 +40,22 @@ where "A \<rightarrow> B \<equiv> TT(_: A). B"
axiomatization where
\<comment> \<open>Type rules\<close>
- Prod_form: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: U i\<rbrakk> \<Longrightarrow> TT x: A. B x: U i" and
+ Prod_form: "\<lbrakk>A: U i; B: A \<leadsto> U i\<rbrakk> \<Longrightarrow> TT x: A. B x: U i" and
- Prod_intro: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> ,\\x: A. b x: TT x: A. B x" and
+ Prod_intro: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: TT x: A. B x" and
Prod_elim: "\<lbrakk>f: TT x: A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and
- Prod_cmp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (,\\x: A. b x)`a \<equiv> b a" and
+ Prod_cmp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (\<lambda>x: A. b x)`a \<equiv> b a" and
- Prod_uniq: "f: TT x: A. B x \<Longrightarrow> ,\\x: A. f`x \<equiv> f" and
+ Prod_uniq: "f: TT x: A. B x \<Longrightarrow> \<lambda>x: A. f`x \<equiv> f" and
\<comment> \<open>Congruence rules\<close>
Prod_form_eq: "\<lbrakk>A: U i; B: A \<leadsto> U i; C: A \<leadsto> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk>
\<Longrightarrow> TT x: A. B x \<equiv> TT x: A. C x" and
- Prod_intro_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> ,\\x: A. b x \<equiv> ,\\x: A. c x"
+ Prod_intro_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x \<equiv> \<lambda>x: A. c x"
text \<open>
The Pure rules for \<open>\<equiv>\<close> only let us judge strict syntactic equality of object lambda expressions.
@@ -71,23 +71,23 @@ lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq
section \<open>Function composition\<close>
definition compose :: "[t, t, t] \<Rightarrow> t"
-where "compose A g f \<equiv> ,\\x: A. g`(f`x)"
+where "compose A g f \<equiv> \<lambda>x: A. g`(f`x)"
declare compose_def [comp]
syntax "_compose" :: "[t, t] \<Rightarrow> t" (infixr "o" 110)
-
parse_translation \<open>
-let fun compose_tr ctxt tms =
+let fun compose_tr ctxt [g, f] =
let
- val g :: f :: _ = tms |> map (Typing.tm_of_ptm ctxt)
+ val [g, f] = [g, f] |> map (Typing.prep_term @{context})
val dom =
case f of
Const ("Prod.lam", _) $ T $ _ => T
- | _ => (case Typing.get_typing f (Typing.typing_assms ctxt) of
+ | Const ("Prod.compose", _) $ T $ _ $ _ => T
+ | _ => (case Typing.get_typing ctxt f of
SOME (Const ("Prod.Prod", _) $ T $ _) => T
- | SOME _ => Exn.error "Can't compose with a non-function"
- | NONE => Exn.error "Cannot infer domain of composition: please state this explicitly")
+ | SOME t => (@{print} t; Exn.error "Can't compose with a non-function")
+ | NONE => Exn.error "Cannot infer domain of composition; please state this explicitly")
in
@{const compose} $ dom $ g $ f
end
@@ -96,16 +96,30 @@ in
end
\<close>
+text \<open>Pretty-printing switch for composition; hides domain type information.\<close>
+
+ML \<open>val pretty_compose = Attrib.setup_config_bool @{binding "pretty_compose"} (K true)\<close>
+
+print_translation \<open>
+let fun compose_tr' ctxt [A, g, f] =
+ if Config.get ctxt pretty_compose
+ then Syntax.const @{syntax_const "_compose"} $ g $ f
+ else Const ("compose", Syntax.read_typ ctxt "t \<Rightarrow> t \<Rightarrow> t") $ A $ g $ f
+in
+ [(@{const_syntax compose}, compose_tr')]
+end
+\<close>
+
lemma compose_assoc:
- assumes "A: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: TT x: C. D x"
+ assumes "A: U i" and "f: A \<rightarrow> B" and "g: B \<rightarrow> C" and "h: TT x: C. D x"
shows "compose A (compose B h g) f \<equiv> compose A h (compose A g f)"
by (derive lems: assms cong)
lemma compose_comp:
assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x"
- shows "(,\\x: B. c x) o (,\\x: A. b x) \<equiv> ,\\x: A. c (b x)"
+ shows "(\<lambda>x: B. c x) o (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)"
by (derive lems: assms cong)
-abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> ,\\x: A. x"
+abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x"
end
diff --git a/typing.ML b/typing.ML
index bfe8409..4bcb633 100644
--- a/typing.ML
+++ b/typing.ML
@@ -6,15 +6,96 @@ Functionality for object-level type inference.
********)
+(* Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on *)
+val trace = Attrib.setup_config_bool @{binding "trace"} (K false)
+
+(* ====================================== Helper functions ====================================== *)
+
+signature TYPING_LIB =
+sig
+ (* Lexical functions *)
+ val unmark: string -> string
+
+ (* General functions *)
+ val get_all_thms: Proof.context -> (string * thm) list
+ val find_thm: Proof.context -> string -> (string * thm) list
+
+ (* Get specific theorems *)
+ val get_this: Proof.context -> thm list
+ val get_assms: Proof.context -> thm list
+end
+
+structure Typing_Lib: TYPING_LIB =
+struct
+
+fun unmark s =
+ Lexicon.unmark_class s
+ handle Fail "unprefix" =>
+ Lexicon.unmark_type s
+ handle Fail "unprefix" =>
+ Lexicon.unmark_const s
+ handle Fail "unprefix" =>
+ Lexicon.unmark_fixed s
+ handle Fail "unprefix" =>
+ s
+
+fun name_and_thm (fact, thm) =
+ ((case fact of
+ Facts.Named ((name, _), _) => name
+ | Facts.Fact name => name),
+ thm)
+
+fun get_all_thms ctxt =
+ let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
+ in ref_thms |> (map name_and_thm)
+ end
+
+(* Search all visible theorems (including local assumptions) containing a given name *)
+fun find_thm ctxt name =
+ let val (_, ref_thms) =
+ Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
+ in
+ ref_thms |> (map name_and_thm)
+ end
+
+(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
+fun get_this ctxt =
+ Proof_Context.get_fact ctxt (Facts.named "local.this")
+ handle ERROR "Undefined fact: \"local.this\"" => (
+ if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
+ []
+ )
+
+(* Get all visible assumptions in the current proof scope.
+ This includes the facts introduced in the statement of the goal using "assumes",
+ as well as all facts introduced using "assume" that are visible in the current block.
+ *)
+val get_assms = Assumption.all_prems_of
+
+end
+
+(* ================================ Type inference functionality ================================ *)
+
signature TYPING =
sig
type jmt = term
+ val is_typing_jmt: term -> bool
val term_of_jmt: jmt -> term
val type_of_jmt: jmt -> term
+
+ val typing_this: Proof.context -> jmt list
val typing_assms: Proof.context -> jmt list
- val get_typing: term -> jmt list -> term option
- val get_global_typing: theory -> Proof.context -> term -> term option
- val tm_of_ptm: Proof.context -> term -> term
+ val typing_all: Proof.context -> jmt list
+
+ val get_typing_in: term -> jmt list -> term option
+ val get_local_typing: Proof.context -> term -> term option
+
+ val get_declared_typing: theory -> term -> term option
+ val put_declared_typing: term -> theory -> theory
+
+ val get_typing: Proof.context -> term -> term option
+
+ val prep_term: Proof.context -> term -> term
end
structure Typing: TYPING =
@@ -22,6 +103,10 @@ struct
type jmt = term
+(* Determine if a term is a typing judgment *)
+fun is_typing_jmt (@{const has_type} $ _ $ _) = true
+ | is_typing_jmt _ = false
+
(* Functions to extract a and A from propositions "a: A" *)
fun term_of_jmt (@{const has_type} $ t $ _) = t
| term_of_jmt _ = Exn.error "Not a typing judgment"
@@ -29,62 +114,106 @@ fun term_of_jmt (@{const has_type} $ t $ _) = t
fun type_of_jmt (@{const has_type} $ _ $ T) = T
| type_of_jmt _ = Exn.error "Not a typing judgment"
+(* Get typing assumptions in "this" *)
+fun typing_this ctxt = Typing_Lib.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt
+
(* Get the typing assumptions in the current context *)
-fun typing_assms ctxt =
- let
- fun is_typing_jmt (@{const has_type} $ _ $ _) = true
- | is_typing_jmt _ = false
- in
- Assumption.all_prems_of ctxt |> map Thm.prop_of |> filter is_typing_jmt
- end
+val typing_assms = Typing_Lib.get_assms #> map Thm.prop_of #> filter is_typing_jmt
-(* Search for a term typing in a list of judgments*)
-fun get_typing tm jmts =
+(* Get all visible typing judgments—Quick hack for now; should record them separately *)
+fun typing_all ctxt =
+ Typing_Lib.get_all_thms ctxt |> map (Thm.prop_of o snd) |> filter is_typing_jmt
+
+(* Search for a term typing in a list of judgments, and return the type if found.
+ --
+ The use of aconv_untyped as opposed to aconv is crucial here:
+ meta-level type inference is performed *after* syntax translation, which means that
+ the translation functions see an unannotated term "f" (in contrast to one annotated
+ e.g. "f::t") as having a blank type field.
+ Using aconv would result in no match ever being found for f, because any judgment
+ involving f records it together with its (non-blank) type field, e.g.
+ "Free ("f", "_")"
+ seen by the translation function, vs.
+ "Free ("f", "t")"
+ recorded in the typing judgment.
+*)
+fun get_typing_in tm jmts =
let val find_type =
fn jmt => if Term.aconv_untyped (tm, term_of_jmt jmt) then SOME (type_of_jmt jmt) else NONE
in get_first find_type jmts end
-(* Private storage space for global typing data *)
-structure Typing_Data = Theory_Data
+(* Search for typing in the local proof context (no global data).
+ We search the facts bound to "this" before searching the assumptions.
+ --
+ A previous version of this function passed the argument
+ (typing_this ctxt @ typing_assms ctxt)
+ to get_typing_in.
+ --
+ This version only evaluates successive lists if the search on the previous list was unsuccessful.
+*)
+fun get_local_typing ctxt tm =
+ case get_typing_in tm (typing_this ctxt) of
+ NONE => get_typing_in tm (typing_assms ctxt)
+ | res => res
+
+(* Storage space for declared typings *)
+structure Declared_Typings = Theory_Data
(
type T = term Symtab.table
val empty = Symtab.empty
val extend = I
-
- fun merge (tbl, tbl') =
- let
- val key_vals = map (Symtab.lookup_key tbl') (Symtab.keys tbl')
- val updates = map (fn SOME kv => Symtab.update kv) key_vals
- fun f u t = u t
- in fold f updates tbl end
+ val merge = K Symtab.empty
)
-
(* Accessor for the above data *)
-fun get_global_typing thy ctxt tm = Symtab.lookup (Typing_Data.get thy) (Syntax.string_of_term ctxt tm)
+fun get_declared_typing thy tm =
+ case tm of
+ (Free (v, _)) => Symtab.lookup (Declared_Typings.get thy) v
+ | _ => NONE
+
+(* Store new typing information for free variables only
+ (constants should have their types declared at the moment of definition).
+ End users should use the "typing" keyword instead.
+*)
+fun put_declared_typing jmt =
+ case jmt of
+ Const("HoTT_Base.has_type", _) $ term $ typing =>
+ (case term of
+ Free (v, _) => Declared_Typings.map (Symtab.update (v, typing))
+ | _ => Exn.error "Cannot declare typing assumption (not a free variable)")
+ | _ => Exn.error "Not a typing judgment"
+
+(* Get the typing of a term *)
+fun get_typing ctxt tm =
+ case get_local_typing ctxt tm of
+ NONE => get_declared_typing (Proof_Context.theory_of ctxt) tm
+ | res => res
-(* Convert a Pure pre-term to an unchecked Pure term *)
-fun tm_of_ptm ctxt ptm =
+(* Prepare a Pure pre-term, converting it partway to a (unchecked) term *)
+fun prep_term ctxt ptm =
let val ptm = Term_Position.strip_positions ptm
in
(case ptm of
- Const ("_constrain", _) $ Free (t, _) $ (Const ("\<^type>fun", _) $ Const(n1, _) $ Const (n2, _)) =>
+ Const ("_constrain", _) $ Free (t, _) $
+ (Const ("\<^type>fun", _) $ Const(typ1, _) $ Const (typ2, _)) =>
let
- val typ1 = unprefix "\<^type>" n1
- val typ2 = unprefix "\<^type>" n2
+ val typ1 = Lexicon.unmark_type typ1
+ val typ2 = Lexicon.unmark_type typ2
val typ = typ1 ^ "\<Rightarrow>" ^ typ2 |> Syntax.read_typ ctxt
in Free (t, typ) end
- | Const ("_constrain", _) $ Free (t, _) $ Const (T, _) =>
- Free (t, Syntax.read_typ ctxt (unprefix "\<^type>" T))
+ | Const ("_constrain", _) $ t $ Const (typ, _) =>
+ let
+ val T = Syntax.read_typ ctxt (Lexicon.unmark_type typ)
+ in
+ case t of
+ Free (s, _) => Free (s, T)
+ | Const (s, _) => Const (Lexicon.unmark_const s, T)
+ | _ => Exn.error "Unimplemented term constraint handler"
+ end
| ptm1 $ ptm2 =>
- (tm_of_ptm ctxt ptm1) $ (tm_of_ptm ctxt ptm2)
- | Const (t, T) =>
- let val t' =
- unprefix "\<^const>" t handle Fail "unprefix" =>
- unprefix "\<^type>" t handle Fail "unprefix" =>
- t
- in Const (t', T) end
+ (prep_term ctxt ptm1) $ (prep_term ctxt ptm2)
| Abs (t, T, ptm') =>
- Abs (t, T, tm_of_ptm ctxt ptm')
+ Abs (t, T, prep_term ctxt ptm')
+ | Const (t, T) => Const (Typing_Lib.unmark t, T)
| t => t)
end