# HG changeset patch # User berghofe # Date 1085168827 -7200 # Node ID 702cb4859cabfcbee3b833f0ef3d44fdc9ed5f6a # Parent 546365fe8349711812d96bf7719c43d3540d94fe Modified functions pt_to_ast and ast_to_term to improve handling of errors in parse (ast) translations caused by ambiguous input. diff -r 546365fe8349 -r 702cb4859cab src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Fri May 21 21:46:25 2004 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Fri May 21 21:47:07 2004 +0200 @@ -50,8 +50,8 @@ 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 pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast - val ast_to_term: (string -> (term list -> term) option) -> Ast.ast -> term + val pts_to_asts: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree list -> Ast.ast list + val asts_to_terms: (string -> (term list -> term) option) -> Ast.ast list -> term list end; structure SynTrans: SYN_TRANS = @@ -452,36 +452,44 @@ -(** pt_to_ast **) +exception TRANSLATION of string * exn -fun pt_to_ast trf pt = +(** pts_to_asts **) + +fun pts_to_asts trf pts = let fun trans a args = (case trf a of None => Ast.mk_appl (Ast.Constant a) args - | Some f => f args handle exn - => (writeln ("Error in parse ast translation for " ^ quote a); - raise exn)); + | Some f => f args handle exn => raise TRANSLATION (a, exn)); (*translate pt bottom-up*) fun 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 (fn pt => Result (ast_of pt) handle exn => Exn exn) pts; + val exns = mapfilter get_exn exn_results; + val results = mapfilter get_result exn_results in - ast_of pt + case results of + [] => (case exns of + TRANSLATION (a, exn) :: _ => + (writeln ("Error in parse ast translation for " ^ quote a); raise exn) + | _ => []) + | _ => results end; -(** ast_to_term **) +(** asts_to_terms **) -fun ast_to_term trf ast = +fun asts_to_terms trf asts = let fun trans a args = (case trf a of None => Term.list_comb (Lexicon.const a, args) - | Some f => f args handle exn - => (writeln ("Error in parse translation for " ^ quote a); - raise exn)); + | Some f => f args handle exn => raise TRANSLATION (a, exn)); fun term_of (Ast.Constant a) = trans a [] | term_of (Ast.Variable x) = Lexicon.read_var x @@ -490,8 +498,18 @@ | 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 (fn t => Result (term_of t) handle exn => Exn exn) asts; + val exns = mapfilter get_exn exn_results; + val results = mapfilter get_result exn_results in - term_of ast + case results of + [] => (case exns of + TRANSLATION (a, exn) :: _ => + (writeln ("Error in parse translation for " ^ quote a); raise exn) + | _ => []) + | _ => results end; end; diff -r 546365fe8349 -r 702cb4859cab src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri May 21 21:46:25 2004 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri May 21 21:47:07 2004 +0200 @@ -339,9 +339,9 @@ fun show_pt pt = let - val raw_ast = SynTrans.pt_to_ast (K None) pt; + val [raw_ast] = SynTrans.pts_to_asts (K None) [pt]; val _ = writeln ("raw: " ^ Ast.str_of_ast raw_ast); - val pre_ast = SynTrans.pt_to_ast (lookup_tr parse_ast_trtab) pt; + val [pre_ast] = SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) [pt]; val _ = Ast.normalize true true (lookup_ruletab parse_ruletab) pre_ast; in () end; in seq show_pt (Parser.parse gram root toks) end; @@ -359,7 +359,7 @@ val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars); fun show_pt pt = - warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt))); + warning (Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts (K None) [pt])))); in if length pts > ! ambiguity_level then if ! ambiguity_is_error then @@ -369,7 +369,7 @@ warning "produces the following parse trees:"; seq show_pt pts) else (); - map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts + SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) pts end; @@ -380,7 +380,7 @@ val {parse_ruletab, parse_trtab, ...} = tabs; val asts = read_asts syn false (SynExt.typ_to_nonterm ty) str; in - map (SynTrans.ast_to_term (lookup_tr parse_trtab)) + SynTrans.asts_to_terms (lookup_tr parse_trtab) (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts) end;