--- a/src/Pure/Isar/expression.ML Thu Jan 15 14:52:35 2009 +0100
+++ b/src/Pure/Isar/expression.ML Fri Jan 16 08:04:38 2009 +0100
@@ -6,37 +6,47 @@
signature EXPRESSION =
sig
- datatype 'term map = Positional of 'term option list | Named of (string * 'term) list;
- type 'term expr = (string * ((string * bool) * 'term map)) list;
- type expression_i = term expr * (Binding.T * typ option * mixfix) list;
- type expression = string expr * (Binding.T * string option * mixfix) list;
+ (* Locale expressions *)
+ datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
+ type 'term expr = (string * ((string * bool) * 'term map)) list
+ type expression_i = term expr * (Binding.T * typ option * mixfix) list
+ type expression = string expr * (Binding.T * string option * mixfix) list
(* Processing of context statements *)
val cert_statement: Element.context_i list -> (term * term list) list list ->
- Proof.context -> (term * term list) list list * Proof.context;
+ Proof.context -> (term * term list) list list * Proof.context
val read_statement: Element.context list -> (string * string list) list list ->
- Proof.context -> (term * term list) list list * Proof.context;
+ Proof.context -> (term * term list) list list * Proof.context
(* Declaring locales *)
+ val cert_declaration: expression_i -> Element.context_i list -> Proof.context ->
+ ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ * Element.context_i list) * ((string * typ) list * Proof.context)
+ val cert_read_declaration: expression_i -> Element.context list -> Proof.context ->
+ ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ * Element.context_i list) * ((string * typ) list * Proof.context)
+ (*FIXME*)
+ val read_declaration: expression -> Element.context list -> Proof.context ->
+ ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ * Element.context_i list) * ((string * typ) list * Proof.context)
val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
- theory -> string * local_theory;
+ theory -> string * local_theory
val add_locale_cmd: bstring -> bstring -> expression -> Element.context list ->
- theory -> string * local_theory;
+ theory -> string * local_theory
(* Interpretation *)
val cert_goal_expression: expression_i -> Proof.context ->
- (term list list * (string * morphism) list * morphism) * Proof.context;
+ (term list list * (string * morphism) list * morphism) * Proof.context
val read_goal_expression: expression -> Proof.context ->
- (term list list * (string * morphism) list * morphism) * Proof.context;
-
- val sublocale: string -> expression_i -> theory -> Proof.state;
- val sublocale_cmd: string -> expression -> theory -> Proof.state;
+ (term list list * (string * morphism) list * morphism) * Proof.context
+ val sublocale: string -> expression_i -> theory -> Proof.state
+ val sublocale_cmd: string -> expression -> theory -> Proof.state
val interpretation: expression_i -> (Attrib.binding * term) list ->
- theory -> Proof.state;
+ theory -> Proof.state
val interpretation_cmd: expression -> (Attrib.binding * string) list ->
- theory -> Proof.state;
- val interpret: expression_i -> bool -> Proof.state -> Proof.state;
- val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
+ theory -> Proof.state
+ val interpret: expression_i -> bool -> Proof.state -> Proof.state
+ val interpret_cmd: expression -> bool -> Proof.state -> Proof.state
end;
@@ -337,7 +347,7 @@
local
-fun prep_full_context_statement parse_typ parse_prop parse_inst prep_vars prep_expr
+fun prep_full_context_statement parse_typ parse_prop prep_vars_elem parse_inst prep_vars_inst prep_expr
strict do_close raw_import raw_elems raw_concl ctxt1 =
let
val thy = ProofContext.theory_of ctxt1;
@@ -359,43 +369,47 @@
val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
in (i+1, insts', ctxt'') end;
- fun prep_elem raw_elem (insts, elems, ctxt) =
+ fun prep_elem insts raw_elem (elems, ctxt) =
let
- val ctxt' = declare_elem prep_vars raw_elem ctxt;
+ val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
- in (insts, elems', ctxt') end;
+ in (elems', ctxt') end;
fun prep_concl raw_concl (insts, elems, ctxt) =
let
val concl = parse_concl parse_prop ctxt raw_concl;
in check_autofix insts elems concl ctxt end;
- val fors = prep_vars fixed ctxt1 |> fst;
+ val fors = prep_vars_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
val (_, insts', ctxt3) = fold prep_inst raw_insts (0, [], ctxt2);
- val (_, elems'', ctxt4) = fold prep_elem raw_elems (insts', [], ctxt3);
- val (insts, elems, concl, ctxt5) =
- prep_concl raw_concl (insts', elems'', ctxt4);
+ val (elems, ctxt4) = fold (prep_elem insts') raw_elems ([], ctxt3);
+ val (insts, elems', concl, ctxt5) =
+ prep_concl raw_concl (insts', elems, ctxt4);
(* Retrieve parameter types *)
- val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes) |
- _ => fn ps => ps) (Fixes fors :: elems) [];
+ val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes)
+ | _ => fn ps => ps) (Fixes fors :: elems') [];
val (Ts, ctxt6) = fold_map ProofContext.inferred_param xs ctxt5;
val parms = xs ~~ Ts; (* params from expression and elements *)
val Fixes fors' = finish_primitive parms I (Fixes fors);
- val (deps, elems') = finish ctxt6 parms do_close insts elems;
+ val (deps, elems'') = finish ctxt6 parms do_close insts elems';
- in ((fors', deps, elems', concl), (parms, ctxt6)) end
+ in ((fors', deps, elems'', concl), (parms, ctxt6)) end
in
+fun cert_full_context_statement x =
+ prep_full_context_statement (K I) (K I) ProofContext.cert_vars
+ make_inst ProofContext.cert_vars (K I) x;
+fun cert_read_full_context_statement x =
+ prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
+ make_inst ProofContext.cert_vars (K I) x;
fun read_full_context_statement x =
- prep_full_context_statement Syntax.parse_typ Syntax.parse_prop parse_inst
- ProofContext.read_vars intern x;
-fun cert_full_context_statement x =
- prep_full_context_statement (K I) (K I) make_inst ProofContext.cert_vars (K I) x;
+ prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
+ parse_inst ProofContext.read_vars intern x;
end;
@@ -407,14 +421,16 @@
fun prep_statement prep activate raw_elems raw_concl context =
let
val ((_, _, elems, concl), _) =
- prep true false ([], []) raw_elems raw_concl context ;
- val (_, context') = activate elems (ProofContext.set_stmt true context);
+ prep true false ([], []) raw_elems raw_concl context;
+ val (_, context') = context |>
+ ProofContext.set_stmt true |>
+ activate elems;
in (concl, context') end;
in
+fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
fun read_statement x = prep_statement read_full_context_statement Element.activate x;
-fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
end;
@@ -431,13 +447,16 @@
val context' = context |>
ProofContext.add_fixes_i fixed |> snd |>
fold Locale.activate_local_facts deps;
- val (elems', _) = activate elems (ProofContext.set_stmt true context');
+ val (elems', _) = context' |>
+ ProofContext.set_stmt true |>
+ activate elems;
in ((fixed, deps, elems'), (parms, ctxt')) end;
in
+fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;
+fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x;
fun read_declaration x = prep_declaration read_full_context_statement Element.activate x;
-fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;
end;
@@ -476,8 +495,8 @@
in
+fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
fun read_goal_expression x = prep_goal_expression read_full_context_statement x;
-fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
end;
@@ -758,8 +777,8 @@
in
+val add_locale = gen_add_locale cert_declaration;
val add_locale_cmd = gen_add_locale read_declaration;
-val add_locale = gen_add_locale cert_declaration;
end;
@@ -804,8 +823,8 @@
in
+fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
-fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
end;
@@ -873,9 +892,9 @@
in
+fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
fun interpretation_cmd x = gen_interpretation read_goal_expression
Syntax.parse_prop Attrib.intern_src x;
-fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
end;
@@ -910,8 +929,8 @@
in
+fun interpret x = gen_interpret cert_goal_expression x;
fun interpret_cmd x = gen_interpret read_goal_expression x;
-fun interpret x = gen_interpret cert_goal_expression x;
end;