src/HOLCF/domain/syntax.ML
changeset 1637 b8a8ae2e5de1
parent 1461 6bcb44e4d6e5
child 2445 51993fea433f
     1.1 --- a/src/HOLCF/domain/syntax.ML	Wed Apr 03 19:02:04 1996 +0200
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Wed Apr 03 19:27:14 1996 +0200
     1.3 @@ -1,5 +1,4 @@
     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 @@ -14,21 +13,24 @@
    1.10  
    1.11  open Domain_Library;
    1.12  infixr 5 -->; infixr 6 ~>;
    1.13 -fun calc_syntax dtypeprod ((dname,typevars),
    1.14 -                (cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
    1.15 +fun calc_syntax dtypeprod ((dname, typevars), (cons':
    1.16 +			   (string * ThyOps.cmixfix * (bool*string*typ) list) list)) =
    1.17  let
    1.18  (* ----- constants concerning the isomorphism ------------------------------------- *)
    1.19  
    1.20  local
    1.21    fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
    1.22 -  fun prod (_,_,args) = if args = [] then Type("one",[])
    1.23 -                                     else foldr' (mk_typ "**") (map opt_lazy args);
    1.24 -
    1.25 +  fun prod     (_,_,args) = if args = [] then Type("one",[])
    1.26 +				         else foldr'(mk_typ "**") (map opt_lazy args);
    1.27 +  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
    1.28 +  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
    1.29  in
    1.30    val dtype  = Type(dname,typevars);
    1.31    val dtype2 = foldr' (mk_typ "++") (map prod cons');
    1.32    val const_rep  = (dname^"_rep" ,              dtype  ~> dtype2, NoSyn');
    1.33    val const_abs  = (dname^"_abs" ,              dtype2 ~> dtype , NoSyn');
    1.34 +  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
    1.35 +						 dtype ~> freetvar "t"), NoSyn');
    1.36    val const_copy = (dname^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
    1.37  end;
    1.38  
    1.39 @@ -42,20 +44,16 @@
    1.40  
    1.41  local
    1.42    val escape = let
    1.43 -        fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
    1.44 -                                                           else        c :: esc cs
    1.45 -        |   esc []        = []
    1.46 -        in implode o esc o explode end;
    1.47 -  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
    1.48 -  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
    1.49 +	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
    1.50 +							   else        c :: esc cs
    1.51 +	|   esc []        = []
    1.52 +	in implode o esc o explode end;
    1.53    fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
    1.54    fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
    1.55 -                                 ThyOps.Mixfix(Mixfix("is'_"^
    1.56 -                                 (if is_infix s then Id else escape)con,[],max_pri)));
    1.57 +			 	 ThyOps.Mixfix(Mixfix("is'_"^
    1.58 +				 (if is_infix s then Id else escape)con,[],max_pri)));
    1.59    fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
    1.60  in
    1.61 -  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
    1.62 -                                                 dtype ~> freetvar "t"), NoSyn');
    1.63    val consts_con = map con cons';
    1.64    val consts_dis = map dis cons';
    1.65    val consts_sel = flat(map sel cons');
    1.66 @@ -63,32 +61,32 @@
    1.67  
    1.68  (* ----- constants concerning induction ------------------------------------------- *)
    1.69  
    1.70 -  val const_take   = (dname^"_take"  ,Type("nat",[]) --> dtype ~> dtype    ,NoSyn');
    1.71 -  val const_finite = (dname^"_finite",dtype-->HOLogic.boolT                ,NoSyn');
    1.72 +  val const_take   = (dname^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
    1.73 +  val const_finite = (dname^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
    1.74  
    1.75  (* ----- case translation --------------------------------------------------------- *)
    1.76  
    1.77  local open Syntax in
    1.78    val case_trans = let 
    1.79 -        fun c_ast con syn = Constant (ThyOps.const_name con syn);
    1.80 -        fun expvar n      = Variable ("e"^(string_of_int n));
    1.81 -        fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
    1.82 -        fun app s (l,r)   = mk_appl (Constant s) [l,r];
    1.83 -        fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
    1.84 -                 [if is_infix syn
    1.85 -                  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
    1.86 -                  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
    1.87 -                  expvar n];
    1.88 -        fun arg1 n (con,_,args) = if args = [] then expvar n
    1.89 -                                  else mk_appl (Constant "LAM ") 
    1.90 -                 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
    1.91 +	fun c_ast con syn = Constant (ThyOps.const_name con syn);
    1.92 +	fun expvar n      = Variable ("e"^(string_of_int n));
    1.93 +	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
    1.94 +	fun app s (l,r)   = mk_appl (Constant s) [l,r];
    1.95 +	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
    1.96 +		 [if is_infix syn
    1.97 +		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
    1.98 +		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
    1.99 +		  expvar n];
   1.100 +	fun arg1 n (con,_,args) = if args = [] then expvar n 
   1.101 +				  else mk_appl (Constant "LAM ") 
   1.102 +		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
   1.103    in mk_appl (Constant "@case") [Variable "x", foldr'
   1.104 -                                 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
   1.105 -                                 (mapn case1 1 cons')] <->
   1.106 +				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
   1.107 +				 (mapn case1 1 cons')] <->
   1.108       mk_appl (Constant "@fapp") [foldl 
   1.109 -                                 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
   1.110 -                                 (Constant (dname^"_when"),mapn arg1 1 cons'),
   1.111 -                                 Variable "x"]
   1.112 +				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
   1.113 +				 (Constant (dname^"_when"),mapn arg1 1 cons'),
   1.114 +				 Variable "x"]
   1.115    end;
   1.116  end;
   1.117  
   1.118 @@ -103,11 +101,10 @@
   1.119  in (* local *)
   1.120  
   1.121  fun add_syntax (comp_dname,eqs': ((string * typ list) *
   1.122 -                (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
   1.123 +		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
   1.124  let
   1.125    fun thy_type  (dname,typevars)  = (dname, length typevars, NoSyn);
   1.126    fun thy_arity (dname,typevars)  = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); 
   1.127 -  (**                 (fn TFree(_,sort) => sort | _ => Imposs "syntax:thy_arities")**)
   1.128    val thy_types   = map (thy_type  o fst) eqs';
   1.129    val thy_arities = map (thy_arity o fst) eqs';
   1.130    val dtypes      = map (Type      o fst) eqs';
   1.131 @@ -118,10 +115,10 @@
   1.132    val ctt           = map (calc_syntax funprod) eqs';
   1.133    val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
   1.134  in thy'' |> add_types      thy_types
   1.135 -         |> add_arities    thy_arities
   1.136 -         |> add_cur_ops_i (flat(map fst ctt))
   1.137 -         |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
   1.138 -         |> add_trrules_i (flat(map snd ctt))
   1.139 +	 |> add_arities    thy_arities
   1.140 +	 |> add_cur_ops_i (flat(map fst ctt))
   1.141 +	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
   1.142 +	 |> add_trrules_i (flat(map snd ctt))
   1.143  end; (* let *)
   1.144  
   1.145  end; (* local *)