- 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
- | 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
module D = Deannotate
module PER = ProofEngineReduction
module Ut = CicUtil
+module DTI = DoubleTypeInference
(* fresh name generator *****************************************************)
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 *********************************************************)
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)
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)
*)
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:
| 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
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
| 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
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, ""
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
(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
+(* 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
@{ ${ 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
@{ ${ 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}.
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 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}.
(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).
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 ≝
projects / helm.git / commitdiff