src/HOLCF/Tools/Domain/domain_extender.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32952 aeb1e44fbc19
child 33038 8f9594c31de4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 (*  Title:      HOLCF/Tools/Domain/domain_extender.ML
     2     Author:     David von Oheimb
     3 
     4 Theory extender for domain command, including theory syntax.
     5 *)
     6 
     7 signature DOMAIN_EXTENDER =
     8 sig
     9   val add_domain_cmd: string ->
    10                       ((string * string option) list * binding * mixfix *
    11                        (binding * (bool * binding option * string) list * mixfix) list) list
    12                       -> theory -> theory
    13   val add_domain: string ->
    14                   ((string * string option) list * binding * mixfix *
    15                    (binding * (bool * binding option * typ) list * mixfix) list) list
    16                   -> theory -> theory
    17 end;
    18 
    19 structure Domain_Extender :> DOMAIN_EXTENDER =
    20 struct
    21 
    22 open Domain_Library;
    23 
    24 (* ----- general testing and preprocessing of constructor list -------------- *)
    25 fun check_and_sort_domain
    26       (dtnvs : (string * typ list) list)
    27       (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
    28       (sg : theory)
    29     : ((string * typ list) *
    30        (binding * (bool * binding option * typ) list * mixfix) list) list =
    31     let
    32       val defaultS = Sign.defaultS sg;
    33       val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
    34                               [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
    35       val test_dupl_cons =
    36           (case duplicates (op =) (map (Binding.name_of o first) (flat cons'')) of 
    37              [] => false | dups => error ("Duplicate constructors: " 
    38                                           ^ commas_quote dups));
    39       val test_dupl_sels =
    40           (case duplicates (op =) (map Binding.name_of (map_filter second
    41                                                                         (maps second (flat cons'')))) of
    42              [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
    43       val test_dupl_tvars =
    44           exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
    45                          [] => false | dups => error("Duplicate type arguments: " 
    46                                                      ^commas_quote dups)) (map snd dtnvs);
    47       (* test for free type variables, illegal sort constraints on rhs,
    48          non-pcpo-types and invalid use of recursive type;
    49          replace sorts in type variables on rhs *)
    50       fun analyse_equation ((dname,typevars),cons') = 
    51           let
    52             val tvars = map dest_TFree typevars;
    53             val distinct_typevars = map TFree tvars;
    54             fun rm_sorts (TFree(s,_)) = TFree(s,[])
    55               | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
    56               | rm_sorts (TVar(s,_))  = TVar(s,[])
    57             and remove_sorts l = map rm_sorts l;
    58             val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
    59             fun analyse indirect (TFree(v,s))  =
    60                 (case AList.lookup (op =) tvars v of 
    61                    NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
    62                  | SOME sort => if gen_eq_set (op =) (s, defaultS) orelse
    63                                    gen_eq_set (op =) (s, sort)
    64                                 then TFree(v,sort)
    65                                 else error ("Inconsistent sort constraint" ^
    66                                             " for type variable " ^ quote v))
    67               | analyse indirect (t as Type(s,typl)) =
    68                 (case AList.lookup (op =) dtnvs s of
    69                    NONE          => if s mem indirect_ok
    70                                     then Type(s,map (analyse false) typl)
    71                                     else Type(s,map (analyse true) typl)
    72                  | SOME typevars => if indirect 
    73                                     then error ("Indirect recursion of type " ^ 
    74                                                 quote (string_of_typ sg t))
    75                                     else if dname <> s orelse
    76                                             (** BUG OR FEATURE?:
    77                                                 mutual recursion may use different arguments **)
    78                                             remove_sorts typevars = remove_sorts typl 
    79                                     then Type(s,map (analyse true) typl)
    80                                     else error ("Direct recursion of type " ^ 
    81                                                 quote (string_of_typ sg t) ^ 
    82                                                 " with different arguments"))
    83               | analyse indirect (TVar _) = Imposs "extender:analyse";
    84             fun check_pcpo lazy T =
    85                 let val ok = if lazy then cpo_type else pcpo_type
    86                 in if ok sg T then T else error
    87                                             ("Constructor argument type is not of sort pcpo: " ^
    88                                              string_of_typ sg T)
    89                 end;
    90             fun analyse_arg (lazy, sel, T) =
    91                 (lazy, sel, check_pcpo lazy (analyse false T));
    92             fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
    93           in ((dname,distinct_typevars), map analyse_con cons') end; 
    94     in ListPair.map analyse_equation (dtnvs,cons'')
    95     end; (* let *)
    96 
    97 (* ----- calls for building new thy and thms -------------------------------- *)
    98 
    99 fun gen_add_domain
   100       (prep_typ : theory -> 'a -> typ)
   101       (comp_dnam : string)
   102       (eqs''' : ((string * string option) list * binding * mixfix *
   103                  (binding * (bool * binding option * 'a) list * mixfix) list) list)
   104       (thy''' : theory) =
   105     let
   106       fun readS (SOME s) = Syntax.read_sort_global thy''' s
   107         | readS NONE = Sign.defaultS thy''';
   108       fun readTFree (a, s) = TFree (a, readS s);
   109 
   110       val dtnvs = map (fn (vs,dname:binding,mx,_) => 
   111                           (dname, map readTFree vs, mx)) eqs''';
   112       val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
   113       fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
   114       fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
   115       val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
   116                          |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
   117       val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
   118       val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
   119       val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list =
   120           check_and_sort_domain dtnvs' cons'' thy'';
   121       val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
   122       val dts  = map (Type o fst) eqs';
   123       val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
   124       fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
   125       fun typid (Type  (id,_)) =
   126           let val c = hd (Symbol.explode (Long_Name.base_name id))
   127           in if Symbol.is_letter c then c else "t" end
   128         | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
   129         | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
   130       fun one_con (con,args,mx) =
   131           ((Syntax.const_name mx (Binding.name_of con)),
   132            ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
   133                                                            DatatypeAux.dtyp_of_typ new_dts tp),
   134                                                           Option.map Binding.name_of sel,vn))
   135                         (args,(mk_var_names(map (typid o third) args)))
   136           ) : cons;
   137       val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
   138       val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
   139       val ((rewss, take_rews), theorems_thy) =
   140           thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
   141               ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
   142     in
   143       theorems_thy
   144         |> Sign.add_path (Long_Name.base_name comp_dnam)
   145         |> (snd o (PureThy.add_thmss [((Binding.name "rews", flat rewss @ take_rews), [])]))
   146         |> Sign.parent_path
   147     end;
   148 
   149 val add_domain = gen_add_domain Sign.certify_typ;
   150 val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
   151 
   152 
   153 (** outer syntax **)
   154 
   155 local structure P = OuterParse and K = OuterKeyword in
   156 
   157 val _ = OuterKeyword.keyword "lazy";
   158 
   159 val dest_decl : (bool * binding option * string) parser =
   160     P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
   161       (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
   162       || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
   163       >> (fn t => (true,NONE,t))
   164       || P.typ >> (fn t => (false,NONE,t));
   165 
   166 val cons_decl =
   167     P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
   168 
   169 val type_var' : (string * string option) parser =
   170     (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
   171 
   172 val type_args' : (string * string option) list parser =
   173     type_var' >> single ||
   174               P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
   175               Scan.succeed [];
   176 
   177 val domain_decl =
   178     (type_args' -- P.binding -- P.opt_infix) --
   179                                              (P.$$$ "=" |-- P.enum1 "|" cons_decl);
   180 
   181 val domains_decl =
   182     Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
   183                 P.and_list1 domain_decl;
   184 
   185 fun mk_domain (opt_name : string option,
   186                doms : ((((string * string option) list * binding) * mixfix) *
   187                        ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
   188     let
   189       val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
   190       val specs : ((string * string option) list * binding * mixfix *
   191                    (binding * (bool * binding option * string) list * mixfix) list) list =
   192           map (fn (((vs, t), mx), cons) =>
   193                   (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
   194       val comp_dnam =
   195           case opt_name of NONE => space_implode "_" names | SOME s => s;
   196     in add_domain_cmd comp_dnam specs end;
   197 
   198 val _ =
   199     OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
   200                         (domains_decl >> (Toplevel.theory o mk_domain));
   201 
   202 end;
   203 
   204 end;