--- a/src/HOLCF/domain/interface.ML Wed Oct 19 21:52:34 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,136 +0,0 @@
-(* Title: HOLCF/domain/interface.ML
- ID: $Id$
- Author: David von Oheimb
-
-Parser for domain section.
-*)
-(** BEWARE: this is still needed for old-style theories **)
-
-local
- open ThyParse;
- open Domain_Library;
-
-(* --- generation of bindings for axioms and theorems in .thy.ML - *)
-
- fun get dname name = "get_thm thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ")";
- fun gen_vals dname name = "val "^ name ^ " = get_thm" ^
- (if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
- " thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ");";
- fun gen_vall name l = "val "^name^" = "^ mk_list l^";";
- val rews = "iso_rews @ when_rews @\n\
- \ con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
- \ copy_rews";
-
- fun gen_struct num ((dname,_), cons') = let
- val axioms1 = ["abs_iso", "rep_iso", "when_def"];
- (* con_defs , sel_defs, dis_defs *)
- val axioms2 = ["copy_def", "reach", "take_def", "finite_def"];
- val theorems = ["iso_rews", "exhaust", "casedist", "when_rews", "con_rews",
- "sel_rews", "dis_rews", "dist_les", "dist_eqs", "inverts",
- "injects", "copy_rews"];
- in
- "structure "^dname^" = struct\n"^
- cat_lines (map (gen_vals dname) axioms1)^"\n"^
- gen_vall "con_defs" (map (fn (con,_,_) =>
- get dname (strip_esc con^"_def")) cons')^"\n"^
- gen_vall "sel_defs" (List.concat (map (fn (_,_,args) => map (fn (_,sel,_) =>
- get dname (sel^"_def")) args) cons'))^"\n"^
- gen_vall "dis_defs" (map (fn (con,_,_) =>
- get dname (dis_name_ con^"_def")) cons')^"\n"^
- cat_lines (map (gen_vals dname) axioms2)^"\n"^
- cat_lines (map (gen_vals dname) theorems)^"\n"^
- (if num > 1 then "val rews = " ^rews ^";\n" else "")
- end;
-
- fun mk_domain eqs'' = let
- val num = length eqs'';
- val dtnvs = map fst eqs'';
- val dnames = map fst dtnvs;
- val comp_dname = implode (separate "_" dnames);
- val conss' = ListPair.map
- (fn (dnam,cons'') => let fun sel n m = upd_second
- (fn NONE => dnam^"_sel_"^(string_of_int n)^
- "_"^(string_of_int m)
- | SOME s => s)
- fun fill_sels n con = upd_third (mapn (sel n) 1) con;
- in mapn fill_sels 1 cons'' end)
- (dnames, map snd eqs'');
- val eqs' = dtnvs~~conss';
-
-(* ----- string for calling add_domain -------------------------------------- *)
-
- val thy_ext_string = let
- fun mk_conslist cons' =
- mk_list (map (fn (c,syn,ts)=> "\n"^
- mk_triple(Library.quote c, syn, mk_list (map (fn (b,s ,tp) =>
- mk_triple(Bool.toString b, "SOME "^Library.quote s, tp)) ts))) cons');
- in "val thy = thy |> Domain_Extender.add_domain "
- ^ mk_pair(Library.quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
- mk_pair (mk_pair (Library.quote n, mk_list vs),
- mk_conslist cs)) eqs'))
- ^ ";\n"
- end;
-
-(* ----- string for producing the structures -------------------------------- *)
-
- val val_gen_string = let
- val comp_axioms = [(* copy, *) "reach", "take_def", "finite_def"
- (*, "bisim_def" *)];
- val comp_theorems = ["take_rews", "take_lemmas", "finites",
- "finite_ind", "ind", "coind"];
- fun collect sep name = if num = 1 then name else
- implode (separate sep (map (fn s => s^"."^name) dnames));
- in
- implode (separate "end; (* struct *)\n"
- (map (gen_struct num) eqs')) ^
- (if num > 1 then "end; (* struct *)\n\
- \structure "^comp_dname^" = struct\n" ^
- gen_vals comp_dname "copy_def" ^"\n" ^
- cat_lines (map (fn name => gen_vall (name^"s")
- (map (fn dn => dn^"."^name) dnames)) comp_axioms)^"\n"
- else "") ^
- gen_vals comp_dname "bisim_def" ^"\n"^
- cat_lines (map (gen_vals comp_dname) comp_theorems)^"\n"^
- "val rews = "^(if num>1 then collect" @ " "rews"else rews)^
- " @ take_rews;\n\
- \end; (* struct *)\n"
- end;
- in (thy_ext_string^
- val_gen_string^
- "val thy = thy",
- "") end;
-
-(* ----- parser for domain declaration equation ----------------------------- *)
-(** BEWARE: should be consistent with domains_decl in extender.ML **)
-
- val name' = name >> unenclose;
- fun esc_quote s = let fun esc [] = []
- | esc ("\""::xs) = esc xs
- | esc ("[" ::xs) = "{"::esc xs
- | esc ("]" ::xs) = "}"::esc xs
- | esc (x ::xs) = x ::esc xs
- in implode (esc (Symbol.explode s)) end;
- val type_var' = ((type_var >> unenclose) ^^
- optional ($$ "::" ^^ !! (sort >> esc_quote)) "") >> Library.quote;
- val type_args = (type_var' >> single
- || "(" $$-- !! (list1 type_var' --$$ ")")
- || empty >> K [])
- val con_typ = (type_args -- name' >> Library.swap)
- (* here ident may be used instead of name'
- to avoid ambiguity with standard mixfix option *)
- val domain_arg = "(" $$-- (optional ($$ "lazy" >> K true) false)
- -- (optional ((name' >> SOME) --$$ "::") NONE)
- -- typ --$$ ")"
- >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
- || typ >> (fn x => (false,NONE,x))
- val domain_cons = name' -- !! (repeat domain_arg)
- -- ThyParse.opt_mixfix
- >> (fn ((con,args),syn) => (con,syn,args));
-in
- val domain_decl = (enum1 "and" (con_typ --$$ "=" -- !!
- (enum1 "|" domain_cons))) >> mk_domain;
- val _ = ThySyn.add_syntax
- ["lazy", "and"]
- [("domain", domain_decl)]
-
-end; (* local *)