src/Pure/Isar/expression.ML
changeset 30784 bd879a0e1f89
parent 30783 275577cefaa8
parent 30778 46de352e018b
child 30786 461f7b5f16a2
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 29 17:38:01 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 19:48:35 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 @@ -158,7 +156,7 @@
    1.65  
    1.66  (* Instantiation morphism *)
    1.67  
    1.68 -fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt =
    1.69 +fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
    1.70    let
    1.71      (* parameters *)
    1.72      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
    1.73 @@ -173,13 +171,13 @@
    1.74      (* instantiation *)
    1.75      val (type_parms'', res') = chop (length type_parms) res;
    1.76      val insts'' = (parm_names ~~ res') |> map_filter
    1.77 -      (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
    1.78 -        inst => SOME inst);
    1.79 +      (fn inst as (x, Free (y, _)) => if x = y then NONE else SOME inst
    1.80 +        | inst => SOME inst);
    1.81      val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
    1.82      val inst = Symtab.make insts'';
    1.83    in
    1.84      (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
    1.85 -      Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
    1.86 +      Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
    1.87    end;
    1.88  
    1.89  
    1.90 @@ -242,7 +240,7 @@
    1.91        in
    1.92          ((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
    1.93            (ctxt', ts))
    1.94 -      end
    1.95 +      end;
    1.96      val (cs', (context', _)) = fold_map prep cs
    1.97        (context, Syntax.check_terms
    1.98          (ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
    1.99 @@ -260,7 +258,8 @@
   1.100        (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
   1.101      val (elem_css', [concl_cs']) = chop (length elem_css) css';
   1.102    in
   1.103 -    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
   1.104 +    (map restore_inst (insts ~~ inst_cs'),
   1.105 +      map restore_elem (elems ~~ elem_css'),
   1.106        concl_cs', ctxt')
   1.107    end;
   1.108  
   1.109 @@ -278,6 +277,7 @@
   1.110    | declare_elem _ (Defines _) ctxt = ctxt
   1.111    | declare_elem _ (Notes _) ctxt = ctxt;
   1.112  
   1.113 +
   1.114  (** Finish locale elements **)
   1.115  
   1.116  fun closeup _ _ false elem = elem
   1.117 @@ -341,7 +341,7 @@
   1.118  
   1.119      val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
   1.120  
   1.121 -    fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
   1.122 +    fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) =
   1.123        let
   1.124          val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   1.125          val inst' = prep_inst ctxt parm_names inst;
   1.126 @@ -359,7 +359,7 @@
   1.127        let
   1.128          val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
   1.129          val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
   1.130 -        val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
   1.131 +        val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt';
   1.132        in (elems', ctxt') end;
   1.133  
   1.134      fun prep_concl raw_concl (insts, elems, ctxt) =
   1.135 @@ -369,11 +369,10 @@
   1.136  
   1.137      val fors = prep_vars_inst fixed ctxt1 |> fst;
   1.138      val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
   1.139 -    val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
   1.140 +    val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
   1.141      val ctxt4 = init_body ctxt3;
   1.142      val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
   1.143 -    val (insts, elems', concl, ctxt6) =
   1.144 -      prep_concl raw_concl (insts', elems, ctxt5);
   1.145 +    val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
   1.146  
   1.147      (* Retrieve parameter types *)
   1.148      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)
   1.149 @@ -392,9 +391,11 @@
   1.150  fun cert_full_context_statement x =
   1.151    prep_full_context_statement (K I) (K I) ProofContext.cert_vars
   1.152    make_inst ProofContext.cert_vars (K I) x;
   1.153 +
   1.154  fun cert_read_full_context_statement x =
   1.155    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
   1.156    make_inst ProofContext.cert_vars (K I) x;
   1.157 +
   1.158  fun read_full_context_statement x =
   1.159    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
   1.160    parse_inst ProofContext.read_vars intern x;
   1.161 @@ -412,7 +413,7 @@
   1.162         prep true false ([], []) I raw_elems raw_concl context;
   1.163       val (_, context') = context |>
   1.164         ProofContext.set_stmt true |>
   1.165 -       activate elems;
   1.166 +       fold_map activate elems;
   1.167    in (concl, context') end;
   1.168  
   1.169  in
   1.170 @@ -440,7 +441,7 @@
   1.171        fold (Context.proof_map o Locale.activate_facts) deps;
   1.172      val (elems', _) = context' |>
   1.173        ProofContext.set_stmt true |>
   1.174 -      activate elems;
   1.175 +      fold_map activate elems;
   1.176    in ((fixed, deps, elems'), (parms, ctxt')) end;
   1.177  
   1.178  in
   1.179 @@ -727,7 +728,8 @@
   1.180      val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
   1.181      val _ =
   1.182        if null extraTs then ()
   1.183 -      else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname));
   1.184 +      else warning ("Additional type variable(s) in locale specification " ^
   1.185 +        quote (Binding.str_of bname));
   1.186  
   1.187      val a_satisfy = Element.satisfy_morphism a_axioms;
   1.188      val b_satisfy = Element.satisfy_morphism b_axioms;