- Procedural: new flag "level=n" to control the reconstruction level (defaults to...

[helm.git] / helm / software / components / acic_procedural / proceduralHelpers.ml

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index a9fa6473f280ac7e12fc50422181b99cf0a248cf..b2f73f311a9d932374fb4694432c6be0a2469469 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -34,6 +34,7 @@ module UM   = UriManager
 module D    = Deannotate
 module PER  = ProofEngineReduction
 module Ut   = CicUtil
+module DTI  = DoubleTypeInference
 
 (* fresh name generator *****************************************************)
 
@@ -61,9 +62,11 @@ let mk_fresh_name context (name, k) =
    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 *********************************************************)
 
@@ -245,17 +248,20 @@ let cic_bc c t =
    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)
@@ -287,17 +293,20 @@ let acic_bc c 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)
@@ -326,3 +335,10 @@ let acic_bc c t =
       | t -> t
    in 
    bc c t
+
+let is_acic_proof sorts context v =
+   let id = Ut.id_of_annterm v in
+   try match Hashtbl.find sorts id with
+      | `Prop -> true
+      | _     -> false
+   with Not_found -> is_proof context (cic v)