From 813f73e76fb7374987ea1e826bcd6f15e22377d9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 19 Jun 2008 12:15:38 +0000 Subject: [PATCH] - Procedural: we now check that an eliminator opens as many goals as the constructors of the eliminated type So nat_double_ind is not an eliminator for Nat :) - Base-2 : now compiles correctly because we fixed the preamble :) --- .../acic_procedural/acic2Procedural.ml | 22 +++++++++++-------- .../contribs/LAMBDA-TYPES/Base-2/preamble.ma | 3 --- .../matita/contribs/LAMBDA-TYPES/Makefile | 15 +++++-------- 3 files changed, 19 insertions(+), 21 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index e71f443d9..b37eef6bb 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -347,20 +347,24 @@ and proc_appl st what hd tl = let script = List.rev (mk_arg st hd) in match rc with | Some (i, j, uri, tyno) -> - let classes, tl, _, where = split2_last classes tl in - let script = List.rev (mk_arg st where) @ script in - let synth = I.S.add 1 synth in + let classes2, tl2, _, where = split2_last classes tl in + let script2 = List.rev (mk_arg st where) @ script in + let synth2 = I.S.add 1 synth in let names = get_ind_names uri tyno in - let qs = proc_bkd_proofs (next st) synth names classes tl in - if is_rewrite_right hd then - script @ mk_rewrite st dtext where qs tl false what + let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in + if List.length qs <> List.length names then + let qs = proc_bkd_proofs (next st) synth [] classes tl in + let hd = mk_exp_args hd tl classes synth in + script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] + else if is_rewrite_right hd then + script2 @ mk_rewrite st dtext where qs tl2 false what else if is_rewrite_left hd then - script @ mk_rewrite st dtext where qs tl true what + script2 @ mk_rewrite st dtext where qs tl2 true what else - let predicate = List.nth tl (parsno - i) in + let predicate = List.nth tl2 (parsno - i) in let e = Cn.mk_pattern j predicate in let using = Some hd in - (* convert_elim st what what e @ *) script @ + (* convert_elim st what what e @ *) script2 @ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] | None -> let qs = proc_bkd_proofs (next st) synth [] classes tl in diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma index 114efbd53..c2c93f323 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma @@ -14,6 +14,3 @@ include "Base-1/definitions.ma". include "Legacy-2/theory.ma". - -alias symbol "minus" = "Coq's natural minus". -alias symbol "lt" = "Coq's natural 'less than'". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index a5bf30015..fb55d6782 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -6,8 +6,7 @@ MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass DIR=$(shell basename $$PWD) -MMAS = $(shell find Legacy-2 -name "*.mma") -# Base-2 +MMAS = $(shell find Legacy-2 Base-2 -name "*.mma") MAS = $(MMAS:%.mma=%.ma) XMAS = Legacy-2/theory.ma Base-2/theory.ma LambdaDelta-2/theory.ma @@ -19,13 +18,13 @@ $(DIR).opt opt all.opt: depends build: $(MAS) $(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends -# $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends + $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends $(H)$(BIN)matitac $(MATITAOPTIONS) 2> /dev/null $(H)rm depends build.opt: $(MAS) $(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends -# $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends + $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2> /dev/null $(H)rm depends @@ -44,14 +43,12 @@ clean.ma: depend: @echo matitadep $(H)$(BIN)matitadep $(foreach FILE,$(XMAS),-exclude $(FILE)) - $(H)cat Legacy-2/depends >> depends -# Base-2/depends + $(H)cat Legacy-2/depends Base-2/depends >> depends depend.opt: @echo matitadep.opt $(H)$(BIN)matitadep.opt $(foreach FILE,$(XMAS),-exclude $(FILE)) - $(H)cat Legacy-2/depends >> depends -# Base-2/depends + $(H)cat Legacy-2/depends Base-2/depends >> depends depends: depend.opt @@ -61,4 +58,4 @@ depends: depend.opt $(H)echo $@ `$(BIN)matitadep.opt -stdout $@` >> depends include Legacy-2/.depend -# include Base-2/.depend +include Base-2/.depend -- 2.39.2