src/HOL/thy_syntax.ML
author clasohm
Thu Nov 02 12:45:58 1995 +0100 (1995-11-02 ago)
changeset 1316 ce35d42d2190
parent 1264 3eb91524b938
child 1430 439e1476a7f8
permissions -rw-r--r--
extended complex_typ
     1 (*  Title:      HOL/thy_syntax.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
     4 
     5 Additional theory file sections for HOL.
     6 
     7 TODO:
     8   move datatype / primrec stuff to pre_datatype.ML (?)
     9 *)
    10 
    11 (*the kind of distinctiveness axioms depends on number of constructors*)
    12 val dtK = 5;  (* FIXME rename?, move? *)
    13 
    14 structure ThySynData: THY_SYN_DATA =
    15 struct
    16 
    17 open ThyParse;
    18 
    19 
    20 (** subtype **)
    21 
    22 fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
    23   let
    24     val name' = if_none opt_name t;
    25     val name = strip_quotes name';
    26   in
    27     (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
    28       [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
    29         "Abs_" ^ name ^ "_inverse"])
    30   end;
    31 
    32 val subtype_decl =
    33   optional ("(" $$-- name --$$ ")" >> Some) None --
    34   type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
    35   >> mk_subtype_decl;
    36 
    37 
    38 
    39 (** (co)inductive **)
    40 
    41 (*co is either "" or "Co"*)
    42 fun inductive_decl co =
    43   let
    44     fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
    45       if Syntax.is_identifier s then "op " ^ s else "_";
    46     fun mk_params (((recs, ipairs), monos), con_defs) =
    47       let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
    48           and srec_tms = mk_list recs
    49           and sintrs   = mk_big_list (map snd ipairs)
    50           val stri_name = big_rec_name ^ "_Intrnl"
    51       in
    52          (";\n\n\
    53           \structure " ^ stri_name ^ " =\n\
    54           \ let open Ind_Syntax in\n\
    55           \  struct\n\
    56           \  val _ = writeln \"" ^ co ^
    57                      "Inductive definition " ^ big_rec_name ^ "\"\n\
    58           \  val rec_tms\t= map (readtm (sign_of thy) termTVar) "
    59                            ^ srec_tms ^ "\n\
    60           \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
    61                            ^ sintrs ^ "\n\
    62           \  end\n\
    63           \ end;\n\n\
    64           \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
    65              stri_name ^ ".rec_tms, " ^
    66              stri_name ^ ".intr_tms)"
    67          ,
    68           "structure " ^ big_rec_name ^ " =\n\
    69           \  struct\n\
    70           \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    71           \  (open " ^ stri_name ^ "\n\
    72           \   val thy\t\t= thy\n\
    73           \   val monos\t\t= " ^ monos ^ "\n\
    74           \   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    75           \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
    76           \  open Result\n\
    77           \  end\n"
    78          )
    79       end
    80     val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    81     fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
    82   in
    83     repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
    84       >> mk_params
    85   end;
    86 
    87 
    88 
    89 (** datatype **)
    90 
    91 local
    92   (* FIXME err -> add_datatype *)
    93   fun mk_cons cs =
    94     (case duplicates (map (fst o fst) cs) of
    95       [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
    96     | dups => error ("Duplicate constructors: " ^ commas_quote dups));
    97 
    98   (*generate names of distinctiveness axioms*)
    99   fun mk_distinct_rules cs tname =
   100     let
   101       val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
   102       (*combine all constructor names with all others w/o duplicates*)
   103       fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
   104       fun neg1 [] = []
   105         | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
   106     in
   107       if length uqcs < dtK then neg1 uqcs
   108       else quote (tname ^ "_ord_distinct") ::
   109         map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
   110     end;
   111 
   112   fun mk_rules tname cons pre = " map (get_axiom thy) " ^
   113     mk_list (map (fn ((s, _), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
   114 
   115   (*generate string for calling add_datatype*)
   116   fun mk_params ((ts, tname), cons) =
   117    ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
   118     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
   119     \val thy = thy",
   120     "structure " ^ tname ^ " =\n\
   121     \struct\n\
   122     \ val inject = map (get_axiom thy) " ^
   123         mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
   124           (filter_out (null o snd o fst) cons)) ^ ";\n\
   125     \ val distinct = " ^
   126         (if length cons < dtK then "let val distinct' = " else "") ^
   127         "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
   128         (if length cons < dtK then
   129           "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
   130           \ distinct') end"
   131          else "") ^ ";\n\
   132     \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
   133     \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
   134     \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
   135     \ val simps = inject @ distinct @ cases @ recs;\n\
   136     \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
   137     \end;\n\
   138     \val dummy = Addsimps " ^ tname ^ ".simps;\n");
   139 
   140   (*parsers*)
   141   val tvars = type_args >> map (cat "dtVar");
   142 
   143   val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
   144     type_var >> cat "dtVar";
   145 
   146   fun complex_typ toks =
   147     let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
   148         val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
   149     in
   150      (typ -- repeat (ident>>quote) >>
   151         (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
   152       "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
   153        (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
   154                          mk_pair (brackets x, y)) (commas fst, ids))) toks
   155     end;
   156 
   157   val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
   158   val constructor = name -- opt_typs -- opt_mixfix;
   159 in
   160   val datatype_decl =
   161     tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
   162 end;
   163 
   164 
   165 
   166 (** primrec **)
   167 
   168 fun mk_primrec_decl ((fname, tname), axms) =
   169   let
   170     fun mk_prove (name, eqn) =
   171       "val " ^ name ^ " = store_thm (" ^ quote name
   172       ^ ", prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
   173       \  (fn _ => [Simp_tac 1]));";
   174 
   175     val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
   176   in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
   177       ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
   178   end;
   179 
   180 val primrec_decl =
   181   name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;
   182 
   183 
   184 
   185 (** sections **)
   186 
   187 val user_keywords = ["intrs", "monos", "con_defs", "|"];
   188 
   189 val user_sections =
   190  [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
   191   ("inductive", inductive_decl ""),
   192   ("coinductive", inductive_decl "Co"),
   193   ("datatype", datatype_decl),
   194   ("primrec", primrec_decl)];
   195 
   196 
   197 end;
   198 
   199 
   200 structure ThySyn = ThySynFun(ThySynData);
   201 init_thy_reader ();
   202