src/ZF/Tools/datatype_package.ML
changeset 32765 3032c0308019
parent 30364 577edc39b501
child 32952 aeb1e44fbc19
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
    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