Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
(* TTITLEF/thy_ops.ML
ID: $Id$
Author: Tobias Mayr
Additional theory file section for HOLCF: ops
There's an elaborate but german description of this program,
write to mayrt@informatik.tu-muenchen.de.
For a short english description of the new sections
write to regensbu@informatik.tu-muenchen.de.
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 (Type("->" ,[larg,t]))=
Type("fun",[larg,op_to_fun true sign t])
| op_to_fun false sign (Type("->",[args,res])) = let
fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs])
| otf t = Type("fun",[t,res]);
in otf args end
| op_to_fun _ sign t = t(*error("Wrong type for cinfix/cmixfix : "^
(Sign.string_of_typ sign 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))::
####**)
(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 _ _ [] = [];
(* generating the translation rules. Called by add_ext_axioms(_i) *)
local open Ast in
fun xrules_of true ((name,typ,CInfixl(i))::tail) =
((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "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) =
((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "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("->" ,[_,t]))= chr n :: argnames (n+1) t
| argnames _ _ = [];
val names = argnames (ord"A") typ;
in if names = [] then [] else [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) =
((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "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) =
((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "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("->" ,[t,_])) =>argnames (ord"A") t
| _ => []);
in if vars = [] then [] else [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("->",[S,T]))) =
(S,typ) :: args_of_curried T
| args_of_curried _ = [];
in
fun args_of_op true typ = Curried_args(rev(args_of_curried typ))
| args_of_op false (typ as (Type("->",[S,T]))) =
Tupeled_args(args_of_tupel S)
| 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
add_trrules_i xrules (add_axioms_i (s_axms @ t_axms)
(add_syntax_i syndecls (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
add_trrules_i xrules (add_axioms_i (s_axms @ t_axms)
(add_syntax_i syndecls (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;
val split_decls = flat o map (fn (xs, y) => map (rpair y) xs);
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 *)