src/HOLCF/domain/syntax.ML
changeset 1461 6bcb44e4d6e5
parent 1274 ea0668a1c0ba
child 1637 b8a8ae2e5de1
     1.1 --- a/src/HOLCF/domain/syntax.ML	Mon Jan 29 14:16:13 1996 +0100
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Tue Jan 30 13:42:57 1996 +0100
     1.3 @@ -15,14 +15,14 @@
     1.4  open Domain_Library;
     1.5  infixr 5 -->; infixr 6 ~>;
     1.6  fun calc_syntax dtypeprod ((dname,typevars),
     1.7 -		(cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
     1.8 +                (cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
     1.9  let
    1.10  (* ----- constants concerning the isomorphism ------------------------------------- *)
    1.11  
    1.12  local
    1.13    fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
    1.14    fun prod (_,_,args) = if args = [] then Type("one",[])
    1.15 -				     else foldr' (mk_typ "**") (map opt_lazy args);
    1.16 +                                     else foldr' (mk_typ "**") (map opt_lazy args);
    1.17  
    1.18  in
    1.19    val dtype  = Type(dname,typevars);
    1.20 @@ -42,20 +42,20 @@
    1.21  
    1.22  local
    1.23    val escape = let
    1.24 -	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
    1.25 -							   else        c :: esc cs
    1.26 -	|   esc []        = []
    1.27 -	in implode o esc o explode end;
    1.28 +        fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
    1.29 +                                                           else        c :: esc cs
    1.30 +        |   esc []        = []
    1.31 +        in implode o esc o explode end;
    1.32    fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
    1.33    fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
    1.34    fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
    1.35    fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
    1.36 -			 	 ThyOps.Mixfix(Mixfix("is'_"^
    1.37 -				 (if is_infix s then Id else escape)con,[],max_pri)));
    1.38 +                                 ThyOps.Mixfix(Mixfix("is'_"^
    1.39 +                                 (if is_infix s then Id else escape)con,[],max_pri)));
    1.40    fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
    1.41  in
    1.42    val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
    1.43 -						 dtype ~> freetvar "t"), NoSyn');
    1.44 +                                                 dtype ~> freetvar "t"), NoSyn');
    1.45    val consts_con = map con cons';
    1.46    val consts_dis = map dis cons';
    1.47    val consts_sel = flat(map sel cons');
    1.48 @@ -64,31 +64,31 @@
    1.49  (* ----- constants concerning induction ------------------------------------------- *)
    1.50  
    1.51    val const_take   = (dname^"_take"  ,Type("nat",[]) --> dtype ~> dtype    ,NoSyn');
    1.52 -  val const_finite = (dname^"_finite",dtype-->HOLogic.boolT		   ,NoSyn');
    1.53 +  val const_finite = (dname^"_finite",dtype-->HOLogic.boolT                ,NoSyn');
    1.54  
    1.55  (* ----- case translation --------------------------------------------------------- *)
    1.56  
    1.57  local open Syntax in
    1.58    val case_trans = let 
    1.59 -	fun c_ast con syn = Constant (ThyOps.const_name con syn);
    1.60 -	fun expvar n      = Variable ("e"^(string_of_int n));
    1.61 -	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
    1.62 -	fun app s (l,r)   = mk_appl (Constant s) [l,r];
    1.63 -	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
    1.64 -		 [if is_infix syn
    1.65 -		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
    1.66 -		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
    1.67 -		  expvar n];
    1.68 -	fun arg1 n (con,_,args) = if args = [] then expvar n
    1.69 -				  else mk_appl (Constant "LAM ") 
    1.70 -		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
    1.71 +        fun c_ast con syn = Constant (ThyOps.const_name con syn);
    1.72 +        fun expvar n      = Variable ("e"^(string_of_int n));
    1.73 +        fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
    1.74 +        fun app s (l,r)   = mk_appl (Constant s) [l,r];
    1.75 +        fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
    1.76 +                 [if is_infix syn
    1.77 +                  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
    1.78 +                  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
    1.79 +                  expvar n];
    1.80 +        fun arg1 n (con,_,args) = if args = [] then expvar n
    1.81 +                                  else mk_appl (Constant "LAM ") 
    1.82 +                 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
    1.83    in mk_appl (Constant "@case") [Variable "x", foldr'
    1.84 -				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
    1.85 -				 (mapn case1 1 cons')] <->
    1.86 +                                 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
    1.87 +                                 (mapn case1 1 cons')] <->
    1.88       mk_appl (Constant "@fapp") [foldl 
    1.89 -				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
    1.90 -				 (Constant (dname^"_when"),mapn arg1 1 cons'),
    1.91 -				 Variable "x"]
    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 @@ -103,7 +103,7 @@
    1.99  in (* local *)
   1.100  
   1.101  fun add_syntax (comp_dname,eqs': ((string * typ list) *
   1.102 -		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
   1.103 +                (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
   1.104  let
   1.105    fun thy_type  (dname,typevars)  = (dname, length typevars, NoSyn);
   1.106    fun thy_arity (dname,typevars)  = (dname, map (K ["pcpo"]) typevars, ["pcpo"]); 
   1.107 @@ -118,10 +118,10 @@
   1.108    val ctt           = map (calc_syntax funprod) eqs';
   1.109    val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
   1.110  in thy'' |> add_types      thy_types
   1.111 -	 |> add_arities    thy_arities
   1.112 -	 |> add_cur_ops_i (flat(map fst ctt))
   1.113 -	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
   1.114 -	 |> add_trrules_i (flat(map snd ctt))
   1.115 +         |> add_arities    thy_arities
   1.116 +         |> add_cur_ops_i (flat(map fst ctt))
   1.117 +         |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
   1.118 +         |> add_trrules_i (flat(map snd ctt))
   1.119  end; (* let *)
   1.120  
   1.121  end; (* local *)