author | wenzelm |
Sun, 21 Jul 2019 15:42:43 +0200 | |
changeset 70389 | 2adff54de67e |
parent 70388 | e31271559de8 |
child 70390 | 772321761cb8 |
permissions | -rw-r--r-- |
11522 | 1 |
(* Title: Pure/Proof/proof_syntax.ML |
11539 | 2 |
Author: Stefan Berghofer, TU Muenchen |
11522 | 3 |
|
4 |
Function for parsing and printing proof terms. |
|
5 |
*) |
|
6 |
||
7 |
signature PROOF_SYNTAX = |
|
8 |
sig |
|
17078 | 9 |
val add_proof_syntax: theory -> theory |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
10 |
val proof_of_term: theory -> bool -> term -> Proofterm.proof |
17078 | 11 |
val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) |
37227
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
12 |
val read_term: theory -> bool -> typ -> string -> term |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
13 |
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof |
17078 | 14 |
val proof_syntax: Proofterm.proof -> theory -> theory |
62922 | 15 |
val proof_of: Proof.context -> bool -> thm -> Proofterm.proof |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
16 |
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
64986 | 17 |
val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T |
11522 | 18 |
end; |
19 |
||
33388 | 20 |
structure Proof_Syntax : PROOF_SYNTAX = |
11522 | 21 |
struct |
22 |
||
23 |
(**** add special syntax for embedding proof terms ****) |
|
24 |
||
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
25 |
val proofT = Proofterm.proofT; |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
26 |
|
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
27 |
local |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
28 |
|
11614 | 29 |
val paramT = Type ("param", []); |
30 |
val paramsT = Type ("params", []); |
|
11522 | 31 |
val idtT = Type ("idt", []); |
70387 | 32 |
val aT = Term.aT []; |
11522 | 33 |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
34 |
fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); |
11522 | 35 |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
36 |
in |
62752 | 37 |
|
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
38 |
fun add_proof_syntax thy = |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
39 |
thy |
22796 | 40 |
|> Sign.root_path |
36449 | 41 |
|> Sign.set_defsort [] |
56436 | 42 |
|> Sign.add_nonterminals_global |
64556 | 43 |
[Binding.make ("param", \<^here>), |
44 |
Binding.make ("params", \<^here>)] |
|
56240 | 45 |
|> Sign.add_syntax Syntax.mode_default |
62752 | 46 |
[("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)), |
47 |
("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), |
|
48 |
("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), |
|
49 |
("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)), |
|
62761 | 50 |
("", paramT --> paramT, Mixfix.mixfix "'(_')"), |
51 |
("", idtT --> paramsT, Mixfix.mixfix "_"), |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
52 |
("", paramT --> paramsT, Mixfix.mixfix "_"), |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
53 |
(Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)), |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
54 |
(Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)), |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
55 |
(Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "?")] |
42204 | 56 |
|> Sign.add_trrules (map Syntax.Parse_Print_Rule |
56436 | 57 |
[(Ast.mk_appl (Ast.Constant "_Lam") |
58 |
[Ast.mk_appl (Ast.Constant "_Lam0") |
|
59 |
[Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"], |
|
60 |
Ast.mk_appl (Ast.Constant "_Lam") |
|
61 |
[Ast.Variable "l", |
|
62 |
Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]), |
|
63 |
(Ast.mk_appl (Ast.Constant "_Lam") |
|
64 |
[Ast.mk_appl (Ast.Constant "_Lam1") |
|
65 |
[Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"], |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
66 |
Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.AbsP")) [Ast.Variable "A", |
56436 | 67 |
(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]), |
68 |
(Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"], |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
69 |
Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.Abst")) |
56436 | 70 |
[(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]); |
11522 | 71 |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
72 |
end; |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
73 |
|
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
74 |
|
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
75 |
(** constants for theorems and axioms **) |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
76 |
|
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
77 |
fun add_proof_atom_consts names thy = |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
78 |
thy |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
79 |
|> Sign.root_path |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
80 |
|> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
81 |
|
11522 | 82 |
|
83 |
(**** translation between proof terms and pure terms ****) |
|
84 |
||
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
85 |
fun proof_of_term thy ty = |
11522 | 86 |
let |
56161 | 87 |
val thms = Global_Theory.all_thms_of thy true; |
16350 | 88 |
val axms = Theory.all_axioms_of thy; |
11522 | 89 |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
19618
diff
changeset
|
90 |
fun mk_term t = (if ty then I else map_types (K dummyT)) |
11614 | 91 |
(Term.no_dummy_patterns t); |
92 |
||
11522 | 93 |
fun prf_of [] (Bound i) = PBound i |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
94 |
| prf_of Ts (Const (s, Type ("Pure.proof", _))) = |
37310 | 95 |
Proofterm.change_type (if ty then SOME Ts else NONE) |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
96 |
(case Long_Name.explode s of |
11614 | 97 |
"axm" :: xs => |
11522 | 98 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
99 |
val name = Long_Name.implode xs; |
17223 | 100 |
val prop = (case AList.lookup (op =) axms name of |
15531 | 101 |
SOME prop => prop |
102 |
| NONE => error ("Unknown axiom " ^ quote name)) |
|
103 |
in PAxm (name, prop, NONE) end |
|
11614 | 104 |
| "thm" :: xs => |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
105 |
let val name = Long_Name.implode xs; |
17223 | 106 |
in (case AList.lookup (op =) thms name of |
37310 | 107 |
SOME thm => |
108 |
fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm)))) |
|
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
109 |
| NONE => error ("Unknown theorem " ^ quote name)) |
11522 | 110 |
end |
111 |
| _ => error ("Illegal proof constant name: " ^ quote s)) |
|
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
112 |
| prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) = |
31903 | 113 |
(case try Logic.class_of_const c_class of |
114 |
SOME c => |
|
37310 | 115 |
Proofterm.change_type (if ty then SOME Ts else NONE) |
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset
|
116 |
(OfClass (TVar ((Name.aT, 0), []), c)) |
31903 | 117 |
| NONE => error ("Bad class constant: " ^ quote c_class)) |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
118 |
| prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
119 |
| prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v |
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
120 |
| prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) = |
25245
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
121 |
if T = proofT then |
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
122 |
error ("Term variable abstraction may not bind proof variable " ^ quote s) |
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
123 |
else Abst (s, if ty then SOME T else NONE, |
37310 | 124 |
Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
125 |
| prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) = |
11614 | 126 |
AbsP (s, case t of |
56241 | 127 |
Const ("Pure.dummy_pattern", _) => NONE |
128 |
| _ $ Const ("Pure.dummy_pattern", _) => NONE |
|
15531 | 129 |
| _ => SOME (mk_term t), |
37310 | 130 |
Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
131 |
| prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) = |
11614 | 132 |
prf_of [] prf1 %% prf_of [] prf2 |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
133 |
| prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) = |
11522 | 134 |
prf_of (T::Ts) prf |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
135 |
| prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf % |
56241 | 136 |
(case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) |
11522 | 137 |
| prf_of _ t = error ("Not a proof term:\n" ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26626
diff
changeset
|
138 |
Syntax.string_of_term_global thy t) |
11522 | 139 |
|
140 |
in prf_of [] end; |
|
141 |
||
142 |
||
143 |
fun cterm_of_proof thy prf = |
|
144 |
let |
|
56161 | 145 |
val thm_names = map fst (Global_Theory.all_thms_of thy true); |
16350 | 146 |
val axm_names = map fst (Theory.all_axioms_of thy); |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
147 |
val thy' = thy |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
148 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
149 |
|> add_proof_atom_consts |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
150 |
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); |
11522 | 151 |
in |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
152 |
(Thm.global_cterm_of thy' (Proofterm.term_of_proof prf), proof_of_term thy true o Thm.term_of) |
11522 | 153 |
end; |
154 |
||
37227
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
155 |
fun read_term thy topsort = |
11522 | 156 |
let |
56161 | 157 |
val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true)); |
16350 | 158 |
val axm_names = map fst (Theory.all_axioms_of thy); |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
159 |
val ctxt = thy |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
160 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
161 |
|> add_proof_atom_consts |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
162 |
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |
42360 | 163 |
|> Proof_Context.init_global |
164 |
|> Proof_Context.allow_dummies |
|
165 |
|> Proof_Context.set_mode Proof_Context.mode_schematic |
|
62958
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset
|
166 |
|> topsort ? |
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset
|
167 |
(Proof_Context.set_defsort [] #> |
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset
|
168 |
Config.put Type_Infer.object_logic false #> |
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset
|
169 |
Config.put Type_Infer_Context.const_sorts false); |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
170 |
in |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
171 |
fn ty => fn s => |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
172 |
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |
39288 | 173 |
|> Type.constraint ty |> Syntax.check_term ctxt |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
174 |
end; |
11522 | 175 |
|
37227
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
176 |
fun read_proof thy topsort = |
bdd8dd217b1f
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
berghofe
parents:
36610
diff
changeset
|
177 |
let val rd = read_term thy topsort proofT |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35262
diff
changeset
|
178 |
in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
11522 | 179 |
|
17078 | 180 |
fun proof_syntax prf = |
11522 | 181 |
let |
37310 | 182 |
val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
183 |
(fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I |
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
184 |
| _ => I) [prf] Symtab.empty); |
37310 | 185 |
val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset
|
186 |
(fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); |
11522 | 187 |
in |
17078 | 188 |
add_proof_syntax #> |
189 |
add_proof_atom_consts |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset
|
190 |
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) |
11522 | 191 |
end; |
192 |
||
62922 | 193 |
fun proof_of ctxt full raw_thm = |
17078 | 194 |
let |
67649 | 195 |
val thm = Thm.transfer' ctxt raw_thm; |
17078 | 196 |
val prop = Thm.full_prop_of thm; |
28814 | 197 |
val prf = Thm.proof_of thm; |
37310 | 198 |
val prf' = |
199 |
(case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of |
|
200 |
(PThm (_, ((_, prop', _), body)), _) => |
|
201 |
if prop = prop' then Proofterm.join_proof body else prf |
|
17078 | 202 |
| _ => prf) |
62922 | 203 |
in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end; |
17078 | 204 |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
205 |
fun pretty_proof ctxt prf = |
42360 | 206 |
Proof_Context.pretty_term_abbrev |
55725
9d605a21d7ec
prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
wenzelm
parents:
52788
diff
changeset
|
207 |
(Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) |
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset
|
208 |
(Proofterm.term_of_proof prf); |
17078 | 209 |
|
64986 | 210 |
fun pretty_clean_proof_of ctxt full thm = |
211 |
pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm); |
|
11522 | 212 |
|
213 |
end; |