X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;h=97353c3e73cee0c1ba5e710fa368f5c399127d1d;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=3f0006a39cf285da71a580ffa57f37b66f1ea87c;hpb=7b922ad1f9832c1edb3acea8f0c910fa2c0c20e5;p=helm.git diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml index 3f0006a39..97353c3e7 100644 --- a/helm/ocaml/cic_unification/freshNamesGenerator.ml +++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml @@ -23,18 +23,23 @@ * 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 context name ~typ = +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 - (match CicTypeChecker.type_of_aux' [] context typ with + 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" @@ -46,17 +51,161 @@ let mk_fresh_name context name ~typ = Str.global_replace (Str.regexp "[0-9]*$") "" name in let already_used name = - List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context + List.exists (function Some (n,_) -> n=name | _ -> false) context in - if not (already_used basename) then + 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' = basename ^ string_of_int n in + let name' = C.Name (basename ^ string_of_int n) in if already_used name' then try_next (n+1) else - C.Name name' + 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) +;;