src/HOLCF/domain/syntax.ML
author oheimb
Mon Oct 27 11:34:33 1997 +0100 (1997-10-27)
changeset 4008 2444085532c6
parent 3793 6e807b50b6c1
child 4122 f63c283cefaf
permissions -rw-r--r--
adapted domain and ax_ops package for name spaces
     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), (cons':
    16 			   (string * ThyOps.cmixfix * (bool*string*typ) list) list)) =
    17 let
    18 (* ----- constants concerning the isomorphism ------------------------------------- *)
    19 
    20 local
    21   fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
    22   fun prod     (_,_,args) = if args = [] then Type("one",[])
    23 				         else foldr'(mk_typ "**") (map opt_lazy args);
    24   fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
    25   fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
    26 in
    27   val dtype  = Type(dname,typevars);
    28   val dtype2 = foldr' (mk_typ "++") (map prod cons');
    29   val dnam = Sign.base_name dname;
    30   val const_rep  = (dnam^"_rep" ,              dtype  ~> dtype2, NoSyn');
    31   val const_abs  = (dnam^"_abs" ,              dtype2 ~> dtype , NoSyn');
    32   val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
    33 					       	 dtype ~> freetvar "t"), NoSyn');
    34   val const_copy = (dnam^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
    35 end;
    36 
    37 (* ----- constants concerning the constructors, discriminators and selectors ------ *)
    38 
    39 fun is_infix (ThyOps.CInfixl       _ ) = true
    40 |   is_infix (ThyOps.CInfixr       _ ) = true
    41 |   is_infix (ThyOps.Mixfix(Infixl _)) = true
    42 |   is_infix (ThyOps.Mixfix(Infixr _)) = true
    43 |   is_infix  _                        = false;
    44 
    45 local
    46   val escape = let
    47 	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
    48 							   else        c :: esc cs
    49 	|   esc []        = []
    50 	in implode o esc o explode end;
    51   fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
    52   fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
    53 			 	 ThyOps.Mixfix(Mixfix("is'_"^
    54 				 (if is_infix s then Id else escape)con,[],max_pri)));
    55   fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
    56 in
    57   val consts_con = map con cons';
    58   val consts_dis = map dis cons';
    59   val consts_sel = flat(map sel cons');
    60 end;
    61 
    62 (* ----- constants concerning induction ------------------------------------------- *)
    63 
    64   val const_take   = (dnam^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
    65   val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
    66 
    67 (* ----- case translation --------------------------------------------------------- *)
    68 
    69 local open Syntax in
    70   val case_trans = let 
    71 	fun c_ast con syn = Constant (ThyOps.const_name con syn);
    72 	fun expvar n      = Variable ("e"^(string_of_int n));
    73 	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
    74 	fun app s (l,r)   = mk_appl (Constant s) [l,r];
    75 	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
    76 		 [if is_infix syn
    77 		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
    78 		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
    79 		  expvar n];
    80 	fun arg1 n (con,_,args) = if args = [] then expvar n 
    81 				  else mk_appl (Constant "LAM ") 
    82 		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
    83   in
    84     ParsePrintRule
    85       (mk_appl (Constant "@case") [Variable "x", foldr'
    86 				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
    87 				 (mapn case1 1 cons')],
    88        mk_appl (Constant "@fapp") [foldl 
    89 				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
    90 				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
    91 				 Variable "x"])
    92   end;
    93 end;
    94 
    95 in ([const_rep, const_abs, const_when, const_copy] @ 
    96      consts_con @ consts_dis @ consts_sel @
    97     [const_take, const_finite],
    98     [case_trans])
    99 end; (* let *)
   100 
   101 (* ----- putting all the syntax stuff together ------------------------------------ *)
   102 
   103 in (* local *)
   104 
   105 fun add_syntax (comp_dnam,eqs': ((string * typ list) *
   106 		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
   107 let
   108   val dtypes  = map (Type      o fst) eqs';
   109   val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp                  )dtypes);
   110   val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
   111   val const_copy   = (comp_dnam^"_copy"  ,funprod ~> funprod       , NoSyn');
   112   val const_bisim  = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
   113   val ctt           = map (calc_syntax funprod) eqs';
   114   val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
   115 in thy'' |> add_cur_ops_i (flat(map fst ctt))
   116 	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
   117 	 |> Theory.add_trrules_i (flat(map snd ctt))
   118 end; (* let *)
   119 
   120 end; (* local *)
   121 end; (* struct *)