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