--- a/src/HOLCF/domain/syntax.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/HOLCF/domain/syntax.ML Tue Jan 30 13:42:57 1996 +0100
@@ -15,14 +15,14 @@
open Domain_Library;
infixr 5 -->; infixr 6 ~>;
fun calc_syntax dtypeprod ((dname,typevars),
- (cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
+ (cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
let
(* ----- constants concerning the isomorphism ------------------------------------- *)
local
fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
fun prod (_,_,args) = if args = [] then Type("one",[])
- else foldr' (mk_typ "**") (map opt_lazy args);
+ else foldr' (mk_typ "**") (map opt_lazy args);
in
val dtype = Type(dname,typevars);
@@ -42,20 +42,20 @@
local
val escape = let
- fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
- else c :: esc cs
- | esc [] = []
- in implode o esc o explode end;
+ fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
+ else c :: esc cs
+ | esc [] = []
+ in implode o esc o explode end;
fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
fun when_type (_ ,_,args) = foldr (op ~>) (map third args,freetvar "t");
fun con (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
fun dis (con ,s,_ ) = (dis_name_ con, dtype~>Type("tr",[]),
- ThyOps.Mixfix(Mixfix("is'_"^
- (if is_infix s then Id else escape)con,[],max_pri)));
+ ThyOps.Mixfix(Mixfix("is'_"^
+ (if is_infix s then Id else escape)con,[],max_pri)));
fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
in
val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
- dtype ~> freetvar "t"), NoSyn');
+ dtype ~> freetvar "t"), NoSyn');
val consts_con = map con cons';
val consts_dis = map dis cons';
val consts_sel = flat(map sel cons');
@@ -64,31 +64,31 @@
(* ----- constants concerning induction ------------------------------------------- *)
val const_take = (dname^"_take" ,Type("nat",[]) --> dtype ~> dtype ,NoSyn');
- val const_finite = (dname^"_finite",dtype-->HOLogic.boolT ,NoSyn');
+ val const_finite = (dname^"_finite",dtype-->HOLogic.boolT ,NoSyn');
(* ----- case translation --------------------------------------------------------- *)
local open Syntax in
val case_trans = let
- fun c_ast con syn = Constant (ThyOps.const_name con syn);
- fun expvar n = Variable ("e"^(string_of_int n));
- fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
- fun app s (l,r) = mk_appl (Constant s) [l,r];
- fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
- [if is_infix syn
- then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
- else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
- expvar n];
- fun arg1 n (con,_,args) = if args = [] then expvar n
- else mk_appl (Constant "LAM ")
- [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
+ fun c_ast con syn = Constant (ThyOps.const_name con syn);
+ fun expvar n = Variable ("e"^(string_of_int n));
+ fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
+ fun app s (l,r) = mk_appl (Constant s) [l,r];
+ fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
+ [if is_infix syn
+ then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
+ else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
+ expvar n];
+ fun arg1 n (con,_,args) = if args = [] then expvar n
+ else mk_appl (Constant "LAM ")
+ [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
in mk_appl (Constant "@case") [Variable "x", foldr'
- (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
- (mapn case1 1 cons')] <->
+ (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
+ (mapn case1 1 cons')] <->
mk_appl (Constant "@fapp") [foldl
- (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
- (Constant (dname^"_when"),mapn arg1 1 cons'),
- Variable "x"]
+ (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
+ (Constant (dname^"_when"),mapn arg1 1 cons'),
+ Variable "x"]
end;
end;
@@ -103,7 +103,7 @@
in (* local *)
fun add_syntax (comp_dname,eqs': ((string * typ list) *
- (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
+ (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
let
fun thy_type (dname,typevars) = (dname, length typevars, NoSyn);
fun thy_arity (dname,typevars) = (dname, map (K ["pcpo"]) typevars, ["pcpo"]);
@@ -118,10 +118,10 @@
val ctt = map (calc_syntax funprod) eqs';
val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
in thy'' |> add_types thy_types
- |> add_arities thy_arities
- |> add_cur_ops_i (flat(map fst ctt))
- |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
- |> add_trrules_i (flat(map snd ctt))
+ |> add_arities thy_arities
+ |> add_cur_ops_i (flat(map fst ctt))
+ |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
+ |> add_trrules_i (flat(map snd ctt))
end; (* let *)
end; (* local *)