cicInspect: node count fixed

proceduralTeX: bug fix
LAMBDA-TYPES/Legacy-2/preamble.ma: bug fix
character: updated

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 50e3024605a564caad2e19be389c4984576ff9e3..6910613d29b3b2d2bf778b751e1ce0b268339277 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -253,7 +253,7 @@ let wrap g st c bo =
 
 let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
-      let count_nodes = I.count_nodes ~implicit:false 0 in 
+      let count_nodes = I.count_nodes ~meta:false 0 in 
       let st, c = {info = ""; dummy = ()}, [] in
       let bo, ty = H.cic_bc c bo, H.cic_bc c ty in 
       let g st bo =

diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml
index f4f25c402f813d6e5c545cdcfd13ffcacd6edfa0..55be4ddb3f17168c41c8bb3ee7c8ab17b0cf77dc 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTeX.ml
+++ b/helm/software/components/acic_procedural/proceduralTeX.ml
@@ -168,9 +168,11 @@ let rec xat frm = function
    | C.AImplicit _                    -> assert false
    | C.AAppl (_, [])                  -> assert false
 
-and xats frm vs =
-   let map v = F.fprintf frm "{%a}" xat v in
-   List.iter map vs
+and xats frm = function
+   | [] -> F.fprintf frm "{}"
+   | vs -> 
+      let map v = F.fprintf frm "{%a}" xat v in
+      List.iter map vs
 
 in
 xat frm t

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 9bb2e576c41d71f0c4e3fae06b11f64a8108af09..b7f3e31b9f87b2cf9fc6ded31f63c350152331b9 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -280,7 +280,7 @@ let rec count_step a = function
 
 and count_steps a = List.fold_left count_step a
 
-let count = I.count_nodes ~implicit:false
+let count = I.count_nodes ~meta:false
 
 let rec count_node a = function
    | Note _

diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml
index 25efa4cab4108969e83b5025dc7d3fbc322c8514..2016ed98c845cfb08af0a6750956f9272aa4461a 100644 (file)
--- a/helm/software/components/cic/cicInspect.ml
+++ b/helm/software/components/cic/cicInspect.ml
@@ -111,12 +111,14 @@ let get_mutinds_of_uri u t =
    let g a = a in
    aux g t S.empty
 
-let count_nodes ~implicit n t =
+let count_nodes ~meta n t =
+   let offset = if meta then 1 else 0 in
    let rec aux n = function
-      | C.Implicit _                 -> if implicit then succ n else n
+      | C.Implicit _                 -> offset + n
       | C.Sort _
       | C.Rel _                      -> succ n
-      | C.Appl ts                    -> List.fold_left aux (succ n) ts
+      | C.Appl ts                    -> 
+         List.fold_left aux (List.length ts - 1 + n) ts
       | C.Const (_, ss)
       | C.MutConstruct (_, _, _, ss)
       | C.MutInd (_, _, ss)
@@ -128,18 +130,18 @@ let count_nodes ~implicit n t =
            | None   -> n
            | Some t -> aux n t
          in
-         List.fold_left map (succ n) ss
-      | C.Cast (t1, t2)
+         List.fold_left map (n + offset) ss
+      | C.Cast (t1, t2) -> aux (aux (offset + n) t2) t1
       | C.Lambda (_, t1, t2)
       | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
-      | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) t1
+      | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (offset + 1 + n) t2) ty) t1
       | C.MutCase (_, _, t1, t2, ss) ->
-         aux (aux (List.fold_left aux (succ n) ss) t2) t1
+         aux (aux (List.fold_left aux (offset + 1 + n) ss) t2) t1
       | C.Fix (_, ss)                ->
          let map n (_, _, t1, t2) = aux (aux n t2) t1 in
-         List.fold_left map (succ n) ss
+         List.fold_left map (2 + n) ss
       | C.CoFix (_, ss)              ->
          let map n (_, t1, t2) = aux (aux n t2) t1 in
-         List.fold_left map (succ n) ss
+         List.fold_left map (2 + n) ss
 in
 aux n t

diff --git a/helm/software/components/cic/cicInspect.mli b/helm/software/components/cic/cicInspect.mli
index 6540441014d0cdce236e806f58b0625468d2f607..a5b79b36d475d0aca0bd741bf9b293350ef75447 100644 (file)
--- a/helm/software/components/cic/cicInspect.mli
+++ b/helm/software/components/cic/cicInspect.mli
@@ -31,6 +31,8 @@ val get_rels_from_premise: int -> Cic.term -> S.t
 
 val get_mutinds_of_uri: UriManager.uri -> Cic.term -> S.t
 
-(* count_nodes n t returns n + the number of nodes in t *)
-(* Cic.Implict nodes are counted if ~implicit:true      *)
-val count_nodes: implicit:bool -> int -> Cic.term -> int
+(* count_nodes n t returns n + the number of nodes in t                *)
+(* implicits, metas and casts are counted if ~meta:true                *)
+(* if ~meta:false, complies with                                       *)
+(* F.Guidi: Procedural representation of CIC Proof Terms. Last version *)
+val count_nodes: meta:bool -> int -> Cic.term -> int

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
index b9b749816f0a47d6b69ab5d130a1e940d0d32858..0666938e899ecbd2702454f0995f6e0ecb8984f3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Legacy-1/definitions.ma".
+include "Legacy-1/theory.ma".
 
 default "equality"
  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind
@@ -42,7 +42,7 @@ interpretation "Coq 7.3.1 logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy
 interpretation "Coq 7.3.1 exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
 interpretation "Coq 7.3.1 natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
 interpretation "Coq 7.3.1 natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
-interpretation "Coq 7.3.1 leibnitz's equality" 'eq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) _ x y).
+interpretation "Coq 7.3.1 leibnitz's equality" 'eq t x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) t x y).
 
 alias symbol "plus" = "Coq 7.3.1 natural plus".
 alias symbol "minus" = "Coq 7.3.1 natural minus".

diff --git a/helm/software/matita/contribs/character/classes/defs.ma b/helm/software/matita/contribs/character/classes/defs.ma
index d5986fe7779a5d20926408cdc9cbef0c7e57a1ee..add242cc449f33d9655fb2b46bbb4e5a59eb318e 100644 (file)
--- a/helm/software/matita/contribs/character/classes/defs.ma
+++ b/helm/software/matita/contribs/character/classes/defs.ma
@@ -25,3 +25,8 @@ with T: nat \to Prop \def
    | t1: \forall i. P i \to T (i * 3)
    | t2: \forall i. T i \to T (i * 3)
 .
+
+inductive S: nat \to Prop \def
+   | s1: \forall i. P i \to S (i * 2)
+   | s2: \forall i. T i \to S (i * 2)
+.

diff --git a/helm/software/matita/contribs/character/classes/props_pt.ma b/helm/software/matita/contribs/character/classes/props_pt.ma
index cc1c449a3339babbffc6b10a9d8dcd203ce6b0c1..64b424ae3c71b7f8fd173594ef3e449a7bbc2662 100644 (file)
--- a/helm/software/matita/contribs/character/classes/props_pt.ma
+++ b/helm/software/matita/contribs/character/classes/props_pt.ma
@@ -62,7 +62,7 @@ theorem pt_inv_gen: \forall i.
  [ lapply linear p_inv_O to H; decompose
  | lapply linear t_inv_O to H; decompose
  | inversion H1; clear H1; intros;
-   [ destruct; autobatch depth = 3
+   [ destruct; autobatch depth = 3 width = 50 size = 50
    | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
      lapply linear plus_inv_S_S_S to H4; decompose;
      lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;