src/HOLCF/Tools/Domain/domain_extender.ML

slightly less ambitious settings, to avoid potential out-of-memory problem;

(*  Title:      HOLCF/Tools/Domain/domain_extender.ML
    Author:     David von Oheimb

Theory extender for domain command, including theory syntax.
*)

signature DOMAIN_EXTENDER =
sig
  val add_domain_cmd:
      string ->
      ((string * string option) list * binding * mixfix *
       (binding * (bool * binding option * string) list * mixfix) list) list
      -> theory -> theory

  val add_domain:
      string ->
      ((string * string option) list * binding * mixfix *
       (binding * (bool * binding option * typ) list * mixfix) list) list
      -> theory -> theory

  val add_new_domain_cmd:
      string ->
      ((string * string option) list * binding * mixfix *
       (binding * (bool * binding option * string) list * mixfix) list) list
      -> theory -> theory

  val add_new_domain:
      string ->
      ((string * string option) list * binding * mixfix *
       (binding * (bool * binding option * typ) list * mixfix) list) list
      -> theory -> theory
end;

structure Domain_Extender :> DOMAIN_EXTENDER =
struct

open Domain_Library;

(* ----- general testing and preprocessing of constructor list -------------- *)
fun check_and_sort_domain
    (definitional : bool)
    (dtnvs : (string * typ list) list)
    (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
    (thy : theory)
    : ((string * typ list) *
       (binding * (bool * binding option * typ) list * mixfix) list) list =
  let
    val defaultS = Sign.defaultS thy;

    val test_dupl_typs =
      case duplicates (op =) (map fst dtnvs) of 
        [] => false | dups => error ("Duplicate types: " ^ commas_quote dups);

    val all_cons = map (Binding.name_of o first) (flat cons'');
    val test_dupl_cons =
      case duplicates (op =) all_cons of 
        [] => false | dups => error ("Duplicate constructors: " 
                                      ^ commas_quote dups);
    val all_sels =
      (map Binding.name_of o map_filter second o maps second) (flat cons'');
    val test_dupl_sels =
      case duplicates (op =) all_sels of
        [] => false | dups => error("Duplicate selectors: "^commas_quote dups);

    fun test_dupl_tvars s =
      case duplicates (op =) (map(fst o dest_TFree)s) of
        [] => false | dups => error("Duplicate type arguments: " 
                                    ^commas_quote dups);
    val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs);

    (* test for free type variables, illegal sort constraints on rhs,
       non-pcpo-types and invalid use of recursive type;
       replace sorts in type variables on rhs *)
    fun analyse_equation ((dname,typevars),cons') = 
      let
        val tvars = map dest_TFree typevars;
        val distinct_typevars = map TFree tvars;
        fun rm_sorts (TFree(s,_)) = TFree(s,[])
          | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
          | rm_sorts (TVar(s,_))  = TVar(s,[])
        and remove_sorts l = map rm_sorts l;
        val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
        fun analyse indirect (TFree(v,s))  =
            (case AList.lookup (op =) tvars v of 
               NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
             | SOME sort => if eq_set (op =) (s, defaultS) orelse
                               eq_set (op =) (s, sort)
                            then TFree(v,sort)
                            else error ("Inconsistent sort constraint" ^
                                        " for type variable " ^ quote v))
          | analyse indirect (t as Type(s,typl)) =
            (case AList.lookup (op =) dtnvs s of
               NONE =>
                 if definitional orelse s mem indirect_ok
                 then Type(s,map (analyse false) typl)
                 else Type(s,map (analyse true) typl)
             | SOME typevars =>
                 if indirect 
                 then error ("Indirect recursion of type " ^ 
                             quote (string_of_typ thy t))
                 else if dname <> s orelse
                         (** BUG OR FEATURE?:
                             mutual recursion may use different arguments **)
                         remove_sorts typevars = remove_sorts typl 
                 then Type(s,map (analyse true) typl)
                 else error ("Direct recursion of type " ^ 
                             quote (string_of_typ thy t) ^ 
                             " with different arguments"))
          | analyse indirect (TVar _) = Imposs "extender:analyse";
        fun check_pcpo lazy T =
            let val ok = if lazy then cpo_type else pcpo_type
            in if ok thy T then T
               else error ("Constructor argument type is not of sort pcpo: " ^
                           string_of_typ thy T)
            end;
        fun analyse_arg (lazy, sel, T) =
            (lazy, sel, check_pcpo lazy (analyse false T));
        fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
      in ((dname,distinct_typevars), map analyse_con cons') end; 
  in ListPair.map analyse_equation (dtnvs,cons'')
  end; (* let *)

(* ----- calls for building new thy and thms -------------------------------- *)

fun gen_add_domain
    (prep_typ : theory -> 'a -> typ)
    (comp_dnam : string)
    (eqs''' : ((string * string option) list * binding * mixfix *
               (binding * (bool * binding option * 'a) list * mixfix) list) list)
    (thy''' : theory) =
  let
    fun readS (SOME s) = Syntax.read_sort_global thy''' s
      | readS NONE = Sign.defaultS thy''';
    fun readTFree (a, s) = TFree (a, readS s);

    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
                        (dname, map readTFree vs, mx)) eqs''';
    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
    fun thy_arity (dname,tvars,mx) =
        (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
    val thy'' =
      thy'''
      |> Sign.add_types (map thy_type dtnvs)
      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
    val cons'' =
      map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
    val dtnvs' =
      map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
    val eqs' : ((string * typ list) *
        (binding * (bool * binding option * typ) list * mixfix) list) list =
      check_and_sort_domain false dtnvs' cons'' thy'';
    val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
    val dts  = map (Type o fst) eqs';
    val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
    fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
    fun typid (Type  (id,_)) =
        let val c = hd (Symbol.explode (Long_Name.base_name id))
        in if Symbol.is_letter c then c else "t" end
      | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
      | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
    fun one_con (con,args,mx) =
        ((Syntax.const_name mx (Binding.name_of con)),
         ListPair.map (fn ((lazy,sel,tp),vn) =>
           mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
                   Option.map Binding.name_of sel,vn))
                      (args,(mk_var_names(map (typid o third) args)))
        ) : cons;
    val eqs : eq list =
        map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
    val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs;
    val ((rewss, take_rews), theorems_thy) =
        thy
          |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
  in
    theorems_thy
      |> Sign.add_path (Long_Name.base_name comp_dnam)
      |> PureThy.add_thmss
           [((Binding.name "rews", flat rewss @ take_rews), [])]
      |> snd
      |> Sign.parent_path
  end;

