X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=0cfd8f07cfe620ed9e2fe58438b6c7d97744b5c6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0885f3037ffdcc1dfb9493ec1214f22f09b77022;hpb=d7a329578a475af98aa5f2a16d9873a576dab599;p=helm.git diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 0885f3037..0cfd8f07c 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -31,21 +31,49 @@ open ProofEngineTypes let proof = ref (None : proof option) let goal = ref (None : goal option) -let apply_tactic ~tactic:tactic = - match !proof,!goal with - None,_ +let get_proof () = !proof;; +let set_proof p = proof := p;; + +let get_current_status_as_xml () = + match get_proof () with + None -> assert false + | Some (uri, metasenv, bo, ty) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let currentproof = + (*CSC: Wrong: [] is just plainly wrong *) + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]) + in + let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = + Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof + in + let xml, bodyxml = + match + Cic2Xml.print_object uri ~ids_to_inner_sorts + ~ask_dtd_to_the_getter:true acurrentproof + with + xml,Some bodyxml -> xml,bodyxml + | _,None -> assert false + in + (xml, bodyxml) +;; + +let apply_tactic ~tactic = + let module PET = ProofEngineTypes in + match get_proof (),!goal with + | None,_ | _,None -> assert false | Some proof', Some goal' -> - let (newproof, newgoals) = tactic ~status:(proof', goal') in - proof := Some newproof; - goal := - (match newgoals, newproof with - goal::_, _ -> Some goal - | [], (_,(goal,_,_)::_,_,_) -> - (* the tactic left no open goal ; let's choose the first open goal *) -(*CSC: here we could implement and use a proof-tree like notion... *) - Some goal - | _, _ -> None) + let (newproof, newgoals) = PET.apply_tactic tactic (proof', goal') in + set_proof (Some newproof); + goal := + (match newgoals, newproof with + goal::_, _ -> Some goal + | [], (_,(goal,_,_)::_,_,_) -> + (* the tactic left no open goal ; let's choose the first open goal *) + (*CSC: here we could implement and use a proof-tree like notion... *) + Some goal + | _, _ -> None) +;; (* metas_in_term term *) (* Returns the ordered list of the metas that occur in [term]. *) @@ -54,25 +82,26 @@ let metas_in_term term = let module C = Cic in let rec aux = function - C.Rel _ - | C.Var _ -> [] + C.Rel _ -> [] | C.Meta (n,_) -> [n] | C.Sort _ - | C.Implicit -> [] + | C.Implicit _ -> [] | C.Cast (te,ty) -> (aux te) @ (aux ty) | C.Prod (_,s,t) -> (aux s) @ (aux t) | C.Lambda (_,s,t) -> (aux s) @ (aux t) | C.LetIn (_,s,t) -> (aux s) @ (aux t) | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l - | C.Const _ - | C.MutInd _ - | C.MutConstruct _ -> [] - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + | C.Var (_,exp_named_subst) + | C.Const (_,exp_named_subst) + | C.MutInd (_,_,exp_named_subst) + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.fold_left (fun i (_,t) -> i @ (aux t)) [] exp_named_subst + | C.MutCase (_,_,outt,t,pl) -> (aux outt) @ (aux t) @ (List.fold_left (fun i t -> i @ (aux t)) [] pl) - | C.Fix (i,fl) -> + | C.Fix (_,fl) -> List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl - | C.CoFix (i,fl) -> + | C.CoFix (_,fl) -> List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl in let metas = aux term in @@ -91,17 +120,19 @@ let metas_in_term term = (* are efficiency reasons. *) let perforate context term ty = let module C = Cic in - match !proof with + match get_proof () with None -> assert false | Some (uri,metasenv,bo,gty as proof') -> - let newmeta = new_meta proof' in + let newmeta = new_meta_of_proof proof' in (* We push the new meta at the end of the list for pretty-printing *) (* purposes: in this way metas are ordered. *) let metasenv' = metasenv@[newmeta,context,ty] in - let irl = identity_relocation_list_for_metavariable context in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*) let bo' = - ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo + ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo in (* It may be possible that some metavariables occurred only in *) (* the term we are perforating and they now occurs no more. We *) @@ -113,7 +144,7 @@ let perforate context term ty = let metasenv'' = List.filter (function (n,_,_) -> List.mem n newmetas) metasenv' in - proof := Some (uri,metasenv'',bo',gty) ; + set_proof (Some (uri,metasenv'',bo',gty)) ; goal := Some newmeta @@ -121,68 +152,10 @@ let perforate context term ty = (* Some easy tactics. *) (************************************************************) -(*CSC: generatore di nomi? Chiedere il nome? *) -let fresh_name = - let next_fresh_index = ref 0 -in - function () -> - incr next_fresh_index ; - "fresh_name" ^ string_of_int !next_fresh_index - -let reduction_tactic reduction_function term = - let curi,metasenv,pbo,pty = - match !proof with - None -> assert false - | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty - in - let metano,context,ty = - match !goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - (* We don't know if [term] is a subterm of [ty] or a subterm of *) - (* the type of one metavariable. So we replace it everywhere. *) - (*CSC: Il vero problema e' che non sapendo dove sia il term non *) - (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) - (*CSC: e' meglio prima cercare il termine e scoprirne il *) - (*CSC: contesto, poi ridurre e infine rimpiazzare. *) - let replace context where= -(*CSC: Per il momento se la riduzione fallisce significa solamente che *) -(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) -(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) - try - let term' = reduction_function context term in - ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' - ~where:where - with - _ -> where - in - let ty' = replace context ty in - let context' = - List.fold_right - (fun entry context -> - match entry with - Some (name,Cic.Def t) -> - (Some (name,Cic.Def (replace context t)))::context - | Some (name,Cic.Decl t) -> - (Some (name,Cic.Decl (replace context t)))::context - | None -> None::context - ) context [] - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some metano - (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) -let reduction_tactic_in_scratch reduction_function term ty = +let reduction_tactic_in_scratch reduction_function terms ty = let metasenv = - match !proof with + match get_proof () with None -> [] | Some (_,metasenv,_,_) -> metasenv in @@ -191,60 +164,14 @@ let reduction_tactic_in_scratch reduction_function term ty = None -> assert false | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in - let term' = reduction_function context term in + let terms' = List.map (reduction_function context) terms in ProofEngineReduction.replace - ~equality:(==) ~what:term ~with_what:term' ~where:ty - -let whd = reduction_tactic CicReduction.whd -let reduce = reduction_tactic ProofEngineReduction.reduce -let simpl = reduction_tactic ProofEngineReduction.simpl + ~equality:(==) ~what:terms ~with_what:terms' ~where:ty +;; let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd -let reduce_in_scratch = - reduction_tactic_in_scratch ProofEngineReduction.reduce -let simpl_in_scratch = - reduction_tactic_in_scratch ProofEngineReduction.simpl - -(* It is just the opposite of whd. The code should probably be merged. *) -let fold term = - let curi,metasenv,pbo,pty = - match !proof with - None -> assert false - | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty - in - let metano,context,ty = - match !goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - let term' = CicReduction.whd context term in - (* We don't know if [term] is a subterm of [ty] or a subterm of *) - (* the type of one metavariable. So we replace it everywhere. *) - (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) - (*CSC: che si guadagni nulla in fatto di efficienza. *) - let replace = - ProofEngineReduction.replace - ~equality:(ProofEngineReduction.syntactic_equality) - ~what:term' ~with_what:term - in - let ty' = replace ty in - let context' = - List.map - (function - Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) - | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t)) - | None -> None - ) context - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some metano +let reduce_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.reduce +let simpl_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.simpl (************************************************************) (* Tactics defined elsewhere *) @@ -253,10 +180,12 @@ let fold term = (* primitive tactics *) let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term) -let intros () = - apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ())) -let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term) -let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term) +let intros ?mk_fresh_name_callback () = + apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ()) +let cut ?mk_fresh_name_callback term = + apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback ~term) +let letin ?mk_fresh_name_callback term = + apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback ~term) let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term) let elim_intros_simpl term = apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term) @@ -268,9 +197,72 @@ let change ~goal_input:what ~input:with_what = let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp) let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) + (* reduction tactics *) + +let whd terms = + apply_tactic + (ReductionTactics.whd_tac ~also_in_hypotheses:true ~terms:(Some terms)) +let reduce terms = + apply_tactic + (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~terms:(Some terms)) +let simpl terms = + apply_tactic + (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~terms:(Some terms)) + +let fold_whd term = + apply_tactic + (ReductionTactics.fold_tac ~reduction:CicReduction.whd + ~also_in_hypotheses:true ~term) +let fold_reduce term = + apply_tactic + (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce + ~also_in_hypotheses:true ~term) +let fold_simpl term = + apply_tactic + (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl + ~also_in_hypotheses:true ~term) + (* other tactics *) -let elim_type term = apply_tactic (Ring.elim_type_tac ~term) +let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term) let ring () = apply_tactic Ring.ring_tac let fourier () = apply_tactic FourierR.fourier_tac -let rewrite term = apply_tactic (FourierR.rewrite_tac ~term) + +(* let auto ~dbd () = apply_tactic (AutoTactic.auto_tac ~dbd) *) +let auto ~dbd () = apply_tactic (AutoTactic.auto_tac_new ~dbd) + + +let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term) +let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term) +let replace ~goal_input:what ~input:with_what = + apply_tactic (EqualityTactics.replace_tac ~what ~with_what) + +let reflexivity () = apply_tactic EqualityTactics.reflexivity_tac +let symmetry () = apply_tactic EqualityTactics.symmetry_tac +let transitivity term = apply_tactic (EqualityTactics.transitivity_tac ~term) + +let exists () = apply_tactic IntroductionTactics.exists_tac +let split () = apply_tactic IntroductionTactics.split_tac +let left () = apply_tactic IntroductionTactics.left_tac +let right () = apply_tactic IntroductionTactics.right_tac + +let assumption () = apply_tactic VariousTactics.assumption_tac + +let generalize ?mk_fresh_name_callback terms = + apply_tactic (VariousTactics.generalize_tac ?mk_fresh_name_callback terms) + +let absurd term = apply_tactic (NegationTactics.absurd_tac ~term) +let contradiction () = apply_tactic NegationTactics.contradiction_tac + +let decompose ~uris_choice_callback term = + apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term) + +let injection term = apply_tactic (DiscriminationTactics.injection_tac ~term) +let discriminate term = apply_tactic (DiscriminationTactics.discriminate_tac ~term) +let decide_equality () = apply_tactic DiscriminationTactics.decide_equality_tac +let compare term = apply_tactic (DiscriminationTactics.compare_tac ~term) + +(* +let prova_tatticali () = apply_tactic Tacticals.prova_tac +*) +