# HG changeset patch # User wenzelm # Date 1300797140 -3600 # Node ID afd11ca8e01879495e04aa9d7d399baacd2ffdd0 # Parent a7a4e04b538633ce3a02c4baa3db99e35dc302cd support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast; diff -r a7a4e04b5386 -r afd11ca8e018 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Tue Mar 22 11:14:33 2011 +0100 +++ b/src/Pure/Syntax/ast.ML Tue Mar 22 13:32:20 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 a7a4e04b5386 -r afd11ca8e018 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Tue Mar 22 11:14:33 2011 +0100 +++ b/src/Pure/Syntax/lexicon.ML Tue Mar 22 13:32:20 2011 +0100 @@ -42,6 +42,7 @@ case_fixed: string -> 'a, case_default: string -> 'a} -> string -> 'a val is_marked: string -> bool + val pretty_position: Position.T -> Pretty.T val encode_position: Position.T -> string val decode_position: string -> Position.T option end; @@ -456,13 +457,20 @@ (* 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 = - op ^ (YXML.output_markup (Position.markup pos Markup.position)); + 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), [])] => - if name = Markup.positionN then SOME (Position.of_properties props) + [XML.Elem ((name, props), [arg])] => + if name = Markup.positionN andalso arg = position_text + then SOME (Position.of_properties props) else NONE | _ => NONE); diff -r a7a4e04b5386 -r afd11ca8e018 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Tue Mar 22 11:14:33 2011 +0100 +++ b/src/Pure/Syntax/printer.ML Tue Mar 22 13:32:20 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 a7a4e04b5386 -r afd11ca8e018 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Tue Mar 22 11:14:33 2011 +0100 +++ b/src/Pure/Syntax/syn_trans.ML Tue Mar 22 13:32:20 2011 +0100 @@ -55,7 +55,7 @@ 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 parsetree_to_ast: Proof.context -> + 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 @@ -98,32 +98,24 @@ 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) + 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 _ => raise TERM ("binder_tr", [x, t]) + in Lexicon.const name $ abs end | binder_tr ts = raise TERM ("binder_tr", ts); in (syn, binder_tr) end; @@ -533,14 +525,19 @@ (** parsetree_to_ast **) -fun parsetree_to_ast ctxt trf = +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); - 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); in ast_of end; diff -r a7a4e04b5386 -r afd11ca8e018 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Mar 22 11:14:33 2011 +0100 +++ b/src/Pure/Syntax/syntax.ML Tue Mar 22 13:32:20 2011 +0100 @@ -620,7 +620,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"]); @@ -708,10 +708,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) @@ -722,7 +722,7 @@ val limit = Config.get ctxt ambiguity_limit; fun show_pt pt = - Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast 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) @@ -733,7 +733,7 @@ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: map show_pt (take limit pts)))); in - some_results (Syn_Trans.parsetree_to_ast ctxt (lookup_tr parse_ast_trtab)) pts + some_results (Syn_Trans.parsetree_to_ast ctxt false (lookup_tr parse_ast_trtab)) pts end; @@ -829,11 +829,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 a7a4e04b5386 -r afd11ca8e018 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Tue Mar 22 11:14:33 2011 +0100 +++ b/src/Pure/Syntax/type_ext.ML Tue Mar 22 13:32:20 2011 +0100 @@ -103,15 +103,19 @@ (* decode_term -- transform parse tree into raw term *) +fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x) + | is_position _ = false; + fun decode_term get_sort map_const map_free tm = let 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 +166,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 a7a4e04b5386 -r afd11ca8e018 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Mar 22 11:14:33 2011 +0100 +++ b/src/Pure/pure_thy.ML Tue Mar 22 13:32:20 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,8 +91,8 @@ ("_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 "..."), ("_constify", typ "num => num_const", Delimfix "_"), @@ -104,6 +104,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 +119,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)),