src/Pure/Isar/expression.ML
changeset 30783 275577cefaa8
parent 30781 7fb900cad123
parent 30764 3e3e7aa0cc7a
child 30784 bd879a0e1f89
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 29 17:25:06 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 17:38:01 2009 +0200
     1.3 @@ -20,14 +20,14 @@
     1.4  
     1.5    (* Declaring locales *)
     1.6    val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
     1.7 -    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
     1.8 +    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
     1.9        * Element.context_i list) * ((string * typ) list * Proof.context)
    1.10    val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
    1.11 -    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
    1.12 +    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    1.13        * Element.context_i list) * ((string * typ) list * Proof.context)
    1.14        (*FIXME*)
    1.15    val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
    1.16 -    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
    1.17 +    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    1.18        * Element.context_i list) * ((string * typ) list * Proof.context)
    1.19    val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
    1.20      theory -> string * local_theory
    1.21 @@ -80,22 +80,17 @@
    1.22  fun parameters_of thy strict (expr, fixed) =
    1.23    let
    1.24      fun reject_dups message xs =
    1.25 -      let val dups = duplicates (op =) xs
    1.26 -      in
    1.27 -        if null dups then () else error (message ^ commas dups)
    1.28 -      end;
    1.29 +      (case duplicates (op =) xs of
    1.30 +        [] => ()
    1.31 +      | dups => error (message ^ commas dups));
    1.32  
    1.33 -    fun match_bind (n, b) = (n = Binding.name_of b);
    1.34 -    fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
    1.35 -      Binding.eq_name (b1, b2) andalso
    1.36 -        (mx1 = mx2 orelse
    1.37 -          error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
    1.38 +    fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso
    1.39 +      (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
    1.40  
    1.41 -    fun params_loc loc =
    1.42 -      (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
    1.43 +    fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
    1.44      fun params_inst (expr as (loc, (prfx, Positional insts))) =
    1.45            let
    1.46 -            val (ps, loc') = params_loc loc;
    1.47 +            val ps = params_loc loc;
    1.48              val d = length ps - length insts;
    1.49              val insts' =
    1.50                if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
    1.51 @@ -103,17 +98,17 @@
    1.52                else insts @ replicate d NONE;
    1.53              val ps' = (ps ~~ insts') |>
    1.54                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    1.55 -          in (ps', (loc', (prfx, Positional insts'))) end
    1.56 +          in (ps', (loc, (prfx, Positional insts'))) end
    1.57        | params_inst (expr as (loc, (prfx, Named insts))) =
    1.58            let
    1.59              val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
    1.60                (map fst insts);
    1.61  
    1.62 -            val (ps, loc') = params_loc loc;
    1.63 +            val ps = params_loc loc;
    1.64              val ps' = fold (fn (p, _) => fn ps =>
    1.65 -              if AList.defined match_bind ps p then AList.delete match_bind p ps
    1.66 -              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
    1.67 -          in (ps', (loc', (prfx, Named insts))) end;
    1.68 +              if AList.defined (op =) ps p then AList.delete (op =) p ps
    1.69 +              else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
    1.70 +          in (ps', (loc, (prfx, Named insts))) end;
    1.71      fun params_expr is =
    1.72            let
    1.73              val (is', ps') = fold_map (fn i => fn ps =>
    1.74 @@ -125,7 +120,7 @@
    1.75  
    1.76      val (implicit, expr') = params_expr expr;
    1.77  
    1.78 -    val implicit' = map (#1 #> Name.of_binding) implicit;
    1.79 +    val implicit' = map #1 implicit;
    1.80      val fixed' = map (#1 #> Name.of_binding) fixed;
    1.81      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
    1.82      val implicit'' =
    1.83 @@ -133,7 +128,7 @@
    1.84        else
    1.85          let val _ = reject_dups
    1.86            "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
    1.87 -        in map (fn (b, mx) => (b, NONE, mx)) implicit end;
    1.88 +        in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
    1.89  
    1.90    in (expr', implicit'' @ fixed) end;
    1.91  
    1.92 @@ -276,7 +271,7 @@
    1.93  
    1.94  fun declare_elem prep_vars (Fixes fixes) ctxt =
    1.95        let val (vars, _) = prep_vars fixes ctxt
    1.96 -      in ctxt |> ProofContext.add_fixes_i vars |> snd end
    1.97 +      in ctxt |> ProofContext.add_fixes vars |> snd end
    1.98    | declare_elem prep_vars (Constrains csts) ctxt =
    1.99        ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
   1.100    | declare_elem _ (Assumes _) ctxt = ctxt
   1.101 @@ -319,8 +314,7 @@
   1.102  fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
   1.103    let
   1.104      val thy = ProofContext.theory_of ctxt;
   1.105 -    val (parm_names, parm_types) = Locale.params_of thy loc |>
   1.106 -      map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
   1.107 +    val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   1.108      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   1.109    in (loc, morph) end;
   1.110  
   1.111 @@ -349,9 +343,7 @@
   1.112  
   1.113      fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
   1.114        let
   1.115 -        val (parm_names, parm_types) = Locale.params_of thy loc |>
   1.116 -          map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
   1.117 -            (*FIXME return value of Locale.params_of has strange type*)
   1.118 +        val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   1.119          val inst' = prep_inst ctxt parm_names inst;
   1.120          val parm_types' = map (TypeInfer.paramify_vars o
   1.121            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
   1.122 @@ -360,7 +352,7 @@
   1.123          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
   1.124          val inst''' = insts'' |> List.last |> snd |> snd;
   1.125          val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
   1.126 -        val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
   1.127 +        val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
   1.128        in (i + 1, insts', ctxt'') end;
   1.129  
   1.130      fun prep_elem insts raw_elem (elems, ctxt) =
   1.131 @@ -376,7 +368,7 @@
   1.132        in check_autofix insts elems concl ctxt end;
   1.133  
   1.134      val fors = prep_vars_inst fixed ctxt1 |> fst;
   1.135 -    val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
   1.136 +    val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
   1.137      val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
   1.138      val ctxt4 = init_body ctxt3;
   1.139      val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
   1.140 @@ -390,9 +382,10 @@
   1.141      val parms = xs ~~ Ts;  (* params from expression and elements *)
   1.142  
   1.143      val Fixes fors' = finish_primitive parms I (Fixes fors);
   1.144 +    val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
   1.145      val (deps, elems'') = finish ctxt6 parms do_close insts elems';
   1.146  
   1.147 -  in ((fors', deps, elems'', concl), (parms, ctxt7)) end
   1.148 +  in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
   1.149  
   1.150  in
   1.151  
   1.152 @@ -432,6 +425,9 @@
   1.153  
   1.154  (* Locale declaration: import + elements *)
   1.155  
   1.156 +fun fix_params params =
   1.157 +  ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
   1.158 +
   1.159  local
   1.160  
   1.161  fun prep_declaration prep activate raw_import init_body raw_elems context =
   1.162 @@ -440,8 +436,8 @@
   1.163        prep false true raw_import init_body raw_elems [] context ;
   1.164      (* Declare parameters and imported facts *)
   1.165      val context' = context |>
   1.166 -      ProofContext.add_fixes_i fixed |> snd |>
   1.167 -      fold Locale.activate_local_facts deps;
   1.168 +      fix_params fixed |>
   1.169 +      fold (Context.proof_map o Locale.activate_facts) deps;
   1.170      val (elems', _) = context' |>
   1.171        ProofContext.set_stmt true |>
   1.172        activate elems;
   1.173 @@ -477,7 +473,7 @@
   1.174      val propss = map (props_of thy) deps;
   1.175  
   1.176      val goal_ctxt = context |>
   1.177 -      ProofContext.add_fixes_i fixed |> snd |>
   1.178 +      fix_params fixed |>
   1.179        (fold o fold) Variable.auto_fixes propss;
   1.180  
   1.181      val export = Variable.export_morphism goal_ctxt context;
   1.182 @@ -658,13 +654,13 @@
   1.183  
   1.184  fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
   1.185    let
   1.186 -    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
   1.187 +    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
   1.188  
   1.189      val (a_pred, a_intro, a_axioms, thy'') =
   1.190        if null exts then (NONE, NONE, [], thy)
   1.191        else
   1.192          let
   1.193 -          val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname
   1.194 +          val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname;
   1.195            val ((statement, intro, axioms), thy') =
   1.196              thy
   1.197              |> def_pred aname parms defs' exts exts';
   1.198 @@ -737,7 +733,8 @@
   1.199      val b_satisfy = Element.satisfy_morphism b_axioms;
   1.200  
   1.201      val params = fixed @
   1.202 -      (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
   1.203 +      maps (fn Fixes fixes =>
   1.204 +        map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
   1.205      val asm = if is_some b_statement then b_statement else a_statement;
   1.206  
   1.207      val notes =
   1.208 @@ -790,7 +787,7 @@
   1.209      fun after_qed witss = ProofContext.theory
   1.210        (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
   1.211          (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
   1.212 -      (fn thy => fold_rev Locale.activate_global_facts
   1.213 +      (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
   1.214          (Locale.get_registrations thy) thy));
   1.215    in Element.witness_proof after_qed propss goal_ctxt end;
   1.216  
   1.217 @@ -830,7 +827,7 @@
   1.218      fun store_eqns_activate regs [] thy =
   1.219            thy
   1.220            |> fold (fn (name, morph) =>
   1.221 -               Locale.activate_global_facts (name, morph $> export)) regs
   1.222 +               Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
   1.223        | store_eqns_activate regs eqs thy =
   1.224            let
   1.225              val eqs' = eqs |> map (Morphism.thm (export' $> export));
   1.226 @@ -842,7 +839,7 @@
   1.227              thy
   1.228              |> fold (fn (name, morph) =>
   1.229                  Locale.amend_registration eq_morph (name, morph) #>
   1.230 -                Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
   1.231 +                Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
   1.232              |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
   1.233              |> snd
   1.234            end;
   1.235 @@ -876,7 +873,7 @@
   1.236      fun store_reg (name, morph) thms =
   1.237        let
   1.238          val morph' = morph $> Element.satisfy_morphism thms $> export;
   1.239 -      in Locale.activate_local_facts (name, morph') end;
   1.240 +      in Context.proof_map (Locale.activate_facts (name, morph')) end;
   1.241  
   1.242      fun after_qed wits =
   1.243        Proof.map_context (fold2 store_reg regs wits);