let rec higher_name arity =
function
Cic.Sort Cic.Prop
- | Cic.Sort Cic.CProp ->
+ | Cic.Sort (Cic.CProp _) ->
if arity = 0 then "A" (* propositions *)
else if arity = 1 then "P" (* predicates *)
else "R" (*relations *)
| 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 ~avoid_beta_redexes:true s t)
+(* warning: on appl we should beta reduce before the recursive call
+ | Cic.Lambda _ -> assert false
+*)
+ | Cic.LetIn (_,s,_,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t)
| Cic.Appl [] -> assert false
| Cic.Appl (he::_) -> guess_a_name context he
| Cic.Const (uri,_)
(try
let ty,_ =
CicTypeChecker.type_of_aux' ~subst metasenv context typ
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph
+ in
(match ty with
C.Sort C.Prop
- | C.Sort C.CProp -> "H"
+ | 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
+ Str.global_replace (Str.regexp "[0-9']*$") "" name
in
let already_used name =
List.exists (function Some (n,_) -> n=name | _ -> false) context
| _ -> 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) ->
+ | Cic.LetIn (n,s,ty,t) ->
let s' = mk_fresh_names ~subst metasenv context s in
+ let ty' = mk_fresh_names ~subst metasenv context ty 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')
+ let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',ty'))::context) t in
+ Cic.LetIn (n',s',ty',t')
| Cic.Appl l ->
Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
| Cic.Const (uri,exp_named_subst) ->
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 tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
+ in
let fl' = List.map
(fun (n,i,ty,bo) ->
let ty' = mk_fresh_names ~subst metasenv context ty 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 tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
+ in
let fl' = List.map
(fun (n,ty,bo) ->
let ty' = mk_fresh_names ~subst metasenv context ty in
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) ->
+ | C.LetIn (n,s,ty,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
+ let ty',rels2 = aux k ty in
+ let t',rels3 = aux (k+1) t in
+ let rels = rels1 @ rels2 @ rels3 in
+ if List.mem k rels3 then
+ C.LetIn (n, s', ty', t'), rels
else
(* (C.Rel 1) is just a dummy term; any term would fit *)
CicSubstitution.subst (C.Rel 1) t', rels