From 3d5b210d4148e1edb9f7a02c888decf9cc6c30e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 21 Jul 2015 11:03:55 +0200 Subject: Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument. --- pretyping/miscops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index a2c97d2cb1..0926e7a299 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,7 @@ let smartmap_cast_type f c = let glob_sort_eq g1 g2 = match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true -| GType l1, GType l2 -> List.for_all2 CString.equal l1 l2 +| GType l1, GType l2 -> List.equal CString.equal l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with -- cgit v1.2.3 From 246a5011d7a794835aa0f9ca198b3a4a74031ed6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 22 Jul 2015 07:30:50 +0200 Subject: Remove obsolete documentation. (Fix bug #4238) --- doc/refman/RefMan-ext.tex | 3 --- 1 file changed, 3 deletions(-) diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index cc5239a779..d63d22a71c 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1375,9 +1375,6 @@ Check (fun l => map length l = map (list nat) nat length l). \Rem To know which are the implicit arguments of an object, use the command {\tt Print Implicit} (see \ref{PrintImplicit}). -\Rem If the list of arguments is empty, the command removes the -implicit arguments of {\qualid}. - \subsection{Automatic declaration of implicit arguments for a constant} {\Coq} can also automatically detect what are the implicit arguments -- cgit v1.2.3 From c07a9f1e558ab55de3011cbfc9749391ed60c768 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 22 Jul 2015 17:18:17 +0200 Subject: Fix incomplete pattern-matching. I was not seeing the warning due to the 10 deprecation warnings before it... --- kernel/cemitcodes.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 0d9334a50c..6dbfbe9cc2 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -308,6 +308,7 @@ type to_patch = emitcodes * (patch list) * fv let rec subst_strcst s sc = match sc with | Const_sorts _ | Const_b0 _ -> sc + | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) -- cgit v1.2.3 From 754775e39b5fa0342a1f4a46cbce0fc98d569d9d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 22 Jul 2015 17:26:49 +0200 Subject: Extraction: fix primitive projection extraction. Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly. --- plugins/extraction/extraction.ml | 3 ++- test-suite/success/primitiveproj.v | 7 +++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 080512b273..6ae519ef60 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -633,7 +633,8 @@ let rec extract_term env mle mlt c args = | Construct (cp,u) -> extract_cons_app env mle mlt cp u args | Proj (p, c) -> - extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args) + let term = Retyping.expand_projection env (Evd.from_env env) p c [] in + extract_term env mle mlt term args | Rel n -> (* As soon as the expected [mlt] for the head is known, *) (* we unify it with an fresh copy of the stored type of [Rel n]. *) diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 068f8ac3cc..125615c535 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -188,3 +188,10 @@ Set Printing All. Check (@p' nat). Check p'. Unset Printing All. + +Record wrap (A : Type) := { unwrap : A; unwrap2 : A }. + +Definition term (x : wrap nat) := x.(unwrap). +Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x. +Recursive Extraction term term'. +(*Unset Printing Primitive Projection Parameters.*) \ No newline at end of file -- cgit v1.2.3 From 74d347365d4f6425d056cc8df49bb8f8e29ad098 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 22 Jul 2015 17:33:51 +0200 Subject: test-suite: add test for bug# 3743. --- test-suite/bugs/closed/3743.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/3743.v diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v new file mode 100644 index 0000000000..4dfb3380a8 --- /dev/null +++ b/test-suite/bugs/closed/3743.v @@ -0,0 +1,11 @@ +(* File reduced by coq-bug-finder from original input, then from 967 lines to 469 lines, then from 459 lines to 35 lines *) +(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0 + coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *) +Require Export Coq.Setoids.Setoid. + +Fail Add Parametric Relation A +: A (@eq A) + transitivity proved by transitivity + as refine_rel. +(* Toplevel input, characters 20-118: +Anomaly: index to an anonymous variable. Please report. *) \ No newline at end of file -- cgit v1.2.3 From ca63912f21d0e88d3f4d1a37cc75f091b90bb077 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 22 Jul 2015 17:40:22 +0200 Subject: Refman: document Show Universes. --- doc/refman/RefMan-pro.tex | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 684a4add4c..7af87a399a 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -453,11 +453,16 @@ In the case of a non-product goal, it prints nothing. This command is similar to the previous one, it simulates the naming process of an {\tt Intros}. -\item{\tt Show Existentials\label{ShowExistentials}}\comindex{Show Existentials} +\item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials} \\ It displays the set of all uninstantiated existential variables in the current proof tree, along with the type and the context of each variable. +\item{\tt Show Universes.\label{ShowUniverses}}\comindex{Show Universes} +\\ It displays the set of all universe constraints and its +normalized form at the current stage of the proof, useful for +debugging universe inconsistencies. + \end{Variants} -- cgit v1.2.3 From d95d2f57c795195eb8fff75a01fc50b1016ce1ca Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 22 Jul 2015 18:01:48 +0200 Subject: Removing the G_xml module again. The file seems to have been reintroduced by error by commit 012fe1a96, but it was not compiled anyway. --- parsing/g_xml.ml4 | 290 ------------------------------------------------------ 1 file changed, 290 deletions(-) delete mode 100644 parsing/g_xml.ml4 diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 deleted file mode 100644 index 992f9c59af..0000000000 --- a/parsing/g_xml.ml4 +++ /dev/null @@ -1,290 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* x ] ] - ; - xml: - [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml; - "<"; "/"; ctag = IDENT; ">" -> - check_tags (!@loc) otag ctag; - XmlTag (!@loc,ctag,attrs,l) - | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" -> - XmlTag (!@loc,tag,attrs,[]) - ] ] - ; - attr: - [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ] - ; -END - -(* Errors *) - -let error_bad_arity loc n = - let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in - user_err_loc (loc,"",str "wrong number of arguments (expect " ++ str s ++ str ").") - -(* Interpreting attributes *) - -let nmtoken (loc,a) = - try int_of_string a - with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") - -let get_xml_attr s al = - try String.List.assoc s al - with Not_found -> error ("No attribute "^s) - -(* Interpreting specific attributes *) - -let ident_of_cdata (loc,a) = Id.of_string a - -let uri_of_data s = - try - let n = String.index s ':' in - let p = String.index s '.' in - let s = String.sub s (n+2) (p-n-2) in - for i = 0 to String.length s - 1 do - match s.[i] with - | '/' -> s.[i] <- '.' - | _ -> () - done; - qualid_of_string s - with Not_found | Invalid_argument _ -> - error ("Malformed URI \""^s^"\"") - -let constant_of_cdata (loc,a) = - let q = uri_of_data a in - try Nametab.locate_constant q - with Not_found -> error ("No such constant "^string_of_qualid q) - -let global_of_cdata (loc,a) = - let q = uri_of_data a in - try Nametab.locate q - with Not_found -> error ("No such global "^string_of_qualid q) - -let inductive_of_cdata a = match global_of_cdata a with - | IndRef (kn,_) -> kn - | _ -> error (string_of_qualid (uri_of_data (snd a)) ^" is not an inductive") - -let ltacref_of_cdata (loc,a) = - let q = uri_of_data a in - try (loc,Nametab.locate_tactic q) - with Not_found -> error ("No such ltac "^string_of_qualid q) - -let sort_of_cdata (loc,a) = match a with - | "Prop" -> GProp - | "Set" -> GSet - | "Type" -> GType None - | _ -> user_err_loc (loc,"",str "sort expected.") - -let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) - -let get_xml_inductive_kn al = - inductive_of_cdata (* uriType apparent synonym of uri *) - (try get_xml_attr "uri" al - with UserError _ -> get_xml_attr "uriType" al) - -let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al) - -let get_xml_inductive al = - (get_xml_inductive_kn al, nmtoken (get_xml_attr "noType" al)) - -let get_xml_constructor al = - (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al)) - -let get_xml_binder al = - try Name (ident_of_cdata (String.List.assoc "binder" al)) - with Not_found -> Anonymous - -let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al) - -let get_xml_name al = ident_of_cdata (get_xml_attr "name" al) - -let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al) - -let get_xml_no al = Evar.unsafe_of_int (nmtoken (get_xml_attr "no" al)) - -(* A leak in the xml dtd: arities of constructor need to know global env *) - -let compute_branches_lengths ind = - let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in - mip.Declarations.mind_consnrealdecls - -let compute_inductive_ndecls ind = - Inductiveops.inductive_nrealdecls ind - -(* Interpreting constr as a glob_constr *) - -let rec interp_xml_constr = function - | XmlTag (loc,"REL",al,[]) -> - GVar (loc, get_xml_ident al) - | XmlTag (loc,"VAR",al,[]) -> - error "XML parser: unable to interp free variables" - | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) -> - let body,decls = List.sep_last xl in - let ctx = List.map interp_xml_decl decls in - List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b)) - ctx (interp_xml_target body) - | XmlTag (loc,"PROD",al,(_::_ as xl)) -> - let body,decls = List.sep_last xl in - let ctx = List.map interp_xml_decl decls in - List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b)) - ctx (interp_xml_target body) - | XmlTag (loc,"LETIN",al,(_::_ as xl)) -> - let body,defs = List.sep_last xl in - let ctx = List.map interp_xml_def defs in - List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b)) - ctx (interp_xml_target body) - | XmlTag (loc,"APPLY",_,x::xl) -> - GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl) - | XmlTag (loc,"instantiate",_, - (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) -> - GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl) - | XmlTag (loc,"META",al,xl) -> - GEvar (loc, get_xml_name al, Some (List.map interp_xml_substitution xl)) - | XmlTag (loc,"CONST",al,[]) -> - GRef (loc, ConstRef (get_xml_constant al), None) - | XmlTag (loc,"MUTCASE",al,x::y::yl) -> - let ind = get_xml_inductive al in - let p = interp_xml_patternsType x in - let tm = interp_xml_inductiveTerm y in - let vars = compute_branches_lengths ind in - let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl - in - let mat = simple_cases_matrix_of_branches ind brs in - let n = compute_inductive_ndecls ind in - let nal,rtn = return_type_of_predicate ind n p in - GCases (loc,RegularStyle,rtn,[tm,nal],mat) - | XmlTag (loc,"MUTIND",al,[]) -> - GRef (loc, IndRef (get_xml_inductive al), None) - | XmlTag (loc,"MUTCONSTRUCT",al,[]) -> - GRef (loc, ConstructRef (get_xml_constructor al), None) - | XmlTag (loc,"FIX",al,xl) -> - let li,lnct = List.split (List.map interp_xml_FixFunction xl) in - let ln,lc,lt = List.split3 lnct in - let lctx = List.map (fun _ -> []) ln in - GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt) - | XmlTag (loc,"COFIX",al,xl) -> - let ln,lc,lt = List.split3 (List.map interp_xml_CoFixFunction xl) in - GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) - | XmlTag (loc,"CAST",al,[x1;x2]) -> - GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2)) - | XmlTag (loc,"SORT",al,[]) -> - GSort (loc, get_xml_sort al) - | XmlTag (loc,s,_,_) -> - user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") - -and interp_xml_tag s = function - | XmlTag (loc,tag,al,xl) when String.equal tag s -> (loc,al,xl) - | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "", - str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".") - -and interp_xml_constr_alias s x = - match interp_xml_tag s x with - | (_,_,[x]) -> interp_xml_constr x - | (loc,_,_) -> error_bad_arity loc 1 - -and interp_xml_term x = interp_xml_constr_alias "term" x -and interp_xml_type x = interp_xml_constr_alias "type" x -and interp_xml_target x = interp_xml_constr_alias "target" x -and interp_xml_body x = interp_xml_constr_alias "body" x -and interp_xml_pattern x = interp_xml_constr_alias "pattern" x -and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x -and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x -and interp_xml_arg x = interp_xml_constr_alias "arg" x -and interp_xml_substitution x = - match interp_xml_tag "substitution" x with - _, al, [x] -> get_xml_name al, interp_xml_constr x - | loc, _, _ -> error_bad_arity loc 1 - (* no support for empty substitution from official dtd *) - -and interp_xml_decl_alias s x = - match interp_xml_tag s x with - | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x) - | (loc,_,_) -> error_bad_arity loc 1 - -and interp_xml_def x = interp_xml_decl_alias "def" x -and interp_xml_decl x = interp_xml_decl_alias "decl" x - -and interp_xml_recursionOrder x = - let (loc, al, l) = interp_xml_tag "RecursionOrder" x in - let (locs, s) = get_xml_attr "type" al in - match s, l with - | "Structural", [] -> GStructRec - | "Structural", _ -> error_bad_arity loc 0 - | "WellFounded", [c] -> GWfRec (interp_xml_type c) - | "WellFounded", _ -> error_bad_arity loc 1 - | "Measure", [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r)) - | "Measure", _ -> error_bad_arity loc 2 - | _ -> user_err_loc (locs,"",str "Invalid recursion order.") - -and interp_xml_FixFunction x = - match interp_xml_tag "FixFunction" x with - | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *) - ((Some (nmtoken (get_xml_attr "recIndex" al)), - interp_xml_recursionOrder x1), - (get_xml_name al, interp_xml_type x2, interp_xml_body x3)) - | (loc,al,[x1;x2]) -> - ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec), - (get_xml_name al, interp_xml_type x1, interp_xml_body x2)) - | (loc,_,_) -> - error_bad_arity loc 1 - -and interp_xml_CoFixFunction x = - match interp_xml_tag "CoFixFunction" x with - | (loc,al,[x1;x2]) -> - (get_xml_name al, interp_xml_type x1, interp_xml_body x2) - | (loc,_,_) -> - error_bad_arity loc 1 - -(* Interpreting tactic argument *) - -let rec interp_xml_tactic_arg = function - | XmlTag (loc,"TERM",[],[x]) -> - ConstrMayEval (ConstrTerm (interp_xml_constr x,None)) - | XmlTag (loc,"CALL",al,xl) -> - let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in - TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl) - | XmlTag (loc,s,_,_) -> - user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") - -let parse_tactic_arg ch = - interp_xml_tactic_arg - (Pcoq.Gram.entry_parse xml_eoi - (Pcoq.Gram.parsable (Stream.of_channel ch))) -- cgit v1.2.3 From f19ff322973c2dffd4f1f34386057ac1e08a227d Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 22 Jul 2015 12:29:13 -0700 Subject: a small amount of documentation on the virtual machine. --- kernel/cbytecodes.ml | 29 +++++++++++++---------------- kernel/cbytecodes.mli | 28 ++++++++++++++-------------- 2 files changed, 27 insertions(+), 30 deletions(-) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 3271ac1458..940b5528d3 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -24,8 +24,8 @@ let fix_tag = 3 let switch_tag = 4 let cofix_tag = 5 let cofix_evaluated_tag = 6 -(* It could be greate if OCaml export this value, - So fixme if this occur in a new version of OCaml *) +(* It would be great if OCaml exported this value, + So fixme if this happens in a new version of OCaml *) let last_variant_tag = 245 type structured_constant = @@ -35,7 +35,6 @@ type structured_constant = | Const_b0 of tag | Const_bn of tag * structured_constant array - type reloc_table = (tag * int) array type annot_switch = @@ -59,24 +58,22 @@ type instruction = | Kpush | Kpop of int | Kpush_retaddr of Label.t - | Kapply of int (* number of arguments *) - | Kappterm of int * int (* number of arguments, slot size *) - | Kreturn of int (* slot size *) + | Kapply of int + | Kappterm of int * int + | Kreturn of int | Kjump | Krestart - | Kgrab of int (* number of arguments *) - | Kgrabrec of int (* rec arg *) - | Kclosure of Label.t * int (* label, number of free variables *) + | Kgrab of int + | Kgrabrec of int + | Kclosure of Label.t * int | Kclosurerec of int * int * Label.t array * Label.t array - (* nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array - (* nb fv, init, lbl types, lbl bodies *) | Kgetglobal of pconstant | Kconst of structured_constant - | Kmakeblock of int * tag (* size, tag *) + | Kmakeblock of int * tag | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int - | Kswitch of Label.t array * Label.t array (* consts,blocks *) + | Kswitch of Label.t array * Label.t array | Kpushfields of int | Kfield of int | Ksetfield of int @@ -210,7 +207,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal (id,u) -> str "getglobal " ++ pr_con id + | Kgetglobal (id,_u) -> str "getglobal " ++ pr_con id | Kconst sc -> str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> @@ -261,12 +258,12 @@ and pp_bytecodes c = match c with | [] -> str "" | Klabel lbl :: c -> - str "L" ++ int lbl ++ str ":" ++ str "\n" ++ + str "L" ++ int lbl ++ str ":" ++ fnl () ++ pp_bytecodes c | Ksequence (l1, l2) :: c -> pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c | i :: c -> - str "\t" ++ pp_instr i ++ str "\n" ++ pp_bytecodes c + tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c let dump_bytecode c = pperrnl (pp_bytecodes c); diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 745ef311b0..8f594a45b5 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -44,13 +44,13 @@ module Label : type instruction = | Klabel of Label.t - | Kacc of int - | Kenvacc of int - | Koffsetclosure of int - | Kpush - | Kpop of int - | Kpush_retaddr of Label.t - | Kapply of int (** number of arguments *) + | Kacc of int (** accu = sp[n] *) + | Kenvacc of int (** accu = coq_env[n] *) + | Koffsetclosure of int (** accu = &coq_env[n] *) + | Kpush (** sp = accu :: sp *) + | Kpop of int (** sp = skipn n sp *) + | Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *) + | Kapply of int (** number of arguments (arguments on top of stack) *) | Kappterm of int * int (** number of arguments, slot size *) | Kreturn of int (** slot size *) | Kjump @@ -62,15 +62,15 @@ type instruction = (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of pconstant + | Kgetglobal of pconstant (** accu = coq_global_data[c] *) | Kconst of structured_constant - | Kmakeblock of int * tag (** size, tag *) + | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block *) | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int | Kswitch of Label.t array * Label.t array (** consts,blocks *) | Kpushfields of int - | Kfield of int - | Ksetfield of int + | Kfield of int (** accu = accu[n] *) + | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *) | Kstop | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (** index of the projected argument, @@ -136,9 +136,9 @@ type vm_env = { type comp_env = { - nb_stack : int; (** nbre de variables sur la pile *) - in_stack : int list; (** position dans la pile *) - nb_rec : int; (** nbre de fonctions mutuellement *) + nb_stack : int; (** number of variables on the stack *) + in_stack : int list; (** position in the stack *) + nb_rec : int; (** number of mutually recursive functions *) (** recursives = nbr *) pos_rec : instruction list; (** instruction d'acces pour les variables *) (** de point fix ou de cofix *) -- cgit v1.2.3 From 92dfc77c7496297e094e2d39790a205d548b31da Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 22 Jul 2015 13:12:43 -0700 Subject: adding a missing case for printing zippers. --- dev/vm_printers.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 4578a3b33d..3d688011c2 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -49,6 +49,7 @@ let rec ppzipper z = close_box() | Zfix _ -> print_string "Zfix" | Zswitch _ -> print_string "Zswitch" + | Zproj _ -> print_string "Zproj" and ppstack s = open_hovbox 0; -- cgit v1.2.3 From 4456b5edc3e2e62624e5251ff1e01dd81fabb29b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Jul 2015 15:02:30 -0700 Subject: Silence `which` On Fedora, `which 2>&1 >/dev/null` doesn't silence stderr, while `which >/dev/null 2>&1` does. --- Makefile.build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.build b/Makefile.build index 404f176ab4..83cdd506e3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -101,7 +101,7 @@ BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils -ifeq ($(shell which codesign 2>&1 > /dev/null && echo $(ARCH)),Darwin) +ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist" CODESIGN:=codesign -s - else -- cgit v1.2.3 From d0f9a5523bf16b18bfdf8f427b0e5f005336fa39 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 24 Jul 2015 15:41:11 +0200 Subject: Fixing bug #4265: "coqdep does not handle From ... Require" for good. --- tools/coqdep.ml | 8 -------- tools/coqdep_common.ml | 37 ++++++++++++++++++++++++++----------- tools/coqdep_common.mli | 2 +- 3 files changed, 27 insertions(+), 20 deletions(-) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index ec8e983ec2..99b6c7e06f 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -36,14 +36,6 @@ let warning_mult suf iter = in iter check -let add_coqlib_known recur phys_dir log_dir f = - match get_extension f [".vo"] with - | (basename,".vo") -> - let name = log_dir@[basename] in - let paths = if recur then suffixes name else [name] in - List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths - | _ -> () - let sort () = let seen = Hashtbl.create 97 in let rec loop file = diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 0868c9e117..d884558527 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -138,24 +138,31 @@ let get_prefix p l = in drop_prefix_rec (p, l) -exception Found of string - -let search_v_known ?from s = match from with -| None -> fst (Hashtbl.find vKnown s) +let search_table (type r) is_root table ?from s = match from with +| None -> Hashtbl.find table s | Some from -> - let iter logpath (phys_dir, root) = - if root then match get_prefix from logpath with + let module M = struct exception Found of r end in + let iter logpath binding = + if is_root binding then match get_prefix from logpath with | None -> () | Some rem -> match get_prefix (List.rev s) (List.rev rem) with | None -> () - | Some _ -> raise (Found phys_dir) + | Some _ -> raise (M.Found binding) in - try Hashtbl.iter iter vKnown; raise Not_found - with Found s -> s + try Hashtbl.iter iter table; raise Not_found + with M.Found s -> s let search_v_known ?from s = - try Some (search_v_known ?from s) with Not_found -> None + let is_root (_, root) = root in + try + let (phys_dir, _) = search_table is_root vKnown ?from s in + Some phys_dir + with Not_found -> None + +let is_in_coqlib ?from s = + let is_root _ = true in + try search_table is_root coqlibKnown ?from s; true with Not_found -> false let clash_v = ref ([]: (string list * string list) list) @@ -353,7 +360,7 @@ let rec traite_fichier_Coq suffixe verbose f = let file_str = safe_assoc from verbose f str in printf " %s%s" (canonize file_str) suffixe with Not_found -> - if verbose && not (Hashtbl.mem coqlibKnown str) then + if verbose && not (is_in_coqlib ?from str) then warning_module_notfound f str end) strl | Declare sl -> @@ -466,6 +473,14 @@ let add_caml_known phys_dir _ f = | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () +let add_coqlib_known recur phys_dir log_dir f = + match get_extension f [".vo"] with + | (basename,".vo") -> + let name = log_dir@[basename] in + let paths = if recur then suffixes name else [name] in + List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths + | _ -> () + let add_known recur phys_dir log_dir f = match get_extension f [".v";".vo"] with | (basename,".v") -> diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 23619d1e60..5e5c4740c6 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -32,7 +32,6 @@ val search_mli_known : string -> dir option val add_mllib_known : string -> dir -> string -> unit val search_mllib_known : string -> dir option val search_v_known : ?from:string list -> string list -> string option -val coqlibKnown : (string list, unit) Hashtbl.t val file_name : string -> string option -> string val escape : string -> string val canonize : string -> string @@ -40,6 +39,7 @@ val mL_dependencies : unit -> unit val coq_dependencies : unit -> unit val suffixes : 'a list -> 'a list list val add_known : bool -> string -> string list -> string -> unit +val add_coqlib_known : bool -> string -> string list -> string -> unit val add_caml_known : string -> string list -> string -> unit val add_directory : bool -> -- cgit v1.2.3 From 8a235780d9b3612e1c01323398da3e80cbbf8e9f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 24 Jul 2015 18:33:11 +0200 Subject: Using maps and sets instead of lists in coqdep. The quadratic behaviour of list searching probably appears with small enough samples. With the advent of usable libraries in Coq, and thus many possible dependencies, better be safe than sorry. --- tools/coqdep.ml | 25 +++++++++++++-------- tools/coqdep_boot.ml | 2 +- tools/coqdep_common.ml | 58 +++++++++++++++++++++++++++++-------------------- tools/coqdep_common.mli | 6 +++-- 4 files changed, 56 insertions(+), 35 deletions(-) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 99b6c7e06f..110d306022 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -289,14 +289,21 @@ struct module DAG = DAG(struct type t = string let compare = compare end) (** TODO: we should share this code with Coqdep_common *) +module VData = struct + type t = string list option * string list + let compare = Pervasives.compare +end + +module VCache = Set.Make(VData) + let treat_coq_file chan = let buf = Lexing.from_channel chan in - let deja_vu_v = ref ([]: (string list option * string list) list) - and deja_vu_ml = ref ([] : string list) in + let deja_vu_v = ref VCache.empty in + let deja_vu_ml = ref StrSet.empty in let mark_v_done from acc str = - let seen = List.mem (from, str) !deja_vu_v in + let seen = VCache.mem (from, str) !deja_vu_v in if not seen then - let () = addQueue deja_vu_v (from, str) in + let () = deja_vu_v := VCache.add (from, str) !deja_vu_v in match search_v_known ?from str with | None -> acc | Some file_str -> (canonize file_str, !suffixe) :: acc @@ -318,8 +325,8 @@ let treat_coq_file chan = in let decl acc str = let s = basename_noext str in - if not (List.mem s !deja_vu_ml) then - let () = addQueue deja_vu_ml s in + if not (StrSet.mem s !deja_vu_ml) then + let () = deja_vu_ml := StrSet.add s !deja_vu_ml in match search_mllib_known s with | Some mldir -> (declare ".cma" mldir s) :: acc | None -> @@ -331,9 +338,9 @@ let treat_coq_file chan = List.fold_left decl acc sl | Load str -> let str = Filename.basename str in - let seen = List.mem (None, [str]) !deja_vu_v in + let seen = VCache.mem (None, [str]) !deja_vu_v in if not seen then - let () = addQueue deja_vu_v (None, [str]) in + let () = deja_vu_v := VCache.add (None, [str]) !deja_vu_v in match search_v_known [str] with | None -> acc | Some file_str -> (canonize file_str, ".v") :: acc @@ -448,7 +455,7 @@ let rec parse = function | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll - | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll + | "-exclude-dir" :: r :: ll -> norec_dirnames := StrSet.add r !norec_dirnames; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index bc3435a644..2d5fd36a63 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -25,7 +25,7 @@ let rec parse = function (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) add_caml_dir r; - norec_dirs:=r::!norec_dirs; + norec_dirs := StrSet.add r !norec_dirs; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index d884558527..8e2159745d 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -17,6 +17,11 @@ open Unix options (see for instance [option_natdynlk] below). *) +module StrSet = Set.Make(String) + +module StrList = struct type t = string list let compare = compare end +module StrListMap = Map.Make(StrList) + let stderr = Pervasives.stderr let stdout = Pervasives.stdout @@ -26,8 +31,8 @@ let option_natdynlk = ref true let option_boot = ref false let option_mldep = ref None -let norec_dirs = ref ([] : string list) -let norec_dirnames = ref ["CVS"; "_darcs"] +let norec_dirs = ref StrSet.empty +let norec_dirnames = ref (List.fold_right StrSet.add ["CVS"; "_darcs"] StrSet.empty) let suffixe = ref ".vo" @@ -90,11 +95,11 @@ let safe_hash_add cmp clq q (k, (v, b)) = try let (v2, _) = Hashtbl.find q k in if not (cmp v v2) then - let rec add_clash = function - (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl - | cl::cltl -> cl::add_clash cltl - | [] -> [(k,[v;v2])] in - clq := add_clash !clq; + let nv = + try v :: StrListMap.find k !clq + with Not_found -> [v; v2] + in + clq := StrListMap.add k nv !clq; (* overwrite previous bindings, as coqc does *) Hashtbl.add q k (v, b) with Not_found -> Hashtbl.add q k (v, b) @@ -164,7 +169,7 @@ let is_in_coqlib ?from s = let is_root _ = true in try search_table is_root coqlibKnown ?from s; true with Not_found -> false -let clash_v = ref ([]: (string list * string list) list) +let clash_v = ref (StrListMap.empty : string list StrListMap.t) let error_cannot_parse s (i,j) = Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; @@ -185,7 +190,7 @@ let warning_declare f s = flush stderr let warning_clash file dir = - match List.assoc dir !clash_v with + match StrListMap.find dir !clash_v with (f1::f2::fl) -> let f = Filename.basename f1 in let d1 = Filename.dirname f1 in @@ -199,7 +204,7 @@ let warning_clash file dir = | _ -> assert false let safe_assoc from verbose file k = - if verbose && List.mem_assoc k !clash_v then warning_clash file k; + if verbose && StrListMap.mem k !clash_v then warning_clash file k; match search_v_known ?from k with | None -> raise Not_found | Some path -> path @@ -257,16 +262,16 @@ let autotraite_fichier_ML md ext = try let chan = open_in (md ^ ext) in let buf = Lexing.from_channel chan in - let deja_vu = ref [md] in + let deja_vu = ref (StrSet.singleton md) in let a_faire = ref "" in let a_faire_opt = ref "" in begin try while true do let (Use_module str) = caml_action buf in - if List.mem str !deja_vu then + if StrSet.mem str !deja_vu then () else begin - addQueue deja_vu str; + deja_vu := StrSet.add str !deja_vu; let byte,opt = depend_ML str in a_faire := !a_faire ^ byte; a_faire_opt := !a_faire_opt ^ opt @@ -342,20 +347,27 @@ let canonize f = | (f,_) :: _ -> escape f | _ -> escape f +module VData = struct + type t = string list option * string list + let compare = Pervasives.compare +end + +module VCache = Set.Make(VData) + let rec traite_fichier_Coq suffixe verbose f = try let chan = open_in f in let buf = Lexing.from_channel chan in - let deja_vu_v = ref ([]: (string list option * string list) list) - and deja_vu_ml = ref ([] : string list) in + let deja_vu_v = ref VCache.empty in + let deja_vu_ml = ref StrSet.empty in try while true do let tok = coq_action buf in match tok with | Require (from, strl) -> List.iter (fun str -> - if not (List.mem (from, str) !deja_vu_v) then begin - addQueue deja_vu_v (from, str); + if not (VCache.mem (from, str) !deja_vu_v) then begin + deja_vu_v := VCache.add (from, str) !deja_vu_v; try let file_str = safe_assoc from verbose f str in printf " %s%s" (canonize file_str) suffixe @@ -371,8 +383,8 @@ let rec traite_fichier_Coq suffixe verbose f = in let decl str = let s = basename_noext str in - if not (List.mem s !deja_vu_ml) then begin - addQueue deja_vu_ml s; + if not (StrSet.mem s !deja_vu_ml) then begin + deja_vu_ml := StrSet.add s !deja_vu_ml; match search_mllib_known s with | Some mldir -> declare ".cma" mldir s | None -> @@ -386,8 +398,8 @@ let rec traite_fichier_Coq suffixe verbose f = in List.iter decl sl | Load str -> let str = Filename.basename str in - if not (List.mem (None, [str]) !deja_vu_v) then begin - addQueue deja_vu_v (None, [str]); + if not (VCache.mem (None, [str]) !deja_vu_v) then begin + deja_vu_v := VCache.add (None, [str]) !deja_vu_v; try let (file_str, _) = Hashtbl.find vKnown [str] in let canon = canonize file_str in @@ -511,9 +523,9 @@ let rec add_directory recur add_file phys_dir log_dir = let phys_f = if phys_dir = "." then f else phys_dir//f in match try (stat phys_f).st_kind with _ -> S_BLK with | S_DIR when recur -> - if List.mem f !norec_dirnames then () + if StrSet.mem f !norec_dirnames then () else - if List.mem phys_f !norec_dirs then () + if StrSet.mem phys_f !norec_dirs then () else add_directory recur add_file phys_f (log_dir@[f]) | S_REG -> add_file phys_dir log_dir f diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 5e5c4740c6..d610a0558d 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -6,13 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module StrSet : Set.S with type elt = string + val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val option_natdynlk : bool ref val option_mldep : string option ref -val norec_dirs : string list ref -val norec_dirnames : string list ref +val norec_dirs : StrSet.t ref +val norec_dirnames : StrSet.t ref val suffixe : string ref type dir = string option val ( // ) : string -> string -> string -- cgit v1.2.3 From beff9386b82c4aa6e066642d56a36c8034f54604 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 26 Jul 2015 07:44:45 +0200 Subject: Remove obsolete question about eta-conversion. --- doc/faq/FAQ.tex | 6 ------ 1 file changed, 6 deletions(-) diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 589933578a..d264ac62a5 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2579,12 +2579,6 @@ Qed. You can help {\Coq} using the {\pattern} tactic. -\Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?} - - This is because \texttt{\{x:A|P x\}} is a notation for -\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to -$\eta$-conversion, this is different from \texttt{sig P}. - \Question{I copy-paste a term and {\Coq} says it is not convertible to the original term. Sometimes it even says the copied term is not -- cgit v1.2.3 From 20147a19e9f9a2bbeab5612c7ac17baaaf810af5 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 26 Jul 2015 08:38:05 +0200 Subject: Regenerate the axiom figure of the FAQ. The .png was ugly (less than 400px wide) and did not match the content of the .fig file (e.g. presence of '$'). To improve things a bit, text is now rendered by latex. --- doc/faq/FAQ.tex | 29 +++- doc/faq/axioms.eps | 413 ++++++++++++++++++++++++++++----------------------- doc/faq/axioms.eps_t | 43 ++++++ doc/faq/axioms.fig | 100 ++++++------- doc/faq/axioms.pdf | Bin 0 -> 4974 bytes doc/faq/axioms.pdf_t | 43 ++++++ doc/faq/axioms.png | Bin 10075 -> 32222 bytes 7 files changed, 381 insertions(+), 247 deletions(-) create mode 100644 doc/faq/axioms.eps_t create mode 100644 doc/faq/axioms.pdf create mode 100644 doc/faq/axioms.pdf_t diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index d264ac62a5..8495156ca1 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -503,19 +503,34 @@ $\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$ \item Extensionality of functions: $\forall f g:A\rightarrow B, (\forall x, f(x)=g(x)) \rightarrow f=g$ \end{itemize} -Here is a summary of the relative strength of these axioms, most -proofs can be found in directory {\tt Logic} of the standard library. -The justification of their validity relies on the interpretability in -set theory. - +Figure~\ref{fig:axioms} is a summary of the relative strength of these +axioms, most proofs can be found in directory {\tt Logic} of the standard +library. (Statements in boldface are the most ``interesting'' ones for +Coq.) The justification of their validity relies on the interpretability +in set theory. + +% fig2dev -m 2 -L png axioms.fig axioms.png +% fig2dev -L pdftex axioms.fig axioms.pdf +% fig2dev -L pdftex_t -p axioms.pdf axioms.fig axioms.pdf_t +% fig2dev -L pstex axioms.fig axioms.eps +% fig2dev -L pstex_t -p axioms.eps axioms.fig axioms.eps_t + +\begin{figure}[htbp] %HEVEA\imgsrc{axioms.png} %BEGIN LATEX +\begin{center} \ifpdf % si on est en pdflatex -\includegraphics[width=1.0\textwidth]{axioms.png} +\scalebox{0.65}{\input{axioms.pdf_t}} +%\includegraphics[width=1.0\textwidth]{axioms.png} \else -\includegraphics[width=1.0\textwidth]{axioms.eps} +\scalebox{0.65}{\input{axioms.eps_t}} +%\includegraphics[width=1.0\textwidth]{axioms.eps} \fi +\end{center} %END LATEX +\caption{The dependency graph of axioms in the Calculus of Inductive Constructions} +\label{fig:axioms} +\end{figure} \Question{What standard axioms are inconsistent with {\Coq}?} diff --git a/doc/faq/axioms.eps b/doc/faq/axioms.eps index 3f3c01c43a..836afc3474 100644 --- a/doc/faq/axioms.eps +++ b/doc/faq/axioms.eps @@ -1,11 +1,11 @@ -%!PS-Adobe-2.0 EPSF-2.0 +%!PS-Adobe-3.0 EPSF-3.0 %%Title: axioms.fig -%%Creator: fig2dev Version 3.2 Patchlevel 4 -%%CreationDate: Wed May 5 18:30:03 2004 -%%For: herbelin@limoux.polytechnique.fr (Hugo Herbelin) -%%BoundingBox: 0 0 437 372 -%%Magnification: 1.0000 +%%Creator: fig2dev Version 3.2 Patchlevel 5e +%%CreationDate: Sun Jul 26 08:23:54 2015 +%%BoundingBox: 0 0 647 514 +%Magnification: 1.0000 %%EndComments +%%BeginProlog /$F2psDict 200 dict def $F2psDict begin $F2psDict /mtrx matrix put @@ -44,10 +44,6 @@ $F2psDict /mtrx matrix put /col31 {1.000 0.840 0.000 srgb} bind def end -save -newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpath --90.0 435.2 translate -1 -1 scale /cp {closepath} bind def /ef {eofill} bind def @@ -80,51 +76,25 @@ newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpa bind def /shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul 4 -2 roll mul srgb} bind def -/reencdict 12 dict def /ReEncode { reencdict begin -/newcodesandnames exch def /newfontname exch def /basefontname exch def -/basefontdict basefontname findfont def /newfont basefontdict maxlength dict def -basefontdict { exch dup /FID ne { dup /Encoding eq -{ exch dup length array copy newfont 3 1 roll put } -{ exch newfont 3 1 roll put } ifelse } { pop pop } ifelse } forall -newfont /FontName newfontname put newcodesandnames aload pop -128 1 255 { newfont /Encoding get exch /.notdef put } for -newcodesandnames length 2 idiv { newfont /Encoding get 3 1 roll put } repeat -newfontname newfont definefont pop end } def -/isovec [ -8#055 /minus 8#200 /grave 8#201 /acute 8#202 /circumflex 8#203 /tilde -8#204 /macron 8#205 /breve 8#206 /dotaccent 8#207 /dieresis -8#210 /ring 8#211 /cedilla 8#212 /hungarumlaut 8#213 /ogonek 8#214 /caron -8#220 /dotlessi 8#230 /oe 8#231 /OE -8#240 /space 8#241 /exclamdown 8#242 /cent 8#243 /sterling -8#244 /currency 8#245 /yen 8#246 /brokenbar 8#247 /section 8#250 /dieresis -8#251 /copyright 8#252 /ordfeminine 8#253 /guillemotleft 8#254 /logicalnot -8#255 /hyphen 8#256 /registered 8#257 /macron 8#260 /degree 8#261 /plusminus -8#262 /twosuperior 8#263 /threesuperior 8#264 /acute 8#265 /mu 8#266 /paragraph -8#267 /periodcentered 8#270 /cedilla 8#271 /onesuperior 8#272 /ordmasculine -8#273 /guillemotright 8#274 /onequarter 8#275 /onehalf -8#276 /threequarters 8#277 /questiondown 8#300 /Agrave 8#301 /Aacute -8#302 /Acircumflex 8#303 /Atilde 8#304 /Adieresis 8#305 /Aring -8#306 /AE 8#307 /Ccedilla 8#310 /Egrave 8#311 /Eacute -8#312 /Ecircumflex 8#313 /Edieresis 8#314 /Igrave 8#315 /Iacute -8#316 /Icircumflex 8#317 /Idieresis 8#320 /Eth 8#321 /Ntilde 8#322 /Ograve -8#323 /Oacute 8#324 /Ocircumflex 8#325 /Otilde 8#326 /Odieresis 8#327 /multiply -8#330 /Oslash 8#331 /Ugrave 8#332 /Uacute 8#333 /Ucircumflex -8#334 /Udieresis 8#335 /Yacute 8#336 /Thorn 8#337 /germandbls 8#340 /agrave -8#341 /aacute 8#342 /acircumflex 8#343 /atilde 8#344 /adieresis 8#345 /aring -8#346 /ae 8#347 /ccedilla 8#350 /egrave 8#351 /eacute -8#352 /ecircumflex 8#353 /edieresis 8#354 /igrave 8#355 /iacute -8#356 /icircumflex 8#357 /idieresis 8#360 /eth 8#361 /ntilde 8#362 /ograve -8#363 /oacute 8#364 /ocircumflex 8#365 /otilde 8#366 /odieresis 8#367 /divide -8#370 /oslash 8#371 /ugrave 8#372 /uacute 8#373 /ucircumflex -8#374 /udieresis 8#375 /yacute 8#376 /thorn 8#377 /ydieresis] def -/Times-Roman /Times-Roman-iso isovec ReEncode /$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def /$F2psEnd {$F2psEnteredState restore end} def +/pageheader { +save +newpath 0 514 moveto 0 0 lineto 647 0 lineto 647 514 lineto closepath clip newpath +-26.1 566.6 translate +1 -1 scale $F2psBegin 10 setmiterlimit 0 slj 0 slc 0.06000 0.06000 sc +} bind def +/pagefooter { +$F2psEnd +restore +} bind def +%%EndProlog +pageheader % % Fig objects follow % @@ -132,247 +102,316 @@ $F2psBegin % here starts figure with depth 50 % Arc 7.500 slw +0 slc gs clippath -3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp +4188 5861 m 4168 6010 l 4227 6018 l 4247 5869 l 4247 5869 l 4202 5984 l 4188 5861 l cp eoclip -n 3600.0 6750.0 150.0 90.0 -90.0 arc +n 14032.5 7222.5 9908.2 -159.9465 -172.9126 arcn gs col0 s gr gr % arrowhead -n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l cp gs 0.00 setgray ef gr col0 s +0 slj +n 4188 5861 m 4202 5984 l 4247 5869 l 4188 5861 l cp gs 0.00 setgray ef gr col0 s % Arc gs clippath -3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp +3465 9040 m 3599 9108 l 3626 9054 l 3492 8987 l 3492 8987 l 3586 9068 l 3465 9040 l cp eoclip -n 3600.0 6450.0 150.0 90.0 -90.0 arc +n 3600.0 8925.0 150.0 90.0000 -90.0000 arc gs col0 s gr gr % arrowhead -n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l cp gs 0.00 setgray ef gr col0 s +n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 l cp gs 0.00 setgray ef gr col0 s % Arc gs clippath -3626 6020 m 3599 5966 l 3465 6034 l 3586 6007 l 3492 6087 l cp -3599 6333 m 3626 6279 l 3492 6212 l 3586 6293 l 3465 6265 l cp +3465 8740 m 3599 8808 l 3626 8754 l 3492 8687 l 3492 8687 l 3586 8768 l 3465 8740 l cp eoclip -n 3600.0 6150.0 150.0 90.0 -90.0 arc +n 3600.0 8625.0 150.0 90.0000 -90.0000 arc gs col0 s gr gr % arrowhead -n 3492 6087 m 3586 6007 l 3465 6034 l 3492 6087 l cp gs 0.00 setgray ef gr col0 s +n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 l cp gs 0.00 setgray ef gr col0 s +% Arc +gs clippath +3492 8262 m 3626 8195 l 3599 8141 l 3465 8209 l 3465 8209 l 3586 8182 l 3492 8262 l cp +3465 8440 m 3599 8508 l 3626 8454 l 3492 8387 l 3492 8387 l 3586 8468 l 3465 8440 l cp +eoclip +n 3600.0 8325.0 150.0 90.0000 -90.0000 arc +gs col0 s gr + gr + % arrowhead -n 3465 6265 m 3586 6293 l 3492 6212 l 3465 6265 l cp gs 0.00 setgray ef gr col0 s +n 3465 8440 m 3586 8468 l 3492 8387 l 3465 8440 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 3492 8262 m 3586 8182 l 3465 8209 l 3492 8262 l cp gs 0.00 setgray ef gr col0 s % Arc gs clippath -3626 6320 m 3599 6266 l 3465 6334 l 3586 6307 l 3492 6387 l cp -3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp +3492 8562 m 3626 8495 l 3599 8441 l 3465 8509 l 3465 8509 l 3586 8482 l 3492 8562 l cp +3465 8740 m 3599 8808 l 3626 8754 l 3492 8687 l 3492 8687 l 3586 8768 l 3465 8740 l cp eoclip -n 3600.0 6450.0 150.0 90.0 -90.0 arc +n 3600.0 8625.0 150.0 90.0000 -90.0000 arc gs col0 s gr gr % arrowhead -n 3492 6387 m 3586 6307 l 3465 6334 l 3492 6387 l cp gs 0.00 setgray ef gr col0 s +n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 l cp gs 0.00 setgray ef gr col0 s % arrowhead -n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l cp gs 0.00 setgray ef gr col0 s +n 3492 8562 m 3586 8482 l 3465 8509 l 3492 8562 l cp gs 0.00 setgray ef gr col0 s % Arc gs clippath -3626 6620 m 3599 6566 l 3465 6634 l 3586 6607 l 3492 6687 l cp -3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp +3492 8862 m 3626 8795 l 3599 8741 l 3465 8809 l 3465 8809 l 3586 8782 l 3492 8862 l cp +3465 9040 m 3599 9108 l 3626 9054 l 3492 8987 l 3492 8987 l 3586 9068 l 3465 9040 l cp eoclip -n 3600.0 6750.0 150.0 90.0 -90.0 arc +n 3600.0 8925.0 150.0 90.0000 -90.0000 arc gs col0 s gr gr % arrowhead -n 3492 6687 m 3586 6607 l 3465 6634 l 3492 6687 l cp gs 0.00 setgray ef gr col0 s +n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 l cp gs 0.00 setgray ef gr col0 s % arrowhead -n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l cp gs 0.00 setgray ef gr col0 s +n 3492 8862 m 3586 8782 l 3465 8809 l 3492 8862 l cp gs 0.00 setgray ef gr col0 s % Arc gs clippath -3626 6920 m 3599 6866 l 3465 6934 l 3586 6907 l 3492 6987 l cp -3599 7233 m 3626 7179 l 3492 7112 l 3586 7193 l 3465 7165 l cp +3492 9162 m 3626 9095 l 3599 9041 l 3465 9109 l 3465 9109 l 3586 9082 l 3492 9162 l cp +3465 9340 m 3599 9408 l 3626 9354 l 3492 9287 l 3492 9287 l 3586 9368 l 3465 9340 l cp eoclip -n 3600.0 7050.0 150.0 90.0 -90.0 arc +n 3600.0 9225.0 150.0 90.0000 -90.0000 arc gs col0 s gr gr % arrowhead -n 3492 6987 m 3586 6907 l 3465 6934 l 3492 6987 l cp gs 0.00 setgray ef gr col0 s +n 3465 9340 m 3586 9368 l 3492 9287 l 3465 9340 l cp gs 0.00 setgray ef gr col0 s % arrowhead -n 3465 7165 m 3586 7193 l 3492 7112 l 3465 7165 l cp gs 0.00 setgray ef gr col0 s +n 3492 9162 m 3586 9082 l 3465 9109 l 3492 9162 l cp gs 0.00 setgray ef gr col0 s % Arc gs clippath -4168 4060 m 4227 4068 l 4247 3919 l 4202 4034 l 4188 3911 l cp +3733 7095 m 3805 7227 l 3858 7198 l 3785 7066 l 3785 7066 l 3817 7186 l 3733 7095 l cp eoclip -n 14032.5 5272.5 9908.2 -159.9 -172.9 arcn +n 6309.5 5767.7 2867.8 -137.3570 150.0374 arcn gs col0 s gr gr % arrowhead -n 4188 3911 m 4202 4034 l 4247 3919 l 4188 3911 l cp gs 0.00 setgray ef gr col0 s +n 3733 7095 m 3817 7186 l 3785 7066 l 3733 7095 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +7204 5860 m 7167 6007 l 7225 6021 l 7262 5874 l 7262 5874 l 7204 5984 l 7204 5860 l cp +eoclip +n 7725 3900 m + 7200 6000 l gs col0 s gr gr + +% arrowhead +n 7204 5860 m 7204 5984 l 7262 5874 l 7204 5860 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath -4170 5790 m 4230 5790 l 4230 5639 l 4200 5759 l 4170 5639 l cp +7170 6914 m 7170 7065 l 7230 7065 l 7230 6914 l 7230 6914 l 7200 7034 l 7170 6914 l cp eoclip -n 4200 5175 m - 4200 5775 l gs col0 s gr gr +n 7200 6225 m + 7200 7050 l gs col0 s gr gr % arrowhead -n 4170 5639 m 4200 5759 l 4230 5639 l 4170 5639 l cp gs 0.00 setgray ef gr col0 s +n 7170 6914 m 7200 7034 l 7230 6914 l 7170 6914 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath -4553 5749 m 4567 5807 l 4714 5771 l 4591 5771 l 4700 5713 l cp +5520 5864 m 5520 6015 l 5580 6015 l 5580 5864 l 5580 5864 l 5550 5984 l 5520 5864 l cp +5580 5761 m 5580 5610 l 5520 5610 l 5520 5761 l 5520 5761 l 5550 5641 l 5580 5761 l cp eoclip -n 7050 5175 m - 4575 5775 l gs col0 s gr gr +n 5550 5625 m + 5550 6000 l gs col0 s gr gr % arrowhead -n 4700 5713 m 4591 5771 l 4714 5771 l 4700 5713 l cp gs 0.00 setgray ef gr col0 s +n 5580 5761 m 5550 5641 l 5520 5761 l 5580 5761 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 5520 5864 m 5550 5984 l 5580 5864 l 5520 5864 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath -4170 4890 m 4230 4890 l 4230 4739 l 4200 4859 l 4170 4739 l cp +3345 3464 m 3345 3615 l 3405 3615 l 3405 3464 l 3405 3464 l 3375 3584 l 3345 3464 l cp +3405 3361 m 3405 3210 l 3345 3210 l 3345 3361 l 3345 3361 l 3375 3241 l 3405 3361 l cp eoclip -n 4200 4275 m - 4200 4875 l gs col0 s gr gr +n 3375 3225 m + 3375 3600 l gs col0 s gr gr % arrowhead -n 4170 4739 m 4200 4859 l 4230 4739 l 4170 4739 l cp gs 0.00 setgray ef gr col0 s +n 3405 3361 m 3375 3241 l 3345 3361 l 3405 3361 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 3345 3464 m 3375 3584 l 3405 3464 l 3345 3464 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath -7131 4907 m 7147 4850 l 7001 4810 l 7109 4871 l 6985 4868 l cp +3344 2114 m 3346 2265 l 3406 2264 l 3404 2113 l 3404 2113 l 3376 2234 l 3344 2114 l cp eoclip -n 4950 4275 m - 7125 4875 l gs col0 s gr gr +n 3373 1950 m + 3376 2250 l gs col0 s gr gr % arrowhead -n 6985 4868 m 7109 4871 l 7001 4810 l 6985 4868 l cp gs 0.00 setgray ef gr col0 s +n 3344 2114 m 3376 2234 l 3404 2113 l 3344 2114 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath -7167 4057 m 7225 4071 l 7262 3924 l 7204 4034 l 7204 3910 l cp +3345 2864 m 3345 3015 l 3405 3015 l 3405 2864 l 3405 2864 l 3375 2984 l 3345 2864 l cp +3405 2761 m 3405 2610 l 3345 2610 l 3345 2761 l 3345 2761 l 3375 2641 l 3405 2761 l cp eoclip -n 7725 1950 m - 7200 4050 l gs col0 s gr gr +n 3375 2625 m + 3375 3000 l gs col0 s gr gr % arrowhead -n 7204 3910 m 7204 4034 l 7262 3924 l 7204 3910 l cp gs 0.00 setgray ef gr col0 s +n 3405 2761 m 3375 2641 l 3345 2761 l 3405 2761 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 3345 2864 m 3375 2984 l 3405 2864 l 3345 2864 l cp gs 0.00 setgray ef gr col0 s % Polyline -n 4350 3075 m - 7350 1950 l gs col0 s gr +n 2175 3600 m + 3750 3600 l gs col0 s gr % Polyline gs clippath -7170 4890 m 7230 4890 l 7230 4739 l 7200 4859 l 7170 4739 l cp +2611 2445 m 2460 2445 l 2460 2505 l 2611 2505 l 2611 2505 l 2491 2475 l 2611 2445 l cp eoclip -n 7200 4275 m - 7200 4875 l gs col0 s gr gr +n 3075 2475 m + 2475 2475 l gs col0 s gr gr % arrowhead -n 7170 4739 m 7200 4859 l 7230 4739 l 7170 4739 l cp gs 0.00 setgray ef gr col0 s +n 2611 2445 m 2491 2475 l 2611 2505 l 2611 2445 l cp gs 0.00 setgray ef gr col0 s % Polyline -n 3075 1875 m - 3975 1875 l gs col0 s gr +gs clippath +3345 1289 m 3347 1440 l 3407 1439 l 3405 1288 l 3405 1288 l 3377 1409 l 3345 1289 l cp +eoclip +n 3374 1125 m + 3377 1425 l gs col0 s gr gr + +% arrowhead +n 3345 1289 m 3377 1409 l 3405 1288 l 3345 1289 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath -5520 4065 m 5580 4065 l 5580 3914 l 5550 4034 l 5520 3914 l cp -5580 3660 m 5520 3660 l 5520 3811 l 5550 3691 l 5580 3811 l cp +1711 945 m 1560 945 l 1560 1005 l 1711 1005 l 1711 1005 l 1591 975 l 1711 945 l cp eoclip -n 5550 3675 m - 5550 4050 l gs col0 s gr gr +n 3075 975 m + 1575 975 l gs col0 s gr gr % arrowhead -n 5580 3811 m 5550 3691 l 5520 3811 l 5580 3811 l cp gs 0.00 setgray ef gr col0 s +n 1711 945 m 1591 975 l 1711 1005 l 1711 945 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +2161 1695 m 2010 1695 l 2010 1755 l 2161 1755 l 2161 1755 l 2041 1725 l 2161 1695 l cp +eoclip +n 3075 1725 m + 2025 1725 l gs col0 s gr gr + % arrowhead -n 5520 3914 m 5550 4034 l 5580 3914 l 5520 3914 l cp gs 0.00 setgray ef gr col0 s +n 2161 1695 m 2041 1725 l 2161 1755 l 2161 1695 l cp gs 0.00 setgray ef gr col0 s % Polyline -n 4575 4050 m - 6450 4050 l gs col0 s gr +n 8025 5925 m 8250 5925 l 9000 4950 l + 9150 4950 l gs col0 s gr % Polyline gs clippath -3495 2265 m 3555 2265 l 3555 2114 l 3525 2234 l 3495 2114 l cp -3555 1860 m 3495 1860 l 3495 2011 l 3525 1891 l 3555 2011 l cp +8312 4025 m 8275 3878 l 8217 3892 l 8254 4039 l 8254 4039 l 8254 3916 l 8312 4025 l cp eoclip -n 3525 1875 m - 3525 2250 l gs col0 s gr gr +n 8625 5400 m + 8250 3900 l gs col0 s gr gr % arrowhead -n 3555 2011 m 3525 1891 l 3495 2011 l 3555 2011 l cp gs 0.00 setgray ef gr col0 s +n 8312 4025 m 8254 3916 l 8254 4039 l 8312 4025 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +4700 7888 m 4553 7924 l 4567 7982 l 4714 7946 l 4714 7946 l 4591 7946 l 4700 7888 l cp +eoclip +n 7050 7350 m + 4575 7950 l gs col0 s gr gr + % arrowhead -n 3495 2114 m 3525 2234 l 3555 2114 l 3495 2114 l cp gs 0.00 setgray ef gr col0 s +n 4700 7888 m 4591 7946 l 4714 7946 l 4700 7888 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath -2219 3988 m 2279 3991 l 2285 3840 l 2251 3959 l 2225 3838 l cp +4170 7814 m 4170 7965 l 4230 7965 l 4230 7814 l 4230 7814 l 4200 7934 l 4170 7814 l cp eoclip -n 2325 1875 m - 2250 3975 l gs col0 s gr gr +n 4200 7500 m + 4200 7950 l gs col0 s gr gr % arrowhead -n 2225 3838 m 2251 3959 l 2285 3840 l 2225 3838 l cp gs 0.00 setgray ef gr col0 s +n 4170 7814 m 4200 7934 l 4230 7814 l 4170 7814 l cp gs 0.00 setgray ef gr col0 s % Polyline -n 7800 1275 m - 2100 1275 l gs col0 s gr -/Times-Roman-iso ff 180.00 scf sf -6600 5100 m -gs 1 -1 sc (Proof-irrelevance) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3675 4200 m -gs 1 -1 sc (Excluded-middle) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -6900 1800 m -gs 1 -1 sc (Predicate extensionality) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3375 3525 m -gs 1 -1 sc (\(Diaconescu\)) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -4650 3600 m -gs 1 -1 sc (Propositional degeneracy) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3825 1800 m -gs 1 -1 sc (Relational choice axiom) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -1725 1800 m -gs 1 -1 sc (Description principle) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -2550 2400 m -gs 1 -1 sc (Functional choice axiom) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3600 5100 m -gs 1 -1 sc (Decidability of equality on $A$) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -4425 4575 m -gs 1 -1 sc (\(needs Prop-impredicativity\)) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -5025 4725 m -gs 1 -1 sc (\(Berardi\)) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -1500 3075 m -gs 1 -1 sc (\(if Set impredicative\)) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -1500 4200 m -gs 1 -1 sc (Not excluded-middle) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3600 6000 m -gs 1 -1 sc (Axiom K on A) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3600 7200 m -gs 1 -1 sc (Invariance by substitution of reflexivity proofs for equality on A) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -6150 4200 m -gs 1 -1 sc (Propositional extensionality) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -2100 1200 m -gs 1 -1 sc (The dependency graph of axioms in the Calculus of Inductive Constructions) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3600 6900 m -gs 1 -1 sc (Injectivity of equality on sigma-types on A) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3600 6300 m -gs 1 -1 sc (Uniqueness of reflexivity proofs for equality on A) col0 sh gr -/Times-Roman-iso ff 180.00 scf sf -3600 6600 m -gs 1 -1 sc (Uniqueness of equality proofs on A) col0 sh gr +gs clippath +1295 3398 m 1339 3543 l 1397 3526 l 1353 3381 l 1353 3381 l 1359 3505 l 1295 3398 l cp +1207 2893 m 1163 2748 l 1105 2765 l 1149 2910 l 1149 2910 l 1144 2787 l 1207 2893 l cp +eoclip +n 1139 2771 m + 1364 3521 l gs col0 s gr gr + +% arrowhead +n 1207 2893 m 1144 2787 l 1149 2910 l 1207 2893 l cp gs 0.00 setgray ef gr col0 s +% arrowhead +n 1295 3398 m 1359 3505 l 1353 3381 l 1295 3398 l cp gs 0.00 setgray ef gr col0 s +% Polyline +n 4425 4875 m + 7350 3825 l gs col0 s gr +% Polyline +gs clippath +1019 1289 m 1021 1440 l 1081 1439 l 1079 1288 l 1079 1288 l 1051 1409 l 1019 1289 l cp +eoclip +n 1048 1125 m + 1051 1425 l gs col0 s gr gr + +% arrowhead +n 1019 1289 m 1051 1409 l 1079 1288 l 1019 1289 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +1020 2114 m 1022 2265 l 1082 2264 l 1080 2113 l 1080 2113 l 1052 2234 l 1020 2114 l cp +eoclip +n 1049 1950 m + 1052 2250 l gs col0 s gr gr + +% arrowhead +n 1020 2114 m 1052 2234 l 1080 2113 l 1020 2114 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +2104 5879 m 2151 6023 l 2208 6005 l 2161 5861 l 2161 5861 l 2170 5985 l 2104 5879 l cp +eoclip +n 1500 3900 m + 2175 6000 l gs col0 s gr gr + +% arrowhead +n 2104 5879 m 2170 5985 l 2161 5861 l 2104 5879 l cp gs 0.00 setgray ef gr col0 s +% Polyline +n 4575 6000 m + 6450 6000 l gs col0 s gr +% Polyline +gs clippath +6900 7063 m 7043 7113 l 7063 7056 l 6920 7006 l 6920 7006 l 7024 7075 l 6900 7063 l cp +eoclip +n 4714 6255 m + 7039 7080 l gs col0 s gr gr + +% arrowhead +n 6900 7063 m 7024 7075 l 6920 7006 l 6900 7063 l cp gs 0.00 setgray ef gr col0 s +% Polyline +gs clippath +4170 7064 m 4170 7215 l 4230 7215 l 4230 7064 l 4230 7064 l 4200 7184 l 4170 7064 l cp +eoclip +n 4200 6225 m + 4200 7200 l gs col-1 s gr gr + +% arrowhead +n 4170 7064 m 4200 7184 l 4230 7064 l 4170 7064 l cp gs 0.00 setgray ef gr col-1 s +% Polyline +2 slj +n 6450 7050 m 6448 7050 l 6444 7049 l 6437 7048 l 6425 7046 l 6408 7044 l + 6385 7040 l 6356 7036 l 6320 7030 l 6279 7024 l 6231 7017 l + 6177 7008 l 6118 6999 l 6054 6990 l 5986 6979 l 5915 6969 l + 5841 6958 l 5766 6946 l 5690 6935 l 5614 6924 l 5539 6913 l + 5464 6902 l 5391 6891 l 5320 6881 l 5252 6871 l 5185 6861 l + 5122 6852 l 5061 6843 l 5002 6835 l 4947 6827 l 4894 6820 l + 4843 6813 l 4796 6807 l 4750 6801 l 4707 6796 l 4666 6791 l + 4627 6786 l 4590 6782 l 4555 6778 l 4521 6774 l 4489 6771 l + 4458 6768 l 4429 6765 l 4400 6763 l 4350 6759 l 4303 6755 l + 4258 6753 l 4216 6751 l 4176 6751 l 4138 6750 l 4102 6751 l + 4068 6752 l 4037 6754 l 4008 6757 l 3980 6760 l 3955 6764 l + 3933 6768 l 3912 6773 l 3894 6778 l 3877 6784 l 3863 6790 l + 3850 6796 l 3839 6803 l 3829 6810 l 3820 6816 l 3813 6823 l + 3806 6830 l 3800 6838 l 3791 6850 l 3783 6863 l 3776 6878 l + 3771 6894 l 3766 6912 l 3762 6932 l 3759 6954 l 3756 6977 l + 3753 7000 l 3752 7021 l 3751 7036 l 3750 7045 l 3750 7049 l + + 3750 7050 l gs col0 s gr % here ends figure; -$F2psEnd -rs +pagefooter showpage +%%Trailer +%EOF diff --git a/doc/faq/axioms.eps_t b/doc/faq/axioms.eps_t new file mode 100644 index 0000000000..38f1a3fed4 --- /dev/null +++ b/doc/faq/axioms.eps_t @@ -0,0 +1,43 @@ +\begin{picture}(0,0)% +\includegraphics{axioms.eps}% +\end{picture}% +\setlength{\unitlength}{3947sp}% +% +\begingroup\makeatletter\ifx\SetFigFont\undefined% +\gdef\SetFigFont#1#2#3#4#5{% + \reset@font\fontsize{#1}{#2pt}% + \fontfamily{#3}\fontseries{#4}\fontshape{#5}% + \selectfont}% +\fi\endgroup% +\begin{picture}(10779,8553)(436,-8605) +\put(3676,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Excluded-middle}}}} +\put(451,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Operator iota}}}} +\put(3151,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive indefinite description}}}} +\put(3151,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}} +\put(451,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive definite descr.}}}} +\put(451,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}} +\put(3826,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Relational choice axiom}}}} +\put(6901,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Predicate extensionality}}}} +\put(1276,-4186){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(if Set impredicative)}}}} +\put(3751,-4411){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Diaconescu)}}}} +\put(4951,-4711){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional degeneracy}}}} +\put(6151,-5311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional extensionality}}}} +\put(4951,-5686){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(needs Prop-impredicativity)}}}} +\put(6001,-5911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Berardi)}}}} +\put(1576,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Not excluded-middle}}}} +\put(3376,-6586){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Decidability of equality on any A}}}} +\put(3601,-7336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Axiom K on A}}}} +\put(3601,-7636){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of reflexivity proofs for equality on A}}}} +\put(3601,-7936){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of equality proofs on A}}}} +\put(3601,-8536){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Invariance by substitution of reflexivity proofs for equality on A}}}} +\put(9001,-4336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional extensionality}}}} +\put(3601,-8236){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Injectivity of equality on Sigma-types on A}}}} +\put(6451,-6436){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Proof-irrelevance}}}} +\put(3151,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Operator epsilon}}}} +\put(3151,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}} +\put(3151,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}indefinite description}}}} +\put(3151,-2311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional choice axiom}}}} +\put(451,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}} +\put(451,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}definite description}}}} +\put(451,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Axiom of unique choice}}}} +\end{picture}% diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig index 78e448865f..9631785030 100644 --- a/doc/faq/axioms.fig +++ b/doc/faq/axioms.fig @@ -1,4 +1,4 @@ -#FIG 3.2 +#FIG 3.2 Produced by xfig version 3.2.5c Landscape Center Inches @@ -27,14 +27,6 @@ Single 1 1 1.00 60.00 120.00 5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 6309.515 5767.724 4200 3825 3450 5550 3825 7200 1 1 1.00 60.00 120.00 -6 2025 300 7725 525 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 7725 525 2025 525 -4 0 0 50 -1 0 12 0.0000 4 180 5700 2025 450 The dependency graph of axioms in the Calculus of Inductive Constructions\001 --6 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 4200 6225 4200 7200 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 7725 3900 7200 6000 @@ -45,8 +37,6 @@ Single 1 1 1.00 60.00 120.00 1 1 1.00 60.00 120.00 5550 5625 5550 6000 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 4575 6000 6450 6000 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 1 1 1.00 60.00 120.00 1 1 1.00 60.00 120.00 @@ -66,12 +56,6 @@ Single 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 3374 1125 3377 1425 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 1049 1950 1052 2250 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 1048 1125 1051 1425 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 3075 975 1575 975 @@ -89,49 +73,59 @@ Single 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 4200 7500 4200 7950 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 + 1 1 1.00 60.00 120.00 + 1 1 1.00 60.00 120.00 + 1139 2771 1364 3521 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 + 4425 4875 7350 3825 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 - 4714 6255 7039 7080 + 1048 1125 1051 1425 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 1049 1950 1052 2250 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 1500 3900 2175 6000 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 + 4575 6000 6450 6000 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 + 4714 6255 7039 7080 +2 1 0 1 -1 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 - 1139 2771 1364 3521 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 4425 4875 7350 3825 + 4200 6225 4200 7200 3 0 0 1 0 7 50 -1 -1 0.000 0 0 0 4 6450 7050 4050 6675 3750 6825 3750 7050 0.000 1.000 1.000 0.000 -4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 3750 Predicate extensionality\001 -4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 3750 Relational choice axiom\001 -4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 6150 Propositional extensionality\001 -4 0 0 50 -1 0 12 0.0000 4 180 1005 450 1050 Operator iota\001 -4 0 0 50 -1 2 12 0.0000 4 135 1020 450 1650 Constructive\001 -4 0 0 50 -1 2 12 0.0000 4 180 1530 450 1875 definite description\001 -4 0 0 50 -1 2 12 0.0000 4 180 2010 9000 5175 Functional extensionality\001 -4 0 0 50 -1 0 12 0.0000 4 180 4740 150 10050 Statements in boldface are the most "interesting" ones for Coq\001 -4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 8475 Uniqueness of reflexivity proofs for equality on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 8775 Uniqueness of equality proofs on A\001 -4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 8175 Axiom K on A\001 -4 0 0 50 -1 2 12 0.0000 4 135 1455 6450 7275 Proof-irrelevance\001 -4 0 0 50 -1 2 12 0.0000 4 180 3360 3600 9075 Injectivity of equality on Sigma-types on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 2175 4950 6525 (needs Prop-impredicativity)\001 -4 0 0 50 -1 0 12 0.0000 4 180 705 6000 6750 (Berardi)\001 -4 0 0 50 -1 2 12 0.0000 4 135 1290 3675 6225 Excluded-middle\001 -4 0 0 50 -1 0 12 0.0000 4 180 1905 4950 5550 Propositional degeneracy\001 -4 0 0 50 -1 0 12 0.0000 4 180 1050 3750 5250 (Diaconescu)\001 -4 0 0 50 -1 0 12 0.0000 4 180 2475 3375 7425 Decidability of equality on any A\001 -4 0 0 50 -1 0 12 0.0000 4 180 1620 1275 5025 (if Set impredicative)\001 -4 0 0 50 -1 0 12 0.0000 4 135 1560 1575 6225 Not excluded-middle\001 -4 0 0 50 -1 0 12 0.0000 4 180 1770 450 2625 in propositional context\001 -4 0 0 50 -1 2 12 0.0000 4 135 1020 3150 1650 Constructive\001 -4 0 0 50 -1 2 12 0.0000 4 180 1665 3150 1875 indefinite description\001 -4 0 0 50 -1 0 12 0.0000 4 180 2610 3150 2400 Constructive indefinite description\001 -4 0 0 50 -1 0 12 0.0000 4 180 1770 3150 2625 in propositional context\001 -4 0 0 50 -1 2 12 0.0000 4 135 1935 3150 3150 Functional choice axiom\001 -4 0 0 50 -1 0 12 0.0000 4 135 2100 450 2400 Constructive definite descr.\001 -4 0 0 50 -1 2 12 0.0000 4 180 1845 450 3750 Axiom of unique choice\001 -4 0 0 50 -1 2 12 0.0000 4 180 1365 3150 1050 Operator epsilon\001 +4 0 -1 50 -1 2 12 0.0000 2 135 1440 3675 6225 Excluded-middle\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1065 450 1050 Operator iota\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2850 3150 2400 Constructive indefinite description\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1965 3150 2625 in propositional context\001 +4 0 -1 50 -1 0 12 0.0000 2 135 2235 450 2400 Constructive definite descr.\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1965 450 2625 in propositional context\001 +4 0 -1 50 -1 0 12 0.0000 2 135 1995 3825 3750 Relational choice axiom\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1965 6900 3750 Predicate extensionality\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1710 1275 5025 (if Set impredicative)\001 +4 0 -1 50 -1 0 12 0.0000 2 165 1065 3750 5250 (Diaconescu)\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2070 4950 5550 Propositional degeneracy\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2310 6150 6150 Propositional extensionality\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2325 4950 6525 (needs Prop-impredicativity)\001 +4 0 -1 50 -1 0 12 0.0000 2 165 720 6000 6750 (Berardi)\001 +4 0 -1 50 -1 0 12 0.0000 2 135 1725 1575 6225 Not excluded-middle\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2730 3375 7425 Decidability of equality on any A\001 +4 0 -1 50 -1 0 12 0.0000 2 135 1170 3600 8175 Axiom K on A\001 +4 0 -1 50 -1 0 12 0.0000 2 180 4035 3600 8475 Uniqueness of reflexivity proofs for equality on A\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2865 3600 8775 Uniqueness of equality proofs on A\001 +4 0 -1 50 -1 0 12 0.0000 2 180 5220 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001 +4 0 -1 50 -1 2 12 0.0000 2 180 2145 9000 5175 Functional extensionality\001 +4 0 -1 50 -1 2 12 0.0000 2 180 3585 3600 9075 Injectivity of equality on Sigma-types on A\001 +4 0 -1 50 -1 2 12 0.0000 2 135 1515 6450 7275 Proof-irrelevance\001 +4 0 -1 50 -1 2 12 0.0000 2 180 1440 3150 1050 Operator epsilon\001 +4 0 -1 50 -1 2 12 0.0000 2 135 1080 3150 1650 Constructive\001 +4 0 -1 50 -1 2 12 0.0000 2 180 1785 3150 1875 indefinite description\001 +4 0 -1 50 -1 2 12 0.0000 2 135 2085 3150 3150 Functional choice axiom\001 +4 0 -1 50 -1 2 12 0.0000 2 135 1080 450 1650 Constructive\001 +4 0 -1 50 -1 2 12 0.0000 2 180 1620 450 1875 definite description\001 +4 0 -1 50 -1 2 12 0.0000 2 180 1980 450 3750 Axiom of unique choice\001 diff --git a/doc/faq/axioms.pdf b/doc/faq/axioms.pdf new file mode 100644 index 0000000000..2ba5bf85b6 Binary files /dev/null and b/doc/faq/axioms.pdf differ diff --git a/doc/faq/axioms.pdf_t b/doc/faq/axioms.pdf_t new file mode 100644 index 0000000000..06dc4b280d --- /dev/null +++ b/doc/faq/axioms.pdf_t @@ -0,0 +1,43 @@ +\begin{picture}(0,0)% +\includegraphics{axioms.pdf}% +\end{picture}% +\setlength{\unitlength}{3947sp}% +% +\begingroup\makeatletter\ifx\SetFigFont\undefined% +\gdef\SetFigFont#1#2#3#4#5{% + \reset@font\fontsize{#1}{#2pt}% + \fontfamily{#3}\fontseries{#4}\fontshape{#5}% + \selectfont}% +\fi\endgroup% +\begin{picture}(10779,8553)(436,-8605) +\put(3676,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Excluded-middle}}}} +\put(451,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Operator iota}}}} +\put(3151,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive indefinite description}}}} +\put(3151,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}} +\put(451,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive definite descr.}}}} +\put(451,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}} +\put(3826,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Relational choice axiom}}}} +\put(6901,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Predicate extensionality}}}} +\put(1276,-4186){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(if Set impredicative)}}}} +\put(3751,-4411){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Diaconescu)}}}} +\put(4951,-4711){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional degeneracy}}}} +\put(6151,-5311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional extensionality}}}} +\put(4951,-5686){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(needs Prop-impredicativity)}}}} +\put(6001,-5911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Berardi)}}}} +\put(1576,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Not excluded-middle}}}} +\put(3376,-6586){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Decidability of equality on any A}}}} +\put(3601,-7336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Axiom K on A}}}} +\put(3601,-7636){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of reflexivity proofs for equality on A}}}} +\put(3601,-7936){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of equality proofs on A}}}} +\put(3601,-8536){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Invariance by substitution of reflexivity proofs for equality on A}}}} +\put(9001,-4336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional extensionality}}}} +\put(3601,-8236){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Injectivity of equality on Sigma-types on A}}}} +\put(6451,-6436){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Proof-irrelevance}}}} +\put(3151,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Operator epsilon}}}} +\put(3151,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}} +\put(3151,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}indefinite description}}}} +\put(3151,-2311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional choice axiom}}}} +\put(451,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}} +\put(451,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}definite description}}}} +\put(451,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Axiom of unique choice}}}} +\end{picture}% diff --git a/doc/faq/axioms.png b/doc/faq/axioms.png index 2aee091660..a86eed7f12 100644 Binary files a/doc/faq/axioms.png and b/doc/faq/axioms.png differ -- cgit v1.2.3 From cf193df65c53813054239463f6496526533e9bab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 27 Jul 2015 13:54:25 +0200 Subject: Fixing bug #2169: "Print Module command shows module type expression incorrectly". --- printing/printmod.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/printing/printmod.ml b/printing/printmod.ml index 295d8aaa66..a80bbb146a 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -315,15 +315,17 @@ let rec print_typ_expr env mp locals mty = let mapp = List.tl lapp in hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++ prlist_with_sep spc (print_modpath locals) mapp ++ str")") - | MEwith(me,WithDef(idl,c))-> + | MEwith(me,WithDef(idl,(c, _)))-> let env' = None in (* TODO: build a proper environment if env <> None *) let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() - ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) - | MEwith(me,WithMod(idl,mp))-> + ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() + ++ Printer.pr_lconstr c) + | MEwith(me,WithMod(idl,mp'))-> let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ - keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc() + ++ print_modpath locals mp') let print_mod_expr env mp locals = function | MEident mp -> print_modpath locals mp -- cgit v1.2.3 From cb145fa37d463210832c437f013231c9f028e1aa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 27 Jul 2015 13:58:05 +0200 Subject: Output test for bug #2169. --- test-suite/output/PrintModule.out | 4 ++++ test-suite/output/PrintModule.v | 34 ++++++++++++++++++++++++++++++++++ 2 files changed, 38 insertions(+) create mode 100644 test-suite/output/PrintModule.out create mode 100644 test-suite/output/PrintModule.v diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out new file mode 100644 index 0000000000..db464fd07e --- /dev/null +++ b/test-suite/output/PrintModule.out @@ -0,0 +1,4 @@ +Module N : S with Definition T := nat := M + +Module N : S with Module T := K := M + diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v new file mode 100644 index 0000000000..999d9a9862 --- /dev/null +++ b/test-suite/output/PrintModule.v @@ -0,0 +1,34 @@ +Module FOO. + +Module M. + Definition T := nat. +End M. + +Module Type S. + Parameter T : Set. +End S. + +Module N : S with Definition T := nat := M. + +Print Module N. + +End FOO. + +Module BAR. + +Module K. End K. +Module Type KS. End KS. + +Module M. + Module T := K. +End M. + +Module Type S. + Declare Module T : KS. +End S. + +Module N : S with Module T := K := M. + +Print Module N. + +End BAR. -- cgit v1.2.3