]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/acic2Procedural.ml
Procedural: bug fix in comment generation
[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml
index 8e99a93322fa6075ca339ce36b63f2a439612592..380e52efec280ca40f308a92b5e0bcafd00c2998 100644 (file)
@@ -38,6 +38,7 @@ module Pp   = CicPp
 module PEH  = ProofEngineHelpers
 module HEL  = HExtlib
 module DTI  = DoubleTypeInference
+module NU   = CicNotationUtil
 
 module Cl   = ProceduralClassify
 module T    = ProceduralTypes
@@ -47,17 +48,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 ******************************************************************)
 
@@ -95,7 +92,7 @@ let push st = {st with case = 1 :: st.case}
 
 let inc st =
    {st with case = match st.case with 
-      | []       -> assert false
+      | []       -> []
       | hd :: tl -> succ hd :: tl
    }
 
@@ -173,9 +170,26 @@ 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 used_premise = C.Name "USED"
+let anonymous_premise = C.Name "PREMISE"
 
 let mk_exp_args hd tl classes synth =
    let meta id = C.AImplicit (id, None) in
@@ -202,8 +216,8 @@ let mk_convert st ?name sty ety note =
         [T.Note note]
       else []
    in
-   assert (Ut.is_sober csty); 
-   assert (Ut.is_sober cety);
+   assert (Ut.is_sober st.context csty); 
+   assert (Ut.is_sober st.context cety);
    if Ut.alpha_equivalence csty cety then script else 
    let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
    match name with
@@ -238,10 +252,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
@@ -266,11 +277,14 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
         in
         if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
            {st with context = Cn.clear st.context premise}, script name
-        else
+        else begin
+           assert (Ut.is_sober st.context (H.cic 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
            st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]
+        end
       | _                         -> assert false
 
 let mk_rewrite st dtext where qs tl direction t = 
@@ -283,17 +297,9 @@ let mk_rewrite st dtext where qs tl direction t =
    T.Rewrite (direction, where, None, e, dtext) :: script
 
 let rec proc_lambda st what name v t =
-   let dno = match get_inner_types st t with
-      | None            -> false
-      | Some (sty, ety) ->
-         let sty, ety = H.cic sty, H.cic ety in
-         DTI.does_not_occur 1 sty && DTI.does_not_occur 1 ety
-   in
-   let dno = dno && DTI.does_not_occur 1 (H.cic t) in
-   let name = match dno, name with
-      | true, _            -> C.Anonymous
-      | false, C.Anonymous -> H.mk_fresh_name st.context used_premise
-      | false, name        -> name
+   let name = match name with
+      | C.Anonymous -> H.mk_fresh_name st.context anonymous_premise
+      | name        -> name
    in
    let entry = Some (name, C.Decl (H.cic v)) in
    let intro = get_intro name in
@@ -313,8 +319,9 @@ and proc_letin st what name v w t =
               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
                  mk_fwd_rewrite st dtext intro tl false v t ity
               | v                                                     ->
+                 assert (Ut.is_sober st.context (H.cic ity));
+                 let ity = H.acic_bc st.context ity in
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
-                 let ity = H.acic_bc st.context ity in
                  st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
            st, C.Decl (H.cic ity), rqv
@@ -388,7 +395,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
@@ -397,8 +405,9 @@ and proc_appl st what hd tl =
    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
-   let script = [T.Note text] in
+   let script = [T.Apply (what, dtext ^ text)] in 
    mk_preamble st what script
 
 and proc_proof st t = 
@@ -409,9 +418,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
@@ -424,63 +432,93 @@ and proc_proof st t =
 
 and proc_bkd_proofs st synth names classes ts =
 try 
-   let get_note =
-      let names = ref (names, push st) in
-      fun f -> 
-         match !names with 
-           | [], st       -> fun _ -> f st
-           | "" :: tl, st -> names := tl, st; fun _ -> f st
-           | hd :: tl, st -> 
-              let note = case st hd in
-              names := tl, inc st; 
-              fun b -> if b then T.Note note :: f st else f st
+   let get_names b = ref (names, if b then push st else st) in
+   let get_note f b names = 
+      match !names with 
+         | [], st       -> f st
+        | "" :: tl, st -> names := tl, st; f st
+        | hd :: tl, st -> 
+           let note = case st hd in
+           names := tl, inc st; 
+           if b then T.Note note :: f st else f st
    in
    let _, dtext = test_depth st in   
    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
-   List.rev_map (fun f -> f b) ps
+   let names = get_names b in
+   List.rev_map (fun f -> f b names) ps
 
 with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 (* object costruction *******************************************************)
 
-let is_theorem pars =
-   pars = [] ||
-   List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
-   List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
-
-let proc_obj st = function
-   | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
-      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.Theorem (Some s, t, "") :: ast @ [T.Qed text]
-   | _                                                               ->
-      failwith "not a theorem"
+let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
+
+let def_flavours = [`Definition]
+
+let get_flavour ?flavour attrs =
+   let rec aux = function
+      | []               -> List.hd th_flavours
+      | `Flavour fl :: _ -> fl
+      | _ :: tl          -> aux tl
+   in
+   match flavour with
+      | Some fl -> fl
+      | None    -> aux attrs
+
+let proc_obj ?flavour 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
+            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, "")]
+        | _                                  ->
+            failwith "not a theorem, definition, axiom or inductive type"
+      end
+   | C.AConstant (_, _, s, None, t, [], attrs)           ->
+      [T.Statement (`Axiom, Some s, t, None, "")]
+   | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
+      [T.Inductive (types, lpsno, "")] 
+   | _                                          ->
+      failwith "not a theorem, definition, axiom or inductive type"
 
 (* 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
+   ?flavour 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 ?flavour 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)