78 |
78 |
79 end |
79 end |
80 |
80 |
81 instantiation prod :: (full_small, full_small) full_small |
81 instantiation prod :: (full_small, full_small) full_small |
82 begin |
82 begin |
83 ML {* @{const_name "Pair"} *} |
83 |
84 definition |
84 definition |
85 "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y), |
85 "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y), |
86 %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d" |
86 %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d" |
87 |
87 |
88 instance .. |
88 instance .. |
95 fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
95 fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
96 where |
96 where |
97 "full_small_fun' f i d = (if i > 1 then |
97 "full_small_fun' f i d = (if i > 1 then |
98 full_small (%(a, at). full_small (%(b, bt). |
98 full_small (%(a, at). full_small (%(b, bt). |
99 full_small_fun' (%(g, gt). f (g(a := b), |
99 full_small_fun' (%(g, gt). f (g(a := b), |
100 (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
100 (%_. let T1 = (Typerep.typerep (TYPE('a))); |
101 |
101 T2 = (Typerep.typerep (TYPE('b))) |
102 (Code_Evaluation.Const (STR ''Fun.fun_upd'') |
102 in |
103 |
103 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
104 (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) |
104 (Code_Evaluation.Const (STR ''Fun.fun_upd'') |
105 |
105 (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], |
106 (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then |
106 Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) |
107 full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))" |
107 (gt ())) (at ())) (bt ())))) (i - 1) d) d) d |
|
108 else (if i > 0 then |
|
109 full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))" |
108 |
110 |
109 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" |
111 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" |
110 where |
112 where |
111 "full_small_fun f d = full_small_fun' f d d" |
113 "full_small_fun f d = full_small_fun' f d d" |
112 |
114 |