X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;fp=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=0295daac326659968bb6d8637ad9956583e90afa;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml deleted file mode 100644 index 0295daac3..000000000 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ /dev/null @@ -1,974 +0,0 @@ -(* 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/62003 *) -(* *) -(**************************************************************************) - -(* 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 seed = - let res = "p" ^ 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 -> raise NotImplemented - | 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,t) -> (occur uri s) 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,_,_,_) -> 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) -;; - -(* -let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts = - let module C = Cic in - let module K = Content in - let rec aux l subproofs = - match l with - [] -> [] - | t::l1 -> - if (test_for_lifting t ~ids_to_inner_types) then - (match subproofs with - [] -> assert false - | p::tl -> - let new_arg = - K.Premise - { K.premise_id = gen_id seed; - K.premise_xref = p.K.proof_id; - K.premise_binder = p.K.proof_name; - K.premise_n = None - } - in new_arg::(aux l1 tl)) - 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") in - if sort ="Prop" then - K.Premise - { K.premise_id = gen_id seed; - K.premise_xref = idr; - K.premise_binder = Some b; - K.premise_n = Some n - } - else (K.Term t) - | _ -> (K.Term t)) in - hd::(aux l1 subproofs) - in aux l subproofs -;; -*) - -(* 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 seed; - K.proof_context = [] ; - K.proof_apply_context = []; - K.proof_conclude = - { K.conclude_id = gen_id 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 seed; - K.proof_context = [] ; - K.proof_apply_context = [{inner_proof with K.proof_name = None}]; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "BU_Conversion"; - K.conclude_args = - [K.Premise - { K.premise_id = gen_id 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 = id ; - K.proof_context = [] ; - K.proof_apply_context = []; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "Exact"; - K.conclude_args = [K.Term 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 is_intro 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 = id ; - K.proof_context = [] ; - K.proof_apply_context = []; - K.proof_conclude = - { K.conclude_id = gen_id 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 -> - if is_intro then Some (C.AProd ("gen"^id,n,s,t)) - else Some (C.ALetIn ("gen"^id,n,s,t))) - }; - } -;; - -let build_decl_item seed id n s ~ids_to_inner_sorts = - let module K = Content in - try - let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in - if sort = "Prop" then - `Hypothesis - { K.dec_name = name_of n; - K.dec_id = gen_id seed; - K.dec_inductive = false; - K.dec_aref = id; - K.dec_type = s - } - else - `Declaration - { K.dec_name = name_of n; - K.dec_id = gen_id seed; - K.dec_inductive = false; - K.dec_aref = id; - K.dec_type = s - } - with - Not_found -> assert false -;; - -let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts = - let module C = Cic in - let module K = Content in - let rec aux = - function - [] -> [],[] - | t::l1 -> - let subproofs,args = aux l1 in - if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then - let new_subproof = - acic2content - seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in - let new_arg = - K.Premise - { K.premise_id = gen_id 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") in - if sort ="Prop" then - K.Premise - { K.premise_id = gen_id seed; - K.premise_xref = idr; - K.premise_binder = Some b; - K.premise_n = Some n - } - else (K.Term t) - | C.AConst(id,uri,[]) -> - let sort = - (try Hashtbl.find ids_to_inner_sorts id - with Not_found -> "Type") in - if sort ="Prop" then - K.Lemma - { K.lemma_id = gen_id seed; - K.lemma_name = UriManager.name_of_uri uri; - K.lemma_uri = UriManager.string_of_uri uri - } - else (K.Term t) - | C.AMutConstruct(id,uri,tyno,consno,[]) -> - let sort = - (try Hashtbl.find ids_to_inner_sorts id - with Not_found -> "Type") in - if sort ="Prop" then - let inductive_types = - (match CicEnvironment.get_obj uri with - Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,_) -> l - ) in - let (_,_,_,constructors) = - List.nth inductive_types tyno in - let name,_ = List.nth constructors (consno - 1) in - K.Lemma - { K.lemma_id = gen_id 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 t) - | _ -> (K.Term t)) in - subproofs,hd::args - in - match (aux 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 id n t ~ids_to_inner_sorts ~ids_to_inner_types = - let module K = Content in - try - let sort = Hashtbl.find ids_to_inner_sorts id in - (match name_of n with - Some "w" -> prerr_endline ("build_def: " ^ sort ); - | _ -> ()); - if sort = "Prop" then - (prerr_endline ("entro"); - let p = - (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) - in - (match p.K.proof_name with - Some "w" -> prerr_endline ("TUTTO BENE:"); - | Some s -> prerr_endline ("mi chiamo " ^ s); - | _ -> prerr_endline ("ho perso il nome");); - prerr_endline ("esco"); `Proof p;) - else - (prerr_endline ("siamo qui???"); - `Definition - { K.def_name = name_of n; - K.def_id = gen_id seed; - K.def_aref = id; - K.def_term = t - }) - 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 ?name ~ids_to_inner_sorts ~ids_to_inner_types t = - let rec aux ?name 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 v - | C.ALambda (id,n,s,t) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then - let proof = aux 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 true proof'' name ~ids_to_inner_types - else raise Not_a_proof - | C.ALetIn (id,n,s,t) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then - let proof = aux 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 id n s 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 false proof'' name ~ids_to_inner_types - else raise Not_a_proof - | C.AAppl (id,li) -> - (try rewrite - seed name id li ~ids_to_inner_types ~ids_to_inner_sorts - with NotApplicable -> - try inductive - seed name id li ~ids_to_inner_types ~ids_to_inner_sorts - with NotApplicable -> - let subproofs, args = - build_subproofs_and_args - seed 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 seed; - K.proof_context = []; - K.proof_apply_context = serialize seed subproofs; - K.proof_conclude = - { K.conclude_id = gen_id 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 = - (match CicEnvironment.get_obj uri with - Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,_) -> l - ) in - let (_,_,_,constructors) = List.nth inductive_types typeno in - let teid = get_id te in - let pp = List.map2 - (fun p (name,_) -> (K.ArgProof (aux ~name p))) - patterns constructors in - let context,term = - (match - build_subproofs_and_args - seed ~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 seed; - K.proof_context = []; - K.proof_apply_context = serialize seed context; - K.proof_conclude = - { K.conclude_id = gen_id 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 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 proofs = - List.map - (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in - let decreasing_args = - List.map (function (_,_,n,_,_) -> n) funs in - let jo = - { K.joint_id = gen_id seed; - K.joint_kind = `Recursive decreasing_args; - K.joint_defs = proofs - } - in - { K.proof_name = name; - K.proof_id = gen_id seed; - K.proof_context = [`Joint jo]; - K.proof_apply_context = []; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "Exact"; - K.conclude_args = - [ K.Premise - { K.premise_id = gen_id 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 - } - } - | C.ACoFix (id,no,funs) -> - let proofs = - List.map - (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in - let jo = - { K.joint_id = gen_id seed; - K.joint_kind = `CoRecursive; - K.joint_defs = proofs - } - in - { K.proof_name = name; - K.proof_id = gen_id seed; - K.proof_context = [`Joint jo]; - K.proof_apply_context = []; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "Exact"; - K.conclude_args = - [ K.Premise - { K.premise_id = gen_id 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 t - -and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = - let aux ?name = acic2content seed ~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 (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or - uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists" - else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd" - 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 = - (match CicEnvironment.get_obj ind_uri with - Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,n) -> (l,n) - ) 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 - if method_name = "Exists" then - (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args)); - prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args))); - 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 seed other_args - ~ids_to_inner_types ~ids_to_inner_sorts in - prerr_endline "****** end other *******"; flush stderr; - 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") in - let hdarg = - if sortarg = "Prop" then - let (co,bo) = - let rec bc = - function - Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) -> - let ce = - build_decl_item - seed idl n s1 ~ids_to_inner_sorts in - if (occur ind_uri s) then - ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; - match t1 with - Cic.ALambda(id2,n2,s2,t2) -> - let inductive_hyp = - `Hypothesis - { K.dec_name = name_of n2; - K.dec_id = gen_id seed; - K.dec_inductive = true; - K.dec_aref = id2; - K.dec_type = s2 - } in - let (context,body) = bc (t,t2) in - (ce::inductive_hyp::context,body) - | _ -> assert false) - else - ( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; - let (context,body) = bc (t,t1) in - (ce::context,body)) - | _ , t -> ([],aux t) in - bc (ty,arg) in - K.ArgProof - { bo with - K.proof_name = Some name; - K.proof_context = co; - }; - else (K.Term 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 seed; - K.proof_context = []; - K.proof_apply_context = serialize seed subproofs; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = method_name; - K.conclude_args = - K.Aux (string_of_int no_constructors) - ::K.Term (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 rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = - let aux ?name = acic2content seed ~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 -> - let uri_str = UriManager.string_of_uri uri in - if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or - uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then - let subproofs,arg = - (match - build_subproofs_and_args - seed ~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") in - if asort = "Prop" then - K.ArgProof (aux a) - else K.Term a in - hd::(ma_aux (n-1) tl) in - (ma_aux 3 args) in - { K.proof_name = name; - K.proof_id = gen_id seed; - K.proof_context = []; - K.proof_apply_context = serialize seed subproofs; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "Rewrite"; - K.conclude_args = - K.Term (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 -;; - -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) as item -> item - | (id,Some (name,Cic.ADecl t)) -> - id, - 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 seed; - K.dec_inductive = false; - K.dec_aref = get_id t; - K.dec_type = t - }) - | (id,Some (name,Cic.ADef t)) -> - id, - 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 seed; - K.def_aref = get_id t; - K.def_term = t - }) - ) 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 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 (get_id bo) (C.Name n) bo - ~ids_to_inner_sorts ~ids_to_inner_types)) - | C.AConstant (_,_,n,Some bo,ty,params) -> - (gen_id seed, params, None, - `Def (K.Const,ty, - build_def_item seed (get_id bo) (C.Name n) bo - ~ids_to_inner_sorts ~ids_to_inner_types)) - | C.AConstant (id,_,n,None,ty,params) -> - (gen_id 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 seed, params, None, - `Def (K.Var,ty, - build_def_item seed (get_id bo) (C.Name n) bo - ~ids_to_inner_sorts ~ids_to_inner_types)) - | C.AVariable (id,n,None,ty,params) -> - (gen_id 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 seed, params, None, - `Joint - { K.joint_id = gen_id 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 seed; - 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 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 -*) - -