X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=7e276a8bcef73f63b273e9ed00ae3f61541f7d09;hb=403b7486e9f2cb5583a2c8035cf419bbac982fb1;hp=1604d92d8029af62abb68fb4f79b0121bd97311a;hpb=4f12c6bc7fb5f1ba3bd42f78abddb77b3b0a8f93;p=helm.git diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 1604d92d8..7e276a8bc 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -34,62 +34,230 @@ let assume id t = ;; let suppose t id ty = +(*BUG: check on t missing *) + let ty = match ty with None -> t | Some ty -> ty in Tacticals.then_ ~start: - (Tactics.intros ~howmany:1 - ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ()) + (Tactics.intros ~howmany:1 + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ()) ~continuation: - (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) - (fun _ metasenv ugraph -> t,metasenv,ugraph)) + (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> ty,metasenv,ugraph)) ;; -let by_term_we_proved t ty id ty' = - match t with - None -> assert false - | Some t -> - Tacticals.thens - ~start: - (Tactics.cut ty - ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) - ~continuations: - [ Tacticals.id_tac ; Tactics.apply t ] +let by_term_we_proved ~dbd ~universe t ty id ty' = + let just = + match t with + None -> Tactics.auto ~dbd ~params:[] ~universe + | Some t -> Tactics.apply t + in + 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 t = - match t with - None -> assert false - | Some t -> - (Tactics.apply ~term:t) +let bydone ~dbd ~universe t = + let just = + match t with + 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 proof,goals = - ProofEngineTypes.apply_tactic - (Tactics.cut t - ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) - status + 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 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 *) + 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) + +let andelim = existselim;; + +let rewritingstep ~dbd ~universe lhs rhs just conclude = + let aux ((proof,goal) as status) = + let (curi,metasenv,proofbo,proofty) = proof in + let _,context,_ = 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")) + | Some uri -> + Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[]) in - let goals' = - match goals with - [fst; snd] -> [snd; fst] - | _ -> assert false - in - proof,goals' + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in + let just = + match just with + `Auto params -> + let params = + if not (List.exists (fun (k,_) -> k = "paramodulation") params) then + ("paramodulation","1")::params + else params in + let params = + if not (List.exists (fun (k,_) -> k = "timeout") params) then + ("timeout","3")::params + else params + in + Tactics.auto ~dbd ~params ~universe + | `Term just -> 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) ; + Tacticals.then_ + ~start:(Tactics.clear ~hyps:[last_hyp_name]) + ~continuation: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) ; + Tacticals.then_ + ~start:(Tactics.clear ~hyps:[last_hyp_name]) + ~continuation:just] + ]) status) + | Some lhs -> + match conclude with + None -> ProofEngineTypes.apply_tactic 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 ; lhs ; rhs])) + ~continuations:[ Tacticals.id_tac ; just ]) status in ProofEngineTypes.mk_tactic aux ;; -let prova _ = assert false -;; -let bywehave _ = assert false -;; -let case _ = assert false -;; -let thesisbecomes _ = assert false +let we_proceed_by_induction_on t pat = + (*BUG here: pat unused *) + Tactics.elim_intros ~depth:0 t ;; -let byinduction _ = assert false + +let case id ~params = + (*BUG here: id unused*) + (*BUG here: it does not verify that the previous branch is closed *) + (*BUG here: the params should be parsed telescopically*) + (*BUG here: the tactic_terms should be terms*) + let rec aux ~params ((proof,goal) as status) = + match params with + [] -> proof,[goal] + | (id,t)::tl -> + match ProofEngineTypes.apply_tactic (assume id t) status with + proof,[goal] -> aux tl (proof,goal) + | _ -> assert false + in + ProofEngineTypes.mk_tactic (aux ~params) ;; -let we_proceed_by_induction_on _ = assert false + +let thesisbecomes t = +let ty = None in + match ty with + 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) ;; -let let1 _ = assert false + +let byinduction t id = suppose t id None;;