src/Pure/Isar/expression.ML
changeset 28885 6f6bf52e75bb
parent 28879 db2816a37a34
child 28895 4e2914c2f8c5
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Nov 24 21:09:31 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Nov 25 18:06:21 2008 +0100
     1.3 @@ -7,13 +7,10 @@
     1.4  
     1.5  signature EXPRESSION =
     1.6  sig
     1.7 -  type 'term map
     1.8 -  type 'morph expr
     1.9 -
    1.10 -  val empty_expr: 'morph expr
    1.11 -
    1.12 -  type expression = (string * string map) expr * (Name.binding * string option * mixfix) list
    1.13 -(*  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list *)
    1.14 +  datatype 'term map = Positional of 'term option list | Named of (string * 'term) list;
    1.15 +  type 'term expr = (string * (string * 'term map)) list;
    1.16 +  type expression = string expr * (Name.binding * string option * mixfix) list;
    1.17 +  type expression_i = term expr * (Name.binding * typ option * mixfix) list;
    1.18  
    1.19    (* Processing of locale statements *)
    1.20    val read_statement: Element.context list -> (string * string list) list list ->
    1.21 @@ -24,16 +21,15 @@
    1.22    (* Declaring locales *)
    1.23    val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
    1.24      string * Proof.context
    1.25 -(*
    1.26    val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    1.27      string * Proof.context
    1.28 -*)
    1.29 +
    1.30    (* Debugging and development *)
    1.31    val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    1.32  end;
    1.33  
    1.34  
    1.35 -structure Expression (*: EXPRESSION *) =
    1.36 +structure Expression : EXPRESSION =
    1.37  struct
    1.38  
    1.39  datatype ctxt = datatype Element.ctxt;
    1.40 @@ -45,11 +41,10 @@
    1.41    Positional of 'term option list |
    1.42    Named of (string * 'term) list;
    1.43  
    1.44 -datatype 'morph expr = Expr of (string * 'morph) list;
    1.45 +type 'term expr = (string * (string * 'term map)) list;
    1.46  
    1.47 -type expression = (string * string map) expr * (Name.binding * string option * mixfix) list;
    1.48 -
    1.49 -val empty_expr = Expr [];
    1.50 +type expression = string expr * (Name.binding * string option * mixfix) list;
    1.51 +type expression_i = term expr * (Name.binding * typ option * mixfix) list;
    1.52  
    1.53  
    1.54  (** Parsing and printing **)
    1.55 @@ -76,12 +71,12 @@
    1.56      fun expr2 x = P.xname x;
    1.57      fun expr1 x = (Scan.optional prefix "" -- expr2 --
    1.58        Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    1.59 -    fun expr0 x = (plus1_unless loc_keyword expr1 >> Expr) x;
    1.60 +    fun expr0 x = (plus1_unless loc_keyword expr1) x;
    1.61    in expr0 -- P.for_fixes end;
    1.62  
    1.63  end;
    1.64  
    1.65 -fun pretty_expr thy (Expr expr) =
    1.66 +fun pretty_expr thy expr =
    1.67    let
    1.68      fun pretty_pos NONE = Pretty.str "_"
    1.69        | pretty_pos (SOME x) = Pretty.str x;
    1.70 @@ -99,19 +94,19 @@
    1.71              Pretty.brk 1 :: pretty_ren ren);
    1.72    in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
    1.73  
    1.74 -fun err_in_expr thy msg (Expr expr) =
    1.75 +fun err_in_expr thy msg expr =
    1.76    let
    1.77      val err_msg =
    1.78        if null expr then msg
    1.79        else msg ^ "\n" ^ Pretty.string_of (Pretty.block
    1.80          [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
    1.81 -          pretty_expr thy (Expr expr)])
    1.82 +          pretty_expr thy expr])
    1.83    in error err_msg end;
    1.84  
    1.85  
    1.86  (** Internalise locale names in expr **)
    1.87  
    1.88 -fun intern thy (Expr instances) = Expr (map (apfst (NewLocale.intern thy)) instances);
    1.89 +fun intern thy instances =  map (apfst (NewLocale.intern thy)) instances;
    1.90  
    1.91  
    1.92  (** Parameters of expression.
    1.93 @@ -142,9 +137,7 @@
    1.94  	      else insts @ replicate d NONE;
    1.95              val ps' = (ps ~~ insts') |>
    1.96                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    1.97 -          in
    1.98 -            (ps', (loc', (prfx, Positional insts')))
    1.99 -          end
   1.100 +          in (ps', (loc', (prfx, Positional insts'))) end
   1.101        | params_inst (expr as (loc, (prfx, Named insts))) =
   1.102            let
   1.103              val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
   1.104 @@ -154,10 +147,8 @@
   1.105              val ps' = fold (fn (p, _) => fn ps =>
   1.106                if AList.defined match_bind ps p then AList.delete match_bind p ps
   1.107                else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
   1.108 -          in
   1.109 -            (ps', (loc', (prfx, Named insts)))
   1.110 -          end;
   1.111 -    fun params_expr (Expr is) =
   1.112 +          in (ps', (loc', (prfx, Named insts))) end;
   1.113 +    fun params_expr is =
   1.114            let
   1.115              val (is', ps') = fold_map (fn i => fn ps =>
   1.116                let
   1.117 @@ -169,9 +160,7 @@
   1.118                    else error ("Conflicting syntax for parameter" ^ quote (Name.display p) ^
   1.119                      " in expression.")) (ps, ps')
   1.120                in (i', ps'') end) is []
   1.121 -          in
   1.122 -            (ps', Expr is')
   1.123 -          end;
   1.124 +          in (ps', is') end;
   1.125  
   1.126      val (parms, expr') = params_expr expr;
   1.127  
   1.128 @@ -205,12 +194,6 @@
   1.129  
   1.130  end;
   1.131  
   1.132 -(* Prepare type inference problem for Syntax.check_terms *)
   1.133 -
   1.134 -fun varify_indexT i ty = ty |> Term.map_atyps
   1.135 -  (fn TFree (a, S) => TVar ((a, i), S)
   1.136 -    | TVar (ai, _) => raise TYPE ("Illegal schematic variable: " ^
   1.137 -        quote (Term.string_of_vname ai), [ty], []));
   1.138  
   1.139  (* Instantiation morphism *)
   1.140  
   1.141 @@ -252,37 +235,71 @@
   1.142      (prep_term ctxt, map (prep_term ctxt) ps)) concl;
   1.143  
   1.144  
   1.145 -(** Type checking **)
   1.146 +(** Simultaneous type inference: instantiations + elements + conclusion **)
   1.147 +
   1.148 +local
   1.149 +
   1.150 +fun mk_type T = (Logic.mk_type T, []);
   1.151 +fun mk_term t = (t, []);
   1.152 +fun mk_propp (p, pats) = (Syntax.type_constraint propT p, pats);
   1.153  
   1.154 -fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map (Logic.mk_type #> rpair [])) fixes
   1.155 -  | extract_elem (Constrains csts) = map (#2 #> single #> map (Logic.mk_type #> rpair [])) csts
   1.156 -  | extract_elem (Assumes asms) = map #2 asms
   1.157 -  | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [(t, ps)]) defs
   1.158 +fun dest_type (T, []) = Logic.dest_type T;
   1.159 +fun dest_term (t, []) = t;
   1.160 +fun dest_propp (p, pats) = (p, pats);
   1.161 +
   1.162 +fun extract_inst (_, (_, ts)) = map mk_term ts;
   1.163 +fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs));
   1.164 +
   1.165 +fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes
   1.166 +  | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts
   1.167 +  | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms
   1.168 +  | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs
   1.169    | extract_elem (Notes _) = [];
   1.170  
   1.171 -fun restore_elem (Fixes fixes, propps) =
   1.172 -      (fixes ~~ propps) |> map (fn ((x, _, mx), propp) =>
   1.173 -        (x, propp |> map (fst #> Logic.dest_type) |> try hd, mx)) |> Fixes
   1.174 -  | restore_elem (Constrains csts, propps) =
   1.175 -      (csts ~~ propps) |> map (fn ((x, _), propp) =>
   1.176 -        (x, propp |> map (fst #> Logic.dest_type) |> hd)) |> Constrains
   1.177 -  | restore_elem (Assumes asms, propps) =
   1.178 -      (asms ~~ propps) |> map (fn ((b, _), propp) => (b, propp)) |> Assumes
   1.179 -  | restore_elem (Defines defs, propps) =
   1.180 -      (defs ~~ propps) |> map (fn ((b, _), [propp]) => (b, propp)) |> Defines
   1.181 +fun restore_elem (Fixes fixes, css) =
   1.182 +      (fixes ~~ css) |> map (fn ((x, _, mx), cs) =>
   1.183 +        (x, cs |> map dest_type |> try hd, mx)) |> Fixes
   1.184 +  | restore_elem (Constrains csts, css) =
   1.185 +      (csts ~~ css) |> map (fn ((x, _), cs) =>
   1.186 +        (x, cs |> map dest_type |> hd)) |> Constrains
   1.187 +  | restore_elem (Assumes asms, css) =
   1.188 +      (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes
   1.189 +  | restore_elem (Defines defs, css) =
   1.190 +      (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
   1.191    | restore_elem (Notes notes, _) = Notes notes;
   1.192  
   1.193 +fun check cs context =
   1.194 +  let
   1.195 +    fun prep (_, pats) (ctxt, t :: ts) =
   1.196 +      let val ctxt' = Variable.auto_fixes t ctxt
   1.197 +      in
   1.198 +        ((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
   1.199 +          (ctxt', ts))
   1.200 +      end
   1.201 +    val (cs', (context', _)) = fold_map prep cs
   1.202 +      (context, Syntax.check_terms
   1.203 +        (ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
   1.204 +  in (cs', context') end;
   1.205 +
   1.206 +in
   1.207 +
   1.208  fun check_autofix insts elems concl ctxt =
   1.209    let
   1.210 -    val instss = map (snd o snd) insts |> (map o map) (fn t => (t, []));
   1.211 -    val elemss = elems |> map extract_elem;
   1.212 -    val all_terms' = (burrow o burrow_fst) (Syntax.check_terms ctxt) (concl @ instss @ flat elemss); 
   1.213 -(*    val (ctxt', all_props') = ProofContext.check_propp_schematic (ctxt, concl @ flat propss); *)
   1.214 -    val ctxt'' = (fold o fold) (fn (t, _) => Variable.auto_fixes t) all_terms' ctxt;
   1.215 -    val (concl', mores') = chop (length concl) all_terms';
   1.216 -    val (insts', elems') = chop (length instss) mores';
   1.217 -  in (insts' |> (map o map) fst |> curry (op ~~) insts |> map (fn ((l, (p, _)), is) => (l, (p, is))),
   1.218 -    elems' |> unflat elemss |> curry (op ~~) elems |> map restore_elem, concl', ctxt'') end;
   1.219 +    val inst_cs = map extract_inst insts;
   1.220 +    val elem_css = map extract_elem elems;
   1.221 +    val concl_cs = (map o map) mk_propp concl;
   1.222 +    (* Type inference *)
   1.223 +    val (inst_cs' :: css', ctxt') =
   1.224 +      (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
   1.225 +    (* Re-check to resolve bindings, elements and conclusion only *)
   1.226 +    val (css'', _) = (fold_burrow o fold_burrow) check css' ctxt';
   1.227 +    val (elem_css'', [concl_cs'']) = chop (length elem_css) css'';
   1.228 +  in
   1.229 +    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css''),
   1.230 +      concl_cs'', ctxt')
   1.231 +  end;
   1.232 +
   1.233 +end;
   1.234  
   1.235  
   1.236  (** Prepare locale elements **)
   1.237 @@ -412,7 +429,8 @@
   1.238          val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   1.239            map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   1.240          val inst' = parse_inst parm_names inst ctxt;
   1.241 -        val parm_types' = map (TypeInfer.paramify_vars o varify_indexT i) parm_types;
   1.242 +        val parm_types' = map (TypeInfer.paramify_vars o
   1.243 +          Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
   1.244          val inst'' = map2 TypeInfer.constrain parm_types' inst';
   1.245          val insts' = insts @ [(loc, (prfx, inst''))];
   1.246          val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt;
   1.247 @@ -491,7 +509,7 @@
   1.248    let
   1.249      val thy = ProofContext.theory_of context;
   1.250  
   1.251 -    val (Expr expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
   1.252 +    val (expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
   1.253      val ((parms, fors, deps, elems, concl), (spec, (_, _, defs))) =
   1.254        prep_elems do_close context fixed expr elements raw_concl;
   1.255  
   1.256 @@ -504,7 +522,7 @@
   1.257  
   1.258  fun prep_statement prep_ctxt elems concl ctxt =
   1.259    let
   1.260 -    val (((_, (ctxt', _), _)), concl) = prep_ctxt false (Expr [], []) elems concl ctxt
   1.261 +    val (((_, (ctxt', _), _)), concl) = prep_ctxt false ([], []) elems concl ctxt
   1.262    in (concl, ctxt') end;
   1.263  
   1.264  in
   1.265 @@ -708,7 +726,7 @@
   1.266  in
   1.267  
   1.268  val add_locale = gen_add_locale read_context;
   1.269 -(* val add_locale_i = gen_add_locale cert_context; *)
   1.270 +val add_locale_i = gen_add_locale cert_context;
   1.271  
   1.272  end;
   1.273