114 val mk_list: typ -> term list -> term |
114 val mk_list: typ -> term list -> term |
115 val dest_list: term -> term list |
115 val dest_list: term -> term list |
116 val stringT: typ |
116 val stringT: typ |
117 val mk_string: string -> term |
117 val mk_string: string -> term |
118 val dest_string: term -> string |
118 val dest_string: term -> string |
119 val message_stringT: typ |
119 val literalT: typ |
120 val mk_message_string: string -> term |
120 val mk_literal: string -> term |
121 val dest_message_string: term -> string |
121 val dest_literal: term -> string |
122 val mk_typerep: typ -> term |
122 val mk_typerep: typ -> term |
123 val mk_term_of: typ -> term -> term |
123 val mk_term_of: typ -> term -> term |
124 val reflect_term: term -> term |
124 val reflect_term: term -> term |
125 val mk_return: typ -> typ -> term -> term |
125 val mk_return: typ -> typ -> term -> term |
126 val mk_ST: ((term * typ) * (string * typ) option) list -> term -> typ -> typ option * typ -> term |
126 val mk_ST: ((term * typ) * (string * typ) option) list -> term -> typ -> typ option * typ -> term |
459 val class_size = "Nat.size"; |
459 val class_size = "Nat.size"; |
460 |
460 |
461 fun size_const T = Const ("Nat.size_class.size", T --> natT); |
461 fun size_const T = Const ("Nat.size_class.size", T --> natT); |
462 |
462 |
463 |
463 |
464 (* index *) |
464 (* code numeral *) |
465 |
465 |
466 val indexT = Type ("Code_Index.index", []); |
466 val code_numeralT = Type ("Code_Numeral.code_numeral", []); |
467 |
467 |
468 |
468 |
469 (* binary numerals and int -- non-unique representation due to leading zeros/ones! *) |
469 (* binary numerals and int -- non-unique representation due to leading zeros/ones! *) |
470 |
470 |
471 val intT = Type ("Int.int", []); |
471 val intT = Type ("Int.int", []); |
584 |
584 |
585 val mk_string = mk_list charT o map (mk_char o ord) o explode; |
585 val mk_string = mk_list charT o map (mk_char o ord) o explode; |
586 val dest_string = implode o map (chr o dest_char) o dest_list; |
586 val dest_string = implode o map (chr o dest_char) o dest_list; |
587 |
587 |
588 |
588 |
589 (* message_string *) |
589 (* literal *) |
590 |
590 |
591 val message_stringT = Type ("String.message_string", []); |
591 val literalT = Type ("String.literal", []); |
592 |
592 |
593 fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT) |
593 fun mk_literal s = Const ("String.literal.STR", stringT --> literalT) |
594 $ mk_string s; |
594 $ mk_string s; |
595 fun dest_message_string (Const ("String.message_string.STR", _) $ t) = |
595 fun dest_literal (Const ("String.literal.STR", _) $ t) = |
596 dest_string t |
596 dest_string t |
597 | dest_message_string t = raise TERM ("dest_message_string", [t]); |
597 | dest_literal t = raise TERM ("dest_literal", [t]); |
598 |
598 |
599 |
599 |
600 (* typerep and term *) |
600 (* typerep and term *) |
601 |
601 |
602 val typerepT = Type ("Typerep.typerep", []); |
602 val typerepT = Type ("Typerep.typerep", []); |
607 val termT = Type ("Code_Eval.term", []); |
607 val termT = Type ("Code_Eval.term", []); |
608 |
608 |
609 fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t; |
609 fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t; |
610 |
610 |
611 fun reflect_term (Const (c, T)) = |
611 fun reflect_term (Const (c, T)) = |
612 Const ("Code_Eval.Const", message_stringT --> typerepT --> termT) |
612 Const ("Code_Eval.Const", literalT --> typerepT --> termT) |
613 $ mk_message_string c $ mk_typerep T |
613 $ mk_literal c $ mk_typerep T |
614 | reflect_term (t1 $ t2) = |
614 | reflect_term (t1 $ t2) = |
615 Const ("Code_Eval.App", termT --> termT --> termT) |
615 Const ("Code_Eval.App", termT --> termT --> termT) |
616 $ reflect_term t1 $ reflect_term t2 |
616 $ reflect_term t1 $ reflect_term t2 |
617 | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t) |
617 | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t) |
618 | reflect_term t = t; |
618 | reflect_term t = t; |