From 54e55518261ee5f3c68758ea070b1bac41400e54 Mon Sep 17 00:00:00 2001 From: acondolu Date: Sun, 23 Jul 2017 22:23:34 +0200 Subject: [PATCH] Better error messages in parser --- ocaml/parser.ml | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/ocaml/parser.ml b/ocaml/parser.ml index 6bcb70d..34b62ba 100644 --- a/ocaml/parser.ml +++ b/ocaml/parser.ml @@ -18,7 +18,7 @@ let mk_var' (bound, free) x = ;; let mk_app' = function - | [] -> raise (ParsingError "bug") + | [] -> assert false | t :: ts -> List.fold_left mk_app t ts ;; @@ -73,12 +73,12 @@ let rec read_smt vars = | Some varname, cs -> let vars' = (varname::bound, free) in (match strip_spaces cs with - | [] -> raise (ParsingError "manca dopo variabile lambda") + | [] -> raise (ParsingError "Lambda expression incomplete") | c::cs -> (if c = '.' then (match read_smt vars' cs with - | None, _, _ -> raise (ParsingError "manca corpo lambda") + | None, _, _ -> raise (ParsingError "Lambda body expected") | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free) - | Some _, _, _ -> raise (ParsingError "???") - ) else raise (ParsingError "manca . nel lambda") + | Some _, _, _ -> assert false + ) else raise (ParsingError "Expected `.` after variable in lambda") )) | _, _ -> assert false ) in let rec aux vars cs = @@ -96,7 +96,7 @@ let rec read_smt vars = | None, cs, vars -> Some [tm], cs, vars | Some ts, cs, vars -> Some (tm :: ts), cs, vars ) - | Some _ -> raise (ParsingError "bug") + | Some _ -> assert false | None -> None, x, vars in fun cs -> match aux vars cs with | None, cs, vars -> None, cs, vars @@ -108,20 +108,20 @@ and read_pars vars = function let cs = strip_spaces cs in match cs with | [] -> None, [], vars - | c::cs -> if c = ')' then tm, cs, vars else raise (ParsingError ") mancante") - ) else raise (ParsingError "???") + | c::cs -> if c = ')' then tm, cs, vars else raise (ParsingError "Missing `)`") + ) else assert false ;; let parse x = match read_smt ([],[]) (explode x) with | Some [y], [], _ -> y - | _, _, _ -> raise (ParsingError "???") + | _, _, _ -> assert false ;; let parse_many strs = let f (x, y) z = match read_smt y (explode z) with | Some[tm], [], vars -> (tm :: x, vars) - | _, _, _ -> raise (ParsingError "???") + | _, _, _ -> assert false in let aux = List.fold_left f ([], ([], [])) (* index zero is reserved *) in let (tms, (_, free)) = aux strs in (List.rev tms, free) @@ -169,7 +169,7 @@ let problem_of_string s = let strs = [div] @ ps @ conv in if List.length ps = 0 && List.length conv = 0 - then raise (ParsingError "empty problem"); + then raise (ParsingError "Parsed empty problem"); (* parse' *) let (tms, free) = parse_many strs in @@ -187,6 +187,7 @@ let problem_of_string s = let open Num in let exclude_bottom = function | #nf_nob as t -> t + (* actually, the following may be assert false *) | `Bottom -> raise (ParsingError "Input term not in normal form") in let rec aux_nob lev : nf_nob -> nf = function | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args) @@ -206,17 +207,17 @@ let div = if not div_provided || div = `Bottom then None else match div with | `I _ as t -> Some t - | _ -> raise (ParsingError "div is not an inert or BOT in the initial problem") in + | _ -> raise (ParsingError "D is not an inert in the initial problem") in let conv = Util.filter_map ( function | #i_n_var as t -> Some t | `Lam _ -> None - | _ -> raise (ParsingError "A term in conv is not i_n_var") + | _ -> raise (ParsingError "A C-term is not i_n_var") ) conv in let ps = List.map ( function | #i_n_var as y -> y - | _ as y -> raise (ParsingError ("A term in num is not i_n_var" ^ Num.string_of_nf y)) + | _ -> raise (ParsingError "An N-term is not i_n_var") ) ps in name, div, conv, ps, free ;; -- 2.39.2