# HG changeset patch # User wenzelm # Date 1302099357 -7200 # Node ID c539d3c9c023a67cf5f772d8a57ef9b584ee748e # Parent bdb88b1cb2b72bda797dea53311262b7ab86a0bb more abstract syntax translation; diff -r bdb88b1cb2b7 -r c539d3c9c023 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Apr 06 15:43:45 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Wed Apr 06 16:15:57 2011 +0200 @@ -118,6 +118,12 @@ val is_keyword: syntax -> string -> bool val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list + val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option + val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option + val print_translation: syntax -> string -> (Proof.context -> typ -> term list -> term) list + val print_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) list + val token_translation: syntax -> string list -> + string -> (Proof.context -> string -> Pretty.T) option type mode val mode_default: mode val mode_input: mode @@ -402,6 +408,8 @@ fun err_dup_trfun name c = error ("More than one " ^ name ^ " for " ^ quote c); +fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c); + fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns; fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab) @@ -413,6 +421,8 @@ (* print (ast) translations *) +fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c); + fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns; fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns; fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2); @@ -495,6 +505,12 @@ fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt gram; +fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab; +fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab; +fun print_translation (Syntax ({print_trtab, ...}, _)) = lookup_tr' print_trtab; +fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = lookup_tr' print_ast_trtab; +fun token_translation (Syntax ({tokentrtab, ...}, _)) = lookup_tokentr tokentrtab; + type mode = string * bool; val mode_default = ("", true); val mode_input = (Print_Mode.input, true); diff -r bdb88b1cb2b7 -r c539d3c9c023 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 15:43:45 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 16:15:57 2011 +0200 @@ -89,8 +89,6 @@ (* parsetree_to_ast *) -fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c); - fun parsetree_to_ast ctxt constrain_pos trf parsetree = let val tsig = ProofContext.tsig_of ctxt; @@ -240,7 +238,7 @@ fun parse_asts ctxt raw root (syms, pos) = let val syn = ProofContext.syn_of ctxt; - val {parse_ast_trtab, ...} = Syntax.rep_syntax syn; + val ast_tr = Syntax.parse_ast_translation syn; val toks = Syntax.tokenize syn raw syms; val _ = List.app (Lexicon.report_token ctxt) toks; @@ -263,14 +261,16 @@ map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts)))); val constrain_pos = not raw andalso Config.get ctxt Syntax.positions; - val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab); + val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr; in map parsetree_to_ast pts end; fun parse_raw ctxt root input = let - val {parse_ruletab, parse_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt); + val syn = ProofContext.syn_of ctxt; + val tr = Syntax.parse_translation syn; + val {parse_ruletab, ...} = Syntax.rep_syntax syn; val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab); - val ast_to_term = ast_to_term ctxt (lookup_tr parse_trtab); + val ast_to_term = ast_to_term ctxt tr; in parse_asts ctxt false root input |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term) @@ -558,17 +558,18 @@ local -fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c); - fun unparse_t t_to_ast prt_t markup ctxt curried t = let - val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = - Syntax.rep_syntax (ProofContext.syn_of ctxt); - val ast = t_to_ast ctxt (lookup_tr' print_trtab) t; + val syn = ProofContext.syn_of ctxt; + val tr' = Syntax.print_translation syn; + val ast_tr' = Syntax.print_ast_translation syn; + val tokentr = Syntax.token_translation syn (print_mode_value ()); + val {print_ruletab, tokentrtab, prtabs, ...} = Syntax.rep_syntax syn; in - Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab) - (Syntax.lookup_tokentr tokentrtab (print_mode_value ())) - (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast)) + t_to_ast ctxt tr' t + |> Ast.normalize ctxt (Symtab.lookup_list print_ruletab) + |> prt_t ctxt curried prtabs ast_tr' tokentr + |> Pretty.markup markup end; in