X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Facic_content%2Facic2content.ml;fp=components%2Facic_content%2Facic2content.ml;h=b10464bdad1acd6133dd117709e9221f0be55b12;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml new file mode 100644 index 000000000..b10464bda --- /dev/null +++ b/components/acic_content/acic2content.ml @@ -0,0 +1,1179 @@ +(* 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.empty_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.empty_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.empty_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 +*) + +