]> matita.cs.unibo.it Git - helm.git/commitdiff
Cic2acic : added some debugging information
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 2 Apr 2007 12:09:35 +0000 (12:09 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 2 Apr 2007 12:09:35 +0000 (12:09 +0000)
Procedural: some refactoring and improvements

helm/software/components/acic_procedural/.depend
helm/software/components/acic_procedural/.depend.opt
helm/software/components/acic_procedural/Makefile
helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralClassify.ml
helm/software/components/acic_procedural/proceduralHelpers.ml [new file with mode: 0644]
helm/software/components/acic_procedural/proceduralHelpers.mli [new file with mode: 0644]
helm/software/components/acic_procedural/proceduralPreprocess.ml
helm/software/components/cic_acic/cic2acic.ml
helm/software/components/cic_acic/cic2acic.mli

index c1c6561c2e348270548de73450a92b54550bd84f..02ce90009e6407f3ad027921cb1c03ce8cc0da8c 100644 (file)
@@ -1,7 +1,11 @@
-proceduralClassify.cmo: proceduralClassify.cmi 
-proceduralClassify.cmx: proceduralClassify.cmi 
-proceduralPreprocess.cmo: proceduralClassify.cmi proceduralPreprocess.cmi 
-proceduralPreprocess.cmx: proceduralClassify.cmx proceduralPreprocess.cmi 
+proceduralHelpers.cmo: proceduralHelpers.cmi 
+proceduralHelpers.cmx: proceduralHelpers.cmi 
+proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi 
+proceduralClassify.cmx: proceduralHelpers.cmx proceduralClassify.cmi 
+proceduralPreprocess.cmo: proceduralHelpers.cmi proceduralClassify.cmi \
+    proceduralPreprocess.cmi 
+proceduralPreprocess.cmx: proceduralHelpers.cmx proceduralClassify.cmx \
+    proceduralPreprocess.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
 proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
@@ -10,7 +14,7 @@ proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
     proceduralMode.cmi proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
     proceduralMode.cmx proceduralConversion.cmi 
-acic2Procedural.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
-    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
-acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
-    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
+acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
+    proceduralClassify.cmi acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
+    proceduralClassify.cmx acic2Procedural.cmi 
index c1c6561c2e348270548de73450a92b54550bd84f..02ce90009e6407f3ad027921cb1c03ce8cc0da8c 100644 (file)
@@ -1,7 +1,11 @@
-proceduralClassify.cmo: proceduralClassify.cmi 
-proceduralClassify.cmx: proceduralClassify.cmi 
-proceduralPreprocess.cmo: proceduralClassify.cmi proceduralPreprocess.cmi 
-proceduralPreprocess.cmx: proceduralClassify.cmx proceduralPreprocess.cmi 
+proceduralHelpers.cmo: proceduralHelpers.cmi 
+proceduralHelpers.cmx: proceduralHelpers.cmi 
+proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi 
+proceduralClassify.cmx: proceduralHelpers.cmx proceduralClassify.cmi 
+proceduralPreprocess.cmo: proceduralHelpers.cmi proceduralClassify.cmi \
+    proceduralPreprocess.cmi 
+proceduralPreprocess.cmx: proceduralHelpers.cmx proceduralClassify.cmx \
+    proceduralPreprocess.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
 proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
@@ -10,7 +14,7 @@ proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
     proceduralMode.cmi proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
     proceduralMode.cmx proceduralConversion.cmi 
-acic2Procedural.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
-    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
-acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
-    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
+acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
+    proceduralClassify.cmi acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
+    proceduralClassify.cmx acic2Procedural.cmi 
index 780462786136d3b9a909e020cba1097882737829..78d3e3b09e86609a81fdd169b0b93b279ffba3b9 100644 (file)
@@ -2,6 +2,7 @@ PACKAGE = acic_procedural
 PREDICATES =
 
 INTERFACE_FILES =               \
+       proceduralHelpers.mli    \
        proceduralClassify.mli   \
        proceduralPreprocess.mli \
        proceduralTypes.mli      \
index 3cf4bb596b38a4cd36c20262bc28b2ce67fc6929..7fd8290ba224783c9856a4cb84a1e2576749c90e 100644 (file)
@@ -26,7 +26,6 @@
 module C    = Cic
 module I    = CicInspect
 module D    = Deannotate
-module DTI  = DoubleTypeInference
 module TC   = CicTypeChecker 
 module Un   = CicUniv
 module UM   = UriManager
@@ -39,7 +38,6 @@ module PEH  = ProofEngineHelpers
 module PER  = ProofEngineReduction
 module Pp   = CicPp
 
-module P    = ProceduralPreprocess
 module Cl   = ProceduralClassify
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
@@ -143,14 +141,14 @@ try
       | {A.annsynthesized = st; A.annexpected = None}    -> Some (st, st)
    with Not_found -> None
 with Invalid_argument _ -> failwith "A2P.get_inner_types"
-
+(*
 let get_inner_sort st v =
 try
    let id = Ut.id_of_annterm v in
    try Hashtbl.find st.sorts id
    with Not_found -> `Type (CicUniv.fresh())
 with Invalid_argument _ -> failwith "A2P.get_sort"
-
+*)
 let get_type msg st bo =
 try   
    let ty, _ = TC.type_of_aux' [] st.context (cic bo) Un.empty_ugraph in
@@ -177,139 +175,133 @@ let get_intro = function
    | C.Name s    -> s
 
 let mk_intros st script =
-try
    if st.intros = [] then script else
    let count = List.length st.intros in
    T.Intros (Some count, List.rev st.intros, "") :: script
-with Invalid_argument _ -> failwith "A2P.mk_intros"
 
-let rec mk_arg st = function
-   | C.ARel (_, _, _, name) as what -> convert st ~name what, what
-   | what                           -> [], what
+let mk_arg st = function
+   | C.ARel (_, _, _, name) as what -> convert st ~name what
+   | _                              -> []
 
-and mk_fwd_rewrite st dtext name tl direction =   
+let mk_fwd_rewrite st dtext name tl direction =   
    assert (List.length tl = 6);
    let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
    match where with
       | C.ARel (_, _, _, premise) ->
-         let script, what = mk_arg st what in
-         T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script
+         let script = mk_arg st what in
+         let where = Some (premise, name) in
+        T.Rewrite (direction, what, where, e, dtext) :: script
       | _                         -> assert false
 
-and mk_rewrite st dtext script t what qs tl direction = 
+let mk_rewrite st dtext what qs tl direction = 
    assert (List.length tl = 5);
    let predicate = List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
-   List.rev script @ convert st t @
    [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
 
-and mk_fwd_proof st dtext name = function
-   | C.AAppl (_, hd :: tl) as v -> 
-      if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
-      if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else
-      let ty = get_type "TC1" st hd in
-      begin match get_inner_types st v with
-         | Some (ity, _) ->
-           let qs = [[T.Id ""]; mk_proof (next st) v] in
-           [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
-         | _             ->
-            let (classes, rc) as h = Cl.classify st.context ty in
-            let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
-           [T.LetIn (name, v, dtext ^ text)]
-      end
-   | C.AMutCase _               -> assert false
-   | C.ACast _                  -> assert false 
-   | v                          ->
-      match get_inner_types st v with
+let rec proc_lambda st name v t =
+   let entry = Some (name, C.Decl (cic v)) in
+   let intro = get_intro name in
+   proc_proof (add st entry intro) t
+
+and proc_letin st what name v t =
+   let intro = get_intro name in
+   let proceed, dtext = test_depth st in
+   let script = if proceed then 
+      let hyp, rqv = match get_inner_types st v with
          | Some (ity, _) ->
-           let qs = [[T.Id ""]; mk_proof (next st) v] in
-           [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
-         | _             ->
-            [T.LetIn (name, v, dtext)]
-
-and mk_proof st = function
-   | C.ALambda (_, name, v, t)        ->
-      let entry = Some (name, C.Decl (cic v)) in
-      let intro = get_intro name in
-      mk_proof (add st entry intro) t
-   | 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 in
-         let q = mk_proof (next (add st entry intro)) t in
-         List.rev_append (mk_fwd_proof st dtext intro v) q
-      else
-        [T.Apply (what, dtext)]
-      in
-      mk_intros st script
-   | C.ARel _ as what                 ->
-      let _, dtext = test_depth st in
-      let text = "assumption" in
-      let script = [T.Apply (what, dtext ^ text)] in 
-      mk_intros st script
-   | C.AMutConstruct _ as what        ->
-      let _, dtext = test_depth st in
-      let script = [T.Apply (what, dtext)] in 
-      mk_intros st script   
-   | C.AAppl (_, hd :: tl) as t       ->
-      let proceed, dtext = test_depth st in
-      let script = if proceed then
-         let ty = get_type "TC2" st hd in
-         let (classes, rc) as h = Cl.classify st.context ty in
-        let decurry = List.length classes - List.length tl in
-        if decurry <> 0 then begin
-           let msg = Printf.sprintf "Decurry: %i\nTerm: %s\nContext: %s"
-              decurry (Pp.ppterm (cic t)) (Pp.ppcontext st.context)
+           let rqv = match v with
+               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
+                 mk_fwd_rewrite st dtext intro tl true
+              | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
+                 mk_fwd_rewrite st dtext intro tl false
+              | v                                                     ->
+                 let qs = [[T.Id ""]; proc_proof (next st) v] in
+                 [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
-           HLog.warn msg; assert false
-        end;
-        let synth = I.S.singleton 0 in
-         let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
-         match rc with
-            | Some (i, j) ->
-              let classes, tl, _, what = split2_last classes tl in
-              let script, what = mk_arg st what in
-              let synth = I.S.add 1 synth in
-              let qs = mk_bkd_proofs (next st) synth classes tl in
-               if is_rewrite_right hd then 
-                 mk_rewrite st dtext script t what qs tl false
-              else if is_rewrite_left hd then 
-                 mk_rewrite st dtext script t what qs tl true
-              else   
-                  let l = succ (List.length tl) in
-                 let predicate = List.nth tl (l - i) in
-                  let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in
-                 let using = Some hd in
-                 List.rev script @ convert st t @
-                 [T.Elim (what, using, e, dtext ^ text); T.Branch (qs, "")]
-           | None        ->
-              let qs = mk_bkd_proofs (next st) synth classes tl in
-              let script, hd = mk_arg st hd in               
-              List.rev script @ convert st t @        
-              [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
-      else
-         [T.Apply (t, dtext)]
+           C.Decl (get_type "TC1" st v), rqv
+        | None          ->
+           C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
       in
-      mk_intros st script
-   | C.AMutCase _                     -> assert false
-   | C.ACast _                        -> assert false
-   | t                                ->
-      let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
-      let script = [T.Note text] in
-      mk_intros st script
-
-and mk_bkd_proofs st synth classes ts =
+      let entry = Some (name, hyp) in
+      let qt = proc_proof (next (add st entry intro)) t in
+      List.rev_append rqv qt      
+   else
+      [T.Apply (what, dtext)]
+   in
+   mk_intros st script
+
+and proc_rel st what = 
+   let _, dtext = test_depth st in
+   let text = "assumption" in
+   let script = [T.Apply (what, dtext ^ text)] in 
+   mk_intros st script
+
+and proc_mutconstruct st what = 
+   let _, dtext = test_depth st in
+   let script = [T.Apply (what, dtext)] in 
+   mk_intros st script   
+
+and proc_appl st what hd tl =
+   let proceed, dtext = test_depth st in
+   let script = if proceed then
+      let ty = get_type "TC2" st hd in
+      let (classes, rc) as h = Cl.classify st.context ty in
+      let argsno = List.length classes in
+      let diff = argsno - List.length tl in
+      if diff <> 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd)));
+      let synth = I.S.singleton 0 in
+      let text = Printf.sprintf "%u %s" argsno (Cl.to_string h) in
+      let script = List.rev (mk_arg st hd) @ convert st what in
+      match rc with
+         | Some (i, j) ->
+           let classes, tl, _, where = split2_last classes tl in
+           let script = List.rev (mk_arg st where) @ script in
+           let synth = I.S.add 1 synth in
+           let qs = proc_bkd_proofs (next st) synth classes tl in
+            if is_rewrite_right hd then 
+              script @ mk_rewrite st dtext where qs tl false
+           else if is_rewrite_left hd then 
+              script @ mk_rewrite st dtext where qs tl true
+           else
+              let predicate = List.nth tl (argsno - i) in
+               let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in
+              let using = Some hd in
+              script @
+              [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
+        | None        ->
+           let qs = proc_bkd_proofs (next st) synth classes tl in
+           script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+   else
+      [T.Apply (what, dtext)]
+   in
+   mk_intros st script
+
+and proc_other st what =
+   let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
+   let script = [T.Note text] in
+   mk_intros st script
+
+
+and proc_proof st = function
+   | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
+   | C.ALetIn (_, name, v, t) as what -> proc_letin st what name v t
+   | C.ARel _ as what                 -> proc_rel st what
+   | C.AMutConstruct _ as what        -> proc_mutconstruct st what
+   | C.AAppl (_, hd :: tl) as what    -> proc_appl st what hd tl
+   | what                             -> proc_other st what
+
+and proc_bkd_proofs st synth classes ts =
 try 
    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 (mk_proof st v) else
+      if I.S.is_empty inv then Some (proc_proof st v) else
       Some [T.Apply (v, dtext ^ "dependent")]
    in
    T.list_map2_filter aux classes ts
-with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
+with Invalid_argument _ -> failwith "A2P.proc_bkd_proofs"
 
 (* object costruction *******************************************************)
 
@@ -317,9 +309,9 @@ 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
+let proc_obj st = function
    | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
-      let ast = mk_proof st v in
+      let ast = proc_proof st v in
       let count = T.count_steps 0 ast in
       let text = Printf.sprintf "tactics: %u" count in
       T.Theorem (s, t, text) :: ast @ [T.Qed ""]
@@ -338,7 +330,7 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
       context   = [];
       intros    = []
    } in
-   HLog.debug "Level 2 transformation";
-   let steps = mk_obj st aobj in
-   HLog.debug "grafite rendering";
+   HLog.debug "Procedural: level 2 transformation";
+   let steps = proc_obj st aobj in
+   HLog.debug "Procedural: grafite rendering";
    List.rev (T.render_steps [] steps)
index 6c1e482c2ff4d86aee5ee01cb988e50ece825630..4f9f99fcee76117056a100bd8f1a13dfb9fcfd24 100644 (file)
@@ -28,6 +28,8 @@ module D   = Deannotate
 module I   = CicInspect
 module PEH = ProofEngineHelpers
 
+module H   = ProceduralHelpers
+
 type dependence = I.S.t * bool
 
 type conclusion = (int * int) option
@@ -52,12 +54,8 @@ let out_table b =
    in
    Array.iteri map b;
    prerr_newline ()
-   
-(****************************************************************************)
-
-let identity x = x
 
-let fst3 (x, _, _) = x
+(* classification ***********************************************************)
 
 let classify_conclusion vs = 
    let rec get_argsno = function
@@ -83,12 +81,13 @@ try
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in
-      (I.get_rels_from_premise h v, I.S.empty, argsno > 0) :: b, succ h
+      let iu = H.is_unsafe h (List.hd vs) in
+      (I.get_rels_from_premise h v, I.S.empty, argsno > 0 && iu) :: b, succ h
    in
    let l, h = List.fold_left map ([], 0) vs in
    let b = Array.of_list (List.rev l) in
    let mk_closure b h =
-      let map j = if j < h then I.S.union (fst3 b.(j)) else identity in 
+      let map j = if j < h then I.S.union (H.fst3 b.(j)) else H.identity in 
       for i = pred h downto 0 do
          let direct, unused, fa = b.(i) in
         b.(i) <- I.S.fold map direct direct, unused, fa 
diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
new file mode 100644 (file)
index 0000000..39607fe
--- /dev/null
@@ -0,0 +1,151 @@
+(* Copyright (C) 2003-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module C    = Cic
+module Rf   = CicRefine
+module Un   = CicUniv
+module Pp   = CicPp
+module TC   = CicTypeChecker
+module PEH  = ProofEngineHelpers
+module E    = CicEnvironment
+module UM   = UriManager
+
+(* fresh name generator *****************************************************)
+
+let split name =
+   let rec aux i =
+      if i <= 0 then assert false else
+      let c = name.[pred i] in
+      if c >= '0' && c <= '9' then aux (pred i) 
+      else Str.string_before name i, Str.string_after name i
+   in
+   let before, after = aux (String.length name) in
+   let i = if after = "" then -1 else int_of_string after in
+   before, i
+
+let join (s, i) =
+   C.Name (if i < 0 then s else s ^ string_of_int i)
+
+let mk_fresh_name context name = 
+   let rec aux i = function
+      | []                            -> name, i
+      | Some (C.Name s, _) :: entries ->
+         let m, j = split s in
+        if m = name && j >= i then aux (succ j) entries else aux i entries
+      | _ :: entries                  -> aux i entries
+   in
+   join (aux (-1) context)
+
+let mk_fresh_name context = function
+   | C.Anonymous -> C.Anonymous
+   | C.Name s    -> mk_fresh_name context s
+
+(* helper functions *********************************************************)
+
+let rec list_map_cps g map = function
+   | []       -> g []
+   | hd :: tl -> 
+      let h hd =
+         let g tl = g (hd :: tl) in
+         list_map_cps g map tl  
+      in
+      map h hd
+
+let identity x = x
+
+let compose f g x = f (g x)
+
+let fst3 (x, _, _) = x
+
+let refine c t =
+   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
+   with e -> 
+      Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
+      Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
+      Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
+      raise e
+
+let get_type c t =
+   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+   with e -> 
+      Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
+      Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
+      raise e
+
+let get_tail c t =
+   match PEH.split_with_whd (c, t) with
+      | (_, hd) :: _, _ -> hd
+      | _               -> assert false
+
+let is_proof c t =
+   match get_tail c (get_type c (get_type c t)) with
+      | C.Sort C.Prop -> true
+      | C.Sort _      -> false
+      | _             -> assert false 
+
+let is_unsafe h (c, t) = true
+
+let is_not_atomic = function
+   | C.Sort _
+   | C.Rel _
+   | C.Const _
+   | C.Var _
+   | C.MutInd _ 
+   | C.MutConstruct _ -> false
+   | _                -> true
+
+let get_ind_type uri tyno =
+   match E.get_obj Un.empty_ugraph uri with
+      | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
+      | _                                           -> assert false
+
+let get_default_eliminator context uri tyno ty =
+   let _, (name, _, _, _) = get_ind_type uri tyno in
+   let ext = match get_tail context (get_type context ty) with
+      | C.Sort C.Prop     -> "_ind"
+      | C.Sort C.Set      -> "_rec"
+      | C.Sort C.CProp    -> "_rec"
+      | C.Sort (C.Type _) -> "_rect"
+      | t                 -> 
+         Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
+         assert false
+   in
+   let buri = UM.buri_of_uri uri in
+   let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
+   C.Const (uri, [])
+
+let get_ind_parameters c t =
+   let ty = get_type c t in
+   let ps = match get_tail c ty with
+      | C.MutInd _                  -> []
+      | C.Appl (C.MutInd _ :: args) -> args
+      | _                           -> assert false
+   in
+   let disp = match get_tail c (get_type c ty) with
+      | C.Sort C.Prop -> 0
+      | C.Sort _      -> 1
+      | _             -> assert false
+   in
+   ps, disp
diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli
new file mode 100644 (file)
index 0000000..8484494
--- /dev/null
@@ -0,0 +1,51 @@
+(* Copyright (C) 2003-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val mk_fresh_name:
+   Cic.context -> Cic.name -> Cic.name
+val list_map_cps:
+  ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b
+val identity:
+  'a -> 'a
+val compose:
+   ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+val fst3:
+   'a * 'b * 'c -> 'a 
+val refine:
+   Cic.context -> Cic.term -> Cic.term
+val get_type:
+   Cic.context -> Cic.term -> Cic.term
+val is_proof:
+   Cic.context -> Cic.term -> bool
+val is_unsafe:
+   int -> Cic.context * Cic.term -> bool
+val is_not_atomic:
+   Cic.term -> bool
+val get_ind_type:
+   UriManager.uri -> int -> int * Cic.inductiveType
+val get_default_eliminator:
+  Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term
+val get_ind_parameters:
+   Cic.context -> Cic.term -> Cic.term list * int
index 6b84dd9b9a823757fe06858147c5ab47500203d7..2b8e1ea3d2307bcdf01b22adfab04a9b457a63b9 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-module UM   = UriManager
 module C    = Cic
 module Pp   = CicPp
-module Un   = CicUniv
 module I    = CicInspect
-module E    = CicEnvironment
 module S    = CicSubstitution
-module TC   = CicTypeChecker 
-module Rf   = CicRefine
 module DTI  = DoubleTypeInference
 module HEL  = HExtlib
 module PEH  = ProofEngineHelpers
 
+module H    = ProceduralHelpers
 module Cl   = ProceduralClassify
 
-(* helper functions *********************************************************)
-
-let rec list_map_cps g map = function
-   | []       -> g []
-   | hd :: tl -> 
-      let h hd =
-         let g tl = g (hd :: tl) in
-         list_map_cps g map tl  
-      in
-      map h hd
-
-let identity x = x
-
-let comp f g x = f (g x)
-
-let refine c t =
-   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
-   with e -> 
-      Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
-      Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
-      Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
-      raise e
-
-let get_type c t =
-   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
-   with e -> 
-      Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
-      Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
-      raise e
-
-let get_tail c t =
-   match PEH.split_with_whd (c, t) with
-      | (_, hd) :: _, _ -> hd
-      | _               -> assert false
-
-let is_proof c t =
-   match get_tail c (get_type c (get_type c t)) with
-      | C.Sort C.Prop -> true
-      | C.Sort _      -> false
-      | _             -> assert false 
-
-let is_not_atomic = function
-   | C.Sort _
-   | C.Rel _
-   | C.Const _
-   | C.Var _
-   | C.MutInd _ 
-   | C.MutConstruct _ -> false
-   | _                -> true
-
-let get_ind_type uri tyno =
-   match E.get_obj Un.empty_ugraph uri with
-      | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
-      | _                                           -> assert false
-
-let get_default_eliminator context uri tyno ty =
-   let _, (name, _, _, _) = get_ind_type uri tyno in
-   let ext = match get_tail context (get_type context ty) with
-      | C.Sort C.Prop     -> "_ind"
-      | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
-      | C.Sort (C.Type _) -> "_rect"
-      | t                 -> 
-         Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
-         assert false
-   in
-   let buri = UM.buri_of_uri uri in
-   let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
-   C.Const (uri, [])
-
-let get_ind_parameters c t =
-   let ty = get_type c t in
-   let ps = match get_tail c ty with
-      | C.MutInd _                  -> []
-      | C.Appl (C.MutInd _ :: args) -> args
-      | _                           -> assert false
-   in
-   let disp = match get_tail c (get_type c ty) with
-      | C.Sort C.Prop -> 0
-      | C.Sort _      -> 1
-      | _             -> assert false
-   in
-   ps, disp
-
 (* term preprocessing: optomization 1 ***************************************)
 
 let defined_premise = "DEFINED"
 
-let define v =
+let define v =
    let name = C.Name defined_premise in
    C.LetIn (name, v, C.Rel 1)
 
 let clear_absts m =
    let rec aux k n = function
-      | C.Lambda (s, v, t) when k > 0    -> 
+      | C.Lambda (s, v, t) when k > 0 -> 
          C.Lambda (s, v, aux (pred k) n t)
-      | C.Lambda (_, _, t) when n > 0    -> 
+      | C.Lambda (_, _, t) when n > 0 -> 
          aux 0 (pred n) (S.lift (-1) t)
-      | t                     when n > 0 ->
+      | t                  when n > 0 ->
          Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t);
         assert false 
       | t                                 -> t
@@ -149,15 +61,17 @@ let rec add_abst k = function
    | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
 
 let rec opt1_letin g es c name v t =
+   let name = H.mk_fresh_name c name in
    let entry = Some (name, C.Def (v, None)) in
    let g t =
       if DTI.does_not_occur 1 t then begin         
-         HLog.warn "Optimizer: remove 1"; g (S.lift (-1) t)
+         let x = S.lift (-1) t in
+        HLog.warn "Optimizer: remove 1"; opt1_proof g true c x 
       end else 
       let g = function
-         | C.LetIn (nname, vv, tt) when is_proof c v ->
-            let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
-           HLog.warn "Optimizer: swap 1"; opt1_proof g false c x 
+         | C.LetIn (nname, vv, tt) when H.is_proof c v ->
+           let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
+           HLog.warn "Optimizer: swap 1"; opt1_proof g true c x 
          | v                               -> 
            g (C.LetIn (name, v, t))
       in
@@ -166,6 +80,7 @@ let rec opt1_letin g es c name v t =
    if es then opt1_proof g es (entry :: c) t else g t
 
 and opt1_lambda g es c name w t =
+   let name = H.mk_fresh_name c name in
    let entry = Some (name, C.Decl w) in
    let g t = 
       let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
@@ -179,43 +94,42 @@ and opt1_appl g es c t vs =
          | C.LetIn (mame, vv, tt) ->
             let vs = List.map (S.lift 1) vs in
            let x = C.LetIn (mame, vv, C.Appl (tt :: vs)) in
-           HLog.warn "Optimizer: swap 2"; opt1_proof g false c x
+           HLog.warn "Optimizer: swap 2"; opt1_proof g true c x
          | C.Lambda (name, ww, tt) ->
            let v, vs = List.hd vs, List.tl vs in
            let x = C.Appl (C.LetIn (name, v, tt) :: vs) in
-           HLog.warn "Optimizer: remove 2"; opt1_proof g false c x
+           HLog.warn "Optimizer: remove 2"; opt1_proof g true c x
         | C.Appl vvs              ->
             let x = C.Appl (vvs @ vs) in
-           HLog.warn "Optimizer: nested application"; opt1_proof g false c x
+           HLog.warn "Optimizer: nested application"; opt1_proof g true c x
         | t                       ->
            let rec aux d rvs = function
-              | [], _                 -> 
+              | [], _                   -> 
                  let x = C.Appl (t :: List.rev rvs) in
-                 if d then opt1_proof g false c x else g x
-              | v :: vs, (cb) :: cs ->
-                 if is_not_atomic v && I.S.mem 0 c && b then begin 
+                 if d then opt1_proof g true c x else g x
+              | v :: vs, (cc, bb) :: cs ->
+                 if H.is_not_atomic v && I.S.mem 0 cc && bb then begin 
                     HLog.warn "Optimizer: anticipate 1"; 
-                    aux true (define c v :: rvs) (vs, cs)
+                     aux true (define v :: rvs) (vs, cs)
                  end else 
                     aux d (v :: rvs) (vs, cs)
-              | _, []                 -> assert false
+              | _, []                   -> assert false
            in
            let h () =
-              let classes, conclusion = Cl.classify c (get_type c t) in
+              let classes, conclusion = Cl.classify c (H.get_type c t) in
               let csno, vsno = List.length classes, List.length vs in
-              if csno < vsno && csno > 0 then
+              if csno < vsno then
                  let vvs, vs = HEL.split_nth csno vs in
-                 let x = C.Appl (define (C.Appl (t :: vvs)) :: vs) in
-                 HLog.warn "Optimizer: anticipate 2"; opt1_proof g false c x
+                 let x = C.Appl (define (C.Appl (t :: vvs)) :: vs) in
+                 HLog.warn "Optimizer: anticipate 2"; opt1_proof g true c x
               else match conclusion, List.rev vs with
-                 | Some _, rv :: rvs when csno = vsno && is_not_atomic rv ->
-                    let x = C.Appl (t :: List.rev rvs @ [define rv]) in
-                    HLog.warn "Optimizer: anticipate 3"; opt1_proof g false c x
+                 | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv ->
+                    let x = C.Appl (t :: List.rev rvs @ [define rv]) in
+                    HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x
                  | Some _, _                                              ->
                     g (C.Appl (t :: vs))
                  | None, _                                                ->
-                    if csno > 0 then aux false [] (vs, classes)
-                    else g (C.Appl (t :: vs))
+                    aux false [] (vs, classes)
            in
            let rec aux h prev = function
               | C.LetIn (name, vv, tt) :: vs ->
@@ -224,7 +138,7 @@ and opt1_appl g es c t vs =
                   let vs = List.map (S.lift 1) vs in
                  let y = C.Appl (t :: List.rev prev @ tt :: vs) in
                  let x = C.LetIn (name, vv, y) in  
-                 HLog.warn "Optimizer: swap 3"; opt1_proof g false c x
+                 HLog.warn "Optimizer: swap 3"; opt1_proof g true c x
               | v :: vs                      -> aux h (v :: prev) vs
               | []                           -> h ()
            in 
@@ -232,12 +146,12 @@ and opt1_appl g es c t vs =
       in
       if es then opt1_proof g es c t else g t
    in
-   if es then list_map_cps g (fun h -> opt1_term h es c) vs else g vs
+   if es then H.list_map_cps g (fun h -> opt1_term h es c) vs else g vs
 
 and opt1_mutcase g es c uri tyno outty arg cases =
-   let eliminator = get_default_eliminator c uri tyno outty in
-   let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in
-   let ps, sort_disp = get_ind_parameters c arg in
+   let eliminator = H.get_default_eliminator c uri tyno outty in
+   let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
+   let ps, sort_disp = H.get_ind_parameters c arg in
    let lps, rps = HEL.split_nth lpsno ps in
    let rpsno = List.length rps in
    let predicate = clear_absts rpsno (1 - sort_disp) outty in   
@@ -260,7 +174,7 @@ and opt1_mutcase g es c uri tyno outty arg cases =
    in
    let lifted_cases = List.map2 map2 cases constructors in
    let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
-   let x = refine c (C.Appl args) in
+   let x = H.refine c (C.Appl args) in
    HLog.warn "Optimizer: remove 3"; opt1_proof g es c x
 
 and opt1_cast g es c t w =
@@ -279,7 +193,7 @@ and opt1_proof g es c = function
    | t                          -> opt1_other g es c t
 
 and opt1_term g es c t = 
-   if is_proof c t then opt1_proof g es c t else g t
+   if H.is_proof c t then opt1_proof g es c t else g t
 
 (* term preprocessing: optomization 2 ***************************************)
 
@@ -292,10 +206,10 @@ let eta_expand g tys t =
    let arg i = C.Rel (succ i) in
    let rec aux i f a = function
       | []            -> f, a 
-      | (_, ty) :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
+      | (_, ty) :: tl -> aux (succ i) (H.compose f (lambda i ty)) (arg i :: a) tl
    in
    let n = List.length tys in
-   let absts, args = aux 0 identity [] tys in
+   let absts, args = aux 0 H.identity [] tys in
    let t = match S.lift n t with
       | C.Appl ts -> C.Appl (ts @ args)
       | t         -> C.Appl (t :: args)
@@ -319,18 +233,18 @@ and opt2_appl g c t vs =
    let g vs =
       let x = C.Appl (t :: vs) in
       let vsno = List.length vs in
-      let _, csno = PEH.split_with_whd (c, get_type c t) in
+      let _, csno = PEH.split_with_whd (c, H.get_type c t) in
       if vsno < csno then 
-         let tys, _ = PEH.split_with_whd (c, get_type c x) in
+         let tys, _ = PEH.split_with_whd (c, H.get_type c x) in
         let tys = List.rev (List.tl tys) in
         let tys, _ = HEL.split_nth (csno - vsno) tys in
          HLog.warn "Optimizer: eta 1"; eta_expand g tys x
       else g x 
    in
-   list_map_cps g (fun h -> opt2_term h c) vs
+   H.list_map_cps g (fun h -> opt2_term h c) vs
 
 and opt2_other g c t =
-   let tys, csno = PEH.split_with_whd (c, get_type c t) in
+   let tys, csno = PEH.split_with_whd (c, H.get_type c t) in
    if csno > 0 then begin
       let tys = List.rev (List.tl tys) in      
       HLog.warn "Optimizer: eta 2"; eta_expand g tys t 
@@ -343,13 +257,17 @@ and opt2_proof g c = function
    | t                     -> opt2_other g c t
 
 and opt2_term g c t = 
-   if is_proof c t then opt2_proof g c t else g t
+   if H.is_proof c t then opt2_proof g c t else g t
 
 (* object preprocessing *****************************************************)
 
 let pp_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
-      let g bo = C.Constant (name, Some bo, ty, pars, attrs) in
+      let g bo = 
+         Printf.eprintf "Optimized: %s\n" (Pp.ppterm bo);
+        let _ = H.get_type [] (C.Cast (bo, ty)) in
+        C.Constant (name, Some bo, ty, pars, attrs)
+      in
       Printf.eprintf "BEGIN: %s\n" name;
       begin try opt1_term (opt2_term g []) true [] bo
       with e -> failwith ("PPP: " ^ Printexc.to_string e) end
index 98b14298274542288534df848c3bedf4303fa78d..89d3d00b410b10c92495716812a8b12cf2423ef9 100644 (file)
@@ -82,16 +82,16 @@ let fresh_id seed ids_to_terms ids_to_father_ids =
 
 let source_id_of_id id = "#source#" ^ id;;
 
-exception NotEnoughElements;;
+exception NotEnoughElements of string;;
 
 (*CSC: cut&paste da cicPp.ml *)
 (* get_nth l n   returns the nth element of the list l if it exists or *)
 (* raises NotEnoughElements if l has less than n elements             *)
-let rec get_nth l n =
+let rec get_nth msg l n =
  match (n,l) with
     (1, he::_) -> he
-  | (n, he::tail) when n > 1 -> get_nth tail (n-1)
-  | (_,_) -> raise NotEnoughElements
+  | (n, he::tail) when n > 1 -> get_nth msg tail (n-1)
+  | (_,_) -> raise (NotEnoughElements msg)
 ;;
 
 
@@ -224,7 +224,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
          match tt with
             C.Rel n ->
              let id =
-              match get_nth context n with
+              match get_nth "1" context n with
                  (Some (C.Name s,_)) -> s
                | _ -> "__" ^ string_of_int n
              in
@@ -643,7 +643,7 @@ let plain_acic_term_of_cic_term =
   match t with
      C.Rel n ->
       let idref,id =
-       match get_nth context n with
+       match get_nth "2" context n with
           idref,(Some (C.Name s,_)) -> idref,s
         | idref,_ -> idref,"__" ^ string_of_int n
       in
index e6379283d61f98b173154cd4d256e08a70a667f0..b63a585e6bab0aafaa6cfc8faba6bace779f3cf6 100644 (file)
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotEnoughElements
+exception NotEnoughElements of string
 
 val source_id_of_id : string -> string