src/HOLCF/domain/interface.ML
changeset 1461 6bcb44e4d6e5
parent 1286 ae25649cbbb1
child 1637 b8a8ae2e5de1
equal deleted inserted replaced
1460:5a6f2aabd538 1461:6bcb44e4d6e5
    24 
    24 
    25   fun gt_ax         name   = "get_axiom thy "^quote name;
    25   fun gt_ax         name   = "get_axiom thy "^quote name;
    26   fun gen_val dname name   = "val "^name^" = " ^gt_ax (dname^"_"^name)^";";
    26   fun gen_val dname name   = "val "^name^" = " ^gt_ax (dname^"_"^name)^";";
    27   fun gen_vall      name l = "val "^name^" = " ^mk_list l^";";
    27   fun gen_vall      name l = "val "^name^" = " ^mk_list l^";";
    28   val rews1 = "iso_rews @ when_rews @\n\
    28   val rews1 = "iso_rews @ when_rews @\n\
    29  	      \con_rews @ sel_rews @ dis_rews @ dists_eq @ dists_le @\n\
    29               \con_rews @ sel_rews @ dis_rews @ dists_eq @ dists_le @\n\
    30 	      \copy_rews";
    30               \copy_rews";
    31 
    31 
    32   fun gen_domain eqname num ((dname,_), cons') = let
    32   fun gen_domain eqname num ((dname,_), cons') = let
    33     val axioms1 = ["abs_iso", "rep_iso", "when_def"];
    33     val axioms1 = ["abs_iso", "rep_iso", "when_def"];
    34 		   (* con_defs , sel_defs, dis_defs *) 
    34                    (* con_defs , sel_defs, dis_defs *) 
    35     val axioms2 = ["copy_def"];
    35     val axioms2 = ["copy_def"];
    36     val theorems = 
    36     val theorems = 
    37 	"iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n    \
    37         "iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n    \
    38 	\dists_eq, dists_le, inverts, injects, copy_rews";
    38         \dists_eq, dists_le, inverts, injects, copy_rews";
    39     in
    39     in
    40       "structure "^dname^" = struct\n"^
    40       "structure "^dname^" = struct\n"^
    41       cat_lines(map (gen_val dname) axioms1)^"\n"^
    41       cat_lines(map (gen_val dname) axioms1)^"\n"^
    42       gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^
    42       gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^
    43       gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) => 
    43       gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) => 
    44 					     gt_ax(sel^"_def")) args)    cons'))^"\n"^
    44                                              gt_ax(sel^"_def")) args)    cons'))^"\n"^
    45       gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def")) 
    45       gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def")) 
    46 								          cons')^"\n"^
    46                                                                           cons')^"\n"^
    47       cat_lines(map (gen_val dname) axioms2)^"\n"^
    47       cat_lines(map (gen_val dname) axioms2)^"\n"^
    48       "val ("^ theorems ^") =\n\
    48       "val ("^ theorems ^") =\n\
    49       \Domain_Theorems.theorems thy "^eqname^";\n" ^
    49       \Domain_Theorems.theorems thy "^eqname^";\n" ^
    50       (if num > 1 then "val rews = " ^rews1 ^";\n" else "")
    50       (if num > 1 then "val rews = " ^rews1 ^";\n" else "")
    51     end;
    51     end;
    55     val dnames = map fst dtnvs;
    55     val dnames = map fst dtnvs;
    56     val num = length dnames;
    56     val num = length dnames;
    57     val comp_dname = implode (separate "_" dnames);
    57     val comp_dname = implode (separate "_" dnames);
    58     val conss' = map (fn (dname,cons'') =>
    58     val conss' = map (fn (dname,cons'') =>
    59       let
    59       let
    60 	fun sel n m = upd_second (fn None   => dname^"_sel_"^(string_of_int n)^
    60         fun sel n m = upd_second (fn None   => dname^"_sel_"^(string_of_int n)^
    61 							 "_"^(string_of_int m)
    61                                                          "_"^(string_of_int m)
    62 				  |  Some s => s)
    62                                   |  Some s => s)
    63 	fun fill_sels n con = upd_third (mapn (sel n) 1) con;
    63         fun fill_sels n con = upd_third (mapn (sel n) 1) con;
    64       in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs''));
    64       in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs''));
    65     val eqs' = dtnvs~~conss';
    65     val eqs' = dtnvs~~conss';
    66 
    66 
    67 (* ----- generation of argument string for calling add_domain --------------------- *)
    67 (* ----- generation of argument string for calling add_domain --------------------- *)
    68 
    68 
    69 
    69 
    70      fun string_of_sort_emb [] = ""
    70      fun string_of_sort_emb [] = ""
    71      |   string_of_sort_emb [x] = "\"" ^x^ "\"" 
    71      |   string_of_sort_emb [x] = "\"" ^x^ "\"" 
    72 	|   string_of_sort_emb (x::xs) = "\"" ^x^ "\"" ^ ", "^(string_of_sort_emb xs);
    72         |   string_of_sort_emb (x::xs) = "\"" ^x^ "\"" ^ ", "^(string_of_sort_emb xs);
    73 
    73 
    74 	fun string_of_sort l = "["^ (string_of_sort_emb l)^"]";
    74         fun string_of_sort l = "["^ (string_of_sort_emb l)^"]";
    75 
    75 
    76     fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
    76     fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
    77     and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort)
    77     and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort)
    78     |   mk_typ (Type (name,args)) = "Type" ^mk_tnv(name,args)
    78     |   mk_typ (Type (name,args)) = "Type" ^mk_tnv(name,args)
    79     |   mk_typ _                  = Imposs "interface:mk_typ";
    79     |   mk_typ _                  = Imposs "interface:mk_typ";
    80     fun mk_conslist cons' = mk_list (map 
    80     fun mk_conslist cons' = mk_list (map 
    81 	  (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list
    81           (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list
    82      (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s,
    82      (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s,
    83 				    mk_typ tp)) ts))) cons');
    83                                     mk_typ tp)) ts))) cons');
    84     in
    84     in
    85       ("val (thy, "^comp_dname^"_equations) = thy |> Extender.add_domain \n"
    85       ("val (thy, "^comp_dname^"_equations) = thy |> Extender.add_domain \n"
    86       ^ mk_pair(quote comp_dname,
    86       ^ mk_pair(quote comp_dname,
    87 		mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
    87                 mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
    88       ^ ";\nval thy = thy",
    88       ^ ";\nval thy = thy",
    89       let
    89       let
    90 	fun plural s = if num > 1 then s^"s" else "["^s^"]";
    90         fun plural s = if num > 1 then s^"s" else "["^s^"]";
    91 	val comp_axioms   = [(* copy, *) "take_def", "finite_def", "reach" 
    91         val comp_axioms   = [(* copy, *) "take_def", "finite_def", "reach" 
    92 			     (*, "bisim_def" *)];
    92                              (*, "bisim_def" *)];
    93 	val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
    93         val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
    94 				["take_lemma","finite"]))^", finite_ind, ind, coind";
    94                                 ["take_lemma","finite"]))^", finite_ind, ind, coind";
    95 	fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), "
    95         fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), "
    96 							   ^comp_dname^"_equations)";
    96                                                            ^comp_dname^"_equations)";
    97 	fun collect sep name = if num = 1 then name else
    97         fun collect sep name = if num = 1 then name else
    98 			   implode (separate sep (map (fn s => s^"."^name) dnames));
    98                            implode (separate sep (map (fn s => s^"."^name) dnames));
    99       in
    99       in
   100 	implode (separate "end; (* struct *)\n\n" 
   100         implode (separate "end; (* struct *)\n\n" 
   101 		 (mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then
   101                  (mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then
   102 	"end; (* struct *)\n\n\
   102         "end; (* struct *)\n\n\
   103 	\structure "^comp_dname^" = struct\n" else "") ^
   103         \structure "^comp_dname^" = struct\n" else "") ^
   104 	 (if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
   104          (if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
   105 	 implode ((map (fn s => gen_vall (plural s)
   105          implode ((map (fn s => gen_vall (plural s)
   106 		  (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^
   106                   (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^
   107 	 gen_val comp_dname "bisim_def" ^"\n\
   107          gen_val comp_dname "bisim_def" ^"\n\
   108         \val ("^ comp_theorems ^") =\n\
   108         \val ("^ comp_theorems ^") =\n\
   109 	\Domain_Theorems.comp_theorems thy \
   109         \Domain_Theorems.comp_theorems thy \
   110 	\(" ^ quote comp_dname   ^ ","^ comp_dname ^"_equations,\n\
   110         \(" ^ quote comp_dname   ^ ","^ comp_dname ^"_equations,\n\
   111 	\ ["^collect "," "cases"    ^"],\n\
   111         \ ["^collect "," "cases"    ^"],\n\
   112 	\ "^ collect "@" "con_rews " ^",\n\
   112         \ "^ collect "@" "con_rews " ^",\n\
   113 	\ "^ collect "@" "copy_rews" ^");\n\
   113         \ "^ collect "@" "copy_rews" ^");\n\
   114 	\val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\
   114         \val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\
   115 	\end; (* struct *)"
   115         \end; (* struct *)"
   116       end
   116       end
   117       ) end;
   117       ) end;
   118 
   118 
   119   fun mk_gen_by (finite,eqs) = let
   119   fun mk_gen_by (finite,eqs) = let
   120       val typs    = map fst eqs;
   120       val typs    = map fst eqs;
   121       val cnstrss = map snd eqs;
   121       val cnstrss = map snd eqs;
   122       val tname = implode (separate "_" typs) in
   122       val tname = implode (separate "_" typs) in
   123       ("|> Extender.add_gen_by "
   123       ("|> Extender.add_gen_by "
   124       ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)),
   124       ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)),
   125 		mk_pair(mk_list(map quote typs), 
   125                 mk_pair(mk_list(map quote typs), 
   126 			mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
   126                         mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
   127       "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
   127       "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
   128 
   128 
   129 (* ----- parser for domain declaration equation ----------------------------------- *)
   129 (* ----- parser for domain declaration equation ----------------------------------- *)
   130 
   130 
   131 (**
   131 (**
   132   val sort = name >> (fn s => [strip_quotes s])
   132   val sort = name >> (fn s => [strip_quotes s])
   133 	  || "{" $$-- !! (list (name >> strip_quotes) --$$ "}");
   133           || "{" $$-- !! (list (name >> strip_quotes) --$$ "}");
   134   val tvar = (type_var -- (optional ("::" $$-- !! sort) ["pcpo"])) >> TFree
   134   val tvar = (type_var -- (optional ("::" $$-- !! sort) ["pcpo"])) >> TFree
   135 **)
   135 **)
   136   val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"]));
   136   val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"]));
   137 
   137 
   138   val type_args = "(" $$-- !! (list1 tvar --$$ ")")
   138   val type_args = "(" $$-- !! (list1 tvar --$$ ")")
   139 	       || tvar  >> (fn x => [x])
   139                || tvar  >> (fn x => [x])
   140 	       || empty >> K [];
   140                || empty >> K [];
   141   val con_typ     = type_args -- ident >> (fn (x,y) => Type(y,x));
   141   val con_typ     = type_args -- ident >> (fn (x,y) => Type(y,x));
   142   val typ         = con_typ 
   142   val typ         = con_typ 
   143 		 || tvar;
   143                  || tvar;
   144   val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)
   144   val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)
   145 			  -- (optional ((ident >> Some) --$$ "::") None)
   145                           -- (optional ((ident >> Some) --$$ "::") None)
   146 			  -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
   146                           -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
   147 		 || ident >> (fn x => (false,None,Type(x,[])))
   147                  || ident >> (fn x => (false,None,Type(x,[])))
   148 		 || tvar  >> (fn x => (false,None,x));
   148                  || tvar  >> (fn x => (false,None,x));
   149   val domain_cons = (name >> strip_quotes) -- !! (repeat domain_arg) 
   149   val domain_cons = (name >> strip_quotes) -- !! (repeat domain_arg) 
   150 		    -- ThyOps.opt_cmixfix
   150                     -- ThyOps.opt_cmixfix
   151 		    >> (fn ((con,args),syn) => (con,syn,args));
   151                     >> (fn ((con,args),syn) => (con,syn,args));
   152 in
   152 in
   153   val domain_decl = (enum1 "," (con_typ --$$ "="  -- !! 
   153   val domain_decl = (enum1 "," (con_typ --$$ "="  -- !! 
   154 			       (enum1 "|" domain_cons))) 	    >> mk_domain;
   154                                (enum1 "|" domain_cons)))            >> mk_domain;
   155   val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
   155   val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
   156 		    (enum1 "," (ident   --$$ "by" -- !!
   156                     (enum1 "," (ident   --$$ "by" -- !!
   157 			       (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by;
   157                                (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by;
   158 end;
   158 end;
   159 
   159 
   160 val user_keywords = "lazy"::"by"::"finite"::
   160 val user_keywords = "lazy"::"by"::"finite"::
   161 		(**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
   161                 (**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
   162 		    ThySynData.user_keywords;
   162                     ThySynData.user_keywords;
   163 val user_sections = ("domain", domain_decl)::("generated", gen_by_decl)::
   163 val user_sections = ("domain", domain_decl)::("generated", gen_by_decl)::
   164 		(**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
   164                 (**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
   165 		    ThySynData.user_sections;
   165                     ThySynData.user_sections;
   166 end;
   166 end;
   167 
   167 
   168 in
   168 in
   169 
   169 
   170 structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *)
   170 structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *)