Optimizer: refactored according to its formal description

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

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index d6638b3f07f5f294d227150f2ad908aca997e38e..3cf4bb596b38a4cd36c20262bc28b2ce67fc6929 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -37,10 +37,10 @@ module Ut   = CicUtil
 module E    = CicEnvironment
 module PEH  = ProofEngineHelpers
 module PER  = ProofEngineReduction
+module Pp   = CicPp
 
 module P    = ProceduralPreprocess
 module Cl   = ProceduralClassify
-module M    = ProceduralMode
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
 
@@ -161,8 +161,6 @@ with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
 let unused_premise = "UNUSED"
 
-let defined_premise = "DEFINED"
-
 let convert st ?name v = 
    match get_inner_types st v with
       | None          -> []
@@ -174,13 +172,9 @@ let convert st ?name v =
            | None    -> [T.Change (st, et, None, e, "")]
            | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
 
-let get_intro name t = 
-try
-match name with 
+let get_intro = function 
    | C.Anonymous -> unused_premise
-   | C.Name s    -> 
-      if DTI.does_not_occur 1 (cic t) then unused_premise else s
-with Invalid_argument _ -> failwith "A2P.get_intro"
+   | C.Name s    -> s
 
 let mk_intros st script =
 try
@@ -189,15 +183,9 @@ try
    T.Intros (Some count, List.rev st.intros, "") :: script
 with Invalid_argument _ -> failwith "A2P.mk_intros"
 
-let rec mk_atomic st dtext what =
-   if T.is_atomic what then 
-      match what with 
-      | C.ARel (_, _, _, name) -> convert st ~name what, what
-      | _                      -> [], what
-   else
-      let name = defined_premise in
-      let script = convert st ~name what in  
-      script @ mk_fwd_proof st dtext name what, T.mk_arel 0 name
+let rec mk_arg st = function
+   | C.ARel (_, _, _, name) as what -> convert st ~name what, what
+   | what                           -> [], what
 
 and mk_fwd_rewrite st dtext name tl direction =   
    assert (List.length tl = 6);
@@ -205,7 +193,7 @@ and mk_fwd_rewrite st dtext name tl direction =
    let e = Cn.mk_pattern 1 predicate in
    match where with
       | C.ARel (_, _, _, premise) ->
-         let script, what = mk_atomic st dtext what in
+         let script, what = mk_arg st what in
          T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script
       | _                         -> assert false
 
@@ -217,21 +205,15 @@ and mk_rewrite st dtext script t what qs tl direction =
    [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
 
 and mk_fwd_proof st dtext name = function
-   | C.ALetIn (_, n, v, t)      ->
-      let entry = Some (n, C.Def (cic v, None)) in
-      let intro = get_intro n t in
-      let qt = mk_fwd_proof (add st entry intro) dtext name t in
-      let qv = mk_fwd_proof st "" intro v in
-      List.append qt qv
    | C.AAppl (_, hd :: tl) as v -> 
       if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
       if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else
       let ty = get_type "TC1" st hd in
       begin match get_inner_types st v with
-         | Some (ity, _) when M.bkd st.context ty ->
+         | Some (ity, _) ->
            let qs = [[T.Id ""]; mk_proof (next st) v] in
            [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
-         | _                                      ->
+         | _             ->
             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)]
@@ -249,13 +231,13 @@ and mk_fwd_proof st dtext name = function
 and mk_proof st = function
    | C.ALambda (_, name, v, t)        ->
       let entry = Some (name, C.Decl (cic v)) in
-      let intro = get_intro name t in
+      let intro = get_intro name in
       mk_proof (add st entry intro) t
    | 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
-         let intro = get_intro name t in
+         let intro = get_intro name in
          let q = mk_proof (next (add st entry intro)) t in
          List.rev_append (mk_fwd_proof st dtext intro v) q
       else
@@ -276,14 +258,19 @@ and mk_proof st = function
       let script = if proceed then
          let ty = get_type "TC2" st hd in
          let (classes, rc) as h = Cl.classify st.context ty in
-         let premises, _ = PEH.split_with_whd (st.context, ty) in
-        assert (List.length classes - List.length tl = 0);
+        let decurry = List.length classes - List.length tl in
+        if decurry <> 0 then begin
+           let msg = Printf.sprintf "Decurry: %i\nTerm: %s\nContext: %s"
+              decurry (Pp.ppterm (cic t)) (Pp.ppcontext st.context)
+           in
+           HLog.warn msg; assert false
+        end;
         let synth = I.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
          match rc with
-            | Some (i, j) when i > 1 && i <= List.length classes && M.is_eliminator premises ->
+            | Some (i, j) ->
               let classes, tl, _, what = split2_last classes tl in
-              let script, what = mk_atomic st dtext what in
+              let script, what = mk_arg st what in
               let synth = I.S.add 1 synth in
               let qs = mk_bkd_proofs (next st) synth classes tl in
                if is_rewrite_right hd then 
@@ -293,13 +280,13 @@ and mk_proof st = function
               else   
                   let l = succ (List.length tl) in
                  let predicate = List.nth tl (l - i) in
-                  let e = Cn.mk_pattern j predicate in
+                  let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in
                  let using = Some hd in
                  List.rev script @ convert st t @
                  [T.Elim (what, using, e, dtext ^ text); T.Branch (qs, "")]
-           | _                                                  ->
+           | None        ->
               let qs = mk_bkd_proofs (next st) synth classes tl in
-              let script, hd = mk_atomic st dtext hd in               
+              let script, hd = mk_arg st hd in               
               List.rev script @ convert st t @        
               [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
       else
@@ -316,7 +303,7 @@ and mk_proof st = function
 and mk_bkd_proofs st synth classes ts =
 try 
    let _, dtext = test_depth st in   
-   let aux inv v =
+   let aux (inv, _) v =
       if I.overlaps synth inv then None else
       if I.S.is_empty inv then Some (mk_proof st v) else
       Some [T.Apply (v, dtext ^ "dependent")]