merged
authorwenzelm
Sun Mar 29 19:48:35 2009 +0200 (2009-03-29)
changeset 30784bd879a0e1f89
parent 30783 275577cefaa8
parent 30778 46de352e018b
child 30785 15f64e05e703
child 30810 83642621425a
merged
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/element.ML	Sun Mar 29 17:38:01 2009 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sun Mar 29 19:48:35 2009 +0200
     1.3 @@ -60,8 +60,9 @@
     1.4      (Attrib.binding * (thm list * Attrib.src list) list) list
     1.5    val eq_morphism: theory -> thm list -> morphism
     1.6    val transfer_morphism: theory -> morphism
     1.7 -  val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
     1.8 -  val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
     1.9 +  val init: context_i -> Context.generic -> Context.generic
    1.10 +  val activate_i: context_i -> Proof.context -> context_i * Proof.context
    1.11 +  val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
    1.12  end;
    1.13  
    1.14  structure Element: ELEMENT =
    1.15 @@ -481,64 +482,54 @@
    1.16  
    1.17  
    1.18  
    1.19 -(** activate in context, return elements and facts **)
    1.20 +(** activate in context **)
    1.21  
    1.22 -local
    1.23 +(* init *)
    1.24  
    1.25 -fun activate_elem (Fixes fixes) ctxt =
    1.26 -      ctxt |> ProofContext.add_fixes fixes |> snd
    1.27 -  | activate_elem (Constrains _) ctxt =
    1.28 -      ctxt
    1.29 -  | activate_elem (Assumes asms) ctxt =
    1.30 +fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
    1.31 +  | init (Constrains _) = I
    1.32 +  | init (Assumes asms) = Context.map_proof (fn ctxt =>
    1.33        let
    1.34          val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
    1.35 -        val ts = maps (map #1 o #2) asms';
    1.36 -        val (_, ctxt') =
    1.37 -          ctxt |> fold Variable.auto_fixes ts
    1.38 -          |> ProofContext.add_assms_i Assumption.presume_export asms';
    1.39 -      in ctxt' end
    1.40 -  | activate_elem (Defines defs) ctxt =
    1.41 +        val (_, ctxt') = ctxt
    1.42 +          |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
    1.43 +          |> ProofContext.add_assms_i Assumption.assume_export asms';
    1.44 +      in ctxt' end)
    1.45 +  | init (Defines defs) = Context.map_proof (fn ctxt =>
    1.46        let
    1.47          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    1.48          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    1.49 -            let val ((c, _), t') = LocalDefs.cert_def ctxt t
    1.50 +            let val ((c, _), t') = LocalDefs.cert_def ctxt t  (* FIXME adapt ps? *)
    1.51              in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
    1.52 -        val (_, ctxt') =
    1.53 -          ctxt |> fold (Variable.auto_fixes o #1) asms
    1.54 +        val (_, ctxt') = ctxt
    1.55 +          |> fold Variable.auto_fixes (map #1 asms)
    1.56            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
    1.57 -      in ctxt' end
    1.58 -  | activate_elem (Notes (kind, facts)) ctxt =
    1.59 +      in ctxt' end)
    1.60 +  | init (Notes (kind, facts)) = (fn context =>
    1.61        let
    1.62 -        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
    1.63 -        val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts';
    1.64 -      in ctxt' end;
    1.65 +        val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
    1.66 +        val context' = context |> Context.mapping
    1.67 +          (PureThy.note_thmss kind facts' #> #2)
    1.68 +          (ProofContext.note_thmss kind facts' #> #2);
    1.69 +      in context' end);
    1.70  
    1.71 -fun gen_activate prep_facts raw_elems ctxt =
    1.72 +
    1.73 +(* activate *)
    1.74 +
    1.75 +fun activate_i elem ctxt =
    1.76    let
    1.77 -    fun activate elem ctxt =
    1.78 -      let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
    1.79 -      in (elem', activate_elem elem' ctxt) end
    1.80 -    val (elems, ctxt') = fold_map activate raw_elems ctxt;
    1.81 -  in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
    1.82 +    val elem' = map_ctxt_attrib Args.assignable elem;
    1.83 +    val ctxt' = Context.proof_map (init elem') ctxt;
    1.84 +  in (map_ctxt_attrib Args.closure elem', ctxt') end;
    1.85  
    1.86 -fun check_name name =
    1.87 -  if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
    1.88 -  else name;
    1.89 -
    1.90 -fun prep_facts prep_name get intern ctxt =
    1.91 -  map_ctxt
    1.92 -   {binding = Binding.map_name prep_name,
    1.93 +fun activate raw_elem ctxt =
    1.94 +  let val elem = raw_elem |> map_ctxt
    1.95 +   {binding = tap Name.of_binding,
    1.96      typ = I,
    1.97      term = I,
    1.98      pattern = I,
    1.99 -    fact = get ctxt,
   1.100 -    attrib = intern (ProofContext.theory_of ctxt)};
   1.101 -
   1.102 -in
   1.103 -
   1.104 -fun activate x = gen_activate (prep_facts check_name ProofContext.get_fact Attrib.intern_src) x;
   1.105 -fun activate_i x = gen_activate (K I) x;
   1.106 +    fact = ProofContext.get_fact ctxt,
   1.107 +    attrib = Attrib.intern_src (ProofContext.theory_of ctxt)}
   1.108 +  in activate_i elem ctxt end;
   1.109  
   1.110  end;
   1.111 -
   1.112 -end;
     2.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 29 17:38:01 2009 +0200
     2.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 19:48:35 2009 +0200
     2.3 @@ -70,12 +70,12 @@
     2.4  fun intern thy instances =  map (apfst (Locale.intern thy)) instances;
     2.5  
     2.6  
     2.7 -(** Parameters of expression.
     2.8 +(** Parameters of expression **)
     2.9  
    2.10 -   Sanity check of instantiations and extraction of implicit parameters.
    2.11 -   The latter only occurs iff strict = false.
    2.12 -   Positional instantiations are extended to match full length of parameter list
    2.13 -   of instantiated locale. **)
    2.14 +(*Sanity check of instantiations and extraction of implicit parameters.
    2.15 +  The latter only occurs iff strict = false.
    2.16 +  Positional instantiations are extended to match full length of parameter list
    2.17 +  of instantiated locale.*)
    2.18  
    2.19  fun parameters_of thy strict (expr, fixed) =
    2.20    let
    2.21 @@ -88,7 +88,7 @@
    2.22        (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
    2.23  
    2.24      fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
    2.25 -    fun params_inst (expr as (loc, (prfx, Positional insts))) =
    2.26 +    fun params_inst (loc, (prfx, Positional insts)) =
    2.27            let
    2.28              val ps = params_loc loc;
    2.29              val d = length ps - length insts;
    2.30 @@ -99,24 +99,22 @@
    2.31              val ps' = (ps ~~ insts') |>
    2.32                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    2.33            in (ps', (loc, (prfx, Positional insts'))) end
    2.34 -      | params_inst (expr as (loc, (prfx, Named insts))) =
    2.35 +      | params_inst (loc, (prfx, Named insts)) =
    2.36            let
    2.37              val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
    2.38                (map fst insts);
    2.39 -
    2.40 -            val ps = params_loc loc;
    2.41 -            val ps' = fold (fn (p, _) => fn ps =>
    2.42 +            val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
    2.43                if AList.defined (op =) ps p then AList.delete (op =) p ps
    2.44 -              else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
    2.45 +              else error (quote p ^ " not a parameter of instantiated expression"));
    2.46            in (ps', (loc, (prfx, Named insts))) end;
    2.47      fun params_expr is =
    2.48 +      let
    2.49 +        val (is', ps') = fold_map (fn i => fn ps =>
    2.50            let
    2.51 -            val (is', ps') = fold_map (fn i => fn ps =>
    2.52 -              let
    2.53 -                val (ps', i') = params_inst i;
    2.54 -                val ps'' = distinct parm_eq (ps @ ps');
    2.55 -              in (i', ps'') end) is []
    2.56 -          in (ps', is') end;
    2.57 +            val (ps', i') = params_inst i;
    2.58 +            val ps'' = distinct parm_eq (ps @ ps');
    2.59 +          in (i', ps'') end) is []
    2.60 +      in (ps', is') end;
    2.61  
    2.62      val (implicit, expr') = params_expr expr;
    2.63  
    2.64 @@ -158,7 +156,7 @@
    2.65  
    2.66  (* Instantiation morphism *)
    2.67  
    2.68 -fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt =
    2.69 +fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
    2.70    let
    2.71      (* parameters *)
    2.72      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
    2.73 @@ -173,13 +171,13 @@
    2.74      (* instantiation *)
    2.75      val (type_parms'', res') = chop (length type_parms) res;
    2.76      val insts'' = (parm_names ~~ res') |> map_filter
    2.77 -      (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
    2.78 -        inst => SOME inst);
    2.79 +      (fn inst as (x, Free (y, _)) => if x = y then NONE else SOME inst
    2.80 +        | inst => SOME inst);
    2.81      val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
    2.82      val inst = Symtab.make insts'';
    2.83    in
    2.84      (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
    2.85 -      Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
    2.86 +      Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
    2.87    end;
    2.88  
    2.89  
    2.90 @@ -242,7 +240,7 @@
    2.91        in
    2.92          ((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
    2.93            (ctxt', ts))
    2.94 -      end
    2.95 +      end;
    2.96      val (cs', (context', _)) = fold_map prep cs
    2.97        (context, Syntax.check_terms
    2.98          (ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
    2.99 @@ -260,7 +258,8 @@
   2.100        (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
   2.101      val (elem_css', [concl_cs']) = chop (length elem_css) css';
   2.102    in
   2.103 -    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
   2.104 +    (map restore_inst (insts ~~ inst_cs'),
   2.105 +      map restore_elem (elems ~~ elem_css'),
   2.106        concl_cs', ctxt')
   2.107    end;
   2.108  
   2.109 @@ -278,6 +277,7 @@
   2.110    | declare_elem _ (Defines _) ctxt = ctxt
   2.111    | declare_elem _ (Notes _) ctxt = ctxt;
   2.112  
   2.113 +
   2.114  (** Finish locale elements **)
   2.115  
   2.116  fun closeup _ _ false elem = elem
   2.117 @@ -341,7 +341,7 @@
   2.118  
   2.119      val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
   2.120  
   2.121 -    fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
   2.122 +    fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) =
   2.123        let
   2.124          val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   2.125          val inst' = prep_inst ctxt parm_names inst;
   2.126 @@ -359,7 +359,7 @@
   2.127        let
   2.128          val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
   2.129          val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
   2.130 -        val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
   2.131 +        val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt';
   2.132        in (elems', ctxt') end;
   2.133  
   2.134      fun prep_concl raw_concl (insts, elems, ctxt) =
   2.135 @@ -369,11 +369,10 @@
   2.136  
   2.137      val fors = prep_vars_inst fixed ctxt1 |> fst;
   2.138      val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
   2.139 -    val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
   2.140 +    val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
   2.141      val ctxt4 = init_body ctxt3;
   2.142      val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
   2.143 -    val (insts, elems', concl, ctxt6) =
   2.144 -      prep_concl raw_concl (insts', elems, ctxt5);
   2.145 +    val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
   2.146  
   2.147      (* Retrieve parameter types *)
   2.148      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)
   2.149 @@ -392,9 +391,11 @@
   2.150  fun cert_full_context_statement x =
   2.151    prep_full_context_statement (K I) (K I) ProofContext.cert_vars
   2.152    make_inst ProofContext.cert_vars (K I) x;
   2.153 +
   2.154  fun cert_read_full_context_statement x =
   2.155    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
   2.156    make_inst ProofContext.cert_vars (K I) x;
   2.157 +
   2.158  fun read_full_context_statement x =
   2.159    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
   2.160    parse_inst ProofContext.read_vars intern x;
   2.161 @@ -412,7 +413,7 @@
   2.162         prep true false ([], []) I raw_elems raw_concl context;
   2.163       val (_, context') = context |>
   2.164         ProofContext.set_stmt true |>
   2.165 -       activate elems;
   2.166 +       fold_map activate elems;
   2.167    in (concl, context') end;
   2.168  
   2.169  in
   2.170 @@ -440,7 +441,7 @@
   2.171        fold (Context.proof_map o Locale.activate_facts) deps;
   2.172      val (elems', _) = context' |>
   2.173        ProofContext.set_stmt true |>
   2.174 -      activate elems;
   2.175 +      fold_map activate elems;
   2.176    in ((fixed, deps, elems'), (parms, ctxt')) end;
   2.177  
   2.178  in
   2.179 @@ -727,7 +728,8 @@
   2.180      val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
   2.181      val _ =
   2.182        if null extraTs then ()
   2.183 -      else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname));
   2.184 +      else warning ("Additional type variable(s) in locale specification " ^
   2.185 +        quote (Binding.str_of bname));
   2.186  
   2.187      val a_satisfy = Element.satisfy_morphism a_axioms;
   2.188      val b_satisfy = Element.satisfy_morphism b_axioms;
     3.1 --- a/src/Pure/Isar/locale.ML	Sun Mar 29 17:38:01 2009 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Sun Mar 29 19:48:35 2009 +0200
     3.3 @@ -245,7 +245,7 @@
     3.4      val dependencies' = filter_out (fn (name, morph) =>
     3.5        member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
     3.6    in
     3.7 -    (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
     3.8 +    (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
     3.9    end;
    3.10  
    3.11  end;
    3.12 @@ -285,59 +285,28 @@
    3.13        (if not (null defs)
    3.14          then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
    3.15          else I);
    3.16 +    val activate = activate_notes activ_elem transfer thy;
    3.17    in
    3.18 -    roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
    3.19 +    roundup thy activate (name, Morphism.identity) (marked, input')
    3.20    end;
    3.21  
    3.22  
    3.23  (** Public activation functions **)
    3.24  
    3.25 -local
    3.26 -
    3.27 -fun init_elem (Fixes fixes) (Context.Proof ctxt) =
    3.28 -      Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
    3.29 -  | init_elem (Assumes assms) (Context.Proof ctxt) =
    3.30 -      let
    3.31 -        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
    3.32 -        val ctxt' = ctxt
    3.33 -          |> fold Variable.auto_fixes (maps (map fst o snd) assms')
    3.34 -          |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
    3.35 -      in Context.Proof ctxt' end
    3.36 -  | init_elem (Defines defs) (Context.Proof ctxt) =
    3.37 -      let
    3.38 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    3.39 -        val ctxt' = ctxt
    3.40 -          |> fold Variable.auto_fixes (map (fst o snd) defs')
    3.41 -          |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
    3.42 -          |> snd;
    3.43 -      in Context.Proof ctxt' end
    3.44 -  | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
    3.45 -      let
    3.46 -        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
    3.47 -      in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
    3.48 -  | init_elem (Notes (kind, facts)) (Context.Theory thy) =
    3.49 -      let
    3.50 -        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
    3.51 -      in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
    3.52 -  | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
    3.53 -
    3.54 -in
    3.55 -
    3.56 -fun activate_declarations dep ctxt =
    3.57 +fun activate_declarations dep = Context.proof_map (fn context =>
    3.58    let
    3.59 -    val context = Context.Proof ctxt;
    3.60      val thy = Context.theory_of context;
    3.61 -    val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents;
    3.62 -  in Context.the_proof context' end;
    3.63 +    val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
    3.64 +  in context' end);
    3.65  
    3.66  fun activate_facts dep context =
    3.67    let
    3.68      val thy = Context.theory_of context;
    3.69 -    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of);
    3.70 +    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
    3.71    in roundup thy activate dep (get_idents context, context) |-> put_idents end;
    3.72  
    3.73  fun init name thy =
    3.74 -  activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
    3.75 +  activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
    3.76      ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
    3.77  
    3.78  fun print_locale thy show_facts raw_name =
    3.79 @@ -354,8 +323,6 @@
    3.80      |> Pretty.writeln
    3.81    end;
    3.82  
    3.83 -end;
    3.84 -
    3.85  
    3.86  (*** Registrations: interpretations in theories ***)
    3.87  
    3.88 @@ -375,8 +342,7 @@
    3.89    Registrations.get #> map (#1 #> apsnd op $>);
    3.90  
    3.91  fun add_registration (name, (base_morph, export)) thy =
    3.92 -  roundup thy (fn _ => fn (name', morph') =>
    3.93 -    Registrations.map (cons ((name', (morph', export)), stamp ())))
    3.94 +  roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
    3.95      (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
    3.96      (* FIXME |-> put_global_idents ?*)
    3.97  
    3.98 @@ -398,14 +364,13 @@
    3.99    end;
   3.100  
   3.101  
   3.102 -
   3.103  (*** Storing results ***)
   3.104  
   3.105  (* Theorems *)
   3.106  
   3.107  fun add_thmss loc kind args ctxt =
   3.108    let
   3.109 -    val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
   3.110 +    val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
   3.111      val ctxt'' = ctxt' |> ProofContext.theory (
   3.112        (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
   3.113          #>