*)
-let constructor_tac ~n ~status:(proof, goal) =
- let module C = Cic in
- let module R = CicReduction in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- match (R.whd context ty) with
- (C.MutInd (uri,typeno,exp_named_subst))
- | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::_)) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
- ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
- | _ -> raise (ProofEngineTypes.Fail "Constructor failed")
-;;
-
-
-let exists_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let split_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let left_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let right_tac ~status =
- constructor_tac ~n:2 ~status
-;;
-
-
-let reflexivity_tac =
- constructor_tac ~n:1
-;;
-
-
-let symmetry_tac ~status:(proof, goal) =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- match (R.whd context ty) with
- (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", []))
-
- | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", []))
-
- | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
-;;
-
-
-let transitivity_tac ~term ~status:((proof, goal) as status) =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let module Tl = Tacticals in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- match (R.whd context ty) with
- (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
- Tl.thens
- ~start:(PrimitiveTactics.apply_tac
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
- ~continuations:
- [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term]
- ~status
-
- | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
- Tl.thens
- ~start:(PrimitiveTactics.apply_tac
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", [])))
- ~continuations:
- [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term]
- ~status
-
- | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
-;;
-
-
(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
-
let assumption_tac ~status:((proof,goal) as status) =
let module C = Cic in
let module R = CicReduction in
- let module T = CicTypeChecker in
let module S = CicSubstitution in
let _,metasenv,_,_ = proof in
let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let rec find n = function
hd::tl ->
-(* (let hdd = hd in
- match hdd with
- Some (name, termine) -> prerr_endline("####" ^ name ^ CicPp.ppterm termine)
- | None -> prerr_endline("#### None")
- );
-*) (match hd with
+ (match hd with
(Some (_, C.Decl t)) when
(R.are_convertible context (S.lift n t) ty) -> n
| (Some (_, C.Def t)) when
(R.are_convertible context
- (T.type_of_aux' metasenv context (S.lift n t)) ty) -> n
+ (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
| _ -> find (n+1) tl
)
- | [] -> raise (ProofEngineTypes.Fail "No such assumption")
+ | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
;;
-(*
+(* Questa invece era in fourierR.ml
+let assumption_tac ~status:(proof,goal)=
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let num = ref 0 in
+ let tac_list = List.map
+ ( fun x -> num := !num + 1;
+ match x with
+ Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
+ | _ -> ("fake",tcl_fail 1)
+ )
+ context
+ in
+ Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
+;;
+*)
+
+
+(* ANCORA DA DEBUGGARE *)
+
+(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
+e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
+contesto e si lifta *)
let generalize_tac ~term ~status:((proof,goal) as status) =
let module C = Cic in
- let module R = CicReduction in
- let module T = CicTypeChecker in
let module P = PrimitiveTactics in
- let module Tl = Tacticals in
+ let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
- Tl.thens
- ~start:(P.cut_tac ~term:(C.Lambda ("dummy_for_gen", (T.type_of_aux' metasenv context term), (R.replace ?????? (C.Name "dummy_for_gen") term )))
- ~continuations: [(P.apply_tac (C.Appl [(C.Rel 1); term])); Tl.id_tac] (* in quest'ordine o viceversa? provare *)
+ let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ T.thens
+ ~start:(P.cut_tac
+ ~term:(
+ C.Prod(
+ (C.Name "dummy_for_gen"),
+ (CicTypeChecker.type_of_aux' metasenv context term),
+ (ProofEngineReduction.replace_lifting_csc 1
+ ~equality:(==)
+ ~what:term
+ ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
+ ~where:ty)
+ )))
+ ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
~status
;;
-let absurd_tac ~term ~status:((proof,goal) as status) =
- PrimitiveTactics.cut_tac
+(* IN FASE DI IMPLEMENTAZIONE *)
+
+let decide_equality_tac =
+ Tacticals.id_tac
+;;
+
+(*
+let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
+ 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,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
+ (* controllo che i due termini siano comparabili *)
+ then
+ T.thens
+ ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
+ ~continuations:[split_tac ; P.intros_tac ~name:"FOO"]
+ else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
;;
*)
projects / helm.git / blobdiff