cicInspect: now we can choose not to count the Cic.Implicit constructors

[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 c9a3232484b30b60378dfc0da9b49bdd18996466..0edb5c8b041c9e2c5415790bd3a1badfca2ead20 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -45,6 +45,7 @@ module Cl   = ProceduralClassify
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
 module H    = ProceduralHelpers
+module X    = ProceduralTeX
 
 type status = {
    sorts : (C.id, A.sort_kind) Hashtbl.t;
@@ -55,6 +56,8 @@ type status = {
    case: int list
 }
 
+let tex_formatter = ref None
+
 let debug = ref false
 
 (* helpers ******************************************************************)
@@ -174,9 +177,22 @@ let get_sub_names head l =
 
 let get_type msg st t = H.get_type msg st.context (H.cic t) 
 
+let clear_absts m =
+   let rec aux k n = function
+      | C.ALambda (id, s, v, t) when k > 0 -> 
+         C.ALambda (id, s, v, aux (pred k) n t)
+      | C.ALambda (_, _, _, t) when n > 0 -> 
+         aux 0 (pred n) (Cn.lift 1 (-1) t)
+      | t                  when n > 0 ->
+         Printf.eprintf "A2P.clear_absts: %u %s\n" n (Pp.ppterm (H.cic t));
+         assert false
+      | t                             -> t
+   in 
+   aux m
+
 (* proof construction *******************************************************)
 
-let anonymous_premise = C.Name "PREMISE"
+let anonymous_premise = C.Name "UNNAMED"
 
 let mk_exp_args hd tl classes synth =
    let meta id = C.AImplicit (id, None) in
@@ -256,7 +272,7 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
            let ity = H.acic_bc st.context ity in
            let br1 = [T.Id ""] in
            let br2 = List.rev (T.Apply (w, "assumption") :: script None) in
-           let text = "non linear rewrite" in
+           let text = "non-linear rewrite" in
            st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]
         end
       | _                         -> assert false
@@ -380,6 +396,26 @@ and proc_appl st what hd tl =
    in
    mk_preamble st what script
 
+and proc_case st what uri tyno u v ts =
+   let proceed, dtext = test_depth st in
+   let script = if proceed then
+      let synth, classes = I.S.empty, Cl.make ts in
+      let names = H.get_ind_names uri tyno in
+      let qs = proc_bkd_proofs (next st) synth names classes ts in
+      let lpsno, _ = H.get_ind_type uri tyno in
+      let ps, sort_disp = H.get_ind_parameters st.context (H.cic v) in
+      let _, rps = HEL.split_nth lpsno ps in
+      let rpsno = List.length rps in   
+      let predicate = clear_absts rpsno (1 - sort_disp) u in
+      let e = Cn.mk_pattern rpsno predicate in
+      let text = "" in
+      let script = List.rev (mk_arg st v) in
+      script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")]   
+   else
+      [T.Apply (what, dtext)]
+   in
+   mk_preamble st what script
+
 and proc_other st what =
    let _, dtext = test_depth st in
    let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
@@ -398,13 +434,14 @@ and proc_proof st t =
       {st with context = context}
    in
    match t with
-      | C.ALambda (_, name, w, t) as what   -> proc_lambda (f st) what name w t
-      | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
-      | C.ARel _ as what                    -> proc_rel (f st) what
-      | C.AMutConstruct _ as what           -> proc_mutconstruct (f st) what
-      | C.AConst _ as what                  -> proc_const (f st) what
-      | C.AAppl (_, hd :: tl) as what       -> proc_appl (f st) what hd tl
-      | what                                -> proc_other (f st) what
+      | C.ALambda (_, name, w, t) as what        -> proc_lambda (f st) what name w t
+      | C.ALetIn (_, name, v, w, t) as what      -> proc_letin (f st) what name v w t
+      | C.ARel _ as what                         -> proc_rel (f st) what
+      | C.AMutConstruct _ as what                -> proc_mutconstruct (f st) what
+      | C.AConst _ as what                       -> proc_const (f st) what
+      | C.AAppl (_, hd :: tl) as what            -> proc_appl (f st) what hd tl
+      | C.AMutCase (_, uri, i, u, v, ts) as what -> proc_case (f st) what uri i u v ts
+      | what                                     -> proc_other (f st) what
 
 and proc_bkd_proofs st synth names classes ts =
 try 
@@ -453,8 +490,8 @@ let proc_obj ?flavour ?(info="") st = function
          | flavour when List.mem flavour th_flavours  ->
             let ast = proc_proof st v in
             let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
-            let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n"
-              "COMMENTS" info "tactics" steps "nodes" nodes
+            let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+              "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
            in
             T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
          | flavour when List.mem flavour def_flavours ->
@@ -481,9 +518,13 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
       context     = [];
       case        = []
    } in
-   L.time_stamp "P : LEVEL 2  ";
-   HLog.debug "Procedural: level 2 transformation";
+   L.time_stamp "P : LEVEL 1  ";
+   HLog.debug "Procedural: level 1 transformation";
    let steps = proc_obj st ?flavour ?info anobj in
+   let _ = match !tex_formatter with
+      | None     -> ()
+      | Some frm -> X.tex_of_steps frm st.sorts steps
+   in
    L.time_stamp "P : RENDERING";
    HLog.debug "Procedural: grafite rendering";
    let r = List.rev (T.render_steps [] steps) in
@@ -499,7 +540,11 @@ let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
       context     = context;
       case        = []
    } in
-   HLog.debug "Procedural: level 2 transformation";
+   HLog.debug "Procedural: level 1 transformation";
    let steps = proc_proof st annterm in
+   let _ = match !tex_formatter with
+      | None     -> ()
+      | Some frm -> X.tex_of_steps frm st.sorts steps
+   in
    HLog.debug "Procedural: grafite rendering";
    List.rev (T.render_steps [] steps)