equal
deleted
inserted
replaced
9 val print_quotinfo: Proof.context -> unit |
9 val print_quotinfo: Proof.context -> unit |
10 val quotdata_lookup_thy: theory -> string -> quotient_info option |
10 val quotdata_lookup_thy: theory -> string -> quotient_info option |
11 val quotdata_lookup: Proof.context -> string -> quotient_info option |
11 val quotdata_lookup: Proof.context -> string -> quotient_info option |
12 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
12 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
13 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
13 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
14 |
|
15 (*FIXME: obsolete *) |
|
16 type qenv = (typ * typ) list |
|
17 val mk_qenv: Proof.context -> qenv |
|
18 val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option |
|
19 |
14 |
20 type qconsts_info = {qconst: term, rconst: term} |
15 type qconsts_info = {qconst: term, rconst: term} |
21 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
16 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
22 val qconsts_lookup: theory -> string -> qconsts_info option |
17 val qconsts_lookup: theory -> string -> qconsts_info option |
23 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
18 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
114 val _ = |
109 val _ = |
115 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
110 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
116 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
111 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
117 |
112 |
118 |
113 |
119 (* FIXME: obsolete: environments for quotient and raw types *) |
|
120 type qenv = (typ * typ) list |
|
121 |
|
122 fun mk_qenv ctxt = |
|
123 let |
|
124 val thy = ProofContext.theory_of ctxt |
|
125 val qinfo = (QuotData.get thy) |> Symtab.dest |> map snd |
|
126 in |
|
127 map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo |
|
128 end |
|
129 |
|
130 fun lookup_qenv _ [] _ = NONE |
|
131 | lookup_qenv eq ((qty, rty)::xs) qty' = |
|
132 if eq (qty', qty) then SOME (qty, rty) |
|
133 else lookup_qenv eq xs qty' |
|
134 |
|
135 (* information about quotient constants *) |
114 (* information about quotient constants *) |
136 type qconsts_info = {qconst: term, rconst: term} |
115 type qconsts_info = {qconst: term, rconst: term} |
137 |
116 |
138 structure QConstsData = Theory_Data |
117 structure QConstsData = Theory_Data |
139 (type T = qconsts_info Symtab.table |
118 (type T = qconsts_info Symtab.table |