Procedural : cic object preprocessor added

depend[.opt]: some fixes

diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend
index 1b2fc5ff0b5505e2701e7cf404bc9ec3f2944937..8cb9645ae7d90c02134a090f652ab83181419547 100644 (file)
--- a/helm/software/components/acic_procedural/.depend
+++ b/helm/software/components/acic_procedural/.depend
@@ -1,14 +1,20 @@
+proceduralPreprocess.cmo: proceduralPreprocess.cmi 
+proceduralPreprocess.cmx: proceduralPreprocess.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
-proceduralClassify.cmo: proceduralClassify.cmi 
-proceduralClassify.cmx: proceduralClassify.cmi 
-proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
-proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
-proceduralConversion.cmo: proceduralTypes.cmi proceduralClassify.cmi \
-    proceduralConversion.cmi 
-proceduralConversion.cmx: proceduralTypes.cmx proceduralClassify.cmx \
-    proceduralConversion.cmi 
-acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \
-    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
-acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \
-    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
+proceduralClassify.cmo: proceduralPreprocess.cmi proceduralClassify.cmi 
+proceduralClassify.cmx: proceduralPreprocess.cmx proceduralClassify.cmi 
+proceduralMode.cmo: proceduralPreprocess.cmi proceduralClassify.cmi \
+    proceduralMode.cmi 
+proceduralMode.cmx: proceduralPreprocess.cmx proceduralClassify.cmx \
+    proceduralMode.cmi 
+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 \
+    proceduralMode.cmi proceduralConversion.cmi proceduralClassify.cmi \
+    acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
+    proceduralMode.cmx proceduralConversion.cmx proceduralClassify.cmx \
+    acic2Procedural.cmi 

diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt
index 1b2fc5ff0b5505e2701e7cf404bc9ec3f2944937..8cb9645ae7d90c02134a090f652ab83181419547 100644 (file)
--- a/helm/software/components/acic_procedural/.depend.opt
+++ b/helm/software/components/acic_procedural/.depend.opt
@@ -1,14 +1,20 @@
+proceduralPreprocess.cmo: proceduralPreprocess.cmi 
+proceduralPreprocess.cmx: proceduralPreprocess.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
-proceduralClassify.cmo: proceduralClassify.cmi 
-proceduralClassify.cmx: proceduralClassify.cmi 
-proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
-proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
-proceduralConversion.cmo: proceduralTypes.cmi proceduralClassify.cmi \
-    proceduralConversion.cmi 
-proceduralConversion.cmx: proceduralTypes.cmx proceduralClassify.cmx \
-    proceduralConversion.cmi 
-acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \
-    proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
-acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \
-    proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi 
+proceduralClassify.cmo: proceduralPreprocess.cmi proceduralClassify.cmi 
+proceduralClassify.cmx: proceduralPreprocess.cmx proceduralClassify.cmi 
+proceduralMode.cmo: proceduralPreprocess.cmi proceduralClassify.cmi \
+    proceduralMode.cmi 
+proceduralMode.cmx: proceduralPreprocess.cmx proceduralClassify.cmx \
+    proceduralMode.cmi 
+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 \
+    proceduralMode.cmi proceduralConversion.cmi proceduralClassify.cmi \
+    acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
+    proceduralMode.cmx proceduralConversion.cmx proceduralClassify.cmx \
+    acic2Procedural.cmi 

diff --git a/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile
index 8b3ea3695eabbb88f9b0d05086dad0e004510477..379f5518bdccedb66f1b616e374915e5e9590557 100644 (file)
--- a/helm/software/components/acic_procedural/Makefile
+++ b/helm/software/components/acic_procedural/Makefile
@@ -2,6 +2,7 @@ PACKAGE = acic_procedural
 PREDICATES =
 
 INTERFACE_FILES =               \
+       proceduralPreprocess.mli \
        proceduralTypes.mli      \
        proceduralClassify.mli   \
        proceduralMode.mli       \

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index bbc358f71e7fbc0db2eebce8f7624e393d072877..28fa9894795e52e629d6cfdf1d14a3064ccfebf6 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -37,6 +37,7 @@ module Ut   = CicUtil
 module E    = CicEnvironment
 module PER  = ProofEngineReduction
 
+module P    = ProceduralPreprocess
 module Cl   = ProceduralClassify
 module M    = ProceduralMode
 module T    = ProceduralTypes
@@ -292,7 +293,7 @@ and mk_proof st = function
       let script = if proceed then
          let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
          let (classes, rc) as h = Cl.classify st.context ty in
