X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftactics%2Finversion_principle.ml;fp=components%2Ftactics%2Finversion_principle.ml;h=f2dd37f9eba744ffce46563f607abc1e8c0c8ba2;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml new file mode 100644 index 000000000..f2dd37f9e --- /dev/null +++ b/components/tactics/inversion_principle.ml @@ -0,0 +1,231 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let debug = false;; +let debug_print = + fun msg -> if debug then prerr_endline (Lazy.force msg) else () + +(* cuts away the last element of a list 'l' *) +let rec cut_last l = + match l with + | hd::tl when tl != [] -> hd:: (cut_last tl) + | _ -> [] +;; + +(* cuts away the first 'n' elements of a list 'l' *) +let rec cut_first n l = + if n>0 then + match l with + | hd::tl -> cut_first (n-1) tl + | [] -> [] + else l +;; + +(* returns the first 'n' elements of a list 'l' *) +let rec takefirst n l = + if n > 0 then + match l with + hd::tl when n > 0 -> hd:: takefirst (n-1) tl + | _ -> assert false + else [] +;; + +(* from a complex Cic.Prod term, returns the list of its components *) +let rec list_of_prod term = + match term with + | Cic.Prod (_,src,tgt) -> src::(list_of_prod tgt) + | _ -> [term] +;; + +let rec build_metas sort cons_list created_vars right_created_vars prop + uri typeno = + match cons_list with + | hd::tl -> + Cic.Prod( + Cic.Anonymous, + Cic.Implicit None, + build_metas sort tl + (List.map (CicSubstitution.lift 1) created_vars) + (List.map (CicSubstitution.lift 1) right_created_vars) + (List.map (CicSubstitution.lift 1) prop) uri typeno) + | [] -> + Cic.Prod( + Cic.Name("H"), (*new name?*) + Cic.Appl([Cic.MutInd(uri, typeno, [])] @ created_vars), + Cic.Appl (( (List.map (CicSubstitution.lift 1) prop) @ + (List.map (CicSubstitution.lift 1 ) right_created_vars) @ + (if Inversion.isSetType sort then [Cic.Rel 1] else [])(*H*)) + )) +;; + +(* computes the type of the abstract P *) +let rec get_prop_arity sort rightparam_tys(*only to name m's*) created_vars_ty + local_rvars left_created_vars nleft uri typeno = + match (created_vars_ty) with + hd::tl when (nleft > 0) -> + get_prop_arity sort rightparam_tys tl local_rvars left_created_vars + (nleft-1) uri typeno + | hd::tl -> + Cic.Prod( + Cic.Name("m" ^ string_of_int(List.length rightparam_tys) ), + hd, + get_prop_arity sort (List.tl rightparam_tys) + (List.map (CicSubstitution.lift 1) tl) + (List.map (CicSubstitution.lift 1) (local_rvars @ [Cic.Rel 1])) + (List.map (CicSubstitution.lift 1) left_created_vars) nleft uri typeno + ) + | [] -> + if Inversion.isSetType sort then + Cic.Prod(Cic.Anonymous, + Cic.Appl([Cic.MutInd(uri, typeno, [])] + @ (List.map (CicSubstitution.lift (-1)) left_created_vars) + @ (List.map (CicSubstitution.lift(-1)) local_rvars) ), + Cic.Sort(Cic.Prop)) + else + Cic.Sort Cic.Prop +;; + +(* created vars is empty at the beginning *) +let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*) + arity cons_list created_vars created_vars_ty nleft + uri typeno = + match (arity) with + Cic.Prod(_,src,tgt) -> + Cic.Prod( + Cic.Name("p" ^ string_of_int(List.length arity_l)), + src, + build_theorem rightparam_tys + (List.tl arity_l) tgt cons_list + (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1])) + (List.map (CicSubstitution.lift 1) (created_vars_ty @ [src])) + nleft uri typeno) + | sort -> + Cic.Prod(Cic.Name("P"), + get_prop_arity sort rightparam_tys created_vars_ty [](*local vars*) + (takefirst nleft created_vars) (*left_created_vars*) nleft uri typeno, + build_metas sort cons_list created_vars (cut_first nleft created_vars) + [(Cic.Rel 1)] uri typeno ) +;; + +let build_inversion uri obj = + (*uri e obj of InductiveDefinition *) + let module PET = ProofEngineTypes in + let build_one typeno name nleft arity cons_list = + (*check if there are right parameters, else return void*) + if List.length (list_of_prod arity) = (nleft + 1) then + None + else + try + let arity_l = cut_last (list_of_prod arity) in + let rightparam_tys = cut_first nleft arity_l in + let theorem = build_theorem rightparam_tys arity_l arity cons_list + [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in + debug_print + (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem))); + let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem + CicUniv.empty_ugraph in + (*DEBUG*) debug_print + (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem))); + let buri = UriManager.buri_of_uri uri in + let inversor_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in + let goal = CicMkImplicit.new_meta metasenv [] in + let metasenv' = (goal,[],ref_theorem)::metasenv in + let attrs = [`Class (`InversionPrinciple); `Generated] in + let _subst = [] in + let proof= + (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in + let _,applies = + List.fold_right + (fun _ (i,applies) -> + i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies) + cons_list (2,[]) + in + let proof1,gl1 = + PET.apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ()) + (*if the number of applies is 1, we cannot use + thens, but then_*) + ~continuation: + (match (List.length applies) with + 0 -> (Inversion.private_inversion_tac (Cic.Rel 1)) + | 1 -> (Tacticals.then_ + ~start:(Inversion.private_inversion_tac + (Cic.Rel 1)) + ~continuation:(PrimitiveTactics.apply_tac + (Cic.Rel 2)) + ) + | _ -> (Tacticals.thens + ~start:(Inversion.private_inversion_tac + (Cic.Rel 1)) + ~continuations:applies + ) + )) + (proof,goal) + in + let metasenv,bo,ty, attrs = + match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs + in + assert (metasenv = []); + Some + (inversor_uri, + Cic.Constant + (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[])) + with + Inversion.EqualityNotDefinedYet -> None + | CicRefine.RefineFailure ls -> + HLog.warn + ("CicRefine.RefineFailure during generation of inversion principle: " ^ + Lazy.force ls) ; + None + | CicRefine.Uncertain ls -> + HLog.warn + ("CicRefine.Uncertain during generation of inversion principle: " ^ + Lazy.force ls) ; + None + | CicRefine.AssertFailure ls -> + HLog.warn + ("CicRefine.AssertFailure during generation of inversion principle: " ^ + Lazy.force ls) ; + None + in + match obj with + | Cic.InductiveDefinition (tys,_,nleft,_) -> + let counter = ref (List.length tys) in + List.fold_right + (fun (name,_,arity,cons_list) res -> + counter := !counter-1; + match build_one !counter name nleft arity cons_list with + | None -> res + | Some inv -> inv::res) + tys [] + |_ -> assert false + +;; + +let init () = ();; + +LibrarySync.build_inversion_principle := build_inversion;;