clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
authorwenzelm
Mon Mar 21 20:56:44 2011 +0100 (2011-03-21)
changeset 420432055515c9d3f
parent 42042 264f8d0e899f
child 42044 17dc2c6edb93
clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Mon Mar 21 20:15:03 2011 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Mon Mar 21 20:56:44 2011 +0100
     1.3 @@ -55,11 +55,10 @@
     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 pts_to_asts: Proof.context ->
     1.8 -    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
     1.9 -    Parser.parsetree list -> Ast.ast list
    1.10 -  val asts_to_terms: Proof.context ->
    1.11 -    (string -> (Proof.context -> term list -> term) option) -> Ast.ast list -> term list
    1.12 +  val parsetree_to_ast: Proof.context ->
    1.13 +    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
    1.14 +  val ast_to_term: Proof.context ->
    1.15 +    (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
    1.16  end;
    1.17  
    1.18  structure Syn_Trans: SYN_TRANS =
    1.19 @@ -534,29 +533,24 @@
    1.20  
    1.21  
    1.22  
    1.23 -(** pts_to_asts **)
    1.24 +(** parsetree_to_ast **)
    1.25  
    1.26 -fun pts_to_asts ctxt trf pts =
    1.27 +fun parsetree_to_ast ctxt trf =
    1.28    let
    1.29      fun trans a args =
    1.30        (case trf a of
    1.31          NONE => Ast.mk_appl (Ast.Constant a) args
    1.32        | SOME f => f ctxt args);
    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 = map (Exn.interruptible_capture ast_of) pts;
    1.39 -    val exns = map_filter Exn.get_exn exn_results;
    1.40 -    val results = map_filter Exn.get_result exn_results
    1.41 -  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
    1.42 +  in ast_of end;
    1.43  
    1.44  
    1.45  
    1.46 -(** asts_to_terms **)
    1.47 +(** ast_to_term **)
    1.48  
    1.49 -fun asts_to_terms ctxt trf asts =
    1.50 +fun ast_to_term ctxt trf =
    1.51    let
    1.52      fun trans a args =
    1.53        (case trf a of
    1.54 @@ -570,10 +564,6 @@
    1.55        | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
    1.56            Term.list_comb (term_of ast, map term_of asts)
    1.57        | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
    1.58 -
    1.59 -    val exn_results = map (Exn.interruptible_capture term_of) asts;
    1.60 -    val exns = map_filter Exn.get_exn exn_results;
    1.61 -    val results = map_filter Exn.get_result exn_results
    1.62 -  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
    1.63 +  in term_of end;
    1.64  
    1.65  end;
     2.1 --- a/src/Pure/Syntax/syntax.ML	Mon Mar 21 20:15:03 2011 +0100
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Mar 21 20:56:44 2011 +0100
     2.3 @@ -714,18 +714,22 @@
     2.4  
     2.5      val limit = Config.get ctxt ambiguity_limit;
     2.6      fun show_pt pt =
     2.7 -      Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
     2.8 -  in
     2.9 -    if len <= Config.get ctxt ambiguity_level then ()
    2.10 -    else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
    2.11 -    else
    2.12 -      (Context_Position.if_visible ctxt warning (cat_lines
    2.13 -        (("Ambiguous input" ^ Position.str_of pos ^
    2.14 -          "\nproduces " ^ string_of_int len ^ " parse trees" ^
    2.15 -          (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    2.16 -          map show_pt (take limit pts))));
    2.17 -    Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
    2.18 -  end;
    2.19 +      Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt (K NONE) pt));
    2.20 +    val _ =
    2.21 +      if len <= Config.get ctxt ambiguity_level then ()
    2.22 +      else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
    2.23 +      else
    2.24 +        (Context_Position.if_visible ctxt warning (cat_lines
    2.25 +          (("Ambiguous input" ^ Position.str_of pos ^
    2.26 +            "\nproduces " ^ string_of_int len ^ " parse trees" ^
    2.27 +            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    2.28 +            map show_pt (take limit pts))));
    2.29 +
    2.30 +    val ast_of = Syn_Trans.parsetree_to_ast ctxt (lookup_tr parse_ast_trtab);
    2.31 +    val exn_results = map (Exn.interruptible_capture ast_of) pts;
    2.32 +    val exns = map_filter Exn.get_exn exn_results;
    2.33 +    val results = map_filter Exn.get_result exn_results
    2.34 +  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
    2.35  
    2.36  
    2.37  (* read *)
    2.38 @@ -733,11 +737,14 @@
    2.39  fun read ctxt (syn as Syntax (tabs, _)) root inp =
    2.40    let
    2.41      val {parse_ruletab, parse_trtab, ...} = tabs;
    2.42 -    val asts = read_asts ctxt syn false root inp;
    2.43 -  in
    2.44 -    Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
    2.45 -      (map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)) asts)
    2.46 -  end;
    2.47 +    val asts = read_asts ctxt syn false root inp
    2.48 +      |> map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab));
    2.49 +
    2.50 +    val term_of = Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab);
    2.51 +    val exn_results = map (Exn.interruptible_capture term_of) asts;
    2.52 +    val exns = map_filter Exn.get_exn exn_results;
    2.53 +    val results = map_filter Exn.get_result exn_results
    2.54 +  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
    2.55  
    2.56  
    2.57  (* read terms *)