diff options
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 154 |
1 files changed, 88 insertions, 66 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 4afc02f9..ffe15531 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -1,21 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp +open Errors open Util open System open Flags open Names -open Term open Check -let coq_root = id_of_string "Coq" +let () = at_exit flush_all + +let fatal_error info anomaly = + flush_all (); pperrnl info; flush_all (); + exit (if anomaly then 129 else 1) + +let coq_root = Id.of_string "Coq" let parse_dir s = let len = String.length s in let rec decoupe_dirs dirs n = @@ -32,27 +37,27 @@ let parse_dir s = let dirpath_of_string s = match parse_dir s with [] -> Check.default_root_prefix - | dir -> make_dirpath (List.map id_of_string dir) + | dir -> DirPath.make (List.map Id.of_string dir) let path_of_string s = match parse_dir s with [] -> invalid_arg "path_of_string" | l::dir -> {dirpath=dir; basename=l} -let (/) = Filename.concat +let ( / ) = Filename.concat let get_version_date () = try - let coqlib = Envars.coqlib () in - let ch = open_in (Filename.concat coqlib "revision") in + let ch = open_in (Envars.coqlib () / "revision") in let ver = input_line ch in let rev = input_line ch in - (ver,rev) + let () = close_in ch in + (ver,rev) with _ -> (Coq_config.version,Coq_config.date) let print_header () = let (ver,rev) = (get_version_date ()) in - Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; - flush stdout + Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; + flush stdout (* Adding files to Coq loadpath *) @@ -65,20 +70,23 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = msg_warning (str ("Cannot open " ^ dir)) let convert_string d = - try id_of_string d - with _ -> - if_verbose warning - ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); - flush_all (); - failwith "caught" + try Id.of_string d + with Errors.UserError _ -> + if_verbose msg_warning + (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + raise Exit let add_rec_path ~unix_path ~coq_root = if exists_dir unix_path then let dirs = all_subdirs ~unix_path in - let prefix = repr_dirpath coq_root in - let convert_dirs (lp,cp) = - (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in - let dirs = map_succeed convert_dirs dirs in + let prefix = DirPath.repr coq_root in + let convert_dirs (lp, cp) = + try + let path = List.rev_map convert_string cp @ prefix in + Some (lp, Names.DirPath.make path) + with Exit -> None + in + let dirs = List.map_filter convert_dirs dirs in List.iter Check.add_load_path dirs; Check.add_load_path (unix_path, coq_root) else @@ -107,14 +115,15 @@ let init_load_path () = let plugins = coqlib/"plugins" in (* NOTE: These directories are searched from last to first *) (* first standard library *) - add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]); + add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]); (* then plugins *) - add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]); + add_rec_path ~unix_path:plugins ~coq_root:(Names.DirPath.make [coq_root]); (* then user-contrib *) if Sys.file_exists user_contrib then add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) - List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) xdg_dirs; + List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) + (xdg_dirs ~warn:(fun x -> msg_warning (str x))); (* then directories in COQPATH *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) @@ -208,10 +217,10 @@ let anomaly_string () = str "Anomaly: " let report () = (str "." ++ spc () ++ str "Please report.") let print_loc loc = - if loc = dummy_loc then + if loc = Loc.ghost then (str"<unknown>") else - let loc = unloc loc in + let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = "\""^s^"\"" @@ -223,8 +232,6 @@ let rec explain_exn = function hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) - | Token.Error txt -> - hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() ) | UserError(s,pps) -> @@ -233,8 +240,6 @@ let rec explain_exn = function hov 0 (str "Out of memory") | Stack_overflow -> hov 0 (str "Stack overflow") - | Anomaly (s,pps) -> - hov 1 (anomaly_string () ++ where s ++ pps ++ report ()) | Match_failure(filename,pos1,pos2) -> hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ str " at line " ++ int pos1 ++ @@ -250,26 +255,57 @@ let rec explain_exn = function | Univ.UniverseInconsistency (o,u,v) -> let msg = if !Flags.debug (*!Constrextern.print_universes*) then - spc() ++ str "(cannot enforce" ++ spc() ++ (*Univ.pr_uni u ++*) spc() ++ + spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++ str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=") - ++ spc() ++ (*Univ.pr_uni v ++*) str")" + ++ spc() ++ Univ.pr_uni v ++ str")" else mt() in hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> -(* hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx *) - (* te)*) - hov 0 (str "Type error") + hov 0 (str "Type error: " ++ + (match te with + | UnboundRel i -> str"UnboundRel " ++ int i + | UnboundVar v -> str"UnboundVar" ++ str(Names.Id.to_string v) + | NotAType _ -> str"NotAType" + | BadAssumption _ -> str"BadAssumption" + | ReferenceVariables _ -> str"ReferenceVariables" + | ElimArity _ -> str"ElimArity" + | CaseNotInductive _ -> str"CaseNotInductive" + | WrongCaseInfo _ -> str"WrongCaseInfo" + | NumberBranches _ -> str"NumberBranches" + | IllFormedBranch _ -> str"IllFormedBranch" + | Generalization _ -> str"Generalization" + | ActualType _ -> str"ActualType" + | CantApplyBadType ((n,a,b),(hd,hdty),args) -> + Format.printf "====== ill-typed term ====@\n"; + Format.printf "@[<hov 2>application head=@ "; + Print.print_pure_constr hd; + Format.printf "@]@\n@[<hov 2>head type=@ "; + Print.print_pure_constr hdty; + Format.printf "@]@\narguments:@\n@[<hv>"; + Array.iteri (fun i (t,ty) -> + Format.printf "@[<hov 2>arg %d=@ " (i+1); + Print.print_pure_constr t; + Format.printf "@ type=@ "; + Print.print_pure_constr ty) args; + Format.printf "@]@\n====== type error ====@\n"; + Print.print_pure_constr b; + Format.printf "@\nis not convertible with@\n"; + Print.print_pure_constr a; + Format.printf "@\n====== universes ====@\n"; + Pp.pp (Univ.pr_universes + (ctx.Environ.env_stratification.Environ.env_universes)); + str("\nCantApplyBadType at argument " ^ string_of_int n) + | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" + | IllFormedRecBody _ -> str"IllFormedRecBody" + | IllTypedRecBody _ -> str"IllTypedRecBody" + | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints")) | Indtypes.InductiveError e -> hov 0 (str "Error related to inductive types") (* let ctx = Check.get_env() in hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*) - | Loc.Exc_located (loc,exc) -> - hov 0 ((if loc = dummy_loc then (mt ()) - else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) - ++ explain_exn exc) | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s = "" then mt () @@ -278,19 +314,17 @@ let rec explain_exn = function str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report ()) - | reraise -> - hov 0 (anomaly_string () ++ str "Uncaught exception " ++ - str (Printexc.to_string reraise)++report()) + | e -> Errors.print e (* for anomalies and other uncaught exceptions *) let parse_args argv = let rec parse = function | [] -> () | "-impredicative-set" :: rem -> - set_engagement Declarations.ImpredicativeSet; parse rem + set_engagement Cic.ImpredicativeSet; parse rem | "-coqlib" :: s :: rem -> if not (exists_dir s) then - (msgnl (str ("Directory '"^s^"' does not exist")); exit 1); + fatal_error (str ("Directory '"^s^"' does not exist")) false; Flags.coqlib := s; Flags.coqlib_spec := true; parse rem @@ -308,7 +342,9 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - print_endline (Envars.coqlib ()); exit 0 + Envars.set_coqlib ~fail:Errors.error; + print_endline (Envars.coqlib ()); + exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () @@ -318,8 +354,6 @@ let parse_args argv = | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem - | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem - | "-admit" :: s :: rem -> add_admit s; parse rem | "-admit" :: [] -> usage () @@ -330,19 +364,10 @@ let parse_args argv = Flags.make_silent true; parse rem | s :: _ when s<>"" && s.[0]='-' -> - msgnl (str "Unknown option " ++ str s); exit 1 + fatal_error (str "Unknown option " ++ str s) false | s :: rem -> add_compile s; parse rem in - try - parse (List.tl (Array.to_list argv)) - with - | UserError(_,s) as e -> begin - try - Stream.empty s; exit 1 - with Stream.Failure -> - msgnl (explain_exn e); exit 1 - end - | e -> begin msgnl (explain_exn e); exit 1 end + parse (List.tl (Array.to_list argv)) (* To prevent from doing the initialization twice *) @@ -354,14 +379,13 @@ let init_with_argv argv = Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) try parse_args argv; + if !Flags.debug then Printexc.record_backtrace true; + Envars.set_coqlib ~fail:Errors.error; if_verbose print_header (); init_load_path (); engage (); with e -> - flush_all(); - message "Error during initialization :"; - msgnl (explain_exn e); - exit 1 + fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e) end let init() = init_with_argv Sys.argv @@ -371,9 +395,7 @@ let run () = compile_files (); flush_all() with e -> - (flush_all(); - Pp.ppnl(explain_exn e); - flush_all(); - exit 1) + if !Flags.debug then Printexc.print_backtrace stderr; + fatal_error (explain_exn e) (is_anomaly e) let start () = init(); run(); Check_stat.stats(); exit 0 |