*)
-(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
+(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
+chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
+funzione di callback che restituisce la (sola) hyp da applicare *)
+
let assumption_tac ~status:((proof,goal) as status) =
let module C = Cic in
let module R = CicReduction in
(* 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 *)
+contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
+
let generalize_tac ~term ~status:((proof,goal) as status) =
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+(*
+ let found = false in
+ let rec new_context context ty =
+ if ty == term then let found = true in context
+ else match ty with
+ C.Rel _
+ | C.Var _
+ | C.Meta _ (* ???? *)
+ | C.Sort s
+ | C.Implicit -> context
+ | C.Cast (val,typ) ->
+ let tmp_context = new_context context val in
+ tmp_context @ (new_context tmp_context typ)
+ | C.Prod (binder, source, target) ->
+ | C.Lambda (binder, source, target) ->
+ let tmp_context = new_context context source in
+ tmp_context @ (new_context tmp_context binder)
+ | C.LetIn (binder, term, target) ->
+ | C.Appl applist ->
+ let rec aux context =
+ match applist with
+ [] -> context
+ | hd::tl ->
+ let tmp_context = (new_context context hd)
+ in aux tmp_context tl
+ in aux context applist
+ | C.Const (uri, exp_named_subst)
+ | C.MutInd (uri, typeno, exp_named_subst)
+ | C.MutConstruct (uri, typeno, consno, exp_named_subst) ->
+ match exp_named_subst with
+ [] -> context
+ | (uri,t)::_ -> new_context context (type_of_aux' context t)
+ | _ -> assert false
+ | C.MutCase (uri, typeno, outtype, iterm, patterns)
+ | C.Fix (funno, funlist)
+ | C.CoFix (funno, funlist) ->
+ match funlist with
+ [] -> context (* caso possibile? *)
+ | (name, index, type, body)::_ ->
+ let tmp_context = ~
+ in
+*)
T.thens
~start:(P.cut_tac
~term:(
(* IN FASE DI IMPLEMENTAZIONE *)
let decide_equality_tac =
+(* il goal e' un termine della forma t1=t2\/~t1=t2; la tattica decide se l'uguaglianza
+e' vera o no e lo risolve *)
Tacticals.id_tac
;;
-(*
-let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
+
+let compare_tac ~term ~status:((proof, goal) as 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 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")
+ 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")) ->
+
+ let term' = (* (t1=t2)\/~(t1=t2) *)
+ C.Appl [
+ (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ;
+ term ;
+ C.Appl [
+ (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 1, [])) ;
+ t1 ;
+ C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2]
+ ]
+ ]
+ in
+ T.thens
+ ~start:(P.cut_tac ~term:term')
+ ~continuations:[
+ T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ;
+ decide_equality_tac]
+ | (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 [
+ (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ;
+ term ;
+ C.Appl [
+ (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"), 1, [])) ;
+ t1 ;
+ C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2]
+ ]
+ ]
+ in
+ T.thens
+ ~start:(P.cut_tac ~term:term')
+ ~continuations:[
+ T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ;
+ decide_equality_tac]
+ | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality")
+;;
+
+
+let discriminate_tac ~term ~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
+ T.id_tac
;;
-*)
projects / helm.git / blobdiff