From 1e1f24496beba354fb3f550496858b5755d9be0b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 29 Apr 2009 20:58:49 +0000 Subject: [PATCH] - procedural: bugfix in "Barendregt convention" test - library/logic/cprop_connectives.ma: reorganized. notations must immediately follow the definition they refer to (or else another definition can use them in the reconstructed version of the file) - core_notation.moo: added a notation for non-functiona 'exists eta-expansion (not a CIC conversion) should be avoided exp. if the rendered text must be reparsed (ie. during the reconstruction) "default" notation facility reactivated in parsing mode since it is not equivalent to the separated rules (they cover eachother). The bug is in the rendering mode - applyTransformation: debugging information added (commented) logic/cprop_connectives.ma reconstructed and compiled !! --- .../components/acic_procedural/procedural2.ml | 2 +- .../acic_procedural/proceduralHelpers.ml | 25 +++++++++++----- .../acic_procedural/proceduralHelpers.mli | 2 +- .../acic_procedural/proceduralOptimizer.ml | 15 ++++++---- .../components/syntax_extensions/.depend | 3 -- helm/software/matita/applyTransformation.ml | 3 +- helm/software/matita/core_notation.moo | 30 +++++++++++++++++++ .../matita/library/logic/connectives.ma | 2 +- .../matita/library/logic/cprop_connectives.ma | 25 +++++++++------- 9 files changed, 77 insertions(+), 30 deletions(-) diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 9dcd20304..f8007d3fc 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -275,7 +275,7 @@ let mk_rewrite st dtext where qs tl direction t = let rec proc_lambda st what name v t = let name = match name with - | C.Anonymous -> H.mk_fresh_name st.context anonymous_premise + | C.Anonymous -> H.mk_fresh_name true st.context anonymous_premise | name -> name in let entry = Some (name, C.Decl (H.cic v)) in diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index a9fa6473f..3628e5944 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -34,6 +34,7 @@ module UM = UriManager module D = Deannotate module PER = ProofEngineReduction module Ut = CicUtil +module DTI = DoubleTypeInference (* fresh name generator *****************************************************) @@ -61,9 +62,11 @@ let mk_fresh_name context (name, k) = in join (aux k context) -let mk_fresh_name context = function - | C.Anonymous -> C.Anonymous +let mk_fresh_name does_not_occur context = function | C.Name s -> mk_fresh_name context (split s) + | C.Anonymous -> + if does_not_occur then C.Anonymous + else mk_fresh_name context (split "LOCAL") (* helper functions *********************************************************) @@ -245,17 +248,20 @@ let cic_bc c t = let get_cofix_decl (sname, w, v) = sname, w in let rec bc c = function | C.LetIn (name, v, ty, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 t in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Def (v, ty)) in let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in C.LetIn (name, v, ty, t) | C.Lambda (name, w, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 t in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Decl w) in let w, t = bc c w, bc (entry :: c) t in C.Lambda (name, w, t) | C.Prod (name, w, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 t in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Decl w) in let w, t = bc c w, bc (entry :: c) t in C.Prod (name, w, t) @@ -287,17 +293,20 @@ let acic_bc c t = let get_cofix_decl (id, sname, w, v) = sname, cic w in let rec bc c = function | C.ALetIn (id, name, v, ty, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 (cic t) in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Def (cic v, cic ty)) in let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in C.ALetIn (id, name, v, ty, t) | C.ALambda (id, name, w, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 (cic t) in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Decl (cic w)) in let w, t = bc c w, bc (entry :: c) t in C.ALambda (id, name, w, t) | C.AProd (id, name, w, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 (cic t) in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Decl (cic w)) in let w, t = bc c w, bc (entry :: c) t in C.AProd (id, name, w, t) diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 6d4ef50da..358012c87 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -24,7 +24,7 @@ *) val mk_fresh_name: - Cic.context -> Cic.name -> Cic.name + bool -> Cic.context -> Cic.name -> Cic.name val list_fold_right_cps: ('b -> 'c) -> (('b -> 'c) -> 'a -> 'b -> 'c) -> 'a list -> 'b -> 'c val list_fold_left_cps: diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index c27966a4a..0364803c7 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -81,7 +81,7 @@ let rec add_abst k = function | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t) let rec opt_letin g st es c name v w t = - let name = H.mk_fresh_name c name in + let name = H.mk_fresh_name true c name in let entry = Some (name, C.Def (v, w)) in let g st t = if DTI.does_not_occur 1 t then @@ -107,7 +107,7 @@ let rec opt_letin g st es c name v w t = if es then opt_proof g st es (entry :: c) t else g st t and opt_lambda g st es c name w t = - let name = H.mk_fresh_name c name in + let name = H.mk_fresh_name true c name in let entry = Some (name, C.Decl w) in let g st t = g st (C.Lambda (name, w, t)) in if es then opt_proof g st es (entry :: c) t else g st t @@ -259,6 +259,14 @@ let optimize_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> let count_nodes = I.count_nodes ~meta:false 0 in let st, c = {info = ""; dummy = ()}, [] in + L.time_stamp ("PO: OPTIMIZING " ^ name); + let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in + if !debug then begin + Printf.eprintf "BEGIN: %s\n" name; + Printf.eprintf "Initial : %s\n" (Pp.ppterm bo); + prerr_string "Ut.pp_term : "; + Ut.pp_term prerr_string [] c bo; prerr_newline () + end; let bo, ty = H.cic_bc c bo, H.cic_bc c ty in let g st bo = if !debug then begin @@ -272,9 +280,6 @@ let optimize_obj = function L.time_stamp ("PO: DONE " ^ name); C.Constant (name, Some bo, ty, pars, attrs), st.info in - L.time_stamp ("PO: OPTIMIZING " ^ name); - if !debug then Printf.eprintf "BEGIN: %s\n" name; - let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in wrap g (info st nodes) c bo | obj -> obj, "" diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 5ae773c49..9f5f5c311 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -219,7 +219,8 @@ let txt_of_cic_object (CicNotationPres.mpres_of_box bobj) ^ "\n\n" ) | G.Procedural depth -> -(* +(* + PO.debug := true; PO.critical := false; Acic2Procedural.tex_formatter := Some Format.std_formatter; let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index fc6a15b06..b93dd98e1 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -1,8 +1,24 @@ +(* exists *******************************************************************) + +notation < "hvbox(\exists ident i : ty break . p)" + right associative with precedence 20 +for @{'exists (\lambda ${ident i} : $ty. $p) }. + +notation < "hvbox(\exists ident i break . p)" + with precedence 20 +for @{'exists (\lambda ${ident i}. $p) }. + +notation "hvbox(∃ _ break . p)" + with precedence 20 +for @{'exists $p }. + +(* notation < "hvbox(\exists ident i opt (: ty) break . p)" right associative with precedence 20 for @{ 'exists ${default @{\lambda ${ident i} : $ty. $p} @{\lambda ${ident i} . $p}}}. +*) notation > "\exists list1 ident x sep , opt (: T). term 19 Px" with precedence 20 @@ -11,11 +27,23 @@ notation > "\exists list1 ident x sep , opt (: T). term 19 Px" @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } } }. +(* sigma ********************************************************************) + +notation < "hvbox(\Sigma ident i : ty break . p)" + left associative with precedence 20 +for @{'sigma (\lambda ${ident i} : $ty. $p) }. + +notation < "hvbox(\Sigma ident i break . p)" + with precedence 20 +for @{'sigma (\lambda ${ident i}. $p) }. + +(* notation < "hvbox(\Sigma ident i opt (: ty) break . p)" right associative with precedence 20 for @{ 'sigma ${default @{\lambda ${ident i} : $ty. $p} @{\lambda ${ident i} . $p}}}. +*) notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px" with precedence 20 @@ -24,6 +52,8 @@ notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px" @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } } }. +(* other notations **********************************************************) + notation "hvbox(\langle term 19 a, break term 19 b\rangle)" with precedence 90 for @{ 'pair $a $b}. diff --git a/helm/software/matita/library/logic/connectives.ma b/helm/software/matita/library/logic/connectives.ma index 832d1a531..16255bdca 100644 --- a/helm/software/matita/library/logic/connectives.ma +++ b/helm/software/matita/library/logic/connectives.ma @@ -69,7 +69,7 @@ definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \lnot A. inductive ex (A:Type) (P:A \to Prop) : Prop \def ex_intro: \forall x:A. P x \to ex A P. -interpretation "exists" 'exists \eta.x = (ex _ x). +interpretation "exists" 'exists x = (ex _ x). inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q. diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma index 2a5af4406..d2e91d555 100644 --- a/helm/software/matita/library/logic/cprop_connectives.ma +++ b/helm/software/matita/library/logic/cprop_connectives.ma @@ -76,7 +76,7 @@ interpretation "logical iff type1" 'iff1 x y = (Iff1 x y). inductive exT (A:Type) (P:A→CProp) : CProp ≝ ex_introT: ∀w:A. P w → exT A P. -interpretation "CProp exists" 'exists \eta.x = (exT _ x). +interpretation "CProp exists" 'exists x = (exT _ x). notation "\ll term 19 a, break term 19 b \gg" with precedence 90 for @{'dependent_pair $a $b}. @@ -84,12 +84,14 @@ interpretation "dependent pair" 'dependent_pair a b = (ex_introT _ _ a b). definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x]. -definition pi2exT ≝ - λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p]. interpretation "exT \fst" 'pi1 = (pi1exT _ _). interpretation "exT \fst" 'pi1a x = (pi1exT _ _ x). interpretation "exT \fst" 'pi1b x y = (pi1exT _ _ x y). + +definition pi2exT ≝ + λA,P.λx:exT A P.match x return λx.P (pi1exT ? ? x) with [ex_introT _ p ⇒ p]. + interpretation "exT \snd" 'pi2 = (pi2exT _ _). interpretation "exT \snd" 'pi2a x = (pi2exT _ _ x). interpretation "exT \snd" 'pi2b x y = (pi2exT _ _ x y). @@ -100,33 +102,36 @@ inductive exP (A:Type) (P:A→Prop) : CProp ≝ interpretation "dependent pair for Prop" 'dependent_pair a b = (ex_introP _ _ a b). -interpretation "CProp exists for Prop" 'exists \eta.x = (exP _ x). +interpretation "CProp exists for Prop" 'exists x = (exP _ x). definition pi1exP ≝ λA,P.λx:exP A P.match x with [ex_introP x _ ⇒ x]. -definition pi2exP ≝ - λA,P.λx:exP A P.match x return λx.P (pi1exP ?? x) with [ex_introP _ p ⇒ p]. interpretation "exP \fst" 'pi1 = (pi1exP _ _). interpretation "exP \fst" 'pi1a x = (pi1exP _ _ x). interpretation "exP \fst" 'pi1b x y = (pi1exP _ _ x y). + +definition pi2exP ≝ + λA,P.λx:exP A P.match x return λx.P (pi1exP ?? x) with [ex_introP _ p ⇒ p]. + interpretation "exP \snd" 'pi2 = (pi2exP _ _). interpretation "exP \snd" 'pi2a x = (pi2exP _ _ x). interpretation "exP \snd" 'pi2b x y = (pi2exP _ _ x y). - inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝ ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R. definition pi1exT23 ≝ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x]. + +interpretation "exT2 \fst" 'pi1 = (pi1exT23 _ _ _ _). +interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x). +interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y). + definition pi2exT23 ≝ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x]. -interpretation "exT2 \fst" 'pi1 = (pi1exT23 _ _ _ _). interpretation "exT2 \snd" 'pi2 = (pi2exT23 _ _ _ _). -interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x). interpretation "exT2 \snd" 'pi2a x = (pi2exT23 _ _ _ _ x). -interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y). interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y). inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝ -- 2.39.2