tuned;
authorwenzelm
Sun Mar 29 19:41:04 2009 +0200 (2009-03-29)
changeset 3077846de352e018b
parent 30777 9960ff945c52
child 30784 bd879a0e1f89
tuned;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 29 18:06:14 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 19:41:04 2009 +0200
     1.3 @@ -70,12 +70,12 @@
     1.4  fun intern thy instances =  map (apfst (Locale.intern thy)) instances;
     1.5  
     1.6  
     1.7 -(** Parameters of expression.
     1.8 +(** Parameters of expression **)
     1.9  
    1.10 -   Sanity check of instantiations and extraction of implicit parameters.
    1.11 -   The latter only occurs iff strict = false.
    1.12 -   Positional instantiations are extended to match full length of parameter list
    1.13 -   of instantiated locale. **)
    1.14 +(*Sanity check of instantiations and extraction of implicit parameters.
    1.15 +  The latter only occurs iff strict = false.
    1.16 +  Positional instantiations are extended to match full length of parameter list
    1.17 +  of instantiated locale.*)
    1.18  
    1.19  fun parameters_of thy strict (expr, fixed) =
    1.20    let
    1.21 @@ -88,7 +88,7 @@
    1.22        (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
    1.23  
    1.24      fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
    1.25 -    fun params_inst (expr as (loc, (prfx, Positional insts))) =
    1.26 +    fun params_inst (loc, (prfx, Positional insts)) =
    1.27            let
    1.28              val ps = params_loc loc;
    1.29              val d = length ps - length insts;
    1.30 @@ -99,24 +99,22 @@
    1.31              val ps' = (ps ~~ insts') |>
    1.32                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    1.33            in (ps', (loc, (prfx, Positional insts'))) end
    1.34 -      | params_inst (expr as (loc, (prfx, Named insts))) =
    1.35 +      | params_inst (loc, (prfx, Named insts)) =
    1.36            let
    1.37              val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
    1.38                (map fst insts);
    1.39 -
    1.40 -            val ps = params_loc loc;
    1.41 -            val ps' = fold (fn (p, _) => fn ps =>
    1.42 +            val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
    1.43                if AList.defined (op =) ps p then AList.delete (op =) p ps
    1.44 -              else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
    1.45 +              else error (quote p ^ " not a parameter of instantiated expression"));
    1.46            in (ps', (loc, (prfx, Named insts))) end;
    1.47      fun params_expr is =
    1.48 +      let
    1.49 +        val (is', ps') = fold_map (fn i => fn ps =>
    1.50            let
    1.51 -            val (is', ps') = fold_map (fn i => fn ps =>
    1.52 -              let
    1.53 -                val (ps', i') = params_inst i;
    1.54 -                val ps'' = distinct parm_eq (ps @ ps');
    1.55 -              in (i', ps'') end) is []
    1.56 -          in (ps', is') end;
    1.57 +            val (ps', i') = params_inst i;
    1.58 +            val ps'' = distinct parm_eq (ps @ ps');
    1.59 +          in (i', ps'') end) is []
    1.60 +      in (ps', is') end;
    1.61  
    1.62      val (implicit, expr') = params_expr expr;
    1.63  
    1.64 @@ -343,7 +341,7 @@
    1.65  
    1.66      val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
    1.67  
    1.68 -    fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
    1.69 +    fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) =
    1.70        let
    1.71          val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
    1.72          val inst' = prep_inst ctxt parm_names inst;
    1.73 @@ -361,7 +359,7 @@
    1.74        let
    1.75          val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
    1.76          val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
    1.77 -        val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
    1.78 +        val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt';
    1.79        in (elems', ctxt') end;
    1.80  
    1.81      fun prep_concl raw_concl (insts, elems, ctxt) =
    1.82 @@ -371,11 +369,10 @@
    1.83  
    1.84      val fors = prep_vars_inst fixed ctxt1 |> fst;
    1.85      val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
    1.86 -    val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
    1.87 +    val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
    1.88      val ctxt4 = init_body ctxt3;
    1.89      val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
    1.90 -    val (insts, elems', concl, ctxt6) =
    1.91 -      prep_concl raw_concl (insts', elems, ctxt5);
    1.92 +    val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
    1.93  
    1.94      (* Retrieve parameter types *)
    1.95      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)