src/HOLCF/domain/syntax.ML
changeset 1274 ea0668a1c0ba
child 1461 6bcb44e4d6e5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Fri Oct 06 17:25:24 1995 +0100
     1.3 @@ -0,0 +1,128 @@
     1.4 +(* syntax.ML
     1.5 +   ID:         $Id$
     1.6 +   Author:  David von Oheimb
     1.7 +   Created: 31-May-95
     1.8 +   Updated: 16-Aug-95 case translation
     1.9 +   Updated: 28-Aug-95 corrections for case translation, simultaneous domain equations
    1.10 +   Copyright 1995 TU Muenchen
    1.11 +*)
    1.12 +
    1.13 +
    1.14 +structure Domain_Syntax = struct 
    1.15 +
    1.16 +local 
    1.17 +
    1.18 +open Domain_Library;
    1.19 +infixr 5 -->; infixr 6 ~>;
    1.20 +fun calc_syntax dtypeprod ((dname,typevars),
    1.21 +		(cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
    1.22 +let
    1.23 +(* ----- constants concerning the isomorphism ------------------------------------- *)
    1.24 +
    1.25 +local
    1.26 +  fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
    1.27 +  fun prod (_,_,args) = if args = [] then Type("one",[])
    1.28 +				     else foldr' (mk_typ "**") (map opt_lazy args);
    1.29 +
    1.30 +in
    1.31 +  val dtype  = Type(dname,typevars);
    1.32 +  val dtype2 = foldr' (mk_typ "++") (map prod cons');
    1.33 +  val const_rep  = (dname^"_rep" ,              dtype  ~> dtype2, NoSyn');
    1.34 +  val const_abs  = (dname^"_abs" ,              dtype2 ~> dtype , NoSyn');
    1.35 +  val const_copy = (dname^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
    1.36 +end;
    1.37 +
    1.38 +(* ----- constants concerning the constructors, discriminators and selectors ------ *)
    1.39 +
    1.40 +fun is_infix (ThyOps.CInfixl       _ ) = true
    1.41 +|   is_infix (ThyOps.CInfixr       _ ) = true
    1.42 +|   is_infix (ThyOps.Mixfix(Infixl _)) = true
    1.43 +|   is_infix (ThyOps.Mixfix(Infixr _)) = true
    1.44 +|   is_infix  _                        = false;
    1.45 +
    1.46 +local
    1.47 +  val escape = let
    1.48 +	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
    1.49 +							   else        c :: esc cs
    1.50 +	|   esc []        = []
    1.51 +	in implode o esc o explode end;
    1.52 +  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
    1.53 +  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
    1.54 +  fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
    1.55 +  fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
    1.56 +			 	 ThyOps.Mixfix(Mixfix("is'_"^
    1.57 +				 (if is_infix s then Id else escape)con,[],max_pri)));
    1.58 +  fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
    1.59 +in
    1.60 +  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
    1.61 +						 dtype ~> freetvar "t"), NoSyn');
    1.62 +  val consts_con = map con cons';
    1.63 +  val consts_dis = map dis cons';
    1.64 +  val consts_sel = flat(map sel cons');
    1.65 +end;
    1.66 +
    1.67 +(* ----- constants concerning induction ------------------------------------------- *)
    1.68 +
    1.69 +  val const_take   = (dname^"_take"  ,Type("nat",[]) --> dtype ~> dtype    ,NoSyn');
    1.70 +  val const_finite = (dname^"_finite",dtype-->HOLogic.boolT		   ,NoSyn');
    1.71 +
    1.72 +(* ----- case translation --------------------------------------------------------- *)
    1.73 +
    1.74 +local open Syntax in
    1.75 +  val case_trans = let 
    1.76 +	fun c_ast con syn = Constant (ThyOps.const_name con syn);
    1.77 +	fun expvar n      = Variable ("e"^(string_of_int n));
    1.78 +	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
    1.79 +	fun app s (l,r)   = mk_appl (Constant s) [l,r];
    1.80 +	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
    1.81 +		 [if is_infix syn
    1.82 +		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
    1.83 +		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
    1.84 +		  expvar n];
    1.85 +	fun arg1 n (con,_,args) = if args = [] then expvar n
    1.86 +				  else mk_appl (Constant "LAM ") 
    1.87 +		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
    1.88 +  in mk_appl (Constant "@case") [Variable "x", foldr'
    1.89 +				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
    1.90 +				 (mapn case1 1 cons')] <->
    1.91 +     mk_appl (Constant "@fapp") [foldl 
    1.92 +				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
    1.93 +				 (Constant (dname^"_when"),mapn arg1 1 cons'),
    1.94 +				 Variable "x"]
    1.95 +  end;
    1.96 +end;
    1.97 +
    1.98 +in ([const_rep, const_abs, const_when, const_copy] @ 
    1.99 +     consts_con @ consts_dis @ consts_sel @
   1.100 +    [const_take, const_finite],
   1.101 +    [case_trans])
   1.102 +end; (* let *)
   1.103 +
   1.104 +(* ----- putting all the syntax stuff together ------------------------------------ *)
   1.105 +
   1.106 +in (* local *)
   1.107 +
   1.108 +fun add_syntax (comp_dname,eqs': ((string * typ list) *
   1.109 +		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
   1.110 +let
   1.111 +  fun thy_type  (dname,typevars)  = (dname, length typevars, NoSyn);
   1.112 +  fun thy_arity (dname,typevars)  = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); 
   1.113 +  (**                 (fn TFree(_,sort) => sort | _ => Imposs "syntax:thy_arities")**)
   1.114 +  val thy_types   = map (thy_type  o fst) eqs';
   1.115 +  val thy_arities = map (thy_arity o fst) eqs';
   1.116 +  val dtypes      = map (Type      o fst) eqs';
   1.117 +  val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp                  )dtypes);
   1.118 +  val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
   1.119 +  val const_copy   = (comp_dname^"_copy"  ,funprod ~> funprod       , NoSyn');
   1.120 +  val const_bisim  = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
   1.121 +  val ctt           = map (calc_syntax funprod) eqs';
   1.122 +  val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
   1.123 +in thy'' |> add_types      thy_types
   1.124 +	 |> add_arities    thy_arities
   1.125 +	 |> add_cur_ops_i (flat(map fst ctt))
   1.126 +	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
   1.127 +	 |> add_trrules_i (flat(map snd ctt))
   1.128 +end; (* let *)
   1.129 +
   1.130 +end; (* local *)
   1.131 +end; (* struct *)