Modified functions pt_to_ast and ast_to_term to improve handling
authorberghofe
Fri May 21 21:47:07 2004 +0200 (2004-05-21)
changeset 14798702cb4859cab
parent 14797 546365fe8349
child 14799 a405aadff16c
Modified functions pt_to_ast and ast_to_term to improve handling
of errors in parse (ast) translations caused by ambiguous input.
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri May 21 21:46:25 2004 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri May 21 21:47:07 2004 +0200
     1.3 @@ -50,8 +50,8 @@
     1.4    val prop_tr': term -> term
     1.5    val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
     1.6    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
     1.7 -  val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
     1.8 -  val ast_to_term: (string -> (term list -> term) option) -> Ast.ast -> term
     1.9 +  val pts_to_asts: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree list -> Ast.ast list
    1.10 +  val asts_to_terms: (string -> (term list -> term) option) -> Ast.ast list -> term list
    1.11  end;
    1.12  
    1.13  structure SynTrans: SYN_TRANS =
    1.14 @@ -452,36 +452,44 @@
    1.15  
    1.16  
    1.17  
    1.18 -(** pt_to_ast **)
    1.19 +exception TRANSLATION of string * exn
    1.20  
    1.21 -fun pt_to_ast trf pt =
    1.22 +(** pts_to_asts **)
    1.23 +
    1.24 +fun pts_to_asts trf pts =
    1.25    let
    1.26      fun trans a args =
    1.27        (case trf a of
    1.28          None => Ast.mk_appl (Ast.Constant a) args
    1.29 -      | Some f => f args handle exn
    1.30 -          => (writeln ("Error in parse ast translation for " ^ quote a);
    1.31 -              raise exn));
    1.32 +      | Some f => f args handle exn => raise TRANSLATION (a, exn));
    1.33  
    1.34      (*translate pt bottom-up*)
    1.35      fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
    1.36        | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
    1.37 +
    1.38 +    val exn_results =
    1.39 +      map (fn pt => Result (ast_of pt) handle exn => Exn exn) pts;
    1.40 +    val exns = mapfilter get_exn exn_results;
    1.41 +    val results = mapfilter get_result exn_results
    1.42    in
    1.43 -    ast_of pt
    1.44 +    case results of
    1.45 +      [] => (case exns of
    1.46 +        TRANSLATION (a, exn) :: _ =>
    1.47 +          (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
    1.48 +      | _ => [])
    1.49 +    | _ => results
    1.50    end;
    1.51  
    1.52  
    1.53  
    1.54 -(** ast_to_term **)
    1.55 +(** asts_to_terms **)
    1.56  
    1.57 -fun ast_to_term trf ast =
    1.58 +fun asts_to_terms trf asts =
    1.59    let
    1.60      fun trans a args =
    1.61        (case trf a of
    1.62          None => Term.list_comb (Lexicon.const a, args)
    1.63 -      | Some f => f args handle exn
    1.64 -          => (writeln ("Error in parse translation for " ^ quote a);
    1.65 -              raise exn));
    1.66 +      | Some f => f args handle exn => raise TRANSLATION (a, exn));
    1.67  
    1.68      fun term_of (Ast.Constant a) = trans a []
    1.69        | term_of (Ast.Variable x) = Lexicon.read_var x
    1.70 @@ -490,8 +498,18 @@
    1.71        | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
    1.72            Term.list_comb (term_of ast, map term_of asts)
    1.73        | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
    1.74 +
    1.75 +    val exn_results =
    1.76 +      map (fn t => Result (term_of t) handle exn => Exn exn) asts;
    1.77 +    val exns = mapfilter get_exn exn_results;
    1.78 +    val results = mapfilter get_result exn_results
    1.79    in
    1.80 -    term_of ast
    1.81 +    case results of
    1.82 +      [] => (case exns of
    1.83 +        TRANSLATION (a, exn) :: _ =>
    1.84 +          (writeln ("Error in parse translation for " ^ quote a); raise exn)
    1.85 +      | _ => [])
    1.86 +    | _ => results
    1.87    end;
    1.88  
    1.89  end;
     2.1 --- a/src/Pure/Syntax/syntax.ML	Fri May 21 21:46:25 2004 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Fri May 21 21:47:07 2004 +0200
     2.3 @@ -339,9 +339,9 @@
     2.4  
     2.5      fun show_pt pt =
     2.6        let
     2.7 -        val raw_ast = SynTrans.pt_to_ast (K None) pt;
     2.8 +        val [raw_ast] = SynTrans.pts_to_asts (K None) [pt];
     2.9          val _ = writeln ("raw: " ^ Ast.str_of_ast raw_ast);
    2.10 -        val pre_ast = SynTrans.pt_to_ast (lookup_tr parse_ast_trtab) pt;
    2.11 +        val [pre_ast] = SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) [pt];
    2.12          val _ = Ast.normalize true true (lookup_ruletab parse_ruletab) pre_ast;
    2.13        in () end;
    2.14    in seq show_pt (Parser.parse gram root toks) end;
    2.15 @@ -359,7 +359,7 @@
    2.16      val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
    2.17  
    2.18      fun show_pt pt =
    2.19 -      warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
    2.20 +      warning (Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts (K None) [pt]))));
    2.21    in
    2.22      if length pts > ! ambiguity_level then
    2.23          if ! ambiguity_is_error then
    2.24 @@ -369,7 +369,7 @@
    2.25               warning "produces the following parse trees:";
    2.26               seq show_pt pts)
    2.27      else ();
    2.28 -    map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
    2.29 +    SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) pts
    2.30    end;
    2.31  
    2.32  
    2.33 @@ -380,7 +380,7 @@
    2.34      val {parse_ruletab, parse_trtab, ...} = tabs;
    2.35      val asts = read_asts syn false (SynExt.typ_to_nonterm ty) str;
    2.36    in
    2.37 -    map (SynTrans.ast_to_term (lookup_tr parse_trtab))
    2.38 +    SynTrans.asts_to_terms (lookup_tr parse_trtab)
    2.39        (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts)
    2.40    end;
    2.41