- 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 !!
let rec proc_lambda st what name v t =
let name = match name with
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
| name -> name
in
let entry = Some (name, C.Decl (H.cic v)) in
module D = Deannotate
module PER = ProofEngineReduction
module Ut = CicUtil
module D = Deannotate
module PER = ProofEngineReduction
module Ut = CicUtil
+module DTI = DoubleTypeInference
(* fresh name generator *****************************************************)
(* fresh name generator *****************************************************)
-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.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 *********************************************************)
(* helper functions *********************************************************)
let get_cofix_decl (sname, w, v) = sname, w in
let rec bc c = function
| C.LetIn (name, v, ty, 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 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 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)
let entry = Some (name, C.Decl w) in
let w, t = bc c w, bc (entry :: c) t in
C.Prod (name, w, 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 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 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 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)
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)
- 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:
val list_fold_right_cps:
('b -> 'c) -> (('b -> 'c) -> 'a -> 'b -> 'c) -> 'a list -> 'b -> 'c
val list_fold_left_cps:
| t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
let rec opt_letin g st es c name v w t =
| 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
let entry = Some (name, C.Def (v, w)) in
let g st t =
if DTI.does_not_occur 1 t then
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 =
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
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
| C.Constant (name, Some bo, ty, pars, attrs) ->
let count_nodes = I.count_nodes ~meta:false 0 in
let st, c = {info = ""; dummy = ()}, [] in
| 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
let bo, ty = H.cic_bc c bo, H.cic_bc c ty in
let g st bo =
if !debug then begin
L.time_stamp ("PO: DONE " ^ name);
C.Constant (name, Some bo, ty, pars, attrs), st.info
in
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, ""
wrap g (info st nodes) c bo
| obj -> obj, ""
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
(CicNotationPres.mpres_of_box bobj)
^ "\n\n" )
| G.Procedural depth ->
(CicNotationPres.mpres_of_box bobj)
^ "\n\n" )
| G.Procedural depth ->
PO.critical := false;
Acic2Procedural.tex_formatter := Some Format.std_formatter;
let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
PO.critical := false;
Acic2Procedural.tex_formatter := Some Format.std_formatter;
let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
+(* 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 < "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
notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
with precedence 20
@{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
}.
@{ ${ 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 < "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
notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
with precedence 20
@{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
}.
@{ ${ 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}.
notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
with precedence 90 for @{ 'pair $a $b}.
inductive ex (A:Type) (P:A \to Prop) : Prop \def
ex_intro: \forall x:A. P x \to ex A P.
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.
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.
inductive exT (A:Type) (P:A→CProp) : CProp ≝
ex_introT: ∀w:A. P w → exT A P.
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}.
notation "\ll term 19 a, break term 19 b \gg"
with precedence 90 for @{'dependent_pair $a $b}.
(ex_introT _ _ a b).
definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
(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).
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).
interpretation "exT \snd" 'pi2 = (pi2exT _ _).
interpretation "exT \snd" 'pi2a x = (pi2exT _ _ x).
interpretation "exT \snd" 'pi2b x y = (pi2exT _ _ x y).
interpretation "dependent pair for Prop" 'dependent_pair a b =
(ex_introP _ _ a b).
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 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).
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).
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].
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].
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 \snd" 'pi2 = (pi2exT23 _ _ _ _).
-interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
interpretation "exT2 \snd" 'pi2a x = (pi2exT23 _ _ _ _ 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 ≝
interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