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