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 -fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map (Logic.mk_type #> rpair [])) fixes
1.149 - | extract_elem (Constrains csts) = map (#2 #> single #> map (Logic.mk_type #> rpair [])) csts
1.150 - | extract_elem (Assumes asms) = map #2 asms
1.151 - | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [(t, ps)]) defs
1.152 +local
1.153 +
1.154 +fun mk_type T = (Logic.mk_type T, []);
1.155 +fun mk_term t = (t, []);
1.156 +fun mk_propp (p, pats) = (Syntax.type_constraint propT p, pats);
1.157 +
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