* 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 metasenv 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' metasenv 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"
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
;;
in
C.Meta(i,l'),rels
| C.Sort _ as t -> t,[]
- | C.Implicit 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
let n' =
match n with
C.Anonymous ->
- if List.mem k rels2 then assert false else 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