(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'
- in
- ProofEngineTypes.mk_tactic aux
+ 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 =
let andelim = existselim;;
-let rewritingstep ~dbd lhs rhs just conclude =
+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 just =
match just with
None ->
- Tactics.auto ~dbd
- ~params:["paramodulation","on"; "timeout","3"]
- | Some just -> Tactics.apply just
+ Tactics.auto ~dbd ~params:["paramodulation","1"; "timeout","3"] ~universe
+ | Some just -> Tactics.apply just
in
match lhs with
None ->
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
- just]) status
+ Tacticals.then_
+ ~start:(Tactics.clear ~hyps:[last_hyp_name])
+ ~continuation:just]) status
| Some name ->
let mk_fresh_name_callback =
fun metasenv context _ ~typ ->
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
- just]
+ Tacticals.then_
+ ~start:(Tactics.clear ~hyps:[last_hyp_name])
+ ~continuation:just]
]) status)
| Some lhs ->
match conclude with
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)
;;