equal
deleted
inserted
replaced
92 |
92 |
93 (*The empty tuple is 0*) |
93 (*The empty tuple is 0*) |
94 fun mk_tuple [] = @{const "0"} |
94 fun mk_tuple [] = @{const "0"} |
95 | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; |
95 | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; |
96 |
96 |
97 fun mk_inject n k u = BalancedTree.access |
97 fun mk_inject n k u = Balanced_Tree.access |
98 {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k; |
98 {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k; |
99 |
99 |
100 val npart = length rec_names; (*number of mutually recursive parts*) |
100 val npart = length rec_names; (*number of mutually recursive parts*) |
101 |
101 |
102 |
102 |
121 let fun call_f (free,[]) = Abs("null", @{typ i}, free) |
121 let fun call_f (free,[]) = Abs("null", @{typ i}, free) |
122 | call_f (free,args) = |
122 | call_f (free,args) = |
123 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) |
123 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) |
124 @{typ i} |
124 @{typ i} |
125 free |
125 free |
126 in BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end; |
126 in Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end; |
127 |
127 |
128 (** Generating function variables for the case definition |
128 (** Generating function variables for the case definition |
129 Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
129 Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
130 |
130 |
131 (*The function variable for a single constructor*) |
131 (*The function variable for a single constructor*) |
156 |
156 |
157 val case_const = Const (case_name, case_typ); |
157 val case_const = Const (case_name, case_typ); |
158 val case_tm = list_comb (case_const, case_args); |
158 val case_tm = list_comb (case_const, case_args); |
159 |
159 |
160 val case_def = PrimitiveDefs.mk_defpair |
160 val case_def = PrimitiveDefs.mk_defpair |
161 (case_tm, BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists)); |
161 (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists)); |
162 |
162 |
163 |
163 |
164 (** Generating function variables for the recursor definition |
164 (** Generating function variables for the recursor definition |
165 Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
165 Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
166 |
166 |