let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
+type options = { do_heavy_checks: bool ; include_paths: string list }
+
(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
* names as long as they are available, then it fallbacks to name generation
* using FreshNamesGenerator module *)
let status,obj = disambiguate_obj status obj in
status, TacticAst.Obj (loc,obj)
-let eval_command status cmd =
+let try_open_in paths path =
+ let rec aux = function
+ | [] -> open_in path
+ | p :: tl ->
+ try
+ open_in (p ^ "/" ^ path)
+ with Sys_error _ -> aux tl
+ in
+ try
+ aux paths
+ with Sys_error _ as exc ->
+ MatitaLog.error ("Unable to read " ^ path);
+ MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
+ raise exc
+;;
+
+let eval_command opts status cmd =
let status,cmd = disambiguate_command status cmd in
match cmd with
| TacticAst.Default (loc, what, uris) as cmd ->
(TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
| TacticAst.Include (loc, path) ->
let path = MatitaMisc.obj_file_of_script path in
- let stream = Stream.of_channel (open_in path) in
+ let stream = Stream.of_channel (try_open_in opts.include_paths path) in
let status = ref status in
!eval_from_stream_ref status stream (fun _ _ -> ());
!status
in
let metasenv = MatitaMisc.get_proof_metasenv status in
match obj with
- Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
+ | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
let name = UriManager.name_of_uri uri in
if not(CicPp.check name ty) then
MatitaLog.warn ("Bad name: " ^ name);
+ if opts.do_heavy_checks then
+ begin
+ let dbd = MatitaDb.instance () in
+ let similar = MetadataQuery.match_term ~dbd ty in
+ let convertible =
+ List.filter (
+ fun u ->
+ let t = CicUtil.term_of_uri u in
+ let ty',g =
+ CicTypeChecker.type_of_aux'
+ metasenv' [] t CicUniv.empty_ugraph
+ in
+ fst(CicReduction.are_convertible [] ty' ty g))
+ similar
+ in
+ (match convertible with
+ | [] -> ()
+ | x::_ ->
+ MatitaLog.warn
+ ("Theorem already proved: " ^ UriManager.string_of_uri x ^
+ "\nPlease use a variant."));
+ end;
assert (metasenv = metasenv');
let goalno =
- match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in
+ match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false
+ in
let initial_proof = (Some uri, metasenv, bo, ty) in
- { status with proof_status = Incomplete_proof (initial_proof,goalno)}
- | _ ->
- if metasenv <> [] then
- command_error (
- "metasenv not empty while giving a definition with body: " ^
- CicMetaSubst.ppmetasenv metasenv []);
- let status = MatitaSync.add_obj uri obj status in
- match obj with
- Cic.Constant _ -> status
- | Cic.InductiveDefinition (_,_,_,attrs) ->
- let status = generate_elimination_principles uri status in
- let rec get_record_attrs =
- function
- [] -> None
- | (`Class (`Record fields))::_ -> Some fields
- | _::tl -> get_record_attrs tl
- in
- (match get_record_attrs attrs with
- None -> status (* not a record *)
- | Some fields -> generate_projections uri fields status)
- | Cic.CurrentProof _
- | Cic.Variable _ -> assert false
+ { status with proof_status = Incomplete_proof (initial_proof,goalno)}
+ | _ ->
+ if metasenv <> [] then
+ command_error (
+ "metasenv not empty while giving a definition with body: " ^
+ CicMetaSubst.ppmetasenv metasenv []);
+ let status = MatitaSync.add_obj uri obj status in
+ match obj with
+ Cic.Constant _ -> status
+ | Cic.InductiveDefinition (_,_,_,attrs) ->
+ let status = generate_elimination_principles uri status in
+ let rec get_record_attrs =
+ function
+ [] -> None
+ | (`Class (`Record fields))::_ -> Some fields
+ | _::tl -> get_record_attrs tl
+ in
+ (match get_record_attrs attrs with
+ None -> status (* not a record *)
+ | Some fields -> generate_projections uri fields status)
+ | Cic.CurrentProof _
+ | Cic.Variable _ -> assert false
-let eval_executable status ex =
+let eval_executable opts status ex =
match ex with
| TacticAst.Tactical (_, tac) -> eval_tactical status tac
- | TacticAst.Command (_, cmd) -> eval_command status cmd
+ | TacticAst.Command (_, cmd) -> eval_command opts status cmd
| TacticAst.Macro (_, mac) ->
command_error (sprintf "The macro %s can't be in a script"
(TacticAstPp.pp_macro_ast mac))
let eval_comment status c = status
-let eval_ast status st =
+
+let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st =
+ let opts =
+ {do_heavy_checks = do_heavy_checks ; include_paths = include_paths}
+ in
match st with
- | TacticAst.Executable (_,ex) -> eval_executable status ex
+ | TacticAst.Executable (_,ex) -> eval_executable opts status ex
| TacticAst.Comment (_,c) -> eval_comment status c
-let eval_from_stream status str cb =
+let eval_from_stream ?do_heavy_checks ?include_paths status str cb =
let stl = CicTextualParser2.parse_statements str in
List.iter
- (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+ (fun ast ->
+ cb !status ast;
+ status := eval_ast ?do_heavy_checks ?include_paths !status ast)
+ stl
;;
(* to avoid a long list of recursive functions *)
eval_from_stream_ref := eval_from_stream;;
-let eval_from_stream_greedy status str cb =
+let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb =
while true do
print_string "matita> ";
flush stdout;
let ast = CicTextualParser2.parse_statement str in
cb !status ast;
- status := eval_ast !status ast
+ status := eval_ast ?do_heavy_checks ?include_paths !status ast
done
;;
-let eval_string status str =
- eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
+let eval_string ?do_heavy_checks ?include_paths status str =
+ eval_from_stream
+ ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->())
let default_options () =
(*
*)
let options =
StringMap.add "basedir"
- (String (Helm_registry.get "matita.basedir" ))
+ (String (Helm_registry.get "matita.basedir"))
no_options
in
options
projects / helm.git / blobdiff