let module P = PrimitiveTactics in
let module T = Tacticals in
let module S = ProofEngineStructuralRules in
- let module U = UriManager in
+ let module U = UriManager in
let (_,metasenv,_,_) = proof in
let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let termty = T.type_of_aux' metasenv context term in
- let uri,exp_named_subst,typeno,args =
- match termty with
- C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
- | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args)
- | _ -> raise (ProofEngineTypes.Fail "Induction: Not an Inductive Type to Eliminate")
- in
- let eliminator_uri =
- let base = U.buri_of_uri uri in
- let name =
- match CicEnvironment.get_obj uri with
- C.InductiveDefinition (tys,_,_) ->
- let (name,_,_,_) = List.nth tys typeno in
- name
- | _ -> assert false
- in
- let ext =
- match T.type_of_aux' metasenv context ty with
- C.Sort C.Prop -> "_ind"
- | C.Sort C.Set -> "_rec"
- | C.Sort C.Type -> "_rect"
- | _ -> assert false
- in
- U.uri_of_string (base ^ "/" ^ name ^ ext ^ ".con")
- in
- apply_tac ~term:(C.Const (eliminator_uri , exp_named_subst)) (* come mi devo comportare con gli args??? *)
+ let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *)
+
+ T.then_ ~start:(T.repeat_tactic
+ ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *)
+ ~continuation:(P.intros))
+ ~continuation:(P.elim_intros_simpl ~term)
+ ~status
;;
*)
+
let elim_type_tac ~term ~status =
let module C = Cic in
let module P = PrimitiveTactics in
*)
-(* PROVE DI DECOMPOSE
+(* PROVE DI DECOMPOSE *)
+(* guardare quali sono i tipi induttivi decomponibili presenti in
+profondita' nel term; chiamare una funzione di call-back passando questa
+lista e ritornando la lista di termini che l'utente vuole decomporre;
+decomporre. *)
-(* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
-let decompose_tac ~what ~where ~status:((proof,goal) as status) =
- let module C = Cic in
- let module R = CicReduction in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let module S = ProofEngineStructuralRules in
- let rec decomposing ty what =
- match (what) with
- [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
- | hd::tl as what ->
- match ty with
- (C.Appl (hd::_)) -> hd
- | _ -> decomposing ty tl
- in
+exception InteractiveUserUriChoiceNotRegistered
- let (_,metasenv,_,_) = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
- T.repeat_tactic
- ~tactic:(T.then_
- ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
- ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where)))) (* ma che ipotesi sto cancellando??? *)
- )
- ~status
+let interactive_user_uri_choice =
+ (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) :
+ (selection_mode:[`SINGLE | `EXTENDED] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string -> msg:string -> string list -> string list) ref)
+;;
+
+exception IllFormedUri of string
+
+let cic_textual_parser_uri_of_string uri' =
+ try
+ (* Constant *)
+ if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+ CicTextualParser0.ConUri (UriManager.uri_of_string uri')
+ else
+ if String.sub uri' (String.length uri' - 4) 4 = ".var" then
+ CicTextualParser0.VarUri (UriManager.uri_of_string uri')
+ else
+ (try
+ (* Inductive Type *)
+ let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+ CicTextualParser0.IndTyUri (uri'',typeno)
+ with
+ _ ->
+ (* Constructor of an Inductive Type *)
+ let uri'',typeno,consno =
+ CicTextualLexer.indconuri_of_uri uri'
+ in
+ CicTextualParser0.IndConUri (uri'',typeno,consno)
+ )
+ with
+ _ -> raise (IllFormedUri uri')
+;;
+
+let constructor_uri_of_string uri =
+ match cic_textual_parser_uri_of_string uri with
+ CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
+ | _ -> assert false
+;;
+
+let call_back uris =
+(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
+ let module U = UriManager in
+ List.map
+ (constructor_uri_of_string)
+ (!interactive_user_uri_choice
+ ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
+ ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
+ (List.map
+ (function (uri,typeno,_) -> U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1))
+ uris)
+ )
;;
-let decompose_tac ~clist ~status:((proof,goal) as status) =
+let decompose_tac ~term ~status:((proof,goal) as status) =
let module C = Cic in
let module R = CicReduction in
let module P = PrimitiveTactics in
let module T = Tacticals in
let module S = ProofEngineStructuralRules in
- let (_,metasenv,_,_) = proof in
+ let _,metasenv,_,_ = proof in
let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
- let rec repeat_elim ~term ~status = (* term -> status -> proof * (goal list) *)
- try
- let (proof, goallist) =
- T.then_
- ~start:(P.elim_simpl_intros_tac ~term)
- ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty)))) (* non so che ipotesi sto cancellando??? *)
- ~status
+ let old_context_len = List.length context in
+(* let nr_of_hyp_still_to_elim = ref 1 in *)
+ let termty = CicTypeChecker.type_of_aux' metasenv context term in
+
+ let rec make_list termty =
+(* altamente inefficente? *)
+ let rec search_inductive_types urilist termty =
+ (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
+ match termty with
+ (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) ->
+ (uri,typeno,exp_named_subst)::urilist
+ | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) ->
+ (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist)
+ | _ -> urilist
+ (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *)
+ in
+ let rec purge_duplicates urilist =
+ let rec aux triple urilist =
+ match urilist with
+ [] -> []
+ | hd::tl ->
+ if (hd = triple)
+ then aux triple tl
+ else hd::(aux triple tl)
in
- let rec step proof goallist =
- match goallist with
- [] -> (proof, [])
- | hd::tl ->
- let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
- let (proof'', goallist'') = step proof' tl in
- proof'', goallist'@goallist''
- in
- step proof goallist
- with
- (Fail _) -> T.id_tac
-
- in
- let rec decomposing ty clist = (* term -> (term list) -> bool *)
- match (clist) with
- [] -> false
- | hd::tl as clist ->
- match ty with
- (C.Appl (hd::_)) -> true
- | _ -> decomposing ty tl
-
+ match urilist with
+ [] -> []
+ | hd::tl -> hd::(purge_duplicates (aux hd tl))
+ in
+ purge_duplicates (search_inductive_types [] termty)
in
- let term = decomposing (R.whd context ty) clist in
- if (term == C.Implicit)
- then (Fail "Decompose: nothing to decompose or no application")
- else repeat_elim ~term ~status
-;;
-*)
-let decompose_tac ~clist ~status =
- let module C = Cic in
- let module R = CicReduction in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let module S = ProofEngineStructuralRules in
+ let urilist =
+ (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *)
+ (* N.B.: due to a bug in call_back exp_named_subst are not significant (they all are []) *)
+ call_back (make_list termty) in
+
+ let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim ~status:((proof,goal) as status) =
+prerr_endline ("%%%%%%% nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));
+ if nr_of_hyp_still_to_elim <> 0 then
+ let _,metasenv,_,_ = proof in
+ let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let old_context_len = List.length context in
+ let termty = CicTypeChecker.type_of_aux' metasenv context term' in
+prerr_endline ("%%%%%%% elim_clear termty= " ^ CicPp.ppterm termty);
+ match termty with
+ C.MutInd (uri,typeno,exp_named_subst)
+ | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_)
+ when (List.mem (uri,typeno,exp_named_subst) urilist) ->
+prerr_endline ("%%%%%%% elim " ^ CicPp.ppterm termty);
+ T.then_
+ ~start:(P.elim_intros_simpl_tac ~term:term')
+ ~continuation:(
+ (* clear the hyp that has just been eliminated *)
+ (fun ~status:((proof,goal) as status) ->
+ let _,metasenv,_,_ = proof in
+ let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let new_context_len = List.length context in
+prerr_endline ("%%%%%%% newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim));
+ let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in
+ T.then_
+ ~start:(
+ if (term'==term) (* this is the first application of elim: there's no need to clear the hyp *)
+ then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end
+ else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
+ ~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)
+ ~status
+ ))
+ ~status
+ | _ ->
+ let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in
+prerr_endline ("%%%%%%% fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim));
+ elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim ~status
+ else (* raise (ProofEngineTypes.Fail "Decomopse: finished decomposing"); *) T.id_tac ~status
- let rec choose ty =
- function
- [] -> C.Implicit (* a cosa serve? *)
- | hd::tl ->
- match ty with
- (C.Appl (hd::_)) -> hd
- | _ -> choose ty tl
- in
-
- let decompose_one_tac ~clist ~status:((proof,goal) as status) =
- let (_,metasenv,_,_) = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let term = choose (R.whd context ty) clist in
- if (term == C.Implicit)
- then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
- else T.then_
- ~start:(P.elim_intros_simpl_tac ~term)
- ~continuation:(S.clear ~hyp:(List.hd context))
-(* (S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)*)
- ~status
- in
- T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
+ in
+(* T.repeat_tactic ~tactic: *)
+ (elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1)
+ ~status
;;
+
*)
-(* 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 / commitdiff