src/HOL/thy_syntax.ML
author wenzelm
Thu Oct 23 12:49:16 1997 +0200 (1997-10-23)
changeset 3980 21ef91734970
parent 3945 ae9c61d69888
child 4001 b6a3c2665c45
permissions -rw-r--r--
added record section;
     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 = 7;  (* FIXME rename?, move? *)
    13 
    14 
    15 local
    16 
    17 open ThyParse;
    18 
    19 
    20 (** typedef **)
    21 
    22 fun mk_typedef_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 typedef_decl =
    33   optional ("(" $$-- name --$$ ")" >> Some) None --
    34   type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
    35   >> mk_typedef_decl;
    36 
    37 
    38 
    39 (** record **)
    40 
    41 val record_decl =
    42   name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" --
    43   repeat1 ((name --$$ "::" -- typ) >> mk_pair)
    44   >> (fn ((x, y), zs) => space_implode " " [x, y, mk_list zs]);
    45 
    46 
    47 (** (co)inductive **)
    48 
    49 (*co is either "" or "Co"*)
    50 fun inductive_decl co =
    51   let
    52     fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
    53       if Syntax.is_identifier s then "op " ^ s else "_";
    54     fun mk_params (((recs, ipairs), monos), con_defs) =
    55       let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
    56           and srec_tms = mk_list recs
    57           and sintrs   = mk_big_list (map snd ipairs)
    58           val intrnl_name = big_rec_name ^ "_Intrnl"
    59       in
    60          (";\n\n\
    61           \structure " ^ intrnl_name ^ " =\n\
    62           \  struct\n\
    63           \  val _ = writeln \"" ^ co ^
    64                      "Inductive definition " ^ big_rec_name ^ "\"\n\
    65           \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) "
    66                            ^ srec_tms ^ "\n\
    67           \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
    68                            ^ sintrs ^ "\n\
    69           \  end;\n\n\
    70           \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
    71              intrnl_name ^ ".rec_tms, " ^
    72              intrnl_name ^ ".intr_tms)"
    73          ,
    74           "structure " ^ big_rec_name ^ " =\n\
    75           \ let\n\
    76           \  val _ = writeln \"Proofs for " ^ co ^ 
    77                      "Inductive definition " ^ big_rec_name ^ "\"\n\
    78           \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    79           \\t  (open " ^ intrnl_name ^ "\n\
    80           \\t   val thy\t\t= thy\n\
    81           \\t   val monos\t\t= " ^ monos ^ "\n\
    82           \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    83           \ in\n\
    84           \  struct\n\
    85           \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
    86           \  open Result\n\
    87           \  end\n\
    88           \ end;\n\n\
    89           \structure " ^ intrnl_name ^ " = struct end;\n\n"
    90          )
    91       end
    92     val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    93     fun optstring s = optional (s $$-- string >> trim) "[]"
    94   in
    95     repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
    96       >> mk_params
    97   end;
    98 
    99 
   100 
   101 (** datatype **)
   102 
   103 local
   104   (* FIXME err -> add_datatype *)
   105   fun mk_cons cs =
   106     (case duplicates (map (fst o fst) cs) of
   107       [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
   108     | dups => error ("Duplicate constructors: " ^ commas_quote dups));
   109 
   110   (*generate names of distinctiveness axioms*)
   111   fun mk_distinct_rules cs tname =
   112     let
   113       val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
   114       (*combine all constructor names with all others w/o duplicates*)
   115       fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
   116       fun neg1 [] = []
   117         | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
   118     in
   119       if length uqcs < dtK then neg1 uqcs
   120       else quote (tname ^ "_ord_distinct") ::
   121         map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
   122     end;
   123 
   124   fun mk_rules tname cons pre = " map (get_axiom thy) " ^
   125     mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
   126 
   127   (*generate string for calling add_datatype and build_record*)
   128   fun mk_params ((ts, tname), cons) =
   129    ("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n"
   130     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
   131     \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
   132     ,
   133     "val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
   134     \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
   135     \structure " ^ tname ^ " =\n\
   136     \struct\n\
   137     \ val inject = map (get_axiom thy) " ^
   138         mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
   139           (filter_out (null o snd o fst) cons)) ^ ";\n\
   140     \ val distinct = " ^
   141         (if length cons < dtK then "let val distinct' = " else "") ^
   142         "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
   143         (if length cons < dtK then
   144           "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
   145           \ distinct') end"
   146          else "") ^ ";\n\
   147     \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
   148     \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
   149     \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
   150     \ val simps = inject @ distinct @ cases @ recs;\n\
   151     \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
   152     \end;\n\
   153     \val dummy = datatypes := Dtype.build_record (thy, " ^
   154       mk_pair ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
   155         mk_list (map (fst o fst) cons)) ^
   156       ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
   157     \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
   158     \val dummy = AddIffs " ^ tname ^ ".inject;\n\
   159     \val dummy = " ^
   160       (if length cons < dtK then "AddIffs " else "Addsimps ") ^
   161       tname ^ ".distinct;\n\
   162     \val dummy = Addsimps(map (fn (_,eqn) =>\n\
   163     \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
   164                      "] eqn (fn _ => [Simp_tac 1]))\n" ^
   165     tname^"_size_eqns)\n"
   166    );
   167 
   168   (*parsers*)
   169   val tvars = type_args >> map (cat "dtVar");
   170 
   171   val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
   172     type_var >> cat "dtVar";
   173 
   174   fun complex_typ toks =
   175     let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
   176         val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
   177     in
   178      (typ -- repeat (ident>>quote) >>
   179         (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
   180       "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
   181        (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
   182                          mk_pair (brackets x, y)) (commas fst, ids))) toks
   183     end;
   184 
   185   val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
   186   val constructor = name -- opt_typs -- opt_mixfix;
   187 in
   188   val datatype_decl =
   189     tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
   190 end;
   191 
   192 
   193 
   194 (** primrec **)
   195 
   196 (*recursion equations have user-supplied names*)
   197 fun mk_primrec_decl_1 ((fname, tname), axms) =
   198   let
   199     (*Isolate type name from the structure's identifier it may be stored in*)
   200     val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
   201 
   202     fun mk_prove (name, eqn) =
   203       "val " ^ name ^ " = store_thm (" ^ quote name
   204       ^ ", prove_goalw thy [get_def thy "
   205       ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
   206       \  (fn _ => [Simp_tac 1]));";
   207 
   208     val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
   209   in ("|> " ^ tname ^ "_add_primrec " ^ axs
   210       , 
   211       cat_lines (map mk_prove axms)
   212       ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
   213   end;
   214 
   215 (*recursion equations have no names*)
   216 fun mk_primrec_decl_2 ((fname, tname), axms) =
   217   let
   218     (*Isolate type name from the structure's identifier it may be stored in*)
   219     val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
   220 
   221     fun mk_prove eqn =
   222       "prove_goalw thy [get_def thy "
   223       ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
   224       \(fn _ => [Simp_tac 1])";
   225 
   226     val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
   227   in ("|> " ^ tname ^ "_add_primrec " ^ axs
   228       ,
   229       "val dummy = Addsimps " ^
   230       brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
   231   end;
   232 
   233 (*function name, argument type and either (name,axiom) pairs or just axioms*)
   234 val primrec_decl =
   235   (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
   236   (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
   237 
   238 
   239 
   240 
   241 (** rec: interface to Slind's TFL **)
   242 
   243 
   244 (*fname: name of function being defined; rel: well-founded relation*)
   245 fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
   246   let val fid = trim fname
   247       val intrnl_name = fid ^ "_Intrnl"
   248   in
   249 	 (";\n\n\
   250           \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   251           \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
   252 	                 quote fid ^ " " ^ 
   253 	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
   254           \val thy = thy"
   255          ,
   256           "structure " ^ fid ^ " =\n\
   257           \  struct\n\
   258           \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
   259           \  val {rules, induct, tcs} = \n\
   260           \    \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
   261           \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
   262           \  end;\n\
   263           \val pats_" ^ intrnl_name ^ " = ();\n")
   264   end;
   265 
   266 val rec_decl = (name -- string -- 
   267 		optional ("congs" $$-- string >> trim) "[]" -- 
   268 		optional ("simpset" $$-- string >> trim) "!simpset" -- 
   269 		repeat1 string >> mk_rec_decl) ;
   270 
   271 
   272 
   273 (** augment thy syntax **)
   274 
   275 in
   276 
   277 val _ = ThySyn.add_syntax
   278  ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
   279  [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
   280   (section "record" "|> Record.add_record" record_decl),
   281   ("inductive", inductive_decl ""),
   282   ("coinductive", inductive_decl "Co"),
   283   ("datatype", datatype_decl),
   284   ("primrec", primrec_decl),
   285   ("recdef", rec_decl)];
   286 
   287 end;