housekeeping:

[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 071377c63f0a90eb5665c85ce80043e9032557e0..b65d131e6a158f8af5d0ccfd495f1e2d96bb40b2 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -176,7 +176,7 @@ let get_type msg st t = H.get_type msg st.context (H.cic t)
 
 (* 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
@@ -221,18 +221,6 @@ let convert st ?name v =
       | None            -> 
          if !debug then [T.Note "NORMAL: NO INNER TYPES"] else []
       | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
-
-let convert_elim st ?name t v pattern =
-   match t, get_inner_types st t, get_inner_types st v with
-      | _, None, _
-      | _, _, None                                            -> [(* T.Note "ELIM: NO INNER TYPES"*)]
-      | C.AAppl (_, hd :: tl), Some (tsty, _), Some (vsty, _) ->
-         let where = List.hd (List.rev tl) in
-         let cty = Cn.elim_inferred_type 
-            st.context (H.cic vsty) (H.cic where) (H.cic hd) (H.cic pattern)
-        in
-         mk_convert st ?name (Cn.fake_annotate "" st.context cty) tsty "ELIM"
-      | _, Some _, Some _                                     -> assert false
          
 let get_intro = function 
    | C.Anonymous -> None
@@ -256,10 +244,9 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
    if (Cn.does_not_occur e) then st, [] else 
    match where with
       | C.ARel (_, _, i, premise) as w ->
-(*         let _script = convert_elim st ~name:(premise, i) v w e in *) 
          let script name =
             let where = Some (premise, name) in
-           let script = mk_arg st what @ mk_arg st w (* @ script *) in
+           let script = mk_arg st what @ mk_arg st w in
            T.Rewrite (direction, what, where, e, dtext) :: script
         in
         if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
@@ -269,7 +256,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
@@ -279,8 +266,7 @@ let mk_rewrite st dtext where qs tl direction t =
    let predicate = List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
    let script = [T.Branch (qs, "")] in
-   if (Cn.does_not_occur e) then script else 
-(*   let script = convert_elim st t t e in *)
+   if (Cn.does_not_occur e) then script else
    T.Rewrite (direction, where, None, e, dtext) :: script
 
 let rec proc_lambda st what name v t =
@@ -382,7 +368,7 @@ and proc_appl st what hd tl =
               let predicate = List.nth tl2 (parsno - i) in
                let e = Cn.mk_pattern j predicate in
               let using = Some hd in
-              (* convert_elim st what what e @ *) script2 @ 
+              script2 @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
         | None        ->
            let names = get_sub_names hd tl in
@@ -461,13 +447,15 @@ let get_flavour ?flavour attrs =
       | Some fl -> fl
       | None    -> aux attrs
 
-let proc_obj ?flavour st = function
+let proc_obj ?flavour ?(info="") st = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
       begin match get_flavour ?flavour attrs with
          | 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 "tactics: %u\nnodes: %u" steps nodes in
+            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 ->
             [T.Statement (flavour, Some s, t, Some v, "")]
@@ -483,8 +471,8 @@ let proc_obj ?flavour st = function
 
 (* interface functions ******************************************************)
 
-let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-   ?flavour prefix anobj = 
+let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types 
+   ?info ?depth ?flavour prefix anobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
@@ -495,7 +483,7 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
    } in
    L.time_stamp "P : LEVEL 2  ";
    HLog.debug "Procedural: level 2 transformation";
-   let steps = proc_obj st ?flavour anobj in
+   let steps = proc_obj st ?flavour ?info anobj in
    L.time_stamp "P : RENDERING";
    HLog.debug "Procedural: grafite rendering";
    let r = List.rev (T.render_steps [] steps) in