* http://cs.unibo.it/helm/.
*)
+open HelmLibraryObjects
-let rec injection_tac ~term ~status:((proof, goal) as status) =
+let rec injection_tac ~term status =
+ let (proof, goal) = status in
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
(match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI) -> (
match tty with
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
| _ -> raise (ProofEngineTypes.Fail "Injection: not a projectable equality")
)
| _ -> raise (ProofEngineTypes.Fail "Injection: not an equation")
- ) ~status
+ ) status
-and injection1_tac ~term ~i ~status:((proof, goal) as status) =
+and injection1_tac ~term ~i status =
+let (proof, goal) = status in
(* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *)
let module C = Cic in
let module S = CicSubstitution in
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with (* an equality *)
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI) -> (
match tty with (* some inductive type *)
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
;
T.then_
~start:
- (fun ~status:((proof,goal) as status) ->
+ (fun status ->
+ let (proof, goal) = status in
let _,metasenv,_,_ = proof in
- let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,gty = CicUtil.lookup_meta goal metasenv in
prerr_endline ("XXXX goal " ^ string_of_int goal) ;
prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ;
prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ;
);
t1]
)
- ~status
+ status
)
~continuation:
(T.then_
~continuation:EqualityTactics.reflexivity_tac
)
]
- ~status
+ status
| _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
)
| _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
diversi *)
-let discriminate'_tac ~term ~status:((proof, goal) as status) =
+let discriminate'_tac ~term status =
+ let (proof, goal) = status in
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI) -> (
match tty with
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
C.Lambda (binder,source,(aux target (k+1)))
| _ ->
if (id = false_constr_id)
- then (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [])
- else (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/True.ind") 0 [])
+ then (C.MutInd(Logic.false_URI,0,[]))
+ else (C.MutInd(Logic.true_URI,0,[]))
in aux red_ty 1
)
constructor_list
let (proof',goals') =
EliminationTactics.elim_type_tac
- ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )
- ~status
+ ~term:(C.MutInd(Logic.false_URI,0,[]))
+ status
in
(match goals' with
[goal'] ->
let _,metasenv',_,_ = proof' in
- let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in
-prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ;
-prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ;
-prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ;
-ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ;
-prerr_endline ("XXXX case " ^ CicPp.ppterm (C.Appl [
- C.Lambda (
- C.Name "x", tty,
- C.MutCase (
- turi, typeno,
- (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
- (C.Rel 1), pattern
- )
- ); t2])) ;
+ let _,context',gty' =
+ CicUtil.lookup_meta goal' metasenv'
+ in
T.then_
~start:
(P.change_tac
~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
~continuation:(IntroductionTactics.constructor_tac ~n:1)
)
- ~status:(proof',goal')
+ (proof',goal')
| _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
)
| _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
;;
-let discriminate_tac ~term ~status =
+let discriminate_tac ~term status =
Tacticals.then_
~start:(* (injection_tac ~term) *) Tacticals.id_tac
~continuation:(discriminate'_tac ~term) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *)
- ~status
+ status
;;
-let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~status
+let compare_tac ~term status = Tacticals.id_tac status
(*
(* term is in the form t1=t2; the tactic leaves two goals: in the first you have to *)
(* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2 *)
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,gty = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with
(C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
~continuations:[
T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ;
decide_equality_tac]
- ~status
+ status
| (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
let term' = (* (t1=t2) \/ ~(t1=t2) *)
C.Appl [
~continuations:[
T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ;
decide_equality_tac]
- ~status
+ status
| _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality")
*)
;;
exception TwoDifferentSubtermsFound of (Cic.term * Cic.term * int)
-let discriminate_tac ~term ~status:((proof, goal) as status) =
+let discriminate_tac ~term status =
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
+ let (proof, goal) = status in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
let (proof',goals') =
EliminationTactics.elim_type_tac
~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )
- ~status
+ status
in
(match goals' with
[goal'] ->
let _,metasenv',_,_ = proof' in
- let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in
-prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ;
-prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ;
-prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ;
-ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ;
-prerr_endline ("XXXX case " ^ CicPp.ppterm (C.Appl [
- C.Lambda (
- C.Name "x", tty,
- C.MutCase (
- turi, typeno,
- (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
- (C.Rel 1), pattern
- )
- ); t2'])) ;
+ let _,context',gty' =
+ CicUtil.lookup_meta goal' metasenv'
+ in
T.then_
~start:
(P.change_tac
~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term)
~continuation:(IntroductionTactics.constructor_tac ~n:1)
)
- ~status:(proof',goal')
+ (proof',goal')
| _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
)
| _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")