From: Andrea Asperti Date: Tue, 19 Jul 2005 11:17:13 +0000 (+0000) Subject: freshNamesGenerator moved into cic_proof_checking. X-Git-Tag: V_0_7_2~179 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97b6922862815029492f65a587172ef8c728b677;p=helm.git freshNamesGenerator moved into cic_proof_checking. --- diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index d3d898457..d4b95366d 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -2,17 +2,13 @@ cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi cicMkImplicit.cmx: cicMkImplicit.cmi -freshNamesGenerator.cmo: freshNamesGenerator.cmi -freshNamesGenerator.cmx: freshNamesGenerator.cmi -cicUnification.cmo: freshNamesGenerator.cmi cicMetaSubst.cmi \ - cicUnification.cmi -cicUnification.cmx: freshNamesGenerator.cmx cicMetaSubst.cmx \ - cicUnification.cmi +cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi +cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi -coercGraph.cmo: freshNamesGenerator.cmi coercDb.cmi coercGraph.cmi -coercGraph.cmx: freshNamesGenerator.cmx coercDb.cmx coercGraph.cmi -cicRefine.cmo: freshNamesGenerator.cmi coercGraph.cmi cicUnification.cmi \ - cicMkImplicit.cmi cicMetaSubst.cmi cicRefine.cmi -cicRefine.cmx: freshNamesGenerator.cmx coercGraph.cmx cicUnification.cmx \ - cicMkImplicit.cmx cicMetaSubst.cmx cicRefine.cmi +coercGraph.cmo: coercDb.cmi coercGraph.cmi +coercGraph.cmx: coercDb.cmx coercGraph.cmi +cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \ + cicMetaSubst.cmi cicRefine.cmi +cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \ + cicMetaSubst.cmx cicRefine.cmi diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index f5699c025..7f1c8f351 100644 --- a/helm/ocaml/cic_unification/Makefile +++ b/helm/ocaml/cic_unification/Makefile @@ -5,7 +5,6 @@ PREDICATES = INTERFACE_FILES = \ cicMetaSubst.mli \ cicMkImplicit.mli \ - freshNamesGenerator.mli \ cicUnification.mli \ coercDb.mli \ coercGraph.mli \ diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml deleted file mode 100644 index 97353c3e7..000000000 --- a/helm/ocaml/cic_unification/freshNamesGenerator.ml +++ /dev/null @@ -1,211 +0,0 @@ -(* Copyright (C) 2004, 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/. - *) - -let debug_print = fun _ -> () - -(* mk_fresh_name context name typ *) -(* returns an identifier which is fresh in the context *) -(* and that resembles [name] as much as possible. *) -(* [typ] will be the type of the variable *) -let mk_fresh_name ~subst metasenv context name ~typ = - let module C = Cic in - let basename = - match name with - C.Anonymous -> - (*CSC: great space for improvements here *) - (try - let ty,_ = - CicTypeChecker.type_of_aux' ~subst metasenv context typ - CicUniv.empty_ugraph in - (match ty with - C.Sort C.Prop - | C.Sort C.CProp -> "H" - | C.Sort C.Set -> "x" - | _ -> "H" - ) - with CicTypeChecker.TypeCheckerFailure _ -> "H" - ) - | C.Name name -> - Str.global_replace (Str.regexp "[0-9]*$") "" name - in - let already_used name = - List.exists (function Some (n,_) -> n=name | _ -> false) context - in - if name <> C.Anonymous && not (already_used name) then - name - else if not (already_used (C.Name basename)) then - C.Name basename - else - let rec try_next n = - let name' = C.Name (basename ^ string_of_int n) in - if already_used name' then - try_next (n+1) - else - name' - in - try_next 1 -;; - -(* clean_dummy_dependent_types term *) -(* returns a copy of [term] where every dummy dependent product *) -(* have been replaced with a non-dependent product and where *) -(* dummy let-ins have been removed. *) -let clean_dummy_dependent_types t = - let module C = Cic in - let rec aux k = - function - C.Rel m as t -> t,[k - m] - | C.Var (uri,exp_named_subst) -> - let exp_named_subst',rels = - List.fold_right - (fun (uri,t) (exp_named_subst,rels) -> - let t',rels' = aux k t in - (uri,t')::exp_named_subst, rels' @ rels - ) exp_named_subst ([],[]) - in - C.Var (uri,exp_named_subst'),rels - | C.Meta (i,l) -> - let l',rels = - List.fold_right - (fun t (l,rels) -> - let t',rels' = - match t with - None -> None,[] - | Some t -> - let t',rels' = aux k t in - Some t', rels' - in - t'::l, rels' @ rels - ) l ([],[]) - in - C.Meta(i,l'),rels - | C.Sort _ as t -> t,[] - | C.Implicit _ as t -> t,[] - | C.Cast (te,ty) -> - let te',rels1 = aux k te in - let ty',rels2 = aux k ty in - C.Cast (te', ty'), rels1@rels2 - | C.Prod (n,s,t) -> - let s',rels1 = aux k s in - let t',rels2 = aux (k+1) t in - let n' = - match n with - C.Anonymous -> - if List.mem k rels2 then -( - debug_print "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ; - C.Anonymous -) - else - C.Anonymous - | C.Name _ as n -> - if List.mem k rels2 then n else C.Anonymous - in - C.Prod (n', s', t'), rels1@rels2 - | C.Lambda (n,s,t) -> - let s',rels1 = aux k s in - let t',rels2 = aux (k+1) t in - C.Lambda (n, s', t'), rels1@rels2 - | C.LetIn (n,s,t) -> - let s',rels1 = aux k s in - let t',rels2 = aux (k+1) t in - let rels = rels1 @ rels2 in - if List.mem k rels2 then - C.LetIn (n, s', t'), rels - else - (* (C.Rel 1) is just a dummy term; any term would fit *) - CicSubstitution.subst (C.Rel 1) t', rels - | C.Appl l -> - let l',rels = - List.fold_right - (fun t (exp_named_subst,rels) -> - let t',rels' = aux k t in - t'::exp_named_subst, rels' @ rels - ) l ([],[]) - in - C.Appl l', rels - | C.Const (uri,exp_named_subst) -> - let exp_named_subst',rels = - List.fold_right - (fun (uri,t) (exp_named_subst,rels) -> - let t',rels' = aux k t in - (uri,t')::exp_named_subst, rels' @ rels - ) exp_named_subst ([],[]) - in - C.Const (uri,exp_named_subst'),rels - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst',rels = - List.fold_right - (fun (uri,t) (exp_named_subst,rels) -> - let t',rels' = aux k t in - (uri,t')::exp_named_subst, rels' @ rels - ) exp_named_subst ([],[]) - in - C.MutInd (uri,tyno,exp_named_subst'),rels - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst',rels = - List.fold_right - (fun (uri,t) (exp_named_subst,rels) -> - let t',rels' = aux k t in - (uri,t')::exp_named_subst, rels' @ rels - ) exp_named_subst ([],[]) - in - C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels - | C.MutCase (sp,i,outty,t,pl) -> - let outty',rels1 = aux k outty in - let t',rels2 = aux k t in - let pl',rels3 = - List.fold_right - (fun t (exp_named_subst,rels) -> - let t',rels' = aux k t in - t'::exp_named_subst, rels' @ rels - ) pl ([],[]) - in - C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3 - | C.Fix (i, fl) -> - let len = List.length fl in - let fl',rels = - List.fold_right - (fun (name,i,ty,bo) (fl,rels) -> - let ty',rels1 = aux k ty in - let bo',rels2 = aux (k + len) bo in - (name,i,ty',bo')::fl, rels1 @ rels2 @ rels - ) fl ([],[]) - in - C.Fix (i, fl'),rels - | C.CoFix (i, fl) -> - let len = List.length fl in - let fl',rels = - List.fold_right - (fun (name,ty,bo) (fl,rels) -> - let ty',rels1 = aux k ty in - let bo',rels2 = aux (k + len) bo in - (name,ty',bo')::fl, rels1 @ rels2 @ rels - ) fl ([],[]) - in - C.CoFix (i, fl'),rels - in - fst (aux 0 t) -;; diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli deleted file mode 100644 index 036ba07a9..000000000 --- a/helm/ocaml/cic_unification/freshNamesGenerator.mli +++ /dev/null @@ -1,38 +0,0 @@ -(* Copyright (C) 2004, 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/. - *) - -(* mk_fresh_name metasenv context name typ *) -(* returns an identifier which is fresh in the context *) -(* and that resembles [name] as much as possible. *) -(* [typ] will be the type of the variable *) -val mk_fresh_name : - subst:Cic.substitution -> - Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name - -(* clean_dummy_dependent_types term *) -(* returns a copy of [term] where every dummy dependent product *) -(* have been replaced with a non-dependent product and where *) -(* dummy let-ins have been removed. *) -val clean_dummy_dependent_types : Cic.term -> Cic.term