From: Claudio Sacerdoti Coen Date: Sun, 20 Jul 2003 11:23:58 +0000 (+0000) Subject: cic_transformations factorized into cic_omdoc and cic_transformations. X-Git-Tag: LucaOK~59 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4bcd14a9ed245ccae631697a05ff5a377c02b179 cic_transformations factorized into cic_omdoc and cic_transformations. --- diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore index 53ffeac63..3a94cf124 100644 --- a/helm/ocaml/.cvsignore +++ b/helm/ocaml/.cvsignore @@ -16,6 +16,7 @@ META.helm-tactics META.helm-urimanager META.helm-xml META.helm-cic_transformations +META.helm-cic_omdoc Makefile Makefile.common autom4te.cache diff --git a/helm/ocaml/META.helm-cic_omdoc.src b/helm/ocaml/META.helm-cic_omdoc.src new file mode 100644 index 000000000..313d19cd2 --- /dev/null +++ b/helm/ocaml/META.helm-cic_omdoc.src @@ -0,0 +1,4 @@ +requires="helm-cic_proof_checking" +version="0.0.1" +archive(byte)="cic_omdoc.cma" +archive(native)="cic_omdoc.cmxa" diff --git a/helm/ocaml/META.helm-cic_transformations.src b/helm/ocaml/META.helm-cic_transformations.src index 1888f9d39..44bb0999c 100644 --- a/helm/ocaml/META.helm-cic_transformations.src +++ b/helm/ocaml/META.helm-cic_transformations.src @@ -1,4 +1,4 @@ -requires="helm-xml helm-cic_proof_checking gdome2-xslt" +requires="helm-xml helm-cic_proof_checking helm-cic_omdoc gdome2-xslt" version="0.0.1" archive(byte)="cic_transformations.cma" archive(native)="cic_transformations.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index aaf8595b1..8eae88814 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -2,7 +2,7 @@ MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ cic_cache cic_proof_checking cic_textual_parser \ tex_cic_textual_parser cic_unification mathql mathql_interpreter \ - mathql_generator tactics cic_transformations + mathql_generator cic_omdoc tactics cic_transformations OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/cic_omdoc/.depend b/helm/ocaml/cic_omdoc/.depend new file mode 100644 index 000000000..1ec905424 --- /dev/null +++ b/helm/ocaml/cic_omdoc/.depend @@ -0,0 +1,9 @@ +contentPp.cmi: content.cmi +doubleTypeInference.cmo: doubleTypeInference.cmi +doubleTypeInference.cmx: doubleTypeInference.cmi +cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi +cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi +content.cmo: content.cmi +content.cmx: content.cmi +contentPp.cmo: content.cmi contentPp.cmi +contentPp.cmx: content.cmx contentPp.cmi diff --git a/helm/ocaml/cic_omdoc/Makefile b/helm/ocaml/cic_omdoc/Makefile new file mode 100644 index 000000000..0fbb566ae --- /dev/null +++ b/helm/ocaml/cic_omdoc/Makefile @@ -0,0 +1,12 @@ +PACKAGE = cic_omdoc +REQUIRES = helm-cic_proof_checking +PREDICATES = + +INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli content.mli \ + contentPp.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +EXTRA_OBJECTS_TO_INSTALL = \ +EXTRA_OBJECTS_TO_CLEAN = + +include ../Makefile.common diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml new file mode 100644 index 000000000..a3cdfbb78 --- /dev/null +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -0,0 +1,408 @@ +(* 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/. + *) + +type anntypes = + {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} +;; + +let gen_id seed = + let res = "i" ^ string_of_int !seed in + incr seed ; + res +;; + +let fresh_id seed ids_to_terms ids_to_father_ids = + fun father t -> + let res = gen_id seed in + Hashtbl.add ids_to_father_ids res father ; + Hashtbl.add ids_to_terms res t ; + res +;; + +let source_id_of_id id = "#source#" ^ id;; + +exception NotEnoughElements;; +exception NameExpected;; + +(*CSC: cut&paste da cicPp.ml *) +(* get_nth l n returns the nth element of the list l if it exists or *) +(* raises NotEnoughElements if l has less than n elements *) +let rec get_nth l n = + match (n,l) with + (1, he::_) -> he + | (n, he::tail) when n > 1 -> get_nth tail (n-1) + | (_,_) -> raise NotEnoughElements +;; + +let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts + ids_to_inner_types metasenv context idrefs t expectedty += + let module D = DoubleTypeInference in + let module T = CicTypeChecker in + let module C = Cic in + let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in + let terms_to_types = + D.double_type_of metasenv context t expectedty + in + let rec aux computeinnertypes father context idrefs tt = + let fresh_id'' = fresh_id' father tt in + (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) + let aux' = aux computeinnertypes (Some fresh_id'') in + (* First of all we compute the inner type and the inner sort *) + (* of the term. They may be useful in what follows. *) + (*CSC: This is a very inefficient way of computing inner types *) + (*CSC: and inner sorts: very deep terms have their types/sorts *) + (*CSC: computed again and again. *) + let string_of_sort t = + match CicReduction.whd context t with + C.Sort C.Prop -> "Prop" + | C.Sort C.Set -> "Set" + | C.Sort C.Type -> "Type" + | _ -> assert false + in + let ainnertypes,innertype,innersort,expected_available = +(*CSC: Here we need the algorithm for Coscoy's double type-inference *) +(*CSC: (expected type + inferred type). Just for now we use the usual *) +(*CSC: type-inference, but the result is very poor. As a very weak *) +(*CSC: patch, I apply whd to the computed type. Full beta *) +(*CSC: reduction would be a much better option. *) + let {D.synthesized = synthesized; D.expected = expected} = + if computeinnertypes then + D.CicHash.find terms_to_types tt + else + (* We are already in an inner-type and Coscoy's double *) + (* type inference algorithm has not been applied. *) + {D.synthesized = + CicReduction.whd context (T.type_of_aux' metasenv context tt) ; + D.expected = None} + in + let innersort = T.type_of_aux' metasenv context synthesized in + let ainnertypes,expected_available = + if computeinnertypes then + let annexpected,expected_available = + match expected with + None -> None,false + | Some expectedty' -> + Some + (aux false (Some fresh_id'') context idrefs expectedty'), + true + in + Some + {annsynthesized = + aux false (Some fresh_id'') context idrefs synthesized ; + annexpected = annexpected + }, expected_available + else + None,false + in + ainnertypes,synthesized, string_of_sort innersort, expected_available + in + let add_inner_type id = + match ainnertypes with + None -> () + | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes + in + match tt with + C.Rel n -> + let id = + match get_nth context n with + (Some (C.Name s,_)) -> s + | _ -> raise NameExpected + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + C.ARel (fresh_id'', List.nth idrefs (n-1), n, id) + | C.Var (uri,exp_named_subst) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + let exp_named_subst' = + List.map + (function i,t -> i, (aux' context idrefs t)) exp_named_subst + in + C.AVar (fresh_id'', uri,exp_named_subst') + | C.Meta (n,l) -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> n = m) metasenv + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + C.AMeta (fresh_id'', n, + (List.map2 + (fun ct t -> + match (ct, t) with + | None, _ -> None + | _, Some t -> Some (aux' context idrefs t) + | Some _, None -> assert false (* due to typing rules *)) + canonical_context l)) + | C.Sort s -> C.ASort (fresh_id'', s) + | C.Implicit -> C.AImplicit (fresh_id'') + | C.Cast (v,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t) + | C.Prod (n,s,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' + (string_of_sort innertype) ; + let sourcetype = T.type_of_aux' metasenv context s in + Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + (string_of_sort sourcetype) ; + let n' = + match n with + C.Anonymous -> n + | C.Name n' -> + if D.does_not_occur 1 t then + C.Anonymous + else + C.Name n' + in + C.AProd + (fresh_id'', n', aux' context idrefs s, + aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t) + | C.Lambda (n,s,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + let sourcetype = T.type_of_aux' metasenv context s in + Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + (string_of_sort sourcetype) ; + if innersort = "Prop" then + begin + let father_is_lambda = + match father with + None -> false + | Some father' -> + match Hashtbl.find ids_to_terms father' with + C.Lambda _ -> true + | _ -> false + in + if (not father_is_lambda) || expected_available then + add_inner_type fresh_id'' + end ; + C.ALambda + (fresh_id'',n, aux' context idrefs s, + aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t) + | C.LetIn (n,s,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.ALetIn + (fresh_id'', n, aux' context idrefs s, + aux' ((Some (n, C.Def s))::context) (fresh_id''::idrefs) t) + | C.Appl l -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.AAppl (fresh_id'', List.map (aux' context idrefs) l) + | C.Const (uri,exp_named_subst) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + let exp_named_subst' = + List.map + (function i,t -> i, (aux' context idrefs t)) exp_named_subst + in + C.AConst (fresh_id'', uri, exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (aux' context idrefs t)) exp_named_subst + in + C.AMutInd (fresh_id'', uri, tyno, exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + let exp_named_subst' = + List.map + (function i,t -> i, (aux' context idrefs t)) exp_named_subst + in + C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst') + | C.MutCase (uri, tyno, outty, term, patterns) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty, + aux' context idrefs term, List.map (aux' context idrefs) patterns) + | C.Fix (funno, funs) -> + let fresh_idrefs = + List.map (function _ -> gen_id seed) funs in + let new_idrefs = List.rev fresh_idrefs @ idrefs in + let tys = + List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.AFix (fresh_id'', funno, + List.map2 + (fun id (name, indidx, ty, bo) -> + (id, name, indidx, aux' context idrefs ty, + aux' (tys@context) new_idrefs bo) + ) fresh_idrefs funs + ) + | C.CoFix (funno, funs) -> + let fresh_idrefs = + List.map (function _ -> gen_id seed) funs in + let new_idrefs = List.rev fresh_idrefs @ idrefs in + let tys = + List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.ACoFix (fresh_id'', funno, + List.map2 + (fun id (name, ty, bo) -> + (id, name, aux' context idrefs ty, + aux' (tys@context) new_idrefs bo) + ) fresh_idrefs funs + ) + in + aux true None context idrefs t +;; + +let acic_of_cic_context metasenv context idrefs t = + let ids_to_terms = Hashtbl.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in + let seed = ref 0 in + acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts + ids_to_inner_types metasenv context idrefs t, + ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types +;; + +let acic_object_of_cic_object obj = + let module C = Cic in + let ids_to_terms = Hashtbl.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in + let ids_to_conjectures = Hashtbl.create 11 in + let ids_to_hypotheses = Hashtbl.create 127 in + let hypotheses_seed = ref 0 in + let conjectures_seed = ref 0 in + let seed = ref 0 in + let acic_term_of_cic_term_context' = + acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts + ids_to_inner_types in + let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in + let aobj = + match obj with + C.Constant (id,Some bo,ty,params) -> + let abo = acic_term_of_cic_term' bo (Some ty) in + let aty = acic_term_of_cic_term' ty None in + C.AConstant + ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params) + | C.Constant (id,None,ty,params) -> + let aty = acic_term_of_cic_term' ty None in + C.AConstant + ("mettereaposto",None,id,None,aty, params) + | C.Variable (id,bo,ty,params) -> + let abo = + match bo with + None -> None + | Some bo -> Some (acic_term_of_cic_term' bo (Some ty)) + in + let aty = acic_term_of_cic_term' ty None in + C.AVariable + ("mettereaposto",id,abo,aty, params) + | C.CurrentProof (id,conjectures,bo,ty,params) -> + let aconjectures = + List.map + (function (i,canonical_context,term) as conjecture -> + let cid = "c" ^ string_of_int !conjectures_seed in + Hashtbl.add ids_to_conjectures cid conjecture ; + incr conjectures_seed ; + let idrefs',revacanonical_context = + let rec aux context idrefs = + function + [] -> idrefs,[] + | hyp::tl -> + let hid = "h" ^ string_of_int !hypotheses_seed in + let new_idrefs = hid::idrefs in + Hashtbl.add ids_to_hypotheses hid hyp ; + incr hypotheses_seed ; + match hyp with + (Some (n,C.Decl t)) -> + let final_idrefs,atl = + aux (hyp::context) new_idrefs tl in + let at = + acic_term_of_cic_term_context' + conjectures context idrefs t None + in + final_idrefs,(hid,Some (n,C.ADecl at))::atl + | (Some (n,C.Def t)) -> + let final_idrefs,atl = + aux (hyp::context) new_idrefs tl in + let at = + acic_term_of_cic_term_context' + conjectures context idrefs t None + in + final_idrefs,(hid,Some (n,C.ADef at))::atl + | None -> + let final_idrefs,atl = + aux (hyp::context) new_idrefs tl + in + final_idrefs,(hid,None)::atl + in + aux [] [] (List.rev canonical_context) + in + let aterm = + acic_term_of_cic_term_context' conjectures + canonical_context idrefs' term None + in + (cid,i,(List.rev revacanonical_context),aterm) + ) conjectures in + let abo = + acic_term_of_cic_term_context' conjectures [] [] bo (Some ty) in + let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in + C.ACurrentProof + ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params) + | C.InductiveDefinition (tys,params,paramsno) -> + let context = + List.map + (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in + let idrefs = List.map (function _ -> gen_id seed) tys in + let atys = + List.map2 + (fun id (name,inductive,ty,cons) -> + let acons = + List.map + (function (name,ty) -> + (name, + acic_term_of_cic_term_context' [] context idrefs ty None) + ) cons + in + (id,name,inductive,acic_term_of_cic_term' ty None,acons) + ) (List.rev idrefs) tys + in + C.AInductiveDefinition ("mettereaposto",atys,params,paramsno) + in + aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types, + ids_to_conjectures,ids_to_hypotheses +;; diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli new file mode 100644 index 000000000..b34d34342 --- /dev/null +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -0,0 +1,56 @@ +(* 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/. + *) + +exception NotEnoughElements +exception NameExpected + +val source_id_of_id : string -> string + +type anntypes = + {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} +;; + +val acic_of_cic_context' : + int ref -> (* seed *) + (Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *) + (Cic.id, string) Hashtbl.t -> (* ids_to_inner_sorts *) + (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *) + Cic.metasenv -> (* metasenv *) + Cic.context -> (* context *) + Cic.id list -> (* idrefs *) + Cic.term -> (* term *) + Cic.term option -> (* expected type *) + Cic.annterm (* annotated term *) + +val acic_object_of_cic_object : + Cic.obj -> (* object *) + Cic.annobj * (* annotated object *) + (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) + (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *) + (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *) + (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml new file mode 100644 index 000000000..be46f5961 --- /dev/null +++ b/helm/ocaml/cic_omdoc/content.ml @@ -0,0 +1,159 @@ +(* 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 *) +(* *) +(**************************************************************************) + +type id = string;; +type joint_recursion_kind = + [ `Recursive + | `CoRecursive + | `Inductive of int (* paramsno *) + | `CoInductive of int (* paramsno *) + ] +;; + +type var_or_const = Var | Const;; + +type 'term declaration = + { dec_name : string option; + dec_id : string ; + dec_inductive : bool; + dec_aref : string; + dec_type : 'term + } +;; + +type 'term definition = + { def_name : string option; + def_id : string ; + def_aref : string ; + def_term : 'term + } +;; + +type 'term inductive = + { inductive_id : string ; + inductive_kind : bool; + inductive_type : 'term; + inductive_constructors : 'term declaration list + } +;; + +type 'term decl_context_element = + [ `Declaration of 'term declaration + | `Hypothesis of 'term declaration + ] +;; + +type ('term,'proof) def_context_element = + [ `Proof of 'proof + | `Definition of 'term definition + ] +;; + +type ('term,'proof) in_joint_context_element = + [ `Inductive of 'term inductive + | 'term decl_context_element + | ('term,'proof) def_context_element + ] +;; + +type ('term,'proof) joint = + { joint_id : string ; + joint_kind : joint_recursion_kind ; + joint_defs : ('term,'proof) in_joint_context_element list + } +;; + +type ('term,'proof) joint_context_element = + [ `Joint of ('term,'proof) joint ] +;; + +type 'term proof = + { proof_name : string option; + proof_id : string ; + proof_context : 'term in_proof_context_element list ; + proof_apply_context: 'term proof list; + proof_conclude : 'term conclude_item + } + +and 'term in_proof_context_element = + [ 'term decl_context_element + | ('term,'term proof) def_context_element + | ('term,'term proof) joint_context_element + ] + +and 'term conclude_item = + { conclude_id :string; + conclude_aref : string; + conclude_method : string; + conclude_args : ('term arg) list ; + conclude_conclusion : 'term option + } + +and 'term arg = + Aux of int + | Premise of premise + | Term of 'term + | ArgProof of 'term proof + | ArgMethod of string (* ???? *) + +and premise = + { premise_id: string; + premise_xref : string ; + premise_binder : string option; + premise_n : int option; + } +;; + +type 'term conjecture = id * int * 'term context * 'term + +and 'term context = 'term hypothesis list + +and 'term hypothesis = + id * + ['term decl_context_element | ('term,'term proof) def_context_element ] option +;; + +type 'term in_object_context_element = + [ `Decl of var_or_const * 'term decl_context_element + | `Def of var_or_const * 'term * ('term,'term proof) def_context_element + | ('term,'term proof) joint_context_element + ] +;; + +type 'term cobj = + id * (* id *) + UriManager.uri list * (* params *) + 'term conjecture list option * (* optional metasenv *) + 'term in_object_context_element (* actual object *) +;; diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli new file mode 100644 index 000000000..b58b84b54 --- /dev/null +++ b/helm/ocaml/cic_omdoc/content.mli @@ -0,0 +1,150 @@ +(* 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/. + *) + +type id = string;; +type joint_recursion_kind = + [ `Recursive + | `CoRecursive + | `Inductive of int (* paramsno *) + | `CoInductive of int (* paramsno *) + ] +;; + +type var_or_const = Var | Const;; + +type 'term declaration = + { dec_name : string option; + dec_id : string ; + dec_inductive : bool; + dec_aref : string; + dec_type : 'term + } +;; + +type 'term definition = + { def_name : string option; + def_id : string ; + def_aref : string ; + def_term : 'term + } +;; + +type 'term inductive = + { inductive_id : string ; + inductive_kind : bool; + inductive_type : 'term; + inductive_constructors : 'term declaration list + } +;; + +type 'term decl_context_element = + [ `Declaration of 'term declaration + | `Hypothesis of 'term declaration + ] +;; + +type ('term,'proof) def_context_element = + [ `Proof of 'proof + | `Definition of 'term definition + ] +;; + +type ('term,'proof) in_joint_context_element = + [ `Inductive of 'term inductive + | 'term decl_context_element + | ('term,'proof) def_context_element + ] +;; + +type ('term,'proof) joint = + { joint_id : string ; + joint_kind : joint_recursion_kind ; + joint_defs : ('term,'proof) in_joint_context_element list + } +;; + +type ('term,'proof) joint_context_element = + [ `Joint of ('term,'proof) joint ] +;; + +type 'term proof = + { proof_name : string option; + proof_id : string ; + proof_context : 'term in_proof_context_element list ; + proof_apply_context: 'term proof list; + proof_conclude : 'term conclude_item + } + +and 'term in_proof_context_element = + [ 'term decl_context_element + | ('term,'term proof) def_context_element + | ('term,'term proof) joint_context_element + ] + +and 'term conclude_item = + { conclude_id :string; + conclude_aref : string; + conclude_method : string; + conclude_args : ('term arg) list ; + conclude_conclusion : 'term option + } + +and 'term arg = + Aux of int + | Premise of premise + | Term of 'term + | ArgProof of 'term proof + | ArgMethod of string (* ???? *) + +and premise = + { premise_id: string; + premise_xref : string ; + premise_binder : string option; + premise_n : int option; + } +;; + +type 'term conjecture = id * int * 'term context * 'term + +and 'term context = 'term hypothesis list + +and 'term hypothesis = + id * + ['term decl_context_element | ('term,'term proof) def_context_element ] option +;; + +type 'term in_object_context_element = + [ `Decl of var_or_const * 'term decl_context_element + | `Def of var_or_const * 'term * ('term,'term proof) def_context_element + | ('term,'term proof) joint_context_element + ] +;; + +type 'term cobj = + id * (* id *) + UriManager.uri list * (* params *) + 'term conjecture list option * (* optional metasenv *) + 'term in_object_context_element (* actual object *) +;; diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml new file mode 100644 index 000000000..3bc8bb306 --- /dev/null +++ b/helm/ocaml/cic_omdoc/contentPp.ml @@ -0,0 +1,146 @@ +(* 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 *) +(* 17/06/2003 *) +(* *) +(***************************************************************************) + +exception ContentPpInternalError;; +exception NotEnoughElements;; +exception TO_DO + +(* Utility functions *) + + +let string_of_name = + function + Some s -> s + | None -> "_" +;; + +(* get_nth l n returns the nth element of the list l if it exists or *) +(* raises NotEnoughElements if l has less than n elements *) +let rec get_nth l n = + match (n,l) with + (1, he::_) -> he + | (n, he::tail) when n > 1 -> get_nth tail (n-1) + | (_,_) -> raise NotEnoughElements +;; + +let rec blanks n = + if n = 0 then "" + else (" " ^ (blanks (n-1)));; + +let rec pproof (p: Cic.annterm Content.proof) indent = + let module Con = Content in + let new_indent = + (match p.Con.proof_name with + Some s -> + prerr_endline + ((blanks indent) ^ "(" ^ s ^ ")"); flush stderr ;(indent + 1) + | None ->indent) in + let new_indent1 = + if (p.Con.proof_context = []) then new_indent + else + (pcontext p.Con.proof_context new_indent; (new_indent + 1)) in + papply_context p.Con.proof_apply_context new_indent1; + pconclude p.Con.proof_conclude new_indent1; + +and pcontext c indent = + List.iter (pcontext_element indent) c + +and pcontext_element indent = + let module Con = Content in + function + `Declaration d -> + (match d.Con.dec_name with + Some s -> + prerr_endline + ((blanks indent) + ^ "Assume " ^ s ^ " : " + ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.dec_type))); + flush stderr + | None -> + prerr_endline ((blanks indent) ^ "NO NAME!!")) + | `Hypothesis h -> + (match h.Con.dec_name with + Some s -> + prerr_endline + ((blanks indent) + ^ "Suppose " ^ s ^ " : " + ^ (CicPp.ppterm (Deannotate.deannotate_term h.Con.dec_type))); + flush stderr + | None -> + prerr_endline ((blanks indent) ^ "NO NAME!!")) + | `Proof p -> pproof p indent + | `Definition d -> + (match d.Con.def_name with + Some s -> + prerr_endline + ((blanks indent) ^ "Let " ^ s ^ " = " + ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.def_term))); + flush stderr + | None -> + prerr_endline ((blanks indent) ^ "NO NAME!!")) + | `Joint ho -> + prerr_endline ((blanks indent) ^ "Joint Def"); + flush stderr + +and papply_context ac indent = + List.iter(function p -> (pproof p indent)) ac + +and pconclude concl indent = + let module Con = Content in + prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr; + pargs concl.Con.conclude_args indent; + match concl.Con.conclude_conclusion with + None -> prerr_endline ((blanks indent) ^"No conclude conclusion");flush stderr + | Some t -> prerr_endline ((blanks indent) ^ "conclude" ^ concl.Con.conclude_method ^ (CicPp.ppterm (Deannotate.deannotate_term t)));flush stderr + +and pargs args indent = + List.iter (parg indent) args + +and parg indent = + let module Con = Content in + function + Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ (string_of_int n));flush stderr + | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr + | Con.Term t -> + prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t))); + flush stderr + | Con.ArgProof p -> pproof p (indent+1) + | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr +;; + +let print_proof p = pproof p 0; + + + + diff --git a/helm/ocaml/cic_omdoc/contentPp.mli b/helm/ocaml/cic_omdoc/contentPp.mli new file mode 100644 index 000000000..85ce238f3 --- /dev/null +++ b/helm/ocaml/cic_omdoc/contentPp.mli @@ -0,0 +1,28 @@ +(* 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 print_proof: Cic.annterm Content.proof -> unit + + diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml new file mode 100644 index 000000000..71422ced1 --- /dev/null +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -0,0 +1,687 @@ +(* 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/. + *) + +exception Impossible of int;; +exception NotWellTyped of string;; +exception WrongUriToConstant of string;; +exception WrongUriToVariable of string;; +exception WrongUriToMutualInductiveDefinitions of string;; +exception ListTooShort;; +exception RelToHiddenHypothesis;; + +type types = {synthesized : Cic.term ; expected : Cic.term option};; + +(* does_not_occur n te *) +(* returns [true] if [Rel n] does not occur in [te] *) +let rec does_not_occur n = + let module C = Cic in + function + C.Rel m when m = n -> false + | C.Rel _ + | C.Meta _ + | C.Sort _ + | C.Implicit -> true + | C.Cast (te,ty) -> + does_not_occur n te && does_not_occur n ty + | C.Prod (name,so,dest) -> + does_not_occur n so && + does_not_occur (n + 1) dest + | C.Lambda (name,so,dest) -> + does_not_occur n so && + does_not_occur (n + 1) dest + | C.LetIn (name,so,dest) -> + does_not_occur n so && + does_not_occur (n + 1) dest + | C.Appl l -> + List.fold_right (fun x i -> i && does_not_occur n x) l true + | C.Var (_,exp_named_subst) + | C.Const (_,exp_named_subst) + | C.MutInd (_,_,exp_named_subst) + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.fold_right (fun (_,x) i -> i && does_not_occur n x) + exp_named_subst true + | C.MutCase (_,_,out,te,pl) -> + does_not_occur n out && does_not_occur n te && + List.fold_right (fun x i -> i && does_not_occur n x) pl true + | C.Fix (_,fl) -> + let len = List.length fl in + let n_plus_len = n + len in + let tys = + List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + in + List.fold_right + (fun (_,_,ty,bo) i -> + i && does_not_occur n ty && + does_not_occur n_plus_len bo + ) fl true + | C.CoFix (_,fl) -> + let len = List.length fl in + let n_plus_len = n + len in + let tys = + List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + in + List.fold_right + (fun (_,ty,bo) i -> + i && does_not_occur n ty && + does_not_occur n_plus_len bo + ) fl true +;; + +(*CSC: potrebbe creare applicazioni di applicazioni *) +(*CSC: ora non e' piu' head, ma completa!!! *) +let rec head_beta_reduce = + let module S = CicSubstitution in + let module C = Cic in + function + C.Rel _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + in + C.Var (uri,exp_named_subst) + | C.Meta (n,l) -> + C.Meta (n, + List.map + (function None -> None | Some t -> Some (head_beta_reduce t)) l + ) + | C.Sort _ as t -> t + | C.Implicit -> assert false + | C.Cast (te,ty) -> + C.Cast (head_beta_reduce te, head_beta_reduce ty) + | C.Prod (n,s,t) -> + C.Prod (n, head_beta_reduce s, head_beta_reduce t) + | C.Lambda (n,s,t) -> + C.Lambda (n, head_beta_reduce s, head_beta_reduce t) + | C.LetIn (n,s,t) -> + C.LetIn (n, head_beta_reduce s, head_beta_reduce t) + | C.Appl ((C.Lambda (name,s,t))::he::tl) -> + let he' = S.subst he t in + if tl = [] then + head_beta_reduce he' + else + head_beta_reduce (C.Appl (he'::tl)) + | C.Appl l -> + C.Appl (List.map head_beta_reduce l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = + List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = + List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t, + List.map head_beta_reduce pl) + | C.Fix (i,fl) -> + let fl' = + List.map + (function (name,i,ty,bo) -> + name,i,head_beta_reduce ty,head_beta_reduce bo + ) fl + in + C.Fix (i,fl') + | C.CoFix (i,fl) -> + let fl' = + List.map + (function (name,ty,bo) -> + name,head_beta_reduce ty,head_beta_reduce bo + ) fl + in + C.CoFix (i,fl') +;; + +(* syntactic_equality up to cookingsno for uris *) +(* (which is often syntactically irrilevant), *) +(* distinction between fake dependent products *) +(* and non-dependent products, alfa-conversion *) +(*CSC: must alfa-conversion be considered or not? *) +let syntactic_equality t t' = + let module C = Cic in + let rec syntactic_equality t t' = + if t = t' then true + else + match t, t' with + C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') -> + UriManager.eq uri uri' && + syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' + | C.Cast (te,ty), C.Cast (te',ty') -> + syntactic_equality te te' && + syntactic_equality ty ty' + | C.Prod (_,s,t), C.Prod (_,s',t') -> + syntactic_equality s s' && + syntactic_equality t t' + | C.Lambda (_,s,t), C.Lambda (_,s',t') -> + syntactic_equality s s' && + syntactic_equality t t' + | C.LetIn (_,s,t), C.LetIn(_,s',t') -> + syntactic_equality s s' && + syntactic_equality t t' + | C.Appl l, C.Appl l' -> + List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' + | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') -> + UriManager.eq uri uri' && + syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' + | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') -> + UriManager.eq uri uri' && i = i' && + syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' + | C.MutConstruct (uri,i,j,exp_named_subst), + C.MutConstruct (uri',i',j',exp_named_subst') -> + UriManager.eq uri uri' && i = i' && j = j' && + syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' + | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> + UriManager.eq sp sp' && i = i' && + syntactic_equality outt outt' && + syntactic_equality t t' && + List.fold_left2 + (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' + | C.Fix (i,fl), C.Fix (i',fl') -> + i = i' && + List.fold_left2 + (fun b (_,i,ty,bo) (_,i',ty',bo') -> + b && i = i' && + syntactic_equality ty ty' && + syntactic_equality bo bo') true fl fl' + | C.CoFix (i,fl), C.CoFix (i',fl') -> + i = i' && + List.fold_left2 + (fun b (_,ty,bo) (_,ty',bo') -> + b && + syntactic_equality ty ty' && + syntactic_equality bo bo') true fl fl' + | _, _ -> false (* we already know that t != t' *) + and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 = + List.fold_left2 + (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true + exp_named_subst1 exp_named_subst2 + in + try + syntactic_equality t t' + with + _ -> false +;; + +let rec split l n = + match (l,n) with + (l,0) -> ([], l) + | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) + | (_,_) -> raise ListTooShort +;; + +let type_of_constant uri = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + raise (NotWellTyped "Reference to an unchecked constant") + in + match cobj with + C.Constant (_,_,ty,_) -> ty + | C.CurrentProof (_,_,_,ty,_) -> ty + | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) +;; + +let type_of_variable uri = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + match CicEnvironment.is_type_checked uri with + CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty + | CicEnvironment.UncheckedObj (C.Variable _) -> + raise (NotWellTyped "Reference to an unchecked variable") + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) +;; + +let type_of_mutual_inductive_defs uri i = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + raise (NotWellTyped "Reference to an unchecked inductive type") + in + match cobj with + C.InductiveDefinition (dl,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity + | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) +;; + +let type_of_mutual_inductive_constr uri i j = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + raise (NotWellTyped "Reference to an unchecked constructor") + in + match cobj with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cl) = List.nth dl i in + let (_,ty) = List.nth cl (j-1) in + ty + | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) +;; + +module CicHash = + Hashtbl.Make + (struct + type t = Cic.term + let equal = (==) + let hash = Hashtbl.hash + end) +;; + +(* type_of_aux' is just another name (with a different scope) for type_of_aux *) +let rec type_of_aux' subterms_to_types metasenv context t expectedty = + (* Coscoy's double type-inference algorithm *) + (* It computes the inner-types of every subterm of [t], *) + (* even when they are not needed to compute the types *) + (* of other terms. *) + let rec type_of_aux context t expectedty = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let module U = UriManager in + let synthesized = + match t with + C.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Decl t) -> S.lift n t + | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty + | None -> raise RelToHiddenHypothesis + with + _ -> raise (NotWellTyped "Not a close term") + ) + | C.Var (uri,exp_named_subst) -> + visit_exp_named_subst context uri exp_named_subst ; + CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) + | C.Meta (n,l) -> + (* Let's visit all the subterms that will not be visited later *) + let (_,canonical_context,_) = + List.find (function (m,_,_) -> n = m) metasenv + in + let lifted_canonical_context = + let rec aux i = + function + [] -> [] + | (Some (n,C.Decl t))::tl -> + (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + | (Some (n,C.Def t))::tl -> + (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + | None::tl -> None::(aux (i+1) tl) + in + aux 1 canonical_context + in + let _ = + List.iter2 + (fun t ct -> + match t,ct with + _,None -> () + | Some t,Some (_,C.Def ct) -> + let expected_type = + R.whd context + (CicTypeChecker.type_of_aux' metasenv context ct) + in + (* Maybe I am a bit too paranoid, because *) + (* if the term is well-typed than t and ct *) + (* are convertible. Nevertheless, I compute *) + (* the expected type. *) + ignore (type_of_aux context t (Some expected_type)) + | Some t,Some (_,C.Decl ct) -> + ignore (type_of_aux context t (Some ct)) + | _,_ -> assert false (* the term is not well typed!!! *) + ) l lifted_canonical_context + in + let (_,canonical_context,ty) = + List.find (function (m,_,_) -> n = m) metasenv + in + (* Checks suppressed *) + CicSubstitution.lift_meta l ty + | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | C.Implicit -> raise (Impossible 21) + | C.Cast (te,ty) -> + (* Let's visit all the subterms that will not be visited later *) + let _ = type_of_aux context te (Some (head_beta_reduce ty)) in + let _ = type_of_aux context ty None in + (* Checks suppressed *) + ty + | C.Prod (name,s,t) -> + let sort1 = type_of_aux context s None + and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in + sort_of_prod context (name,s) (sort1,sort2) + | C.Lambda (n,s,t) -> + (* Let's visit all the subterms that will not be visited later *) + let _ = type_of_aux context s None in + let expected_target_type = + match expectedty with + None -> None + | Some expectedty' -> + let ty = + match R.whd context expectedty' with + C.Prod (_,_,expected_target_type) -> + head_beta_reduce expected_target_type + | _ -> assert false + in + Some ty + in + let type2 = + type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type + in + (* Checks suppressed *) + C.Prod (n,s,type2) + | C.LetIn (n,s,t) -> +(*CSC: What are the right expected types for the source and *) +(*CSC: target of a LetIn? None used. *) + (* Let's visit all the subterms that will not be visited later *) + let _ = type_of_aux context s None in + let t_typ = + (* Checks suppressed *) + type_of_aux ((Some (n,(C.Def s)))::context) t None + in + if does_not_occur 1 t_typ then + (* since [Rel 1] does not occur in typ, substituting any term *) + (* in place of [Rel 1] is equivalent to delifting once *) + CicSubstitution.subst C.Implicit t_typ + else + C.LetIn (n,s,t_typ) + | C.Appl (he::tl) when List.length tl > 0 -> + let expected_hetype = + (* Inefficient, the head is computed twice. But I know *) + (* of no other solution. *) + R.whd context (CicTypeChecker.type_of_aux' metasenv context he) + in + let hetype = type_of_aux context he (Some expected_hetype) in + let tlbody_and_type = + let rec aux = + function + _,[] -> [] + | C.Prod (n,s,t),he::tl -> + (he, type_of_aux context he (Some (head_beta_reduce s))):: + (aux (R.whd context (S.subst he t), tl)) + | _ -> assert false + in + aux (expected_hetype, tl) + in + eat_prods context hetype tlbody_and_type + | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") + | C.Const (uri,exp_named_subst) -> + visit_exp_named_subst context uri exp_named_subst ; + CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) + | C.MutInd (uri,i,exp_named_subst) -> + visit_exp_named_subst context uri exp_named_subst ; + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_defs uri i) + | C.MutConstruct (uri,i,j,exp_named_subst) -> + visit_exp_named_subst context uri exp_named_subst ; + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_constr uri i j) + | C.MutCase (uri,i,outtype,term,pl) -> + let outsort = type_of_aux context outtype None in + let (need_dummy, k) = + let rec guess_args context t = + match CicReduction.whd context t with + C.Sort _ -> (true, 0) + | C.Prod (name, s, t) -> + let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in + if n = 0 then + (* last prod before sort *) + match CicReduction.whd context s with + C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> + (false, 1) + | C.Appl ((C.MutInd (uri',i',_)) :: _) + when U.eq uri' uri && i' = i -> (false, 1) + | _ -> (true, 1) + else + (b, n + 1) + | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") + in + let (b, k) = guess_args context outsort in + if not b then (b, k - 1) else (b, k) + in + let (parameters, arguments,exp_named_subst) = + let type_of_term = + CicTypeChecker.type_of_aux' metasenv context term + in + match + R.whd context (type_of_aux context term + (Some (head_beta_reduce type_of_term))) + with + (*CSC manca il caso dei CAST *) + C.MutInd (uri',i',exp_named_subst) -> + (* Checks suppressed *) + [],[],exp_named_subst + | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) -> + let params,args = + split tl (List.length tl - k) + in params,args,exp_named_subst + | _ -> + raise (NotWellTyped "MutCase: the term is not an inductive one") + in + (* Checks suppressed *) + (* Let's visit all the subterms that will not be visited later *) + let (cl,parsno) = + match CicEnvironment.get_cooked_obj uri with + C.InductiveDefinition (tl,_,parsno) -> + let (_,_,_,cl) = List.nth tl i in (cl,parsno) + | _ -> + raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + in + let _ = + List.fold_left + (fun j (p,(_,c)) -> + let cons = + if parameters = [] then + (C.MutConstruct (uri,i,j,exp_named_subst)) + else + (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) + in + let expectedtype = + type_of_branch context parsno need_dummy outtype cons + (CicTypeChecker.type_of_aux' metasenv context cons) + in + ignore (type_of_aux context p + (Some (head_beta_reduce expectedtype))) ; + j+1 + ) 1 (List.combine pl cl) + in + if not need_dummy then + C.Appl ((outtype::arguments)@[term]) + else if arguments = [] then + outtype + else + C.Appl (outtype::arguments) + | C.Fix (i,fl) -> + (* Let's visit all the subterms that will not be visited later *) + let context' = + List.rev + (List.map + (fun (n,_,ty,_) -> + let _ = type_of_aux context ty None in + (Some (C.Name n,(C.Decl ty))) + ) fl + ) @ + context + in + let _ = + List.iter + (fun (_,_,ty,bo) -> + let expectedty = + head_beta_reduce (CicSubstitution.lift (List.length fl) ty) + in + ignore (type_of_aux context' bo (Some expectedty)) + ) fl + in + (* Checks suppressed *) + let (_,_,ty,_) = List.nth fl i in + ty + | C.CoFix (i,fl) -> + (* Let's visit all the subterms that will not be visited later *) + let context' = + List.rev + (List.map + (fun (n,ty,_) -> + let _ = type_of_aux context ty None in + (Some (C.Name n,(C.Decl ty))) + ) fl + ) @ + context + in + let _ = + List.iter + (fun (_,ty,bo) -> + let expectedty = + head_beta_reduce (CicSubstitution.lift (List.length fl) ty) + in + ignore (type_of_aux context' bo (Some expectedty)) + ) fl + in + (* Checks suppressed *) + let (_,ty,_) = List.nth fl i in + ty + in + let synthesized' = head_beta_reduce synthesized in + let types,res = + match expectedty with + None -> + (* No expected type *) + {synthesized = synthesized' ; expected = None}, synthesized + | Some ty when syntactic_equality synthesized' ty -> + (* The expected type is synthactically equal to *) + (* the synthesized type. Let's forget it. *) + {synthesized = synthesized' ; expected = None}, synthesized + | Some expectedty' -> + {synthesized = synthesized' ; expected = Some expectedty'}, + expectedty' + in + CicHash.add subterms_to_types t types ; + res + + and visit_exp_named_subst context uri exp_named_subst = + let uris_and_types = + match CicEnvironment.get_cooked_obj uri with + Cic.Constant (_,_,_,params) + | Cic.CurrentProof (_,_,_,_,params) + | Cic.Variable (_,_,_,params) + | Cic.InductiveDefinition (_,params,_) -> + List.map + (function uri -> + match CicEnvironment.get_cooked_obj uri with + Cic.Variable (_,None,ty,_) -> uri,ty + | _ -> assert false (* the theorem is well-typed *) + ) params + in + let rec check uris_and_types subst = + match uris_and_types,subst with + _,[] -> [] + | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' -> + ignore (type_of_aux context t (Some ty)) ; + let tytl' = + List.map + (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl + in + check tytl' substtl + | _,_ -> assert false (* the theorem is well-typed *) + in + check uris_and_types exp_named_subst + + and sort_of_prod context (name,s) (t1, t2) = + let module C = Cic in + let t1' = CicReduction.whd context t1 in + let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in + match (t1', t2') with + (C.Sort s1, C.Sort s2) + when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) + C.Sort s2 + | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | (_,_) -> + raise + (NotWellTyped + ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2')) + + and eat_prods context hetype = + (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) + (*CSC: cucinati *) + function + [] -> hetype + | (hete, hety)::tl -> + (match (CicReduction.whd context hetype) with + Cic.Prod (n,s,t) -> + (* Checks suppressed *) + eat_prods context (CicSubstitution.subst hete t) tl + | _ -> raise (NotWellTyped "Appl: wrong Prod-type") + ) + +and type_of_branch context argsno need_dummy outtype term constype = + let module C = Cic in + let module R = CicReduction in + match R.whd context constype with + C.MutInd (_,_,_) -> + if need_dummy then + outtype + else + C.Appl [outtype ; term] + | C.Appl (C.MutInd (_,_,_)::tl) -> + let (_,arguments) = split tl argsno + in + if need_dummy && arguments = [] then + outtype + else + C.Appl (outtype::arguments@(if need_dummy then [] else [term])) + | C.Prod (name,so,de) -> + let term' = + match CicSubstitution.lift 1 term with + C.Appl l -> C.Appl (l@[C.Rel 1]) + | t -> C.Appl [t ; C.Rel 1] + in + C.Prod (C.Anonymous,so,type_of_branch + ((Some (name,(C.Decl so)))::context) argsno need_dummy + (CicSubstitution.lift 1 outtype) term' de) + | _ -> raise (Impossible 20) + + in + type_of_aux context t expectedty +;; + +let double_type_of metasenv context t expectedty = + let subterms_to_types = CicHash.create 503 in + ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ; + subterms_to_types +;; diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli new file mode 100644 index 000000000..d7d06ae42 --- /dev/null +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli @@ -0,0 +1,25 @@ +exception Impossible of int +exception NotWellTyped of string +exception WrongUriToConstant of string +exception WrongUriToVariable of string +exception WrongUriToMutualInductiveDefinitions of string +exception ListTooShort +exception RelToHiddenHypothesis + +type types = {synthesized : Cic.term ; expected : Cic.term option};; + +module CicHash : + sig + type 'a t + val find : 'a t -> Cic.term -> 'a + end +;; + +val double_type_of : + Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t + +(** Auxiliary functions **) + +(* does_not_occur n te *) +(* returns [true] if [Rel n] does not occur in [te] *) +val does_not_occur : int -> Cic.term -> bool diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 0259effd1..0de0fcda0 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -4,9 +4,9 @@ PREDICATES = REDUCTION_IMPLEMENTATION = cicReductionMachine.ml -INTERFACE_FILES = logger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \ - cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ - cicTypeChecker.mli +INTERFACE_FILES = logger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \ + cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ + cicTypeChecker.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) # Metadata tools only need zeta-reduction diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 8dee5ae2b..459aa8c8b 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,32 +1,20 @@ -cic2Xml.cmi: cic2acic.cmi -cic2content.cmi: cic2acic.cmi content.cmi -contentPp.cmi: content.cmi cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi -content2pres.cmi: content.cmi mpresentation.cmi +content2pres.cmi: mpresentation.cmi cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi -applyStylesheets.cmi: cic2acic.cmi -doubleTypeInference.cmo: doubleTypeInference.cmi -doubleTypeInference.cmx: doubleTypeInference.cmi -cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi -cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi -content.cmo: content.cmi -content.cmx: content.cmi -cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi -cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi -cic2content.cmo: cic2acic.cmi content.cmi cic2content.cmi -cic2content.cmx: cic2acic.cmx content.cmx cic2content.cmi -content_expressions.cmo: cic2acic.cmi content_expressions.cmi -content_expressions.cmx: cic2acic.cmx content_expressions.cmi -contentPp.cmo: content.cmi contentPp.cmi -contentPp.cmx: content.cmx contentPp.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 mpresentation.cmx: mpresentation.cmi cexpr2pres.cmo: content_expressions.cmi mpresentation.cmi cexpr2pres.cmi cexpr2pres.cmx: content_expressions.cmx mpresentation.cmx cexpr2pres.cmi -content2pres.cmo: cexpr2pres.cmi content.cmi content_expressions.cmi \ - mpresentation.cmi content2pres.cmi -content2pres.cmx: cexpr2pres.cmx content.cmx content_expressions.cmx \ - mpresentation.cmx content2pres.cmi +content2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ + content2pres.cmi +content2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ + content2pres.cmi cexpr2pres_hashtbl.cmo: cexpr2pres.cmi content_expressions.cmi \ mpresentation.cmi cexpr2pres_hashtbl.cmi cexpr2pres_hashtbl.cmx: cexpr2pres.cmx content_expressions.cmx \ @@ -35,8 +23,8 @@ misc.cmo: misc.cmi misc.cmx: misc.cmi xml2Gdome.cmo: xml2Gdome.cmi xml2Gdome.cmx: xml2Gdome.cmi -sequentPp.cmo: cic2Xml.cmi cic2acic.cmi sequentPp.cmi -sequentPp.cmx: cic2Xml.cmx cic2acic.cmx sequentPp.cmi +sequentPp.cmo: cic2Xml.cmi sequentPp.cmi +sequentPp.cmx: cic2Xml.cmx sequentPp.cmi applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ applyStylesheets.cmi applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \ diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 126e250ba..e1581421e 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -1,12 +1,11 @@ PACKAGE = cic_transformations -REQUIRES = helm-xml helm-cic_proof_checking gdome2-xslt +REQUIRES = helm-xml helm-cic_proof_checking helm-cic_omdoc gdome2-xslt PREDICATES = -INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli content.mli \ - cic2Xml.mli cic2content.mli content_expressions.mli \ - contentPp.mli mpresentation.mli cexpr2pres.mli \ - content2pres.mli cexpr2pres_hashtbl.mli misc.mli \ - xml2Gdome.mli sequentPp.mli applyStylesheets.mli +INTERFACE_FILES = cic2Xml.mli cic2content.mli content_expressions.mli \ + mpresentation.mli cexpr2pres.mli content2pres.mli \ + cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ + applyStylesheets.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/cic_transformations/cic2acic.ml b/helm/ocaml/cic_transformations/cic2acic.ml deleted file mode 100644 index a3cdfbb78..000000000 --- a/helm/ocaml/cic_transformations/cic2acic.ml +++ /dev/null @@ -1,408 +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/. - *) - -type anntypes = - {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} -;; - -let gen_id seed = - let res = "i" ^ string_of_int !seed in - incr seed ; - res -;; - -let fresh_id seed ids_to_terms ids_to_father_ids = - fun father t -> - let res = gen_id seed in - Hashtbl.add ids_to_father_ids res father ; - Hashtbl.add ids_to_terms res t ; - res -;; - -let source_id_of_id id = "#source#" ^ id;; - -exception NotEnoughElements;; -exception NameExpected;; - -(*CSC: cut&paste da cicPp.ml *) -(* get_nth l n returns the nth element of the list l if it exists or *) -(* raises NotEnoughElements if l has less than n elements *) -let rec get_nth l n = - match (n,l) with - (1, he::_) -> he - | (n, he::tail) when n > 1 -> get_nth tail (n-1) - | (_,_) -> raise NotEnoughElements -;; - -let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - ids_to_inner_types metasenv context idrefs t expectedty -= - let module D = DoubleTypeInference in - let module T = CicTypeChecker in - let module C = Cic in - let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in - let terms_to_types = - D.double_type_of metasenv context t expectedty - in - let rec aux computeinnertypes father context idrefs tt = - let fresh_id'' = fresh_id' father tt in - (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) - let aux' = aux computeinnertypes (Some fresh_id'') in - (* First of all we compute the inner type and the inner sort *) - (* of the term. They may be useful in what follows. *) - (*CSC: This is a very inefficient way of computing inner types *) - (*CSC: and inner sorts: very deep terms have their types/sorts *) - (*CSC: computed again and again. *) - let string_of_sort t = - match CicReduction.whd context t with - C.Sort C.Prop -> "Prop" - | C.Sort C.Set -> "Set" - | C.Sort C.Type -> "Type" - | _ -> assert false - in - let ainnertypes,innertype,innersort,expected_available = -(*CSC: Here we need the algorithm for Coscoy's double type-inference *) -(*CSC: (expected type + inferred type). Just for now we use the usual *) -(*CSC: type-inference, but the result is very poor. As a very weak *) -(*CSC: patch, I apply whd to the computed type. Full beta *) -(*CSC: reduction would be a much better option. *) - let {D.synthesized = synthesized; D.expected = expected} = - if computeinnertypes then - D.CicHash.find terms_to_types tt - else - (* We are already in an inner-type and Coscoy's double *) - (* type inference algorithm has not been applied. *) - {D.synthesized = - CicReduction.whd context (T.type_of_aux' metasenv context tt) ; - D.expected = None} - in - let innersort = T.type_of_aux' metasenv context synthesized in - let ainnertypes,expected_available = - if computeinnertypes then - let annexpected,expected_available = - match expected with - None -> None,false - | Some expectedty' -> - Some - (aux false (Some fresh_id'') context idrefs expectedty'), - true - in - Some - {annsynthesized = - aux false (Some fresh_id'') context idrefs synthesized ; - annexpected = annexpected - }, expected_available - else - None,false - in - ainnertypes,synthesized, string_of_sort innersort, expected_available - in - let add_inner_type id = - match ainnertypes with - None -> () - | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes - in - match tt with - C.Rel n -> - let id = - match get_nth context n with - (Some (C.Name s,_)) -> s - | _ -> raise NameExpected - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then - add_inner_type fresh_id'' ; - C.ARel (fresh_id'', List.nth idrefs (n-1), n, id) - | C.Var (uri,exp_named_subst) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then - add_inner_type fresh_id'' ; - let exp_named_subst' = - List.map - (function i,t -> i, (aux' context idrefs t)) exp_named_subst - in - C.AVar (fresh_id'', uri,exp_named_subst') - | C.Meta (n,l) -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> n = m) metasenv - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then - add_inner_type fresh_id'' ; - C.AMeta (fresh_id'', n, - (List.map2 - (fun ct t -> - match (ct, t) with - | None, _ -> None - | _, Some t -> Some (aux' context idrefs t) - | Some _, None -> assert false (* due to typing rules *)) - canonical_context l)) - | C.Sort s -> C.ASort (fresh_id'', s) - | C.Implicit -> C.AImplicit (fresh_id'') - | C.Cast (v,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t) - | C.Prod (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' - (string_of_sort innertype) ; - let sourcetype = T.type_of_aux' metasenv context s in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort sourcetype) ; - let n' = - match n with - C.Anonymous -> n - | C.Name n' -> - if D.does_not_occur 1 t then - C.Anonymous - else - C.Name n' - in - C.AProd - (fresh_id'', n', aux' context idrefs s, - aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t) - | C.Lambda (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - let sourcetype = T.type_of_aux' metasenv context s in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort sourcetype) ; - if innersort = "Prop" then - begin - let father_is_lambda = - match father with - None -> false - | Some father' -> - match Hashtbl.find ids_to_terms father' with - C.Lambda _ -> true - | _ -> false - in - if (not father_is_lambda) || expected_available then - add_inner_type fresh_id'' - end ; - C.ALambda - (fresh_id'',n, aux' context idrefs s, - aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t) - | C.LetIn (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.ALetIn - (fresh_id'', n, aux' context idrefs s, - aux' ((Some (n, C.Def s))::context) (fresh_id''::idrefs) t) - | C.Appl l -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.AAppl (fresh_id'', List.map (aux' context idrefs) l) - | C.Const (uri,exp_named_subst) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then - add_inner_type fresh_id'' ; - let exp_named_subst' = - List.map - (function i,t -> i, (aux' context idrefs t)) exp_named_subst - in - C.AConst (fresh_id'', uri, exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (aux' context idrefs t)) exp_named_subst - in - C.AMutInd (fresh_id'', uri, tyno, exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then - add_inner_type fresh_id'' ; - let exp_named_subst' = - List.map - (function i,t -> i, (aux' context idrefs t)) exp_named_subst - in - C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst') - | C.MutCase (uri, tyno, outty, term, patterns) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty, - aux' context idrefs term, List.map (aux' context idrefs) patterns) - | C.Fix (funno, funs) -> - let fresh_idrefs = - List.map (function _ -> gen_id seed) funs in - let new_idrefs = List.rev fresh_idrefs @ idrefs in - let tys = - List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.AFix (fresh_id'', funno, - List.map2 - (fun id (name, indidx, ty, bo) -> - (id, name, indidx, aux' context idrefs ty, - aux' (tys@context) new_idrefs bo) - ) fresh_idrefs funs - ) - | C.CoFix (funno, funs) -> - let fresh_idrefs = - List.map (function _ -> gen_id seed) funs in - let new_idrefs = List.rev fresh_idrefs @ idrefs in - let tys = - List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.ACoFix (fresh_id'', funno, - List.map2 - (fun id (name, ty, bo) -> - (id, name, aux' context idrefs ty, - aux' (tys@context) new_idrefs bo) - ) fresh_idrefs funs - ) - in - aux true None context idrefs t -;; - -let acic_of_cic_context metasenv context idrefs t = - let ids_to_terms = Hashtbl.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let seed = ref 0 in - acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - ids_to_inner_types metasenv context idrefs t, - ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types -;; - -let acic_object_of_cic_object obj = - let module C = Cic in - let ids_to_terms = Hashtbl.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let ids_to_conjectures = Hashtbl.create 11 in - let ids_to_hypotheses = Hashtbl.create 127 in - let hypotheses_seed = ref 0 in - let conjectures_seed = ref 0 in - let seed = ref 0 in - let acic_term_of_cic_term_context' = - acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - ids_to_inner_types in - let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in - let aobj = - match obj with - C.Constant (id,Some bo,ty,params) -> - let abo = acic_term_of_cic_term' bo (Some ty) in - let aty = acic_term_of_cic_term' ty None in - C.AConstant - ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params) - | C.Constant (id,None,ty,params) -> - let aty = acic_term_of_cic_term' ty None in - C.AConstant - ("mettereaposto",None,id,None,aty, params) - | C.Variable (id,bo,ty,params) -> - let abo = - match bo with - None -> None - | Some bo -> Some (acic_term_of_cic_term' bo (Some ty)) - in - let aty = acic_term_of_cic_term' ty None in - C.AVariable - ("mettereaposto",id,abo,aty, params) - | C.CurrentProof (id,conjectures,bo,ty,params) -> - let aconjectures = - List.map - (function (i,canonical_context,term) as conjecture -> - let cid = "c" ^ string_of_int !conjectures_seed in - Hashtbl.add ids_to_conjectures cid conjecture ; - incr conjectures_seed ; - let idrefs',revacanonical_context = - let rec aux context idrefs = - function - [] -> idrefs,[] - | hyp::tl -> - let hid = "h" ^ string_of_int !hypotheses_seed in - let new_idrefs = hid::idrefs in - Hashtbl.add ids_to_hypotheses hid hyp ; - incr hypotheses_seed ; - match hyp with - (Some (n,C.Decl t)) -> - let final_idrefs,atl = - aux (hyp::context) new_idrefs tl in - let at = - acic_term_of_cic_term_context' - conjectures context idrefs t None - in - final_idrefs,(hid,Some (n,C.ADecl at))::atl - | (Some (n,C.Def t)) -> - let final_idrefs,atl = - aux (hyp::context) new_idrefs tl in - let at = - acic_term_of_cic_term_context' - conjectures context idrefs t None - in - final_idrefs,(hid,Some (n,C.ADef at))::atl - | None -> - let final_idrefs,atl = - aux (hyp::context) new_idrefs tl - in - final_idrefs,(hid,None)::atl - in - aux [] [] (List.rev canonical_context) - in - let aterm = - acic_term_of_cic_term_context' conjectures - canonical_context idrefs' term None - in - (cid,i,(List.rev revacanonical_context),aterm) - ) conjectures in - let abo = - acic_term_of_cic_term_context' conjectures [] [] bo (Some ty) in - let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in - C.ACurrentProof - ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params) - | C.InductiveDefinition (tys,params,paramsno) -> - let context = - List.map - (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in - let idrefs = List.map (function _ -> gen_id seed) tys in - let atys = - List.map2 - (fun id (name,inductive,ty,cons) -> - let acons = - List.map - (function (name,ty) -> - (name, - acic_term_of_cic_term_context' [] context idrefs ty None) - ) cons - in - (id,name,inductive,acic_term_of_cic_term' ty None,acons) - ) (List.rev idrefs) tys - in - C.AInductiveDefinition ("mettereaposto",atys,params,paramsno) - in - aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types, - ids_to_conjectures,ids_to_hypotheses -;; diff --git a/helm/ocaml/cic_transformations/cic2acic.mli b/helm/ocaml/cic_transformations/cic2acic.mli deleted file mode 100644 index b34d34342..000000000 --- a/helm/ocaml/cic_transformations/cic2acic.mli +++ /dev/null @@ -1,56 +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/. - *) - -exception NotEnoughElements -exception NameExpected - -val source_id_of_id : string -> string - -type anntypes = - {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} -;; - -val acic_of_cic_context' : - int ref -> (* seed *) - (Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *) - (Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *) - (Cic.id, string) Hashtbl.t -> (* ids_to_inner_sorts *) - (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *) - Cic.metasenv -> (* metasenv *) - Cic.context -> (* context *) - Cic.id list -> (* idrefs *) - Cic.term -> (* term *) - Cic.term option -> (* expected type *) - Cic.annterm (* annotated term *) - -val acic_object_of_cic_object : - Cic.obj -> (* object *) - Cic.annobj * (* annotated object *) - (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) - (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) - (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) - (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *) - (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *) - (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) diff --git a/helm/ocaml/cic_transformations/content.ml b/helm/ocaml/cic_transformations/content.ml deleted file mode 100644 index be46f5961..000000000 --- a/helm/ocaml/cic_transformations/content.ml +++ /dev/null @@ -1,159 +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 *) -(* *) -(**************************************************************************) - -type id = string;; -type joint_recursion_kind = - [ `Recursive - | `CoRecursive - | `Inductive of int (* paramsno *) - | `CoInductive of int (* paramsno *) - ] -;; - -type var_or_const = Var | Const;; - -type 'term declaration = - { dec_name : string option; - dec_id : string ; - dec_inductive : bool; - dec_aref : string; - dec_type : 'term - } -;; - -type 'term definition = - { def_name : string option; - def_id : string ; - def_aref : string ; - def_term : 'term - } -;; - -type 'term inductive = - { inductive_id : string ; - inductive_kind : bool; - inductive_type : 'term; - inductive_constructors : 'term declaration list - } -;; - -type 'term decl_context_element = - [ `Declaration of 'term declaration - | `Hypothesis of 'term declaration - ] -;; - -type ('term,'proof) def_context_element = - [ `Proof of 'proof - | `Definition of 'term definition - ] -;; - -type ('term,'proof) in_joint_context_element = - [ `Inductive of 'term inductive - | 'term decl_context_element - | ('term,'proof) def_context_element - ] -;; - -type ('term,'proof) joint = - { joint_id : string ; - joint_kind : joint_recursion_kind ; - joint_defs : ('term,'proof) in_joint_context_element list - } -;; - -type ('term,'proof) joint_context_element = - [ `Joint of ('term,'proof) joint ] -;; - -type 'term proof = - { proof_name : string option; - proof_id : string ; - proof_context : 'term in_proof_context_element list ; - proof_apply_context: 'term proof list; - proof_conclude : 'term conclude_item - } - -and 'term in_proof_context_element = - [ 'term decl_context_element - | ('term,'term proof) def_context_element - | ('term,'term proof) joint_context_element - ] - -and 'term conclude_item = - { conclude_id :string; - conclude_aref : string; - conclude_method : string; - conclude_args : ('term arg) list ; - conclude_conclusion : 'term option - } - -and 'term arg = - Aux of int - | Premise of premise - | Term of 'term - | ArgProof of 'term proof - | ArgMethod of string (* ???? *) - -and premise = - { premise_id: string; - premise_xref : string ; - premise_binder : string option; - premise_n : int option; - } -;; - -type 'term conjecture = id * int * 'term context * 'term - -and 'term context = 'term hypothesis list - -and 'term hypothesis = - id * - ['term decl_context_element | ('term,'term proof) def_context_element ] option -;; - -type 'term in_object_context_element = - [ `Decl of var_or_const * 'term decl_context_element - | `Def of var_or_const * 'term * ('term,'term proof) def_context_element - | ('term,'term proof) joint_context_element - ] -;; - -type 'term cobj = - id * (* id *) - UriManager.uri list * (* params *) - 'term conjecture list option * (* optional metasenv *) - 'term in_object_context_element (* actual object *) -;; diff --git a/helm/ocaml/cic_transformations/content.mli b/helm/ocaml/cic_transformations/content.mli deleted file mode 100644 index b58b84b54..000000000 --- a/helm/ocaml/cic_transformations/content.mli +++ /dev/null @@ -1,150 +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/. - *) - -type id = string;; -type joint_recursion_kind = - [ `Recursive - | `CoRecursive - | `Inductive of int (* paramsno *) - | `CoInductive of int (* paramsno *) - ] -;; - -type var_or_const = Var | Const;; - -type 'term declaration = - { dec_name : string option; - dec_id : string ; - dec_inductive : bool; - dec_aref : string; - dec_type : 'term - } -;; - -type 'term definition = - { def_name : string option; - def_id : string ; - def_aref : string ; - def_term : 'term - } -;; - -type 'term inductive = - { inductive_id : string ; - inductive_kind : bool; - inductive_type : 'term; - inductive_constructors : 'term declaration list - } -;; - -type 'term decl_context_element = - [ `Declaration of 'term declaration - | `Hypothesis of 'term declaration - ] -;; - -type ('term,'proof) def_context_element = - [ `Proof of 'proof - | `Definition of 'term definition - ] -;; - -type ('term,'proof) in_joint_context_element = - [ `Inductive of 'term inductive - | 'term decl_context_element - | ('term,'proof) def_context_element - ] -;; - -type ('term,'proof) joint = - { joint_id : string ; - joint_kind : joint_recursion_kind ; - joint_defs : ('term,'proof) in_joint_context_element list - } -;; - -type ('term,'proof) joint_context_element = - [ `Joint of ('term,'proof) joint ] -;; - -type 'term proof = - { proof_name : string option; - proof_id : string ; - proof_context : 'term in_proof_context_element list ; - proof_apply_context: 'term proof list; - proof_conclude : 'term conclude_item - } - -and 'term in_proof_context_element = - [ 'term decl_context_element - | ('term,'term proof) def_context_element - | ('term,'term proof) joint_context_element - ] - -and 'term conclude_item = - { conclude_id :string; - conclude_aref : string; - conclude_method : string; - conclude_args : ('term arg) list ; - conclude_conclusion : 'term option - } - -and 'term arg = - Aux of int - | Premise of premise - | Term of 'term - | ArgProof of 'term proof - | ArgMethod of string (* ???? *) - -and premise = - { premise_id: string; - premise_xref : string ; - premise_binder : string option; - premise_n : int option; - } -;; - -type 'term conjecture = id * int * 'term context * 'term - -and 'term context = 'term hypothesis list - -and 'term hypothesis = - id * - ['term decl_context_element | ('term,'term proof) def_context_element ] option -;; - -type 'term in_object_context_element = - [ `Decl of var_or_const * 'term decl_context_element - | `Def of var_or_const * 'term * ('term,'term proof) def_context_element - | ('term,'term proof) joint_context_element - ] -;; - -type 'term cobj = - id * (* id *) - UriManager.uri list * (* params *) - 'term conjecture list option * (* optional metasenv *) - 'term in_object_context_element (* actual object *) -;; diff --git a/helm/ocaml/cic_transformations/contentPp.ml b/helm/ocaml/cic_transformations/contentPp.ml deleted file mode 100644 index 3bc8bb306..000000000 --- a/helm/ocaml/cic_transformations/contentPp.ml +++ /dev/null @@ -1,146 +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 *) -(* 17/06/2003 *) -(* *) -(***************************************************************************) - -exception ContentPpInternalError;; -exception NotEnoughElements;; -exception TO_DO - -(* Utility functions *) - - -let string_of_name = - function - Some s -> s - | None -> "_" -;; - -(* get_nth l n returns the nth element of the list l if it exists or *) -(* raises NotEnoughElements if l has less than n elements *) -let rec get_nth l n = - match (n,l) with - (1, he::_) -> he - | (n, he::tail) when n > 1 -> get_nth tail (n-1) - | (_,_) -> raise NotEnoughElements -;; - -let rec blanks n = - if n = 0 then "" - else (" " ^ (blanks (n-1)));; - -let rec pproof (p: Cic.annterm Content.proof) indent = - let module Con = Content in - let new_indent = - (match p.Con.proof_name with - Some s -> - prerr_endline - ((blanks indent) ^ "(" ^ s ^ ")"); flush stderr ;(indent + 1) - | None ->indent) in - let new_indent1 = - if (p.Con.proof_context = []) then new_indent - else - (pcontext p.Con.proof_context new_indent; (new_indent + 1)) in - papply_context p.Con.proof_apply_context new_indent1; - pconclude p.Con.proof_conclude new_indent1; - -and pcontext c indent = - List.iter (pcontext_element indent) c - -and pcontext_element indent = - let module Con = Content in - function - `Declaration d -> - (match d.Con.dec_name with - Some s -> - prerr_endline - ((blanks indent) - ^ "Assume " ^ s ^ " : " - ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.dec_type))); - flush stderr - | None -> - prerr_endline ((blanks indent) ^ "NO NAME!!")) - | `Hypothesis h -> - (match h.Con.dec_name with - Some s -> - prerr_endline - ((blanks indent) - ^ "Suppose " ^ s ^ " : " - ^ (CicPp.ppterm (Deannotate.deannotate_term h.Con.dec_type))); - flush stderr - | None -> - prerr_endline ((blanks indent) ^ "NO NAME!!")) - | `Proof p -> pproof p indent - | `Definition d -> - (match d.Con.def_name with - Some s -> - prerr_endline - ((blanks indent) ^ "Let " ^ s ^ " = " - ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.def_term))); - flush stderr - | None -> - prerr_endline ((blanks indent) ^ "NO NAME!!")) - | `Joint ho -> - prerr_endline ((blanks indent) ^ "Joint Def"); - flush stderr - -and papply_context ac indent = - List.iter(function p -> (pproof p indent)) ac - -and pconclude concl indent = - let module Con = Content in - prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr; - pargs concl.Con.conclude_args indent; - match concl.Con.conclude_conclusion with - None -> prerr_endline ((blanks indent) ^"No conclude conclusion");flush stderr - | Some t -> prerr_endline ((blanks indent) ^ "conclude" ^ concl.Con.conclude_method ^ (CicPp.ppterm (Deannotate.deannotate_term t)));flush stderr - -and pargs args indent = - List.iter (parg indent) args - -and parg indent = - let module Con = Content in - function - Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ (string_of_int n));flush stderr - | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr - | Con.Term t -> - prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t))); - flush stderr - | Con.ArgProof p -> pproof p (indent+1) - | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr -;; - -let print_proof p = pproof p 0; - - - - diff --git a/helm/ocaml/cic_transformations/contentPp.mli b/helm/ocaml/cic_transformations/contentPp.mli deleted file mode 100644 index 85ce238f3..000000000 --- a/helm/ocaml/cic_transformations/contentPp.mli +++ /dev/null @@ -1,28 +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 print_proof: Cic.annterm Content.proof -> unit - - diff --git a/helm/ocaml/cic_transformations/doubleTypeInference.ml b/helm/ocaml/cic_transformations/doubleTypeInference.ml deleted file mode 100644 index 71422ced1..000000000 --- a/helm/ocaml/cic_transformations/doubleTypeInference.ml +++ /dev/null @@ -1,687 +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/. - *) - -exception Impossible of int;; -exception NotWellTyped of string;; -exception WrongUriToConstant of string;; -exception WrongUriToVariable of string;; -exception WrongUriToMutualInductiveDefinitions of string;; -exception ListTooShort;; -exception RelToHiddenHypothesis;; - -type types = {synthesized : Cic.term ; expected : Cic.term option};; - -(* does_not_occur n te *) -(* returns [true] if [Rel n] does not occur in [te] *) -let rec does_not_occur n = - let module C = Cic in - function - C.Rel m when m = n -> false - | C.Rel _ - | C.Meta _ - | C.Sort _ - | C.Implicit -> true - | C.Cast (te,ty) -> - does_not_occur n te && does_not_occur n ty - | C.Prod (name,so,dest) -> - does_not_occur n so && - does_not_occur (n + 1) dest - | C.Lambda (name,so,dest) -> - does_not_occur n so && - does_not_occur (n + 1) dest - | C.LetIn (name,so,dest) -> - does_not_occur n so && - does_not_occur (n + 1) dest - | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur n x) l true - | C.Var (_,exp_named_subst) - | C.Const (_,exp_named_subst) - | C.MutInd (_,_,exp_named_subst) - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && does_not_occur n x) - exp_named_subst true - | C.MutCase (_,_,out,te,pl) -> - does_not_occur n out && does_not_occur n te && - List.fold_right (fun x i -> i && does_not_occur n x) pl true - | C.Fix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len in - let tys = - List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl - in - List.fold_right - (fun (_,_,ty,bo) i -> - i && does_not_occur n ty && - does_not_occur n_plus_len bo - ) fl true - | C.CoFix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len in - let tys = - List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur n ty && - does_not_occur n_plus_len bo - ) fl true -;; - -(*CSC: potrebbe creare applicazioni di applicazioni *) -(*CSC: ora non e' piu' head, ma completa!!! *) -let rec head_beta_reduce = - let module S = CicSubstitution in - let module C = Cic in - function - C.Rel _ as t -> t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst - in - C.Var (uri,exp_named_subst) - | C.Meta (n,l) -> - C.Meta (n, - List.map - (function None -> None | Some t -> Some (head_beta_reduce t)) l - ) - | C.Sort _ as t -> t - | C.Implicit -> assert false - | C.Cast (te,ty) -> - C.Cast (head_beta_reduce te, head_beta_reduce ty) - | C.Prod (n,s,t) -> - C.Prod (n, head_beta_reduce s, head_beta_reduce t) - | C.Lambda (n,s,t) -> - C.Lambda (n, head_beta_reduce s, head_beta_reduce t) - | C.LetIn (n,s,t) -> - C.LetIn (n, head_beta_reduce s, head_beta_reduce t) - | C.Appl ((C.Lambda (name,s,t))::he::tl) -> - let he' = S.subst he t in - if tl = [] then - head_beta_reduce he' - else - head_beta_reduce (C.Appl (he'::tl)) - | C.Appl l -> - C.Appl (List.map head_beta_reduce l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst - in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst - in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t, - List.map head_beta_reduce pl) - | C.Fix (i,fl) -> - let fl' = - List.map - (function (name,i,ty,bo) -> - name,i,head_beta_reduce ty,head_beta_reduce bo - ) fl - in - C.Fix (i,fl') - | C.CoFix (i,fl) -> - let fl' = - List.map - (function (name,ty,bo) -> - name,head_beta_reduce ty,head_beta_reduce bo - ) fl - in - C.CoFix (i,fl') -;; - -(* syntactic_equality up to cookingsno for uris *) -(* (which is often syntactically irrilevant), *) -(* distinction between fake dependent products *) -(* and non-dependent products, alfa-conversion *) -(*CSC: must alfa-conversion be considered or not? *) -let syntactic_equality t t' = - let module C = Cic in - let rec syntactic_equality t t' = - if t = t' then true - else - match t, t' with - C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') -> - UriManager.eq uri uri' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.Cast (te,ty), C.Cast (te',ty') -> - syntactic_equality te te' && - syntactic_equality ty ty' - | C.Prod (_,s,t), C.Prod (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Lambda (_,s,t), C.Lambda (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Appl l, C.Appl l' -> - List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' - | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') -> - UriManager.eq uri uri' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') -> - UriManager.eq uri uri' && i = i' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutConstruct (uri,i,j,exp_named_subst), - C.MutConstruct (uri',i',j',exp_named_subst') -> - UriManager.eq uri uri' && i = i' && j = j' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> - UriManager.eq sp sp' && i = i' && - syntactic_equality outt outt' && - syntactic_equality t t' && - List.fold_left2 - (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' - | C.Fix (i,fl), C.Fix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,i,ty,bo) (_,i',ty',bo') -> - b && i = i' && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | C.CoFix (i,fl), C.CoFix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,ty,bo) (_,ty',bo') -> - b && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | _, _ -> false (* we already know that t != t' *) - and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 = - List.fold_left2 - (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true - exp_named_subst1 exp_named_subst2 - in - try - syntactic_equality t t' - with - _ -> false -;; - -let rec split l n = - match (l,n) with - (l,0) -> ([], l) - | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) - | (_,_) -> raise ListTooShort -;; - -let type_of_constant uri = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj - | CicEnvironment.UncheckedObj uobj -> - raise (NotWellTyped "Reference to an unchecked constant") - in - match cobj with - C.Constant (_,_,ty,_) -> ty - | C.CurrentProof (_,_,_,ty,_) -> ty - | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) -;; - -let type_of_variable uri = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty - | CicEnvironment.UncheckedObj (C.Variable _) -> - raise (NotWellTyped "Reference to an unchecked variable") - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) -;; - -let type_of_mutual_inductive_defs uri i = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj - | CicEnvironment.UncheckedObj uobj -> - raise (NotWellTyped "Reference to an unchecked inductive type") - in - match cobj with - C.InductiveDefinition (dl,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) -;; - -let type_of_mutual_inductive_constr uri i j = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj - | CicEnvironment.UncheckedObj uobj -> - raise (NotWellTyped "Reference to an unchecked constructor") - in - match cobj with - C.InductiveDefinition (dl,_,_) -> - let (_,_,_,cl) = List.nth dl i in - let (_,ty) = List.nth cl (j-1) in - ty - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) -;; - -module CicHash = - Hashtbl.Make - (struct - type t = Cic.term - let equal = (==) - let hash = Hashtbl.hash - end) -;; - -(* type_of_aux' is just another name (with a different scope) for type_of_aux *) -let rec type_of_aux' subterms_to_types metasenv context t expectedty = - (* Coscoy's double type-inference algorithm *) - (* It computes the inner-types of every subterm of [t], *) - (* even when they are not needed to compute the types *) - (* of other terms. *) - let rec type_of_aux context t expectedty = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let module U = UriManager in - let synthesized = - match t with - C.Rel n -> - (try - match List.nth context (n - 1) with - Some (_,C.Decl t) -> S.lift n t - | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty - | None -> raise RelToHiddenHypothesis - with - _ -> raise (NotWellTyped "Not a close term") - ) - | C.Var (uri,exp_named_subst) -> - visit_exp_named_subst context uri exp_named_subst ; - CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) - | C.Meta (n,l) -> - (* Let's visit all the subterms that will not be visited later *) - let (_,canonical_context,_) = - List.find (function (m,_,_) -> n = m) metasenv - in - let lifted_canonical_context = - let rec aux i = - function - [] -> [] - | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def t))::tl -> - (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) - | None::tl -> None::(aux (i+1) tl) - in - aux 1 canonical_context - in - let _ = - List.iter2 - (fun t ct -> - match t,ct with - _,None -> () - | Some t,Some (_,C.Def ct) -> - let expected_type = - R.whd context - (CicTypeChecker.type_of_aux' metasenv context ct) - in - (* Maybe I am a bit too paranoid, because *) - (* if the term is well-typed than t and ct *) - (* are convertible. Nevertheless, I compute *) - (* the expected type. *) - ignore (type_of_aux context t (Some expected_type)) - | Some t,Some (_,C.Decl ct) -> - ignore (type_of_aux context t (Some ct)) - | _,_ -> assert false (* the term is not well typed!!! *) - ) l lifted_canonical_context - in - let (_,canonical_context,ty) = - List.find (function (m,_,_) -> n = m) metasenv - in - (* Checks suppressed *) - CicSubstitution.lift_meta l ty - | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) - | C.Implicit -> raise (Impossible 21) - | C.Cast (te,ty) -> - (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context te (Some (head_beta_reduce ty)) in - let _ = type_of_aux context ty None in - (* Checks suppressed *) - ty - | C.Prod (name,s,t) -> - let sort1 = type_of_aux context s None - and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in - sort_of_prod context (name,s) (sort1,sort2) - | C.Lambda (n,s,t) -> - (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context s None in - let expected_target_type = - match expectedty with - None -> None - | Some expectedty' -> - let ty = - match R.whd context expectedty' with - C.Prod (_,_,expected_target_type) -> - head_beta_reduce expected_target_type - | _ -> assert false - in - Some ty - in - let type2 = - type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type - in - (* Checks suppressed *) - C.Prod (n,s,type2) - | C.LetIn (n,s,t) -> -(*CSC: What are the right expected types for the source and *) -(*CSC: target of a LetIn? None used. *) - (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context s None in - let t_typ = - (* Checks suppressed *) - type_of_aux ((Some (n,(C.Def s)))::context) t None - in - if does_not_occur 1 t_typ then - (* since [Rel 1] does not occur in typ, substituting any term *) - (* in place of [Rel 1] is equivalent to delifting once *) - CicSubstitution.subst C.Implicit t_typ - else - C.LetIn (n,s,t_typ) - | C.Appl (he::tl) when List.length tl > 0 -> - let expected_hetype = - (* Inefficient, the head is computed twice. But I know *) - (* of no other solution. *) - R.whd context (CicTypeChecker.type_of_aux' metasenv context he) - in - let hetype = type_of_aux context he (Some expected_hetype) in - let tlbody_and_type = - let rec aux = - function - _,[] -> [] - | C.Prod (n,s,t),he::tl -> - (he, type_of_aux context he (Some (head_beta_reduce s))):: - (aux (R.whd context (S.subst he t), tl)) - | _ -> assert false - in - aux (expected_hetype, tl) - in - eat_prods context hetype tlbody_and_type - | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") - | C.Const (uri,exp_named_subst) -> - visit_exp_named_subst context uri exp_named_subst ; - CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) - | C.MutInd (uri,i,exp_named_subst) -> - visit_exp_named_subst context uri exp_named_subst ; - CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_defs uri i) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - visit_exp_named_subst context uri exp_named_subst ; - CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_constr uri i j) - | C.MutCase (uri,i,outtype,term,pl) -> - let outsort = type_of_aux context outtype None in - let (need_dummy, k) = - let rec guess_args context t = - match CicReduction.whd context t with - C.Sort _ -> (true, 0) - | C.Prod (name, s, t) -> - let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in - if n = 0 then - (* last prod before sort *) - match CicReduction.whd context s with - C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> - (false, 1) - | C.Appl ((C.MutInd (uri',i',_)) :: _) - when U.eq uri' uri && i' = i -> (false, 1) - | _ -> (true, 1) - else - (b, n + 1) - | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") - in - let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) - in - let (parameters, arguments,exp_named_subst) = - let type_of_term = - CicTypeChecker.type_of_aux' metasenv context term - in - match - R.whd context (type_of_aux context term - (Some (head_beta_reduce type_of_term))) - with - (*CSC manca il caso dei CAST *) - C.MutInd (uri',i',exp_named_subst) -> - (* Checks suppressed *) - [],[],exp_named_subst - | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) -> - let params,args = - split tl (List.length tl - k) - in params,args,exp_named_subst - | _ -> - raise (NotWellTyped "MutCase: the term is not an inductive one") - in - (* Checks suppressed *) - (* Let's visit all the subterms that will not be visited later *) - let (cl,parsno) = - match CicEnvironment.get_cooked_obj uri with - C.InductiveDefinition (tl,_,parsno) -> - let (_,_,_,cl) = List.nth tl i in (cl,parsno) - | _ -> - raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) - in - let _ = - List.fold_left - (fun j (p,(_,c)) -> - let cons = - if parameters = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) - in - let expectedtype = - type_of_branch context parsno need_dummy outtype cons - (CicTypeChecker.type_of_aux' metasenv context cons) - in - ignore (type_of_aux context p - (Some (head_beta_reduce expectedtype))) ; - j+1 - ) 1 (List.combine pl cl) - in - if not need_dummy then - C.Appl ((outtype::arguments)@[term]) - else if arguments = [] then - outtype - else - C.Appl (outtype::arguments) - | C.Fix (i,fl) -> - (* Let's visit all the subterms that will not be visited later *) - let context' = - List.rev - (List.map - (fun (n,_,ty,_) -> - let _ = type_of_aux context ty None in - (Some (C.Name n,(C.Decl ty))) - ) fl - ) @ - context - in - let _ = - List.iter - (fun (_,_,ty,bo) -> - let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) - in - ignore (type_of_aux context' bo (Some expectedty)) - ) fl - in - (* Checks suppressed *) - let (_,_,ty,_) = List.nth fl i in - ty - | C.CoFix (i,fl) -> - (* Let's visit all the subterms that will not be visited later *) - let context' = - List.rev - (List.map - (fun (n,ty,_) -> - let _ = type_of_aux context ty None in - (Some (C.Name n,(C.Decl ty))) - ) fl - ) @ - context - in - let _ = - List.iter - (fun (_,ty,bo) -> - let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) - in - ignore (type_of_aux context' bo (Some expectedty)) - ) fl - in - (* Checks suppressed *) - let (_,ty,_) = List.nth fl i in - ty - in - let synthesized' = head_beta_reduce synthesized in - let types,res = - match expectedty with - None -> - (* No expected type *) - {synthesized = synthesized' ; expected = None}, synthesized - | Some ty when syntactic_equality synthesized' ty -> - (* The expected type is synthactically equal to *) - (* the synthesized type. Let's forget it. *) - {synthesized = synthesized' ; expected = None}, synthesized - | Some expectedty' -> - {synthesized = synthesized' ; expected = Some expectedty'}, - expectedty' - in - CicHash.add subterms_to_types t types ; - res - - and visit_exp_named_subst context uri exp_named_subst = - let uris_and_types = - match CicEnvironment.get_cooked_obj uri with - Cic.Constant (_,_,_,params) - | Cic.CurrentProof (_,_,_,_,params) - | Cic.Variable (_,_,_,params) - | Cic.InductiveDefinition (_,params,_) -> - List.map - (function uri -> - match CicEnvironment.get_cooked_obj uri with - Cic.Variable (_,None,ty,_) -> uri,ty - | _ -> assert false (* the theorem is well-typed *) - ) params - in - let rec check uris_and_types subst = - match uris_and_types,subst with - _,[] -> [] - | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' -> - ignore (type_of_aux context t (Some ty)) ; - let tytl' = - List.map - (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl - in - check tytl' substtl - | _,_ -> assert false (* the theorem is well-typed *) - in - check uris_and_types exp_named_subst - - and sort_of_prod context (name,s) (t1, t2) = - let module C = Cic in - let t1' = CicReduction.whd context t1 in - let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in - match (t1', t2') with - (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) - C.Sort s2 - | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) - | (_,_) -> - raise - (NotWellTyped - ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2')) - - and eat_prods context hetype = - (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) - (*CSC: cucinati *) - function - [] -> hetype - | (hete, hety)::tl -> - (match (CicReduction.whd context hetype) with - Cic.Prod (n,s,t) -> - (* Checks suppressed *) - eat_prods context (CicSubstitution.subst hete t) tl - | _ -> raise (NotWellTyped "Appl: wrong Prod-type") - ) - -and type_of_branch context argsno need_dummy outtype term constype = - let module C = Cic in - let module R = CicReduction in - match R.whd context constype with - C.MutInd (_,_,_) -> - if need_dummy then - outtype - else - C.Appl [outtype ; term] - | C.Appl (C.MutInd (_,_,_)::tl) -> - let (_,arguments) = split tl argsno - in - if need_dummy && arguments = [] then - outtype - else - C.Appl (outtype::arguments@(if need_dummy then [] else [term])) - | C.Prod (name,so,de) -> - let term' = - match CicSubstitution.lift 1 term with - C.Appl l -> C.Appl (l@[C.Rel 1]) - | t -> C.Appl [t ; C.Rel 1] - in - C.Prod (C.Anonymous,so,type_of_branch - ((Some (name,(C.Decl so)))::context) argsno need_dummy - (CicSubstitution.lift 1 outtype) term' de) - | _ -> raise (Impossible 20) - - in - type_of_aux context t expectedty -;; - -let double_type_of metasenv context t expectedty = - let subterms_to_types = CicHash.create 503 in - ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ; - subterms_to_types -;; diff --git a/helm/ocaml/cic_transformations/doubleTypeInference.mli b/helm/ocaml/cic_transformations/doubleTypeInference.mli deleted file mode 100644 index d7d06ae42..000000000 --- a/helm/ocaml/cic_transformations/doubleTypeInference.mli +++ /dev/null @@ -1,25 +0,0 @@ -exception Impossible of int -exception NotWellTyped of string -exception WrongUriToConstant of string -exception WrongUriToVariable of string -exception WrongUriToMutualInductiveDefinitions of string -exception ListTooShort -exception RelToHiddenHypothesis - -type types = {synthesized : Cic.term ; expected : Cic.term option};; - -module CicHash : - sig - type 'a t - val find : 'a t -> Cic.term -> 'a - end -;; - -val double_type_of : - Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t - -(** Auxiliary functions **) - -(* does_not_occur n te *) -(* returns [true] if [Rel n] does not occur in [te] *) -val does_not_occur : int -> Cic.term -> bool