standard_parse_term: added pp/check argument, include disambig here (from sign.ML);
authorwenzelm
Mon Aug 20 23:41:43 2007 +0200 (2007-08-20)
changeset 24372743575ccfec8
parent 24371 80bd6edc8ba4
child 24373 eb199bbbaec0
standard_parse_term: added pp/check argument, include disambig here (from sign.ML);
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Aug 20 23:41:40 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Aug 20 23:41:43 2007 +0200
     1.3 @@ -73,11 +73,11 @@
     1.4    val print_trans: syntax -> unit
     1.5    val print_syntax: syntax -> unit
     1.6    val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
     1.7 -  val standard_parse_term:
     1.8 +  val standard_parse_term: Pretty.pp -> (term -> term Exn.result) ->
     1.9      (((string * int) * sort) list -> string * int -> Term.sort) ->
    1.10      (string -> string option) -> (string -> string option) ->
    1.11      (typ -> typ) -> (sort -> sort) -> Proof.context ->
    1.12 -    (string -> bool) -> syntax -> typ -> string -> term list
    1.13 +    (string -> bool) -> syntax -> typ -> string -> term
    1.14    val standard_parse_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
    1.15      (sort -> sort) -> string -> typ
    1.16    val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort
    1.17 @@ -441,9 +441,36 @@
    1.18  
    1.19  (* read terms *)
    1.20  
    1.21 -fun standard_parse_term get_sort map_const map_free map_type map_sort ctxt is_logtype syn ty str =
    1.22 -  map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
    1.23 -    (read ctxt is_logtype syn ty str);
    1.24 +(*brute-force disambiguation via type-inference*)
    1.25 +fun disambig _ _ [t] = t
    1.26 +  | disambig pp check ts =
    1.27 +      let
    1.28 +        val err_results = map check ts;
    1.29 +        val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
    1.30 +        val results = map_filter Exn.get_result err_results;
    1.31 +
    1.32 +        val ambiguity = length ts;
    1.33 +        fun ambig_msg () =
    1.34 +          if ambiguity > 1 andalso ambiguity <= ! ambiguity_level then
    1.35 +            "Got more than one parse tree.\n\
    1.36 +            \Retry with smaller ambiguity_level for more information."
    1.37 +          else "";
    1.38 +      in
    1.39 +        if null results then cat_error (ambig_msg ()) (cat_lines errs)
    1.40 +        else if length results = 1 then
    1.41 +          (if ambiguity > ! ambiguity_level then
    1.42 +            warning "Fortunately, only one parse tree is type correct.\n\
    1.43 +              \You may still want to disambiguate your grammar or your input."
    1.44 +          else (); hd results)
    1.45 +        else cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
    1.46 +          cat_lines (map (Pretty.string_of_term pp) ts))
    1.47 +      end;
    1.48 +
    1.49 +fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
    1.50 +    ctxt is_logtype syn ty str =
    1.51 +  read ctxt is_logtype syn ty str
    1.52 +  |> map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
    1.53 +  |> disambig (Printer.pp_show_brackets pp) check;
    1.54  
    1.55  
    1.56  (* read types *)