src/HOL/Tools/record_package.ML
changeset 8274 0d8fa545bd5c
parent 8246 efb3c8253d90
child 8294 c50607ff9704
equal deleted inserted replaced
8273:9f9e6c65487d 8274:0d8fa545bd5c
   657     val base = Sign.base_name;
   657     val base = Sign.base_name;
   658 
   658 
   659 
   659 
   660     (* basic components *)
   660     (* basic components *)
   661 
   661 
       
   662     val rN = "r";
       
   663 
   662     val alphas = map fst args;
   664     val alphas = map fst args;
   663     val name = Sign.full_name sign bname;       (*not made part of record name space!*)
   665     val name = Sign.full_name sign bname;       (*not made part of record name space!*)
   664 
   666 
   665     val parent_fields = flat (map #fields parents);
   667     val parent_fields = flat (map #fields parents);
   666     val parent_names = map fst parent_fields;
   668     val parent_names = map fst parent_fields;
   667     val parent_types = map snd parent_fields;
   669     val parent_types = map snd parent_fields;
   668     val parent_len = length parent_fields;
   670     val parent_len = length parent_fields;
   669     val parent_xs = variantlist (map (base o fst) parent_fields, [moreN]);
   671     val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, rN]);
   670     val parent_vars = ListPair.map Free (parent_xs, parent_types);
   672     val parent_vars = ListPair.map Free (parent_xs, parent_types);
   671     val parent_named_vars = parent_names ~~ parent_vars;
   673     val parent_named_vars = parent_names ~~ parent_vars;
   672 
   674 
   673     val fields = map (apfst full) bfields;
   675     val fields = map (apfst full) bfields;
   674     val names = map fst fields;
   676     val names = map fst fields;
   675     val types = map snd fields;
   677     val types = map snd fields;
   676     val len = length fields;
   678     val len = length fields;
   677     val xs = variantlist (map fst bfields, moreN :: parent_xs);
   679     val xs = variantlist (map fst bfields, moreN :: rN :: parent_xs);
   678     val vars = ListPair.map Free (xs, types);
   680     val vars = ListPair.map Free (xs, types);
   679     val named_vars = names ~~ vars;
   681     val named_vars = names ~~ vars;
   680 
   682 
   681     val all_fields = parent_fields @ fields;
   683     val all_fields = parent_fields @ fields;
   682     val all_names = parent_names @ names;
   684     val all_names = parent_names @ names;
   696     val parent_more = funpow parent_len mk_snd;
   698     val parent_more = funpow parent_len mk_snd;
   697     val idxs = 0 upto (len - 1);
   699     val idxs = 0 upto (len - 1);
   698 
   700 
   699     val rec_schemeT = mk_recordT (all_fields, moreT);
   701     val rec_schemeT = mk_recordT (all_fields, moreT);
   700     val rec_scheme = mk_record (all_named_vars, more);
   702     val rec_scheme = mk_record (all_named_vars, more);
   701     val r = Free ("r", rec_schemeT);
   703     val r = Free (rN, rec_schemeT);
   702     val recT = mk_recordT (all_fields, HOLogic.unitT);
   704     val recT = mk_recordT (all_fields, HOLogic.unitT);
   703 
   705 
   704 
   706 
   705     (* prepare print translation functions *)
   707     (* prepare print translation functions *)
   706 
   708