src/HOL/Tools/functor.ML
author wenzelm
Sat Jul 30 21:10:02 2016 +0200 (2016-07-30)
changeset 63568 e63c8f2fbd28
parent 63120 629a4c5e953e
child 67149 e61557884799
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Tools/functor.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Functorial structure of types.
     5 *)
     6 
     7 signature FUNCTOR =
     8 sig
     9   val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list
    10   val construct_mapper: Proof.context -> (string * bool -> term)
    11     -> bool -> typ -> typ -> term
    12   val functor_: string option -> term -> local_theory -> Proof.state
    13   val functor_cmd: string option -> string -> Proof.context -> Proof.state
    14   type entry
    15   val entries: Proof.context -> entry list Symtab.table
    16 end;
    17 
    18 structure Functor : FUNCTOR =
    19 struct
    20 
    21 (* bookkeeping *)
    22 
    23 val compN = "comp";
    24 val idN = "id";
    25 val compositionalityN = "compositionality";
    26 val identityN = "identity";
    27 
    28 type entry = { mapper: term, variances: (sort * (bool * bool)) list,
    29   comp: thm, id: thm };
    30 
    31 structure Data = Generic_Data
    32 (
    33   type T = entry list Symtab.table
    34   val empty = Symtab.empty
    35   val extend = I
    36   fun merge data = Symtab.merge (K true) data
    37 );
    38 
    39 val entries = Data.get o Context.Proof;
    40 
    41 
    42 (* type analysis *)
    43 
    44 fun term_with_typ ctxt T t =
    45   Envir.subst_term_types
    46     (Sign.typ_match (Proof_Context.theory_of ctxt) (fastype_of t, T) Vartab.empty) t;
    47 
    48 fun find_atomic ctxt T =
    49   let
    50     val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt);
    51     fun add_variance is_contra T =
    52       AList.map_default (op =) (T, (false, false))
    53         ((if is_contra then apsnd else apfst) (K true));
    54     fun analyze' is_contra (_, (co, contra)) T =
    55       (if co then analyze is_contra T else I)
    56       #> (if contra then analyze (not is_contra) T else I)
    57     and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
    58           of NONE => add_variance is_contra T
    59            | SOME variances => fold2 (analyze' is_contra) variances Ts)
    60       | analyze is_contra T = add_variance is_contra T;
    61   in analyze false T [] end;
    62 
    63 fun construct_mapper ctxt atomic =
    64   let
    65     val lookup = hd o Symtab.lookup_list (entries ctxt);
    66     fun constructs is_contra (_, (co, contra)) T T' =
    67       (if co then [construct is_contra T T'] else [])
    68       @ (if contra then [construct (not is_contra) T T'] else [])
    69     and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
    70           let
    71             val { mapper = raw_mapper, variances, ... } = lookup tyco;
    72             val args = maps (fn (arg_pattern, (T, T')) =>
    73               constructs is_contra arg_pattern T T')
    74                 (variances ~~ (Ts ~~ Ts'));
    75             val (U, U') = if is_contra then (T', T) else (T, T');
    76             val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper;
    77           in list_comb (mapper, args) end
    78       | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
    79   in construct end;
    80 
    81 
    82 (* mapper properties *)
    83 
    84 val compositionality_ss =
    85   simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm comp_def}]);
    86 
    87 fun make_comp_prop ctxt variances (tyco, mapper) =
    88   let
    89     val sorts = map fst variances
    90     val (((vs3, vs2), vs1), _) = ctxt
    91       |> Variable.invent_types sorts
    92       ||>> Variable.invent_types sorts
    93       ||>> Variable.invent_types sorts
    94     val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
    95     fun mk_argT ((T, T'), (_, (co, contra))) =
    96       (if co then [(T --> T')] else [])
    97       @ (if contra then [(T' --> T)] else []);
    98     val contras = maps (fn (_, (co, contra)) =>
    99       (if co then [false] else []) @ (if contra then [true] else [])) variances;
   100     val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
   101     val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
   102     fun invents n k nctxt =
   103       let
   104         val names = Name.invent nctxt n k;
   105       in (names, fold Name.declare names nctxt) end;
   106     val ((names21, names32), nctxt) = Variable.names_of ctxt
   107       |> invents "f" (length Ts21)
   108       ||>> invents "f" (length Ts32);
   109     val T1 = Type (tyco, Ts1);
   110     val T2 = Type (tyco, Ts2);
   111     val T3 = Type (tyco, Ts3);
   112     val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
   113     val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
   114       if not is_contra then
   115         HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
   116       else
   117         HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
   118       ) contras (args21 ~~ args32)
   119     fun mk_mapper T T' args = list_comb
   120       (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
   121     val mapper21 = mk_mapper T2 T1 (map Free args21);
   122     val mapper32 = mk_mapper T3 T2 (map Free args32);
   123     val mapper31 = mk_mapper T3 T1 args31;
   124     val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   125       (HOLogic.mk_comp (mapper21, mapper32), mapper31);
   126     val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
   127     val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   128       (mapper21 $ (mapper32 $ x), mapper31 $ x);
   129     val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
   130     val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
   131     fun prove_compositionality ctxt comp_thm =
   132       Goal.prove_sorry ctxt [] [] compositionality_prop
   133         (K (ALLGOALS (Method.insert_tac ctxt [@{thm fun_cong} OF [comp_thm]]
   134           THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
   135           THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
   136   in (comp_prop, prove_compositionality) end;
   137 
   138 val identity_ss =
   139   simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm id_def}]);
   140 
   141 fun make_id_prop ctxt variances (tyco, mapper) =
   142   let
   143     val (vs, _) = Variable.invent_types (map fst variances) ctxt;
   144     val Ts = map TFree vs;
   145     fun bool_num b = if b then 1 else 0;
   146     fun mk_argT (T, (_, (co, contra))) =
   147       replicate (bool_num co + bool_num contra) T
   148     val arg_Ts = maps mk_argT (Ts ~~ variances)
   149     val T = Type (tyco, Ts);
   150     val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper;
   151     val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
   152     val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
   153     val rhs = HOLogic.id_const T;
   154     val (id_prop, identity_prop) =
   155       apply2 (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
   156     fun prove_identity ctxt id_thm =
   157       Goal.prove_sorry ctxt [] [] identity_prop
   158         (K (ALLGOALS (Method.insert_tac ctxt [id_thm] THEN'
   159           Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
   160   in (id_prop, prove_identity) end;
   161 
   162 
   163 (* analyzing and registering mappers *)
   164 
   165 fun consume _ _ [] = (false, [])
   166   | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
   167 
   168 fun split_mapper_typ "fun" T =
   169       let
   170         val (Ts', T') = strip_type T;
   171         val (Ts'', T'') = split_last Ts';
   172         val (Ts''', T''') = split_last Ts'';
   173       in (Ts''', T''', T'' --> T') end
   174   | split_mapper_typ _ T =
   175       let
   176         val (Ts', T') = strip_type T;
   177         val (Ts'', T'') = split_last Ts';
   178       in (Ts'', T'', T') end;
   179 
   180 fun analyze_mapper ctxt input_mapper =
   181   let
   182     val T = fastype_of input_mapper;
   183     val _ = Type.no_tvars T;
   184     val _ =
   185       if null (subtract (op =) (Term.add_tfreesT T []) (Term.add_tfrees input_mapper []))
   186       then ()
   187       else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper);
   188     val _ =
   189       if null (Term.add_vars (singleton
   190         (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
   191       then ()
   192       else error ("Illegal locally free variable(s) in term: "
   193         ^ Syntax.string_of_term ctxt input_mapper);
   194     val mapper = singleton (Variable.polymorphic ctxt) input_mapper;
   195     val _ =
   196       if null (Term.add_tfreesT (fastype_of mapper) []) then ()
   197       else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ ctxt T);
   198     fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
   199       | add_tycos _ = I;
   200     val tycos = add_tycos T [];
   201     val tyco = if tycos = ["fun"] then "fun"
   202       else case remove (op =) "fun" tycos
   203        of [tyco] => tyco
   204         | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ ctxt T);
   205   in (mapper, T, tyco) end;
   206 
   207 fun analyze_variances ctxt tyco T =
   208   let
   209     fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
   210     val (Ts, T1, T2) = split_mapper_typ tyco T
   211       handle List.Empty => bad_typ ();
   212     val _ =
   213       apply2 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
   214         handle TYPE _ => bad_typ ();
   215     val (vs1, vs2) =
   216       apply2 (map dest_TFree o snd o dest_Type) (T1, T2)
   217         handle TYPE _ => bad_typ ();
   218     val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
   219       then bad_typ () else ();
   220     fun check_variance_pair (var1 as (_, sort1), var2 as (_, sort2)) =
   221       let
   222         val coT = TFree var1 --> TFree var2;
   223         val contraT = TFree var2 --> TFree var1;
   224         val sort = Sign.inter_sort (Proof_Context.theory_of ctxt) (sort1, sort2);
   225       in
   226         consume (op =) coT
   227         ##>> consume (op =) contraT
   228         #>> pair sort
   229       end;
   230     val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
   231     val _ = if null left_variances then () else bad_typ ();
   232   in variances end;
   233 
   234 fun gen_functor prep_term some_prfx raw_mapper lthy =
   235   let
   236     val (mapper, T, tyco) = analyze_mapper lthy (prep_term lthy raw_mapper);
   237     val prfx = the_default (Long_Name.base_name tyco) some_prfx;
   238     val variances = analyze_variances lthy tyco T;
   239     val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper);
   240     val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper);
   241     val qualify = Binding.qualify true prfx o Binding.name;
   242     fun mapper_declaration comp_thm id_thm phi context =
   243       let
   244         val typ_instance = Sign.typ_instance (Context.theory_of context);
   245         val mapper' = Morphism.term phi mapper;
   246         val T_T' = apply2 fastype_of (mapper, mapper');
   247         val vars = Term.add_vars mapper' [];
   248       in
   249         if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T')
   250         then (Data.map o Symtab.cons_list) (tyco,
   251           { mapper = mapper', variances = variances,
   252             comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
   253         else context
   254       end;
   255     fun after_qed [single_comp_thm, single_id_thm] lthy =
   256       lthy
   257       |> Local_Theory.note ((qualify compN, []), single_comp_thm)
   258       ||>> Local_Theory.note ((qualify idN, []), single_id_thm)
   259       |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy =>
   260         lthy
   261         |> Local_Theory.note ((qualify compositionalityN, []),
   262             [prove_compositionality lthy comp_thm])
   263         |> snd
   264         |> Local_Theory.note ((qualify identityN, []),
   265             [prove_identity lthy id_thm])
   266         |> snd
   267         |> Local_Theory.declaration {syntax = false, pervasive = false}
   268           (mapper_declaration comp_thm id_thm))
   269   in
   270     lthy
   271     |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
   272   end
   273 
   274 val functor_ = gen_functor Syntax.check_term;
   275 val functor_cmd = gen_functor Syntax.read_term;
   276 
   277 val _ =
   278   Outer_Syntax.local_theory_to_proof @{command_keyword functor}
   279     "register operations managing the functorial structure of a type"
   280     (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term >> uncurry functor_cmd);
   281 
   282 end;