cicDischarge: final fixup. Now correctly processes Coq/Init/Logic.mma :)

[helm.git] / helm / software / components / cic_proof_checking / cicDischarge.ml

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index 4ad41eef774913594c15f865c304c74ce07e92a2..65b5cea3393918525b68a721f7713b39955f32a0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicDischarge.ml
+++ b/helm/software/components/cic_proof_checking/cicDischarge.ml
@@ -211,12 +211,20 @@ let rec discharge_term st t = match t with
            C.Lambda (C.Anonymous, vty, S.lift 1 wb)
         else
 (* Fixing needed, some right parametes *)
-        if frpsno = rpsno then
-            let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
+        if frpsno = rpsno && named then
+           let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
            if !debug then begin
               out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
            end;
-           let vty, wb = S.lift rpsno vty, S.lift (succ rpsno) wb in 
+           let vty, wb = S.lift rpsno vty, S.lift 1 wb in 
+           let vty = match vty with
+              | C.Appl (C.MutInd (fu, fm, _) as hd :: args) 
+                 when UM.eq fu u && fm = m && List.length args = psno ->
+                 let largs, _ = X.split_nth lpsno args in
+                 C.Appl (hd :: largs @ Ut.mk_rels rpsno 0)  
+              | _                                                     ->
+                 assert false
+           in
            close false wc (C.Lambda (C.Anonymous, vty, wb))
 (* This case should not happen *)
         else assert false 
@@ -294,14 +302,14 @@ let rec discharge_object dn du obj =
       if w' == w && vars = [] then obj else
       let w'' = sh w w' in
 (* We do not typecheck because variables are not closed *)
-      C.Variable (dn b, None, w'', [], attrs)
+      C.Variable (dn b, None, w'', vars, attrs)
    | C.Variable (b, Some v, w, vars, attrs)            ->
       let st = init_status dn du ls vars in
       let w', v' = discharge_term st w, discharge_term st v in
       if w' == w && v' == v && vars = [] then obj else
       let w'', v'' = sh w w', sh v v' in
 (* We do not typecheck because variables are not closed *)
-      C.Variable (dn b, Some v'', w'', [], attrs)
+      C.Variable (dn b, Some v'', w'', vars, attrs)
    | C.Constant (b, None, w, vars, attrs)              ->
       let st = init_status dn du ls vars in
       let w' = discharge_term st w in
@@ -338,14 +346,23 @@ and discharge_uri dn du uri =
    obj', obj' == obj
 
 and discharge_vars dn du vars =
-(* We should check that the dependences are ordered telesopically *)   
-   let map u =
-      match discharge_uri dn du u with
-         | C.Variable (b, None, w, _, _), _   -> Some (C.Name b, C.Decl w)
-         | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
-        | _                                  -> None
-   in
-   List.rev_map map vars
+   let rec aux us c = function
+      | []      -> c
+      | u :: tl ->
+         let e = match discharge_uri dn du u with
+            | C.Variable (b, None, w, vars, _), _   -> 
+              let map = relocate us (List.rev vars) in 
+              let w = S.lift_map 1 map w in
+              Some (C.Name b, C.Decl w)
+            | C.Variable (b, Some v, w, vars, _), _ -> 
+              let map = relocate us (List.rev vars) in
+              let v, w = S.lift_map 1 map v, S.lift_map 1 map w in
+              Some (C.Name b, C.Def (v, w))
+           | _                                     -> assert false
+         in
+                aux (u :: us) (e :: c) tl
+   in 
+   aux [] [] vars
 
 and init_status dn du ls vars =
    let c, rl = discharge_vars dn du vars, List.rev vars in