From 9ece6e414b255f519426d5643782af4f7dfc584f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 4 Jul 2008 12:03:19 +0000 Subject: [PATCH] - 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 --- .../acic_procedural/acic2Procedural.ml | 8 +++++--- .../acic_procedural/proceduralClassify.ml | 20 ++++++++++++++++++- .../acic_procedural/proceduralClassify.mli | 8 +++++--- .../acic_procedural/proceduralHelpers.ml | 12 +++++++++++ .../acic_procedural/proceduralHelpers.mli | 2 ++ helm/software/components/tactics/tactics.mli | 2 +- .../matita/contribs/LAMBDA-TYPES/Makefile | 2 +- 7 files changed, 45 insertions(+), 9 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index b37eef6bb..ecd4abc74 100644 --- 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 4c0014d2e..e69b471ca 100644 --- 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 aea3c6e81..6a93a1fda 100644 --- 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 4d8652107..54e8ebe05 100644 --- 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 c374a1866..e1b7f49f6 100644 --- 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 7e7127695..927ae8102 100644 --- 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 d9b0cab53..e44fbb49a 100644 --- 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) -- 2.39.2