equal
deleted
inserted
replaced
63 |
63 |
64 fun get_mapfun ctxt s = |
64 fun get_mapfun ctxt s = |
65 let |
65 let |
66 val thy = ProofContext.theory_of ctxt |
66 val thy = ProofContext.theory_of ctxt |
67 val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
67 val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
68 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
68 val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exc |
69 in |
69 in |
70 Const (mapfun, dummyT) |
70 Const (mapfun, dummyT) |
71 end |
71 end |
72 |
72 |
73 (* makes a Free out of a TVar *) |
73 (* makes a Free out of a TVar *) |
100 *) |
100 *) |
101 fun get_rty_qty ctxt s = |
101 fun get_rty_qty ctxt s = |
102 let |
102 let |
103 val thy = ProofContext.theory_of ctxt |
103 val thy = ProofContext.theory_of ctxt |
104 val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
104 val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
105 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
105 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exc |
106 in |
106 in |
107 (#rtyp qdata, #qtyp qdata) |
107 (#rtyp qdata, #qtyp qdata) |
108 end |
108 end |
109 |
109 |
110 (* takes two type-environments and looks |
110 (* takes two type-environments and looks |
268 |
268 |
269 fun get_relmap ctxt s = |
269 fun get_relmap ctxt s = |
270 let |
270 let |
271 val thy = ProofContext.theory_of ctxt |
271 val thy = ProofContext.theory_of ctxt |
272 val exc = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
272 val exc = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
273 val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc |
273 val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exc |
274 in |
274 in |
275 Const (relmap, dummyT) |
275 Const (relmap, dummyT) |
276 end |
276 end |
277 |
277 |
278 fun mk_relmap ctxt vs rty = |
278 fun mk_relmap ctxt vs rty = |
292 fun get_equiv_rel ctxt s = |
292 fun get_equiv_rel ctxt s = |
293 let |
293 let |
294 val thy = ProofContext.theory_of ctxt |
294 val thy = ProofContext.theory_of ctxt |
295 val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
295 val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
296 in |
296 in |
297 #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exc |
297 #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exc |
298 end |
298 end |
299 |
299 |
300 fun equiv_match_err ctxt ty_pat ty = |
300 fun equiv_match_err ctxt ty_pat ty = |
301 let |
301 let |
302 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
302 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
550 in |
550 in |
551 if same_const rtrm qtrm then rtrm |
551 if same_const rtrm qtrm then rtrm |
552 else |
552 else |
553 let |
553 let |
554 val rtrm' = #rconst (qconsts_lookup thy qtrm) |
554 val rtrm' = #rconst (qconsts_lookup thy qtrm) |
555 handle NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm |
555 handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm |
556 in |
556 in |
557 if Pattern.matches thy (rtrm', rtrm) |
557 if Pattern.matches thy (rtrm', rtrm) |
558 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
558 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
559 end |
559 end |
560 end |
560 end |