module D = Deannotate
module PER = ProofEngineReduction
module Ut = CicUtil
+module DTI = DoubleTypeInference
(* fresh name generator *****************************************************)
in
join (aux k context)
-let mk_fresh_name context = function
- | C.Anonymous -> C.Anonymous
+let mk_fresh_name does_not_occur context = function
| C.Name s -> mk_fresh_name context (split s)
+ | C.Anonymous ->
+ if does_not_occur then C.Anonymous
+ else mk_fresh_name context (split "LOCAL")
(* helper functions *********************************************************)
let get_cofix_decl (sname, w, v) = sname, w in
let rec bc c = function
| C.LetIn (name, v, ty, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Def (v, ty)) in
let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
C.LetIn (name, v, ty, t)
| C.Lambda (name, w, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Decl w) in
let w, t = bc c w, bc (entry :: c) t in
C.Lambda (name, w, t)
| C.Prod (name, w, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Decl w) in
let w, t = bc c w, bc (entry :: c) t in
C.Prod (name, w, t)
let get_cofix_decl (id, sname, w, v) = sname, cic w in
let rec bc c = function
| C.ALetIn (id, name, v, ty, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Def (cic v, cic ty)) in
let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
C.ALetIn (id, name, v, ty, t)
| C.ALambda (id, name, w, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Decl (cic w)) in
let w, t = bc c w, bc (entry :: c) t in
C.ALambda (id, name, w, t)
| C.AProd (id, name, w, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Decl (cic w)) in
let w, t = bc c w, bc (entry :: c) t in
C.AProd (id, name, w, t)