From cf5b84fca20d90722298e9a5f5399ff15a3bc1d4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 11 Jul 2005 14:08:33 +0000 Subject: [PATCH] added a flag to do the check of alredy-proved-theorem --- helm/matita/matitaEngine.ml | 96 +++++++++++++++++++++++------------- helm/matita/matitaEngine.mli | 9 +++- helm/matita/matitaScript.ml | 5 +- 3 files changed, 72 insertions(+), 38 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index c5b2fb987..53772ccf2 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -443,7 +443,7 @@ let disambiguate_command status = function let status,obj = disambiguate_obj status obj in status, TacticAst.Obj (loc,obj) -let eval_command status cmd = +let eval_command do_heavy_checks status cmd = let status,cmd = disambiguate_command status cmd in match cmd with | TacticAst.Default (loc, what, uris) as cmd -> @@ -521,73 +521,99 @@ let eval_command status cmd = 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 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 do_heavy_checks status ex = match ex with | TacticAst.Tactical (_, tac) -> eval_tactical status tac - | TacticAst.Command (_, cmd) -> eval_command status cmd + | TacticAst.Command (_, cmd) -> eval_command do_heavy_checks 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) status st = match st with - | TacticAst.Executable (_,ex) -> eval_executable status ex + | TacticAst.Executable (_,ex) -> eval_executable do_heavy_checks status ex | TacticAst.Comment (_,c) -> eval_comment status c -let eval_from_stream status str cb = +let eval_from_stream ?do_heavy_checks 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 !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 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 !status ast done ;; -let eval_string status str = - eval_from_stream status (Stream.of_string str) (fun _ _ -> ()) +let eval_string ?do_heavy_checks status str = + eval_from_stream + ?do_heavy_checks status (Stream.of_string str) (fun _ _ -> ()) let default_options () = (* diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 9311215f3..05092770b 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -25,21 +25,28 @@ exception Drop -val eval_string: MatitaTypes.status ref -> string -> unit +(* heavy checks slow down the compilation process but give you some interesting + * infos like if the theorem is a duplicate *) +val eval_string: + ?do_heavy_checks:bool -> + MatitaTypes.status ref -> string -> unit val eval_from_stream: + ?do_heavy_checks:bool -> MatitaTypes.status ref -> char Stream.t -> (MatitaTypes.status -> (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> unit val eval_from_stream_greedy: + ?do_heavy_checks:bool -> MatitaTypes.status ref-> char Stream.t -> (MatitaTypes.status -> (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> unit val eval_ast: + ?do_heavy_checks:bool -> MatitaTypes.status -> (CicAst.term,TacticAst.obj,string) TacticAst.statement -> MatitaTypes.status diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index ce613ef71..7aa31d33b 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -77,10 +77,11 @@ let eval_with_engine status user_goal parsed_text st = match status.proof_status with | Incomplete_proof (_, goal) when goal <> user_goal -> goal_changed := true; - MatitaEngine.eval_ast status (goal_ast user_goal) + MatitaEngine.eval_ast + ~do_heavy_checks:true status (goal_ast user_goal) | _ -> status in - let new_status = MatitaEngine.eval_ast status st in + let new_status = MatitaEngine.eval_ast ~do_heavy_checks:true status st in let new_aliases = match ex with | TA.Command (_, TA.Alias _) -- 2.39.2