From: Claudio Sacerdoti Coen Date: Sun, 20 Jul 2003 15:37:04 +0000 (+0000) Subject: cic2content.ml* moved from cic_transformations to cic_omdoc. X-Git-Tag: LucaOK~56 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=9e781c8957ff049e7bba65e1d611e5f007b02fb5 cic2content.ml* moved from cic_transformations to cic_omdoc. --- diff --git a/helm/ocaml/cic_omdoc/.depend b/helm/ocaml/cic_omdoc/.depend index d12896d47..5dfc55b8a 100644 --- a/helm/ocaml/cic_omdoc/.depend +++ b/helm/ocaml/cic_omdoc/.depend @@ -1,4 +1,5 @@ contentPp.cmi: content.cmi +cic2content.cmi: cic2acic.cmi content.cmi content2cic.cmi: content.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi @@ -10,5 +11,7 @@ content.cmo: content.cmi content.cmx: content.cmi contentPp.cmo: content.cmi contentPp.cmi contentPp.cmx: content.cmx contentPp.cmi +cic2content.cmo: cic2acic.cmi content.cmi cic2content.cmi +cic2content.cmx: cic2acic.cmx content.cmx cic2content.cmi content2cic.cmo: content.cmi content2cic.cmi content2cic.cmx: content.cmx content2cic.cmi diff --git a/helm/ocaml/cic_omdoc/Makefile b/helm/ocaml/cic_omdoc/Makefile index e1e081ac6..33f1b3f07 100644 --- a/helm/ocaml/cic_omdoc/Makefile +++ b/helm/ocaml/cic_omdoc/Makefile @@ -3,7 +3,7 @@ REQUIRES = helm-cic_proof_checking PREDICATES = INTERFACE_FILES = eta_fixing.mli doubleTypeInference.mli cic2acic.mli \ - content.mli contentPp.mli content2cic.mli + content.mli contentPp.mli cic2content.mli content2cic.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = \ diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml new file mode 100644 index 000000000..82f0005f5 --- /dev/null +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -0,0 +1,899 @@ +(* 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 = + 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,_,_) -> false + | C.AMeta (id,_,_) -> 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 notfound -> false) + | C.ALambda (id,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.ALetIn (id,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.AAppl (id,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.AConst (id,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.AMutInd (id,_,_,_) -> false + | C.AMutConstruct (id,_,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + (* oppure: false *) + | C.AMutCase (id,_,_,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.AFix (id,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> false) + | C.ACoFix (id,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with notfound -> 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 subrpoofs = + 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 notfound -> "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_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = [] + } in + p.K.proof_apply_context@[p1] + else + [p] +;; + +let rec serialize seed = + function + [] -> [] + | p::tl -> (flat seed p)@(serialize seed tl);; + +(* 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 = None ; + 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]; + K.conclude_conclusion = Some expty + }; + } + else + { K.proof_name = None ; + K.proof_id = gen_id seed; + K.proof_context = [] ; + K.proof_apply_context = [inner_proof]; + 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 notfound -> 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 notfound -> + (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 + 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 + } +;; + +let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = + let module K = Content in + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) + else + `Definition + { K.def_name = name_of n; + K.def_id = gen_id seed; + K.def_aref = id; + K.def_term = t + } + +(* 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 = None) ~ids_to_inner_sorts ~ids_to_inner_types t = + let rec aux ?(name = None) 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 ~name:None 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 = name; + 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 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:(Some "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 notfound -> 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 teid = get_id te in + let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in + (match + (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized + with notfound -> None) + with + Some tety -> (* we must lift up the argument *) + let p = (aux te) in + { K.proof_name = Some "name"; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = flat seed p; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "Case"; + K.conclude_args = (K.Term ty)::(K.Term te)::pp; + K.conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + } + } + | None -> + { K.proof_name = 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 = "Case"; + K.conclude_args = (K.Term ty)::(K.Term te)::pp; + K.conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + } + } + ) + | C.AFix (id, no, [(id1,n,_,ty,bo)]) -> + let proof = (aux bo) in (* must be recursive !! *) + { K.proof_name = name; + K.proof_id = gen_id seed; + K.proof_context = [`Proof proof]; + 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 = proof.K.proof_id; + K.premise_binder = proof.K.proof_name; + K.premise_n = Some 1; + } + ]; + K.conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + } + } + | C.AFix (id, no, funs) -> + let proofs = + List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in + let jo = + { K.joint_id = gen_id seed; + K.joint_kind = `Recursive; + 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 notfound -> None + } + } + | C.ACoFix (id,no,[(id1,n,ty,bo)]) -> + let proof = (aux bo) in (* must be recursive !! *) + { K.proof_name = name; + K.proof_id = gen_id seed; + K.proof_context = [`Proof proof]; + 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 = proof.K.proof_id; + K.premise_binder = proof.K.proof_name; + K.premise_n = Some 1; + } + ]; + K.conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with notfound -> None + } + } + | C.ACoFix (id,no,funs) -> + let proofs = + List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in + let jo = + { K.joint_id = gen_id seed; + K.joint_kind = `Recursive; + 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 notfound -> None + }; + } + in + let id = get_id t in + generate_conversion seed false id t1 ~ids_to_inner_types +in aux ~name:name t + +and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = + let aux ?(name = None) = acic2content seed ~name:None ~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 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 + 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 args_to_lift = + List.filter (test_for_lifting ~ids_to_inner_types) other_args in + let subproofs = + match args_to_lift with + [_] -> List.map aux args_to_lift + | _ -> List.map (aux ~name:(Some "H")) args_to_lift in + prerr_endline "****** end subproofs *******"; flush stderr; + let other_method_args = + build_args seed other_args subproofs + ~ids_to_inner_types ~ids_to_inner_sorts in +(* + let rparams,inductive_arg = + let rec aux = + function + [] -> assert false + | [ia] -> [],ia + | a::tl -> let (p,ia) = aux tl in (a::p,ia) in + aux other_method_args 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 ~name:None) 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 = None; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = subproofs; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "ByInduction"; + K.conclude_args = + K.Aux 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 notfound -> None + } + } + | _ -> raise NotApplicable + +and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = + let aux ?(name = None) = acic2content seed ~name:None ~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 subproof = aux (List.nth args 3) in + let method_args = + let rec ma_aux n = function + [] -> [] + | a::tl -> + let hd = + if n = 0 then + K.Premise + { K.premise_id = gen_id seed; + K.premise_xref = subproof.K.proof_id; + K.premise_binder = None; + K.premise_n = None + } + 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 = None; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = [subproof]; + 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 notfound -> None + } + } + else raise NotApplicable + | _ -> raise NotApplicable +;; + +let map_conjectures + seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty) += + let context' = + List.map + (function + (id,None) as item -> item + | (id,Some (name,Cic.ADecl t)) -> + id, + Some + (build_decl_item seed (get_id t) name t + ~ids_to_inner_sorts) + | (id,Some (name,Cic.ADef t)) -> + id, + Some + (build_def_item seed (get_id t) name t + ~ids_to_inner_sorts ~ids_to_inner_types) + ) 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 +*) + + diff --git a/helm/ocaml/cic_omdoc/cic2content.mli b/helm/ocaml/cic_omdoc/cic2content.mli new file mode 100644 index 000000000..16eb5333f --- /dev/null +++ b/helm/ocaml/cic_omdoc/cic2content.mli @@ -0,0 +1,30 @@ +(* 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/. + *) + +val annobj2content : + ids_to_inner_sorts:(string, string) Hashtbl.t -> + ids_to_inner_types:(string, Cic2acic.anntypes) Hashtbl.t -> + Cic.annobj -> + Cic.annterm Content.cobj diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 459aa8c8b..c7ccf7049 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -3,8 +3,6 @@ content2pres.cmi: mpresentation.cmi cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi cic2Xml.cmo: cic2Xml.cmi cic2Xml.cmx: cic2Xml.cmi -cic2content.cmo: cic2content.cmi -cic2content.cmx: cic2content.cmi content_expressions.cmo: content_expressions.cmi content_expressions.cmx: content_expressions.cmi mpresentation.cmo: mpresentation.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index e1581421e..3a3630640 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -2,7 +2,7 @@ PACKAGE = cic_transformations REQUIRES = helm-xml helm-cic_proof_checking helm-cic_omdoc gdome2-xslt PREDICATES = -INTERFACE_FILES = cic2Xml.mli cic2content.mli content_expressions.mli \ +INTERFACE_FILES = cic2Xml.mli content_expressions.mli \ mpresentation.mli cexpr2pres.mli content2pres.mli \ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ applyStylesheets.mli diff --git a/helm/ocaml/cic_transformations/cic2content.ml b/helm/ocaml/cic_transformations/cic2content.ml deleted file mode 100644 index 3fd8422cc..000000000 --- a/helm/ocaml/cic_transformations/cic2content.ml +++ /dev/null @@ -1,901 +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 = - 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,_,_) -> false - | C.AMeta (id,_,_) -> 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 notfound -> false) - | C.ALambda (id,_,_,_) -> - (try - ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; - true; - with notfound -> false) - | C.ALetIn (id,_,_,_) -> - (try - ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; - true; - with notfound -> false) - | C.AAppl (id,_) -> - (try - ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; - true; - with notfound -> false) - | C.AConst (id,_,_) -> - (try - ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; - true; - with notfound -> false) - | C.AMutInd (id,_,_,_) -> false - | C.AMutConstruct (id,_,_,_,_) -> - (try - ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; - true; - with notfound -> false) - (* oppure: false *) - | C.AMutCase (id,_,_,_,_,_) -> - (try - ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; - true; - with notfound -> false) - | C.AFix (id,_,_) -> - (try - ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; - true; - with notfound -> false) - | C.ACoFix (id,_,_) -> - (try - ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; - true; - with notfound -> 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 subrpoofs = - 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 notfound -> "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_id = gen_id seed; - K.proof_context = []; - K.proof_apply_context = [] - } in - p.K.proof_apply_context@[p1] - else - [p] -;; - -let rec serialize seed = - function - [] -> [] - | p::tl -> (flat seed p)@(serialize seed tl);; - -(* 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 = None ; - 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]; - K.conclude_conclusion = Some expty - }; - } - else - { K.proof_name = None ; - K.proof_id = gen_id seed; - K.proof_context = [] ; - K.proof_apply_context = [inner_proof]; - 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 notfound -> 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 notfound -> - (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 - 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 - } -;; - -let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = - let module K = Content in - let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then - `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) - else - `Definition - { K.def_name = name_of n; - K.def_id = gen_id seed; - K.def_aref = id; - K.def_term = t - } - -(* 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 = None) ~ids_to_inner_sorts ~ids_to_inner_types t = - let rec aux ?(name = None) t = - let module C = Cic in - let module X = Xml in - let module K = Content in - let module U = UriManager 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 ~name:None 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 = name; - 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 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:(Some "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 notfound -> 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 teid = get_id te in - let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in - (match - (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized - with notfound -> None) - with - Some tety -> (* we must lift up the argument *) - let p = (aux te) in - { K.proof_name = Some "name"; - K.proof_id = gen_id seed; - K.proof_context = []; - K.proof_apply_context = flat seed p; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "Case"; - K.conclude_args = (K.Term ty)::(K.Term te)::pp; - K.conclude_conclusion = - try Some - (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None - } - } - | None -> - { K.proof_name = 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 = "Case"; - K.conclude_args = (K.Term ty)::(K.Term te)::pp; - K.conclude_conclusion = - try Some - (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None - } - } - ) - | C.AFix (id, no, [(id1,n,_,ty,bo)]) -> - let proof = (aux bo) in (* must be recursive !! *) - { K.proof_name = name; - K.proof_id = gen_id seed; - K.proof_context = [`Proof proof]; - 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 = proof.K.proof_id; - K.premise_binder = proof.K.proof_name; - K.premise_n = Some 1; - } - ]; - K.conclude_conclusion = - try Some - (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None - } - } - | C.AFix (id, no, funs) -> - let proofs = - List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in - let jo = - { K.joint_id = gen_id seed; - K.joint_kind = `Recursive; - 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 notfound -> None - } - } - | C.ACoFix (id,no,[(id1,n,ty,bo)]) -> - let proof = (aux bo) in (* must be recursive !! *) - { K.proof_name = name; - K.proof_id = gen_id seed; - K.proof_context = [`Proof proof]; - 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 = proof.K.proof_id; - K.premise_binder = proof.K.proof_name; - K.premise_n = Some 1; - } - ]; - K.conclude_conclusion = - try Some - (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None - } - } - | C.ACoFix (id,no,funs) -> - let proofs = - List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in - let jo = - { K.joint_id = gen_id seed; - K.joint_kind = `Recursive; - 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 notfound -> None - }; - } - in - let id = get_id t in - generate_conversion seed false id t1 ~ids_to_inner_types -in aux ~name:name t - -and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = - let aux ?(name = None) = acic2content seed ~name:None ~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 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 - 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 args_to_lift = - List.filter (test_for_lifting ~ids_to_inner_types) other_args in - let subproofs = - match args_to_lift with - [_] -> List.map aux args_to_lift - | _ -> List.map (aux ~name:(Some "H")) args_to_lift in - prerr_endline "****** end subproofs *******"; flush stderr; - let other_method_args = - build_args seed other_args subproofs - ~ids_to_inner_types ~ids_to_inner_sorts in -(* - let rparams,inductive_arg = - let rec aux = - function - [] -> assert false - | [ia] -> [],ia - | a::tl -> let (p,ia) = aux tl in (a::p,ia) in - aux other_method_args 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 ~name:None) 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 = None; - K.proof_id = gen_id seed; - K.proof_context = []; - K.proof_apply_context = subproofs; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "ByInduction"; - K.conclude_args = - K.Aux 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 notfound -> None - } - } - | _ -> raise NotApplicable - -and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = - let aux ?(name = None) = acic2content seed ~name:None ~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 subproof = aux (List.nth args 3) in - let method_args = - let rec ma_aux n = function - [] -> [] - | a::tl -> - let hd = - if n = 0 then - K.Premise - { K.premise_id = gen_id seed; - K.premise_xref = subproof.K.proof_id; - K.premise_binder = None; - K.premise_n = None - } - 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 = None; - K.proof_id = gen_id seed; - K.proof_context = []; - K.proof_apply_context = [subproof]; - 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 notfound -> None - } - } - else raise NotApplicable - | _ -> raise NotApplicable -;; - -let map_conjectures - seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty) -= - let context' = - List.map - (function - (id,None) as item -> item - | (id,Some (name,Cic.ADecl t)) -> - id, - Some - (build_decl_item seed (get_id t) name t - ~ids_to_inner_sorts) - | (id,Some (name,Cic.ADef t)) -> - id, - Some - (build_def_item seed (get_id t) name t - ~ids_to_inner_sorts ~ids_to_inner_types) - ) 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 -*) - - diff --git a/helm/ocaml/cic_transformations/cic2content.mli b/helm/ocaml/cic_transformations/cic2content.mli deleted file mode 100644 index 16eb5333f..000000000 --- a/helm/ocaml/cic_transformations/cic2content.mli +++ /dev/null @@ -1,30 +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/. - *) - -val annobj2content : - ids_to_inner_sorts:(string, string) Hashtbl.t -> - ids_to_inner_types:(string, Cic2acic.anntypes) Hashtbl.t -> - Cic.annobj -> - Cic.annterm Content.cobj