- we replaced a normalize with a whd in the classification algorithm

[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 fb95a6d0c4cf4e842831398e5f7186ac99ae77ac..54e8ebe050fb5a59cad06150b1c4238daa9da784 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -32,6 +32,8 @@ module PEH  = ProofEngineHelpers
 module E    = CicEnvironment
 module UM   = UriManager
 module D    = Deannotate
+module PER  = ProofEngineReduction
+module Ut   = CicUtil
 
 (* fresh name generator *****************************************************)
 
@@ -81,7 +83,7 @@ let compose f g x = f (g x)
 let fst3 (x, _, _) = x
 
 let refine c t =
-   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
+   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.oblivion_ugraph in t
    with e -> 
       Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
@@ -89,7 +91,7 @@ let refine c t =
       raise e
 
 let get_type c t =
-   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+   try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty
    with e -> 
       Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
       Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
@@ -124,7 +126,7 @@ let is_not_atomic = function
 let is_atomic t = not (is_not_atomic t)
 
 let get_ind_type uri tyno =
-   match E.get_obj Un.empty_ugraph uri with
+   match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
       | _                                           -> assert false
 
@@ -133,7 +135,7 @@ let get_default_eliminator context uri tyno ty =
    let ext = match get_tail context (get_type context ty) with
       | C.Sort C.Prop     -> "_ind"
       | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
+      | C.Sort (C.CProp _)   -> "_rect"
       | C.Sort (C.Type _) -> "_rect"
       | t                 -> 
          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
@@ -159,6 +161,16 @@ let get_ind_parameters c t =
 
 let cic = D.deannotate_term
 
+let occurs c ~what ~where =
+   let result = ref false in
+   let equality c t1 t2 =
+      let r = Ut.alpha_equivalence t1 t2 in
+      result := !result || r; r
+   in
+   let context, what, with_what = c, [what], [C.Rel 0] in
+   let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
+   !result
+
 (* Ensuring Barendregt convenction ******************************************)
 
 let rec add_entries map c = function
@@ -180,11 +192,11 @@ let cic_bc c t =
    let get_fix_decl (sname, i, w, v) = sname, w in
    let get_cofix_decl (sname, w, v) = sname, w in
    let rec bc c = function
-      | C.LetIn (name, v, t) ->
+      | C.LetIn (name, v, ty, t) ->
          let name = mk_fresh_name c name in
-         let entry = Some (name, C.Def (v, None)) in
-         let v, t = bc c v, bc (entry :: c) t in
-        C.LetIn (name, v, t)
+         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 entry = Some (name, C.Decl w) in
@@ -222,11 +234,11 @@ let acic_bc c t =
    let get_fix_decl (id, sname, i, w, v) = sname, cic w in
    let get_cofix_decl (id, sname, w, v) = sname, cic w in
    let rec bc c = function
-      | C.ALetIn (id, name, v, t) ->
+      | C.ALetIn (id, name, v, ty, t) ->
          let name = mk_fresh_name c name in
-         let entry = Some (name, C.Def (cic v, None)) in
-         let v, t = bc c v, bc (entry :: c) t in
-        C.ALetIn (id, name, v, t)
+         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 entry = Some (name, C.Decl (cic w)) in