- Procedural: bug fix in rendering the application: we must handle the

              arguments that are inferrable but do not occur in the goal
- LAMBDA-TYPES: bug fix in Makefile: MAS was not computed correctly

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index b37eef6bbc989034b8dbe2e7fd851dc454baf943..ecd4abc744d79704f02a7cd201ba9fcdf295a58e 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -331,14 +331,16 @@ and proc_appl st what hd tl =
    let script = if proceed then
       let ty = get_type "TC2" st hd in
       let classes, rc = Cl.classify st.context ty in
-      let goal_arity = match get_inner_types st what with
-         | None          -> 0
-        | Some (ity, _) -> snd (PEH.split_with_whd (st.context, H.cic ity))
+      let goal_arity, goal = match get_inner_types st what with
+         | None            -> 0, None
+        | Some (ity, ety) -> 
+          snd (PEH.split_with_whd (st.context, H.cic ity)), Some (H.cic ety)
       in
       let parsno, argsno = List.length classes, List.length tl in
       let decurry = parsno - argsno in
       let diff = goal_arity - decurry in
       if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (H.cic hd)));
+      let classes = Cl.adjust st.context tl ?goal classes in
       let rec mk_synth a n =
          if n < 0 then a else mk_synth (I.S.add n a) (pred n)
       in

diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml
index 4c0014d2e320e4e214aa511f66f1694ee9b6ac59..e69b471ca265400e5057f99c5870529c85072e3f 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralClassify.ml
+++ b/helm/software/components/acic_procedural/proceduralClassify.ml
@@ -31,7 +31,7 @@ module PEH = ProofEngineHelpers
 
 module H   = ProceduralHelpers
 
-type dependence = I.S.t * bool
+type dependences = (I.S.t * bool) list
 
 type conclusion = (int * int * UM.uri * int) option
 
@@ -111,3 +111,21 @@ try
    let extract (x, y, z) = y, z in
    List.rev_map extract (List.tl (Array.to_list b)), rc
 with Invalid_argument _ -> failwith "Classify.classify"
+
+(* adjusting the inferrable arguments that do not occur in the goal *********)
+
+let adjust c vs ?goal classes = 
+   let list_xmap2 map l1 l2 = 
+      let rec aux a = function
+         | hd1 :: tl1, hd2 :: tl2 -> aux (map hd1 hd2 :: a) (tl1,tl2)
+        | _, l2                  -> List.rev_append l2 a
+      in
+      List.rev (aux [] (l1, l2))
+   in
+   let map where what (i, b) = 
+      let what = H.cic what in
+      (i, b || not (H.occurs c ~what ~where))
+   in
+   match goal with
+      | None      -> classes
+      | Some goal -> list_xmap2 (map goal) vs classes

diff --git a/helm/software/components/acic_procedural/proceduralClassify.mli b/helm/software/components/acic_procedural/proceduralClassify.mli
index aea3c6e8164dd1af743670cfd959a6d6d29a3997..6a93a1fdaaad4b4d0ac1a3b79a728135590e9aac 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralClassify.mli
+++ b/helm/software/components/acic_procedural/proceduralClassify.mli
@@ -23,10 +23,12 @@
  * http://cs.unibo.it/helm/.
  *)
 
-type dependence = CicInspect.S.t * bool
+type dependences = (CicInspect.S.t * bool) list
 
 type conclusion = (int * int * UriManager.uri * int) option
 
-val classify: Cic.context -> Cic.term -> dependence list * conclusion
+val classify: Cic.context -> Cic.term -> dependences * conclusion
 
-val to_string: dependence list * conclusion -> string
+val adjust: Cic.context -> Cic.annterm list -> ?goal:Cic.term -> dependences -> dependences
+
+val to_string: dependences * conclusion -> string

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 4d86521074122e31e6907a28c25887355809dd99..54e8ebe050fb5a59cad06150b1c4238daa9da784 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -32,6 +32,8 @@ module PEH  = ProofEngineHelpers
 module E    = CicEnvironment
 module UM   = UriManager
 module D    = Deannotate
+module PER  = ProofEngineReduction
+module Ut   = CicUtil
 
 (* fresh name generator *****************************************************)
 
@@ -159,6 +161,16 @@ let get_ind_parameters c t =
 
 let cic = D.deannotate_term
 
+let occurs c ~what ~where =
+   let result = ref false in
+   let equality c t1 t2 =
+      let r = Ut.alpha_equivalence t1 t2 in
+      result := !result || r; r
+   in
+   let context, what, with_what = c, [what], [C.Rel 0] in
+   let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
+   !result
+
 (* Ensuring Barendregt convenction ******************************************)
 
 let rec add_entries map c = function

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli
index c374a1866c9b266659513bd107e8b8f8ba8dd71b..e1b7f49f6bfaa55d8810407d31df45cdbe903f83 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.mli
+++ b/helm/software/components/acic_procedural/proceduralHelpers.mli
@@ -55,6 +55,8 @@ val get_ind_parameters:
    Cic.context -> Cic.term -> Cic.term list * int
 val cic: 
    Cic.annterm -> Cic.term
+val occurs:
+   Cic.context -> what:Cic.term -> where:Cic.term -> bool
 val cic_bc:
    Cic.context -> Cic.term -> Cic.term
 val acic_bc:

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 7e71276957457d786a2e672750b191c145f9027d..927ae8102e06c4f05a18f0bf04fb09616f873876 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jul  2 12:58:59 CEST 2008 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jul  2 19:37:38 CEST 2008 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyP : term:Cic.term -> ProofEngineTypes.tactic

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
index d9b0cab539c128ef70da99e4a1590b3ebc5e0bac..e44fbb49acf339c35dbe10dc65136e69a5ae4bae 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
@@ -10,7 +10,7 @@ DIRS = Legacy-2 Base-2 LambdaDelta-2
 
 SILENTMAKE = $(H)$(MAKE) H=$(H) -s --no-print-directory
 
-MAS = $(patsubst %.mma, %.ma, $(shell find $(DIRS) -name "*.mma"))
+MAS = $(shell find $(DIRS) -mindepth 2 -name "*.ma")
 
 all: depends
        $(H)$(RM) $(LOG)