Deleted debug message (PolyML).
authorballarin
Thu Nov 20 10:29:35 2008 +0100 (2008-11-20)
changeset 28859d50b523c55db
parent 28858 855e61829e22
child 28860 b1d46059d502
Deleted debug message (PolyML).
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Nov 20 00:03:55 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Nov 20 10:29:35 2008 +0100
     1.3 @@ -108,16 +108,16 @@
     1.4    in error err_msg end;
     1.5  
     1.6  
     1.7 -(** Internalise locale names **)
     1.8 +(** Internalise locale names in expr **)
     1.9  
    1.10 -fun intern_expr thy (Expr instances) = Expr (map (apfst (NewLocale.intern thy)) instances);
    1.11 +fun intern thy (Expr instances) = Expr (map (apfst (NewLocale.intern thy)) instances);
    1.12  
    1.13  
    1.14 -(** Parameters of expression (not expression_i).
    1.15 +(** Parameters of expression.
    1.16     Sanity check of instantiations.
    1.17     Positional instantiations are extended to match full length of parameter list. **)
    1.18  
    1.19 -fun parameters thy (expr, fixed : (Name.binding * string option * mixfix) list) =
    1.20 +fun parameters_of thy (expr, fixed) =
    1.21    let
    1.22      fun reject_dups message xs =
    1.23        let val dups = duplicates (op =) xs
    1.24 @@ -130,8 +130,7 @@
    1.25        (* FIXME: cannot compare bindings for equality. *)
    1.26  
    1.27      fun params_loc loc =
    1.28 -          (NewLocale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc)
    1.29 -            handle ERROR msg => err_in_expr thy msg (Expr [(loc, ("", Named []))]);
    1.30 +          (NewLocale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
    1.31      fun params_inst (expr as (loc, (prfx, Positional insts))) =
    1.32            let
    1.33              val (ps, loc') = params_loc loc;
    1.34 @@ -148,14 +147,12 @@
    1.35        | params_inst (expr as (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 -              handle ERROR msg => err_in_expr thy msg (Expr [expr]);
    1.40 +              (map fst insts);
    1.41  
    1.42              val (ps, loc') = params_loc loc;
    1.43              val ps' = fold (fn (p, _) => fn ps =>
    1.44                if AList.defined match_bind ps p then AList.delete match_bind p ps
    1.45 -              else err_in_expr thy (quote p ^" not a parameter of instantiated expression.")
    1.46 -                (Expr [expr])) insts ps;
    1.47 +              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
    1.48            in
    1.49              (ps', (loc', (prfx, Named insts)))
    1.50            end;
    1.51 @@ -168,8 +165,8 @@
    1.52                    (* FIXME: should check for bindings being the same.
    1.53                       Instead we check for equal name and syntax. *)
    1.54                    if mx1 = mx2 then mx1
    1.55 -                  else err_in_expr thy ("Conflicting syntax for parameter" ^ quote (Name.name_of p) ^ " in expression.")
    1.56 -                    (Expr is)) (ps, ps')
    1.57 +                  else error ("Conflicting syntax for parameter" ^ quote (Name.name_of p) ^
    1.58 +                    " in expression.")) (ps, ps')
    1.59                in (i', ps'') end) is []
    1.60            in
    1.61              (ps', Expr is')
    1.62 @@ -177,17 +174,19 @@
    1.63  
    1.64      val (parms, expr') = params_expr expr;
    1.65  
    1.66 -    val parms' = map (fst #> Name.name_of) parms;
    1.67 +    val parms' = map (#1 #> Name.name_of) parms;
    1.68      val fixed' = map (#1 #> Name.name_of) fixed;
    1.69      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
    1.70      val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
    1.71  
    1.72 -  in (expr', (parms, fixed)) end;
    1.73 +  in (expr', (map (fn (b, mx) => (b, NONE, mx)) parms @ fixed)) end;
    1.74  
    1.75  
    1.76  (** Read instantiation **)
    1.77  
    1.78 -fun read_inst parse_term parms (prfx, insts) ctxt =
    1.79 +local
    1.80 +
    1.81 +fun prep_inst parse_term parms (prfx, insts) ctxt =
    1.82    let
    1.83      (* parameters *)
    1.84      val (parm_names, parm_types) = split_list parms;
    1.85 @@ -221,32 +220,36 @@
    1.86      (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
    1.87        Morphism.name_morphism (Name.qualified prfx), ctxt')
    1.88    end;
    1.89 -        
    1.90 +
    1.91 +in
    1.92 +
    1.93 +fun read_inst x = prep_inst Syntax.parse_term x;
    1.94 +(* fun cert_inst x = prep_inst (K I) x; *)
    1.95 +
    1.96 +end;
    1.97 +
    1.98          
    1.99 -(** Debugging **)
   1.100 +(** Test code **)
   1.101    
   1.102  fun debug_parameters raw_expr ctxt =
   1.103    let
   1.104      val thy = ProofContext.theory_of ctxt;
   1.105 -    val expr = apfst (intern_expr thy) raw_expr;
   1.106 -    val (expr', (parms, fixed)) = parameters thy expr;
   1.107 +    val expr = apfst (intern thy) raw_expr;
   1.108 +    val (expr', fixed) = parameters_of thy expr;
   1.109    in ctxt end;
   1.110  
   1.111  
   1.112  fun debug_context (raw_expr, fixed) ctxt =
   1.113    let
   1.114      val thy = ProofContext.theory_of ctxt;
   1.115 -    val expr = intern_expr thy raw_expr;
   1.116 -    val (expr', (parms, fixed)) = parameters thy (expr, fixed);
   1.117 +    val expr = intern thy raw_expr;
   1.118 +    val (expr', fixed) = parameters_of thy (expr, fixed);
   1.119  
   1.120 -    fun declare_parameters (parms, fixed) ctxt =
   1.121 +    fun declare_parameters fixed ctxt =
   1.122        let
   1.123 -      val (parms', ctxt') =
   1.124 -        ProofContext.add_fixes (map (fn (p, mx) => (p, NONE, mx)) parms) ctxt;
   1.125 -      val (fixed', ctxt'') =
   1.126 -        ProofContext.add_fixes fixed ctxt';
   1.127 +      val (fixed', ctxt') = ProofContext.add_fixes fixed ctxt;
   1.128        in
   1.129 -        (parms' @ fixed', ctxt'')
   1.130 +        (fixed', ctxt')
   1.131        end;
   1.132  
   1.133      fun rough_inst loc prfx insts ctxt =
   1.134 @@ -304,7 +307,7 @@
   1.135  
   1.136      val Expr [(loc1, (prfx1, insts1))] = expr';
   1.137      val ctxt0 = ProofContext.init thy;
   1.138 -    val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0;
   1.139 +    val (parms, ctxt') = declare_parameters fixed ctxt0;
   1.140      val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
   1.141      val ctxt'' = add_declarations loc1 morph1 ctxt';
   1.142    in ctxt0 end;
   1.143 @@ -348,8 +351,6 @@
   1.144      val termss = elems |> map extract_elem;
   1.145      val all_terms' = (burrow o burrow_fst) (Syntax.check_terms ctxt) (concl @ flat termss); 
   1.146  (*    val (ctxt', all_props') = ProofContext.check_propp_schematic (ctxt, concl @ flat propss); *)
   1.147 -val _ = "check" |> warning;
   1.148 -val _ = PolyML.makestring all_terms' |> warning;
   1.149      val (concl', terms') = chop (length concl) all_terms';
   1.150      val ctxt'' = (fold o fold) (fn (t, _) => Variable.auto_fixes t) terms' ctxt;
   1.151    in (terms' |> unflat termss |> curry (op ~~) elems |> map restore_elem, concl', ctxt'') end;
   1.152 @@ -476,10 +477,10 @@
   1.153      (* Retrieve parameter types *) 
   1.154      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
   1.155        _ => fn ps => ps) elems [];
   1.156 -    val (Ts, _) = fold_map ProofContext.inferred_param xs ctxt; 
   1.157 +    val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
   1.158      val parms = xs ~~ Ts;
   1.159  
   1.160 -    val (elems', text) = finish_elems ctxt parms do_close elems ((([], []), ([], [])), ([], [], []));
   1.161 +    val (elems', text) = finish_elems ctxt' parms do_close elems ((([], []), ([], [])), ([], [], []));
   1.162      (* text has the following structure:
   1.163             (((exts, exts'), (ints, ints')), (xs, env, defs))
   1.164         where
   1.165 @@ -520,10 +521,8 @@
   1.166    let
   1.167      val thy = ProofContext.theory_of context;
   1.168  
   1.169 -    val (expr, (params, fors)) = parameters thy (apfst (prep_expr thy) imprt);
   1.170 -    val ctxt = context |>
   1.171 -      ProofContext.add_fixes (map (fn (b, mx) => (b, NONE, mx)) params) |> snd |>
   1.172 -      ProofContext.add_fixes fors |> snd;
   1.173 +    val (expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
   1.174 +    val ctxt = context |> ProofContext.add_fixes fixed |> snd;
   1.175    in
   1.176      case expr of
   1.177          Expr [] => let
   1.178 @@ -547,7 +546,7 @@
   1.179  in
   1.180  
   1.181  fun read_context imprt body ctxt =
   1.182 -  #1 (prep_context_statement intern_expr read_elems true imprt body [] ctxt);
   1.183 +  #1 (prep_context_statement intern read_elems true imprt body [] ctxt);
   1.184  fun cert_context imprt body ctxt =
   1.185    #1 (prep_context_statement (K I) cert_elems true imprt body [] ctxt);
   1.186