From e5108fbb1b112d713e611f7dbcd8a2ab8002e9a5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 19 Jul 2005 11:13:33 +0000 Subject: [PATCH] Moved freshNameGenerator inside cic_proof_checking (and revised). CVS : --- helm/ocaml/cic_proof_checking/.depend | 4 + helm/ocaml/cic_proof_checking/Makefile | 1 + helm/ocaml/cic_proof_checking/cicElim.ml | 17 +- .../cic_proof_checking/freshNamesGenerator.ml | 352 ++++++++++++++++++ .../freshNamesGenerator.mli | 46 +++ 5 files changed, 415 insertions(+), 5 deletions(-) create mode 100755 helm/ocaml/cic_proof_checking/freshNamesGenerator.ml create mode 100644 helm/ocaml/cic_proof_checking/freshNamesGenerator.mli diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index e99b1253d..b41b42a93 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -18,6 +18,10 @@ cicTypeChecker.cmo: cicUnivUtils.cmi cicSubstitution.cmi cicReduction.cmi \ cicPp.cmi cicLogger.cmi cicEnvironment.cmi cicTypeChecker.cmi cicTypeChecker.cmx: cicUnivUtils.cmx cicSubstitution.cmx cicReduction.cmx \ cicPp.cmx cicLogger.cmx cicEnvironment.cmx cicTypeChecker.cmi +freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \ + freshNamesGenerator.cmi +freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \ + freshNamesGenerator.cmi cicElim.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicReduction.cmi \ cicPp.cmi cicEnvironment.cmi cicElim.cmi cicElim.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicReduction.cmx \ diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 63d79e14e..530f42640 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -14,6 +14,7 @@ INTERFACE_FILES = \ cicMiniReduction.mli \ cicReduction.mli \ cicTypeChecker.mli \ + freshNamesGenerator.mli \ cicElim.mli \ cicRecord.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index ab7ddd0e1..869d5d08b 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -28,13 +28,16 @@ open Printf exception Elim_failure of string exception Can_t_eliminate -let debug_print = fun _ -> () +(* +let debug_print = fun _ -> () *) +let debug_print = prerr_endline let counter = ref ~-1 ;; -let fresh_binder () = +let fresh_binder () = Cic.Name "matita_dummy" +(* incr counter; - Cic.Name ("e" ^ string_of_int !counter) + Cic.Name ("e" ^ string_of_int !counter) *) (** verifies if a given inductive type occurs in a term in target position *) let rec recursive uri typeno = function @@ -364,10 +367,14 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = in add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic in -(* debug_print (CicPp.ppterm eliminator_type); debug_print (CicPp.ppterm eliminator_body); -*) + let eliminator_type = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in + let eliminator_body = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in +debug_print (CicPp.ppterm eliminator_type); +debug_print (CicPp.ppterm eliminator_body); let (computed_type, ugraph) = try CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph diff --git a/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml b/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml new file mode 100755 index 000000000..67d213547 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml @@ -0,0 +1,352 @@ +(* 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 _ -> () + +let rec higher_name arity = + function + Cic.Sort Cic.Prop + | Cic.Sort Cic.CProp -> + if arity = 0 then "A" (* propositions *) + else if arity = 1 then "P" (* predicates *) + else "R" (*relations *) + | Cic.Sort Cic.Set + -> if arity = 0 then "S" else "F" + | Cic.Sort (Cic.Type _ ) -> + if arity = 0 then "T" else "F" + | Cic.Prod (_,_,t) -> higher_name (arity+1) t + | _ -> "f" + +let get_initial s = + if String.length s = 0 then "_" + else + let head = String.sub s 0 1 in + String.lowercase head + +(* only used when the sort is not Prop or CProp *) +let rec guess_a_name context ty = + match ty with + Cic.Rel n -> + (match List.nth context (n-1) with + None -> assert false + | Some (Cic.Anonymous,_) -> assert false + | Some (Cic.Name s,_) -> get_initial s) + | Cic.Var (uri,_) -> get_initial (UriManager.name_of_uri uri) + | Cic.Sort _ -> higher_name 0 ty + | Cic.Implicit _ -> assert false + | Cic.Cast (t1,t2) -> guess_a_name context t1 + | Cic.Prod (na_,_,t) -> higher_name 1 t + | Cic.Lambda _ -> assert false + | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst s t) + | Cic.Appl [] -> assert false + | Cic.Appl (he::_) -> guess_a_name context he + | Cic.Const (uri,_) + | Cic.MutInd (uri,_,_) + | Cic.MutConstruct (uri,_,_,_) -> get_initial (UriManager.name_of_uri uri) + | _ -> "x" + +(* 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 -> + (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" + | _ -> guess_a_name context typ + ) + 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 +;; + +(* let mk_fresh_names ~subst metasenv context t *) +let rec mk_fresh_names ~subst metasenv context t = + match t with + Cic.Rel _ -> t + | Cic.Var (uri,exp_named_subst) -> + let ens = + List.map + (fun (uri,t) -> + (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in + Cic.Var (uri,ens) + | Cic.Meta (i,l) -> + let l' = + List.map + (fun t -> + match t with + None -> None + | Some t -> Some (mk_fresh_names ~subst metasenv context t)) l in + Cic.Meta(i,l') + | Cic.Sort _ + | Cic.Implicit _ -> t + | Cic.Cast (te,ty) -> + let te' = mk_fresh_names ~subst metasenv context te in + let ty' = mk_fresh_names ~subst metasenv context ty in + Cic.Cast (te', ty') + | Cic.Prod (n,s,t) -> + let s' = mk_fresh_names ~subst metasenv context s in + let n' = + match n with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name "matita_dummy" -> + mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' + | _ -> n in + let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in + Cic.Prod (n',s',t') + | Cic.Lambda (n,s,t) -> + let s' = mk_fresh_names ~subst metasenv context s in + let n' = + match n with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name "matita_dummy" -> + mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' + | _ -> n in + let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in + Cic.Lambda (n',s',t') + | Cic.LetIn (n,s,t) -> + let s' = mk_fresh_names ~subst metasenv context s in + let n' = + match n with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name "matita_dummy" -> + mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' + | _ -> n in + let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in + Cic.LetIn (n',s',t') + | Cic.Appl l -> + Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l) + | Cic.Const (uri,exp_named_subst) -> + let ens = + List.map + (fun (uri,t) -> + (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in + Cic.Const(uri,ens) + | Cic.MutInd (uri,tyno,exp_named_subst) -> + let ens = + List.map + (fun (uri,t) -> + (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in + Cic.MutInd (uri,tyno,ens) + | Cic.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let ens = + List.map + (fun (uri,t) -> + (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in + Cic.MutConstruct (uri,tyno,consno, ens) + | Cic.MutCase (sp,i,outty,t,pl) -> + let outty' = mk_fresh_names ~subst metasenv context outty in + let t' = mk_fresh_names ~subst metasenv context t in + let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in + Cic.MutCase (sp, i, outty', t', pl') + | Cic.Fix (i, fl) -> + let tys = List.map + (fun (n,_,ty,_) -> + Some (Cic.Name n,(Cic.Decl ty))) fl in + let fl' = List.map + (fun (n,i,ty,bo) -> + let ty' = mk_fresh_names ~subst metasenv context ty in + let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in + (n,i,ty',bo')) fl in + Cic.Fix (i, fl') + | Cic.CoFix (i, fl) -> + let tys = List.map + (fun (n,_,ty) -> + Some (Cic.Name n,(Cic.Decl ty))) fl in + let fl' = List.map + (fun (n,ty,bo) -> + let ty' = mk_fresh_names ~subst metasenv context ty in + let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in + (n,ty',bo')) fl in + Cic.CoFix (i, fl') +;; + +(* 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_proof_checking/freshNamesGenerator.mli b/helm/ocaml/cic_proof_checking/freshNamesGenerator.mli new file mode 100644 index 000000000..b90c0f2f5 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/freshNamesGenerator.mli @@ -0,0 +1,46 @@ +(* 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 + +(* mk_fresh_names metasenv context term *) +(* returns a term t' convertible with term where all *) +(* matita_dummies have been replaced by fresh names *) + +val mk_fresh_names : + subst:Cic.substitution -> + Cic.metasenv -> Cic.context -> Cic.term -> Cic.term + +(* 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 -- 2.39.2