equal
deleted
inserted
replaced
62 | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
62 | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
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 exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
68 val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exc |
68 val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
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 *) |
99 a quotient definition |
99 a quotient definition |
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 exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
105 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exc |
105 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
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 |
267 Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2 |
267 Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2 |
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 exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
273 val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exc |
273 val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
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 = |
290 end |
290 end |
291 |
291 |
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 exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
296 in |
296 in |
297 #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exc |
297 #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
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 |