src/HOL/Tools/Predicate_Compile/core_data.ML
author wenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 54742 7a86358a3c0b
parent 52732 b4da1f2ec73f
child 55437 3fd63b92ea3b
permissions -rw-r--r--
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
     1 (*  Title:      HOL/Tools/Predicate_Compile/core_data.ML
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 
     4 Data of the predicate compiler core.
     5 *)
     6 
     7 signature CORE_DATA =
     8 sig
     9   type mode = Predicate_Compile_Aux.mode
    10   type compilation = Predicate_Compile_Aux.compilation
    11   type compilation_funs = Predicate_Compile_Aux.compilation_funs
    12   
    13   datatype predfun_data = PredfunData of {
    14     definition : thm,
    15     intro : thm,
    16     elim : thm,
    17     neg_intro : thm option
    18   };
    19 
    20   datatype pred_data = PredData of {
    21     intros : (string option * thm) list,
    22     elim : thm option,
    23     preprocessed : bool,
    24     function_names : (compilation * (mode * string) list) list,
    25     predfun_data : (mode * predfun_data) list,
    26     needs_random : mode list
    27   };
    28 
    29   structure PredData : THEORY_DATA
    30   
    31   (* queries *)
    32   val defined_functions : compilation -> Proof.context -> string -> bool
    33   val is_registered : Proof.context -> string -> bool
    34   val function_name_of : compilation -> Proof.context -> string -> mode -> string
    35   val the_elim_of : Proof.context -> string -> thm
    36   val has_elim : Proof.context -> string -> bool
    37   
    38   val needs_random : Proof.context -> string -> mode -> bool
    39   
    40   val predfun_intro_of : Proof.context -> string -> mode -> thm
    41   val predfun_neg_intro_of : Proof.context -> string -> mode -> thm option
    42   val predfun_elim_of : Proof.context -> string -> mode -> thm
    43   val predfun_definition_of : Proof.context -> string -> mode -> thm
    44   
    45   val all_preds_of : Proof.context -> string list
    46   val modes_of: compilation -> Proof.context -> string -> mode list
    47   val all_modes_of : compilation -> Proof.context -> (string * mode list) list
    48   val all_random_modes_of : Proof.context -> (string * mode list) list
    49   val intros_of : Proof.context -> string -> thm list
    50   val names_of : Proof.context -> string -> string option list
    51 
    52   val intros_graph_of : Proof.context -> thm list Graph.T
    53   
    54   (* updaters *)
    55   
    56   val register_predicate : (string * thm list * thm) -> theory -> theory
    57   val register_intros : string * thm list -> theory -> theory
    58 
    59   (* FIXME: naming of function is strange *)
    60   val defined_function_of : compilation -> string -> theory -> theory
    61   val add_intro : string option * thm -> theory -> theory
    62   val set_elim : thm -> theory -> theory
    63   val set_function_name : compilation -> string -> mode -> string -> theory -> theory
    64   val add_predfun_data : string -> mode -> thm * ((thm * thm) * thm option) -> theory -> theory
    65   val set_needs_random : string -> mode list -> theory -> theory
    66   (* sophisticated updaters *)
    67   val extend_intro_graph : string list -> theory -> theory
    68   val preprocess_intros : string -> theory -> theory
    69   
    70   (* alternative function definitions *)
    71   val register_alternative_function : string -> mode -> string -> theory -> theory
    72   val alternative_compilation_of_global : theory -> string -> mode ->
    73     (compilation_funs -> typ -> term) option
    74   val alternative_compilation_of : Proof.context -> string -> mode ->
    75     (compilation_funs -> typ -> term) option
    76   val functional_compilation : string -> mode -> compilation_funs -> typ -> term
    77   val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory
    78   val force_modes_and_compilations : string ->
    79     (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
    80 
    81 end;
    82 
    83 structure Core_Data : CORE_DATA =
    84 struct
    85 
    86 open Predicate_Compile_Aux;
    87 
    88 (* book-keeping *)
    89 
    90 datatype predfun_data = PredfunData of {
    91   definition : thm,
    92   intro : thm,
    93   elim : thm,
    94   neg_intro : thm option
    95 };
    96 
    97 fun rep_predfun_data (PredfunData data) = data;
    98 
    99 fun mk_predfun_data (definition, ((intro, elim), neg_intro)) =
   100   PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
   101 
   102 datatype pred_data = PredData of {
   103   intros : (string option * thm) list,
   104   elim : thm option,
   105   preprocessed : bool,
   106   function_names : (compilation * (mode * string) list) list,
   107   predfun_data : (mode * predfun_data) list,
   108   needs_random : mode list
   109 };
   110 
   111 fun rep_pred_data (PredData data) = data;
   112 
   113 fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
   114   PredData {intros = intros, elim = elim, preprocessed = preprocessed,
   115     function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
   116 
   117 fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
   118   mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
   119 
   120 fun eq_option eq (NONE, NONE) = true
   121   | eq_option eq (SOME x, SOME y) = eq (x, y)
   122   | eq_option eq _ = false
   123 
   124 fun eq_pred_data (PredData d1, PredData d2) = 
   125   eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
   126   eq_option Thm.eq_thm (#elim d1, #elim d2)
   127 
   128 structure PredData = Theory_Data
   129 (
   130   type T = pred_data Graph.T;
   131   val empty = Graph.empty;
   132   val extend = I;
   133   val merge = Graph.merge eq_pred_data;
   134 );
   135 
   136 (* queries *)
   137 
   138 fun lookup_pred_data ctxt name =
   139   Option.map rep_pred_data (try (Graph.get_node (PredData.get (Proof_Context.theory_of ctxt))) name)
   140 
   141 fun the_pred_data ctxt name = case lookup_pred_data ctxt name
   142  of NONE => error ("No such predicate " ^ quote name)  
   143   | SOME data => data;
   144 
   145 val is_registered = is_some oo lookup_pred_data
   146 
   147 val all_preds_of = Graph.keys o PredData.get o Proof_Context.theory_of
   148 
   149 val intros_of = map snd o #intros oo the_pred_data
   150 
   151 val names_of = map fst o #intros oo the_pred_data
   152 
   153 fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
   154  of NONE => error ("No elimination rule for predicate " ^ quote name)
   155   | SOME thm => thm
   156   
   157 val has_elim = is_some o #elim oo the_pred_data
   158 
   159 fun function_names_of compilation ctxt name =
   160   case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
   161     NONE => error ("No " ^ string_of_compilation compilation
   162       ^ " functions defined for predicate " ^ quote name)
   163   | SOME fun_names => fun_names
   164 
   165 fun function_name_of compilation ctxt name mode =
   166   case AList.lookup eq_mode
   167     (function_names_of compilation ctxt name) mode of
   168     NONE => error ("No " ^ string_of_compilation compilation
   169       ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
   170   | SOME function_name => function_name
   171 
   172 fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
   173 
   174 fun all_modes_of compilation ctxt =
   175   map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
   176     (all_preds_of ctxt)
   177 
   178 val all_random_modes_of = all_modes_of Random
   179 
   180 fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
   181     NONE => false
   182   | SOME data => AList.defined (op =) (#function_names data) compilation
   183 
   184 fun needs_random ctxt s m =
   185   member (op =) (#needs_random (the_pred_data ctxt s)) m
   186 
   187 fun lookup_predfun_data ctxt name mode =
   188   Option.map rep_predfun_data
   189     (AList.lookup eq_mode (#predfun_data (the_pred_data ctxt name)) mode)
   190 
   191 fun the_predfun_data ctxt name mode =
   192   case lookup_predfun_data ctxt name mode of
   193     NONE => error ("No function defined for mode " ^ string_of_mode mode ^
   194       " of predicate " ^ name)
   195   | SOME data => data;
   196 
   197 val predfun_definition_of = #definition ooo the_predfun_data
   198 
   199 val predfun_intro_of = #intro ooo the_predfun_data
   200 
   201 val predfun_elim_of = #elim ooo the_predfun_data
   202 
   203 val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
   204 
   205 val intros_graph_of =
   206   Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o Proof_Context.theory_of
   207 
   208 fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =
   209   let
   210     val thy = Proof_Context.theory_of ctxt
   211     val nargs = length (binder_types (fastype_of pred))
   212     fun PEEK f dependent_tactic st = dependent_tactic (f st) st
   213     fun meta_eq_of th = th RS @{thm eq_reflection}
   214     val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
   215     fun instantiate i n {context, params, prems, asms, concl, schematics} =
   216       let
   217         fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
   218         fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
   219           |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
   220         val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
   221         val case_th =
   222           rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
   223         val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems
   224         val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
   225         val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
   226           OF (replicate nargs @{thm refl})
   227         val thesis =
   228           Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'
   229             OF prems'
   230       in
   231         (rtac thesis 1)
   232       end
   233     val tac =
   234       etac pre_cases_rule 1
   235       THEN
   236       (PEEK nprems_of
   237         (fn n =>
   238           ALLGOALS (fn i =>
   239             rewrite_goal_tac ctxt [@{thm split_paired_all}] i
   240             THEN (SUBPROOF (instantiate i n) ctxt i))))
   241   in
   242     Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
   243   end
   244 
   245 (* updaters *)
   246 
   247 (* fetching introduction rules or registering introduction rules *)
   248 
   249 val no_compilation = ([], ([], []))
   250 
   251 fun fetch_pred_data ctxt name =
   252   case try (Inductive.the_inductive ctxt) name of
   253     SOME (info as (_, result)) => 
   254       let
   255         fun is_intro_of intro =
   256           let
   257             val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
   258           in (fst (dest_Const const) = name) end;
   259         val thy = Proof_Context.theory_of ctxt
   260         val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
   261         val index = find_index (fn s => s = name) (#names (fst info))
   262         val pre_elim = nth (#elims result) index
   263         val pred = nth (#preds result) index
   264         val elim_t = mk_casesrule ctxt pred intros
   265         val nparams = length (Inductive.params_of (#raw_induct result))
   266         val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
   267       in
   268         mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
   269       end
   270   | NONE => error ("No such predicate: " ^ quote name)
   271 
   272 fun add_predfun_data name mode data =
   273   let
   274     val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
   275   in PredData.map (Graph.map_node name (map_pred_data add)) end
   276 
   277 fun is_inductive_predicate ctxt name =
   278   is_some (try (Inductive.the_inductive ctxt) name)
   279 
   280 fun depending_preds_of ctxt (key, value) =
   281   let
   282     val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value)
   283   in
   284     fold Term.add_const_names intros []
   285       |> (fn cs =>
   286         if member (op =) cs @{const_name "HOL.eq"} then
   287           insert (op =) @{const_name Predicate.eq} cs
   288         else cs)
   289       |> filter (fn c => (not (c = key)) andalso
   290         (is_inductive_predicate ctxt c orelse is_registered ctxt c))
   291   end;
   292 
   293 fun add_intro (opt_case_name, thm) thy =
   294   let
   295     val (name, _) = dest_Const (fst (strip_intro_concl thm))
   296     fun cons_intro gr =
   297      case try (Graph.get_node gr) name of
   298        SOME _ => Graph.map_node name (map_pred_data
   299          (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
   300      | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
   301   in PredData.map cons_intro thy end
   302 
   303 fun set_elim thm =
   304   let
   305     val (name, _) = dest_Const (fst 
   306       (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
   307   in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
   308 
   309 fun register_predicate (constname, intros, elim) thy =
   310   let
   311     val named_intros = map (pair NONE) intros
   312   in
   313     if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
   314       PredData.map
   315         (Graph.new_node (constname,
   316           mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
   317     else thy
   318   end
   319 
   320 fun register_intros (constname, pre_intros) thy =
   321   let
   322     val T = Sign.the_const_type thy constname
   323     fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))
   324     val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then
   325       error ("register_intros: Introduction rules of different constants are used\n" ^
   326         "expected rules for " ^ constname ^ ", but received rules for " ^
   327           commas (map constname_of_intro pre_intros))
   328       else ()
   329     val pred = Const (constname, T)
   330     val pre_elim = 
   331       (Drule.export_without_context o Skip_Proof.make_thm thy)
   332       (mk_casesrule (Proof_Context.init_global thy) pred pre_intros)
   333   in register_predicate (constname, pre_intros, pre_elim) thy end
   334 
   335 fun defined_function_of compilation pred =
   336   let
   337     val set = (apsnd o apfst) (cons (compilation, []))
   338   in
   339     PredData.map (Graph.map_node pred (map_pred_data set))
   340   end
   341 
   342 fun set_function_name compilation pred mode name =
   343   let
   344     val set = (apsnd o apfst)
   345       (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
   346   in
   347     PredData.map (Graph.map_node pred (map_pred_data set))
   348   end
   349 
   350 fun set_needs_random name modes =
   351   let
   352     val set = (apsnd o apsnd o apsnd) (K modes)
   353   in
   354     PredData.map (Graph.map_node name (map_pred_data set))
   355   end  
   356 
   357 fun extend' value_of edges_of key (G, visited) =
   358   let
   359     val (G', v) = case try (Graph.get_node G) key of
   360         SOME v => (G, v)
   361       | NONE => (Graph.new_node (key, value_of key) G, value_of key)
   362     val (G'', visited') = fold (extend' value_of edges_of)
   363       (subtract (op =) visited (edges_of (key, v)))
   364       (G', key :: visited)
   365   in
   366     (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
   367   end;
   368 
   369 fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) 
   370 
   371 fun extend_intro_graph names thy =
   372   let
   373     val ctxt = Proof_Context.init_global thy
   374   in
   375     PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names) thy
   376   end
   377 
   378 fun preprocess_intros name thy =
   379   PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
   380     if preprocessed then (rules, preprocessed)
   381     else
   382       let
   383         val (named_intros, SOME elim) = rules
   384         val named_intros' = map (apsnd (preprocess_intro thy)) named_intros
   385         val pred = Const (name, Sign.the_const_type thy name)
   386         val ctxt = Proof_Context.init_global thy
   387         val elim_t = mk_casesrule ctxt pred (map snd named_intros')
   388         val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
   389       in
   390         ((named_intros', SOME elim'), true)
   391       end))))
   392     thy  
   393 
   394 (* registration of alternative function names *)
   395 
   396 structure Alt_Compilations_Data = Theory_Data
   397 (
   398   type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
   399   val empty = Symtab.empty;
   400   val extend = I;
   401   fun merge data : T = Symtab.merge (K true) data;
   402 );
   403 
   404 fun alternative_compilation_of_global thy pred_name mode =
   405   AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
   406 
   407 fun alternative_compilation_of ctxt pred_name mode =
   408   AList.lookup eq_mode
   409     (Symtab.lookup_list (Alt_Compilations_Data.get (Proof_Context.theory_of ctxt)) pred_name) mode
   410 
   411 fun force_modes_and_compilations pred_name compilations =
   412   let
   413     (* thm refl is a dummy thm *)
   414     val modes = map fst compilations
   415     val (needs_random, non_random_modes) = pairself (map fst)
   416       (List.partition (fn (_, (_, random)) => random) compilations)
   417     val non_random_dummys = map (rpair "dummy") non_random_modes
   418     val all_dummys = map (rpair "dummy") modes
   419     val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
   420       @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
   421     val alt_compilations = map (apsnd fst) compilations
   422   in
   423     PredData.map (Graph.new_node
   424       (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
   425     #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
   426   end
   427 
   428 fun functional_compilation fun_name mode compfuns T =
   429   let
   430     val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
   431       mode (binder_types T)
   432     val bs = map (pair "x") inpTs
   433     val bounds = map Bound (rev (0 upto (length bs) - 1))
   434     val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
   435   in fold_rev Term.abs bs (mk_single compfuns (list_comb (f, bounds))) end
   436 
   437 fun register_alternative_function pred_name mode fun_name =
   438   Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
   439     (pred_name, (mode, functional_compilation fun_name mode)))
   440 
   441 fun force_modes_and_functions pred_name fun_names =
   442   force_modes_and_compilations pred_name
   443     (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
   444     fun_names)
   445 
   446 end;