68 in |
68 in |
69 |
69 |
70 val _ = O.add_commands |
70 val _ = O.add_commands |
71 [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)), |
71 [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)), |
72 ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))] |
72 ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))] |
|
73 |
|
74 end; |
|
75 |
|
76 |
|
77 (* code theorem antiquotation *) |
|
78 |
|
79 local |
|
80 |
|
81 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
|
82 |
|
83 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
|
84 |
|
85 fun no_vars ctxt thm = |
|
86 let |
|
87 val ctxt' = Variable.set_body false ctxt; |
|
88 val ((_, [thm]), _) = Variable.import_thms true [thm] ctxt'; |
|
89 in thm end; |
|
90 |
|
91 fun pretty_code_thm src ctxt raw_const = |
|
92 let |
|
93 val thy = ProofContext.theory_of ctxt; |
|
94 val const = Code_Unit.check_const thy raw_const; |
|
95 val (_, funcgr) = Code_Funcgr.make thy [const]; |
|
96 val thms = Code_Funcgr.eqns funcgr const |
|
97 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
|
98 |> map (no_vars ctxt o AxClass.overload thy); |
|
99 in ThyOutput.output_list pretty_thm src ctxt thms end; |
|
100 |
|
101 in |
|
102 |
|
103 val _ = O.add_commands |
|
104 [("code_thms", ThyOutput.args Args.term pretty_code_thm)]; |
73 |
105 |
74 end; |
106 end; |
75 |
107 |
76 |
108 |
77 (* code antiquotation *) |
109 (* code antiquotation *) |