diff options
Diffstat (limited to '')
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | hott/Equivalence.thy | 23 | ||||
| -rw-r--r-- | hott/Identity.thy | 82 | ||||
| -rw-r--r-- | spartan/core/Spartan.thy | 2 | ||||
| -rw-r--r-- | spartan/core/elaborated_expression.ML | 402 | ||||
| -rw-r--r-- | spartan/core/elaboration.ML | 76 | ||||
| -rw-r--r-- | spartan/core/goals.ML | 125 | ||||
| -rw-r--r-- | spartan/core/lib.ML | 37 | ||||
| -rw-r--r-- | spartan/core/typechecking.ML | 57 |
9 files changed, 659 insertions, 146 deletions
@@ -1,4 +1,5 @@ *~ +*.bak \#*.thy# \#*.ML# diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index d976677..d844b59 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -33,13 +33,16 @@ Lemma (derive) hsym: "g: \<Prod>x: A. B x" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" - shows "H: f ~ g \<Longrightarrow> g ~ f" - unfolding homotopy_def - apply intro - apply (rule pathinv) - \<guillemotright> by (elim H) - \<guillemotright> by typechk - done + "H: f ~ g" + shows "g ~ f" +unfolding homotopy_def +proof intro + fix x assume "x: A" then have "H x: f x = g x" + using \<open>H:_\<close>[unfolded homotopy_def] + \<comment> \<open>this should become unnecessary when definitional unfolding is implemented\<close> + by typechk + thus "g x = f x" by (rule pathinv) fact +qed typechk Lemma (derive) htrans: assumes @@ -71,9 +74,9 @@ Lemma (derive) commute_homotopy: assumes "A: U i" "B: U i" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" "f: A \<rightarrow> B" "g: A \<rightarrow> B" - "H: homotopy A (fn _. B) f g" + "H: f ~ g" shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)" \<comment> \<open>Need this assumption unfolded for typechecking\<close> supply assms(8)[unfolded homotopy_def] @@ -94,7 +97,7 @@ Corollary (derive) commute_homotopy': "A: U i" "x: A" "f: A \<rightarrow> A" - "H: homotopy A (fn _. A) f (id A)" + "H: f ~ (id A)" shows "H (f x) = f [H x]" oops diff --git a/hott/Identity.thy b/hott/Identity.thy index 29ce26a..728537c 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -135,14 +135,14 @@ lemmas section \<open>Basic propositional equalities\<close> Lemma (derive) refl_pathcomp: - assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" + assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(refl x) \<bullet> p = p" apply (eq p) apply (reduce; intro) done Lemma (derive) pathcomp_refl: - assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" + assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \<bullet> (refl y) = p" apply (eq p) apply (reduce; intro) @@ -166,24 +166,24 @@ Lemma ru_refl [comp]: unfolding pathcomp_refl_def by reduce Lemma (derive) inv_pathcomp: - assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" + assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\<inverse> \<bullet> p = refl y" by (eq p) (reduce; intro) Lemma (derive) pathcomp_inv: - assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" + assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \<bullet> p\<inverse> = refl x" by (eq p) (reduce; intro) Lemma (derive) pathinv_pathinv: - assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" + assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\<inverse>\<inverse> = p" by (eq p) (reduce; intro) Lemma (derive) pathcomp_assoc: assumes "A: U i" "x: A" "y: A" "z: A" "w: A" - "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" "r: z =\<^bsub>A\<^esub> w" + "p: x = y" "q: y = z" "r: z = w" shows "p \<bullet> (q \<bullet> r) = p \<bullet> q \<bullet> r" apply (eq p) focus prems vars x p @@ -203,7 +203,7 @@ Lemma (derive) ap: "A: U i" "B: U i" "x: A" "y: A" "f: A \<rightarrow> B" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "f x = f y" by (eq p) intro @@ -222,7 +222,7 @@ Lemma (derive) ap_pathcomp: "A: U i" "B: U i" "x: A" "y: A" "z: A" "f: A \<rightarrow> B" - "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" + "p: x = y" "q: y = z" shows "f[p \<bullet> q] = f[p] \<bullet> f[q]" apply (eq p) @@ -237,7 +237,7 @@ Lemma (derive) ap_pathinv: "A: U i" "B: U i" "x: A" "y: A" "f: A \<rightarrow> B" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "f[p\<inverse>] = f[p]\<inverse>" by (eq p) (reduce; intro) @@ -248,7 +248,7 @@ Lemma (derive) ap_funcomp: "A: U i" "B: U i" "C: U i" "x: A" "y: A" "f: A \<rightarrow> B" "g: B \<rightarrow> C" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "(g \<circ> f)[p] = g[f[p]]" apply (eq p) \<guillemotright> by reduce @@ -256,7 +256,7 @@ Lemma (derive) ap_funcomp: done Lemma (derive) ap_id: - assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" + assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(id A)[p] = p" apply (eq p) \<guillemotright> by reduce @@ -271,7 +271,7 @@ Lemma (derive) transport: "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "P x \<rightarrow> P y" by (eq p) intro @@ -308,7 +308,7 @@ Lemma (derive) transport_left_inv: "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)" by (eq p) (reduce; refl) @@ -317,7 +317,7 @@ Lemma (derive) transport_right_inv: "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "(trans P p) \<circ> (trans P p\<inverse>) = id (P y)" by (eq p) (reduce; intro) @@ -327,7 +327,7 @@ Lemma (derive) transport_pathcomp: "\<And>x. x: A \<Longrightarrow> P x: U i" "x: A" "y: A" "z: A" "u: P x" - "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" + "p: x = y" "q: y = z" shows "trans P q (trans P p u) = trans P (p \<bullet> q) u" apply (eq p) focus prems vars x p @@ -342,7 +342,7 @@ Lemma (derive) transport_compose_typefam: "\<And>x. x: B \<Longrightarrow> P x: U i" "f: A \<rightarrow> B" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" "u: P (f x)" shows "trans (fn x. P (f x)) p u = trans P f[p] u" by (eq p) (reduce; intro) @@ -355,7 +355,7 @@ Lemma (derive) transport_function_family: "f: \<Prod>x: A. P x \<rightarrow> Q x" "x: A" "y: A" "u: P x" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "trans Q p ((f x) u) = (f y) (trans P p u)" by (eq p) (reduce; intro) @@ -363,7 +363,7 @@ Lemma (derive) transport_const: assumes "A: U i" "B: U i" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "\<Prod>b: B. trans (fn _. B) p b = b" by (intro, eq p) (reduce; intro) @@ -384,7 +384,7 @@ Lemma (derive) pathlift: "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" "u: P x" shows "<x, u> = <y, trans P p u>" by (eq p) (reduce; intro) @@ -409,7 +409,7 @@ Lemma (derive) pathlift_fst: "\<And>x. x: A \<Longrightarrow> P x: U i" "x: A" "y: A" "u: P x" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "fst[lift P p u] = p" apply (eq p) \<guillemotright> by reduce @@ -425,7 +425,7 @@ Lemma (derive) apd: "\<And>x. x: A \<Longrightarrow> P x: U i" "f: \<Prod>x: A. P x" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "trans P p (f x) = f y" by (eq p) (reduce; intro) @@ -448,7 +448,7 @@ Lemma (derive) apd_ap: "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A" "y: A" - "p: x =\<^bsub>A\<^esub> y" + "p: x = y" shows "apd f p = trans_const B p (f x) \<bullet> f[p]" by (eq p) (reduce; intro) @@ -457,10 +457,9 @@ section \<open>Whiskering\<close> Lemma (derive) right_whisker: assumes "A: U i" "a: A" "b: A" "c: A" - shows "\<lbrakk>p: a = b; q: a = b; r: b = c; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow> p \<bullet> r = q \<bullet> r" - \<comment> \<open>TODO: In the above we need to annotate the type of \<alpha> with the type `a = b` - in order for the `eq` method to work correctly. This should be fixed with a - pre-proof elaborator.\<close> + and "p: a = b" "q: a = b" "r: b = c" + and "\<alpha>: p = q" + shows "p \<bullet> r = q \<bullet> r" apply (eq r) focus prems vars x s t proof - @@ -473,7 +472,9 @@ Lemma (derive) right_whisker: Lemma (derive) left_whisker: assumes "A: U i" "a: A" "b: A" "c: A" - shows "\<lbrakk>p: b = c; q: b = c; r: a = b; \<alpha>: p =\<^bsub>b = c\<^esub> q\<rbrakk> \<Longrightarrow> r \<bullet> p = r \<bullet> q" + and "p: b = c" "q: b = c" "r: a = b" + and "\<alpha>: p = q" + shows "r \<bullet> p = r \<bullet> q" apply (eq r) focus prems prms vars x s t proof - @@ -495,15 +496,13 @@ translations "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha>" \<leftharpoondown> "CONST left_whisker A a b c p q r \<alpha>" Lemma whisker_refl [comp]: - assumes "A: U i" "a: A" "b: A" - shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow> - \<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>" + assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\<alpha>: p = q" + shows "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>" unfolding right_whisker_def by reduce Lemma refl_whisker [comp]: - assumes "A: U i" "a: A" "b: A" - shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p = q\<rbrakk> \<Longrightarrow> - (refl a) \<bullet>\<^sub>l\<^bsub>b\<^esub> \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>" + assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\<alpha>: p = q" + shows "(refl a) \<bullet>\<^sub>l\<^bsub>b\<^esub> \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>" unfolding left_whisker_def by reduce method left_whisker = (rule left_whisker) @@ -524,20 +523,22 @@ begin Lemma (derive) horiz_pathcomp: notes assums - shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> ?prf \<alpha> \<beta>: p \<bullet> r = q \<bullet> s" + assumes "\<alpha>: p = q" "\<beta>: r = s" + shows "p \<bullet> r = q \<bullet> s" proof (rule pathcomp) - show "\<alpha>: p = q \<Longrightarrow> p \<bullet> r = q \<bullet> r" by right_whisker - show "\<beta>: r = s \<Longrightarrow> .. = q \<bullet> s" by left_whisker + show "p \<bullet> r = q \<bullet> r" by right_whisker fact + show ".. = q \<bullet> s" by left_whisker fact qed typechk text \<open>A second horizontal composition:\<close> Lemma (derive) horiz_pathcomp': notes assums - shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> ?prf \<alpha> \<beta>: p \<bullet> r = q \<bullet> s" + assumes "\<alpha>: p = q" "\<beta>: r = s" + shows "p \<bullet> r = q \<bullet> s" proof (rule pathcomp) - show "\<beta>: r = s \<Longrightarrow> p \<bullet> r = p \<bullet> s" by left_whisker - show "\<alpha>: p = q \<Longrightarrow> .. = q \<bullet> s" by right_whisker + show "p \<bullet> r = p \<bullet> s" by left_whisker fact + show ".. = q \<bullet> s" by right_whisker fact qed typechk notation horiz_pathcomp (infix "\<star>" 121) @@ -545,7 +546,8 @@ notation horiz_pathcomp' (infix "\<star>''" 121) Lemma (derive) horiz_pathcomp_eq_horiz_pathcomp': notes assums - shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> \<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>" + assumes "\<alpha>: p = q" "\<beta>: r = s" + shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>" unfolding horiz_pathcomp_def horiz_pathcomp'_def apply (eq \<alpha>, eq \<beta>) focus vars p apply (eq p) diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 2c7216e..11bdc2b 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -215,6 +215,8 @@ method_setup known = subsection \<open>Statement commands\<close> ML_file \<open>focus.ML\<close> +ML_file \<open>elaboration.ML\<close> +ML_file \<open>elaborated_expression.ML\<close> ML_file \<open>goals.ML\<close> subsection \<open>Proof methods\<close> diff --git a/spartan/core/elaborated_expression.ML b/spartan/core/elaborated_expression.ML new file mode 100644 index 0000000..49b7758 --- /dev/null +++ b/spartan/core/elaborated_expression.ML @@ -0,0 +1,402 @@ +(* Title: elaborated_expression.ML + Author: Joshua Chen + +A modification of parts of ~~/Pure/Isar/expression.ML to incorporate elaboration +into the assumptions mechanism. + +Most of this file is copied verbatim from the original; the only changes are the +addition of `elaborate` and a modification to `activate_i`. +*) + +structure Elaborated_Expression = struct + +local + +open Element + +fun mk_type T = (Logic.mk_type T, []) +fun mk_term t = (t, []) +fun mk_propp (p, pats) = (Type.constraint propT p, pats) + +fun dest_type (T, []) = Logic.dest_type T +fun dest_term (t, []) = t +fun dest_propp (p, pats) = (p, pats) + +fun extract_inst (_, (_, ts)) = map mk_term ts +fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs)) + +fun extract_eqns es = map (mk_term o snd) es +fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs + +fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes + | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts + | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms + | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs + | extract_elem (Notes _) = [] + | extract_elem (Lazy_Notes _) = [] + +fun restore_elem (Fixes fixes, css) = + (fixes ~~ css) |> map (fn ((x, _, mx), cs) => + (x, cs |> map dest_type |> try hd, mx)) |> Fixes + | restore_elem (Constrains csts, css) = + (csts ~~ css) |> map (fn ((x, _), cs) => + (x, cs |> map dest_type |> hd)) |> Constrains + | restore_elem (Assumes asms, css) = + (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes + | restore_elem (Defines defs, css) = + (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines + | restore_elem (elem as Notes _, _) = elem + | restore_elem (elem as Lazy_Notes _, _) = elem + +fun prep (_, pats) (ctxt, t :: ts) = + let val ctxt' = Proof_Context.augment t ctxt + in + ((t, Syntax.check_props + (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats), + (ctxt', ts)) + end + +fun check cs ctxt = + let + val (cs', (ctxt', _)) = fold_map prep cs + (ctxt, Syntax.check_terms + (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs)) + in (cs', ctxt') end + +fun inst_morphism params ((prfx, mandatory), insts') ctxt = + let + (* parameters *) + val parm_types = map #2 params; + val type_parms = fold Term.add_tfreesT parm_types []; + + (* type inference *) + val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types; + val type_parms' = fold Term.add_tvarsT parm_types' []; + val checked = + (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts') + |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) + val (type_parms'', insts'') = chop (length type_parms') checked; + + (* context *) + val ctxt' = fold Proof_Context.augment checked ctxt; + val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt'; + val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt'; + + (* instantiation *) + val instT = + (type_parms ~~ map Logic.dest_type type_parms'') + |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); + val cert_inst = + ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'') + |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); + in + (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> + Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') + end; + +fun abs_def ctxt = + Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of; + +fun declare_elem prep_var (Element.Fixes fixes) ctxt = + let val (vars, _) = fold_map prep_var fixes ctxt + in ctxt |> Proof_Context.add_fixes vars |> snd end + | declare_elem prep_var (Element.Constrains csts) ctxt = + ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd + | declare_elem _ (Element.Assumes _) ctxt = ctxt + | declare_elem _ (Element.Defines _) ctxt = ctxt + | declare_elem _ (Element.Notes _) ctxt = ctxt + | declare_elem _ (Element.Lazy_Notes _) ctxt = ctxt; + +fun parameters_of thy strict (expr, fixed) = + let + val ctxt = Proof_Context.init_global thy; + + fun reject_dups message xs = + (case duplicates (op =) xs of + [] => () + | dups => error (message ^ commas dups)); + + fun parm_eq ((p1, mx1), (p2, mx2)) = + p1 = p2 andalso + (Mixfix.equal (mx1, mx2) orelse + error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^ + Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); + + fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); + fun params_inst (loc, (prfx, (Expression.Positional insts, eqns))) = + let + val ps = params_loc loc; + val d = length ps - length insts; + val insts' = + if d < 0 then + error ("More arguments than parameters in instantiation of locale " ^ + quote (Locale.markup_name ctxt loc)) + else insts @ replicate d NONE; + val ps' = (ps ~~ insts') |> + map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); + in (ps', (loc, (prfx, (Expression.Positional insts', eqns)))) end + | params_inst (loc, (prfx, (Expression.Named insts, eqns))) = + let + val _ = + reject_dups "Duplicate instantiation of the following parameter(s): " + (map fst insts); + val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => + if AList.defined (op =) ps p then AList.delete (op =) p ps + else error (quote p ^ " not a parameter of instantiated expression")); + in (ps', (loc, (prfx, (Expression.Named insts, eqns)))) end; + fun params_expr is = + let + val (is', ps') = fold_map (fn i => fn ps => + let + val (ps', i') = params_inst i; + val ps'' = distinct parm_eq (ps @ ps'); + in (i', ps'') end) is [] + in (ps', is') end; + + val (implicit, expr') = params_expr expr; + + val implicit' = map #1 implicit; + val fixed' = map (Variable.check_name o #1) fixed; + val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; + val implicit'' = + if strict then [] + else + let + val _ = + reject_dups + "Parameter(s) declared simultaneously in expression and for clause: " + (implicit' @ fixed'); + in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end; + in (expr', implicit'' @ fixed) end; + +fun parse_elem prep_typ prep_term ctxt = + Element.map_ctxt + {binding = I, + typ = prep_typ ctxt, + term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt), + pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt), + fact = I, + attrib = I}; + +fun prepare_stmt prep_prop prep_obtains ctxt stmt = + (case stmt of + Element.Shows raw_shows => + raw_shows |> (map o apsnd o map) (fn (t, ps) => + (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t, + map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) + | Element.Obtains raw_obtains => + let + val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt; + val obtains = prep_obtains thesis_ctxt thesis raw_obtains; + in map (fn (b, t) => ((b, []), [(t, [])])) obtains end); + +fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) => + let val x = Binding.name_of binding + in (binding, AList.lookup (op =) parms x, mx) end) + +fun finish_inst ctxt (loc, (prfx, inst)) = + let + val thy = Proof_Context.theory_of ctxt; + val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt; + in (loc, morph) end + +fun closeup _ _ false elem = elem + | closeup (outer_ctxt, ctxt) parms true elem = + let + (* FIXME consider closing in syntactic phase -- before type checking *) + fun close_frees t = + let + val rev_frees = + Term.fold_aterms (fn Free (x, T) => + if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I + else insert (op =) (x, T) | _ => I) t []; + in fold (Logic.all o Free) rev_frees t end; + + fun no_binds [] = [] + | no_binds _ = error "Illegal term bindings in context element"; + in + (case elem of + Assumes asms => Assumes (asms |> map (fn (a, propps) => + (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) + | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) => + let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t) + in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end)) + | e => e) + end + +fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes) + | finish_elem _ _ _ (Constrains _) = Constrains [] + | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms) + | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs) + | finish_elem _ _ _ (elem as Notes _) = elem + | finish_elem _ _ _ (elem as Lazy_Notes _) = elem + +fun check_autofix insts eqnss elems concl ctxt = + let + val inst_cs = map extract_inst insts; + val eqns_cs = map extract_eqns eqnss; + val elem_css = map extract_elem elems; + val concl_cs = (map o map) mk_propp (map snd concl); + (* Type inference *) + val (inst_cs' :: eqns_cs' :: css', ctxt') = + (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt; + val (elem_css', [concl_cs']) = chop (length elem_css) css'; + in + ((map restore_inst (insts ~~ inst_cs'), + map restore_eqns (eqnss ~~ eqns_cs'), + map restore_elem (elems ~~ elem_css'), + map fst concl ~~ concl_cs'), ctxt') + end + +fun prep_full_context_statement + parse_typ parse_prop + prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr + {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt + ctxt1 + = + let + val thy = Proof_Context.theory_of ctxt1 + val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import) + fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = + let + val params = map #1 (Locale.params_of thy loc) + val inst' = prep_inst ctxt (map #1 params) inst + val parm_types' = + params |> map (#2 #> Logic.varifyT_global #> + Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> + Type_Infer.paramify_vars) + val inst'' = map2 Type.constraint parm_types' inst' + val insts' = insts @ [(loc, (prfx, inst''))] + val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt + val inst''' = insts'' |> List.last |> snd |> snd + val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt + val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2 + handle ERROR msg => if null eqns then error msg else + (Locale.tracing ctxt1 + (msg ^ "\nFalling back to reading rewrites clause before activation."); + ctxt2) + val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns + val eqns' = (prep_eqns ctxt' o map snd) eqns + val eqnss' = [attrss ~~ eqns'] + val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt' + val rewrite_morph = eqns' + |> map (abs_def ctxt') + |> Variable.export_terms ctxt' ctxt + |> Element.eq_term_morphism (Proof_Context.theory_of ctxt) + |> the_default Morphism.identity + val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt + val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'] + in (i + 1, insts', eqnss', ctxt'') end + + fun prep_elem raw_elem ctxt = + let + val ctxt' = ctxt + |> Context_Position.set_visible false + |> declare_elem prep_var_elem raw_elem + |> Context_Position.restore_visible ctxt + val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem + in (elems', ctxt') end + + val fors = fold_map prep_var_inst fixed ctxt1 |> fst + val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd + val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2) + + fun prep_stmt elems ctxt = + check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt + + val _ = + if fixed_frees then () + else + (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of + [] => () + | frees => error ("Illegal free variables in expression: " ^ + commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))) + + val ((insts, _, elems', concl), ctxt4) = ctxt3 + |> init_body + |> fold_map prep_elem raw_elems + |-> prep_stmt + + (* parameters from expression and elements *) + val xs = maps (fn Element.Fixes fixes => map (Variable.check_name o #1) fixes | _ => []) + (Element.Fixes fors :: elems') + val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4 + val fors' = finish_fixes parms fors + val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors' + val deps = map (finish_inst ctxt5) insts + val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems' + in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end + +fun prep_inst prep_term ctxt parms (Expression.Positional insts) = + (insts ~~ parms) |> map + (fn (NONE, p) => Free (p, dummyT) + | (SOME t, _) => prep_term ctxt t) + | prep_inst prep_term ctxt parms (Expression.Named insts) = + parms |> map (fn p => + (case AList.lookup (op =) insts p of + SOME t => prep_term ctxt t | + NONE => Free (p, dummyT))) +fun parse_inst x = prep_inst Syntax.parse_term x +fun check_expr thy instances = map (apfst (Locale.check thy)) instances + +val read_full_context_statement = prep_full_context_statement + Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains + Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src + Proof_Context.read_var check_expr + +in + +fun prep_statement prep activate raw_elems raw_stmt ctxt = + let + val ((_, _, _, elems, concl), _) = + prep {strict = true, do_close = false, fixed_frees = true} + ([], []) I raw_elems raw_stmt ctxt; + val ctxt' = ctxt + |> Proof_Context.set_stmt true + |> fold_map activate elems |> #2 + |> Proof_Context.restore_stmt ctxt; + in (concl, ctxt') end + +fun elaborate ctxt assms = + let + fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env) + fun elab_fact (fact, xs) assums = + let val (subst, fact') = Elab.elab_stmt ctxt assums fact in + ((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums) + end + fun elab (b, facts) assums = + let val (facts', assums') = fold_map elab_fact facts assums + in ((b, facts'), assums') end + in + #1 (fold_map elab assms []) + end + +fun activate_i elem ctxt = + let + val elem' = + (case (map_ctxt_attrib o map) Token.init_assignable elem of + Defines defs => + Defines (defs |> map (fn ((a, atts), (t, ps)) => + ((Thm.def_binding_optional + (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts), + (t, ps)))) + | Assumes assms => Assumes (elaborate ctxt assms) + | e => e); + val ctxt' = Context.proof_map (init elem') ctxt; + in ((map_ctxt_attrib o map) Token.closure elem', ctxt') end + +fun activate raw_elem ctxt = + let val elem = raw_elem |> map_ctxt + {binding = I, + typ = I, + term = I, + pattern = I, + fact = Proof_Context.get_fact ctxt, + attrib = Attrib.check_src ctxt} + in activate_i elem ctxt end; + +fun read_statement x = prep_statement read_full_context_statement activate x + +end + +end
\ No newline at end of file diff --git a/spartan/core/elaboration.ML b/spartan/core/elaboration.ML new file mode 100644 index 0000000..27b6bb0 --- /dev/null +++ b/spartan/core/elaboration.ML @@ -0,0 +1,76 @@ +(* Title: elaboration.ML + Author: Joshua Chen + +Basic elaboration. +*) + +structure Elab: sig + +val elab: Proof.context -> cterm list -> term -> Envir.env +val elab_stmt: Proof.context -> cterm list -> term -> Envir.env * term + +end = struct + +(*Elaborate `tm` by solving the inference problem `tm: {}`, knowing `assums`, + which are fully elaborated, in `ctxt`. Return a substitution.*) +fun elab ctxt assums tm = + if Lib.no_vars tm + then Envir.init + else + let + val inf = Goal.init (Thm.cterm_of ctxt (Lib.typing_of_term tm)) + val res = Types.check_infer (map Thm.assume assums) 1 (ctxt, inf) + val tm' = + Thm.prop_of (#2 (Seq.hd (Seq.filter_results res))) + |> Lib.dest_prop |> Lib.term_of_typing + handle TERM ("dest_typing", [t]) => + let val typ = Logic.unprotect (Logic.strip_assums_concl t) + |> Lib.term_of_typing + in + error ("Elaboration of " ^ Syntax.string_of_term ctxt typ ^ " failed") + end + in + Seq.hd (Unify.matchers (Context.Proof ctxt) [(tm, tm')]) + end + handle Option => error + ("Elaboration of " ^ Syntax.string_of_term ctxt tm ^ " failed") + +(*Recursively elaborate a statement \<And>x ... y. \<lbrakk>...\<rbrakk> \<Longrightarrow> P x ... y by elaborating + only the types of typing judgments (in particular, does not look at judgmental + equality statements). Could also elaborate the terms of typing judgments, but + for now we assume that these are always free variables in all the cases we're + interested in.*) +fun elab_stmt ctxt assums stmt = + let + val stmt = Lib.dest_prop stmt + fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env) + in + if Lib.no_vars stmt orelse Lib.is_eq stmt then + (Envir.init, stmt) + else if Lib.is_typing stmt then + let + val typ = Lib.type_of_typing stmt + val subst = elab ctxt assums typ + in (subst, subst_term subst stmt) end + else + let + fun elab' assums (x :: xs) = + let + val (env, x') = elab_stmt ctxt assums x + val assums' = + if Lib.no_vars x' then Thm.cterm_of ctxt x' :: assums else assums + in env :: elab' assums' xs end + | elab' _ [] = [] + val (prems, concl) = Lib.decompose_goal ctxt stmt + val subst = fold (curry Envir.merge) (elab' assums prems) Envir.init + val prems' = map (Thm.cterm_of ctxt o subst_term subst) prems + val subst' = + if Lib.is_typing concl then + let val typ = Lib.type_of_typing concl + in Envir.merge (subst, elab ctxt (assums @ prems') typ) end + else subst + in (subst', subst_term subst' stmt) end + end + + +end diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index 4b53a7f..3e2bd09 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -15,27 +15,27 @@ val long_keyword = val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) - Binding.empty_atts -- - Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement - >> (fn ((binding, includes), (elems, concl)) => - (true, binding, includes, elems, concl)) + Binding.empty_atts + -- Scan.optional Parse_Spec.includes [] + -- Parse_Spec.long_statement >> + (fn ((binding, includes), (elems, concl)) => + (true, binding, includes, elems, concl)) val short_statement = - Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes - >> (fn ((shows, assumes), fixes) => + Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> + (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], - [Element.Fixes fixes, Element.Assumes assumes], - Element.Shows shows)) + [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows) + ) fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = let val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt val prems = Assumption.local_prems_of elems_ctxt ctxt - val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) - stmt elems_ctxt - in - case raw_stmt of - Element.Shows _ => + val stmt_ctxt = + fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt + in case raw_stmt + of Element.Shows _ => let val stmt' = Attrib.map_specs (map prep_att) stmt in (([], prems, stmt', NONE), stmt_ctxt) end | Element.Obtains raw_obtains => @@ -50,11 +50,8 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])] ||> Proof_Context.restore_stmt asms_ctxt - - val stmt' = [ - (Binding.empty_atts, - [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])]) - ] + val stmt' = + [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])] in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) @@ -65,23 +62,19 @@ fun define_proof_term name (local_name, [th]) lthy = let fun make_name_binding suffix local_name = let val base_local_name = Long_Name.base_name local_name - in - Binding.qualified_name - ((case base_local_name of - "" => name - | _ => base_local_name) - ^(case suffix of - SOME "prf" => "_prf" - | SOME "def" => "_def" - | _ => "")) + in Binding.qualified_name + ((case base_local_name of "" => name | _ => base_local_name) ^ + (case suffix + of SOME "prf" => "_prf" + | SOME "def" => "_def" + | _ => "")) end val (prems, concl) = (Logic.strip_assums_hyp (Thm.prop_of th), - Logic.strip_assums_concl (Thm.prop_of th)) + Logic.strip_assums_concl (Thm.prop_of th)) in - if not (Lib.is_typing concl) then - ([], lthy) + if not (Lib.is_typing concl) then ([], lthy) else let val prems_vars = distinct Term.aconv (flat (map (Lib.collect_subterms is_Var) prems)) @@ -91,18 +84,16 @@ fun define_proof_term name (local_name, [th]) lthy = val params = inter Term.aconv concl_vars prems_vars - val prf_tm = - fold_rev lambda params (Lib.term_of_typing concl) + val prf_tm = fold_rev lambda params (Lib.term_of_typing concl) val ((_, (_, raw_def)), lthy') = Local_Theory.define ((make_name_binding NONE local_name, Mixfix.NoSyn), ((make_name_binding (SOME "prf") local_name, []), prf_tm)) lthy - val def = - fold - (fn th1 => fn th2 => Thm.combination th2 th1) - (map (Thm.reflexive o Thm.cterm_of lthy) params) - raw_def + val def = fold + (fn th1 => fn th2 => Thm.combination th2 th1) + (map (Thm.reflexive o Thm.cterm_of lthy) params) + raw_def val ((_, def'), lthy'') = Local_Theory.note ((make_name_binding (SOME "def") local_name, []), [def]) @@ -112,26 +103,26 @@ fun define_proof_term name (local_name, [th]) lthy = end end | define_proof_term _ _ _ = error - ("Unimplemented: handling proof terms of multiple facts in" - ^" single result") + ("Unimplemented: proof terms for multiple facts in one statement") fun gen_schematic_theorem - bundle_includes prep_att prep_stmt - gen_prf long kind before_qed after_qed (name, raw_atts) - raw_includes raw_elems raw_concl int lthy = + bundle_includes prep_att prep_stmt + gen_prf_tm long kind + before_qed after_qed + (name, raw_atts) raw_includes raw_elems raw_concl + do_print lthy + = let - val _ = Local_Theory.assert lthy; - + val _ = Local_Theory.assert lthy val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy)) val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy |> bundle_includes raw_includes |> prep_statement (prep_att lthy) prep_stmt elems raw_concl val atts = more_atts @ map (prep_att lthy) raw_atts val pos = Position.thread_data () - val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN - fun after_qed' results goal_ctxt' = + fun gen_and_after_qed results goal_ctxt' = let val results' = burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) @@ -147,35 +138,34 @@ fun gen_schematic_theorem true) val (res', lthy'') = - if gen_prf + if gen_prf_tm then let - val (prf_tm_defs, lthy'') = - fold - (fn result => fn (defs, lthy) => - apfst (fn new_defs => defs @ new_defs) - (define_proof_term (Binding.name_of name) result lthy)) - res ([], lthy') - + val (prf_tm_defs, new_lthy) = fold + (fn result => fn (defs, lthy) => + apfst (fn new_defs => defs @ new_defs) + (define_proof_term (Binding.name_of name) result lthy)) + res + ([], lthy') val res_folded = - map (apsnd (map (Local_Defs.fold lthy'' prf_tm_defs))) res + map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res in Local_Theory.notes_kind kind [((name, @{attributes [typechk]} @ atts), [(maps #2 res_folded, [])])] - lthy'' + new_lthy end else Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy' - val _ = Proof_Display.print_results int pos lthy'' + val _ = Proof_Display.print_results do_print pos lthy'' ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res') val _ = if substmts then map - (fn (name, ths) => Proof_Display.print_results int pos lthy'' + (fn (name, ths) => Proof_Display.print_results do_print pos lthy'' (("and", name), [("", ths)])) res else [] @@ -186,7 +176,7 @@ fun gen_schematic_theorem goal_ctxt |> not (null prems) ? (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd) - |> Proof.theorem before_qed after_qed' (map snd stmt) + |> Proof.theorem before_qed gen_and_after_qed (map snd stmt) |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths) end @@ -194,16 +184,16 @@ val schematic_theorem_cmd = gen_schematic_theorem Bundle.includes_cmd Attrib.check_src - Expression.read_statement + Elaborated_Expression.read_statement fun theorem spec descr = - Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) - (Scan.option (Args.parens (Args.$$$ "derive")) - -- (long_statement || short_statement) >> - (fn (opt_derive, (long, binding, includes, elems, concl)) => - schematic_theorem_cmd - (case opt_derive of SOME "derive" => true | _ => false) - long descr NONE (K I) binding includes elems concl)) + Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) + ( Scan.option (Args.parens (Args.$$$ "derive")) + -- (long_statement || short_statement) >> + (fn (opt_derive, (long, binding, includes, elems, concl)) => + schematic_theorem_cmd + (case opt_derive of SOME "derive" => true | _ => false) + long descr NONE (K I) binding includes elems concl) ) fun definition spec descr = Outer_Syntax.local_theory_to_proof' spec "definition via proof" @@ -211,7 +201,6 @@ fun definition spec descr = (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd true long descr NONE (K I) binding includes elems concl)) - in val _ = theorem \<^command_keyword>\<open>Theorem\<close> "Theorem" diff --git a/spartan/core/lib.ML b/spartan/core/lib.ML index 7b93a08..392ae2e 100644 --- a/spartan/core/lib.ML +++ b/spartan/core/lib.ML @@ -6,13 +6,16 @@ val max: ('a * 'a -> bool) -> 'a list -> 'a val maxint: int list -> int (*Terms*) -val is_rigid: term -> bool val no_vars: term -> bool +val is_rigid: term -> bool +val is_eq: term -> bool +val dest_prop: term -> term val dest_eq: term -> term * term val mk_Var: string -> int -> typ -> term val lambda_var: term -> term -> term val is_typing: term -> bool +val mk_typing: term -> term -> term val dest_typing: term -> term * term val term_of_typing: term -> term val type_of_typing: term -> term @@ -21,6 +24,7 @@ val mk_Pi: term -> term -> term -> term val typing_of_term: term -> term (*Goals*) +val decompose_goal: Proof.context -> term -> term list * term val rigid_typing_concl: term -> bool (*Subterms*) @@ -49,9 +53,15 @@ val maxint = max (op >) (* Meta *) +val no_vars = not o exists_subterm is_Var + val is_rigid = not o is_Var o head_of -val no_vars = not o exists_subterm is_Var +fun is_eq (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _) = true + | is_eq _ = false + +fun dest_prop (Const (\<^const_name>\<open>Pure.prop\<close>, _) $ P) = P + | dest_prop P = P fun dest_eq (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ def) = (t, def) | dest_eq _ = error "dest_eq" @@ -72,8 +82,10 @@ fun lambda_var x tm = fun is_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ _ $ _) = true | is_typing _ = false +fun mk_typing t T = \<^const>\<open>has_type\<close> $ t $ T + fun dest_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ t $ T) = (t, T) - | dest_typing _ = error "dest_typing" + | dest_typing t = raise TERM ("dest_typing", [t]) val term_of_typing = #1 o dest_typing val type_of_typing = #2 o dest_typing @@ -82,11 +94,28 @@ fun mk_Pi v typ body = Const (\<^const_name>\<open>Pi\<close>, dummyT) $ typ $ l fun typing_of_term tm = \<^const>\<open>has_type\<close> $ tm $ Var (("*?", 0), \<^typ>\<open>o\<close>) (*The above is a bit hacky; basically we need to guarantee that the schematic - var is fresh*) + var is fresh. This works for now because no other code in the Isabelle system + or the current logic uses this identifier.*) (** Goals **) +(*Breaks a goal \<And>x ... y. \<lbrakk>P1; ... Pn\<rbrakk> \<Longrightarrow> Q into ([P1, ..., Pn], Q), fixing + \<And>-quantified variables and keeping schematics.*) +fun decompose_goal ctxt goal = + let + val focus = + #1 (Subgoal.focus_prems ctxt 1 NONE (Thm.trivial (Thm.cterm_of ctxt goal))) + + val schematics = #2 (#schematics focus) + |> map (fn (v, ctm) => (Thm.term_of ctm, Var v)) + in + map Thm.prop_of (#prems focus) @ [Thm.term_of (#concl focus)] + |> map (subst_free schematics) + |> (fn xs => chop (length xs - 1) xs) |> apsnd the_single + end + handle List.Empty => error "Lib.decompose_goal" + fun rigid_typing_concl goal = let val concl = Logic.strip_assums_concl goal in is_typing concl andalso is_rigid (term_of_typing concl) end diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML index 946ecd6..57164a1 100644 --- a/spartan/core/typechecking.ML +++ b/spartan/core/typechecking.ML @@ -11,6 +11,8 @@ 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 debug_typechk: bool Config.T + val known_ctac: thm list -> int -> context_tactic val check_infer: thm list -> int -> context_tactic @@ -35,6 +37,12 @@ fun put_types typings = foldr1 (op o) (map put_type typings) (* Context tactics for type-checking *) +val debug_typechk = + Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false) + +fun debug_tac ctxt s = + if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac + (*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) => @@ -46,42 +54,43 @@ fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => 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 + |> map (Simplifier.norm_hhf ctxt) + in + (debug_tac ctxt "resolve" THEN resolve_tac ctxt ths i ORELSE + debug_tac ctxt "assume" THEN 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>form\<close>) - @(Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) - @(map #1 (Elim.rules ctxt))) - in (resolve_from_net_tac ctxt net) i end - else no_tac) - val ctxt' = ctxt - in - TACTIC_CONTEXT ctxt' (tac i st) - end -in +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>form\<close>) + @(Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) + @(map #1 (Elim.rules ctxt))) + in (resolve_from_net_tac ctxt net) i end + else no_tac) + + val ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*) + in + TACTIC_CONTEXT ctxt' (tac i st) + end fun check_infer facts i (cst as (_, st)) = - let - val ctac = known_ctac facts CORELSE' check_infer_step facts + let val ctac = known_ctac facts CORELSE' check_infer_step facts in cst |> (ctac i CTHEN CREPEAT_IN_RANGE i (Thm.nprems_of st - i) (CTRY o CREPEAT_ALL_NEW_FWD ctac)) end -end end |