src/HOLCF/domain/syntax.ML
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 9060 b0dd884b1848
child 14981 e73f8140af78
permissions -rw-r--r--
GPLed;
oheimb@2453
     1
(*  Title:      HOLCF/domain/syntax.ML
oheimb@2445
     2
    ID:         $Id$
wenzelm@12030
     3
    Author:     David von Oheimb
wenzelm@12030
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
oheimb@2445
     5
wenzelm@12030
     6
Syntax generator for domain section.
regensbu@1274
     7
*)
regensbu@1274
     8
regensbu@1274
     9
structure Domain_Syntax = struct 
regensbu@1274
    10
regensbu@1274
    11
local 
regensbu@1274
    12
regensbu@1274
    13
open Domain_Library;
oheimb@4122
    14
infixr 5 -->; infixr 6 ->>;
oheimb@4122
    15
fun calc_syntax dtypeprod ((dname, typevars), 
oheimb@4122
    16
	(cons': (string * mixfix * (bool*string*typ) list) list)) =
regensbu@1274
    17
let
oheimb@4122
    18
(* ----- constants concerning the isomorphism ------------------------------- *)
regensbu@1274
    19
regensbu@1274
    20
local
oheimb@4122
    21
  fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
oheimb@4122
    22
  fun prod     (_,_,args) = if args = [] then oneT
oheimb@4122
    23
			    else foldr' mk_sprodT (map opt_lazy args);
oheimb@4122
    24
  fun freetvar s = let val tvar = mk_TFree s in
oheimb@4122
    25
		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
oheimb@4122
    26
  fun when_type (_   ,_,args) = foldr (op ->>) (map third args,freetvar "t");
regensbu@1274
    27
in
regensbu@1274
    28
  val dtype  = Type(dname,typevars);
oheimb@4122
    29
  val dtype2 = foldr' mk_ssumT (map prod cons');
oheimb@4008
    30
  val dnam = Sign.base_name dname;
oheimb@4122
    31
  val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
oheimb@4122
    32
  val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
oheimb@4122
    33
  val const_when = (dnam^"_when",foldr (op ->>) ((map when_type cons'),
oheimb@4122
    34
					        dtype ->> freetvar "t"), NoSyn);
oheimb@4122
    35
  val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
regensbu@1274
    36
end;
regensbu@1274
    37
oheimb@4122
    38
(* ----- constants concerning constructors, discriminators, and selectors --- *)
regensbu@1274
    39
regensbu@1274
    40
local
regensbu@1274
    41
  val escape = let
oheimb@4122
    42
	fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
oheimb@4122
    43
							 else      c::esc cs
oheimb@4122
    44
	|   esc []      = []
wenzelm@4709
    45
	in implode o esc o Symbol.explode end;
oheimb@4122
    46
  fun con (name,s,args) = (name,foldr (op ->>) (map third args,dtype),s);
oheimb@4122
    47
  fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
wenzelm@5700
    48
			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
oheimb@4122
    49
			(* stricly speaking, these constants have one argument,
oheimb@4122
    50
			   but the mixfix (without arguments) is introduced only
oheimb@4122
    51
			   to generate parse rules for non-alphanumeric names*)
oheimb@4122
    52
  fun sel (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args;
regensbu@1274
    53
in
regensbu@1274
    54
  val consts_con = map con cons';
regensbu@1274
    55
  val consts_dis = map dis cons';
regensbu@1274
    56
  val consts_sel = flat(map sel cons');
regensbu@1274
    57
end;
regensbu@1274
    58
oheimb@4122
    59
(* ----- constants concerning induction ------------------------------------- *)
regensbu@1274
    60
oheimb@4122
    61
  val const_take   = (dnam^"_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
oheimb@4122
    62
  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT       , NoSyn);
regensbu@1274
    63
oheimb@4122
    64
(* ----- case translation --------------------------------------------------- *)
regensbu@1274
    65
regensbu@1274
    66
local open Syntax in
regensbu@1274
    67
  val case_trans = let 
oheimb@4122
    68
	fun c_ast con mx = Constant (const_name con mx);
oheimb@4122
    69
	fun expvar n     = Variable ("e"^(string_of_int n));
oheimb@4122
    70
	fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
oheimb@4122
    71
					 (string_of_int m));
oheimb@1637
    72
	fun app s (l,r)   = mk_appl (Constant s) [l,r];
wenzelm@9060
    73
	fun case1 n (con,mx,args) = mk_appl (Constant "_case1")
slotosch@5291
    74
		 [foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
oheimb@1637
    75
		  expvar n];
oheimb@1637
    76
	fun arg1 n (con,_,args) = if args = [] then expvar n 
oheimb@1637
    77
				  else mk_appl (Constant "LAM ") 
oheimb@1637
    78
		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
wenzelm@3534
    79
  in
wenzelm@3534
    80
    ParsePrintRule
wenzelm@9060
    81
      (mk_appl (Constant "_case_syntax") [Variable "x", foldr'
wenzelm@9060
    82
				(fn (c,cs) => mk_appl (Constant"_case2") [c,cs])
wenzelm@3534
    83
				 (mapn case1 1 cons')],
slotosch@5291
    84
       mk_appl (Constant "Rep_CFun") [foldl 
slotosch@5291
    85
				(fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ])
oheimb@4008
    86
				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
wenzelm@3534
    87
				 Variable "x"])
regensbu@1274
    88
  end;
regensbu@1274
    89
end;
regensbu@1274
    90
regensbu@1274
    91
in ([const_rep, const_abs, const_when, const_copy] @ 
regensbu@1274
    92
     consts_con @ consts_dis @ consts_sel @
regensbu@1274
    93
    [const_take, const_finite],
regensbu@1274
    94
    [case_trans])
regensbu@1274
    95
end; (* let *)
regensbu@1274
    96
oheimb@4122
    97
(* ----- putting all the syntax stuff together ------------------------------ *)
regensbu@1274
    98
regensbu@1274
    99
in (* local *)
regensbu@1274
   100
oheimb@4008
   101
fun add_syntax (comp_dnam,eqs': ((string * typ list) *
oheimb@4122
   102
	(string * mixfix * (bool*string*typ) list) list) list) thy'' =
regensbu@1274
   103
let
oheimb@4122
   104
  val dtypes  = map (Type o fst) eqs';
oheimb@4122
   105
  val boolT   = HOLogic.boolT;
oheimb@4122
   106
  val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
oheimb@4122
   107
  val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
oheimb@4122
   108
  val const_copy   = (comp_dnam^"_copy"  ,funprod ->> funprod, NoSyn);
oheimb@4122
   109
  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> boolT  , NoSyn);
regensbu@1274
   110
  val ctt           = map (calc_syntax funprod) eqs';
oheimb@4122
   111
in thy'' |> ContConsts.add_consts_i (flat (map fst ctt) @ 
oheimb@4122
   112
				    (if length eqs'>1 then [const_copy] else[])@
oheimb@4122
   113
				    [const_bisim])
wenzelm@3771
   114
	 |> Theory.add_trrules_i (flat(map snd ctt))
regensbu@1274
   115
end; (* let *)
regensbu@1274
   116
regensbu@1274
   117
end; (* local *)
regensbu@1274
   118
end; (* struct *)