Procedural: bug fix

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

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index bbc358f71e7fbc0db2eebce8f7624e393d072877..e91c4bdfc1b9c8f24bb94c9ed83d9fef15dc418b 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -37,6 +37,7 @@ module Ut   = CicUtil
 module E    = CicEnvironment
 module PER  = ProofEngineReduction
 
+module P    = ProceduralPreprocess
 module Cl   = ProceduralClassify
 module M    = ProceduralMode
 module T    = ProceduralTypes
@@ -218,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
@@ -226,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)                           ->
@@ -247,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
@@ -262,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
@@ -292,7 +297,7 @@ and mk_proof st = function
       let script = if proceed then
          let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
          let (classes, rc) as h = Cl.classify st.context ty in
-         let premises, _ = Cl.split st.context ty in
+         let premises, _ = P.split st.context ty in
         let decurry = List.length classes - List.length tl in
          if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
          if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
@@ -341,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