src/Pure/Isar/expression.ML
author ballarin
Fri Nov 14 16:49:52 2008 +0100 (2008-11-14)
changeset 28795 6891e273c33b
parent 28701 ca5840b1f7b3
child 28832 cf7237498e7a
permissions -rw-r--r--
Initial part of locale reimplementation.
     1 (*  Title:      Pure/Isar/expression.ML
     2     ID:         $Id$
     3     Author:     Clemens Ballarin, TU Muenchen
     4 
     5 New locale development --- experimental.
     6 *)
     7 
     8 signature EXPRESSION =
     9 sig
    10   type map
    11   type 'morph expr
    12 
    13   val empty_expr: 'morph expr
    14 
    15   type expression = (string * map) expr * (Name.binding * string option * mixfix) list
    16   type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list
    17 
    18   (* Declaring locales *)
    19   val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
    20     string * Proof.context
    21 (*
    22   val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    23     string * Proof.context
    24 *)
    25 
    26   (* Debugging and development *)
    27   val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    28   val debug_parameters: expression -> Proof.context -> Proof.context
    29   val debug_context: expression -> Proof.context -> Proof.context
    30 
    31 end;
    32 
    33 
    34 structure Expression: EXPRESSION =
    35 struct
    36 
    37 datatype ctxt = datatype Element.ctxt;
    38 
    39 
    40 (*** Expressions ***)
    41 
    42 datatype map =
    43   Positional of string option list |
    44   Named of (string * string) list;
    45 
    46 datatype 'morph expr = Expr of (string * 'morph) list;
    47 
    48 type expression = (string * map) expr * (Name.binding * string option * mixfix) list;
    49 type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list;
    50 
    51 val empty_expr = Expr [];
    52 
    53 
    54 (** Parsing and printing **)
    55 
    56 local
    57 
    58 structure P = OuterParse;
    59 
    60 val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    61    P.$$$ "defines" || P.$$$ "notes";
    62 fun plus1_unless test scan =
    63   scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    64 
    65 val prefix = P.name --| P.$$$ ":";
    66 val named = P.name -- (P.$$$ "=" |-- P.term);
    67 val position = P.maybe P.term;
    68 val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
    69   Scan.repeat1 position >> Positional;
    70 
    71 in
    72 
    73 val parse_expression =
    74   let
    75     fun expr2 x = P.xname x;
    76     fun expr1 x = (Scan.optional prefix "" -- expr2 --
    77       Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    78     fun expr0 x = (plus1_unless loc_keyword expr1 >> Expr) x;
    79   in expr0 -- P.for_fixes end;
    80 
    81 end;
    82 
    83 fun pretty_expr thy (Expr expr) =
    84   let
    85     fun pretty_pos NONE = Pretty.str "_"
    86       | pretty_pos (SOME x) = Pretty.str x;
    87     fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=",
    88           Pretty.brk 1, Pretty.str y] |> Pretty.block;
    89     fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |>
    90           map pretty_pos |> Pretty.breaks
    91       | pretty_ren (Named []) = []
    92       | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 ::
    93           (ps |> map pretty_named |> Pretty.separate "and");
    94     fun pretty_rename (loc, ("", ren)) =
    95           Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) 
    96       | pretty_rename (loc, (prfx, ren)) =
    97           Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) ::
    98             Pretty.brk 1 :: pretty_ren ren);
    99   in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
   100 
   101 fun err_in_expr thy msg (Expr expr) =
   102   let
   103     val err_msg =
   104       if null expr then msg
   105       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   106         [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
   107           pretty_expr thy (Expr expr)])
   108   in error err_msg end;
   109 
   110 
   111 (** Internalise locale names **)
   112 
   113 fun intern_expr thy (Expr instances) = Expr (map (apfst (NewLocale.intern thy)) instances);
   114 
   115 
   116 (** Parameters of expression (not expression_i).
   117    Sanity check of instantiations.
   118    Positional instantiations are extended to match full length of parameter list. **)
   119 
   120 fun parameters thy (expr, fixed : (Name.binding * string option * mixfix) list) =
   121   let
   122     fun reject_dups message xs =
   123       let val dups = duplicates (op =) xs
   124       in
   125         if null dups then () else error (message ^ commas dups)
   126       end;
   127 
   128     fun match_bind (n, b) = (n = Name.name_of b);
   129     fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
   130       (* FIXME: cannot compare bindings for equality. *)
   131 
   132     fun params_loc loc =
   133           (NewLocale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc)
   134             handle ERROR msg => err_in_expr thy msg (Expr [(loc, ("", Named []))]);
   135     fun params_inst (expr as (loc, (prfx, Positional insts))) =
   136           let
   137             val (ps, loc') = params_loc loc;
   138 	    val d = length ps - length insts;
   139 	    val insts' =
   140 	      if d < 0 then err_in_expr thy "More arguments than parameters in instantiation."
   141                 (Expr [expr])
   142 	      else insts @ replicate d NONE;
   143             val ps' = (ps ~~ insts') |>
   144               map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
   145           in
   146             (ps', (loc', (prfx, Positional insts')))
   147           end
   148       | params_inst (expr as (loc, (prfx, Named insts))) =
   149           let
   150             val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
   151               (map fst insts)
   152               handle ERROR msg => err_in_expr thy msg (Expr [expr]);
   153 
   154             val (ps, loc') = params_loc loc;
   155             val ps' = fold (fn (p, _) => fn ps =>
   156               if AList.defined match_bind ps p then AList.delete match_bind p ps
   157               else err_in_expr thy (quote p ^" not a parameter of instantiated expression.")
   158                 (Expr [expr])) insts ps;
   159           in
   160             (ps', (loc', (prfx, Named insts)))
   161           end;
   162     fun params_expr (Expr is) =
   163           let
   164             val (is', ps') = fold_map (fn i => fn ps =>
   165               let
   166                 val (ps', i') = params_inst i;
   167                 val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) =>
   168                   (* FIXME: should check for bindings being the same.
   169                      Instead we check for equal name and syntax. *)
   170                   if mx1 = mx2 then mx1
   171                   else err_in_expr thy ("Conflicting syntax for parameter" ^ quote (Name.name_of p) ^ " in expression.")
   172                     (Expr is)) (ps, ps')
   173               in (i', ps'') end) is []
   174           in
   175             (ps', Expr is')
   176           end;
   177 
   178     val (parms, expr') = params_expr expr;
   179 
   180     val parms' = map (fst #> Name.name_of) parms;
   181     val fixed' = map (#1 #> Name.name_of) fixed;
   182     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   183     val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
   184 
   185   in (expr', (parms, fixed)) end;
   186 
   187 
   188 (** Read instantiation **)
   189 
   190 fun read_inst parse_term parms (prfx, insts) ctxt =
   191   let
   192     (* parameters *)
   193     val (parm_names, parm_types) = split_list parms;
   194     val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   195 
   196     (* parameter instantiations *)
   197     val insts' = case insts of
   198       Positional insts => (insts ~~ parm_names) |> map (fn
   199         (NONE, p) => parse_term ctxt p |
   200         (SOME t, _) => parse_term ctxt t) |
   201       Named insts => parm_names |> map (fn
   202         p => case AList.lookup (op =) insts p of
   203           SOME t => parse_term ctxt t |
   204           NONE => parse_term ctxt p);
   205 
   206     (* type inference and contexts *)
   207     val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   208     val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   209     val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   210     val res = Syntax.check_terms ctxt arg;
   211     val ctxt' = ctxt |> fold Variable.auto_fixes res;
   212 
   213     (* instantiation *)
   214     val (type_parms'', res') = chop (length type_parms) res;
   215     val insts'' = (parm_names ~~ res') |> map_filter
   216       (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
   217         inst => SOME inst);
   218     val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
   219     val inst = Symtab.make insts'';
   220   in
   221     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
   222       Morphism.name_morphism (Name.qualified prfx), ctxt')
   223   end;
   224         
   225         
   226 (** Debugging **)
   227   
   228 fun debug_parameters raw_expr ctxt =
   229   let
   230     val thy = ProofContext.theory_of ctxt;
   231     val expr = apfst (intern_expr thy) raw_expr;
   232     val (expr', (parms, fixed)) = parameters thy expr;
   233   in ctxt end;
   234 
   235 
   236 fun debug_context (raw_expr, fixed) ctxt =
   237   let
   238     val thy = ProofContext.theory_of ctxt;
   239     val expr = intern_expr thy raw_expr;
   240     val (expr', (parms, fixed)) = parameters thy (expr, fixed);
   241 
   242     fun declare_parameters (parms, fixed) ctxt =
   243       let
   244       val (parms', ctxt') =
   245         ProofContext.add_fixes (map (fn (p, mx) => (p, NONE, mx)) parms) ctxt;
   246       val (fixed', ctxt'') =
   247         ProofContext.add_fixes fixed ctxt';
   248       in
   249         (parms' @ fixed', ctxt'')
   250       end;
   251 
   252     fun rough_inst loc prfx insts ctxt =
   253       let
   254         (* locale data *)
   255         val (parm_names, parm_types) = loc |> NewLocale.params_of thy |>
   256           map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   257 
   258         (* type parameters *)
   259         val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   260 
   261         (* parameter instantiations *)
   262         val insts' = case insts of
   263           Positional insts => (insts ~~ parm_names) |> map (fn
   264             (NONE, p) => Syntax.parse_term ctxt p |
   265             (SOME t, _) => Syntax.parse_term ctxt t) |
   266           Named insts => parm_names |> map (fn
   267             p => case AList.lookup (op =) insts p of
   268               SOME t => Syntax.parse_term ctxt t |
   269               NONE => Syntax.parse_term ctxt p);
   270 
   271 	(* type inference and contexts *)
   272         val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   273         val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   274 	val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   275 	val res = Syntax.check_terms ctxt arg;
   276 	val ctxt' = ctxt |> fold Variable.auto_fixes res;
   277 
   278 	(* instantiation *)
   279 	val (type_parms'', res') = chop (length type_parms) res;
   280         val insts'' = (parm_names ~~ res') |> map_filter
   281           (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
   282             inst => SOME inst);
   283 	val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
   284 	val inst = Symtab.make insts'';
   285       in
   286         (Element.inst_morphism thy (instT, inst) $>
   287           Morphism.name_morphism (Name.qualified prfx), ctxt')
   288       end;
   289 
   290     fun add_declarations loc morph ctxt =
   291       let
   292         (* locale data *)
   293         val parms = loc |> NewLocale.params_of thy |>
   294           map (fn (b, SOME T, mx) => ((Name.name_of b, T), mx));
   295         val (typ_decls, term_decls) = NewLocale.declarations_of thy loc;
   296 
   297         (* declarations from locale *)
   298 	val ctxt'' = ctxt |>
   299 	  fold_rev (fn decl => Context.proof_map (decl morph)) typ_decls |>
   300 	  fold_rev (fn decl => Context.proof_map (decl morph)) term_decls;
   301       in
   302         ctxt''
   303       end;
   304 
   305     val Expr [(loc1, (prfx1, insts1))] = expr';
   306     val ctxt0 = ProofContext.init thy;
   307     val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0;
   308     val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
   309     val ctxt'' = add_declarations loc1 morph1 ctxt';
   310   in ctxt0 end;
   311 
   312 
   313 (*** Locale processing ***)
   314 
   315 (** Prepare locale elements **)
   316 
   317 local
   318 
   319 fun declare_elem prep_vars (Fixes fixes) ctxt =
   320       let val (vars, _) = prep_vars fixes ctxt
   321       in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
   322   | declare_elem prep_vars (Constrains csts) ctxt =
   323       let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
   324       in ([], ctxt') end
   325   | declare_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
   326   | declare_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
   327   | declare_elem _ (Notes _) ctxt = ([], ctxt);
   328 
   329 in
   330 
   331 fun declare_elems prep_vars raw_elems ctxt =
   332   fold_map (declare_elem prep_vars) raw_elems ctxt;
   333 
   334 end;
   335 
   336 local
   337 
   338 val norm_term = Envir.beta_norm oo Term.subst_atomic;
   339 
   340 fun abstract_thm thy eq =
   341   Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
   342 
   343 fun bind_def ctxt eq (xs, env, ths) =
   344   let
   345     val ((y, T), b) = LocalDefs.abs_def eq;
   346     val b' = norm_term env b;
   347     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
   348     fun err msg = error (msg ^ ": " ^ quote y);
   349   in
   350     exists (fn (x, _) => x = y) xs andalso
   351       err "Attempt to define previously specified variable";
   352     exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
   353       err "Attempt to redefine variable";
   354     (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
   355   end;
   356 
   357 fun eval_text _ (Fixes _) text = text
   358   | eval_text _ (Constrains _) text = text
   359   | eval_text _ (Assumes asms)
   360         (((exts, exts'), (ints, ints')), (xs, env, defs)) =
   361       let
   362         val ts = maps (map #1 o #2) asms;
   363         val ts' = map (norm_term env) ts;
   364         val spec' = ((exts @ ts, exts' @ ts'), (ints, ints'));
   365       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
   366   | eval_text ctxt (Defines defs) (spec, binds) =
   367       (spec, fold (bind_def ctxt o #1 o #2) defs binds)
   368   | eval_text _ (Notes _) text = text;
   369 
   370 fun closeup _ false elem = elem
   371   | closeup ctxt true elem =
   372       let
   373         fun close_frees t =
   374           let
   375             val rev_frees =
   376               Term.fold_aterms (fn Free (x, T) =>
   377                 if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
   378           in Term.list_all_free (rev rev_frees, t) end;
   379 
   380         fun no_binds [] = []
   381           | no_binds _ = error "Illegal term bindings in locale element";
   382       in
   383         (case elem of
   384           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
   385             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
   386         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
   387             (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
   388         | e => e)
   389       end;
   390 
   391 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
   392       let val x = Name.name_of binding
   393       in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   394   | finish_ext_elem _ _ (Constrains _, _) = Constrains []
   395   | finish_ext_elem _ close (Assumes asms, propp) =
   396       close (Assumes (map #1 asms ~~ propp))
   397   | finish_ext_elem _ close (Defines defs, propp) =
   398       close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
   399   | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
   400 
   401 fun finish_elem ctxt parms do_close (elem, propp) text =
   402   let
   403     val elem' = finish_ext_elem parms (closeup ctxt do_close) (elem, propp);
   404     val text' = eval_text ctxt elem' text;
   405   in (elem', text') end
   406   
   407 in
   408 
   409 fun finish_elems ctxt parms do_close elems text =
   410   fold_map (finish_elem ctxt parms do_close) elems text;
   411 
   412 end;
   413 
   414 
   415 local
   416 
   417 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   418 
   419 fun frozen_tvars ctxt Ts =
   420   #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   421   |> map (fn ((xi, S), T) => (xi, (S, T)));
   422 
   423 fun unify_frozen ctxt maxidx Ts Us =
   424   let
   425     fun paramify NONE i = (NONE, i)
   426       | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   427 
   428     val (Ts', maxidx') = fold_map paramify Ts maxidx;
   429     val (Us', maxidx'') = fold_map paramify Us maxidx';
   430     val thy = ProofContext.theory_of ctxt;
   431 
   432     fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   433           handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   434       | unify _ env = env;
   435     val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   436     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   437     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   438   in map (Option.map (Envir.norm_type unifier')) Vs end;
   439 
   440 fun prep_elems prep_vars prepp do_close context raw_elems raw_concl =
   441   let
   442     val (raw_propps, raw_ctxt) = declare_elems prep_vars raw_elems context;
   443       (* raw_ctxt is context enriched by syntax from raw_elems *)
   444 
   445     fun prep_prop raw_propp (raw_ctxt, raw_concl) =
   446       let
   447         (* process patterns (conclusion and external elements) *)
   448         val (ctxt, all_propp) = prepp (raw_ctxt, raw_concl @ raw_propp);
   449         (* add type information from conclusion and external elements to context *)
   450         val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
   451         (* resolve schematic variables (patterns) in conclusion and external elements. *)
   452         val all_propp' = map2 (curry (op ~~))
   453           (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
   454         val (concl, propp) = chop (length raw_concl) all_propp';
   455       in (propp, (ctxt, concl)) end
   456 
   457     val (propps, (ctxt, concl)) = fold_burrow prep_prop raw_propps (raw_ctxt, raw_concl);
   458 
   459     (* Infer parameter types *) 
   460     val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
   461       _ => fn ps => ps) raw_elems [];
   462     val typing = unify_frozen ctxt 0
   463       (map (Variable.default_type raw_ctxt) xs)
   464       (map (Variable.default_type ctxt) xs);
   465     val parms = param_types (xs ~~ typing);
   466 
   467     (* CB: extract information from assumes and defines elements
   468        (fixes, constrains and notes in raw_elemss don't have an effect on
   469        text and elemss), compute final form of context elements. *)
   470    val (elems, text) = finish_elems ctxt parms do_close
   471       (raw_elems ~~ propps) ((([], []), ([], [])), ([], [], []));
   472     (* CB: text has the following structure:
   473            (((exts, exts'), (ints, ints')), (xs, env, defs))
   474        where
   475          exts: external assumptions (terms in external assumes elements)
   476          exts': dito, normalised wrt. env
   477          ints: internal assumptions (terms in internal assumes elements)
   478          ints': dito, normalised wrt. env
   479          xs: the free variables in exts' and ints' and rhss of definitions,
   480            this includes parameters except defined parameters
   481          env: list of term pairs encoding substitutions, where the first term
   482            is a free variable; substitutions represent defines elements and
   483            the rhs is normalised wrt. the previous env
   484          defs: theorems representing the substitutions from defines elements
   485            (thms are normalised wrt. env).
   486        elems is an updated version of raw_elems:
   487          - type info added to Fixes and modified in Constrains
   488          - axiom and definition statement replaced by corresponding one
   489            from proppss in Assumes and Defines
   490          - Facts unchanged
   491        *)
   492    in ((parms, elems, concl), text) end
   493 
   494 in
   495 
   496 fun read_elems x = prep_elems ProofContext.read_vars ProofContext.read_propp_schematic x;
   497 fun cert_elems x = prep_elems ProofContext.cert_vars ProofContext.cert_propp_schematic x;
   498 
   499 end;
   500 
   501 
   502 (* facts and attributes *)
   503 
   504 local
   505 
   506 fun check_name name =
   507   if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
   508   else name;
   509 
   510 fun prep_facts prep_name get intern ctxt elem = elem |> Element.map_ctxt
   511      {var = I, typ = I, term = I,
   512       name = Name.map_name prep_name,
   513       fact = get ctxt,
   514       attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
   515 
   516 in
   517 
   518 fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
   519 fun cert_facts x = prep_facts I (K I) (K I) x;
   520 
   521 end;
   522 
   523 
   524 (* activate elements in context, return elements and facts *)
   525 
   526 local
   527 
   528 fun axioms_export axs _ As =
   529   (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
   530 
   531 
   532 (* NB: derived ids contain only facts at this stage *)
   533 
   534 fun activate_elem (Fixes fixes) ctxt =
   535       ([], ctxt |> ProofContext.add_fixes_i fixes |> snd)
   536   | activate_elem (Constrains _) ctxt =
   537       ([], ctxt)
   538   | activate_elem (Assumes asms) ctxt =
   539       let
   540         val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   541         val ts = maps (map #1 o #2) asms';
   542         val (_, ctxt') =
   543           ctxt |> fold Variable.auto_fixes ts
   544           |> ProofContext.add_assms_i (axioms_export []) asms';
   545       in ([], ctxt') end
   546   | activate_elem (Defines defs) ctxt =
   547       let
   548         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   549         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
   550             let val ((c, _), t') = LocalDefs.cert_def ctxt t
   551             in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
   552         val (_, ctxt') =
   553           ctxt |> fold (Variable.auto_fixes o #1) asms
   554           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
   555       in ([], ctxt') end
   556   | activate_elem (Notes (kind, facts)) ctxt =
   557       let
   558         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
   559         val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
   560       in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end;
   561 
   562 in
   563 
   564 fun activate_elems prep_facts raw_elems ctxt =
   565   let
   566     val elems = map (prep_facts ctxt) raw_elems;
   567     val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt);
   568     val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
   569   in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end;
   570 
   571 end;
   572 
   573 
   574 (* full context statements: import + elements + conclusion *)
   575 
   576 local
   577 
   578 fun prep_context_statement prep_expr prep_elems prep_facts
   579     do_close imprt elements raw_concl context =
   580   let
   581     val thy = ProofContext.theory_of context;
   582 
   583     val (expr, (params, fors)) = parameters thy (apfst (prep_expr thy) imprt);
   584     val ctxt = context |>
   585       ProofContext.add_fixes (map (fn (b, mx) => (b, NONE, mx)) params) |> snd |>
   586       ProofContext.add_fixes fors |> snd;
   587   in
   588     case expr of
   589         Expr [] => let
   590           val ((parms, elems, concl), (spec, (_, _, defs))) = prep_elems do_close
   591             context elements raw_concl;
   592           val ((elems', _), ctxt') =
   593             activate_elems prep_facts elems (ProofContext.set_stmt true ctxt);
   594         in
   595           (((ctxt', elems'), (parms, spec, defs)), concl)
   596         end
   597 (*
   598         | Expr [(name, insts)] => let
   599           val parms = parameters_of thy name |> map (fn (b, SOME T, _) => (Name.name_of b, T));
   600           val (morph, ctxt') = read_inst parms insts context;
   601         in
   602           
   603         end
   604 *)
   605 end
   606 
   607 in
   608 
   609 fun read_context imprt body ctxt =
   610   #1 (prep_context_statement intern_expr read_elems read_facts true imprt body [] ctxt);
   611 (*
   612 fun cert_context imprt body ctxt =
   613   #1 (prep_context_statement (K I) cert_elems cert_facts true imprt body [] ctxt);
   614 *)
   615 end;
   616 
   617 
   618 (** Dependencies **)
   619 
   620 
   621 
   622 (*** Locale declarations ***)
   623 
   624 local
   625 
   626 (* introN: name of theorems for introduction rules of locale and
   627      delta predicates;
   628    axiomsN: name of theorem set with destruct rules for locale predicates,
   629      also name suffix of delta predicates. *)
   630 
   631 val introN = "intro";
   632 val axiomsN = "axioms";
   633 
   634 fun atomize_spec thy ts =
   635   let
   636     val t = Logic.mk_conjunction_balanced ts;
   637     val body = ObjectLogic.atomize_term thy t;
   638     val bodyT = Term.fastype_of body;
   639   in
   640     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
   641     else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
   642   end;
   643 
   644 (* achieve plain syntax for locale predicates (without "PROP") *)
   645 
   646 fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
   647   if length args = n then
   648     Syntax.const "_aprop" $
   649       Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
   650   else raise Match);
   651 
   652 (* CB: define one predicate including its intro rule and axioms
   653    - bname: predicate name
   654    - parms: locale parameters
   655    - defs: thms representing substitutions from defines elements
   656    - ts: terms representing locale assumptions (not normalised wrt. defs)
   657    - norm_ts: terms representing locale assumptions (normalised wrt. defs)
   658    - thy: the theory
   659 *)
   660 
   661 fun def_pred bname parms defs ts norm_ts thy =
   662   let
   663     val name = Sign.full_name thy bname;
   664 
   665     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
   666     val env = Term.add_term_free_names (body, []);
   667     val xs = filter (member (op =) env o #1) parms;
   668     val Ts = map #2 xs;
   669     val extraTs = (Term.term_tfrees body \\ fold Term.add_tfreesT Ts [])
   670       |> Library.sort_wrt #1 |> map TFree;
   671     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
   672 
   673     val args = map Logic.mk_type extraTs @ map Free xs;
   674     val head = Term.list_comb (Const (name, predT), args);
   675     val statement = ObjectLogic.ensure_propT thy head;
   676 
   677     val ([pred_def], defs_thy) =
   678       thy
   679       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
   680       |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
   681       |> PureThy.add_defs false
   682         [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
   683     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
   684 
   685     val cert = Thm.cterm_of defs_thy;
   686 
   687     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
   688       MetaSimplifier.rewrite_goals_tac [pred_def] THEN
   689       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   690       Tactic.compose_tac (false,
   691         Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   692 
   693     val conjuncts =
   694       (Drule.equal_elim_rule2 OF [body_eq,
   695         MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   696       |> Conjunction.elim_balanced (length ts);
   697     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   698       Element.prove_witness defs_ctxt t
   699        (MetaSimplifier.rewrite_goals_tac defs THEN
   700         Tactic.compose_tac (false, ax, 0) 1));
   701   in ((statement, intro, axioms), defs_thy) end;
   702 
   703 in
   704 
   705 (* CB: main predicate definition function *)
   706 
   707 fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
   708   let
   709     val (a_pred, a_intro, a_axioms, thy'') =
   710       if null exts then (NONE, NONE, [], thy)
   711       else
   712         let
   713           val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
   714           val ((statement, intro, axioms), thy') =
   715             thy
   716             |> def_pred aname parms defs exts exts';
   717           val (_, thy'') =
   718             thy'
   719             |> Sign.add_path aname
   720             |> Sign.no_base_names
   721             |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
   722             ||> Sign.restore_naming thy';
   723           in (SOME statement, SOME intro, axioms, thy'') end;
   724     val (b_pred, b_intro, b_axioms, thy'''') =
   725       if null ints then (NONE, NONE, [], thy'')
   726       else
   727         let
   728           val ((statement, intro, axioms), thy''') =
   729             thy''
   730             |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred);
   731           val (_, thy'''') =
   732             thy'''
   733             |> Sign.add_path pname
   734             |> Sign.no_base_names
   735             |> PureThy.note_thmss Thm.internalK
   736                  [((Name.binding introN, []), [([intro], [])]),
   737                   ((Name.binding axiomsN, []),
   738                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
   739             ||> Sign.restore_naming thy''';
   740         in (SOME statement, SOME intro, axioms, thy'''') end;
   741   in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
   742 
   743 end;
   744 
   745 
   746 local
   747 
   748 fun assumes_to_notes (Assumes asms) axms =
   749       fold_map (fn (a, spec) => fn axs =>
   750           let val (ps, qs) = chop (length spec) axs
   751           in ((a, [(ps, [])]), qs) end) asms axms
   752       |> apfst (curry Notes Thm.assumptionK)
   753   | assumes_to_notes e axms = (e, axms);
   754 
   755 fun defines_to_notes thy (Defines defs) defns =
   756     let
   757       val defs' = map (fn (_, (def, _)) => def) defs
   758       val notes = map (fn (a, (def, _)) =>
   759         (a, [([assume (cterm_of thy def)], [])])) defs
   760     in
   761       (Notes (Thm.definitionK, notes), defns @ defs')
   762     end
   763   | defines_to_notes _ e defns = (e, defns);
   764 
   765 fun gen_add_locale prep_ctxt
   766     bname predicate_name raw_imprt raw_body thy =
   767   let
   768     val thy_ctxt = ProofContext.init thy;
   769     val name = Sign.full_name thy bname;
   770     val _ = NewLocale.test_locale thy name andalso
   771       error ("Duplicate definition of locale " ^ quote name);
   772 
   773     val ((body_ctxt, body_elems), text as (parms, ((_, exts'), _), defs)) =
   774       prep_ctxt raw_imprt raw_body thy_ctxt;
   775     val ((statement, intro, axioms), _, thy') =
   776       define_preds predicate_name text thy;
   777 
   778     val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
   779     val _ = if null extraTs then ()
   780       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
   781 
   782     val params = body_elems |>
   783       map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat;
   784 
   785     val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
   786 
   787     val notes = body_elems' |>
   788       (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness axioms)) |>
   789       fst |>
   790       map_filter (fn Notes notes => SOME notes | _ => NONE);
   791 
   792     val loc_ctxt = thy' |>
   793       NewLocale.register_locale name (extraTs, params) (statement, defns) ([], [])
   794         (map (fn n => (n, stamp ())) notes |> rev) [] |>
   795       NewLocale.init name
   796   in (name, loc_ctxt) end;
   797 
   798 in
   799 
   800 val add_locale = gen_add_locale read_context;
   801 (* val add_locale_i = gen_add_locale cert_context; *)
   802 
   803 end;
   804 
   805 end;