X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=42214b57bc4861f979ddac93f83569e09dbb437c;hb=1f974ca07c502d85c9a3760aaaf633bae3c84fb6;hp=b1cbc74abdacec4633ff828efcb1a71999355da7;hpb=977e819edc19f6c25d9f05c2fafe72c63ad301fd;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index b1cbc74ab..42214b57b 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -24,6 +24,7 @@
  *)
 
 module C    = Cic
+module I    = CicInspect
 module D    = Deannotate
 module DTI  = DoubleTypeInference
 module TC   = CicTypeChecker 
@@ -228,7 +229,7 @@ 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
@@ -241,11 +242,16 @@ 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
-   | 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
@@ -253,7 +259,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
@@ -264,16 +270,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
@@ -281,13 +287,13 @@ and mk_proof st = function
          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 = Cl.S.singleton 0 in
+	 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 ->
 	       let classes, tl, _, what = split2_last classes tl in
 	       let script, what = mk_atomic st dtext what in
-	       let synth = Cl.S.add 1 synth 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 
 	          List.rev script @ convert st t @
@@ -308,7 +314,15 @@ and mk_proof st = function
          [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
@@ -317,8 +331,8 @@ and mk_bkd_proofs st synth classes ts =
 try 
    let _, dtext = test_depth st in   
    let aux inv v =
-      if Cl.overlaps synth inv then None else
-      if Cl.S.is_empty inv then Some (mk_proof st v) else
+      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")]
    in
    T.list_map2_filter aux classes ts