procedural : some improvements.

[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 e26dd68a2ac23004f0e0de013d6cef8aa91ca8fd..22936c1a4531a6338dcb2ca3e7916cf062f41490 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -34,8 +34,10 @@ module HObj = HelmLibraryObjects
 module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
+module PER  = ProofEngineReduction
 
-module Cl   = CicClassify
+module Cl   = ProceduralClassify
+module M    = ProceduralMode
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
 
@@ -153,6 +155,14 @@ let assumed_premise = "ASSUMED"
 
 let expanded_premise = "EXPANDED"
 
+let convert st v = 
+   match get_inner_types st v with
+      | Some (st, et) ->
+         let cst, cet = cic st, cic et in
+        if PER.alpha_equivalence cst cet then [] else 
+        [T.Change (st, et, "")]
+      | None          -> []
+
 let eta_expand n t =
    let ty = C.AImplicit ("", None) in
    let name i = Printf.sprintf "%s%u" expanded_premise i in 
@@ -218,24 +228,29 @@ and mk_fwd_rewrite st dtext name tl direction =
          [T.Branch (qs, ""); p2; p1] 
 
 and mk_fwd_proof st dtext name = function
-   | C.AAppl (_, hd :: tl) as v -> 
+   | C.AAppl (_, hd :: tl) as v                         -> 
       if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else  
       if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
+      let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
       begin match get_inner_types st v with
-         | Some (ity, _) ->
+         | Some (ity, _) when M.bkd st.context ty ->
            let qs = [[T.Id ""]; mk_proof (next st) v] in
            [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
-         | None          ->
-            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 text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
             [T.LetIn (name, v, dtext ^ text)]
       end
-   | v                          -> 
-      [T.LetIn (name, v, dtext)] 
+   | 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
+   | v                                                  ->
+      [T.LetIn (name, v, dtext)]
 
 and mk_proof st = function
-   | C.ALambda (_, name, v, t) as what -> 
+   | C.ALambda (_, name, v, t) as what             ->
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
       let ety = match get_inner_types st what with
@@ -243,7 +258,7 @@ and mk_proof st = function
         | None          -> None
       in
       mk_proof (add st entry intro ety) t
-   | C.ALetIn (_, name, v, t) as what  ->
+   | C.ALetIn (_, name, v, t) as what              ->
       let proceed, dtext = test_depth st in
       let script = if proceed then 
          let entry = Some (name, C.Def (cic v, None)) in
@@ -254,16 +269,16 @@ and mk_proof st = function
         [T.Apply (what, dtext)]
       in
       mk_intros st script
-   | C.ARel _ as what                  ->
+   | C.ARel _ as what                              ->
       let _, dtext = test_depth st in
       let text = "assumption" in
       let script = [T.Apply (what, dtext ^ text)] in 
       mk_intros st script
-   | C.AMutConstruct _ as what         ->
+   | C.AMutConstruct _ as what                     ->
       let _, dtext = test_depth st in
       let script = [T.Apply (what, dtext)] in 
       mk_intros st script   
-   | C.AAppl (_, hd :: tl) as t        ->
+   | C.AAppl (_, hd :: tl) as t                    ->
       let proceed, dtext = test_depth st in
       let script = if proceed then
          let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
@@ -280,25 +295,33 @@ and mk_proof st = function
               let synth = Cl.S.add 1 synth in
               let qs = mk_bkd_proofs (next st) synth classes tl in
                if is_rewrite_right hd then 
-                 List.rev script @ 
+                 List.rev script @ convert st t @
                  [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
               else if is_rewrite_left hd then 
-                 List.rev script @
+                 List.rev script @ convert st t @
                  [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
               else   
                  let using = Some hd in
-                 List.rev script @
+                 List.rev script @ convert st t @
                  [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
            | _                                                  ->
               let qs = mk_bkd_proofs (next st) synth classes tl in
               let script, hd = mk_atomic st dtext hd in               
-              List.rev script @               
+              List.rev script @ convert st t @        
               [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
       else
          [T.Apply (t, dtext)]
       in
       mk_intros st script
-   | t                                 ->
+   | C.AMutCase (id, uri, tyno, outty, arg, cases) ->
+      begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
+         | None   -> 
+            let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in
+            let script = [T.Note text] in
+            mk_intros st script
+         | Some t -> mk_proof st t
+      end
+   | t                                             ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in
       mk_intros st script