-         let premises, _ = Cl.split st.context ty in
+         let premises, _ = P.split st.context ty in
         let decurry = List.length classes - List.length tl in
          if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
          if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else

diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml
index 6fd8a5e60597adb67540b4219ea20d1677d9e442..2fd2d979d7053abecb185562b9567858df3e6b8c 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralClassify.ml
+++ b/helm/software/components/acic_procedural/proceduralClassify.ml
@@ -24,10 +24,11 @@
  *)
 
 module C = Cic
-module R = CicReduction
 module D = Deannotate
 module I = CicInspect
 
+module P = ProceduralPreprocess
+
 type conclusion = (int * int) option
 
 (* debugging ****************************************************************)
@@ -55,15 +56,6 @@ let out_table b =
 
 let id x = x
 
-let split c t =
-   let add s v c = Some (s, C.Decl v) :: c in
-   let rec aux whd a n c = function
-      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
-      | v when whd        -> v :: a, n
-      | v                 -> aux true a n c (R.whd ~delta:true c v)
-    in
-    aux false [] 0 c t
-
 let classify_conclusion = function
    | C.Rel i                -> Some (i, 0)
    | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
@@ -71,7 +63,7 @@ let classify_conclusion = function
 
 let classify c t =
 try   
-   let vs, h = split c t in
+   let vs, h = P.split c t in
    let rc = classify_conclusion (List.hd vs) in
    let map (b, h) v = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in
    let l, h = List.fold_left map ([], 0) vs in

diff --git a/helm/software/components/acic_procedural/proceduralClassify.mli b/helm/software/components/acic_procedural/proceduralClassify.mli
index 35c07ab472052fda0556b647052d93624799108b..90c2c785262819efebab53563ff1bc3dea4056b4 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralClassify.mli
+++ b/helm/software/components/acic_procedural/proceduralClassify.mli
@@ -28,5 +28,3 @@ type conclusion = (int * int) option
 val classify: Cic.context -> Cic.term -> CicInspect.S.t list * conclusion
 
 val to_string: CicInspect.S.t list * conclusion -> string
-
-val split: Cic.context -> Cic.term -> Cic.term list * int

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 3bee4dd57e0cdebc9c7bbb3298b159ec964d5b36..3df6802ffa7f84b47f65d33b4bc36e30809447ef 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -30,8 +30,8 @@ module TC   = CicTypeChecker
 module D    = Deannotate
 module UM   = UriManager
 
+module P    = ProceduralPreprocess
 module T    = ProceduralTypes
-module Cl   = ProceduralClassify
 module M    = ProceduralMode
 
 (* helpers ******************************************************************)
@@ -174,7 +174,7 @@ try
         if is_recursive premise then 0, lift (succ k) 1 case, succ k else
         0, case, succ k
       in
-      let premises, _ = Cl.split context cty in
+      let premises, _ = P.split context cty in
       let _, lifted_case, _ =
          List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises))
       in

diff --git a/helm/software/components/acic_procedural/proceduralMode.ml b/helm/software/components/acic_procedural/proceduralMode.ml
index 433966d1b68200e0896b8748a7abe200fb5720d8..2b233a4bf358e4fc18d9f2de8bc6cb265b0b42e8 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralMode.ml
+++ b/helm/software/components/acic_procedural/proceduralMode.ml
@@ -24,6 +24,8 @@
  *)
 
 module C  = Cic
+
+module P = ProceduralPreprocess
 module Cl = ProceduralClassify
 
 let is_eliminator = function
@@ -47,9 +49,9 @@ let rec is_appl b = function
 
 let bkd c t =
    let classes, rc = Cl.classify c t in
-   let premises, _ = Cl.split c t in
+   let premises, _ = P.split c t in
    match rc with
       | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true
       | _ ->
-         let ts, _ = Cl.split c t in
+         let ts, _ = P.split c t in
          is_appl true (List.hd ts)

diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend
index 0d1e0cafcf05ef125febf912738e0d2c5a4ac904..a1a32d4570a08eb2986107a8522226e6aaf4877d 100644 (file)
--- a/helm/software/components/cic/.depend
+++ b/helm/software/components/cic/.depend
@@ -5,6 +5,7 @@ cicUtil.cmi: cic.cmo
 helmLibraryObjects.cmi: cic.cmo 
 discrimination_tree.cmi: cic.cmo 
 path_indexing.cmi: cic.cmo 
