thy_syntax.ML

additional theory file sections for HOL;

(*  Title:      HOL/thy_syntax.ML
    ID:         $Id$
    Author:     Markus Wenzel and Lawrence C Paulson

Additional theory file sections for HOL.

TODO:
  datatype, primrec
*)

structure ThySynData: THY_SYN_DATA =
struct

open ThyParse;


(* subtype *)

fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
  let
    val name' = if_none opt_name t;
    val name = strip_quotes name';
  in
    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
      ["Rep_" ^ name, "Rep_" ^ name ^ "_inverse", "Abs_" ^ name ^ "_inverse"])
  end;

val subtype_decl =
  optional ("(" $$-- name --$$ ")" >> Some) None --
  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
  >> mk_subtype_decl;


(* (co)inductive *)

(*co is either "" or "Co"*)
fun inductive_decl co =
  let
      fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
	  if Syntax.is_identifier s then "op " ^ s  else "_"
      fun mk_params (((recs, ipairs), monos), con_defs) =
        let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
	    and srec_tms = mk_list recs
            and sintrs   = mk_big_list (map snd ipairs)
            val stri_name = big_rec_name ^ "_Intrnl"
        in
	   (";\n\n\
            \structure " ^ stri_name ^ " =\n\
            \ let open Ind_Syntax in\n\
            \  struct\n\
            \  val _ = writeln \"" ^ co ^ 
	               "Inductive definition " ^ big_rec_name ^ "\"\n\
            \  val rec_tms\t= map (readtm (sign_of thy) termTVar) "
	                     ^ srec_tms ^ "\n\
            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
	                     ^ sintrs ^ "\n\
            \  end\n\
            \ end;\n\n\
            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
	       stri_name ^ ".rec_tms, " ^
               stri_name ^ ".intr_tms)"
           ,
	    "structure " ^ big_rec_name ^ " =\n\
            \  struct\n\
            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
            \  (open " ^ stri_name ^ "\n\
            \   val thy\t\t= thy\n\
            \   val monos\t\t= " ^ monos ^ "\n\
            \   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
            \  open Result\n\
            \  end\n"
	   )
	end
      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
  in repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
     >> mk_params
  end;


(* sections *)

val user_keywords = ["|", "intrs", "monos", "con_defs"];

val user_sections =
 [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
  ("inductive", inductive_decl ""),
  ("coinductive", inductive_decl "Co")];


end;


structure ThySyn = ThySynFun(ThySynData);
init_thy_reader ();