src/HOLCF/Tools/domain/domain_syntax.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 23152 9497234a2743
child 26046 1624b3304bb9
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOLCF/Tools/domain/domain_syntax.ML
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     3
    Author:     David von Oheimb
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     4
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     5
Syntax generator for domain command.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     6
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     7
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     8
structure Domain_Syntax = struct 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     9
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    10
local 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    11
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    12
open Domain_Library;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    13
infixr 5 -->; infixr 6 ->>;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    14
fun calc_syntax dtypeprod ((dname, typevars), 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    15
	(cons': (string * mixfix * (bool * string option * typ) list) list)) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    16
let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    17
(* ----- constants concerning the isomorphism ------------------------------- *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    18
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    19
local
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    20
  fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    21
  fun prod     (_,_,args) = if args = [] then oneT
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    22
			    else foldr1 mk_sprodT (map opt_lazy args);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    23
  fun freetvar s = let val tvar = mk_TFree s in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    24
		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    25
  fun when_type (_   ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    26
in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    27
  val dtype  = Type(dname,typevars);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    28
  val dtype2 = foldr1 mk_ssumT (map prod cons');
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    29
  val dnam = Sign.base_name dname;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    30
  val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    31
  val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    32
  val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    33
  val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    34
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    35
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    36
(* ----- constants concerning constructors, discriminators, and selectors --- *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    37
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    38
local
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    39
  val escape = let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    40
	fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    41
							 else      c::esc cs
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    42
	|   esc []      = []
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    43
	in implode o esc o Symbol.explode end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    44
  fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    45
  fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    46
			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    47
			(* strictly speaking, these constants have one argument,
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    48
			   but the mixfix (without arguments) is introduced only
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    49
			   to generate parse rules for non-alphanumeric names*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    50
  fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_maybeT(mk_ctupleT(map third args)),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    51
			   Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    52
  fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    53
  fun sel (_   ,_,args) = List.mapPartial sel1 args;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    54
  fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    55
			  if tvar mem typevars then freetvar ("t"^s) n else tvar end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    56
  fun mk_patT (a,b)     = a ->> mk_maybeT b;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    57
  fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    58
  fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    59
			   mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    60
			   Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    61
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    62
in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    63
  val consts_con = map con cons';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    64
  val consts_dis = map dis cons';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    65
  val consts_mat = map mat cons';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    66
  val consts_pat = map pat cons';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    67
  val consts_sel = List.concat(map sel cons');
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    68
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    69
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    70
(* ----- constants concerning induction ------------------------------------- *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    71
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    72
  val const_take   = (dnam^"_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    73
  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT       , NoSyn);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    74
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    75
(* ----- case translation --------------------------------------------------- *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    76
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    77
local open Syntax in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    78
  local
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    79
    fun c_ast con mx = Constant (const_name con mx);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    80
    fun expvar n     = Variable ("e"^(string_of_int n));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    81
    fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    82
				     (string_of_int m));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    83
    fun argvars n args = mapn (argvar n) 1 args;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    84
    fun app s (l,r)  = mk_appl (Constant s) [l,r];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    85
    val cabs = app "_cabs";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    86
    val capp = app "Rep_CFun";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    87
    fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    88
    fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    89
    fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    90
    fun when1 n m = if n = m then arg1 n else K (Constant "UU");
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    91
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    92
    fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    93
    fun app_pat x = mk_appl (Constant "_pat") [x];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    94
    fun args_list [] = Constant "Unity"
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    95
    |   args_list xs = foldr1 (app "_args") xs;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    96
  in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    97
    val case_trans = ParsePrintRule
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    98
        (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    99
         capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   100
    
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   101
    val abscon_trans = mapn (fn n => fn (con,mx,args) => ParsePrintRule
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   102
        (cabs (con1 n (con,mx,args), expvar n),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   103
         Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   104
    
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   105
    val Case_trans = List.concat (map (fn (con,mx,args) =>
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   106
      let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   107
        val cname = c_ast con mx;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   108
        val pname = Constant (pat_name_ con);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   109
        val ns = 1 upto length args;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   110
        val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   111
        val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   112
        val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   113
      in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   114
        [ParseRule (app_pat (Library.foldl capp (cname, xs)),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   115
                    mk_appl pname (map app_pat xs)),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   116
         ParseRule (app_var (Library.foldl capp (cname, xs)),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   117
                    app_var (args_list xs)),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   118
         PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   119
                    app "_match" (mk_appl pname ps, args_list vs))]
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   120
      end) cons');
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   121
  end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   122
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   123
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   124
in ([const_rep, const_abs, const_when, const_copy] @ 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   125
     consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   126
    [const_take, const_finite],
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   127
    (case_trans::(abscon_trans @ Case_trans)))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   128
end; (* let *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   129
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   130
(* ----- putting all the syntax stuff together ------------------------------ *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   131
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   132
in (* local *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   133
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   134
fun add_syntax (comp_dnam,eqs': ((string * typ list) *
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   135
	(string * mixfix * (bool * string option * typ) list) list) list) thy'' =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   136
let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   137
  val dtypes  = map (Type o fst) eqs';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   138
  val boolT   = HOLogic.boolT;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   139
  val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   140
  val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   141
  val const_copy   = (comp_dnam^"_copy"  ,funprod ->> funprod, NoSyn);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   142
  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> boolT  , NoSyn);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   143
  val ctt           = map (calc_syntax funprod) eqs';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   144
in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   145
				    (if length eqs'>1 then [const_copy] else[])@
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   146
				    [const_bisim])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   147
	 |> Sign.add_trrules_i (List.concat(map snd ctt))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   148
end; (* let *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   149
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   150
end; (* local *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   151
end; (* struct *)