611 literalT --> listT typerepT --> typerepT) $ mk_literal tyco |
611 literalT --> listT typerepT --> typerepT) $ mk_literal tyco |
612 $ mk_list typerepT (map mk_typerep Ts) |
612 $ mk_list typerepT (map mk_typerep Ts) |
613 | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep", |
613 | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep", |
614 Term.itselfT T --> typerepT) $ Logic.mk_type T; |
614 Term.itselfT T --> typerepT) $ Logic.mk_type T; |
615 |
615 |
616 val termT = Type ("Code_Eval.term", []); |
616 val termT = Type ("Code_Evaluation.term", []); |
617 |
617 |
618 fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT); |
618 fun term_of_const T = Const ("Code_Evaluation.term_of_class.term_of", T --> termT); |
619 |
619 |
620 fun mk_term_of T t = term_of_const T $ t; |
620 fun mk_term_of T t = term_of_const T $ t; |
621 |
621 |
622 fun reflect_term (Const (c, T)) = |
622 fun reflect_term (Const (c, T)) = |
623 Const ("Code_Eval.Const", literalT --> typerepT --> termT) |
623 Const ("Code_Evaluation.Const", literalT --> typerepT --> termT) |
624 $ mk_literal c $ mk_typerep T |
624 $ mk_literal c $ mk_typerep T |
625 | reflect_term (t1 $ t2) = |
625 | reflect_term (t1 $ t2) = |
626 Const ("Code_Eval.App", termT --> termT --> termT) |
626 Const ("Code_Evaluation.App", termT --> termT --> termT) |
627 $ reflect_term t1 $ reflect_term t2 |
627 $ reflect_term t1 $ reflect_term t2 |
628 | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t) |
628 | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t) |
629 | reflect_term t = t; |
629 | reflect_term t = t; |
630 |
630 |
631 fun mk_valtermify_app c vs T = |
631 fun mk_valtermify_app c vs T = |
632 let |
632 let |
633 fun termifyT T = mk_prodT (T, unitT --> termT); |
633 fun termifyT T = mk_prodT (T, unitT --> termT); |
634 fun valapp T T' = Const ("Code_Eval.valapp", |
634 fun valapp T T' = Const ("Code_Evaluation.valapp", |
635 termifyT (T --> T') --> termifyT T --> termifyT T'); |
635 termifyT (T --> T') --> termifyT T --> termifyT T'); |
636 fun mk_fTs [] _ = [] |
636 fun mk_fTs [] _ = [] |
637 | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T; |
637 | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T; |
638 val Ts = map snd vs; |
638 val Ts = map snd vs; |
639 val t = Const (c, Ts ---> T); |
639 val t = Const (c, Ts ---> T); |