we rebuilt the dependences

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

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index b3a247b02c448ca53aa7070a677d8f4574f97ef6..3eadc2fcf985395f9613a64a859decb0fb45d515 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -26,18 +26,16 @@
 module C    = Cic
 module E    = CicEnvironment
 module Un   = CicUniv
-module TC   = CicTypeChecker 
-module D    = Deannotate
+module TC   = CicTypeChecker
 module UM   = UriManager
 module Rd   = CicReduction
 module PEH  = ProofEngineHelpers
 module PT   = PrimitiveTactics
-
 module DTI  = DoubleTypeInference
 
-(* helpers ******************************************************************)
+module H    = ProceduralHelpers
 
-let cic = D.deannotate_term
+(* helpers ******************************************************************)
 
 let rec list_sub start length = function
    | _  :: tl when start  > 0 -> list_sub (pred start) length tl
@@ -72,7 +70,7 @@ let lift k n =
       | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
       | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
       | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
-      | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term k ty, lift_term (succ k) t)
+      | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k ty, lift_term k s, lift_term (succ k) t)
       | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
       | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
    in
@@ -126,7 +124,7 @@ let clear_absts m =
       | C.ALambda (_, _, _, t) when n > 0  -> 
          aux 0 (pred n) (lift 1 (-1) t)
       | t                      when n > 0  ->
-           Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (cic t));
+           Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (H.cic t));
            assert false 
       | t                                  -> t
    in 
@@ -210,9 +208,9 @@ let get_clears c p xtypes =
            else 
               hd, names, v
         in
-        let p = C.LetIn (n, v, assert false, p) in
-        let it = C.LetIn (n, v, assert false, it) in
-        let et = C.LetIn (n, v, assert false, et) in
+        let p = C.LetIn (n, v, x, p) in
+        let it = C.LetIn (n, v, x, it) in
+        let et = C.LetIn (n, v, x, et) in
         aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
         let p = C.Lambda (n, meta, p) in
@@ -220,9 +218,9 @@ let get_clears c p xtypes =
         let et = C.Lambda (n, meta, et) in
         aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
-        let p = C.LetIn (n, meta, assert false, p) in
-        let it = C.LetIn (n, meta, assert false, it) in
-        let et = C.LetIn (n, meta, assert false, et) in
+        let p = C.LetIn (n, meta, meta, p) in
+        let it = C.LetIn (n, meta, meta, it) in
+        let et = C.LetIn (n, meta, meta, et) in
         aux (hd :: c) names p it et tl
       | None :: tl                                        -> assert false
    in
@@ -240,8 +238,8 @@ let clear c hyp =
    aux [] c
 
 let elim_inferred_type context goal arg using cpattern =
-   let metasenv, ugraph = [], Un.empty_ugraph in 
-   let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
+   let metasenv, ugraph = [], Un.default_ugraph in
+   let ety = H.get_type "elim_inferred_type" context using in
    let _splits, args_no = PEH.split_with_whd (context, ety) in
    let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim 
       ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no
@@ -249,3 +247,7 @@ let elim_inferred_type context goal arg using cpattern =
    let ty = C.Appl (predicate :: actual_args) in
    let upto = List.length actual_args in
    Rd.head_beta_reduce ~delta:false ~upto ty
+
+let does_not_occur = function
+   | C.AImplicit (_, None) -> true
+   | _                     -> false