From 592b7d81b57ec66e0ee007de336e249b07ae0258 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 2 Mar 2009 20:34:04 +0000 Subject: [PATCH] cicInspect: node count fixed proceduralTeX: bug fix LAMBDA-TYPES/Legacy-2/preamble.ma: bug fix character: updated --- .../acic_procedural/proceduralOptimizer.ml | 2 +- .../acic_procedural/proceduralTeX.ml | 8 +++++--- .../acic_procedural/proceduralTypes.ml | 2 +- helm/software/components/cic/cicInspect.ml | 20 ++++++++++--------- helm/software/components/cic/cicInspect.mli | 8 +++++--- .../LAMBDA-TYPES/Legacy-2/preamble.ma | 4 ++-- .../matita/contribs/character/classes/defs.ma | 5 +++++ .../contribs/character/classes/props_pt.ma | 2 +- 8 files changed, 31 insertions(+), 20 deletions(-) diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 50e302460..6910613d2 100644 --- 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 f4f25c402..55be4ddb3 100644 --- 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 9bb2e576c..b7f3e31b9 100644 --- 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 25efa4cab..2016ed98c 100644 --- 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 654044101..a5b79b36d 100644 --- 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 b9b749816..0666938e8 100644 --- 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 d5986fe77..add242cc4 100644 --- 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 cc1c449a3..64b424ae3 100644 --- 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; -- 2.39.2