src/Pure/Isar/expression.ML
changeset 28795 6891e273c33b
parent 28701 ca5840b1f7b3
child 28832 cf7237498e7a
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Nov 14 14:00:52 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Nov 14 16:49:52 2008 +0100
     1.3 @@ -2,21 +2,31 @@
     1.4      ID:         $Id$
     1.5      Author:     Clemens Ballarin, TU Muenchen
     1.6  
     1.7 -Locale expressions --- experimental.
     1.8 +New locale development --- experimental.
     1.9  *)
    1.10  
    1.11  signature EXPRESSION =
    1.12  sig
    1.13 +  type map
    1.14 +  type 'morph expr
    1.15  
    1.16 -type map
    1.17 -type 'morph expr
    1.18 +  val empty_expr: 'morph expr
    1.19 +
    1.20 +  type expression = (string * map) expr * (Name.binding * string option * mixfix) list
    1.21 +  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list
    1.22  
    1.23 -type expression = (string * map) expr * (Name.binding * string option * mixfix) list
    1.24 -type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list
    1.25 +  (* Declaring locales *)
    1.26 +  val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
    1.27 +    string * Proof.context
    1.28 +(*
    1.29 +  val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    1.30 +    string * Proof.context
    1.31 +*)
    1.32  
    1.33 -val parse_expr: OuterParse.token list -> expression * OuterParse.token list
    1.34 -val debug_parameters: expression -> Proof.context -> Proof.context
    1.35 -val debug_context: expression -> Proof.context -> Proof.context
    1.36 +  (* Debugging and development *)
    1.37 +  val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    1.38 +  val debug_parameters: expression -> Proof.context -> Proof.context
    1.39 +  val debug_context: expression -> Proof.context -> Proof.context
    1.40  
    1.41  end;
    1.42  
    1.43 @@ -24,7 +34,10 @@
    1.44  structure Expression: EXPRESSION =
    1.45  struct
    1.46  
    1.47 -(* Locale expressions *)
    1.48 +datatype ctxt = datatype Element.ctxt;
    1.49 +
    1.50 +
    1.51 +(*** Expressions ***)
    1.52  
    1.53  datatype map =
    1.54    Positional of string option list |
    1.55 @@ -35,6 +48,8 @@
    1.56  type expression = (string * map) expr * (Name.binding * string option * mixfix) list;
    1.57  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list;
    1.58  
    1.59 +val empty_expr = Expr [];
    1.60 +
    1.61  
    1.62  (** Parsing and printing **)
    1.63  
    1.64 @@ -43,7 +58,7 @@
    1.65  structure P = OuterParse;
    1.66  
    1.67  val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    1.68 -   P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
    1.69 +   P.$$$ "defines" || P.$$$ "notes";
    1.70  fun plus1_unless test scan =
    1.71    scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    1.72  
    1.73 @@ -55,7 +70,7 @@
    1.74  
    1.75  in
    1.76  
    1.77 -val parse_expr =
    1.78 +val parse_expression =
    1.79    let
    1.80      fun expr2 x = P.xname x;
    1.81      fun expr1 x = (Scan.optional prefix "" -- expr2 --
    1.82 @@ -65,25 +80,42 @@
    1.83  
    1.84  end;
    1.85  
    1.86 -(*
    1.87 -fun pretty_expr thy (Locale loc) =
    1.88 -      [Pretty.str "Locale", Pretty.brk 1, Pretty.str (Locale.extern thy loc)]
    1.89 -  | pretty_expr thy (Instance (expr, (prfx, Positional insts))) =
    1.90 -      let
    1.91 -        val insts' = (* chop trailing NONEs *)
    1.92 -      
    1.93 -  | pretty_expr thy (Instance (expr, (prfx, Named insts))) =
    1.94 -*)
    1.95 +fun pretty_expr thy (Expr expr) =
    1.96 +  let
    1.97 +    fun pretty_pos NONE = Pretty.str "_"
    1.98 +      | pretty_pos (SOME x) = Pretty.str x;
    1.99 +    fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=",
   1.100 +          Pretty.brk 1, Pretty.str y] |> Pretty.block;
   1.101 +    fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |>
   1.102 +          map pretty_pos |> Pretty.breaks
   1.103 +      | pretty_ren (Named []) = []
   1.104 +      | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 ::
   1.105 +          (ps |> map pretty_named |> Pretty.separate "and");
   1.106 +    fun pretty_rename (loc, ("", ren)) =
   1.107 +          Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) 
   1.108 +      | pretty_rename (loc, (prfx, ren)) =
   1.109 +          Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) ::
   1.110 +            Pretty.brk 1 :: pretty_ren ren);
   1.111 +  in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
   1.112 +
   1.113 +fun err_in_expr thy msg (Expr expr) =
   1.114 +  let
   1.115 +    val err_msg =
   1.116 +      if null expr then msg
   1.117 +      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   1.118 +        [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
   1.119 +          pretty_expr thy (Expr expr)])
   1.120 +  in error err_msg end;
   1.121  
   1.122  
   1.123 -(** Processing of locale expression **)
   1.124 +(** Internalise locale names **)
   1.125  
   1.126 -fun intern thy (Expr instances) = Expr (map (apfst (Locale.intern thy)) instances);
   1.127 +fun intern_expr thy (Expr instances) = Expr (map (apfst (NewLocale.intern thy)) instances);
   1.128  
   1.129  
   1.130 -(* Parameters of expression (not expression_i).
   1.131 +(** Parameters of expression (not expression_i).
   1.132     Sanity check of instantiations.
   1.133 -   Positional instantiations are extended to match full length of parameter list. *)
   1.134 +   Positional instantiations are extended to match full length of parameter list. **)
   1.135  
   1.136  fun parameters thy (expr, fixed : (Name.binding * string option * mixfix) list) =
   1.137    let
   1.138 @@ -93,63 +125,110 @@
   1.139          if null dups then () else error (message ^ commas dups)
   1.140        end;
   1.141  
   1.142 -    fun params2 loc =
   1.143 -          (Locale.parameters_of thy loc |> map (fn ((p, _), mx) => (p, mx)), loc) ;
   1.144 -    fun params1 (loc, (prfx, Positional insts)) =
   1.145 +    fun match_bind (n, b) = (n = Name.name_of b);
   1.146 +    fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
   1.147 +      (* FIXME: cannot compare bindings for equality. *)
   1.148 +
   1.149 +    fun params_loc loc =
   1.150 +          (NewLocale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc)
   1.151 +            handle ERROR msg => err_in_expr thy msg (Expr [(loc, ("", Named []))]);
   1.152 +    fun params_inst (expr as (loc, (prfx, Positional insts))) =
   1.153            let
   1.154 -            val (ps, loc') = params2 loc;
   1.155 +            val (ps, loc') = params_loc loc;
   1.156  	    val d = length ps - length insts;
   1.157  	    val insts' =
   1.158 -	      if d < 0 then error ("More arguments than parameters in instantiation.")
   1.159 -(* FIXME print expr *)
   1.160 +	      if d < 0 then err_in_expr thy "More arguments than parameters in instantiation."
   1.161 +                (Expr [expr])
   1.162  	      else insts @ replicate d NONE;
   1.163              val ps' = (ps ~~ insts') |>
   1.164                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
   1.165            in
   1.166              (ps', (loc', (prfx, Positional insts')))
   1.167            end
   1.168 -      | params1 (loc, (prfx, Named insts)) =
   1.169 +      | params_inst (expr as (loc, (prfx, Named insts))) =
   1.170            let
   1.171              val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
   1.172 -              (map fst insts);
   1.173 -(* FIXME print expr *)
   1.174 +              (map fst insts)
   1.175 +              handle ERROR msg => err_in_expr thy msg (Expr [expr]);
   1.176  
   1.177 -            val (ps, loc') = params2 loc;
   1.178 +            val (ps, loc') = params_loc loc;
   1.179              val ps' = fold (fn (p, _) => fn ps =>
   1.180 -              if AList.defined (op =) ps p then AList.delete (op =) p ps
   1.181 -              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
   1.182 -(* FIXME print expr *)
   1.183 -(* FIXME AList lacks a version of delete that signals the absence of the deleted item *)
   1.184 +              if AList.defined match_bind ps p then AList.delete match_bind p ps
   1.185 +              else err_in_expr thy (quote p ^" not a parameter of instantiated expression.")
   1.186 +                (Expr [expr])) insts ps;
   1.187            in
   1.188              (ps', (loc', (prfx, Named insts)))
   1.189            end;
   1.190 -    fun params0 (Expr is) =
   1.191 +    fun params_expr (Expr is) =
   1.192            let
   1.193              val (is', ps') = fold_map (fn i => fn ps =>
   1.194                let
   1.195 -                val (ps', i') = params1 i;
   1.196 -                val ps'' = AList.join (op =) (fn p => fn (mx1, mx2) =>
   1.197 +                val (ps', i') = params_inst i;
   1.198 +                val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) =>
   1.199 +                  (* FIXME: should check for bindings being the same.
   1.200 +                     Instead we check for equal name and syntax. *)
   1.201                    if mx1 = mx2 then mx1
   1.202 -                  else error ("Conflicting syntax for parameter" ^ quote p ^ " in expression.")) (ps, ps')
   1.203 -(* FIXME print Expr is *)
   1.204 +                  else err_in_expr thy ("Conflicting syntax for parameter" ^ quote (Name.name_of p) ^ " in expression.")
   1.205 +                    (Expr is)) (ps, ps')
   1.206                in (i', ps'') end) is []
   1.207            in
   1.208              (ps', Expr is')
   1.209            end;
   1.210  
   1.211 -    val (parms, expr') = params0 expr;
   1.212 +    val (parms, expr') = params_expr expr;
   1.213  
   1.214 -    val parms' = map fst parms;
   1.215 +    val parms' = map (fst #> Name.name_of) parms;
   1.216      val fixed' = map (#1 #> Name.name_of) fixed;
   1.217      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   1.218      val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
   1.219  
   1.220    in (expr', (parms, fixed)) end;
   1.221  
   1.222 +
   1.223 +(** Read instantiation **)
   1.224 +
   1.225 +fun read_inst parse_term parms (prfx, insts) ctxt =
   1.226 +  let
   1.227 +    (* parameters *)
   1.228 +    val (parm_names, parm_types) = split_list parms;
   1.229 +    val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   1.230 +
   1.231 +    (* parameter instantiations *)
   1.232 +    val insts' = case insts of
   1.233 +      Positional insts => (insts ~~ parm_names) |> map (fn
   1.234 +        (NONE, p) => parse_term ctxt p |
   1.235 +        (SOME t, _) => parse_term ctxt t) |
   1.236 +      Named insts => parm_names |> map (fn
   1.237 +        p => case AList.lookup (op =) insts p of
   1.238 +          SOME t => parse_term ctxt t |
   1.239 +          NONE => parse_term ctxt p);
   1.240 +
   1.241 +    (* type inference and contexts *)
   1.242 +    val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   1.243 +    val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   1.244 +    val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   1.245 +    val res = Syntax.check_terms ctxt arg;
   1.246 +    val ctxt' = ctxt |> fold Variable.auto_fixes res;
   1.247 +
   1.248 +    (* instantiation *)
   1.249 +    val (type_parms'', res') = chop (length type_parms) res;
   1.250 +    val insts'' = (parm_names ~~ res') |> map_filter
   1.251 +      (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
   1.252 +        inst => SOME inst);
   1.253 +    val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
   1.254 +    val inst = Symtab.make insts'';
   1.255 +  in
   1.256 +    (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
   1.257 +      Morphism.name_morphism (Name.qualified prfx), ctxt')
   1.258 +  end;
   1.259 +        
   1.260 +        
   1.261 +(** Debugging **)
   1.262 +  
   1.263  fun debug_parameters raw_expr ctxt =
   1.264    let
   1.265      val thy = ProofContext.theory_of ctxt;
   1.266 -    val expr = apfst (intern thy) raw_expr;
   1.267 +    val expr = apfst (intern_expr thy) raw_expr;
   1.268      val (expr', (parms, fixed)) = parameters thy expr;
   1.269    in ctxt end;
   1.270  
   1.271 @@ -157,13 +236,13 @@
   1.272  fun debug_context (raw_expr, fixed) ctxt =
   1.273    let
   1.274      val thy = ProofContext.theory_of ctxt;
   1.275 -    val expr = intern thy raw_expr;
   1.276 +    val expr = intern_expr thy raw_expr;
   1.277      val (expr', (parms, fixed)) = parameters thy (expr, fixed);
   1.278  
   1.279      fun declare_parameters (parms, fixed) ctxt =
   1.280        let
   1.281        val (parms', ctxt') =
   1.282 -        ProofContext.add_fixes (map (fn (p, mx) => (Name.binding p, NONE, mx)) parms) ctxt;
   1.283 +        ProofContext.add_fixes (map (fn (p, mx) => (p, NONE, mx)) parms) ctxt;
   1.284        val (fixed', ctxt'') =
   1.285          ProofContext.add_fixes fixed ctxt';
   1.286        in
   1.287 @@ -173,8 +252,8 @@
   1.288      fun rough_inst loc prfx insts ctxt =
   1.289        let
   1.290          (* locale data *)
   1.291 -        val (parm_names, parm_types) = loc |> Locale.parameters_of thy |>
   1.292 -          map fst |> split_list;
   1.293 +        val (parm_names, parm_types) = loc |> NewLocale.params_of thy |>
   1.294 +          map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   1.295  
   1.296          (* type parameters *)
   1.297          val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   1.298 @@ -211,8 +290,9 @@
   1.299      fun add_declarations loc morph ctxt =
   1.300        let
   1.301          (* locale data *)
   1.302 -        val parms = loc |> Locale.parameters_of thy;
   1.303 -        val (typ_decls, term_decls) = Locale.declarations_of thy loc;
   1.304 +        val parms = loc |> NewLocale.params_of thy |>
   1.305 +          map (fn (b, SOME T, mx) => ((Name.name_of b, T), mx));
   1.306 +        val (typ_decls, term_decls) = NewLocale.declarations_of thy loc;
   1.307  
   1.308          (* declarations from locale *)
   1.309  	val ctxt'' = ctxt |>
   1.310 @@ -227,7 +307,499 @@
   1.311      val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0;
   1.312      val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
   1.313      val ctxt'' = add_declarations loc1 morph1 ctxt';
   1.314 -  in ctxt'' end;
   1.315 +  in ctxt0 end;
   1.316 +
   1.317 +
   1.318 +(*** Locale processing ***)
   1.319 +
   1.320 +(** Prepare locale elements **)
   1.321 +
   1.322 +local
   1.323 +
   1.324 +fun declare_elem prep_vars (Fixes fixes) ctxt =
   1.325 +      let val (vars, _) = prep_vars fixes ctxt
   1.326 +      in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
   1.327 +  | declare_elem prep_vars (Constrains csts) ctxt =
   1.328 +      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
   1.329 +      in ([], ctxt') end
   1.330 +  | declare_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
   1.331 +  | declare_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
   1.332 +  | declare_elem _ (Notes _) ctxt = ([], ctxt);
   1.333 +
   1.334 +in
   1.335 +
   1.336 +fun declare_elems prep_vars raw_elems ctxt =
   1.337 +  fold_map (declare_elem prep_vars) raw_elems ctxt;
   1.338 +
   1.339 +end;
   1.340 +
   1.341 +local
   1.342 +
   1.343 +val norm_term = Envir.beta_norm oo Term.subst_atomic;
   1.344 +
   1.345 +fun abstract_thm thy eq =
   1.346 +  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
   1.347 +
   1.348 +fun bind_def ctxt eq (xs, env, ths) =
   1.349 +  let
   1.350 +    val ((y, T), b) = LocalDefs.abs_def eq;
   1.351 +    val b' = norm_term env b;
   1.352 +    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
   1.353 +    fun err msg = error (msg ^ ": " ^ quote y);
   1.354 +  in
   1.355 +    exists (fn (x, _) => x = y) xs andalso
   1.356 +      err "Attempt to define previously specified variable";
   1.357 +    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
   1.358 +      err "Attempt to redefine variable";
   1.359 +    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
   1.360 +  end;
   1.361 +
   1.362 +fun eval_text _ (Fixes _) text = text
   1.363 +  | eval_text _ (Constrains _) text = text
   1.364 +  | eval_text _ (Assumes asms)
   1.365 +        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
   1.366 +      let
   1.367 +        val ts = maps (map #1 o #2) asms;
   1.368 +        val ts' = map (norm_term env) ts;
   1.369 +        val spec' = ((exts @ ts, exts' @ ts'), (ints, ints'));
   1.370 +      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
   1.371 +  | eval_text ctxt (Defines defs) (spec, binds) =
   1.372 +      (spec, fold (bind_def ctxt o #1 o #2) defs binds)
   1.373 +  | eval_text _ (Notes _) text = text;
   1.374 +
   1.375 +fun closeup _ false elem = elem
   1.376 +  | closeup ctxt true elem =
   1.377 +      let
   1.378 +        fun close_frees t =
   1.379 +          let
   1.380 +            val rev_frees =
   1.381 +              Term.fold_aterms (fn Free (x, T) =>
   1.382 +                if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
   1.383 +          in Term.list_all_free (rev rev_frees, t) end;
   1.384 +
   1.385 +        fun no_binds [] = []
   1.386 +          | no_binds _ = error "Illegal term bindings in locale element";
   1.387 +      in
   1.388 +        (case elem of
   1.389 +          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
   1.390 +            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
   1.391 +        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
   1.392 +            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
   1.393 +        | e => e)
   1.394 +      end;
   1.395 +
   1.396 +fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
   1.397 +      let val x = Name.name_of binding
   1.398 +      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   1.399 +  | finish_ext_elem _ _ (Constrains _, _) = Constrains []
   1.400 +  | finish_ext_elem _ close (Assumes asms, propp) =
   1.401 +      close (Assumes (map #1 asms ~~ propp))
   1.402 +  | finish_ext_elem _ close (Defines defs, propp) =
   1.403 +      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
   1.404 +  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
   1.405 +
   1.406 +fun finish_elem ctxt parms do_close (elem, propp) text =
   1.407 +  let
   1.408 +    val elem' = finish_ext_elem parms (closeup ctxt do_close) (elem, propp);
   1.409 +    val text' = eval_text ctxt elem' text;
   1.410 +  in (elem', text') end
   1.411 +  
   1.412 +in
   1.413 +
   1.414 +fun finish_elems ctxt parms do_close elems text =
   1.415 +  fold_map (finish_elem ctxt parms do_close) elems text;
   1.416 +
   1.417 +end;
   1.418 +
   1.419 +
   1.420 +local
   1.421 +
   1.422 +fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   1.423 +
   1.424 +fun frozen_tvars ctxt Ts =
   1.425 +  #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   1.426 +  |> map (fn ((xi, S), T) => (xi, (S, T)));
   1.427 +
   1.428 +fun unify_frozen ctxt maxidx Ts Us =
   1.429 +  let
   1.430 +    fun paramify NONE i = (NONE, i)
   1.431 +      | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   1.432 +
   1.433 +    val (Ts', maxidx') = fold_map paramify Ts maxidx;
   1.434 +    val (Us', maxidx'') = fold_map paramify Us maxidx';
   1.435 +    val thy = ProofContext.theory_of ctxt;
   1.436 +
   1.437 +    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   1.438 +          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   1.439 +      | unify _ env = env;
   1.440 +    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   1.441 +    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   1.442 +    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   1.443 +  in map (Option.map (Envir.norm_type unifier')) Vs end;
   1.444 +
   1.445 +fun prep_elems prep_vars prepp do_close context raw_elems raw_concl =
   1.446 +  let
   1.447 +    val (raw_propps, raw_ctxt) = declare_elems prep_vars raw_elems context;
   1.448 +      (* raw_ctxt is context enriched by syntax from raw_elems *)
   1.449 +
   1.450 +    fun prep_prop raw_propp (raw_ctxt, raw_concl) =
   1.451 +      let
   1.452 +        (* process patterns (conclusion and external elements) *)
   1.453 +        val (ctxt, all_propp) = prepp (raw_ctxt, raw_concl @ raw_propp);
   1.454 +        (* add type information from conclusion and external elements to context *)
   1.455 +        val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
   1.456 +        (* resolve schematic variables (patterns) in conclusion and external elements. *)
   1.457 +        val all_propp' = map2 (curry (op ~~))
   1.458 +          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
   1.459 +        val (concl, propp) = chop (length raw_concl) all_propp';
   1.460 +      in (propp, (ctxt, concl)) end
   1.461 +
   1.462 +    val (propps, (ctxt, concl)) = fold_burrow prep_prop raw_propps (raw_ctxt, raw_concl);
   1.463 +
   1.464 +    (* Infer parameter types *) 
   1.465 +    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
   1.466 +      _ => fn ps => ps) raw_elems [];
   1.467 +    val typing = unify_frozen ctxt 0
   1.468 +      (map (Variable.default_type raw_ctxt) xs)
   1.469 +      (map (Variable.default_type ctxt) xs);
   1.470 +    val parms = param_types (xs ~~ typing);
   1.471 +
   1.472 +    (* CB: extract information from assumes and defines elements
   1.473 +       (fixes, constrains and notes in raw_elemss don't have an effect on
   1.474 +       text and elemss), compute final form of context elements. *)
   1.475 +   val (elems, text) = finish_elems ctxt parms do_close
   1.476 +      (raw_elems ~~ propps) ((([], []), ([], [])), ([], [], []));
   1.477 +    (* CB: text has the following structure:
   1.478 +           (((exts, exts'), (ints, ints')), (xs, env, defs))
   1.479 +       where
   1.480 +         exts: external assumptions (terms in external assumes elements)
   1.481 +         exts': dito, normalised wrt. env
   1.482 +         ints: internal assumptions (terms in internal assumes elements)
   1.483 +         ints': dito, normalised wrt. env
   1.484 +         xs: the free variables in exts' and ints' and rhss of definitions,
   1.485 +           this includes parameters except defined parameters
   1.486 +         env: list of term pairs encoding substitutions, where the first term
   1.487 +           is a free variable; substitutions represent defines elements and
   1.488 +           the rhs is normalised wrt. the previous env
   1.489 +         defs: theorems representing the substitutions from defines elements
   1.490 +           (thms are normalised wrt. env).
   1.491 +       elems is an updated version of raw_elems:
   1.492 +         - type info added to Fixes and modified in Constrains
   1.493 +         - axiom and definition statement replaced by corresponding one
   1.494 +           from proppss in Assumes and Defines
   1.495 +         - Facts unchanged
   1.496 +       *)
   1.497 +   in ((parms, elems, concl), text) end
   1.498 +
   1.499 +in
   1.500 +
   1.501 +fun read_elems x = prep_elems ProofContext.read_vars ProofContext.read_propp_schematic x;
   1.502 +fun cert_elems x = prep_elems ProofContext.cert_vars ProofContext.cert_propp_schematic x;
   1.503 +
   1.504 +end;
   1.505 +
   1.506 +
   1.507 +(* facts and attributes *)
   1.508 +
   1.509 +local
   1.510 +
   1.511 +fun check_name name =
   1.512 +  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
   1.513 +  else name;
   1.514 +
   1.515 +fun prep_facts prep_name get intern ctxt elem = elem |> Element.map_ctxt
   1.516 +     {var = I, typ = I, term = I,
   1.517 +      name = Name.map_name prep_name,
   1.518 +      fact = get ctxt,
   1.519 +      attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
   1.520 +
   1.521 +in
   1.522 +
   1.523 +fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
   1.524 +fun cert_facts x = prep_facts I (K I) (K I) x;
   1.525 +
   1.526 +end;
   1.527 +
   1.528 +
   1.529 +(* activate elements in context, return elements and facts *)
   1.530 +
   1.531 +local
   1.532 +
   1.533 +fun axioms_export axs _ As =
   1.534 +  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
   1.535  
   1.536  
   1.537 +(* NB: derived ids contain only facts at this stage *)
   1.538 +
   1.539 +fun activate_elem (Fixes fixes) ctxt =
   1.540 +      ([], ctxt |> ProofContext.add_fixes_i fixes |> snd)
   1.541 +  | activate_elem (Constrains _) ctxt =
   1.542 +      ([], ctxt)
   1.543 +  | activate_elem (Assumes asms) ctxt =
   1.544 +      let
   1.545 +        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   1.546 +        val ts = maps (map #1 o #2) asms';
   1.547 +        val (_, ctxt') =
   1.548 +          ctxt |> fold Variable.auto_fixes ts
   1.549 +          |> ProofContext.add_assms_i (axioms_export []) asms';
   1.550 +      in ([], ctxt') end
   1.551 +  | activate_elem (Defines defs) ctxt =
   1.552 +      let
   1.553 +        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   1.554 +        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
   1.555 +            let val ((c, _), t') = LocalDefs.cert_def ctxt t
   1.556 +            in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
   1.557 +        val (_, ctxt') =
   1.558 +          ctxt |> fold (Variable.auto_fixes o #1) asms
   1.559 +          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
   1.560 +      in ([], ctxt') end
   1.561 +  | activate_elem (Notes (kind, facts)) ctxt =
   1.562 +      let
   1.563 +        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
   1.564 +        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
   1.565 +      in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end;
   1.566 +
   1.567 +in
   1.568 +
   1.569 +fun activate_elems prep_facts raw_elems ctxt =
   1.570 +  let
   1.571 +    val elems = map (prep_facts ctxt) raw_elems;
   1.572 +    val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt);
   1.573 +    val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
   1.574 +  in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end;
   1.575 +
   1.576  end;
   1.577 +
   1.578 +
   1.579 +(* full context statements: import + elements + conclusion *)
   1.580 +
   1.581 +local
   1.582 +
   1.583 +fun prep_context_statement prep_expr prep_elems prep_facts
   1.584 +    do_close imprt elements raw_concl context =
   1.585 +  let
   1.586 +    val thy = ProofContext.theory_of context;
   1.587 +
   1.588 +    val (expr, (params, fors)) = parameters thy (apfst (prep_expr thy) imprt);
   1.589 +    val ctxt = context |>
   1.590 +      ProofContext.add_fixes (map (fn (b, mx) => (b, NONE, mx)) params) |> snd |>
   1.591 +      ProofContext.add_fixes fors |> snd;
   1.592 +  in
   1.593 +    case expr of
   1.594 +        Expr [] => let
   1.595 +          val ((parms, elems, concl), (spec, (_, _, defs))) = prep_elems do_close
   1.596 +            context elements raw_concl;
   1.597 +          val ((elems', _), ctxt') =
   1.598 +            activate_elems prep_facts elems (ProofContext.set_stmt true ctxt);
   1.599 +        in
   1.600 +          (((ctxt', elems'), (parms, spec, defs)), concl)
   1.601 +        end
   1.602 +(*
   1.603 +        | Expr [(name, insts)] => let
   1.604 +          val parms = parameters_of thy name |> map (fn (b, SOME T, _) => (Name.name_of b, T));
   1.605 +          val (morph, ctxt') = read_inst parms insts context;
   1.606 +        in
   1.607 +          
   1.608 +        end
   1.609 +*)
   1.610 +end
   1.611 +
   1.612 +in
   1.613 +
   1.614 +fun read_context imprt body ctxt =
   1.615 +  #1 (prep_context_statement intern_expr read_elems read_facts true imprt body [] ctxt);
   1.616 +(*
   1.617 +fun cert_context imprt body ctxt =
   1.618 +  #1 (prep_context_statement (K I) cert_elems cert_facts true imprt body [] ctxt);
   1.619 +*)
   1.620 +end;
   1.621 +
   1.622 +
   1.623 +(** Dependencies **)
   1.624 +
   1.625 +
   1.626 +
   1.627 +(*** Locale declarations ***)
   1.628 +
   1.629 +local
   1.630 +
   1.631 +(* introN: name of theorems for introduction rules of locale and
   1.632 +     delta predicates;
   1.633 +   axiomsN: name of theorem set with destruct rules for locale predicates,
   1.634 +     also name suffix of delta predicates. *)
   1.635 +
   1.636 +val introN = "intro";
   1.637 +val axiomsN = "axioms";
   1.638 +
   1.639 +fun atomize_spec thy ts =
   1.640 +  let
   1.641 +    val t = Logic.mk_conjunction_balanced ts;
   1.642 +    val body = ObjectLogic.atomize_term thy t;
   1.643 +    val bodyT = Term.fastype_of body;
   1.644 +  in
   1.645 +    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
   1.646 +    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
   1.647 +  end;
   1.648 +
   1.649 +(* achieve plain syntax for locale predicates (without "PROP") *)
   1.650 +
   1.651 +fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
   1.652 +  if length args = n then
   1.653 +    Syntax.const "_aprop" $
   1.654 +      Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
   1.655 +  else raise Match);
   1.656 +
   1.657 +(* CB: define one predicate including its intro rule and axioms
   1.658 +   - bname: predicate name
   1.659 +   - parms: locale parameters
   1.660 +   - defs: thms representing substitutions from defines elements
   1.661 +   - ts: terms representing locale assumptions (not normalised wrt. defs)
   1.662 +   - norm_ts: terms representing locale assumptions (normalised wrt. defs)
   1.663 +   - thy: the theory
   1.664 +*)
   1.665 +
   1.666 +fun def_pred bname parms defs ts norm_ts thy =
   1.667 +  let
   1.668 +    val name = Sign.full_name thy bname;
   1.669 +
   1.670 +    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
   1.671 +    val env = Term.add_term_free_names (body, []);
   1.672 +    val xs = filter (member (op =) env o #1) parms;
   1.673 +    val Ts = map #2 xs;
   1.674 +    val extraTs = (Term.term_tfrees body \\ fold Term.add_tfreesT Ts [])
   1.675 +      |> Library.sort_wrt #1 |> map TFree;
   1.676 +    val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
   1.677 +
   1.678 +    val args = map Logic.mk_type extraTs @ map Free xs;
   1.679 +    val head = Term.list_comb (Const (name, predT), args);
   1.680 +    val statement = ObjectLogic.ensure_propT thy head;
   1.681 +
   1.682 +    val ([pred_def], defs_thy) =
   1.683 +      thy
   1.684 +      |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
   1.685 +      |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
   1.686 +      |> PureThy.add_defs false
   1.687 +        [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
   1.688 +    val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
   1.689 +
   1.690 +    val cert = Thm.cterm_of defs_thy;
   1.691 +
   1.692 +    val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
   1.693 +      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
   1.694 +      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   1.695 +      Tactic.compose_tac (false,
   1.696 +        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   1.697 +
   1.698 +    val conjuncts =
   1.699 +      (Drule.equal_elim_rule2 OF [body_eq,
   1.700 +        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   1.701 +      |> Conjunction.elim_balanced (length ts);
   1.702 +    val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   1.703 +      Element.prove_witness defs_ctxt t
   1.704 +       (MetaSimplifier.rewrite_goals_tac defs THEN
   1.705 +        Tactic.compose_tac (false, ax, 0) 1));
   1.706 +  in ((statement, intro, axioms), defs_thy) end;
   1.707 +
   1.708 +in
   1.709 +
   1.710 +(* CB: main predicate definition function *)
   1.711 +
   1.712 +fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
   1.713 +  let
   1.714 +    val (a_pred, a_intro, a_axioms, thy'') =
   1.715 +      if null exts then (NONE, NONE, [], thy)
   1.716 +      else
   1.717 +        let
   1.718 +          val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
   1.719 +          val ((statement, intro, axioms), thy') =
   1.720 +            thy
   1.721 +            |> def_pred aname parms defs exts exts';
   1.722 +          val (_, thy'') =
   1.723 +            thy'
   1.724 +            |> Sign.add_path aname
   1.725 +            |> Sign.no_base_names
   1.726 +            |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
   1.727 +            ||> Sign.restore_naming thy';
   1.728 +          in (SOME statement, SOME intro, axioms, thy'') end;
   1.729 +    val (b_pred, b_intro, b_axioms, thy'''') =
   1.730 +      if null ints then (NONE, NONE, [], thy'')
   1.731 +      else
   1.732 +        let
   1.733 +          val ((statement, intro, axioms), thy''') =
   1.734 +            thy''
   1.735 +            |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred);
   1.736 +          val (_, thy'''') =
   1.737 +            thy'''
   1.738 +            |> Sign.add_path pname
   1.739 +            |> Sign.no_base_names
   1.740 +            |> PureThy.note_thmss Thm.internalK
   1.741 +                 [((Name.binding introN, []), [([intro], [])]),
   1.742 +                  ((Name.binding axiomsN, []),
   1.743 +                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
   1.744 +            ||> Sign.restore_naming thy''';
   1.745 +        in (SOME statement, SOME intro, axioms, thy'''') end;
   1.746 +  in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
   1.747 +
   1.748 +end;
   1.749 +
   1.750 +
   1.751 +local
   1.752 +
   1.753 +fun assumes_to_notes (Assumes asms) axms =
   1.754 +      fold_map (fn (a, spec) => fn axs =>
   1.755 +          let val (ps, qs) = chop (length spec) axs
   1.756 +          in ((a, [(ps, [])]), qs) end) asms axms
   1.757 +      |> apfst (curry Notes Thm.assumptionK)
   1.758 +  | assumes_to_notes e axms = (e, axms);
   1.759 +
   1.760 +fun defines_to_notes thy (Defines defs) defns =
   1.761 +    let
   1.762 +      val defs' = map (fn (_, (def, _)) => def) defs
   1.763 +      val notes = map (fn (a, (def, _)) =>
   1.764 +        (a, [([assume (cterm_of thy def)], [])])) defs
   1.765 +    in
   1.766 +      (Notes (Thm.definitionK, notes), defns @ defs')
   1.767 +    end
   1.768 +  | defines_to_notes _ e defns = (e, defns);
   1.769 +
   1.770 +fun gen_add_locale prep_ctxt
   1.771 +    bname predicate_name raw_imprt raw_body thy =
   1.772 +  let
   1.773 +    val thy_ctxt = ProofContext.init thy;
   1.774 +    val name = Sign.full_name thy bname;
   1.775 +    val _ = NewLocale.test_locale thy name andalso
   1.776 +      error ("Duplicate definition of locale " ^ quote name);
   1.777 +
   1.778 +    val ((body_ctxt, body_elems), text as (parms, ((_, exts'), _), defs)) =
   1.779 +      prep_ctxt raw_imprt raw_body thy_ctxt;
   1.780 +    val ((statement, intro, axioms), _, thy') =
   1.781 +      define_preds predicate_name text thy;
   1.782 +
   1.783 +    val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
   1.784 +    val _ = if null extraTs then ()
   1.785 +      else warning ("Additional type variable(s) in locale specification " ^ quote bname);
   1.786 +
   1.787 +    val params = body_elems |>
   1.788 +      map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat;
   1.789 +
   1.790 +    val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
   1.791 +
   1.792 +    val notes = body_elems' |>
   1.793 +      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness axioms)) |>
   1.794 +      fst |>
   1.795 +      map_filter (fn Notes notes => SOME notes | _ => NONE);
   1.796 +
   1.797 +    val loc_ctxt = thy' |>
   1.798 +      NewLocale.register_locale name (extraTs, params) (statement, defns) ([], [])
   1.799 +        (map (fn n => (n, stamp ())) notes |> rev) [] |>
   1.800 +      NewLocale.init name
   1.801 +  in (name, loc_ctxt) end;
   1.802 +
   1.803 +in
   1.804 +
   1.805 +val add_locale = gen_add_locale read_context;
   1.806 +(* val add_locale_i = gen_add_locale cert_context; *)
   1.807 +
   1.808 +end;
   1.809 +
   1.810 +end;