--- a/src/HOLCF/ax_ops/thy_ops.ML Tue Nov 04 14:37:51 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,449 +0,0 @@
-(* TTITLEF/thy_ops.ML
- ID: $Id$
- Author: Tobias Mayr
-
-Additional theory file section for HOLCF: ops
-
-TODO:
- maybe AST-representation with "op name" instead of _I_...
-*)
-
-signature THY_OPS =
-sig
- (* continuous mixfixes (extension of datatype Mixfix.mixfix) *)
- datatype cmixfix =
- Mixfix of Mixfix.mixfix |
- CInfixl of int |
- CInfixr of int |
- CMixfix of string * int list *int;
-
- exception CINFIX of cmixfix;
- val cmixfix_to_mixfix : cmixfix -> Mixfix.mixfix;
-
- (* theory extenders : *)
- val add_ops : {curried: bool, total: bool, strict: bool} ->
- (string * string * cmixfix) list -> theory -> theory;
- val add_ops_i : {curried: bool, total: bool, strict: bool} ->
- (string * typ * cmixfix) list -> theory -> theory;
- val ops_keywords : string list;
- val ops_sections : (string * (ThyParse.token list ->
- (string * string) * ThyParse.token list)) list;
- val opt_cmixfix: ThyParse.token list -> (string * ThyParse.token list);
- val const_name : string -> cmixfix -> string;
-end;
-
-structure ThyOps : THY_OPS =
-struct
-
-open HOLCFlogic;
-
-(** library ******************************************************)
-
-(* abbreviations *)
-val internal = fst; (* cinfix-ops will have diffrent internal/external names *)
-val external = snd;
-
-fun apsnd_of_three f = fn (a,b,c) => (a,f b,c);
-
-
-(******** ops ********************)
-
-(* the extended copy of mixfix *)
-datatype cmixfix =
- Mixfix of Mixfix.mixfix |
- CInfixl of int |
- CInfixr of int |
- CMixfix of string * int list *int;
-
-exception CINFIX of cmixfix;
-
-fun cmixfix_to_mixfix (Mixfix x) = x
- | cmixfix_to_mixfix x = raise CINFIX x;
-
-
-(** theory extender : add_ops *)
-
-(* generating the declarations of the new constants. *************
- cinfix names x are internally non infix (renamed by mk_internal_name)
- and externally non continous infix function names (changed by op_to_fun).
- Thus the cinfix declaration is splitted in an 'oldstyle' decl,
- which is NoSyn (non infix) and is added by add_consts_i,
- and an syn(tactic) decl, which is an infix function (not operation)
- added by add_syntax_i, so that it can appear in input strings, but
- not in terms.
- The interface between internal and external names is realized by
- transrules A x B <=> _x ' A ' B (generated by xrules_of)
- The boolean argument 'curried' distinguishes between curried and
- tupeled syntax of operation application *)
-
-local
- fun strip ("'" :: c :: cs) = c :: strip cs
- | strip ["'"] = []
- | strip (c :: cs) = c :: strip cs
- | strip [] = [];
-
- val strip_esc = implode o strip o explode;
-
- fun infix_name c = "op " ^ strip_esc c;
-in
- val mk_internal_name = infix_name;
-(*
-(* changing e.g. 'ab' to '_I_97_98'.
- Called by oldstyle, xrules_of, strictness_axms and totality_axms. *)
- fun mk_internal_name name =
- let fun alphanum (s::ss) = "_"^(string_of_int (ord s))^(alphanum ss)
- | alphanum [] = "";
- in
- "_I"^(alphanum o explode) name
- end;
-*)
- (* extension of Pure/Syntax/mixfix.ML: SynExt.const_name *)
- fun const_name c (CInfixl _) = mk_internal_name c
- | const_name c (CInfixr _) = mk_internal_name c
- | const_name c (CMixfix _) = c
- | const_name c (Mixfix x) = Syntax.const_name c x;
-end;
-
-(* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *)
-(*####*)
-fun op_to_fun true sign (ty as Type(name ,[larg,t]))= if name = cfun_arrow
- then Type("fun",[larg,op_to_fun true sign t]) else ty
- | op_to_fun false sign (ty as Type(name,[args,res])) = let
- fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs])
- | otf t = Type("fun",[t,res]);
- in if name = cfun_arrow then otf args else ty end
- | op_to_fun _ sign t = t;
-(*####*)
-
-(* oldstyle is called by add_ext_axioms(_i) *)
- (* the first part is just copying the homomorphic part of the structures *)
-fun oldstyle ((name,typ,Mixfix(x))::tl) =
- (name,typ,x)::(oldstyle tl)
- | oldstyle ((name,typ,CInfixl(i))::tl) =
- (mk_internal_name name,typ,Mixfix.NoSyn)::
- (oldstyle tl)
- | oldstyle ((name,typ,CInfixr(i))::tl) =
- (mk_internal_name name,typ,Mixfix.NoSyn)::
- (oldstyle tl)
- | oldstyle ((name,typ,CMixfix(x))::tl) =
- (name,typ,Mixfix.NoSyn)::
- (oldstyle tl)
- | oldstyle [] = [];
-
-(* generating the external purely syntactical infix functions.
- Called by add_ext_axioms(_i) *)
-fun syn_decls curried sign ((name,typ,CInfixl(i))::tl) =
- (name,op_to_fun curried sign typ,Mixfix.Infixl(i))::
- (syn_decls curried sign tl)
- | syn_decls curried sign ((name,typ,CInfixr(i))::tl) =
- (name,op_to_fun curried sign typ,Mixfix.Infixr(i))::
- (syn_decls curried sign tl)
- | syn_decls curried sign ((name,typ,CMixfix(x))::tl) =
- (name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
-
- (syn_decls curried sign tl)
- | syn_decls curried sign (_::tl) = syn_decls curried sign tl
- | syn_decls _ _ [] = [];
-
-fun translate name vars rhs =
- Syntax.ParsePrintRule ((Ast.mk_appl (Constant (mk_internal_name name))
- (map Variable vars)),
- rhs);
-
-(* generating the translation rules. Called by add_ext_axioms(_i) *)
-local open Ast in
-fun xrules_of true ((name,typ,CInfixl(i))::tail) =
- translate name ["A","B"]
- (mk_appl (Constant "@fapp")
- [(mk_appl (Constant "@fapp")
- [Constant (mk_internal_name name),Variable "A"]),Variable "B"])
- ::xrules_of true tail
- | xrules_of true ((name,typ,CInfixr(i))::tail) =
- translate name ["A","B"]
- (mk_appl (Constant "@fapp")
- [(mk_appl (Constant "@fapp")
- [Constant (mk_internal_name name),Variable "A"]),Variable "B"])
- ::xrules_of true tail
-(*####*)
- | xrules_of true ((name,typ,CMixfix(_))::tail) =
- let fun argnames n (Type(name ,[_,t]))= if name = cfun_arrow then
- chr n :: argnames (n+1) t else []
- | argnames _ _ = [];
- val names = argnames (ord"A") typ;
- in if names = [] then [] else
- [Syntax.ParsePrintRule (mk_appl (Constant name) (map Variable names),
- foldl (fn (t,arg) =>
- (mk_appl (Constant "@fapp") [t,Variable arg]))
- (Constant name,names))]
- end
- @xrules_of true tail
-(*####*)
- | xrules_of false ((name,typ,CInfixl(i))::tail) =
- translate name ["A","B"]
- (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
- (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
- ::xrules_of false tail
- | xrules_of false ((name,typ,CInfixr(i))::tail) =
- translate name ["A","B"]
- (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
- (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
- ::xrules_of false tail
-(*####*)
- | xrules_of false ((name,typ,CMixfix(_))::tail) =
- let fun foldr' f l =
- let fun itr [] = raise LIST "foldr'"
- | itr [a] = a
- | itr (a::l) = f(a, itr l)
- in itr l end;
- fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
- | argnames n _ = [chr n];
- val vars = map Variable (case typ of (Type(name ,[t,_])) =>
- if name = cfun_arrow then argnames (ord"A") t else []
- | _ => []);
- in if vars = [] then [] else
- [Syntax.ParsePrintRule
- (mk_appl (Constant name) vars,
- mk_appl (Constant "@fapp")
- [Constant name,
- case vars of [v] => v
- | args => mk_appl (Constant "@ctuple")
- [hd args,
- foldr' (fn (t,arg) =>
- mk_appl (Constant "_args")
- [t,arg]) (tl args)]])]
- end
- @xrules_of false tail
-(*####*)
- | xrules_of c ((name,typ,Mixfix(_))::tail) = xrules_of c tail
- | xrules_of _ [] = [];
-end;
-(**** producing the new axioms ****************)
-
-datatype arguments = Curried_args of ((typ*typ) list) |
- Tupeled_args of (typ list);
-
-fun num_of_args (Curried_args l) = length l
- | num_of_args (Tupeled_args l) = length l;
-
-fun types_of (Curried_args l) = map fst l
- | types_of (Tupeled_args l) = l;
-
-fun mk_mkNotEqUU_vars (typ::tl) cnt = mkNotEqUU (Free("x"^(string_of_int cnt),typ))::
- (mk_mkNotEqUU_vars tl (cnt+1))
- | mk_mkNotEqUU_vars [] _ = [];
-
-local
- (* T1*...*Tn goes to [T1,...,Tn] *)
- fun args_of_tupel (Type("*",[left,right])) = left::(args_of_tupel right)
- | args_of_tupel T = [T];
-
- (* A1->...->An->R goes to [(A1,B1),...,(An,Bn)] where Bi=Ai->...->An->R
- Bi is the Type of the function that is applied to an Ai type argument *)
- fun args_of_curried (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
- (S,typ) :: args_of_curried T else []
- | args_of_curried _ = [];
-in
- fun args_of_op true typ = Curried_args(rev(args_of_curried typ))
- | args_of_op false (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
- Tupeled_args(args_of_tupel S) else Tupeled_args([])
- | args_of_op false _ = Tupeled_args([]);
-end;
-
-(* generates for the type t the type of the fapp constant
- that will be applied to t *)
-fun mk_fapp_typ (typ as Type(_(*"->"*),argl)) = Type("fun",[typ,Type("fun",argl)])
- | mk_fapp_typ t = (
- error("Internal error:mk_fapp_typ: wrong argument\n"));
-
-fun mk_arg_tupel_UU uu_pos [typ] n =
- if n<>uu_pos then Free("x"^(string_of_int n),typ)
- else Const("UU",typ)
- | mk_arg_tupel_UU uu_pos (typ::tail) n =
- mkCPair
- (if n<>uu_pos then Free("x"^(string_of_int n),typ)
- else Const("UU",typ))
- (mk_arg_tupel_UU uu_pos tail (n+1))
- | mk_arg_tupel_UU _ [] _ = error("Internal error:mk_arg_tupel: empty list");
-
-fun mk_app_UU cnt uu_pos fname (Curried_args((typ,ftyp)::tl)) =
- Const("fapp",mk_fapp_typ ftyp) $
- (mk_app_UU (cnt-1) uu_pos fname (Curried_args tl))$
- (if cnt = uu_pos then Const("UU",typ)
- else Free("x"^(string_of_int cnt),typ))
- | mk_app_UU _ _ (name,typ) (Curried_args []) = Const(name,typ)
- | mk_app_UU cnt uu_pos (name,typ) (Tupeled_args []) = Const(name,typ)
- | mk_app_UU cnt uu_pos (name,typ) (Tupeled_args list) =
- Const("fapp",mk_fapp_typ typ) $ Const(name,typ) $
- mk_arg_tupel_UU uu_pos list 0;
-
-fun mk_app cnt fname args = mk_app_UU cnt (~1) fname args;
-
-(* producing the strictness axioms *)
-local
- fun s_axm_of curried name typ args num cnt =
- if cnt = num then
- error("Internal error: s_axm_of: arg is no operation "^(external name))
- else
- let val app = mk_app_UU (num-1) cnt (internal name,typ) args
- val equation = HOLogic.mk_eq(app,Const("UU",fastype_of app))
- in
- if cnt = num-1 then equation
- else And $ equation $
- s_axm_of curried name typ args num (cnt+1)
- end;
-in
- fun strictness_axms curried ((rawname,typ,cmixfix)::tail) =
- let val name = case cmixfix of
- (CInfixl _) => (mk_internal_name rawname,rawname)
- | (CInfixr _) => (mk_internal_name rawname,rawname)
- | _ => (rawname,rawname)
- val args = args_of_op curried typ;
- val num = num_of_args args;
- in
- ((external name)^"_strict",
- if num <> 0
- then HOLogic.mk_Trueprop(s_axm_of curried name typ args num 0)
- else HOLogic.mk_Trueprop(True)) :: strictness_axms curried tail
- end
- | strictness_axms _ [] = [];
-end; (*local*)
-
-(* producing the totality axioms *)
-
-fun totality_axms curried ((rawname,typ,cmixfix)::tail) =
- let val name = case cmixfix of
- (CInfixl _) => (mk_internal_name rawname,rawname)
- | (CInfixr _) => (mk_internal_name rawname,rawname)
- | _ => (rawname,rawname)
- val args = args_of_op curried typ;
- val prems = mk_mkNotEqUU_vars (if curried then rev (types_of args)
- else (types_of args)) 0;
- val term = mk_app (num_of_args args - 1) (internal name,typ) args;
- in
- ((external name)^"_total",
- if num_of_args args <> 0
- then Logic.list_implies (prems,mkNotEqUU term)
- else HOLogic.mk_Trueprop(True)) :: totality_axms curried tail
- end
- | totality_axms _ [] = [];
-
-
-
-(* the theory extenders ****************************)
-
-fun add_ops {curried,strict,total} raw_decls thy =
- let val {sign,...} = rep_theory thy;
- val decls = map (apsnd_of_three (typ_of o read_ctyp sign)) raw_decls;
- val oldstyledecls = oldstyle decls;
- val syndecls = syn_decls curried sign decls;
- val xrules = xrules_of curried decls;
- val s_axms = (if strict then strictness_axms curried decls else []);
- val t_axms = (if total then totality_axms curried decls else []);
- in
- Theory.add_trrules_i xrules (PureThy.add_store_axioms_i (s_axms @ t_axms)
- (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
- end;
-
-fun add_ops_i {curried,strict,total} decls thy =
- let val {sign,...} = rep_theory thy;
- val oldstyledecls = oldstyle decls;
- val syndecls = syn_decls curried sign decls;
- val xrules = xrules_of curried decls;
- val s_axms = (if strict then strictness_axms curried decls else []);
- val t_axms = (if total then totality_axms curried decls else []);
- in
- Theory.add_trrules_i xrules (PureThy.add_store_axioms_i (s_axms @ t_axms)
- (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
- end;
-
-
-(* parser: ops_decls ********************************)
-
-local open ThyParse
-in
-(* the following is an adapted version of const_decls from thy_parse.ML *)
-
-val names1 = list1 name;
-
-fun split_decls decls = flat (map (fn (xs, y) => map (rpair y) xs) decls);
-
-fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
-
-fun mk_strict_vals [] = ""
- | mk_strict_vals [name] =
- "get_axiom thy \""^name^"_strict\"\n"
- | mk_strict_vals (name::tail) =
- "get_axiom thy \""^name^"_strict\",\n"^
- mk_strict_vals tail;
-
-fun mk_total_vals [] = ""
- | mk_total_vals [name] =
- "get_axiom thy \""^name^"_total\"\n"
- | mk_total_vals (name::tail) =
- "get_axiom thy \""^name^"_total\",\n"^
- mk_total_vals tail;
-
-fun mk_ops_decls (((curried,strict),total),list) =
- (* call for the theory extender *)
- ("|> ThyOps.add_ops \n"^
- "{ curried = "^curried^" , strict = "^strict^
- " , total = "^total^" } \n"^
- (mk_big_list o map mk_triple2) list^";\n"^
- "val strict_axms = []; val total_axms = [];\nval thy = thy\n",
- (* additional declarations *)
- (if strict="true" then "val strict_axms = strict_axms @ [\n"^
- mk_strict_vals (map (strip_quotes o fst) list)^
- "];\n"
- else "")^
- (if total="true" then "val total_axms = total_axms @ [\n"^
- mk_total_vals (map (strip_quotes o fst) list)^
- "];\n"
- else ""));
-
-(* mixfix annotations *)
-
-fun cat_parens pre1 pre2 s = cat pre1 (parens (cat pre2 s));
-
-val infxl = "infixl" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixl";
-val infxr = "infixr" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixr";
-
-val cinfxl = "cinfixl" $$-- !! nat >> cat "ThyOps.CInfixl";
-val cinfxr = "cinfixr" $$-- !! nat >> cat "ThyOps.CInfixr";
-
-val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
-
-val cmixfx = "cmixfix" $$-- string -- !! (opt_pris -- optional nat "max_pri")
- >> (cat "ThyOps.CMixfix" o mk_triple2);
-
-val bindr = "binder" $$--
- !! (string -- ( ("[" $$-- nat --$$ "]") -- nat
- || nat >> (fn n => (n,n))
- ) )
- >> (cat_parens "ThyOps.Mixfix" "Binder" o mk_triple2);
-
-val mixfx = string -- !! (opt_pris -- optional nat "max_pri")
- >> (cat_parens "ThyOps.Mixfix" "Mixfix" o mk_triple2);
-
-fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "ThyOps.Mixfix NoSyn";
-
-val opt_cmixfix = opt_syn (mixfx || infxl || infxr || bindr ||
- cinfxl || cinfxr || cmixfx);
-
-fun ops_decls toks=
- (optional ($$ "curried" >> K "true") "false" --
- optional ($$ "strict" >> K "true") "false" --
- optional ($$ "total" >> K "true") "false" --
- (repeat1 (names1 --$$ "::" -- !! (string -- opt_cmixfix))
- >> split_decls)
- >> mk_ops_decls) toks
-
-end;
-
-(*** new keywords and sections: ******************************************)
-
-val ops_keywords = ["curried","strict","total","cinfixl","cinfixr","cmixfix"];
- (* "::" is already a pure keyword *)
-
-val ops_sections = [("ops" , ops_decls) ];
-
-end; (* the structure ThyOps *)