--- a/NEWS Tue Mar 22 20:06:10 2011 +0100
+++ b/NEWS Tue Mar 22 21:22:50 2011 +0100
@@ -71,6 +71,16 @@
* Path.print is the official way to show file-system paths to users
(including quotes etc.).
+* Inner syntax: identifiers in parse trees of generic categories
+"logic", "aprop", "idt" etc. carry position information (disguised as
+type constraints). Occasional INCOMPATIBILITY with non-compliant
+translations that choke on unexpected type constraints. Positions can
+be stripped in ML translations via Syntax.strip_positions /
+Syntax.strip_positions_ast, or via the syntax constant
+"_strip_positions" within parse trees. As last resort, positions can
+be disabled via the configuration option Syntax.positions, which is
+called "syntax_positions" in Isar attribute syntax.
+
New in Isabelle2011 (January 2011)
--- a/src/CCL/Term.thy Tue Mar 22 20:06:10 2011 +0100
+++ b/src/CCL/Term.thy Tue Mar 22 21:22:50 2011 +0100
@@ -40,16 +40,16 @@
letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
syntax
- "_let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)"
+ "_let" :: "[id,i,i]=>i" ("(3let _ be _/ in _)"
[0,0,60] 60)
- "_letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)"
+ "_letrec" :: "[id,id,i,i]=>i" ("(3letrec _ _ be _/ in _)"
[0,0,0,60] 60)
- "_letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)"
+ "_letrec2" :: "[id,id,id,i,i]=>i" ("(3letrec _ _ _ be _/ in _)"
[0,0,0,0,60] 60)
- "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
+ "_letrec3" :: "[id,id,id,id,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
[0,0,0,0,0,60] 60)
ML {*
--- a/src/HOL/HOL.thy Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/HOL.thy Tue Mar 22 21:22:50 2011 +0100
@@ -106,7 +106,7 @@
iff (infixr "\<longleftrightarrow>" 25)
nonterminal letbinds and letbind
-nonterminal case_syn and cases_syn
+nonterminal case_pat and case_syn and cases_syn
syntax
"_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10)
@@ -116,10 +116,14 @@
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10)
- "_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
- "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
- "" :: "case_syn => cases_syn" ("_")
- "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
+ "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
+ "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ =>/ _)" 10)
+ "" :: "case_syn => cases_syn" ("_")
+ "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
+ "_strip_positions" :: "'a => case_pat" ("_")
+
+syntax (xsymbols)
+ "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
translations
"THE x. P" == "CONST The (%x. P)"
@@ -130,9 +134,6 @@
in Syntax.const @{syntax_const "_The"} $ x $ t end)]
*} -- {* To avoid eta-contraction of body *}
-syntax (xsymbols)
- "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
-
notation (xsymbols)
All (binder "\<forall>" 10) and
Ex (binder "\<exists>" 10) and
--- a/src/HOL/HOLCF/Cfun.thy Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Tue Mar 22 21:22:50 2011 +0100
@@ -57,7 +57,7 @@
let
fun Lambda_ast_tr [pats, body] =
Syntax.fold_ast_p @{syntax_const "_cabs"}
- (Syntax.unfold_ast @{syntax_const "_cargs"} pats, body)
+ (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
| Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
*}
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Mar 22 21:22:50 2011 +0100
@@ -458,7 +458,7 @@
fun con1 authentic n (con,args) =
Library.foldl capp (c_ast authentic con, argvars n args)
fun case1 authentic (n, c) =
- app "_case1" (con1 authentic n c, expvar n)
+ app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
fun when1 n (m, c) =
if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Mar 22 21:22:50 2011 +0100
@@ -100,16 +100,17 @@
subsection {* Case syntax *}
-nonterminal Case_syn and Cases_syn
+nonterminal Case_pat and Case_syn and Cases_syn
syntax
"_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10)
- "_Case1" :: "['a, 'b] => Case_syn" ("(2_ =>/ _)" 10)
+ "_Case1" :: "[Case_pat, 'b] => Case_syn" ("(2_ =>/ _)" 10)
"" :: "Case_syn => Cases_syn" ("_")
"_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" ("_/ | _")
+ "_strip_positions" :: "'a => Case_pat" ("_")
syntax (xsymbols)
- "_Case1" :: "['a, 'b] => Case_syn" ("(2_ \<Rightarrow>/ _)" 10)
+ "_Case1" :: "[Case_pat, 'b] => Case_syn" ("(2_ \<Rightarrow>/ _)" 10)
translations
"_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"
--- a/src/HOL/Hoare/Hoare_Logic.thy Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Mar 22 21:22:50 2011 +0100
@@ -89,8 +89,10 @@
*}
(* com_tr *)
ML{*
-fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
- Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+fun com_tr (t as (Const(@{syntax_const "_assign"},_) $ x $ e)) xs =
+ (case Syntax.strip_positions x of
+ Free (a, _) => Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+ | _ => t)
| com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
| com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
@@ -105,11 +107,12 @@
ML{*
local
-fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
- | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T);
+fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
+ | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
-fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
- | vars_tr t = [var_tr t]
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) =
+ var_tr (Syntax.strip_positions idt) :: vars_tr vars
+ | vars_tr t = [var_tr (Syntax.strip_positions t)]
in
fun hoare_vars_tr [vars, pre, prg, post] =
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Mar 22 21:22:50 2011 +0100
@@ -91,8 +91,10 @@
*}
(* com_tr *)
ML{*
-fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
- Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+fun com_tr (t as (Const (@{syntax_const "_assign"},_) $ x $ e)) xs =
+ (case Syntax.strip_positions x of
+ Free (a, _) => Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+ | _ => t)
| com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
| com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
@@ -103,15 +105,16 @@
| com_tr t _ = t (* if t is just a Free/Var *)
*}
-(* triple_tr *) (* FIXME does not handle "_idtdummy" *)
+(* triple_tr *) (* FIXME does not handle "_idtdummy" *)
ML{*
local
fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
| var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
-fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
- | vars_tr t = [var_tr t]
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) =
+ var_tr (Syntax.strip_positions idt) :: vars_tr vars
+ | vars_tr t = [var_tr (Syntax.strip_positions t)]
in
fun hoare_vars_tr [vars, pre, prg, post] =
--- a/src/HOL/Isar_Examples/Hoare.thy Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Tue Mar 22 21:22:50 2011 +0100
@@ -302,7 +302,7 @@
then show ?thesis by simp
qed
-lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
+lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
by (rule basic)
text {* Note that above formulation of assignment corresponds to our
--- a/src/HOL/List.thy Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/List.thy Tue Mar 22 21:22:50 2011 +0100
@@ -384,7 +384,7 @@
let
val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
val e = if opti then singl e else e;
- val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
+ val case1 = Syntax.const @{syntax_const "_case1"} $ Syntax.strip_positions p $ e;
val case2 =
Syntax.const @{syntax_const "_case1"} $
Syntax.const @{const_syntax dummy_pattern} $ NilC;
--- a/src/HOL/Statespace/state_space.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/Statespace/state_space.ML Tue Mar 22 21:22:50 2011 +0100
@@ -623,7 +623,11 @@
then Syntax.const "StateFun.lookup" $ Syntax.const "undefined" $ Syntax.free n $ s
else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
-fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n;
+fun lookup_tr ctxt [s, x] =
+ (case Syntax.strip_positions x of
+ Free (n,_) => gen_lookup_tr ctxt s n
+ | _ => raise Match);
+
fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n;
fun lookup_tr' ctxt [_$Free (prj,_),n as (_$Free (name,_)),s] =
@@ -651,7 +655,10 @@
else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[]))
end;
-fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
+fun update_tr ctxt [s, x, v] =
+ (case Syntax.strip_positions x of
+ Free (n, _) => gen_update_tr false ctxt n v s
+ | _ => raise Match);
fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
if Long_Name.base_name k = Long_Name.base_name KN then
--- a/src/HOL/Tools/Datatype/datatype_case.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Tue Mar 22 21:22:50 2011 +0100
@@ -37,7 +37,7 @@
*---------------------------------------------------------------------------*)
fun ty_info tab sT =
- case tab sT of
+ (case tab sT of
SOME ({descr, case_name, index, sorts, ...} : info) =>
let
val (_, (tname, dts, constrs)) = nth descr index;
@@ -48,7 +48,7 @@
constructors = map (fn (cname, dts') =>
Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
end
- | NONE => NONE;
+ | NONE => NONE);
(*---------------------------------------------------------------------------
@@ -93,8 +93,7 @@
raise CASE_ERROR ("type mismatch", ~1)
val c' = ty_inst ty_theta c
val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)
- in (c', gvars)
- end;
+ in (c', gvars) end;
(*---------------------------------------------------------------------------
@@ -102,21 +101,22 @@
* pattern with constructor = name.
*---------------------------------------------------------------------------*)
fun mk_group (name, T) rows =
- let val k = length (binder_types T)
- in fold (fn (row as ((prfx, p :: rst), rhs as (_, (i, _)))) =>
- fn ((in_group, not_in_group), (names, cnstrts)) => (case strip_comb p of
- (Const (name', _), args) =>
- if name = name' then
- if length args = k then
- let val (args', cnstrts') = split_list (map strip_constraints args)
- in
- ((((prfx, args' @ rst), rhs) :: in_group, not_in_group),
- (default_names names args', map2 append cnstrts cnstrts'))
- end
- else raise CASE_ERROR
- ("Wrong number of arguments for constructor " ^ name, i)
- else ((in_group, row :: not_in_group), (names, cnstrts))
- | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
+ let val k = length (binder_types T) in
+ fold (fn (row as ((prfx, p :: rst), rhs as (_, (i, _)))) =>
+ fn ((in_group, not_in_group), (names, cnstrts)) =>
+ (case strip_comb p of
+ (Const (name', _), args) =>
+ if name = name' then
+ if length args = k then
+ let val (args', cnstrts') = split_list (map strip_constraints args)
+ in
+ ((((prfx, args' @ rst), rhs) :: in_group, not_in_group),
+ (default_names names args', map2 append cnstrts cnstrts'))
+ end
+ else raise CASE_ERROR
+ ("Wrong number of arguments for constructor " ^ name, i)
+ else ((in_group, row :: not_in_group), (names, cnstrts))
+ | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
end;
@@ -158,8 +158,7 @@
constraints = cnstrts,
group = in_group'} :: A}
end
- in part {constrs = constructors, rows = rows, A = []}
- end;
+ in part {constrs = constructors, rows = rows, A = []} end;
(*---------------------------------------------------------------------------
* Misc. routines used in mk_case
@@ -210,48 +209,46 @@
| mk {path, rows as ((row as ((_, [Free _]), _)) :: _ :: _)} =
mk {path = path, rows = [row]}
| mk {path = u :: rstp, rows as ((_, _ :: _), _) :: _} =
- let val col0 = map (fn ((_, p :: _), (_, (i, _))) => (p, i)) rows
- in case Option.map (apfst head_of)
- (find_first (not o is_Free o fst) col0) of
+ let val col0 = map (fn ((_, p :: _), (_, (i, _))) => (p, i)) rows in
+ (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
NONE =>
let
val rows' = map (fn ((v, _), row) => row ||>
pattern_subst [(v, u)] |>> v_to_prfx) (col0 ~~ rows);
val (pref_patl, tm) = mk {path = rstp, rows = rows'}
in (map v_to_pats pref_patl, tm) end
- | SOME (Const (cname, cT), i) => (case ty_info tab (cname, cT) of
- NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
- | SOME {case_name, constructors} =>
- let
- val pty = body_type cT;
- val used' = fold Term.add_free_names rstp used;
- val nrows = maps (expand constructors used' pty) rows;
- val subproblems = partition ty_match ty_inst type_of used'
- constructors pty range_ty nrows;
- val constructors' = map #constructor subproblems
- val news = map (fn {new_formals, group, ...} =>
- {path = new_formals @ rstp, rows = group}) subproblems;
- val (pat_rect, dtrees) = split_list (map mk news);
- val case_functions = map2
- (fn {new_formals, names, constraints, ...} =>
- fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
- Abs (if s = "" then name else s, T,
- abstract_over (x, t)) |>
- fold mk_fun_constrain cnstrts)
- (new_formals ~~ names ~~ constraints))
- subproblems dtrees;
- val types = map type_of (case_functions @ [u]);
- val case_const = Const (case_name, types ---> range_ty)
- val tree = list_comb (case_const, case_functions @ [u])
- val pat_rect1 = maps mk_pat (constructors ~~ constructors' ~~ pat_rect)
- in (pat_rect1, tree)
- end)
+ | SOME (Const (cname, cT), i) =>
+ (case ty_info tab (cname, cT) of
+ NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
+ | SOME {case_name, constructors} =>
+ let
+ val pty = body_type cT;
+ val used' = fold Term.add_free_names rstp used;
+ val nrows = maps (expand constructors used' pty) rows;
+ val subproblems = partition ty_match ty_inst type_of used'
+ constructors pty range_ty nrows;
+ val constructors' = map #constructor subproblems
+ val news = map (fn {new_formals, group, ...} =>
+ {path = new_formals @ rstp, rows = group}) subproblems;
+ val (pat_rect, dtrees) = split_list (map mk news);
+ val case_functions = map2
+ (fn {new_formals, names, constraints, ...} =>
+ fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
+ Abs (if s = "" then name else s, T,
+ abstract_over (x, t)) |>
+ fold mk_fun_constrain cnstrts)
+ (new_formals ~~ names ~~ constraints))
+ subproblems dtrees;
+ val types = map type_of (case_functions @ [u]);
+ val case_const = Const (case_name, types ---> range_ty)
+ val tree = list_comb (case_const, case_functions @ [u])
+ val pat_rect1 = maps mk_pat (constructors ~~ constructors' ~~ pat_rect)
+ in (pat_rect1, tree) end)
| SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
- Syntax.string_of_term ctxt t, i)
+ Syntax.string_of_term ctxt t, i))
end
| mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
- in mk
- end;
+ in mk end;
fun case_error s = error ("Error in case expression:\n" ^ s);
@@ -289,12 +286,12 @@
val finals = map row_of_pat patts2
val originals = map (row_of_pat o #2) rows
val _ =
- case subtract (op =) finals originals of
- [] => ()
- | is =>
- (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
- ("The following clauses are redundant (covered by preceding clauses):\n" ^
- cat_lines (map (string_of_clause o nth clauses) is));
+ (case subtract (op =) finals originals of
+ [] => ()
+ | is =>
+ (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
+ ("The following clauses are redundant (covered by preceding clauses):\n" ^
+ cat_lines (map (string_of_clause o nth clauses) is)));
in
(case_tm, patts2)
end;
@@ -308,48 +305,46 @@
(* parse translation *)
fun case_tr err tab_of ctxt [t, u] =
- let
- val thy = ProofContext.theory_of ctxt;
- val intern_const_syntax = Consts.intern_syntax (Sign.consts_of thy);
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val intern_const_syntax = Consts.intern_syntax (Sign.consts_of thy);
- (* replace occurrences of dummy_pattern by distinct variables *)
- (* internalize constant names *)
- fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
- let val (t', used') = prep_pat t used
- in (c $ t' $ tT, used') end
- | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
- let val x = Name.variant used "x"
- in (Free (x, T), x :: used) end
- | prep_pat (Const (s, T)) used =
- (Const (intern_const_syntax s, T), used)
- | prep_pat (v as Free (s, T)) used =
- let val s' = Sign.intern_const thy s
- in
- if Sign.declared_const thy s' then
- (Const (s', T), used)
- else (v, used)
- end
- | prep_pat (t $ u) used =
- let
- val (t', used') = prep_pat t used;
- val (u', used'') = prep_pat u used'
- in
- (t' $ u', used'')
- end
- | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
- fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
- let val (l', cnstrts) = strip_constraints l
- in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts)
- end
- | dest_case1 t = case_error "dest_case1";
- fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
- | dest_case2 t = [t];
- val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
- val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
- (if err then Error else Warning) []
- (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
- (flat cnstrts) t) cases;
- in case_tm end
+ (* replace occurrences of dummy_pattern by distinct variables *)
+ (* internalize constant names *)
+ fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
+ let val (t', used') = prep_pat t used
+ in (c $ t' $ tT, used') end
+ | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
+ let val x = Name.variant used "x"
+ in (Free (x, T), x :: used) end
+ | prep_pat (Const (s, T)) used =
+ (Const (intern_const_syntax s, T), used)
+ | prep_pat (v as Free (s, T)) used =
+ let val s' = Sign.intern_const thy s in
+ if Sign.declared_const thy s' then
+ (Const (s', T), used)
+ else (v, used)
+ end
+ | prep_pat (t $ u) used =
+ let
+ val (t', used') = prep_pat t used;
+ val (u', used'') = prep_pat u used'
+ in
+ (t' $ u', used'')
+ end
+ | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
+ fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
+ let val (l', cnstrts) = strip_constraints l
+ in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts) end
+ | dest_case1 t = case_error "dest_case1";
+ fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
+ | dest_case2 t = [t];
+ val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
+ val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
+ (if err then Error else Warning) []
+ (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
+ (flat cnstrts) t) cases;
+ in case_tm end
| case_tr _ _ _ ts = case_error "case_tr";
@@ -360,7 +355,7 @@
(* destruct one level of pattern matching *)
fun gen_dest_case name_of type_of tab d used t =
- case apfst name_of (strip_comb t) of
+ (case apfst name_of (strip_comb t) of
(SOME cname, ts as _ :: _) =>
let
val (fs, x) = split_last ts;
@@ -375,15 +370,14 @@
in (xs', subst_bounds (rev xs', u)) end;
fun is_dependent i t =
let val k = length (strip_abs_vars t) - i
- in k < 0 orelse exists (fn j => j >= k)
- (loose_bnos (strip_abs_body t))
- end;
+ in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end;
fun count_cases (_, _, true) = I
| count_cases (c, (_, body), false) =
AList.map_default op aconv (body, []) (cons c);
val is_undefined = name_of #> equal (SOME @{const_name undefined});
fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
- in case ty_info tab cname of
+ in
+ (case ty_info tab cname of
SOME {constructors, case_name} =>
if length fs = length constructors then
let
@@ -400,26 +394,28 @@
val R = type_of t;
val dummy =
if d then Const (@{const_name dummy_pattern}, R)
- else Free (Name.variant used "x", R)
+ else Free (Name.variant used "x", R);
in
- SOME (x, map mk_case (case find_first (is_undefined o fst) cases' of
- SOME (_, cs) =>
- if length cs = length constructors then [hd cases]
- else filter_out (fn (_, (_, body), _) => is_undefined body) cases
- | NONE => case cases' of
- [] => cases
- | (default, cs) :: _ =>
- if length cs = 1 then cases
- else if length cs = length constructors then
- [hd cases, (dummy, ([], default), false)]
- else
- filter_out (fn (c, _, _) => member op aconv cs c) cases @
- [(dummy, ([], default), false)]))
+ SOME (x,
+ map mk_case
+ (case find_first (is_undefined o fst) cases' of
+ SOME (_, cs) =>
+ if length cs = length constructors then [hd cases]
+ else filter_out (fn (_, (_, body), _) => is_undefined body) cases
+ | NONE => case cases' of
+ [] => cases
+ | (default, cs) :: _ =>
+ if length cs = 1 then cases
+ else if length cs = length constructors then
+ [hd cases, (dummy, ([], default), false)]
+ else
+ filter_out (fn (c, _, _) => member op aconv cs c) cases @
+ [(dummy, ([], default), false)]))
end handle CASE_ERROR _ => NONE
else NONE
- | _ => NONE
+ | _ => NONE)
end
- | _ => NONE;
+ | _ => NONE);
val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
val dest_case' = gen_dest_case (try (dest_Const #> fst #> Syntax.unmark_const)) (K dummyT);
@@ -428,7 +424,7 @@
(* destruct nested patterns *)
fun strip_case'' dest (pat, rhs) =
- case dest (Term.add_free_names pat []) rhs of
+ (case dest (Term.add_free_names pat []) rhs of
SOME (exp as Free _, clauses) =>
if member op aconv (OldTerm.term_frees pat) exp andalso
not (exists (fn (_, rhs') =>
@@ -437,13 +433,13 @@
maps (strip_case'' dest) (map (fn (pat', rhs') =>
(subst_free [(exp, pat')] pat, rhs')) clauses)
else [(pat, rhs)]
- | _ => [(pat, rhs)];
+ | _ => [(pat, rhs)]);
fun gen_strip_case dest t =
- case dest [] t of
+ (case dest [] t of
SOME (x, clauses) =>
SOME (x, maps (strip_case'' dest) clauses)
- | NONE => NONE;
+ | NONE => NONE);
val strip_case = gen_strip_case oo dest_case;
val strip_case' = gen_strip_case oo dest_case';
@@ -455,8 +451,7 @@
let
val thy = ProofContext.theory_of ctxt;
fun mk_clause (pat, rhs) =
- let val xs = Term.add_frees pat []
- in
+ let val xs = Term.add_frees pat [] in
Syntax.const @{syntax_const "_case1"} $
map_aterms
(fn Free p => Syntax.mark_boundT p
@@ -466,14 +461,14 @@
(fn x as Free (s, T) =>
if member (op =) xs (s, T) then Syntax.mark_bound s else x
| t => t) rhs
- end
+ end;
in
- case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
+ (case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
SOME (x, clauses) =>
Syntax.const @{syntax_const "_case_syntax"} $ x $
foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
(map mk_clause clauses)
- | NONE => raise Match
+ | NONE => raise Match)
end;
end;
--- a/src/Pure/General/timing.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/General/timing.ML Tue Mar 22 21:22:50 2011 +0100
@@ -75,11 +75,9 @@
fun cond_timeit enabled msg e =
if enabled then
let
- val (timing, result) = timing (Exn.capture e) ();
+ val (timing, result) = timing (Exn.interruptible_capture e) ();
val end_msg = message timing;
- val _ =
- if Exn.is_interrupt_exn result then ()
- else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
+ val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
in Exn.release result end
else e ();
--- a/src/Pure/Isar/attrib.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Mar 22 21:22:50 2011 +0100
@@ -400,6 +400,7 @@
val _ = Context.>> (Context.map_theory
(register_config Syntax.ast_trace_raw #>
register_config Syntax.ast_stat_raw #>
+ register_config Syntax.positions_raw #>
register_config Syntax.show_brackets_raw #>
register_config Syntax.show_sorts_raw #>
register_config Syntax.show_types_raw #>
--- a/src/Pure/Isar/proof.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/Isar/proof.ML Tue Mar 22 21:22:50 2011 +0100
@@ -999,7 +999,7 @@
val test_proof =
try (local_skip_proof true)
|> Unsynchronized.setmp testing true
- |> Exn.capture;
+ |> Exn.interruptible_capture;
fun after_qed' results =
refine_goals print_rule (context_of state) (flat results)
@@ -1012,9 +1012,7 @@
(case test_proof goal_state of
Exn.Result (SOME _) => goal_state
| Exn.Result NONE => error (fail_msg (context_of goal_state))
- | Exn.Exn exn =>
- if Exn.is_interrupt exn then reraise exn
- else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
+ | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
end;
in
--- a/src/Pure/ML/ml_syntax.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/ML/ml_syntax.ML Tue Mar 22 21:22:50 2011 +0100
@@ -106,7 +106,7 @@
handle Fail _ => Symbol.explode str;
val body' =
if length body <= max_len then body
- else take max_len body @ ["..."];
+ else take (Int.max (max_len, 0)) body @ ["..."];
in Pretty.str (quote (implode (map print_char body'))) end;
end;
--- a/src/Pure/Syntax/ast.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/Syntax/ast.ML Tue Mar 22 21:22:50 2011 +0100
@@ -17,7 +17,6 @@
sig
include AST0
val mk_appl: ast -> ast list -> ast
- val str_of_ast: ast -> string
val pretty_ast: ast -> Pretty.T
val pretty_rule: ast * ast -> Pretty.T
val fold_ast: string -> ast list -> ast
@@ -70,12 +69,11 @@
(** print asts in a LISP-like style **)
-fun str_of_ast (Constant a) = quote a
- | str_of_ast (Variable x) = x
- | str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";
-
fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
- | pretty_ast (Variable x) = Pretty.str x
+ | pretty_ast (Variable x) =
+ (case Lexicon.decode_position x of
+ SOME pos => Lexicon.pretty_position pos
+ | NONE => Pretty.str x)
| pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
fun pretty_rule (lhs, rhs) =
@@ -175,6 +173,9 @@
val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
val ast_stat = Config.bool ast_stat_raw;
+fun message head body =
+ Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
+
(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
fun normalize ctxt get_rules pre_ast =
let
@@ -209,8 +210,7 @@
| rewrite ast = try_headless_rules ast;
fun rewrote old_ast new_ast =
- if trace then
- tracing ("rewrote: " ^ str_of_ast old_ast ^ " -> " ^ str_of_ast new_ast)
+ if trace then tracing (message "rewrote:" (pretty_rule (old_ast, new_ast)))
else ();
fun norm_root ast =
@@ -239,11 +239,11 @@
end;
- val _ = if trace then tracing ("pre: " ^ str_of_ast pre_ast) else ();
+ val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else ();
val post_ast = normal pre_ast;
val _ =
if trace orelse stat then
- tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
+ tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^
string_of_int (! passes) ^ " passes, " ^
string_of_int (! changes) ^ " changes, " ^
string_of_int (! failed_matches) ^ " matches failed")
--- a/src/Pure/Syntax/lexicon.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/Syntax/lexicon.ML Tue Mar 22 21:22:50 2011 +0100
@@ -42,6 +42,11 @@
case_fixed: string -> 'a,
case_default: string -> 'a} -> string -> 'a
val is_marked: string -> bool
+ val dummy_type: term
+ val fun_type: term
+ val pretty_position: Position.T -> Pretty.T
+ val encode_position: Position.T -> string
+ val decode_position: string -> Position.T option
end;
signature LEXICON =
@@ -377,6 +382,9 @@
unmark {case_class = K true, case_type = K true, case_const = K true,
case_fixed = K true, case_default = K false};
+val dummy_type = const (mark_type "dummy");
+val fun_type = const (mark_type "fun");
+
(* read numbers *)
@@ -449,6 +457,26 @@
in
{mant = sign * #1 (Library.read_int (intpart @ fracpart)),
exp = length fracpart}
- end
+ end;
+
+
+(* positions *)
+
+val position_dummy = "<position>";
+val position_text = XML.Text position_dummy;
+
+fun pretty_position pos =
+ Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
+
+fun encode_position pos =
+ YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
+
+fun decode_position str =
+ (case YXML.parse_body str handle Fail msg => error msg of
+ [XML.Elem ((name, props), [arg])] =>
+ if name = Markup.positionN andalso arg = position_text
+ then SOME (Position.of_properties props)
+ else NONE
+ | _ => NONE);
end;
--- a/src/Pure/Syntax/printer.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/Syntax/printer.ML Tue Mar 22 21:22:50 2011 +0100
@@ -415,7 +415,7 @@
| tokentrT _ _ = NONE
and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
- | astT (Ast.Variable x, _) = [Pretty.str x]
+ | astT (ast as Ast.Variable x, _) = [Ast.pretty_ast ast]
| astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
| astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
| astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
--- a/src/Pure/Syntax/syn_trans.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Tue Mar 22 21:22:50 2011 +0100
@@ -55,11 +55,10 @@
val prop_tr': term -> term
val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
- val pts_to_asts: Proof.context ->
- (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
- Parser.parsetree list -> Ast.ast list
- val asts_to_terms: Proof.context ->
- (string -> (Proof.context -> term list -> term) option) -> Ast.ast list -> term list
+ val parsetree_to_ast: Proof.context -> bool ->
+ (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
+ val ast_to_term: Proof.context ->
+ (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
end;
structure Syn_Trans: SYN_TRANS =
@@ -68,6 +67,12 @@
(** parse (ast) translations **)
+(* strip_positions *)
+
+fun strip_positions_ast_tr [ast] = Type_Ext.strip_positions_ast ast
+ | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
+
+
(* constify *)
fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
@@ -99,33 +104,26 @@
val constrainAbsC = "_constrainAbs";
fun absfree_proper (x, T, t) =
- if can Name.dest_internal x then error ("Illegal internal variable in abstraction: " ^ quote x)
+ if can Name.dest_internal x
+ then error ("Illegal internal variable in abstraction: " ^ quote x)
else Term.absfree (x, T, t);
-fun abs_tr (*"_abs"*) [Free (x, T), t] = absfree_proper (x, T, t)
- | abs_tr (*"_abs"*) [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
- | abs_tr (*"_abs"*) [Const ("_constrain", _) $ Free (x, T) $ tT, t] =
- Lexicon.const constrainAbsC $ absfree_proper (x, T, t) $ tT
- | abs_tr (*"_abs"*) [Const ("_constrain", _) $ Const ("_idtdummy", T) $ tT, t] =
- Lexicon.const constrainAbsC $ Term.absdummy (T, t) $ tT
- | abs_tr (*"_abs"*) ts = raise TERM ("abs_tr", ts);
+fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
+ | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
+ | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Lexicon.const constrainAbsC $ abs_tr [x, t] $ tT
+ | abs_tr ts = raise TERM ("abs_tr", ts);
(* binder *)
fun mk_binder_tr (syn, name) =
let
- fun tr (Free (x, T), t) = Lexicon.const name $ absfree_proper (x, T, t)
- | tr (Const ("_idtdummy", T), t) = Lexicon.const name $ Term.absdummy (T, t)
- | tr (Const ("_constrain", _) $ Free (x, T) $ tT, t) =
- Lexicon.const name $ (Lexicon.const constrainAbsC $ absfree_proper (x, T, t) $ tT)
- | tr (Const ("_constrain", _) $ Const ("_idtdummy", T) $ tT, t) =
- Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absdummy (T, t) $ tT)
- | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
- | tr (t1, t2) = raise TERM ("binder_tr", [t1, t2]);
-
- fun binder_tr [idts, body] = tr (idts, body)
- | binder_tr ts = raise TERM ("binder_tr", ts);
+ fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
+ fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
+ | binder_tr [x, t] =
+ let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
+ in Lexicon.const name $ abs end
+ | binder_tr ts = err ts;
in (syn, binder_tr) end;
@@ -197,8 +195,10 @@
fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
| update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
| update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
- list_comb (c $ update_name_tr [t] $
- (Lexicon.const "\\<^type>fun" $ ty $ Lexicon.const "\\<^type>dummy"), ts)
+ if Type_Ext.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
+ else
+ list_comb (c $ update_name_tr [t] $
+ (Lexicon.fun_type $ (Lexicon.fun_type $ ty $ ty) $ Lexicon.dummy_type), ts)
| update_name_tr ts = raise TERM ("update_name_tr", ts);
@@ -348,10 +348,8 @@
(* idtyp constraints *)
-fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant c, x, ty], xs] =
- if c = "_constrain" then
- Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
- else raise Match
+fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
+ Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
| idtyp_ast_tr' _ _ = raise Match;
@@ -498,7 +496,8 @@
(** Pure translations **)
val pure_trfuns =
- ([("_constify", constify_ast_tr),
+ ([("_strip_positions", strip_positions_ast_tr),
+ ("_constify", constify_ast_tr),
("_appl", appl_ast_tr),
("_applC", applC_ast_tr),
("_lambda", lambda_ast_tr),
@@ -534,29 +533,29 @@
-(** pts_to_asts **)
+(** parsetree_to_ast **)
-fun pts_to_asts ctxt trf pts =
+fun parsetree_to_ast ctxt constrain_pos trf =
let
fun trans a args =
(case trf a of
NONE => Ast.mk_appl (Ast.Constant a) args
| SOME f => f ctxt args);
- (*translate pt bottom-up*)
- fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
+ fun ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
+ if constrain_pos then
+ Ast.Appl [Ast.Constant "_constrain", ast_of pt,
+ Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
+ else ast_of pt
+ | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
| ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
-
- val exn_results = map (Exn.interruptible_capture ast_of) pts;
- val exns = map_filter Exn.get_exn exn_results;
- val results = map_filter Exn.get_result exn_results
- in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
+ in ast_of end;
-(** asts_to_terms **)
+(** ast_to_term **)
-fun asts_to_terms ctxt trf asts =
+fun ast_to_term ctxt trf =
let
fun trans a args =
(case trf a of
@@ -570,10 +569,6 @@
| term_of (Ast.Appl (ast :: (asts as _ :: _))) =
Term.list_comb (term_of ast, map term_of asts)
| term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
-
- val exn_results = map (Exn.interruptible_capture term_of) asts;
- val exns = map_filter Exn.get_exn exn_results;
- val results = map_filter Exn.get_result exn_results
- in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
+ in term_of end;
end;
--- a/src/Pure/Syntax/syntax.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML Tue Mar 22 21:22:50 2011 +0100
@@ -110,6 +110,8 @@
val print_trans: syntax -> unit
val print_syntax: syntax -> unit
val guess_infix: syntax -> string -> mixfix option
+ val positions_raw: Config.raw
+ val positions: bool Config.T
val ambiguity_enabled: bool Config.T
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
@@ -620,7 +622,7 @@
(Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
"asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
- "index", "struct"]);
+ "index", "struct", "id_position", "longid_position"]);
@@ -687,8 +689,19 @@
(** read **)
+fun some_results f xs =
+ let
+ val exn_results = map (Exn.interruptible_capture f) xs;
+ val exns = map_filter Exn.get_exn exn_results;
+ val results = map_filter Exn.get_result exn_results;
+ in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
+
+
(* read_ast *)
+val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
+val positions = Config.bool positions_raw;
+
val ambiguity_enabled =
Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
@@ -700,10 +713,10 @@
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
-fun read_asts ctxt (Syntax (tabs, _)) xids root (syms, pos) =
+fun read_asts ctxt (Syntax (tabs, _)) raw root (syms, pos) =
let
val {lexicon, gram, parse_ast_trtab, ...} = tabs;
- val toks = Lexicon.tokenize lexicon xids syms;
+ val toks = Lexicon.tokenize lexicon raw syms;
val _ = List.app (Lexicon.report_token ctxt) toks;
val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
@@ -714,29 +727,30 @@
val limit = Config.get ctxt ambiguity_limit;
fun show_pt pt =
- Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
+ Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt false (K NONE) pt));
+ val _ =
+ if len <= Config.get ctxt ambiguity_level then ()
+ else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
+ else
+ (Context_Position.if_visible ctxt warning (cat_lines
+ (("Ambiguous input" ^ Position.str_of pos ^
+ "\nproduces " ^ string_of_int len ^ " parse trees" ^
+ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+ map show_pt (take limit pts))));
+
+ val constrain_pos = not raw andalso Config.get ctxt positions;
in
- if len <= Config.get ctxt ambiguity_level then ()
- else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
- else
- (Context_Position.if_visible ctxt warning (cat_lines
- (("Ambiguous input" ^ Position.str_of pos ^
- "\nproduces " ^ string_of_int len ^ " parse trees" ^
- (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map show_pt (take limit pts))));
- Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
+ some_results (Syn_Trans.parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
end;
(* read *)
fun read ctxt (syn as Syntax (tabs, _)) root inp =
- let
- val {parse_ruletab, parse_trtab, ...} = tabs;
- val asts = read_asts ctxt syn false root inp;
- in
- Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
- (map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)) asts)
+ let val {parse_ruletab, parse_trtab, ...} = tabs in
+ read_asts ctxt syn false root inp
+ |> map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab))
+ |> some_results (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab))
end;
@@ -822,11 +836,11 @@
local
-fun check_rule (rule as (lhs, rhs)) =
+fun check_rule rule =
(case Ast.rule_error rule of
SOME msg =>
error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
- Ast.str_of_ast lhs ^ " -> " ^ Ast.str_of_ast rhs)
+ Pretty.string_of (Ast.pretty_rule rule))
| NONE => rule);
fun read_pattern ctxt syn (root, str) =
--- a/src/Pure/Syntax/type_ext.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/Syntax/type_ext.ML Tue Mar 22 21:22:50 2011 +0100
@@ -9,6 +9,9 @@
val sort_of_term: term -> sort
val term_sorts: term -> (indexname * sort) list
val typ_of_term: (indexname -> sort) -> term -> typ
+ val is_position: term -> bool
+ val strip_positions: term -> term
+ val strip_positions_ast: Ast.ast -> Ast.ast
val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
(string -> bool * string) -> (string -> string option) -> term -> term
val term_of_typ: bool -> typ -> term
@@ -101,6 +104,27 @@
in typ_of tm end;
+(* positions *)
+
+fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x)
+ | is_position _ = false;
+
+fun strip_positions ((t as Const (c, _)) $ u $ v) =
+ if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
+ then strip_positions u
+ else t $ strip_positions u $ strip_positions v
+ | strip_positions (t $ u) = strip_positions t $ strip_positions u
+ | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
+ | strip_positions t = t;
+
+fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) =
+ if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x)
+ then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts)
+ else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts))
+ | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts)
+ | strip_positions_ast ast = ast;
+
+
(* decode_term -- transform parse tree into raw term *)
fun decode_term get_sort map_const map_free tm =
@@ -108,10 +132,11 @@
val decodeT = typ_of_term (get_sort (term_sorts tm));
fun decode (Const ("_constrain", _) $ t $ typ) =
- Type.constraint (decodeT typ) (decode t)
- | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
- if T = dummyT then Abs (x, decodeT typ, decode t)
- else Type.constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
+ if is_position typ then decode t
+ else Type.constraint (decodeT typ) (decode t)
+ | decode (Const ("_constrainAbs", _) $ t $ typ) =
+ if is_position typ then decode t
+ else Type.constraint (decodeT typ --> dummyT) (decode t)
| decode (Abs (x, T, t)) = Abs (x, T, decode t)
| decode (t $ u) = decode t $ decode u
| decode (Const (a, T)) =
@@ -162,7 +187,9 @@
fun term_of (Type (a, Ts)) =
Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
- | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
+ | term_of (TFree (x, S)) =
+ if is_some (Lexicon.decode_position x) then Lexicon.free x
+ else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
| term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
in term_of ty end;
--- a/src/Pure/pure_thy.ML Tue Mar 22 20:06:10 2011 +0100
+++ b/src/Pure/pure_thy.ML Tue Mar 22 21:22:50 2011 +0100
@@ -69,9 +69,9 @@
("_abs", typ "'a", NoSyn),
("", typ "'a => args", Delimfix "_"),
("_args", typ "'a => args => args", Delimfix "_,/ _"),
- ("", typ "id => idt", Delimfix "_"),
+ ("", typ "id_position => idt", Delimfix "_"),
("_idtdummy", typ "idt", Delimfix "'_"),
- ("_idtyp", typ "id => type => idt", Mixfix ("_::_", [], 0)),
+ ("_idtyp", typ "id_position => type => idt", Mixfix ("_::_", [], 0)),
("_idtypdummy", typ "type => idt", Mixfix ("'_()::_", [], 0)),
("", typ "idt => idt", Delimfix "'(_')"),
("", typ "idt => idts", Delimfix "_"),
@@ -80,8 +80,8 @@
("", typ "pttrn => pttrns", Delimfix "_"),
("_pttrns", typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)),
("", typ "aprop => aprop", Delimfix "'(_')"),
- ("", typ "id => aprop", Delimfix "_"),
- ("", typ "longid => aprop", Delimfix "_"),
+ ("", typ "id_position => aprop", Delimfix "_"),
+ ("", typ "longid_position => aprop", Delimfix "_"),
("", typ "var => aprop", Delimfix "_"),
("_DDDOT", typ "aprop", Delimfix "..."),
("_aprop", typ "aprop => prop", Delimfix "PROP _"),
@@ -91,10 +91,11 @@
("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
("_mk_ofclass", typ "dummy", NoSyn),
("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"),
- ("", typ "id => logic", Delimfix "_"),
- ("", typ "longid => logic", Delimfix "_"),
+ ("", typ "id_position => logic", Delimfix "_"),
+ ("", typ "longid_position => logic", Delimfix "_"),
("", typ "var => logic", Delimfix "_"),
("_DDDOT", typ "logic", Delimfix "..."),
+ ("_strip_positions", typ "'a", NoSyn),
("_constify", typ "num => num_const", Delimfix "_"),
("_constify", typ "float_token => float_const", Delimfix "_"),
("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"),
@@ -104,6 +105,9 @@
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
("_update_name", typ "idt", NoSyn),
(Syntax.constrainAbsC, typ "'a", NoSyn),
+ ("_constrain_position", typ "id => id_position", Delimfix "_"),
+ ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
+ ("_type_constraint_", typ "'a", NoSyn),
(const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
(const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
@@ -116,9 +120,8 @@
("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
+ ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
- ("_type_constraint_", typ "'a", NoSyn),
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
(const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
(const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),