(* Copyright (C) 2000, 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/. *) (**************************************************************************) (* *) (* PROJECT HELM *) (* *) (* Andrea Asperti *) (* 16/6/2003 *) (* *) (**************************************************************************) (* $Id$ *) let object_prefix = "obj:";; let declaration_prefix = "decl:";; let definition_prefix = "def:";; let inductive_prefix = "ind:";; let joint_prefix = "joint:";; let proof_prefix = "proof:";; let conclude_prefix = "concl:";; let premise_prefix = "prem:";; let lemma_prefix = "lemma:";; let hide_coercions = ref true;; (* e se mettessi la conversione di BY nell'apply_context ? *) (* sarebbe carino avere l'invariante che la proof2pres generasse sempre prove con contesto vuoto *) let gen_id prefix seed = let res = prefix ^ string_of_int !seed in incr seed ; res ;; let name_of = function Cic.Anonymous -> None | Cic.Name b -> Some b;; exception Not_a_proof;; exception NotImplemented;; exception NotApplicable;; (* we do not care for positivity, here, that in any case is enforced by well typing. Just a brutal search *) let rec occur uri = let module C = Cic in function C.Rel _ -> false | C.Var _ -> false | C.Meta _ -> false | C.Sort _ -> false | C.Implicit _ -> assert false | C.Prod (_,s,t) -> (occur uri s) or (occur uri t) | C.Cast (te,ty) -> (occur uri te) | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *) | C.LetIn (_,s,ty,t) -> (occur uri s) or (occur uri ty) or (occur uri t) | C.Appl l -> List.fold_left (fun b a -> if b then b else (occur uri a)) false l | C.Const (_,_) -> false | C.MutInd (uri1,_,_) -> if uri = uri1 then true else false | C.MutConstruct (_,_,_,_) -> false | C.MutCase _ -> false (* presuming too much?? *) | C.Fix _ -> false (* presuming too much?? *) | C.CoFix (_,_) -> false (* presuming too much?? *) ;; let get_id = let module C = Cic in function C.ARel (id,_,_,_) -> id | C.AVar (id,_,_) -> id | C.AMeta (id,_,_) -> id | C.ASort (id,_) -> id | C.AImplicit _ -> raise NotImplemented | C.AProd (id,_,_,_) -> id | C.ACast (id,_,_) -> id | C.ALambda (id,_,_,_) -> id | C.ALetIn (id,_,_,_,_) -> id | C.AAppl (id,_) -> id | C.AConst (id,_,_) -> id | C.AMutInd (id,_,_,_) -> id | C.AMutConstruct (id,_,_,_,_) -> id | C.AMutCase (id,_,_,_,_,_) -> id | C.AFix (id,_,_) -> id | C.ACoFix (id,_,_) -> id ;; let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts= let module C = Cic in let module C2A = Cic2acic in (* atomic terms are never lifted, according to my policy *) function C.ARel (id,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.AVar (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.AMeta (id,_,_) -> (try Hashtbl.find ids_to_inner_sorts id = `Prop with Not_found -> assert false) | C.ASort (id,_) -> false | C.AImplicit _ -> raise NotImplemented | C.AProd (id,_,_,_) -> false | C.ACast (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.ALambda (id,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.ALetIn (id,_,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.AAppl (id,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.AConst (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.AMutInd (id,_,_,_) -> false | C.AMutConstruct (id,_,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) (* oppure: false *) | C.AMutCase (id,_,_,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.AFix (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) | C.ACoFix (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) ;; (* transform a proof p into a proof list, concatenating the last conclude element to the apply_context list, in case context is empty. Otherwise, it just returns [p] *) let flat seed p = let module K = Content in if (p.K.proof_context = []) then if p.K.proof_apply_context = [] then [p] else let p1 = { p with K.proof_context = []; K.proof_apply_context = [] } in p.K.proof_apply_context@[p1] else [p] ;; let rec serialize seed = function [] -> [] | a::l -> (flat seed a)@(serialize seed l) ;; (* top_down = true if the term is a LAMBDA or a decl *) let generate_conversion seed top_down id inner_proof ~ids_to_inner_types = let module C2A = Cic2acic in let module K = Content in let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected) with Not_found -> None) in match exp with None -> inner_proof | Some expty -> if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then { K.proof_name = inner_proof.K.proof_name; K.proof_id = gen_id proof_prefix seed; K.proof_context = [] ; K.proof_apply_context = []; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "TD_Conversion"; K.conclude_args = [K.ArgProof {inner_proof with K.proof_name = None}]; K.conclude_conclusion = Some expty }; } else { K.proof_name = inner_proof.K.proof_name; K.proof_id = gen_id proof_prefix seed; K.proof_context = [] ; K.proof_apply_context = [{inner_proof with K.proof_name = None}]; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "BU_Conversion"; K.conclude_args = [K.Premise { K.premise_id = gen_id premise_prefix seed; K.premise_xref = inner_proof.K.proof_id; K.premise_binder = None; K.premise_n = None } ]; K.conclude_conclusion = Some expty }; } ;; let generate_exact seed t id name ~ids_to_inner_types = let module C2A = Cic2acic in let module K = Content in { K.proof_name = name; K.proof_id = gen_id proof_prefix seed ; K.proof_context = [] ; K.proof_apply_context = []; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "Exact"; K.conclude_args = [K.Term (false, t)]; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None }; } ;; let generate_intros_let_tac seed id n s ty inner_proof name ~ids_to_inner_types = let module C2A = Cic2acic in let module C = Cic in let module K = Content in { K.proof_name = name; K.proof_id = gen_id proof_prefix seed ; K.proof_context = [] ; K.proof_apply_context = []; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "Intros+LetTac"; K.conclude_args = [K.ArgProof inner_proof]; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> (match inner_proof.K.proof_conclude.K.conclude_conclusion with None -> None | Some t -> match ty with None -> Some (C.AProd ("gen"^id,n,s,t)) | Some ty -> Some (C.ALetIn ("gen"^id,n,s,ty,t))) }; } ;; let build_decl_item seed id n s ~ids_to_inner_sorts = let module K = Content in let sort = try Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)) with Not_found -> None in match sort with | Some `Prop -> `Hypothesis { K.dec_name = name_of n; K.dec_id = gen_id declaration_prefix seed; K.dec_inductive = false; K.dec_aref = id; K.dec_type = s } | _ -> `Declaration { K.dec_name = name_of n; K.dec_id = gen_id declaration_prefix seed; K.dec_inductive = false; K.dec_aref = id; K.dec_type = s } ;; let infer_dependent ~headless context metasenv = function | [] -> assert false | [t] -> [false, t] | he::tl as l -> if headless then List.map (function s -> false,s) l else try let hety,_ = CicTypeChecker.type_of_aux' metasenv context (Deannotate.deannotate_term he) CicUniv.oblivion_ugraph in let fstorder t = match CicReduction.whd context t with | Cic.Prod _ -> false | _ -> true in let rec dummify_last_tgt t = match CicReduction.whd context t with | Cic.Prod (n,s,tgt) -> Cic.Prod(n,s, dummify_last_tgt tgt) | _ -> Cic.Implicit None in let rec aux ty = function | [] -> [] | t::tl -> match FreshNamesGenerator.clean_dummy_dependent_types (dummify_last_tgt ty) with | Cic.Prod (n,src,tgt) -> (n <> Cic.Anonymous && fstorder src, t) :: aux (CicSubstitution.subst (Deannotate.deannotate_term t) tgt) tl | _ -> List.map (fun s -> false,s) (t::tl) in (false, he) :: aux hety tl with CicTypeChecker.TypeCheckerFailure _ -> assert false ;; let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts = let module C = Cic in let module K = Content in let rec aux n = function [] -> [],[] | (dep, t)::l1 -> let need_lifting = test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts in let subproofs,args = aux (n + if need_lifting then 1 else 0) l1 in if need_lifting then let new_subproof = acic2content seed context metasenv ~name:("H" ^ string_of_int n) ~ids_to_inner_types ~ids_to_inner_sorts t in let new_arg = K.Premise { K.premise_id = gen_id premise_prefix seed; K.premise_xref = new_subproof.K.proof_id; K.premise_binder = new_subproof.K.proof_name; K.premise_n = None } in new_subproof::subproofs,new_arg::args else let hd = (match t with C.ARel (idr,idref,n,b) -> let sort = (try Hashtbl.find ids_to_inner_sorts idr with Not_found -> `Type (CicUniv.fresh())) in if sort = `Prop then K.Premise { K.premise_id = gen_id premise_prefix seed; K.premise_xref = idr; K.premise_binder = Some b; K.premise_n = Some n } else (K.Term (dep,t)) | C.AConst(id,uri,[]) -> let sort = (try Hashtbl.find ids_to_inner_sorts id with Not_found -> `Type (CicUniv.fresh())) in if sort = `Prop then K.Lemma { K.lemma_id = gen_id lemma_prefix seed; K.lemma_name = UriManager.name_of_uri uri; K.lemma_uri = UriManager.string_of_uri uri } else (K.Term (dep,t)) | C.AMutConstruct(id,uri,tyno,consno,[]) -> let sort = (try Hashtbl.find ids_to_inner_sorts id with Not_found -> `Type (CicUniv.fresh())) in if sort = `Prop then let inductive_types = (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with | Cic.InductiveDefinition (l,_,_,_) -> l | _ -> assert false ) in let (_,_,_,constructors) = List.nth inductive_types tyno in let name,_ = List.nth constructors (consno - 1) in K.Lemma { K.lemma_id = gen_id lemma_prefix seed; K.lemma_name = name; K.lemma_uri = UriManager.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")" } else (K.Term (dep,t)) | _ -> (K.Term (dep,t))) in subproofs,hd::args in match (aux 1 (infer_dependent ~headless context metasenv l)) with [p],args -> [{p with K.proof_name = None}], List.map (function K.Premise prem when prem.K.premise_xref = p.K.proof_id -> K.Premise {prem with K.premise_binder = None} | i -> i) args | p,a as c -> c and build_def_item seed context metasenv id n t ty ~ids_to_inner_sorts ~ids_to_inner_types = let module K = Content in try let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then (let p = (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) in `Proof p;) else `Definition { K.def_name = name_of n; K.def_id = gen_id definition_prefix seed; K.def_aref = id; K.def_term = t; K.def_type = ty } with Not_found -> assert false (* the following function must be called with an object of sort Prop. For debugging purposes this is tested again, possibly raising an Not_a_proof exception *) and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_types t = let rec aux ?name context t = let module C = Cic in let module K = Content in let module C2A = Cic2acic in let t1 = match t with C.ARel (id,idref,n,b) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AVar (id,uri,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMeta (id,n,l) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.ASort (id,s) -> raise Not_a_proof | C.AImplicit _ -> raise NotImplemented | C.AProd (_,_,_,_) -> raise Not_a_proof | C.ACast (id,v,t) -> aux context v | C.ALambda (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then let proof = aux ((Some (n,Cic.Decl (Deannotate.deannotate_term s)))::context) t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then match proof.K.proof_conclude.K.conclude_args with [K.ArgProof p] -> p | _ -> assert false else proof in let proof'' = { proof' with K.proof_name = None; K.proof_context = (build_decl_item seed id n s ids_to_inner_sorts):: proof'.K.proof_context } in generate_intros_let_tac seed id n s None proof'' name ~ids_to_inner_types else raise Not_a_proof | C.ALetIn (id,n,s,ty,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then let proof = aux ((Some (n, Cic.Def (Deannotate.deannotate_term s,Deannotate.deannotate_term ty)))::context) t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then match proof.K.proof_conclude.K.conclude_args with [K.ArgProof p] -> p | _ -> assert false else proof in let proof'' = { proof' with K.proof_name = None; K.proof_context = ((build_def_item seed context metasenv (get_id s) n s ty ids_to_inner_sorts ids_to_inner_types):> Cic.annterm K.in_proof_context_element) ::proof'.K.proof_context; } in generate_intros_let_tac seed id n s (Some ty) proof'' name ~ids_to_inner_types else raise Not_a_proof | C.AAppl (id,li) -> (try coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> try rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> try inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> try transitivity seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> let subproofs, args = build_subproofs_and_args seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts in (* let args_to_lift = List.filter (test_for_lifting ~ids_to_inner_types) li in let subproofs = match args_to_lift with [_] -> List.map aux args_to_lift | _ -> List.map (aux ~name:"H") args_to_lift in let args = build_args seed li subproofs ~ids_to_inner_types ~ids_to_inner_sorts in *) { K.proof_name = name; K.proof_id = gen_id proof_prefix seed; K.proof_context = []; K.proof_apply_context = serialize seed subproofs; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "Apply"; K.conclude_args = args; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None }; }) | C.AConst (id,uri,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> let inductive_types,noparams = (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false | Cic.InductiveDefinition (l,_,n,_) -> l,n ) in let (_,_,_,constructors) = List.nth inductive_types typeno in let name_and_arities = let rec count_prods = function C.Prod (_,_,t) -> 1 + count_prods t | _ -> 0 in List.map (function (n,t) -> Some n,((count_prods t) - noparams)) constructors in let pp = let build_proof p (name,arity) = let rec make_context_and_body c p n = if n = 0 then c,(aux context p) else (match p with Cic.ALambda(idl,vname,s1,t1) -> let ce = build_decl_item seed idl vname s1 ~ids_to_inner_sorts in make_context_and_body (ce::c) t1 (n-1) | _ -> assert false) in let context,body = make_context_and_body [] p arity in K.ArgProof {body with K.proof_name = name; K.proof_context=context} in List.map2 build_proof patterns name_and_arities in let context,term = (match build_subproofs_and_args ~headless:true seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts [te] with l,[t] -> l,t | _ -> assert false) in { K.proof_name = name; K.proof_id = gen_id proof_prefix seed; K.proof_context = []; K.proof_apply_context = serialize seed context; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "Case"; K.conclude_args = (K.Aux (UriManager.string_of_uri uri)):: (K.Aux (string_of_int typeno))::(K.Term (false,ty))::term::pp; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None } } | C.AFix (id, no, funs) -> let context' = List.fold_left (fun ctx (_,n,_,ty,_) -> let ty = Deannotate.deannotate_term ty in Some (Cic.Name n,Cic.Decl ty) :: ctx) [] funs @ context in let proofs = List.map (function (_,name,_,_,bo) -> `Proof (aux context' ~name bo)) funs in let fun_name = List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no in let decreasing_args = List.map (function (_,_,n,_,_) -> n) funs in let jo = { K.joint_id = gen_id joint_prefix seed; K.joint_kind = `Recursive decreasing_args; K.joint_defs = proofs } in { K.proof_name = name; K.proof_id = gen_id proof_prefix seed; K.proof_context = [`Joint jo]; K.proof_apply_context = []; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "Exact"; K.conclude_args = [ K.Premise { K.premise_id = gen_id premise_prefix seed; K.premise_xref = jo.K.joint_id; K.premise_binder = Some fun_name; K.premise_n = Some no; } ]; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None } } | C.ACoFix (id,no,funs) -> let context' = List.fold_left (fun ctx (_,n,ty,_) -> let ty = Deannotate.deannotate_term ty in Some (Cic.Name n,Cic.Decl ty) :: ctx) [] funs @ context in let proofs = List.map (function (_,name,_,bo) -> `Proof (aux context' ~name bo)) funs in let jo = { K.joint_id = gen_id joint_prefix seed; K.joint_kind = `CoRecursive; K.joint_defs = proofs } in { K.proof_name = name; K.proof_id = gen_id proof_prefix seed; K.proof_context = [`Joint jo]; K.proof_apply_context = []; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "Exact"; K.conclude_args = [ K.Premise { K.premise_id = gen_id premise_prefix seed; K.premise_xref = jo.K.joint_id; K.premise_binder = Some "tiralo fuori"; K.premise_n = Some no; } ]; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None }; } in let id = get_id t in generate_conversion seed false id t1 ~ids_to_inner_types in aux ?name context t and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts = let aux context ?name = acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts in let module C2A = Cic2acic in let module K = Content in let module C = Cic in match li with C.AConst (idc,uri,exp_named_subst)::args -> let uri_str = UriManager.string_of_uri uri in let suffix = Str.regexp_string "_ind.con" in let len = String.length uri_str in let n = (try (Str.search_backward suffix uri_str len) with Not_found -> -1) in if n<0 then raise NotApplicable else let method_name = if UriManager.eq uri HelmLibraryObjects.Logic.ex_ind_URI then "Exists" else if UriManager.eq uri HelmLibraryObjects.Logic.and_ind_URI then "AndInd" else if UriManager.eq uri HelmLibraryObjects.Logic.false_ind_URI then "FalseInd" else "ByInduction" in let prefix = String.sub uri_str 0 n in let ind_str = (prefix ^ ".ind") in let ind_uri = UriManager.uri_of_string ind_str in let inductive_types,noparams = (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in match o with | Cic.InductiveDefinition (l,_,n,_) -> (l,n) | _ -> assert false ) in let rec split n l = if n = 0 then ([],l) else let p,a = split (n-1) (List.tl l) in ((List.hd l::p),a) in let params_and_IP,tail_args = split (noparams+1) args in let constructors = (match inductive_types with [(_,_,_,l)] -> l | _ -> raise NotApplicable) (* don't care for mutual ind *) in let constructors1 = let rec clean_up n t = if n = 0 then t else (match t with (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t) | _ -> assert false) in List.map (clean_up noparams) constructors in let no_constructors= List.length constructors in let args_for_cases, other_args = split no_constructors tail_args in let subproofs,other_method_args = build_subproofs_and_args ~headless:true seed context metasenv other_args ~ids_to_inner_types ~ids_to_inner_sorts in let method_args= let rec build_method_args = function [],_-> [] (* extra args are ignored ???? *) | (name,ty)::tlc,arg::tla -> let idarg = get_id arg in let sortarg = (try (Hashtbl.find ids_to_inner_sorts idarg) with Not_found -> `Type (CicUniv.fresh())) in let hdarg = if sortarg = `Prop then let (co,bo) = let rec bc context = function Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) -> let context' = Some (n,Cic.Decl(Deannotate.deannotate_term s1)) ::context in let ce = build_decl_item seed idl n s1 ~ids_to_inner_sorts in if (occur ind_uri s) then ( match t1 with Cic.ALambda(id2,n2,s2,t2) -> let context'' = Some (n2,Cic.Decl (Deannotate.deannotate_term s2)) ::context' in let inductive_hyp = `Hypothesis { K.dec_name = name_of n2; K.dec_id = gen_id declaration_prefix seed; K.dec_inductive = true; K.dec_aref = id2; K.dec_type = s2 } in let (context,body) = bc context'' (t,t2) in (ce::inductive_hyp::context,body) | _ -> assert false) else ( let (context,body) = bc context' (t,t1) in (ce::context,body)) | _ , t -> ([],aux context t) in bc context (ty,arg) in K.ArgProof { bo with K.proof_name = Some name; K.proof_context = co; }; else (K.Term (false,arg)) in hdarg::(build_method_args (tlc,tla)) | _ -> assert false in build_method_args (constructors1,args_for_cases) in { K.proof_name = name; K.proof_id = gen_id proof_prefix seed; K.proof_context = []; K.proof_apply_context = serialize seed subproofs; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = method_name; K.conclude_args = K.Aux (string_of_int no_constructors) ::K.Term (false,(C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))) ::method_args@other_method_args; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None } } | _ -> raise NotApplicable and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts = match li with | ((Cic.AConst _) as he)::tl | ((Cic.AMutInd _) as he)::tl | ((Cic.AMutConstruct _) as he)::tl when CoercDb.is_a_coercion' (Deannotate.deannotate_term he) && !hide_coercions -> let rec last = function [] -> assert false | [t] -> t | _::tl -> last tl in acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl) | _ -> raise NotApplicable and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts = let aux context ?name = acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts in let module C2A = Cic2acic in let module K = Content in let module C = Cic in match li with C.AConst (sid,uri,exp_named_subst)::args -> if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI or UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI or LibraryObjects.is_eq_ind_URI uri or LibraryObjects.is_eq_ind_r_URI uri then let subproofs,arg = (match build_subproofs_and_args seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3] with l,[p] -> l,p | _,_ -> assert false) in let method_args = let rec ma_aux n = function [] -> [] | a::tl -> let hd = if n = 0 then arg else let aid = get_id a in let asort = (try (Hashtbl.find ids_to_inner_sorts aid) with Not_found -> `Type (CicUniv.fresh())) in if asort = `Prop then K.ArgProof (aux context a) else K.Term (false,a) in hd::(ma_aux (n-1) tl) in (ma_aux 3 args) in { K.proof_name = name; K.proof_id = gen_id proof_prefix seed; K.proof_context = []; K.proof_apply_context = serialize seed subproofs; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI || LibraryObjects.is_eq_ind_URI uri then "RewriteLR" else "RewriteRL"; K.conclude_args = K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None } } else raise NotApplicable | _ -> raise NotApplicable and transitivity seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts = let module C2A = Cic2acic in let module K = Content in let module C = Cic in match li with | C.AConst (sid,uri,exp_named_subst)::args when LibraryObjects.is_trans_eq_URI uri -> let exp_args = List.map snd exp_named_subst in let t1,t2,t3,p1,p2 = match exp_args@args with | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2 | _ -> raise NotApplicable in { K.proof_name = name; K.proof_id = gen_id proof_prefix seed; K.proof_context = []; K.proof_apply_context = []; K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "Eq_chain"; K.conclude_args = K.Term (false,t1):: (transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1) @ [K.Term (false,t2)]@ (transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2) @ [K.Term (false,t3)]; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None } } | _ -> raise NotApplicable and transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts t = let module C2A = Cic2acic in let module K = Content in let module C = Cic in match t with | C.AAppl (_,C.AConst (sid,uri,exp_named_subst)::args) when LibraryObjects.is_trans_eq_URI uri -> let exp_args = List.map snd exp_named_subst in let t1,t2,t3,p1,p2 = match exp_args@args with | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2 | _ -> raise NotApplicable in (transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1) @[K.Term (false,t2)] @(transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2) | _ -> [K.ArgProof (acic2content seed context metasenv ~ids_to_inner_sorts ~ids_to_inner_types t)] ;; let map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty) = let module K = Content in let context' = List.map (function (id,None) -> None | (id,Some (name,Cic.ADecl t)) -> Some (* We should call build_decl_item, but we have not computed *) (* the inner-types ==> we always produce a declaration *) (`Declaration { K.dec_name = name_of name; K.dec_id = gen_id declaration_prefix seed; K.dec_inductive = false; K.dec_aref = get_id t; K.dec_type = t }) | (id,Some (name,Cic.ADef (t,ty))) -> Some (* We should call build_def_item, but we have not computed *) (* the inner-types ==> we always produce a declaration *) (`Definition { K.def_name = name_of name; K.def_id = gen_id definition_prefix seed; K.def_aref = get_id t; K.def_term = t; K.def_type = ty }) ) context in (id,n,context',ty) ;; (* map_sequent is similar to map_conjectures, but the for the hid of the hypothesis, which are preserved instead of generating fresh ones. We shall have to adopt a uniform policy, soon or later *) let map_sequent ((id,n,context,ty):Cic.annconjecture) = let module K = Content in let context' = List.map (function (id,None) -> None | (id,Some (name,Cic.ADecl t)) -> Some (* We should call build_decl_item, but we have not computed *) (* the inner-types ==> we always produce a declaration *) (`Declaration { K.dec_name = name_of name; K.dec_id = id; K.dec_inductive = false; K.dec_aref = get_id t; K.dec_type = t }) | (id,Some (name,Cic.ADef (t,ty))) -> Some (* We should call build_def_item, but we have not computed *) (* the inner-types ==> we always produce a declaration *) (`Definition { K.def_name = name_of name; K.def_id = id; K.def_aref = get_id t; K.def_term = t; K.def_type = ty }) ) context in (id,n,context',ty) ;; let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = let module C = Cic in let module K = Content in let module C2A = Cic2acic in let seed = ref 0 in function C.ACurrentProof (_,_,n,conjectures,bo,ty,params,_) -> (gen_id object_prefix seed, params, Some (List.map (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types) conjectures), `Def (K.Const,ty, build_def_item seed [] (Deannotate.deannotate_conjectures conjectures) (get_id bo) (C.Name n) bo ty ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AConstant (_,_,n,Some bo,ty,params,_) -> (gen_id object_prefix seed, params, None, `Def (K.Const,ty, build_def_item seed [] [] (get_id bo) (C.Name n) bo ty ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AConstant (id,_,n,None,ty,params,_) -> (gen_id object_prefix seed, params, None, `Decl (K.Const, build_decl_item seed id (C.Name n) ty ~ids_to_inner_sorts)) | C.AVariable (_,n,Some bo,ty,params,_) -> (gen_id object_prefix seed, params, None, `Def (K.Var,ty, build_def_item seed [] [] (get_id bo) (C.Name n) bo ty ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AVariable (id,n,None,ty,params,_) -> (gen_id object_prefix seed, params, None, `Decl (K.Var, build_decl_item seed id (C.Name n) ty ~ids_to_inner_sorts)) | C.AInductiveDefinition (id,l,params,nparams,_) -> (gen_id object_prefix seed, params, None, `Joint { K.joint_id = gen_id joint_prefix seed; K.joint_kind = `Inductive nparams; K.joint_defs = List.map (build_inductive seed) l }) and build_inductive seed = let module K = Content in fun (_,n,b,ty,l) -> `Inductive { K.inductive_id = gen_id inductive_prefix seed; K.inductive_name = n; K.inductive_kind = b; K.inductive_type = ty; K.inductive_constructors = build_constructors seed l } and build_constructors seed l = let module K = Content in List.map (fun (n,t) -> { K.dec_name = Some n; K.dec_id = gen_id declaration_prefix seed; K.dec_inductive = false; K.dec_aref = ""; K.dec_type = t }) l ;; (* and 'term cinductiveType = id * string * bool * 'term * (* typename, inductive, arity *) 'term cconstructor list (* constructors *) and 'term cconstructor = string * 'term *)