aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2012-07-06Fixes bug #2678aspiwack
Some "dependent evars" were forgotten in the emacs mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15530 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-28Cleaning opening of the standard List module.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15500 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-25Added a .mli to pretyping/program.mlppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15490 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-21Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:msozeau
take care of checking progress when solving the remaining problems, distinguishing between solved and stuck conversions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15467 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Fixing use of an error instead of a boolean result in the unificationherbelin
subroutine choose_less_dependent_instance. This might solve bug #2495 (only "might solve" because the bug does not come with a reproducible example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15461 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
known instances in unification.ml). This refines the fix to bug #1918. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-15Reductionops abstract machine uses Zcase & Zfix stack node.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15444 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-15Reductionops : Better abstract machine stack utilitiespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15443 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-04Replacing some str with strbrkppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15418 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01More cleaningppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01Cleaning Pp.ppnl useppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-30More uniformisation in Pp.warn functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29No more Univ in grammar.cmaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in ↵letouzey
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Impossible branches inference fixup (bug 2761)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15307 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Partial revert of r15148 in order to compile with Camlp4pboutill
+ comment correction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15253 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-25Avoid unneeded head-normalizations in coercion code.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15246 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-25Do not delta-head-normalize the proposition argument of sigma types during ↵msozeau
coercion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15245 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Corrects a bug in the refine tactic which could drop evar bodies.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15205 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Adds a comment: precondition on Evd.addaspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15204 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-16Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15184 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-05Speedup free_vars_and_rels_up_alias_expansion (evarconv)gareuselesinge
Small cache to avoid checking the same Rel or Var twice. Consider an unification problem like the following one: a := huge b := F1 a + F2 a c := G1 b + G2 b =============== ?i[c,b,a] == ?g[c,c,c] The old code, as the "not optimal" comment was suggesting, did process every item in the explicit substitution, even duplicated ones, unfolding the letins over and over. This was the cause of the huge slowdown in the definition of cormen_lup in Ssreflect/theories/matrix.v, that follows: Fixpoint cormen_lup {n} := match n return let M := 'M[F]_n.+1 in M -> M * M * M with | 0 => fun A => (1, 1, A) | _.+1 => fun A => let k := odflt 0 [pick k | A k 0 != 0] in let A1 : 'M_(1 + _) := xrow 0 k A in let P1 : 'M_(1 + _) := tperm_mx 0 k in let Schur := ((A k 0)^-1 *: dlsubmx A1) *m ursubmx A1 in let: (P2, L2, U2) := cormen_lup (drsubmx A1 - Schur) in let P := block_mx 1 0 0 P2 *m P1 in let L := block_mx 1 0 ((A k 0)^-1 *: (P2 *m dlsubmx A1)) L2 in let U := block_mx (ulsubmx A1) (ursubmx A1) 0 U2 in (P, L, U) end. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15116 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-26Unification: Fixing bug in materialize_evar (spotted by MathClasses).herbelin
Also fixed apparent other bug in the presence of let-ins. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15099 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to know if it occurs in rigid position or not. Such equations typically come from matching problems such as "match a return ?T[a] with pair a1 a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified with ?A. This possible dependency is kept since commits r15060-15062. The heuristic is to restrict ?T so that the dependency is removed, leading to a behavior similar to the one existing before these commits. This allows BGsection15.v, from contrib Ssreflect, to compile as it did before these commits. Also, removed one function exported without true need in r15061. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23Little bug in r15061 leading to unusable debug mode.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15082 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
Same for check_leq instead of check_geq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-22evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structuresgareuselesinge
Canonical Structure inference works on named terms only: i.e. the projection and the value must be named (with few exceptions). The set of named (head) terms is: (Var _|Construct _|Ind _|Const _|Prod _|Sort _) The set of unnamed is thus: (Case _|Fix _|CoFix _|Evar _|Meta _|Rel _) The MaybeFlex/MaybeFlex case, when no CS inference takes place, unfolds the rhs only if it exposes a named term. If it exposes an unnamed term, it tries to unfold on the lhs first. Note that unnamed terms are whd normal terms, since iota and zeta are performed by evar_apprec. So the algorithm behaves as before, but stops unfolding the rhs 1 delta step before it exposes an unnamed term. Then it starts unfolding the lhs. If the lhs exposes a rigid term the rhs is naturally unfolded, going back to same situation in which the algorithm was ending before. But while it unfolds on the left, the rhs is still named, and canonical structure inference can succeed. Ex failing before, the "canon_" prefix marks projections/values declared as canonical. Record test := K { canon_proj : nat } (* canon_proj x := math x with K y => y end *) canon_val x := match x with 0 => 0 | S m => m end Canonical Structure canon_struct x := K (canon_val x) (* aliases *) proj := canon_proj val := canon_val Old alg: proj ? ===?=== val x proj ? ===?=== canon_val x proj ? ===?=== match x with ... end canon_proj ? ===?=== match x with ... end (* no inference *) match ? with K x...end ===?=== match x with 0 ...end (* FAIL *) New alg: proj ? ===?=== val x proj ? ===?=== canon_val x canon_proj ? ===?=== canon_val x (* inference works: ? := canon_struct *) In case canon_struct is not declared for canon_proj and canon_val it continues like that: canon_proj ? ===?=== canon_val x match ? with K x...end ===?=== canon_val x match ? with K x...end ===?=== match x with 0 ...end (* FAIL *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15077 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
by default typeclass resolution is not launched on goal evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
The optimisation done of Namegen.visibly_occur_id did not preserve the previous behavior when pr_constr/constr_extern/detype were called on a term with free rel variables. We backtrack on it to go back to the 8.2 behavior. Seized this opportunity to clarify the meaning of the at_top flag in constrextern.ml and printer.ml and to rename it into goal_concl_style. The badly-named at_top flag was introduced in Coq 6.3 in 1999 to mean that when printing variables bound in the goal, names had to avoid the names of the variables of the goal context, so as to keep naming stable when using "intro"; in r4458, printing improved by not avoiding names that were short names of global definitions, e.g. "S", or "O" (except when the at_top flag was on for compatibility reasons). Other printing strategies could be possible in the non-goal-concl-style mode. For instance, all bound variables could be made distinct in a given expression, even if no clash occur, therefore following so-called Barendregt's convention. This could be done by setting "avoid" to "ids_of_rel_context (rel_context env)" in extern_constr and extern_type (and then, Namegen.visibly_occur_id could be re-simplified again!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15067 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Use a careful analysis of dependencies in restricting instances toherbelin
solve the following kind of code broken by being less restrictive on projecting: Set Printing Existential Instances. Parameter f : forall x, x=0 -> x=0 -> x=1 /\ x=2. Parameter g : forall y, y=0 /\ y=0. Check match g _ with conj a b => f _ a b end. (* and the return clause should not depend on the "_" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15064 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep aherbelin
candidate for the possible projection (as was introduced in 8.4beta) but try also to imitate (as was done before 8.4beta but not done in 8.4beta). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15062 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Generalized the use of evar candidates in type inference unification:herbelin
- use evar candidates instead of postponed conversion problems when it is known (according to the projection heuristic used) that an evar has only a fixed number of possible instances (as e.g. in equation ?n[x,x] = x, with x a variable); - this allows to be more robust in solving remaining problems: if several instanciations exist, and one is not compatible with a previous instantiation made among several choices for another evar, backtracking is now possible; - this allows in particular to fix regression #2670 (two postponed conversion problems solved in an inconsistent way); - but this requires more code. At the same time, a refactoring of the code has been made so as to hopefully clarify the elementary pieces of the algorithm. For instance, there are now generic functions for both applying a filter and giving candidates. The filter is systematically generalized so as to have the ccl of the evar well-typed even in situations where we could try on the contrary to restrict the evars occurring in the ccl. Anyway, when the representation of instances will be optimized using identity substitutions, it will no longer be useful to use the filter to shorten the size of the instances. Then, the filters will have, like candidates, the only role of restricting the search space for potential solutions to the unification problems. Also, solve_refl can now be used to restrict equations ?x[t1..tn]=?x[u1..un] up to conversion instead of up to unification. This (potententially) looses constraints but this avoids looping at the time of considering remaining problems and applying heuristics to them. Also added printing of evar candidates in debugging evar printers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15061 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Reorganizing the structure of evarutil.ml (only restructuration, noherbelin
change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-19More adaptations of pretyping/coercion to Program mode.msozeau
- (Regular) Casts become typing constraints again. - Coerce tycon to inductive type when applying bidirectional typechecking hint. - Coerce lambda expressions to tycon, might require coercions now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15058 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-19Fix bugs related to Program integration.msozeau
- reinstall (x : T | P) binder syntax extension. - fix a wrong Evd.define in coercion code. - Simplify interface of eterm_obligations to take a single evar_map. - Fix a slightly subtle bug related to resolvability of evars: some were marked unresolvable and never set back to resolvable across calls to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-19Fixes bug: #2692 (Arguments/simpl off by 1)gareuselesinge
simpl was accessing the reduction stack at position n when the length of the stack was exactly n. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15049 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-19Arguments/simpl: allow ! even on non fixpointsgareuselesinge
It is now possible to tell simpl to unfold a constant that hides no "match" but is applied to concrete arguments. Arguments id _ !n. Goal forall x, id x = id 2. intros; simpl. x : nat ======== id x = 2 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15048 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Fix merge and add missing file.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15040 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Revise API of understand_ltac to be parameterized by a flag for resolution ↵msozeau
of evars. Used when interpreting a constr in Ltac: resolution is now launched if the constr is casted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Merge fixesmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15037 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Everything compiles again.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Second step of integration of Program:msozeau
- Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 20:10:58 +0000