equal
deleted
inserted
replaced
9 val print_quotdata: Proof.context -> unit |
9 val print_quotdata: Proof.context -> unit |
10 val quotdata_lookup_thy: theory -> quotient_info list |
10 val quotdata_lookup_thy: theory -> quotient_info list |
11 val quotdata_lookup: Proof.context -> quotient_info list |
11 val quotdata_lookup: Proof.context -> quotient_info list |
12 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
12 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
13 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
13 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
|
14 |
|
15 type qenv = (typ * typ) list |
|
16 val mk_qenv: Proof.context -> qenv |
|
17 val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option |
14 end; |
18 end; |
15 |
19 |
16 structure Quotient_Info: QUOTIENT_INFO = |
20 structure Quotient_Info: QUOTIENT_INFO = |
17 struct |
21 struct |
|
22 |
18 |
23 |
19 (* data containers *) |
24 (* data containers *) |
20 (*******************) |
25 (*******************) |
21 |
26 |
22 (* info about map- and rel-functions *) |
27 (* info about map- and rel-functions *) |
100 |
105 |
101 val _ = |
106 val _ = |
102 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
107 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
103 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
108 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
104 |
109 |
|
110 |
|
111 (* environments of quotient and raw types *) |
|
112 type qenv = (typ * typ) list |
|
113 |
|
114 fun mk_qenv ctxt = |
|
115 let |
|
116 val qinfo = quotdata_lookup ctxt |
|
117 in |
|
118 map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo |
|
119 end |
|
120 |
|
121 fun lookup_qenv _ [] _ = NONE |
|
122 | lookup_qenv eq ((qty, rty)::xs) qty' = |
|
123 if eq (qty', qty) then SOME (qty, rty) |
|
124 else lookup_qenv eq xs qty' |
|
125 |
105 end; (* structure *) |
126 end; (* structure *) |
106 |
127 |
107 open Quotient_Info |
128 open Quotient_Info |