src/ZF/Datatype.ML
changeset 802 2f2fbf0a7e4f
parent 733 5207fca25b6b
child 1461 6bcb44e4d6e5
equal deleted inserted replaced
801:316121afb5b5 802:2f2fbf0a7e4f
    65 
    65 
    66 open CoInductive Con
    66 open CoInductive Con
    67 end;
    67 end;
    68 
    68 
    69 
    69 
    70 (*For installing the theory section.   co is either "" or "Co"*)
       
    71 fun datatype_decl co =
       
    72   let open ThyParse Ind_Syntax
       
    73       (*generate strings*)
       
    74       fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
       
    75       val mk_data = mk_list o map mk_const o snd
       
    76       val mk_scons = mk_big_list o map mk_data
       
    77       fun mk_intr_name s =  (*the "op" cancels any infix status*)
       
    78 	  if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
       
    79       fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
       
    80         let val rec_names = map (scan_to_id o trim o fst) rec_pairs
       
    81 	    val big_rec_name = space_implode "_" rec_names
       
    82 	    and srec_tms = mk_list (map fst rec_pairs)
       
    83             and scons    = mk_scons rec_pairs
       
    84             and sdom_sum = 
       
    85 		if dom = ""  then co ^ "data_domain rec_tms" (*default*)
       
    86 		else "readtm (sign_of thy) iT " ^ dom
       
    87             val stri_name = big_rec_name ^ "_Intrnl"
       
    88             val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
       
    89         in
       
    90 	   (";\n\n\
       
    91             \structure " ^ stri_name ^ " =\n\
       
    92             \ let open Ind_Syntax in\n\
       
    93             \  struct\n\
       
    94             \  val _ = writeln \"" ^ co ^ 
       
    95 	               "Datatype definition " ^ big_rec_name ^ "\"\n\
       
    96             \  val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\
       
    97             \  val dom_sum\t= " ^ sdom_sum ^ "\n\
       
    98             \  and con_ty_lists\t= read_constructs (sign_of thy)\n" 
       
    99 	           ^ scons ^ "\n\
       
   100             \  val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\
       
   101             \  end\n\
       
   102             \ end;\n\n\
       
   103             \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ 
       
   104 	         mk_list (map quote rec_names) ^ ", " ^ 
       
   105                  stri_name ^ ".con_ty_lists) \n\
       
   106             \              |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
       
   107 	       stri_name ^ ".rec_tms, " ^
       
   108                stri_name ^ ".dom_sum, " ^
       
   109                stri_name ^ ".intr_tms)"
       
   110            ,
       
   111 	    "structure " ^ big_rec_name ^ " =\n\
       
   112             \  struct\n\
       
   113             \  val _ = writeln \"Proofs for " ^ co ^ 
       
   114 	               "Datatype definition " ^ big_rec_name ^ "\"\n\
       
   115             \  structure Result = " ^ co ^ "Data_section_Fun\n\
       
   116             \  (open " ^ stri_name ^ "\n\
       
   117             \   val thy\t\t= thy\n\
       
   118             \   val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
       
   119             \   val monos\t\t= " ^ monos ^ "\n\
       
   120             \   val type_intrs\t= " ^ type_intrs ^ "\n\
       
   121             \   val type_elims\t= " ^ type_elims ^ ");\n\n\
       
   122             \  val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
       
   123             \  open Result\n\
       
   124             \  end\n"
       
   125 	   )
       
   126 	end
       
   127       fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
       
   128       val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
       
   129       val construct = name -- string_list -- opt_mixfix;
       
   130   in optional ("<=" $$-- string) "" --
       
   131      enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
       
   132      optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
       
   133      >> mk_params
       
   134 end;