src/Pure/Isar/expression.ML
changeset 28872 686963dbf6cd
parent 28862 53f13f763d4f
child 28879 db2816a37a34
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Nov 21 15:54:53 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Nov 21 18:01:39 2008 +0100
     1.3 @@ -7,13 +7,13 @@
     1.4  
     1.5  signature EXPRESSION =
     1.6  sig
     1.7 -  type map
     1.8 +  type 'term map
     1.9    type 'morph expr
    1.10  
    1.11    val empty_expr: 'morph expr
    1.12  
    1.13 -  type expression = (string * map) expr * (Name.binding * string option * mixfix) list
    1.14 -  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list
    1.15 +  type expression = (string * string map) expr * (Name.binding * string option * mixfix) list
    1.16 +(*  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list *)
    1.17  
    1.18    (* Declaring locales *)
    1.19    val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
    1.20 @@ -22,12 +22,8 @@
    1.21    val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    1.22      string * Proof.context
    1.23  *)
    1.24 -
    1.25    (* Debugging and development *)
    1.26    val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    1.27 -  val debug_parameters: expression -> Proof.context -> Proof.context
    1.28 -  val debug_context: expression -> Proof.context -> Proof.context
    1.29 -
    1.30  end;
    1.31  
    1.32  
    1.33 @@ -39,14 +35,13 @@
    1.34  
    1.35  (*** Expressions ***)
    1.36  
    1.37 -datatype map =
    1.38 -  Positional of string option list |
    1.39 -  Named of (string * string) list;
    1.40 +datatype 'term map =
    1.41 +  Positional of 'term option list |
    1.42 +  Named of (string * 'term) list;
    1.43  
    1.44  datatype 'morph expr = Expr of (string * 'morph) list;
    1.45  
    1.46 -type expression = (string * map) expr * (Name.binding * string option * mixfix) list;
    1.47 -type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list;
    1.48 +type expression = (string * string map) expr * (Name.binding * string option * mixfix) list;
    1.49  
    1.50  val empty_expr = Expr [];
    1.51  
    1.52 @@ -184,31 +179,47 @@
    1.53  
    1.54  (** Read instantiation **)
    1.55  
    1.56 +(* Parse positional or named instantiation *)
    1.57 +
    1.58  local
    1.59  
    1.60 -fun prep_inst parse_term parms (prfx, insts) ctxt =
    1.61 +fun prep_inst parse_term parms (Positional insts) ctxt =
    1.62 +      (insts ~~ parms) |> map (fn
    1.63 +        (NONE, p) => Syntax.parse_term ctxt p |
    1.64 +        (SOME t, _) => parse_term ctxt t)
    1.65 +  | prep_inst parse_term parms (Named insts) ctxt =
    1.66 +      parms |> map (fn p => case AList.lookup (op =) insts p of
    1.67 +        SOME t => parse_term ctxt t |
    1.68 +        NONE => Syntax.parse_term ctxt p);
    1.69 +
    1.70 +in
    1.71 +
    1.72 +fun parse_inst x = prep_inst Syntax.parse_term x;
    1.73 +fun make_inst x = prep_inst (K I) x;
    1.74 +
    1.75 +end;
    1.76 +
    1.77 +(* Prepare type inference problem for Syntax.check_terms *)
    1.78 +
    1.79 +fun varify_indexT i ty = ty |> Term.map_atyps
    1.80 +  (fn TFree (a, S) => TVar ((a, i), S)
    1.81 +    | TVar (ai, _) => raise TYPE ("Illegal schematic variable: " ^
    1.82 +        quote (Term.string_of_vname ai), [ty], []));
    1.83 +
    1.84 +(* Instantiation morphism *)
    1.85 +
    1.86 +fun inst_morph (parm_names, parm_types) (prfx, insts') ctxt =
    1.87    let
    1.88      (* parameters *)
    1.89 -    val (parm_names, parm_types) = split_list parms;
    1.90      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
    1.91  
    1.92 -    (* parameter instantiations *)
    1.93 -    val insts' = case insts of
    1.94 -      Positional insts => (insts ~~ parm_names) |> map (fn
    1.95 -        (NONE, p) => parse_term ctxt p |
    1.96 -        (SOME t, _) => parse_term ctxt t) |
    1.97 -      Named insts => parm_names |> map (fn
    1.98 -        p => case AList.lookup (op =) insts p of
    1.99 -          SOME t => parse_term ctxt t |
   1.100 -          NONE => parse_term ctxt p);
   1.101 -
   1.102      (* type inference and contexts *)
   1.103      val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   1.104      val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   1.105      val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   1.106      val res = Syntax.check_terms ctxt arg;
   1.107      val ctxt' = ctxt |> fold Variable.auto_fixes res;
   1.108 -
   1.109 +    
   1.110      (* instantiation *)
   1.111      val (type_parms'', res') = chop (length type_parms) res;
   1.112      val insts'' = (parm_names ~~ res') |> map_filter
   1.113 @@ -221,97 +232,6 @@
   1.114        Morphism.name_morphism (Name.qualified prfx), ctxt')
   1.115    end;
   1.116  
   1.117 -in
   1.118 -
   1.119 -fun read_inst x = prep_inst Syntax.parse_term x;
   1.120 -(* fun cert_inst x = prep_inst (K I) x; *)
   1.121 -
   1.122 -end;
   1.123 -
   1.124 -        
   1.125 -(** Test code **)
   1.126 -  
   1.127 -fun debug_parameters raw_expr ctxt =
   1.128 -  let
   1.129 -    val thy = ProofContext.theory_of ctxt;
   1.130 -    val expr = apfst (intern thy) raw_expr;
   1.131 -    val (expr', fixed) = parameters_of thy expr;
   1.132 -  in ctxt end;
   1.133 -
   1.134 -
   1.135 -fun debug_context (raw_expr, fixed) ctxt =
   1.136 -  let
   1.137 -    val thy = ProofContext.theory_of ctxt;
   1.138 -    val expr = intern thy raw_expr;
   1.139 -    val (expr', fixed) = parameters_of thy (expr, fixed);
   1.140 -
   1.141 -    fun declare_parameters fixed ctxt =
   1.142 -      let
   1.143 -      val (fixed', ctxt') = ProofContext.add_fixes fixed ctxt;
   1.144 -      in
   1.145 -        (fixed', ctxt')
   1.146 -      end;
   1.147 -
   1.148 -    fun rough_inst loc prfx insts ctxt =
   1.149 -      let
   1.150 -        (* locale data *)
   1.151 -        val (parm_names, parm_types) = loc |> NewLocale.params_of thy |>
   1.152 -          map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   1.153 -
   1.154 -        (* type parameters *)
   1.155 -        val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   1.156 -
   1.157 -        (* parameter instantiations *)
   1.158 -        val insts' = case insts of
   1.159 -          Positional insts => (insts ~~ parm_names) |> map (fn
   1.160 -            (NONE, p) => Syntax.parse_term ctxt p |
   1.161 -            (SOME t, _) => Syntax.parse_term ctxt t) |
   1.162 -          Named insts => parm_names |> map (fn
   1.163 -            p => case AList.lookup (op =) insts p of
   1.164 -              SOME t => Syntax.parse_term ctxt t |
   1.165 -              NONE => Syntax.parse_term ctxt p);
   1.166 -
   1.167 -	(* type inference and contexts *)
   1.168 -        val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   1.169 -        val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   1.170 -	val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   1.171 -	val res = Syntax.check_terms ctxt arg;
   1.172 -	val ctxt' = ctxt |> fold Variable.auto_fixes res;
   1.173 -
   1.174 -	(* instantiation *)
   1.175 -	val (type_parms'', res') = chop (length type_parms) res;
   1.176 -        val insts'' = (parm_names ~~ res') |> map_filter
   1.177 -          (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
   1.178 -            inst => SOME inst);
   1.179 -	val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
   1.180 -	val inst = Symtab.make insts'';
   1.181 -      in
   1.182 -        (Element.inst_morphism thy (instT, inst) $>
   1.183 -          Morphism.name_morphism (Name.qualified prfx), ctxt')
   1.184 -      end;
   1.185 -
   1.186 -    fun add_declarations loc morph ctxt =
   1.187 -      let
   1.188 -        (* locale data *)
   1.189 -        val parms = loc |> NewLocale.params_of thy |>
   1.190 -          map (fn (b, SOME T, mx) => ((Name.name_of b, T), mx));
   1.191 -        val (typ_decls, term_decls) = NewLocale.declarations_of thy loc;
   1.192 -
   1.193 -        (* declarations from locale *)
   1.194 -	val ctxt'' = ctxt |>
   1.195 -	  fold_rev (fn decl => Context.proof_map (decl morph)) typ_decls |>
   1.196 -	  fold_rev (fn decl => Context.proof_map (decl morph)) term_decls;
   1.197 -      in
   1.198 -        ctxt''
   1.199 -      end;
   1.200 -
   1.201 -    val Expr [(loc1, (prfx1, insts1))] = expr';
   1.202 -    val ctxt0 = ProofContext.init thy;
   1.203 -    val (parms, ctxt') = declare_parameters fixed ctxt0;
   1.204 -    val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
   1.205 -    val ctxt'' = add_declarations loc1 morph1 ctxt';
   1.206 -  in ctxt0 end;
   1.207 -
   1.208  
   1.209  (*** Locale processing ***)
   1.210  
   1.211 @@ -346,14 +266,17 @@
   1.212        (defs ~~ propps) |> map (fn ((b, _), [propp]) => (b, propp)) |> Defines
   1.213    | restore_elem (Notes notes, _) = Notes notes;
   1.214  
   1.215 -fun check_autofix_elems elems concl ctxt =
   1.216 +fun check_autofix insts elems concl ctxt =
   1.217    let
   1.218 -    val termss = elems |> map extract_elem;
   1.219 -    val all_terms' = (burrow o burrow_fst) (Syntax.check_terms ctxt) (concl @ flat termss); 
   1.220 +    val instss = map (snd o snd) insts |> (map o map) (fn t => (t, []));
   1.221 +    val elemss = elems |> map extract_elem;
   1.222 +    val all_terms' = (burrow o burrow_fst) (Syntax.check_terms ctxt) (concl @ instss @ flat elemss); 
   1.223  (*    val (ctxt', all_props') = ProofContext.check_propp_schematic (ctxt, concl @ flat propss); *)
   1.224 -    val (concl', terms') = chop (length concl) all_terms';
   1.225 -    val ctxt'' = (fold o fold) (fn (t, _) => Variable.auto_fixes t) terms' ctxt;
   1.226 -  in (terms' |> unflat termss |> curry (op ~~) elems |> map restore_elem, concl', ctxt'') end;
   1.227 +    val ctxt'' = (fold o fold) (fn (t, _) => Variable.auto_fixes t) all_terms' ctxt;
   1.228 +    val (concl', mores') = chop (length concl) all_terms';
   1.229 +    val (insts', elems') = chop (length instss) mores';
   1.230 +  in (insts' |> (map o map) fst |> curry (op ~~) insts |> map (fn ((l, (p, _)), is) => (l, (p, is))),
   1.231 +    elems' |> unflat elemss |> curry (op ~~) elems |> map restore_elem, concl', ctxt'') end;
   1.232  
   1.233  
   1.234  (** Prepare locale elements **)
   1.235 @@ -363,14 +286,12 @@
   1.236        in ctxt |> ProofContext.add_fixes_i vars |> snd end
   1.237    | declare_elem prep_vars (Constrains csts) ctxt =
   1.238        ctxt |> prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) |> snd
   1.239 -  | declare_elem _ (Assumes asms) ctxt = ctxt
   1.240 -  | declare_elem _ (Defines defs) ctxt = ctxt
   1.241 +  | declare_elem _ (Assumes _) ctxt = ctxt
   1.242 +  | declare_elem _ (Defines _) ctxt = ctxt
   1.243    | declare_elem _ (Notes _) ctxt = ctxt;
   1.244  
   1.245  (** Finish locale elements, extract specification text **)
   1.246  
   1.247 -local
   1.248 -
   1.249  val norm_term = Envir.beta_norm oo Term.subst_atomic;
   1.250  
   1.251  fun abstract_thm thy eq =
   1.252 @@ -390,18 +311,20 @@
   1.253      (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
   1.254    end;
   1.255  
   1.256 -fun eval_text _ (Fixes _) text = text
   1.257 -  | eval_text _ (Constrains _) text = text
   1.258 -  | eval_text _ (Assumes asms)
   1.259 +fun eval_text _ _ (Fixes _) text = text
   1.260 +  | eval_text _ _ (Constrains _) text = text
   1.261 +  | eval_text _ is_ext (Assumes asms)
   1.262          (((exts, exts'), (ints, ints')), (xs, env, defs)) =
   1.263        let
   1.264          val ts = maps (map #1 o #2) asms;
   1.265          val ts' = map (norm_term env) ts;
   1.266 -        val spec' = ((exts @ ts, exts' @ ts'), (ints, ints'));
   1.267 +        val spec' =
   1.268 +          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
   1.269 +          else ((exts, exts'), (ints @ ts, ints' @ ts'));
   1.270        in (spec', (fold Term.add_frees ts' xs, env, defs)) end
   1.271 -  | eval_text ctxt (Defines defs) (spec, binds) =
   1.272 +  | eval_text ctxt _ (Defines defs) (spec, binds) =
   1.273        (spec, fold (bind_def ctxt o #1 o #2) defs binds)
   1.274 -  | eval_text _ (Notes _) text = text;
   1.275 +  | eval_text _ _ (Notes _) text = text;
   1.276  
   1.277  fun closeup _ _ false elem = elem
   1.278    | closeup ctxt parms true elem =
   1.279 @@ -424,26 +347,44 @@
   1.280          | e => e)
   1.281        end;
   1.282  
   1.283 -fun finish_ext_elem parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
   1.284 +fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
   1.285        let val x = Name.name_of binding
   1.286        in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   1.287 -  | finish_ext_elem _ _ (Constrains _) = Constrains []
   1.288 -  | finish_ext_elem _ close (Assumes asms) = close (Assumes asms)
   1.289 -  | finish_ext_elem _ close (Defines defs) = close (Defines defs)
   1.290 -  | finish_ext_elem _ _ (Notes facts) = Notes facts;
   1.291 +  | finish_primitive _ _ (Constrains _) = Constrains []
   1.292 +  | finish_primitive _ close (Assumes asms) = close (Assumes asms)
   1.293 +  | finish_primitive _ close (Defines defs) = close (Defines defs)
   1.294 +  | finish_primitive _ _ (Notes facts) = Notes facts;
   1.295 +
   1.296 +fun finish_inst ctxt parms do_close (loc, (prfx, inst)) text =
   1.297 +  let
   1.298 +    val thy = ProofContext.theory_of ctxt;
   1.299 +    val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   1.300 +      map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   1.301 +    val (asm, defs) = NewLocale.specification_of thy loc;
   1.302 +    val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   1.303 +    val asm' = Option.map (Morphism.term morph) asm;
   1.304 +    val defs' = map (Morphism.term morph) defs;
   1.305 +    val text' = text |>
   1.306 +      (if is_some asm
   1.307 +        then eval_text ctxt false (Assumes [(Attrib.no_binding, [(the asm', [])])])
   1.308 +        else I) |>
   1.309 +      (if not (null defs)
   1.310 +        then eval_text ctxt false (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs'))
   1.311 +        else I)
   1.312 +(* FIXME clone from new_locale.ML *)
   1.313 +  in ((loc, morph), text') end;
   1.314  
   1.315  fun finish_elem ctxt parms do_close elem text =
   1.316    let
   1.317 -    val elem' = finish_ext_elem parms (closeup ctxt parms do_close) elem;
   1.318 -    val text' = eval_text ctxt elem' text;
   1.319 +    val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
   1.320 +    val text' = eval_text ctxt true elem' text;
   1.321    in (elem', text') end
   1.322    
   1.323 -in
   1.324 -
   1.325 -fun finish_elems ctxt parms do_close elems text =
   1.326 -  fold_map (finish_elem ctxt parms do_close) elems text;
   1.327 -
   1.328 -end;
   1.329 +fun finish ctxt parms do_close insts elems text =
   1.330 +  let
   1.331 +    val (deps, text') = fold_map (finish_inst ctxt parms do_close) insts text;
   1.332 +    val (elems', text'') = fold_map (finish_elem ctxt parms do_close) elems text';
   1.333 +  in (deps, elems', text'') end;
   1.334  
   1.335  
   1.336  local
   1.337 @@ -455,38 +396,59 @@
   1.338  fun fold_prefixes f xs y = fold_suffixes (f o rev) (rev xs) y;
   1.339  *)
   1.340  
   1.341 -fun prep_elems parse_typ parse_prop prep_vars do_close context raw_elems raw_concl =
   1.342 +fun prep_elems parse_typ parse_prop parse_inst prep_vars
   1.343 +    do_close context fixed raw_insts raw_elems raw_concl =
   1.344    let
   1.345 -    fun prep_elem raw_elem (elems, ctxt) =
   1.346 +    val thy = ProofContext.theory_of context;
   1.347 +
   1.348 +    fun prep_inst (loc, (prfx, inst)) (i, ids, insts, ctxt) =
   1.349 +      let
   1.350 +        val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   1.351 +          map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   1.352 +        val inst' = parse_inst parm_names inst ctxt;
   1.353 +        val parm_types' = map (TypeInfer.paramify_vars o varify_indexT i) parm_types;
   1.354 +        val inst'' = map2 TypeInfer.constrain parm_types' inst';
   1.355 +        val insts' = insts @ [(loc, (prfx, inst''))];
   1.356 +        val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt;
   1.357 +        val inst''' = insts'' |> List.last |> snd |> snd;
   1.358 +        val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
   1.359 +        val (ids', ctxt'') = NewLocale.activate_declarations loc morph thy ids ctxt;
   1.360 +      in (i+1, ids', insts', ctxt'') end;
   1.361 +  
   1.362 +    fun prep_elem raw_elem (insts, elems, ctxt) =
   1.363        let
   1.364          val ctxt' = declare_elem prep_vars raw_elem ctxt;
   1.365          val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
   1.366          (* FIXME term bindings *)
   1.367 -        val (_, _, ctxt'') = check_autofix_elems elems' [] ctxt';
   1.368 -      in (elems', ctxt'') end;
   1.369 +        val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
   1.370 +      in (insts, elems', ctxt') end;
   1.371  
   1.372 -    fun prep_concl raw_concl (elems, ctxt) =
   1.373 +    fun prep_concl raw_concl (insts, elems, ctxt) =
   1.374        let
   1.375          val concl = (map o map) (fn (t, ps) =>
   1.376            (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl;
   1.377 -      in check_autofix_elems elems concl ctxt end;
   1.378 +      in check_autofix insts elems concl ctxt end;
   1.379  
   1.380 -    val (elems, concl, ctxt) = fold prep_elem raw_elems ([], context) |>
   1.381 -      prep_concl raw_concl;
   1.382 +    val fors = prep_vars fixed context |> fst;
   1.383 +    val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
   1.384 +    val (_, _, insts', ctxt') = fold prep_inst raw_insts (0, NewLocale.empty, [], ctxt);
   1.385 +    val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
   1.386 +    val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
   1.387  
   1.388 -    (* Retrieve parameter types *) 
   1.389 +    (* Retrieve parameter types *)
   1.390      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
   1.391 -      _ => fn ps => ps) elems [];
   1.392 +      _ => fn ps => ps) (Fixes fors :: elems) [];
   1.393      val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
   1.394      val parms = xs ~~ Ts;
   1.395  
   1.396 -    val (elems', text) = finish_elems ctxt' parms do_close elems ((([], []), ([], [])), ([], [], []));
   1.397 +    val Fixes fors' = finish_primitive parms I (Fixes fors);
   1.398 +    val (deps, elems', text) = finish ctxt' parms do_close insts elems ((([], []), ([], [])), ([], [], []));
   1.399      (* text has the following structure:
   1.400             (((exts, exts'), (ints, ints')), (xs, env, defs))
   1.401         where
   1.402 -         exts: external assumptions (terms in external assumes elements)
   1.403 +         exts: external assumptions (terms in assumes elements)
   1.404           exts': dito, normalised wrt. env
   1.405 -         ints: internal assumptions (terms in internal assumes elements)
   1.406 +         ints: internal assumptions (terms in assumptions from insts)
   1.407           ints': dito, normalised wrt. env
   1.408           xs: the free variables in exts' and ints' and rhss of definitions,
   1.409             this includes parameters except defined parameters
   1.410 @@ -502,12 +464,14 @@
   1.411           - Facts unchanged
   1.412         *)
   1.413  
   1.414 -  in ((parms, elems', concl), text) end
   1.415 +  in ((parms, fors', deps, elems', concl), text) end
   1.416  
   1.417  in
   1.418  
   1.419 -fun read_elems x = prep_elems Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars x;
   1.420 -fun cert_elems x = prep_elems (K I) (K I) ProofContext.cert_vars x;
   1.421 +fun read_elems x = prep_elems Syntax.parse_typ Syntax.parse_prop parse_inst
   1.422 +  ProofContext.read_vars x;
   1.423 +fun cert_elems x = prep_elems (K I) (K I) make_inst
   1.424 +  ProofContext.cert_vars x;
   1.425  
   1.426  end;
   1.427  
   1.428 @@ -521,35 +485,26 @@
   1.429    let
   1.430      val thy = ProofContext.theory_of context;
   1.431  
   1.432 -    val (expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
   1.433 +    val (Expr expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
   1.434      val ctxt = context |> ProofContext.add_fixes fixed |> snd;
   1.435 +    (* FIXME push inside prep_elems *)
   1.436 +    val ((parms, fors, deps, elems, concl), (spec, (_, _, defs))) =
   1.437 +      prep_elems do_close context fixed expr elements raw_concl;
   1.438 +    (* FIXME activate deps *)
   1.439 +    val ((elems', _), ctxt') =
   1.440 +      Element.activate elems (ProofContext.set_stmt true ctxt);
   1.441    in
   1.442 -    case expr of
   1.443 -        Expr [] => let
   1.444 -          val ((parms, elems, concl), (spec, (_, _, defs))) = prep_elems do_close
   1.445 -            context elements raw_concl;
   1.446 -          val ((elems', _), ctxt') =
   1.447 -            Element.activate elems (ProofContext.set_stmt true ctxt);
   1.448 -        in
   1.449 -          (((ctxt', elems'), (parms, spec, defs)), concl)
   1.450 -        end
   1.451 -(*
   1.452 -        | Expr [(name, insts)] => let
   1.453 -          val parms = parameters_of thy name |> map (fn (b, SOME T, _) => (Name.name_of b, T));
   1.454 -          val (morph, ctxt') = read_inst parms insts context;
   1.455 -        in
   1.456 -          
   1.457 -        end
   1.458 -*)
   1.459 -end
   1.460 +    (((fors, deps), (ctxt', elems'), (parms, spec, defs)), concl)
   1.461 +  end
   1.462  
   1.463  in
   1.464  
   1.465  fun read_context imprt body ctxt =
   1.466    #1 (prep_context_statement intern read_elems true imprt body [] ctxt);
   1.467 +(*
   1.468  fun cert_context imprt body ctxt =
   1.469    #1 (prep_context_statement (K I) cert_elems true imprt body [] ctxt);
   1.470 -
   1.471 +*)
   1.472  end;
   1.473  
   1.474  
   1.475 @@ -700,7 +655,7 @@
   1.476      end
   1.477    | defines_to_notes _ e defns = (e, defns);
   1.478  
   1.479 -fun gen_add_locale prep_ctxt
   1.480 +fun gen_add_locale prep_context
   1.481      bname predicate_name raw_imprt raw_body thy =
   1.482    let
   1.483      val thy_ctxt = ProofContext.init thy;
   1.484 @@ -708,28 +663,31 @@
   1.485      val _ = NewLocale.test_locale thy name andalso
   1.486        error ("Duplicate definition of locale " ^ quote name);
   1.487  
   1.488 -    val ((body_ctxt, body_elems), text as (parms, ((_, exts'), _), defs)) =
   1.489 -      prep_ctxt raw_imprt raw_body thy_ctxt;
   1.490 -    val ((statement, intro, axioms), _, thy') =
   1.491 +    val ((fors, deps), (_, body_elems), text as (parms, ((_, exts'), _), defs)) =
   1.492 +      prep_context raw_imprt raw_body thy_ctxt;
   1.493 +    val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   1.494        define_preds predicate_name text thy;
   1.495  
   1.496      val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
   1.497      val _ = if null extraTs then ()
   1.498        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
   1.499  
   1.500 -    val params = body_elems |>
   1.501 -      map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat;
   1.502 -
   1.503 +    val satisfy = Element.satisfy_morphism b_axioms;
   1.504 +    val params = fors @
   1.505 +      (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
   1.506      val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
   1.507  
   1.508      val notes = body_elems' |>
   1.509 -      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness axioms)) |>
   1.510 -      fst |>
   1.511 +      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
   1.512 +      fst |> map (Element.morph_ctxt satisfy) |>
   1.513        map_filter (fn Notes notes => SOME notes | _ => NONE);
   1.514  
   1.515 +    val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
   1.516 +
   1.517      val loc_ctxt = thy' |>
   1.518 -      NewLocale.register_locale name (extraTs, params) (statement, defns) ([], [])
   1.519 -        (map (fn n => (n, stamp ())) notes |> rev) [] |>
   1.520 +      NewLocale.register_locale name (extraTs, params)
   1.521 +        (if is_some b_statement then b_statement else a_statement, map prop_of defs) ([], [])
   1.522 +        (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
   1.523        NewLocale.init name
   1.524    in (name, loc_ctxt) end;
   1.525