author  wenzelm 
Sun, 21 Jul 2019 15:19:07 +0200  
changeset 70388  e31271559de8 
parent 70387  35dd9212bf29 
child 70389  2adff54de67e 
permissions  rwrr 
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 "?")] 
61957
301833d9013a
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
60826
diff
changeset

56 
> Sign.add_syntax (Print_Mode.ASCII, true) 
62752  57 
[("_Lam", [paramsT, proofT] > proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)), 
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

58 
(Lexicon.mark_const "Pure.Appt", [proofT, aT] > proofT, mixfix ("(1_ %/ _)", [4, 5], 4)), 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

59 
(Lexicon.mark_const "Pure.AppP", [proofT, proofT] > proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))] 
42204  60 
> Sign.add_trrules (map Syntax.Parse_Print_Rule 
56436  61 
[(Ast.mk_appl (Ast.Constant "_Lam") 
62 
[Ast.mk_appl (Ast.Constant "_Lam0") 

63 
[Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"], 

64 
Ast.mk_appl (Ast.Constant "_Lam") 

65 
[Ast.Variable "l", 

66 
Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]), 

67 
(Ast.mk_appl (Ast.Constant "_Lam") 

68 
[Ast.mk_appl (Ast.Constant "_Lam1") 

69 
[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

70 
Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.AbsP")) [Ast.Variable "A", 
56436  71 
(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]), 
72 
(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

73 
Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.Abst")) 
56436  74 
[(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]); 
11522  75 

70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

76 
end; 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

77 

e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

78 

e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

79 
(** constants for theorems and axioms **) 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

80 

e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

81 
fun add_proof_atom_consts names thy = 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

82 
thy 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

83 
> Sign.root_path 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

84 
> 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

85 

11522  86 

87 
(**** translation between proof terms and pure terms ****) 

88 

28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset

89 
fun proof_of_term thy ty = 
11522  90 
let 
56161  91 
val thms = Global_Theory.all_thms_of thy true; 
16350  92 
val axms = Theory.all_axioms_of thy; 
11522  93 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
19618
diff
changeset

94 
fun mk_term t = (if ty then I else map_types (K dummyT)) 
11614  95 
(Term.no_dummy_patterns t); 
96 

11522  97 
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

98 
 prf_of Ts (Const (s, Type ("Pure.proof", _))) = 
37310  99 
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

100 
(case Long_Name.explode s of 
11614  101 
"axm" :: xs => 
11522  102 
let 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

103 
val name = Long_Name.implode xs; 
17223  104 
val prop = (case AList.lookup (op =) axms name of 
15531  105 
SOME prop => prop 
106 
 NONE => error ("Unknown axiom " ^ quote name)) 

107 
in PAxm (name, prop, NONE) end 

11614  108 
 "thm" :: xs => 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

109 
let val name = Long_Name.implode xs; 
17223  110 
in (case AList.lookup (op =) thms name of 
37310  111 
SOME thm => 
112 
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

113 
 NONE => error ("Unknown theorem " ^ quote name)) 
11522  114 
end 
115 
 _ => 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

116 
 prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) = 
31903  117 
(case try Logic.class_of_const c_class of 
118 
SOME c => 

37310  119 
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

120 
(OfClass (TVar ((Name.aT, 0), []), c)) 
31903  121 
 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

122 
 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

123 
 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

124 
 prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) = 
25245
1fcfcdcba53c
Added wellformedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset

125 
if T = proofT then 
1fcfcdcba53c
Added wellformedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset

126 
error ("Term variable abstraction may not bind proof variable " ^ quote s) 
1fcfcdcba53c
Added wellformedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset

127 
else Abst (s, if ty then SOME T else NONE, 
37310  128 
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

129 
 prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) = 
11614  130 
AbsP (s, case t of 
56241  131 
Const ("Pure.dummy_pattern", _) => NONE 
132 
 _ $ Const ("Pure.dummy_pattern", _) => NONE 

15531  133 
 _ => SOME (mk_term t), 
37310  134 
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

135 
 prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) = 
11614  136 
prf_of [] prf1 %% prf_of [] prf2 
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

137 
 prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) = 
11522  138 
prf_of (T::Ts) prf 
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

139 
 prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf % 
56241  140 
(case t of Const ("Pure.dummy_pattern", _) => NONE  _ => SOME (mk_term t)) 
11522  141 
 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

142 
Syntax.string_of_term_global thy t) 
11522  143 

144 
in prf_of [] end; 

145 

146 

147 
fun cterm_of_proof thy prf = 

148 
let 

56161  149 
val thm_names = map fst (Global_Theory.all_thms_of thy true); 
16350  150 
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

151 
val thy' = thy 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset

152 
> add_proof_syntax 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset

153 
> add_proof_atom_consts 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

154 
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); 
11522  155 
in 
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
70387
diff
changeset

156 
(Thm.global_cterm_of thy' (Proofterm.term_of_proof prf), proof_of_term thy true o Thm.term_of) 
11522  157 
end; 
158 

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

159 
fun read_term thy topsort = 
11522  160 
let 
56161  161 
val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true)); 
16350  162 
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

163 
val ctxt = thy 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset

164 
> add_proof_syntax 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset

165 
> add_proof_atom_consts 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

166 
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) 
42360  167 
> Proof_Context.init_global 
168 
> Proof_Context.allow_dummies 

169 
> 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

170 
> topsort ? 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset

171 
(Proof_Context.set_defsort [] #> 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset

172 
Config.put Type_Infer.object_logic false #> 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62922
diff
changeset

173 
Config.put Type_Infer_Context.const_sorts false); 
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset

174 
in 
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset

175 
fn ty => fn s => 
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset

176 
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s 
39288  177 
> Type.constraint ty > Syntax.check_term ctxt 
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset

178 
end; 
11522  179 

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

180 
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

181 
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

182 
in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; 
11522  183 

17078  184 
fun proof_syntax prf = 
11522  185 
let 
37310  186 
val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true 
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset

187 
(fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I 
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset

188 
 _ => I) [prf] Symtab.empty); 
37310  189 
val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true 
28807
9f3ecb4aaac2
proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28375
diff
changeset

190 
(fn PAxm (name, _, _) => Symtab.update (name, ())  _ => I) [prf] Symtab.empty); 
11522  191 
in 
17078  192 
add_proof_syntax #> 
193 
add_proof_atom_consts 

30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

194 
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) 
11522  195 
end; 
196 

62922  197 
fun proof_of ctxt full raw_thm = 
17078  198 
let 
67649  199 
val thm = Thm.transfer' ctxt raw_thm; 
17078  200 
val prop = Thm.full_prop_of thm; 
28814  201 
val prf = Thm.proof_of thm; 
37310  202 
val prf' = 
203 
(case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of 

204 
(PThm (_, ((_, prop', _), body)), _) => 

205 
if prop = prop' then Proofterm.join_proof body else prf 

17078  206 
 _ => prf) 
62922  207 
in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end; 
17078  208 

27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset

209 
fun pretty_proof ctxt prf = 
42360  210 
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

211 
(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

212 
(Proofterm.term_of_proof prf); 
17078  213 

64986  214 
fun pretty_clean_proof_of ctxt full thm = 
215 
pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm); 

11522  216 

217 
end; 