(* 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.oblivion_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;;