--- a/src/HOLCF/domain/syntax.ML Wed Apr 03 19:02:04 1996 +0200
+++ b/src/HOLCF/domain/syntax.ML Wed Apr 03 19:27:14 1996 +0200
@@ -1,5 +1,4 @@
(* syntax.ML
- ID: $Id$
Author: David von Oheimb
Created: 31-May-95
Updated: 16-Aug-95 case translation
@@ -14,21 +13,24 @@
open Domain_Library;
infixr 5 -->; infixr 6 ~>;
-fun calc_syntax dtypeprod ((dname,typevars),
- (cons':(string*ThyOps.cmixfix*(bool*string*typ) list) list))=
+fun calc_syntax dtypeprod ((dname, typevars), (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);
-
+ fun prod (_,_,args) = if args = [] then Type("one",[])
+ else foldr'(mk_typ "**") (map opt_lazy args);
+ 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");
in
val dtype = Type(dname,typevars);
val dtype2 = foldr' (mk_typ "++") (map prod cons');
val const_rep = (dname^"_rep" , dtype ~> dtype2, NoSyn');
val const_abs = (dname^"_abs" , dtype2 ~> dtype , NoSyn');
+ val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
+ dtype ~> freetvar "t"), NoSyn');
val const_copy = (dname^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn');
end;
@@ -42,20 +44,16 @@
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 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 esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
+ else c :: esc cs
+ | esc [] = []
+ in implode o esc o explode end;
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');
val consts_con = map con cons';
val consts_dis = map dis cons';
val consts_sel = flat(map sel cons');
@@ -63,32 +61,32 @@
(* ----- constants concerning induction ------------------------------------------- *)
- val const_take = (dname^"_take" ,Type("nat",[]) --> dtype ~> dtype ,NoSyn');
- val const_finite = (dname^"_finite",dtype-->HOLogic.boolT ,NoSyn');
+ val const_take = (dname^"_take" , Type("nat",[]) --> dtype ~> dtype, 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,11 +101,10 @@
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"]);
- (** (fn TFree(_,sort) => sort | _ => Imposs "syntax:thy_arities")**)
val thy_types = map (thy_type o fst) eqs';
val thy_arities = map (thy_arity o fst) eqs';
val dtypes = map (Type o fst) eqs';
@@ -118,10 +115,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 *)