X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=24801542dabcb76f57a6684a6d60fccaef31a488;hb=66929b8edb58d468a134b648466f3e9c45ba5c0e;hp=4a7d3e52c6329263d838cf063b6aa9020743d051;hpb=d348c454be6bae89169ed2948067e62e33f62bd8;p=helm.git diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 4a7d3e52c..24801542d 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -45,79 +45,118 @@ let suppose t id ty = (fun _ metasenv ugraph -> ty,metasenv,ugraph)) ;; -let by_term_we_proved ~dbd t ty id ty' = +let by_term_we_proved ~dbd ~universe t ty id ty' = let just = match t with - None -> Tactics.auto ~dbd ~params:[] + None -> Tactics.auto ~dbd ~params:[] ~universe | Some t -> Tactics.apply t in - let continuation = - match ty' with - None -> Tacticals.id_tac - | Some ty' -> - Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) - (fun _ metasenv ugraph -> ty,metasenv,ugraph) - in - Tacticals.thens - ~start: - (Tactics.cut ty - ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) - ~continuations:[ continuation ; just ] + match id with + None -> + (match ty' with + None -> assert false + | Some ty' -> + Tacticals.then_ + ~start:(Tactics.change + ~pattern:(ProofEngineTypes.conclusion_pattern None) + (fun _ metasenv ugraph -> ty,metasenv,ugraph)) + ~continuation:just + ) + | Some id -> + let continuation = + match ty' with + None -> Tacticals.id_tac + | Some ty' -> + Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> ty',metasenv,ugraph) + in + Tacticals.thens + ~start: + (Tactics.cut ty + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) + ~continuations:[ continuation ; just ] ;; -let bydone ~dbd t = +let bydone ~dbd ~universe t = let just = match t with - None -> Tactics.auto ~dbd ~params:[] + None -> Tactics.auto ~dbd ~params:[] ~universe | Some t -> Tactics.apply t in just ;; let we_need_to_prove t id ty = - let aux status = - let cont,cutted = - match ty with - None -> Tacticals.id_tac,t - | Some ty -> - Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) - (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in - let proof,goals = - ProofEngineTypes.apply_tactic - (Tacticals.thens - ~start: - (Tactics.cut cutted - ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) - ~continuations:[cont]) - status - in - let goals' = - match goals with - [fst; snd] -> [snd; fst] - | _ -> assert false - in - proof,goals' + match id with + None -> + (match ty with + None -> Tacticals.id_tac (*BUG: check missing here *) + | Some ty -> + Tactics.change ~pattern:(ProofEngineTypes.conclusion_pattern None) + (fun _ metasenv ugraph -> ty,metasenv,ugraph)) + | Some id -> + let aux status = + let cont,cutted = + match ty with + None -> Tacticals.id_tac,t + | Some ty -> + Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in + let proof,goals = + ProofEngineTypes.apply_tactic + (Tacticals.thens + ~start: + (Tactics.cut cutted + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) + ~continuations:[cont]) + status + in + let goals' = + match goals with + [fst; snd] -> [snd; fst] + | _ -> assert false + in + proof,goals' + in + ProofEngineTypes.mk_tactic aux +;; + +let existselim ~dbd ~universe t id1 t1 id2 t2 = + let aux (proof, goal) = + let (n,metasenv,_subst,bo,ty,attrs) = proof in + let metano,context,_ = CicUtil.lookup_meta goal metasenv in + let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in + let proof' = (n,metasenv,_subst,bo,ty,attrs) in + ProofEngineTypes.apply_tactic ( + Tacticals.thens + ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)])) + ~continuations: + [ Tactics.elim_intros (Cic.Rel 1) + ~mk_fresh_name_callback: + (let i = ref 0 in + fun _ _ _ ~typ -> + incr i; + if !i = 1 then Cic.Name id1 else Cic.Name id2) ; + (match t with + None -> Tactics.auto ~dbd ~params:[] ~universe + | Some t -> Tactics.apply t) + ]) (proof', goal) in ProofEngineTypes.mk_tactic aux ;; -let existselim t id1 t1 id2 t2 = -(*BUG: t1 and t2 not used *) -(*PARSING BUG: t2 is parsed in the current context, but it may - have occurrences of id1 in it *) +let andelim t id1 t1 id2 t2 = Tactics.elim_intros t - ~mk_fresh_name_callback: - (let i = ref 0 in - fun _ _ _ ~typ -> - incr i; - if !i = 1 then Cic.Name id1 else Cic.Name id2) + ~mk_fresh_name_callback: + (let i = ref 0 in + fun _ _ _ ~typ -> + incr i; + if !i = 1 then Cic.Name id1 else Cic.Name id2) -let andelim = existselim;; - -let rewritingstep ~dbd lhs rhs just conclude = +let rewritingstep ~dbd ~universe lhs rhs just last_step = let aux ((proof,goal) as status) = - let (curi,metasenv,proofbo,proofty) = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in + let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in + let _,context,gty = CicUtil.lookup_meta goal metasenv in let eq,trans = match LibraryObjects.eq_URI () with None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command")) @@ -128,76 +167,105 @@ let rewritingstep ~dbd lhs rhs just conclude = CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in let just = match just with - None -> - Tactics.auto ~dbd - ~params:["paramodulation","on"; "timeout","3"] - | Some just -> Tactics.apply just + `Auto params -> + let params = + if not (List.exists (fun (k,_) -> k = "timeout") params) then + ("timeout","3")::params + else params + in + let params' = + if not (List.exists (fun (k,_) -> k = "paramodulation") params) then + ("paramodulation","1")::params + else params + in + if params = params' then + Tactics.auto ~dbd ~params ~universe + else + Tacticals.first + [Tactics.auto ~dbd ~params ~universe ; + Tactics.auto ~dbd ~params:params' ~universe] + | `Term just -> + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context just + CicUniv.empty_ugraph + in + Tactics.solve_rewrite + ~universe:(Universe.index Universe.empty + (Universe.key ty) just) ~steps:1 () + (* Tactics.apply just *) in - match lhs with - None -> - let plhs,prhs = - match - fst - (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1) - CicUniv.empty_ugraph) - with - Cic.Appl [_;_;plhs;prhs] -> plhs,prhs - | _ -> assert false in - let last_hyp_name = - match context with - (Some (Cic.Name id,_))::_ -> id - | _ -> assert false - in - (match conclude with - None -> - ProofEngineTypes.apply_tactic - (Tacticals.thens - ~start:(Tactics.apply ~term:trans) - ~continuations: - [ Tactics.apply prhs ; - Tactics.apply (Cic.Rel 1) ; - just]) status - | Some name -> - let mk_fresh_name_callback = - fun metasenv context _ ~typ -> - FreshNamesGenerator.mk_fresh_name ~subst:[] - metasenv context name ~typ - in - ProofEngineTypes.apply_tactic - (Tacticals.thens - ~start:(Tactics.cut ~mk_fresh_name_callback - (Cic.Appl [eq ; ty ; plhs ; rhs])) - ~continuations: - [ Tactics.clear ~hyps:[last_hyp_name] ; - Tacticals.thens - ~start:(Tactics.apply ~term:trans) - ~continuations: - [ Tactics.apply prhs ; - Tactics.apply (Cic.Rel 1) ; - just] - ]) status) - | Some lhs -> - match conclude with - None -> ProofEngineTypes.apply_tactic just status - | Some name -> + let plhs,prhs,prepare = + match lhs with + None -> + let plhs,prhs = + match gty with + Cic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> assert false + in + plhs,prhs, + (fun continuation -> + ProofEngineTypes.apply_tactic continuation status) + | Some (None,lhs) -> + let plhs,prhs = + match gty with + Cic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> assert false + in + (*CSC: manca check plhs convertibile con lhs *) + plhs,prhs, + (fun continuation -> + ProofEngineTypes.apply_tactic continuation status) + | Some (Some name,lhs) -> + let newmeta = CicMkImplicit.new_meta metasenv [] in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let plhs = lhs in + let prhs = Cic.Meta(newmeta,irl) in + plhs,prhs, + (fun continuation -> + let metasenv = (newmeta, context, ty)::metasenv in let mk_fresh_name_callback = - fun metasenv context _ ~typ -> - FreshNamesGenerator.mk_fresh_name ~subst:[] - metasenv context name ~typ + fun metasenv context _ ~typ -> + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context + (Cic.Name name) ~typ in + let proof = curi,metasenv,_subst,proofbo,proofty, attrs in + let proof,goals = ProofEngineTypes.apply_tactic (Tacticals.thens - ~start: - (Tactics.cut ~mk_fresh_name_callback - (Cic.Appl [eq ; ty ; lhs ; rhs])) - ~continuations:[ Tacticals.id_tac ; just ]) status + ~start:(Tactics.cut ~mk_fresh_name_callback + (Cic.Appl [eq ; ty ; lhs ; prhs])) + ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal) + in + let goals = + match goals with + [g1;g2] -> [g2;newmeta;g1] + | _ -> assert false + in + proof,goals) + in + let continuation = + if last_step then + (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*) + just + else + Tacticals.thens + ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs])) + ~continuations:[just ; Tacticals.id_tac] + in + prepare continuation in ProofEngineTypes.mk_tactic aux ;; -let we_proceed_by_induction_on t pat = +let we_proceed_by_cases_on t pat = (*BUG here: pat unused *) - Tactics.elim_intros ~depth:0 t + Tactics.cases_intros t +;; + +let we_proceed_by_induction_on t pat = + let pattern = None, [], Some pat in + Tactics.elim_intros ~depth:0 (*~pattern*) t ;; let case id ~params = @@ -218,10 +286,12 @@ let case id ~params = let thesisbecomes t = let ty = None in - (*BUG here: missing check on t *) match ty with - None -> Tacticals.id_tac + None -> + Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole))) + (fun _ metasenv ugraph -> t,metasenv,ugraph) | Some ty -> + (*BUG here: missing check on t *) Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole))) (fun _ metasenv ugraph -> ty,metasenv,ugraph) ;;