fun gen_add_new_domain
    (prep_typ : theory -> 'a -> typ)
    (comp_dnam : string)
    (eqs''' : ((string * string option) list * binding * mixfix *
               (binding * (bool * binding option * 'a) list * mixfix) list) list)
    (thy''' : theory) =
  let
    fun readS (SOME s) = Syntax.read_sort_global thy''' s
      | readS NONE = Sign.defaultS thy''';
    fun readTFree (a, s) = TFree (a, readS s);

    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
                        (dname, map readTFree vs, mx)) eqs''';
    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
    fun thy_arity (dname,tvars,mx) =
      (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, @{sort rep});

    (* this theory is used just for parsing and error checking *)
    val tmp_thy = thy'''
      |> Theory.copy
      |> Sign.add_types (map thy_type dtnvs)
      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;

    val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list =
      map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
    val dtnvs' : (string * typ list) list =
      map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
    val eqs' : ((string * typ list) *
        (binding * (bool * binding option * typ) list * mixfix) list) list =
      check_and_sort_domain true dtnvs' cons'' tmp_thy;

    fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
    fun mk_con_typ (bind, args, mx) =
        if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
    fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
    
    val thy'' = thy''' |>
      Domain_Isomorphism.domain_isomorphism
        (map (fn ((vs, dname, mx, _), eq) =>
                 (map fst vs, dname, mx, mk_eq_typ eq))
             (eqs''' ~~ eqs'))

    val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
    val dts  = map (Type o fst) eqs';
    val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
    fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
    fun typid (Type  (id,_)) =
        let val c = hd (Symbol.explode (Long_Name.base_name id))
        in if Symbol.is_letter c then c else "t" end
      | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
      | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
    fun one_con (con,args,mx) =
        ((Syntax.const_name mx (Binding.name_of con)),
         ListPair.map (fn ((lazy,sel,tp),vn) =>
           mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
                   Option.map Binding.name_of sel,vn))
                      (args,(mk_var_names(map (typid o third) args)))
        ) : cons;
    val eqs : eq list =
        map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
    val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs;
    val ((rewss, take_rews), theorems_thy) =
        thy
          |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
  in
    theorems_thy
      |> Sign.add_path (Long_Name.base_name comp_dnam)
      |> PureThy.add_thmss
           [((Binding.name "rews", flat rewss @ take_rews), [])]
      |> snd
      |> Sign.parent_path
  end;

val add_domain = gen_add_domain Sign.certify_typ;
val add_domain_cmd = gen_add_domain Syntax.read_typ_global;

val add_new_domain = gen_add_new_domain Sign.certify_typ;
val add_new_domain_cmd = gen_add_new_domain Syntax.read_typ_global;


(** outer syntax **)

local structure P = OuterParse and K = OuterKeyword in

val _ = OuterKeyword.keyword "lazy";

val dest_decl : (bool * binding option * string) parser =
  P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
    (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
    || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
    >> (fn t => (true,NONE,t))
    || P.typ >> (fn t => (false,NONE,t));

val cons_decl =
  P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;

val type_var' : (string * string option) parser =
  (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));

val type_args' : (string * string option) list parser =
  type_var' >> single
  || P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")")
  || Scan.succeed [];

val domain_decl =
  (type_args' -- P.binding -- P.opt_infix) --
    (P.$$$ "=" |-- P.enum1 "|" cons_decl);

val domains_decl =
  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
    P.and_list1 domain_decl;

fun mk_domain
    (definitional : bool)
    (opt_name : string option,
     doms : ((((string * string option) list * binding) * mixfix) *
             ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
  let
    val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
    val specs : ((string * string option) list * binding * mixfix *
                 (binding * (bool * binding option * string) list * mixfix) list) list =
        map (fn (((vs, t), mx), cons) =>
                (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
    val comp_dnam =
        case opt_name of NONE => space_implode "_" names | SOME s => s;
  in
    if definitional 
    then add_new_domain_cmd comp_dnam specs
    else add_domain_cmd comp_dnam specs
  end;

val _ =
  OuterSyntax.command "domain" "define recursive domains (HOLCF)"
    K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));

val _ =
  OuterSyntax.command "new_domain" "define recursive domains (HOLCF)"
    K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));

end;

end;