src/HOLCF/ax_ops/thy_ops.ML

PureThy.add_store_axioms_i;

(*  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 *)