attributes now in the proof status: commit 4

[helm.git] / helm / software / components / content_pres / acic2Procedural.ml

diff --git a/helm/software/components/content_pres/acic2Procedural.ml b/helm/software/components/content_pres/acic2Procedural.ml
index f568ac7c564bb9d5b21dc30f1405afa06c1a1839..18ded2e7969579acd0fb94707f00a6ce1afc8278 100644 (file)
--- a/helm/software/components/content_pres/acic2Procedural.ml
+++ b/helm/software/components/content_pres/acic2Procedural.ml
@@ -37,7 +37,7 @@ module A    = Cic2acic
 module T    = CicUtil
 
 type status = {
-   sorts : (Cic.id, Cic2acic.sort_kind) Hashtbl.t;
+   sorts : (C.id, Cic2acic.sort_kind) Hashtbl.t;
    types : (C.id, A.anntypes) Hashtbl.t;
    prefix: string;
    max_depth: int option;
@@ -51,10 +51,12 @@ type status = {
 let cic = D.deannotate_term
 
 let split2_last l1 l2 =
+try
    let n = pred (List.length l1) in
    let before1, after1 = P.list_split n l1 in
    let before2, after2 = P.list_split n l2 in
    before1, before2, List.hd after1, List.hd after2
+with Invalid_argument _ -> failwith "A2P.split2_last"
 
 let string_of_head = function
    | C.ASort _         -> "sort"
@@ -80,30 +82,39 @@ let add st entry intro =
    {st with entries = entry :: st.entries; intros = intro :: st.intros}
 
 let test_depth st =
+try   
    let msg = Printf.sprintf "Depth %u: " st.depth in
    match st.max_depth with
       | None   -> true, "" 
       | Some d -> 
          if st.depth < d then true, msg else false, "DEPTH EXCEDED"
+with Invalid_argument _ -> failwith "A2P.test_depth"
 
 let get_itype st v =
+try
    let id = T.id_of_annterm v in
    try Some ((Hashtbl.find st.types id).A.annsynthesized)
    with Not_found -> None
+with Invalid_argument _ -> failwith "A2P.get_itype"
 
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
 
-let get_intro name t = match name with 
+let get_intro name t = 
+try
+match name with 
    | C.Anonymous -> unused_premise
    | C.Name s    -> 
       if DTI.does_not_occur 1 (cic t) then unused_premise else s
+with Invalid_argument _ -> failwith "A2P.get_intro"
 
 let mk_intros st script =
+try
    if st.intros = [] then script else
    let count = List.length st.intros in
    P.Intros (Some count, List.rev st.intros, "") :: script
+with Invalid_argument _ -> failwith "A2P.mk_intros"
 
 let is_rewrite_right = function
    | C.AConst (_, uri, []) ->
@@ -117,7 +128,12 @@ let is_rewrite_left = function
 
 let mk_premise = function
    | C.ARel (_, _, _, binder) -> binder
-   | _                        -> assert false
+   | C.AVar (_, uri, _)
+   | C.AConst (_, uri, _)                  -> UM.name_of_uri uri
+   | C.ASort (_, sort)                     -> assert false
+   | C.AMutInd (_, uri, tno, _)            -> assert false
+   | C.AMutConstruct (_, uri, tno, cno, _) -> assert false
+   | _                                     -> assert false
 
 let rec mk_fwd_proof st dtext name = function
    | C.AAppl (_, hd :: tl) as v -> 
@@ -150,8 +166,9 @@ and mk_proof st = function
    | 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
          let intro = get_intro name t in
-         let q = mk_proof (next st) t in
+         let q = mk_proof (next (add st entry intro)) t in
          List.rev_append (mk_fwd_proof st dtext intro v) q
       else
         [P.Apply (what, dtext)]
@@ -193,23 +210,33 @@ and mk_proof st = function
       mk_intros st script
 
 and mk_bkd_proofs st synth classes ts =
+try 
    let _, dtext = test_depth st in   
    let aux inv v =
       if L.overlaps synth inv then None else
       if L.S.is_empty inv then Some (mk_proof st v) else
       Some [P.Apply (v, dtext ^ "dependent")]
    in
+   let l1, l2 = List.length classes, List.length ts in
+   if l1 > l2 then failwith "partial application" else
+   if l1 < l2 then failwith "too many arguments" else
    P.list_map2_filter aux classes ts
+with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
 
 (* object costruction *******************************************************)
 
+let is_theorem pars =   
+   List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
+   List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
+
 let mk_obj st = function
-   | C.AConstant (_, _, s, Some v, t, [], _) ->
+   | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
       let ast = mk_proof st v in
       let count = P.count_steps 0 ast in
       let text = Printf.sprintf "tactics: %u" count in
       P.Theorem (s, t, text) :: ast @ [P.Qed ""]
-   | _                                       -> assert false
+   | _                                                               ->
+      [P.Note "not a theorem"]
 
 (* interface functions ******************************************************)