+cicInspect.cmi: cic.cmo 
 cic.cmo: cicUniv.cmi 
 cic.cmx: cicUniv.cmx 
 unshare.cmo: cic.cmo unshare.cmi 

diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt
index 94eaa78b8a468f8118c429937416408334fccda4..21644fbe7da98e6b55a63307d99ec8ae2f341994 100644 (file)
--- a/helm/software/components/cic/.depend.opt
+++ b/helm/software/components/cic/.depend.opt
@@ -5,6 +5,7 @@ cicUtil.cmi: cic.cmx
 helmLibraryObjects.cmi: cic.cmx 
 discrimination_tree.cmi: cic.cmx 
 path_indexing.cmi: cic.cmx 
+cicInspect.cmi: cic.cmx 
 cic.cmo: cicUniv.cmi 
 cic.cmx: cicUniv.cmx 
 unshare.cmo: cic.cmx unshare.cmi 

diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend
index 8b943bb3dd240c37f5ae34b8181da2689fa68237..add1a46c368998004c9f02aec983dae07f75c414 100644 (file)
--- a/helm/software/matita/.depend
+++ b/helm/software/matita/.depend
@@ -17,9 +17,9 @@ matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \
     matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \
     applyTransformation.cmx matitacLib.cmi 
 matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \
-    matitacLib.cmi matitaWiki.cmo gragrep.cmi 
+    matitacLib.cmi matitaWiki.cmo matitaInit.cmi matitaEngine.cmi gragrep.cmi 
 matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \
-    matitacLib.cmx matitaWiki.cmx gragrep.cmx 
+    matitacLib.cmx matitaWiki.cmx matitaInit.cmx matitaEngine.cmx gragrep.cmx 
 matitadep.cmo: matitaInit.cmi matitadep.cmi 
 matitadep.cmx: matitaInit.cmx matitadep.cmi 
 matitaEngine.cmo: matitaEngine.cmi 

diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt
index b0119369bbd71bf23bfa0c3e9ad735bf96617e52..fd3810b9701f549f825f9c039ce1a4658ec4fc57 100644 (file)
--- a/helm/software/matita/.depend.opt
+++ b/helm/software/matita/.depend.opt
@@ -17,9 +17,9 @@ matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \
     matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \
     applyTransformation.cmx matitacLib.cmi 
 matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \
-    matitacLib.cmi matitaWiki.cmx gragrep.cmi 
+    matitacLib.cmi matitaWiki.cmx matitaInit.cmi matitaEngine.cmi gragrep.cmi 
 matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \
-    matitacLib.cmx matitaWiki.cmx gragrep.cmx 
+    matitacLib.cmx matitaWiki.cmx matitaInit.cmx matitaEngine.cmx gragrep.cmx 
 matitadep.cmo: matitaInit.cmi matitadep.cmi 
 matitadep.cmx: matitaInit.cmx matitadep.cmi 
 matitaEngine.cmo: matitaEngine.cmi 

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index f1c1f496d200f41a15ea38171e25747e2e08042e..cff93ace3458413cf2e4089c36a9df3cde4d5709 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -35,6 +35,8 @@
 
 (* $Id$ *)
 
+module G = GrafiteAst
+
 let mpres_document pres_box =
   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
 
@@ -156,27 +158,34 @@ let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm =
    remove_closed_substs s
 
 let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
-  let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = 
-     try Cic2acic.acic_object_of_cic_object obj
+  let get_aobj obj = 
+     try   
+        let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
+            Cic2acic.acic_object_of_cic_object obj
+        in
+       aobj, ids_to_inner_sorts, ids_to_inner_types
      with e -> 
         let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
        failwith msg
   in
   match style with
-     | GrafiteAst.Declarative      ->
-        let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
+     | G.Declarative      ->
+        let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
+       let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
         let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
         remove_closed_substs ("\n\n" ^
           BoxPp.render_to_string ?map_unicode_to_tex
             (function _::x::_ -> x | _ -> assert false) n
             (CicNotationPres.mpres_of_box bobj)
        )
-     | GrafiteAst.Procedural depth ->
+     | G.Procedural depth ->
+        let obj = ProceduralPreprocess.pp_obj obj in
+       let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
         let term_pp = term2pres (n - 8) ids_to_inner_sorts in
         let lazy_term_pp = term_pp in
         let obj_pp = CicNotationPp.pp_obj term_pp in
         let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
-        let script = Acic2Procedural.acic2procedural 
+       let script = Acic2Procedural.acic2procedural 
           ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
        "\n" ^ String.concat "" (List.map aux script)