- 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 42214b57bc4861f979ddac93f83569e09dbb437c..cf8159b0c06c7c6d49d7d97b9224d98ad5786911 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -55,7 +55,7 @@ type status = {
 
 (* helpers ******************************************************************)
 
-let id x = x
+let identity x = x
 
 let comp f g x = f (g x)
 
@@ -115,6 +115,18 @@ let is_rewrite_left = function
    | C.AConst (_, uri, []) ->
       UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
    | _                     -> false
+
+let is_fwd_rewrite_right hd tl =
+   if is_rewrite_right hd then match List.nth tl 3 with
+      | C.ARel _ -> true
+      | _        -> false
+   else false
+
+let is_fwd_rewrite_left hd tl =
+   if is_rewrite_left hd then match List.nth tl 3 with
+      | C.ARel _ -> true
+      | _        -> false
+   else false
 (*
 let get_ind_name uri tno xcno =
 try   
@@ -156,23 +168,26 @@ let assumed_premise = "ASSUMED"
 
 let expanded_premise = "EXPANDED"
 
-let convert st v = 
+let convert st ?name v = 
    match get_inner_types st v with
+      | None          -> []
       | Some (st, et) ->
          let cst, cet = cic st, cic et in
         if PER.alpha_equivalence cst cet then [] else 
-        [T.Change (st, et, "")]
-      | None          -> []
+        match name with
+           | None    -> [T.Change (st, et, None, "")]
+           | Some id -> [T.Change (st, et, Some (id, id), ""); T.ClearBody (id, "")]
 
 let eta_expand n t =
+   let id = Ut.id_of_annterm t in
    let ty = C.AImplicit ("", None) in
    let name i = Printf.sprintf "%s%u" expanded_premise i in 
-   let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in
+   let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in
    let arg i n = T.mk_arel (n - i) (name 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)
    in
-   let absts, args = aux 0 id [] in
+   let absts, args = aux 0 identity [] in
    match Cn.lift 1 n t with
       | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
       | t                -> absts (C.AAppl ("", t :: args))  
@@ -203,9 +218,14 @@ try
 with Invalid_argument _ -> failwith "A2P.mk_intros"
 
 let rec mk_atomic st dtext what =
-   if T.is_atomic what then [], what else
-   let name = defined_premise in
-   mk_fwd_proof st dtext name what, T.mk_arel 0 name
+   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
 
 and mk_fwd_rewrite st dtext name tl direction =
    let what, where = List.nth tl 5, List.nth tl 3 in
@@ -215,7 +235,9 @@ and mk_fwd_rewrite st dtext name tl direction =
    in
    match where with
       | C.ARel (_, _, _, binder) -> rewrite binder
-      | _                        -> 
+      | _                        -> assert false
+
+(*      
         assert (get_inner_sort st where = `Prop);
         let pred, old = List.nth tl 2, List.nth tl 1 in
         let pred_name = defined_premise in
@@ -227,11 +249,11 @@ and mk_fwd_rewrite st dtext name tl direction =
          let p2 = T.Cut (cut_name, cut_type, cut_text) in
          let qs = [rewrite cut_name; mk_proof (next st) where] in 
          [T.Branch (qs, ""); p2; p1] 
-
+*)
 and mk_fwd_proof st dtext name = function
    | 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
+      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, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
       begin match get_inner_types st v with
          | Some (ity, _) when M.bkd st.context ty ->
@@ -240,7 +262,7 @@ and mk_fwd_proof st dtext name = function
          | _                                      ->
             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)]
+           [T.LetIn (name, v, dtext ^ text)]
       end
    | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
       begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
@@ -284,13 +306,14 @@ 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 decurry = List.length classes - List.length tl in
+         let premises, _ = Cl.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
         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 ->
+            | Some (i, j) when i > 1 && i <= List.length classes && M.is_eliminator premises ->
               let classes, tl, _, what = split2_last classes tl in
               let script, what = mk_atomic st dtext what in
               let synth = I.S.add 1 synth in
@@ -316,11 +339,11 @@ and mk_proof st = function
       mk_intros st script
    | C.AMutCase (id, uri, tyno, outty, arg, cases) ->
       begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
-         | None   -> 
+         | _ (* 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
+(*         | Some t -> mk_proof st t *)
       end
    | t                                             ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in