src/Pure/Isar/expression.ML
changeset 28879 db2816a37a34
parent 28872 686963dbf6cd
child 28885 6f6bf52e75bb
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Nov 24 18:02:52 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Nov 24 18:03:48 2008 +0100
     1.3 @@ -15,6 +15,12 @@
     1.4    type expression = (string * string map) expr * (Name.binding * string option * mixfix) list
     1.5  (*  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list *)
     1.6  
     1.7 +  (* Processing of locale statements *)
     1.8 +  val read_statement: Element.context list -> (string * string list) list list ->
     1.9 +    Proof.context ->  (term * term list) list list * Proof.context;
    1.10 +  val cert_statement: Element.context_i list -> (term * term list) list list ->
    1.11 +    Proof.context -> (term * term list) list list * Proof.context;
    1.12 +
    1.13    (* Declaring locales *)
    1.14    val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
    1.15      string * Proof.context
    1.16 @@ -27,7 +33,7 @@
    1.17  end;
    1.18  
    1.19  
    1.20 -structure Expression: EXPRESSION =
    1.21 +structure Expression (*: EXPRESSION *) =
    1.22  struct
    1.23  
    1.24  datatype ctxt = datatype Element.ctxt;
    1.25 @@ -131,8 +137,8 @@
    1.26              val (ps, loc') = params_loc loc;
    1.27  	    val d = length ps - length insts;
    1.28  	    val insts' =
    1.29 -	      if d < 0 then err_in_expr thy "More arguments than parameters in instantiation."
    1.30 -                (Expr [expr])
    1.31 +	      if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
    1.32 +                quote (NewLocale.extern thy loc))
    1.33  	      else insts @ replicate d NONE;
    1.34              val ps' = (ps ~~ insts') |>
    1.35                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    1.36 @@ -401,7 +407,7 @@
    1.37    let
    1.38      val thy = ProofContext.theory_of context;
    1.39  
    1.40 -    fun prep_inst (loc, (prfx, inst)) (i, ids, insts, ctxt) =
    1.41 +    fun prep_inst (loc, (prfx, inst)) (i, marked, insts, ctxt) =
    1.42        let
    1.43          val (parm_names, parm_types) = NewLocale.params_of thy loc |>
    1.44            map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
    1.45 @@ -412,8 +418,8 @@
    1.46          val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt;
    1.47          val inst''' = insts'' |> List.last |> snd |> snd;
    1.48          val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
    1.49 -        val (ids', ctxt'') = NewLocale.activate_declarations loc morph thy ids ctxt;
    1.50 -      in (i+1, ids', insts', ctxt'') end;
    1.51 +        val (marked', ctxt'') = NewLocale.activate_declarations thy (loc, morph) (marked, ctxt);
    1.52 +      in (i+1, marked', insts', ctxt'') end;
    1.53    
    1.54      fun prep_elem raw_elem (insts, elems, ctxt) =
    1.55        let
    1.56 @@ -470,7 +476,7 @@
    1.57  
    1.58  fun read_elems x = prep_elems Syntax.parse_typ Syntax.parse_prop parse_inst
    1.59    ProofContext.read_vars x;
    1.60 -fun cert_elems x = prep_elems (K I) (K I) make_inst
    1.61 +fun cert_elems x = prep_elems (K I) (K I)  make_inst
    1.62    ProofContext.cert_vars x;
    1.63  
    1.64  end;
    1.65 @@ -480,31 +486,39 @@
    1.66  
    1.67  local
    1.68  
    1.69 -fun prep_context_statement prep_expr prep_elems
    1.70 +fun prep_context_statement prep_expr prep_elems activate_elems
    1.71      do_close imprt elements raw_concl context =
    1.72    let
    1.73      val thy = ProofContext.theory_of context;
    1.74  
    1.75      val (Expr expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
    1.76 -    val ctxt = context |> ProofContext.add_fixes fixed |> snd;
    1.77 -    (* FIXME push inside prep_elems *)
    1.78      val ((parms, fors, deps, elems, concl), (spec, (_, _, defs))) =
    1.79        prep_elems do_close context fixed expr elements raw_concl;
    1.80 -    (* FIXME activate deps *)
    1.81 -    val ((elems', _), ctxt') =
    1.82 -      Element.activate elems (ProofContext.set_stmt true ctxt);
    1.83 +
    1.84 +    val (_, ctxt0) = ProofContext.add_fixes_i fors context;
    1.85 +    val (_, ctxt) = fold (NewLocale.activate_facts thy) deps (NewLocale.empty, ctxt0);  
    1.86 +    val ((elems', _), ctxt') = activate_elems elems (ProofContext.set_stmt true ctxt);
    1.87    in
    1.88      (((fors, deps), (ctxt', elems'), (parms, spec, defs)), concl)
    1.89 -  end
    1.90 +  end;
    1.91 +
    1.92 +fun prep_statement prep_ctxt elems concl ctxt =
    1.93 +  let
    1.94 +    val (((_, (ctxt', _), _)), concl) = prep_ctxt false (Expr [], []) elems concl ctxt
    1.95 +  in (concl, ctxt') end;
    1.96  
    1.97  in
    1.98  
    1.99 +fun read_statement body concl ctxt =
   1.100 +  prep_statement (prep_context_statement intern read_elems Element.activate) body concl ctxt;
   1.101 +fun cert_statement body concl ctxt =
   1.102 +  prep_statement (prep_context_statement (K I) cert_elems Element.activate_i) body concl ctxt;
   1.103 +
   1.104  fun read_context imprt body ctxt =
   1.105 -  #1 (prep_context_statement intern read_elems true imprt body [] ctxt);
   1.106 -(*
   1.107 +  #1 (prep_context_statement intern read_elems Element.activate true imprt body [] ctxt);
   1.108  fun cert_context imprt body ctxt =
   1.109 -  #1 (prep_context_statement (K I) cert_elems true imprt body [] ctxt);
   1.110 -*)
   1.111 +  #1 (prep_context_statement (K I) cert_elems Element.activate_i true imprt body [] ctxt);
   1.112 +
   1.113  end;
   1.114  
   1.115