X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=dbdfb979209b146c32ee303f89dbe1f599adb096;hb=8ae990161006978a019f0afda4ff8d56a78d1fd0;hp=8dd8e02aa44051b121511de0806b200b7af6cc65;hpb=f505d9e257aa3209652264b97bb62d87ce592091;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 8dd8e02aa..dbdfb9792 100644
--- 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
@@ -54,10 +55,6 @@ type status = {
 
 (* helpers ******************************************************************)
 
-let identity x = x
-
-let comp f g x = f (g x)
-
 let cic = D.deannotate_term
 
 let split2_last l1 l2 =
@@ -153,43 +150,28 @@ try
    with Not_found -> `Type (CicUniv.fresh())
 with Invalid_argument _ -> failwith "A2P.get_sort"
 
+let get_type msg st bo =
+try   
+   let ty, _ = TC.type_of_aux' [] st.context (cic bo) Un.empty_ugraph in
+   ty
+with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
+
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
 
 let defined_premise = "DEFINED"
 
-let expanded_premise = "EXPANDED"
-
 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 
+	 let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
 	 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 (id, C.Name (name i), ty, t) in
-   let arg i n = T.mk_arel (n - i) (name (n - i - 1)) 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 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))  
-
-let appl_expand n = function
-   | C.AAppl (id, ts) -> 
-      let before, after = T.list_split (List.length ts + n) ts in
-      C.AAppl ("", C.AAppl (id, before) :: after)
-   | _                -> assert false
+	    | 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
@@ -216,19 +198,34 @@ let rec mk_atomic st dtext what =
       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
+and mk_fwd_rewrite st dtext name tl direction =   
+   assert (List.length tl = 6);
+   let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
+   let e = Cn.mk_pattern 1 predicate in
    match where with
       | C.ARel (_, _, _, premise) ->
          let script, what = mk_atomic st dtext what in
-         T.Rewrite (direction, what, Some (premise, name), dtext) :: script
+         T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script
       | _                         -> assert false
 
+and mk_rewrite st dtext script t what qs tl direction = 
+   assert (List.length tl = 5);
+   let predicate = List.nth tl 2 in
+   let e = Cn.mk_pattern 1 predicate in
+   List.rev script @ convert st t @
+   [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
+
 and mk_fwd_proof st dtext name = function
-   | C.AAppl (_, hd :: tl) as v                         -> 
+   | 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, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+      let ty = get_type "TC1" st hd in
       begin match get_inner_types st v with
          | Some (ity, _) when M.bkd st.context ty ->
 	    let qs = [[T.Id ""]; mk_proof (next st) v] in
@@ -238,20 +235,22 @@ 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 ->
-      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)]
+   | C.AMutCase _               -> assert false
+   | C.ACast _                  -> assert false 
+   | v                          ->
+      match get_inner_types st v with
+         | Some (ity, _) ->
+	    let qs = [[T.Id ""]; mk_proof (next st) v] in
+	    [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
+         | _             ->
+            [T.LetIn (name, v, dtext)]
 
 and mk_proof st = function
-   | C.ALambda (_, name, v, t)                     ->
+   | C.ALambda (_, name, v, t)        ->
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
       mk_proof (add st entry intro) 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
@@ -262,24 +261,22 @@ 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
+         let ty = get_type "TC2" st hd in
          let (classes, rc) as h = Cl.classify st.context ty 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 premises, _ = P.split st.context ty in
+	 assert (List.length classes - List.length tl = 0);
 	 let synth = I.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
          match rc with
@@ -289,15 +286,16 @@ and mk_proof st = function
 	       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 
-	          List.rev script @ convert st t @
-		  [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
+	          mk_rewrite st dtext script t what qs tl false
 	       else if is_rewrite_left hd then 
-	          List.rev script @ convert st t @
-		  [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
+	          mk_rewrite st dtext script t what qs tl true
 	       else   
-	          let using = Some hd in
+                  let l = succ (List.length tl) in
+		  let predicate = List.nth tl (l - i) in
+                  let e = Cn.mk_pattern j predicate in
+		  let using = Some hd in
 		  List.rev script @ convert st t @
-	          [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
+	          [T.Elim (what, using, e, 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               
@@ -307,15 +305,9 @@ and mk_proof st = function
          [T.Apply (t, dtext)]
       in
       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 *)  -> 
-            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                                             ->
+   | C.AMutCase _                     -> assert false
+   | C.ACast _                        -> assert false
+   | t                                ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in
       mk_intros st script