# HG changeset patch # User wenzelm # Date 1300825370 -3600 # Node ID b579e787b582e91745529698baed2f7d17681a62 # Parent 66c8281349ecc1ace84065b241d27e0bd580ad42# Parent 3eba96ff3d3e7cb823715868eb23a212f40637bd merged diff -r 66c8281349ec -r b579e787b582 NEWS --- 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) diff -r 66c8281349ec -r b579e787b582 src/CCL/Term.thy --- 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 {* diff -r 66c8281349ec -r b579e787b582 src/HOL/HOL.thy --- 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 "\" 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_ \/ _)" 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_ \/ _)" 10) - notation (xsymbols) All (binder "\" 10) and Ex (binder "\" 10) and diff -r 66c8281349ec -r b579e787b582 src/HOL/HOLCF/Cfun.thy --- 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; *} diff -r 66c8281349ec -r b579e787b582 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- 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}) diff -r 66c8281349ec -r b579e787b582 src/HOL/HOLCF/ex/Pattern_Match.thy --- 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_ \/ _)" 10) + "_Case1" :: "[Case_pat, 'b] => Case_syn" ("(2_ \/ _)" 10) translations "_Case_syntax x ms" == "CONST cases\(ms\x)" diff -r 66c8281349ec -r b579e787b582 src/HOL/Hoare/Hoare_Logic.thy --- 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] = diff -r 66c8281349ec -r b579e787b582 src/HOL/Hoare/Hoare_Logic_Abort.thy --- 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] = diff -r 66c8281349ec -r b579e787b582 src/HOL/Isar_Examples/Hoare.thy --- 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 [\a/\x] \x := \a P" +lemma assign: "|- P [\a/\x::'a] \x := \a P" by (rule basic) text {* Note that above formulation of assignment corresponds to our diff -r 66c8281349ec -r b579e787b582 src/HOL/List.thy --- 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; diff -r 66c8281349ec -r b579e787b582 src/HOL/Statespace/state_space.ML --- 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 diff -r 66c8281349ec -r b579e787b582 src/HOL/Tools/Datatype/datatype_case.ML --- 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; diff -r 66c8281349ec -r b579e787b582 src/Pure/General/timing.ML --- 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 (); diff -r 66c8281349ec -r b579e787b582 src/Pure/Isar/attrib.ML --- 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 #> diff -r 66c8281349ec -r b579e787b582 src/Pure/Isar/proof.ML --- 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 diff -r 66c8281349ec -r b579e787b582 src/Pure/ML/ml_syntax.ML --- 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; diff -r 66c8281349ec -r b579e787b582 src/Pure/Syntax/ast.ML --- 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") diff -r 66c8281349ec -r b579e787b582 src/Pure/Syntax/lexicon.ML --- 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 = ""; +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; diff -r 66c8281349ec -r b579e787b582 src/Pure/Syntax/printer.ML --- 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]); diff -r 66c8281349ec -r b579e787b582 src/Pure/Syntax/syn_trans.ML --- 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; diff -r 66c8281349ec -r b579e787b582 src/Pure/Syntax/syntax.ML --- 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) = diff -r 66c8281349ec -r b579e787b582 src/Pure/Syntax/type_ext.ML --- 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; diff -r 66c8281349ec -r b579e787b582 src/Pure/pure_thy.ML --- 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 ("\\_", [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 ("_\\_", [1000, 0], 1000)), ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\_", [4, 0], 3)), - ("_idtyp", typ "id => type => idt", Mixfix ("_\\_", [], 0)), + ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\_", [], 0)), ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), - ("_type_constraint_", typ "'a", NoSyn), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), (const "==", typ "'a => 'a => prop", Infixr ("\\", 2)), (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)),