better metavariable context

[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 298259cb56a7a9d45ce803c767534581a928f391..c95e815daad5e4755f77f026f6df0c35ea6be0c1 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -47,17 +47,13 @@ module H    = ProceduralHelpers
 type status = {
    sorts : (C.id, A.sort_kind) Hashtbl.t;
    types : (C.id, A.anntypes) Hashtbl.t;
-   prefix: string;
    max_depth: int option;
    depth: int;
    context: C.context;
-   clears: string list;
-   clears_note: string;
-   case: int list;
-   skip_thm_and_qed : bool;
+   case: int list
 }
 
-let debug = true
+let debug = false
 
 (* helpers ******************************************************************)
 
@@ -173,6 +169,23 @@ try
       | (_, _, _, cs) -> List.map fst cs  
 with Invalid_argument _ -> failwith "A2P.get_ind_names"
 
+let string_of_atomic = function
+   | C.ARel (_, _, _, s)               -> s
+   | C.AVar (_, uri, _)                -> H.name_of_uri uri None None
+   | C.AConst (_, uri, _)              -> H.name_of_uri uri None None
+   | C.AMutInd (_, uri, i, _)          -> H.name_of_uri uri (Some i) None
+   | C.AMutConstruct (_, uri, i, j, _) -> H.name_of_uri uri (Some i) (Some j)
+   | _                                 -> ""
+
+let get_sub_names head l =
+   let s = string_of_atomic head in
+   if s = "" then [] else
+   let map (names, i) _ = 
+      let name = Printf.sprintf "%s_%u" s i in name :: names, succ i
+   in
+   let names, _ = List.fold_left map ([], 1) l in 
+   List.rev names
+
 (* proof construction *******************************************************)
 
 let anonymous_premise = C.Name "PREMISE"
@@ -238,10 +251,7 @@ let get_intro = function
    | C.Name s    -> Some s
 
 let mk_preamble st what script =
-   let clears st script =
-      if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script
-   in
-   clears st (convert st what @ script)   
+   convert st what @ script   
 
 let mk_arg st = function
    | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
@@ -384,7 +394,8 @@ and proc_appl st what hd tl =
               (* convert_elim st what what e @ *) script2 @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
         | None        ->
-           let qs = proc_bkd_proofs (next st) synth [] classes tl in
+           let names = get_sub_names hd tl in
+           let qs = proc_bkd_proofs (next st) synth names classes tl in
            let hd = mk_exp_args hd tl classes synth in
            script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
    else
@@ -406,9 +417,8 @@ and proc_proof st t =
          (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) 
          | None          -> None, "\nNo types"
       in
-      let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
-      let note = Pp.ppcontext st.context ^ note in
-      {st with context = context; clears = clears; clears_note = note; }
+      let context, _clears = Cn.get_clears st.context (H.cic t) xtypes in
+      {st with context = context}
    in
    match t with
       | C.ALambda (_, name, w, t) as what   -> proc_lambda (f st) what name w t
@@ -436,7 +446,7 @@ try
    let aux (inv, _) v =
       if I.overlaps synth inv then None else
       if I.S.is_empty inv then Some (get_note (fun st -> proc_proof st v)) else
-      Some (fun _ -> [T.Apply (v, dtext ^ "dependent")])
+      Some (get_note (fun _ -> [T.Apply (v, dtext ^ "dependent")]))
    in  
    let ps = T.list_map2_filter aux classes ts in
    let b = List.length ps > 1 in
@@ -459,8 +469,7 @@ let proc_obj st = function
       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
-      if st.skip_thm_and_qed then ast
-      else T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text]
+      T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text]
    | C.AConstant (_, _, s, Some v, t, [], pars) when is_definition pars ->
       [T.Statement (`Definition, Some s, t, Some v, "")]
    | C.AConstant (_, _, s, None, t, [], pars)                           ->
@@ -470,21 +479,32 @@ let proc_obj st = function
 
 (* interface functions ******************************************************)
 
-let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-?(skip_thm_and_qed=false) prefix aobj = 
+let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
+   prefix anobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
-      prefix      = prefix;
       max_depth   = depth;
       depth       = 0;
       context     = [];
-      clears      = [];
-      clears_note = "";
-      case        = [];
-      skip_thm_and_qed = skip_thm_and_qed;
+      case        = []
+   } in
+   HLog.debug "Procedural: level 2 transformation";
+   let steps = proc_obj st anobj in
+   HLog.debug "Procedural: grafite rendering";
+   List.rev (T.render_steps [] steps)
+
+let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
+   prefix context annterm = 
+   let st = {
+      sorts       = ids_to_inner_sorts;
+      types       = ids_to_inner_types;
+      max_depth   = depth;
+      depth       = 0;
+      context     = context;
+      case        = []
    } in
    HLog.debug "Procedural: level 2 transformation";
-   let steps = proc_obj st aobj in
+   let steps = proc_proof st annterm in
    HLog.debug "Procedural: grafite rendering";
    List.rev (T.render_steps [] steps)