--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/domain/syntax.ML Fri Oct 06 17:25:24 1995 +0100
@@ -0,0 +1,128 @@
+(* syntax.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Created: 31-May-95
+ Updated: 16-Aug-95 case translation
+ Updated: 28-Aug-95 corrections for case translation, simultaneous domain equations
+ Copyright 1995 TU Muenchen
+*)
+
+
+structure Domain_Syntax = struct
+
+local
+
+open Domain_Library;
+infixr 5 -->; infixr 6 ~>;
+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);
+
+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_copy = (dname^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn');
+end;
+
+(* ----- constants concerning the constructors, discriminators and selectors ------ *)
+
+fun is_infix (ThyOps.CInfixl _ ) = true
+| is_infix (ThyOps.CInfixr _ ) = true
+| is_infix (ThyOps.Mixfix(Infixl _)) = true
+| is_infix (ThyOps.Mixfix(Infixr _)) = true
+| is_infix _ = false;
+
+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 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)));
+ 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');
+end;
+
+(* ----- constants concerning induction ------------------------------------------- *)
+
+ 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];
+ in mk_appl (Constant "@case") [Variable "x", foldr'
+ (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"]
+ end;
+end;
+
+in ([const_rep, const_abs, const_when, const_copy] @
+ consts_con @ consts_dis @ consts_sel @
+ [const_take, const_finite],
+ [case_trans])
+end; (* let *)
+
+(* ----- putting all the syntax stuff together ------------------------------------ *)
+
+in (* local *)
+
+fun add_syntax (comp_dname,eqs': ((string * typ list) *
+ (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';
+ val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp )dtypes);
+ val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
+ val const_copy = (comp_dname^"_copy" ,funprod ~> funprod , NoSyn');
+ val const_bisim = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
+ 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))
+end; (* let *)
+
+end; (* local *)
+end; (* struct *)