Procedural: bug fix

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 28fa9894795e52e629d6cfdf1d14a3064ccfebf6..e91c4bdfc1b9c8f24bb94c9ed83d9fef15dc418b 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -219,6 +219,7 @@ let rec mk_atomic st dtext what =
       script @ mk_fwd_proof st dtext name what, T.mk_arel 0 name
 
 and mk_fwd_rewrite st dtext name tl direction =
+try   
    let what, where = List.nth tl 5, List.nth tl 3 in
    let rps, predicate = [List.nth tl 4], List.nth tl 2 in
    let e = Cn.mk_pattern rps predicate in
@@ -227,6 +228,7 @@ and mk_fwd_rewrite st dtext name tl direction =
          let script, what = mk_atomic st dtext what in
          T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script
       | _                         -> assert false
+with e -> failwith ("mk_fwd_rewrite: " ^ Printexc.to_string e)
 
 and mk_fwd_proof st dtext name = function
    | C.ALetIn (_, n, v, t)                           ->
@@ -248,12 +250,12 @@ and mk_fwd_proof st dtext name = function
             let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
            [T.LetIn (name, v, dtext ^ text)]
       end
-   | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
+(*   | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
       begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
          | None   -> [T.LetIn (name, v, dtext)] 
          | Some v -> mk_fwd_proof st dtext name v
       end
-   | C.ACast (_, v, _)                                  ->
+*)   | C.ACast (_, v, _)                                  ->
       mk_fwd_proof st dtext name v
    | v                                                  ->
       match get_inner_types st v with
@@ -263,7 +265,9 @@ and mk_fwd_proof st dtext name = function
          | _             ->
             [T.LetIn (name, v, dtext)]
 
-and mk_proof st = function
+and mk_proof st t = 
+try   
+   match t with
    | C.ALambda (_, name, v, t)                     ->
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
@@ -342,6 +346,7 @@ and mk_proof st = function
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in
       mk_intros st script
+with e -> failwith ("mk_proof: " ^ Printexc.to_string e)
 
 and mk_bkd_proofs st synth classes ts =
 try 

diff --git a/helm/software/components/acic_procedural/proceduralPreprocess.ml b/helm/software/components/acic_procedural/proceduralPreprocess.ml
index d31d0113b9067b6ba0c3b456fd8a2a1329ae3450..4862db759178c25e7d66bd8524854079738c26e7 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralPreprocess.ml
+++ b/helm/software/components/acic_procedural/proceduralPreprocess.ml
@@ -26,7 +26,7 @@
 module C    = Cic
 module Un   = CicUniv
 module S    = CicSubstitution
-module R    = CicReduction
+module Rd   = CicReduction
 module TC   = CicTypeChecker 
 module DTI  = DoubleTypeInference
 module HEL  = HExtlib
@@ -41,7 +41,7 @@ let get_type c t =
    let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
 
 let is_proof c t =
-   match (get_type c (get_type c t)) with
+   match Rd.whd ~delta:true c (get_type c (get_type c t)) with
       | C.Sort C.Prop -> true
       | _             -> false
 
@@ -59,7 +59,7 @@ let split c t =
    let rec aux whd a n c = function
       | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
       | v when whd        -> v :: a, n
-      | v                 -> aux true a n c (R.whd ~delta:true c v)
+      | v                 -> aux true a n c (Rd.whd ~delta:true c v)
     in
     aux false [] 0 c t
 
@@ -78,19 +78,25 @@ let expanded_premise = "EXPANDED"
 
 let defined_premise = "DEFINED"
 
-let eta_expand n t =
-   let ty = C.Implicit None in
+let eta_expand tys t =
+   let n = List.length tys in
    let name i = Printf.sprintf "%s%u" expanded_premise i in 
-   let lambda i t = C.Lambda (C.Name (name i), ty, t) in
+   let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
    let arg i n = C.Rel (n - i) in
-   let rec aux i f a =
-      if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
+   let rec aux i f a = function
+      | []       -> f, a 
+      | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i n :: a) tl
    in
-   let absts, args = aux 0 identity [] in
+   let absts, args = aux 0 identity [] tys in
    absts (C.Appl (S.lift n t :: args))
 
-let eta_fix t proof decurry =
-   if proof && decurry > 0 then eta_expand decurry t else t
+let get_tys c decurry t = 
+   let tys, _ = split c (get_type c t) in
+   let tys, _ = HEL.split_nth decurry (List.tl tys) in
+   List.rev tys
+
+let eta_fix c t proof decurry =
+   if proof && decurry > 0 then eta_expand (get_tys c decurry t) t else t
 
 let rec pp_cast g ht es c t v =
    if es then pp_proof g ht es c t else find g ht t
@@ -99,7 +105,7 @@ and pp_lambda g ht es c name v t =
    let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
    let entry = Some (name, C.Decl v) in
    let g t _ decurry = 
-      let t = eta_fix t true decurry in
+      let t = eta_fix (entry :: c) t true decurry in
       g (C.Lambda (name, v, t)) true 0 in
    if es then pp_proof g ht es (entry :: c) t else find g ht t
 
@@ -112,7 +118,7 @@ and pp_letin g ht es c name v t =
             let x = C.LetIn (mame, w, C.LetIn (name, u, S.lift_from 2 1 t)) in
            pp_proof g ht false c x 
          | v                               -> 
-            let v = eta_fix v proof d in
+            let v = eta_fix c v proof d in
            g (C.LetIn (name, v, t)) true decurry
       in
       if es then pp_term g ht es c v else find g ht v
@@ -130,7 +136,7 @@ and pp_appl_one g ht es c t v =
                let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in
               pp_proof g ht false c x
            | C.Appl ts, v when decurry > 0      ->
-              let v = eta_fix v proof d in
+              let v = eta_fix c v proof d in
               g (C.Appl (List.append ts [v])) true (pred decurry)
            | t, v  when is_not_atomic t         ->
               let mame = C.Name defined_premise in
@@ -138,7 +144,7 @@ and pp_appl_one g ht es c t v =
               pp_proof g ht false c x
            | t, v                               ->
                let _, premsno = split c (get_type c t) in
-              let v = eta_fix v proof d in
+              let v = eta_fix c v proof d in
                g (C.Appl [t; v]) true (pred premsno)
       in
       if es then pp_term g ht es c v else find g ht v
@@ -169,9 +175,10 @@ and pp_term g ht es c t =
 let pp_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
       let g bo proof decurry = 
-         let bo = eta_fix bo proof decurry in
+         let bo = eta_fix [] bo proof decurry in
          C.Constant (name, Some bo, ty, pars, attrs)
       in
       let ht = C.CicHash.create 1 in
-      pp_term g ht true [] bo
+      begin try pp_term g ht true [] bo
+      with e -> failwith ("PPP: " ^ Printexc.to_string e) end
    | obj                                         -> obj