283 |
283 |
284 (* consts signature *) |
284 (* consts signature *) |
285 |
285 |
286 fun const_constraint thy c = |
286 fun const_constraint thy c = |
287 let val ((_, consts), constraints) = #consts (rep_sg thy) in |
287 let val ((_, consts), constraints) = #consts (rep_sg thy) in |
288 (case Symtab.curried_lookup constraints c of |
288 (case Symtab.lookup constraints c of |
289 NONE => Option.map #1 (Symtab.curried_lookup consts c) |
289 NONE => Option.map #1 (Symtab.lookup consts c) |
290 | some => some) |
290 | some => some) |
291 end; |
291 end; |
292 |
292 |
293 fun the_const_constraint thy c = |
293 fun the_const_constraint thy c = |
294 (case const_constraint thy c of SOME T => T |
294 (case const_constraint thy c of SOME T => T |
295 | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); |
295 | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); |
296 |
296 |
297 val const_type = Option.map #1 oo (Symtab.curried_lookup o #2 o #1 o #consts o rep_sg); |
297 val const_type = Option.map #1 oo (Symtab.lookup o #2 o #1 o #consts o rep_sg); |
298 |
298 |
299 fun the_const_type thy c = |
299 fun the_const_type thy c = |
300 (case const_type thy c of SOME T => T |
300 (case const_type thy c of SOME T => T |
301 | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); |
301 | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); |
302 |
302 |
515 |
515 |
516 (* type and constant names *) |
516 (* type and constant names *) |
517 |
517 |
518 fun read_tyname thy raw_c = |
518 fun read_tyname thy raw_c = |
519 let val c = intern_type thy raw_c in |
519 let val c = intern_type thy raw_c in |
520 (case Symtab.curried_lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of |
520 (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of |
521 SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT) |
521 SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT) |
522 | _ => error ("Undeclared type constructor: " ^ quote c)) |
522 | _ => error ("Undeclared type constructor: " ^ quote c)) |
523 end; |
523 end; |
524 |
524 |
525 fun read_const thy raw_c = |
525 fun read_const thy raw_c = |
715 val c = int_const thy raw_c; |
715 val c = int_const thy raw_c; |
716 val T = Term.zero_var_indexesT (Term.no_dummyT (prep_typ thy raw_T)) |
716 val T = Term.zero_var_indexesT (Term.no_dummyT (prep_typ thy raw_T)) |
717 handle TYPE (msg, _, _) => error msg; |
717 handle TYPE (msg, _, _) => error msg; |
718 val _ = cert_term thy (Const (c, T)) |
718 val _ = cert_term thy (Const (c, T)) |
719 handle TYPE (msg, _, _) => error msg; |
719 handle TYPE (msg, _, _) => error msg; |
720 in thy |> map_consts (apsnd (Symtab.curried_update (c, T))) end; |
720 in thy |> map_consts (apsnd (Symtab.update (c, T))) end; |
721 |
721 |
722 val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort); |
722 val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort); |
723 val add_const_constraint_i = gen_add_constraint (K I) certify_typ; |
723 val add_const_constraint_i = gen_add_constraint (K I) certify_typ; |
724 |
724 |
725 |
725 |