diff -r 35dd9212bf29 -r e31271559de8 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Jul 21 12:28:02 2019 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sun Jul 21 15:19:07 2019 +0200 @@ -6,10 +6,8 @@ signature PROOF_SYNTAX = sig - val proofT: typ val add_proof_syntax: theory -> theory val proof_of_term: theory -> bool -> term -> Proofterm.proof - val term_of_proof: Proofterm.proof -> term val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) val read_term: theory -> bool -> typ -> string -> term val read_proof: theory -> bool -> bool -> string -> Proofterm.proof @@ -24,40 +22,23 @@ (**** add special syntax for embedding proof terms ****) -val proofT = Type ("proof", []); +val proofT = Proofterm.proofT; + +local + val paramT = Type ("param", []); val paramsT = Type ("params", []); val idtT = Type ("idt", []); val aT = Term.aT []; - -(** constants for theorems and axioms **) +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); -fun add_proof_atom_consts names thy = - thy - |> Sign.root_path - |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); - - -(** constants for application and abstraction **) - -fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); +in fun add_proof_syntax thy = thy |> Sign.root_path |> Sign.set_defsort [] - |> Sign.add_types_global - [(Binding.make ("proof", \<^here>), 0, NoSyn)] - |> fold (snd oo Sign.declare_const_global) - [((Binding.make ("Appt", \<^here>), [proofT, aT] ---> proofT), mixfix ("(1_ \/ _)", [4, 5], 4)), - ((Binding.make ("AppP", \<^here>), [proofT, proofT] ---> proofT), mixfix ("(1_ \/ _)", [4, 5], 4)), - ((Binding.make ("Abst", \<^here>), (aT --> proofT) --> proofT), NoSyn), - ((Binding.make ("AbsP", \<^here>), [propT, proofT --> proofT] ---> proofT), NoSyn), - ((Binding.make ("Hyp", \<^here>), propT --> proofT), NoSyn), - ((Binding.make ("Oracle", \<^here>), propT --> proofT), NoSyn), - ((Binding.make ("OfClass", \<^here>), (Term.a_itselfT --> propT) --> proofT), NoSyn), - ((Binding.make ("MinProof", \<^here>), proofT), Mixfix.mixfix "?")] |> Sign.add_nonterminals_global [Binding.make ("param", \<^here>), Binding.make ("params", \<^here>)] @@ -68,11 +49,14 @@ ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)), ("", paramT --> paramT, Mixfix.mixfix "'(_')"), ("", idtT --> paramsT, Mixfix.mixfix "_"), - ("", paramT --> paramsT, Mixfix.mixfix "_")] + ("", paramT --> paramsT, Mixfix.mixfix "_"), + (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \/ _)", [4, 5], 4)), + (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \/ _)", [4, 5], 4)), + (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "?")] |> Sign.add_syntax (Print_Mode.ASCII, true) [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)), - (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)), - (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))] + (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)), + (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))] |> Sign.add_trrules (map Syntax.Parse_Print_Rule [(Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam0") @@ -83,12 +67,22 @@ (Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam1") [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"], - Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A", + Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.AbsP")) [Ast.Variable "A", (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]), (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"], - Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst")) + Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.Abst")) [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]); +end; + + +(** constants for theorems and axioms **) + +fun add_proof_atom_consts names thy = + thy + |> Sign.root_path + |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); + (**** translation between proof terms and pure terms ****) @@ -101,7 +95,7 @@ (Term.no_dummy_patterns t); fun prf_of [] (Bound i) = PBound i - | prf_of Ts (Const (s, Type ("proof", _))) = + | prf_of Ts (Const (s, Type ("Pure.proof", _))) = Proofterm.change_type (if ty then SOME Ts else NONE) (case Long_Name.explode s of "axm" :: xs => @@ -119,30 +113,30 @@ | NONE => error ("Unknown theorem " ^ quote name)) end | _ => error ("Illegal proof constant name: " ^ quote s)) - | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = + | prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) = (case try Logic.class_of_const c_class of SOME c => Proofterm.change_type (if ty then SOME Ts else NONE) (OfClass (TVar ((Name.aT, 0), []), c)) | NONE => error ("Bad class constant: " ^ quote c_class)) - | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop - | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v - | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) = + | prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop + | prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v + | prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) = if T = proofT then error ("Term variable abstraction may not bind proof variable " ^ quote s) else Abst (s, if ty then SOME T else NONE, Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) - | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = + | prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) = AbsP (s, case t of Const ("Pure.dummy_pattern", _) => NONE | _ $ Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t), Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) - | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = + | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) = prf_of [] prf1 %% prf_of [] prf2 - | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) = + | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) = prf_of (T::Ts) prf - | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % + | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf % (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) | prf_of _ t = error ("Not a proof term:\n" ^ Syntax.string_of_term_global thy t) @@ -150,48 +144,6 @@ in prf_of [] end; -val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT); -val AppPt = Const ("AppP", [proofT, proofT] ---> proofT); -val Hypt = Const ("Hyp", propT --> proofT); -val Oraclet = Const ("Oracle", propT --> proofT); -val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT); -val MinProoft = Const ("MinProof", proofT); - -val mk_tyapp = fold (fn T => fn prf => Const ("Appt", - [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); - -fun term_of _ (PThm (_, ((name, _, NONE), _))) = - Const (Long_Name.append "thm" name, proofT) - | term_of _ (PThm (_, ((name, _, SOME Ts), _))) = - mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT)) - | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) - | term_of _ (PAxm (name, _, SOME Ts)) = - mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT)) - | term_of _ (OfClass (T, c)) = - mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) - | term_of _ (PBound i) = Bound i - | term_of Ts (Abst (s, opT, prf)) = - let val T = the_default dummyT opT - in Const ("Abst", (T --> proofT) --> proofT) $ - Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf)) - end - | term_of Ts (AbsP (s, t, prf)) = - AbsPt $ the_default Term.dummy_prop t $ - Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf)) - | term_of Ts (prf1 %% prf2) = - AppPt $ term_of Ts prf1 $ term_of Ts prf2 - | term_of Ts (prf % opt) = - let val t = the_default Term.dummy opt - in Const ("Appt", - [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $ - term_of Ts prf $ t - end - | term_of Ts (Hyp t) = Hypt $ t - | term_of Ts (Oracle (_, t, _)) = Oraclet $ t - | term_of Ts MinProof = MinProoft; - -val term_of_proof = term_of []; - fun cterm_of_proof thy prf = let val thm_names = map fst (Global_Theory.all_thms_of thy true); @@ -201,7 +153,7 @@ |> add_proof_atom_consts (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); in - (Thm.global_cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) + (Thm.global_cterm_of thy' (Proofterm.term_of_proof prf), proof_of_term thy true o Thm.term_of) end; fun read_term thy topsort = @@ -257,7 +209,7 @@ fun pretty_proof ctxt prf = Proof_Context.pretty_term_abbrev (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) - (term_of_proof prf); + (Proofterm.term_of_proof prf); fun pretty_clean_proof_of ctxt full thm = pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm);