aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Cases.v
Commit message (Collapse)AuthorAge
* Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| | | | | Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v).
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Clarification of the existence of three algorithms for solving unconstrained evars: - the type-class mechanism - the heuristics for solving pending conversion problems and multi-candidates - Declare Implicit Tactic (when called from tactics) Main function for solving unconstrained evars (when not using understand): Pretyping.solve_remaining_evars - Clarification of the existence of three corresponding kinds of errors when reporting about unsolved evars: Main function for checking resolution of evars independently of the understand functions: Pretyping.check_evars_are_solved - Introduction of inference flags in pretyping for governing which combination of the algorithms to use when calling some understand function; there is also a flag of expanding or not evars and for requiring or not the resolution of all evars - Less hackish way of managing Pretyping.type_constraint: all three different possibilities are now represented by three different constructors - Main semantical changes done: - solving unconstrained evars and reporting is not any longer mixed: one first tries to find unconstrained evars by any way possible; one eventually reports on the existence of unsolved evars using check_evars_are_solved - checking unsolved evars is now done by looking at the evar map, not by looking at the evars occurring in the terms to pretype; the only observed consequence so far is in Cases.v because of subterms (surprisingly) disappering after compilation of pattern-matching - the API changed, see dev/doc/changes.txt Still to do: - Find more uniform naming schemes: - for distinguishing when sigma is passed as a reference or as a value (are used: suffix _evars, prefix e_) - for distinguishing when evars are allowed to remain uninstantiated or not (are used: suffix _evars, again, suffix _tcc, infix _open_) - be more consistent on the use of names evd/sigma/evars or evdref/evars - By the way, shouldn't "understand" be better renamed into "infer" or "preinfer", or "pretype". Grammatically, "understanding a term" looks strange. - Investigate whether the inference flags in tacinterp.ml are really what we want (e.g. do we really want that heuristic remains activated when typeclasses are explicitly deactivated, idem in Tacinterp.interp_open_constr where flags are strange). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Taking into account the possibility of having a type of type which isGravatar herbelin2012-12-18
| | | | | | | | an evar in typing.ml. Thanks to HoTT people for noticing the problem. Fixed behavior of e_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the test-suite by removing any Reset in the scriptsGravatar letouzey2012-03-23
| | | | | | | | Reset and the other backtracking commands (Back, BackTo, Backtrack) are now allowed only during interactive session, not in compiled or loaded scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15087 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating Cases.v test.Gravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14700 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight change of the semantics of user-given casts: they don't reallyGravatar msozeau2008-11-07
| | | | | | | | | | | | | | | | | help the type _checking_ anymore (they don't become typing constraints) but they permit to coerce a subterm in a type. In particular, when using a VM cast we avoid unneeded, unexpected conversions using the default machine (oops!). Also remove the corresponding comment in pretyping and fix the wrong use of casts in toplevel/command: accept the trouble of using evars. This has the somewhat adverse effect that when typing casted object we now have no typing constraints (see e.g. examples in Cases.v)! Probably, this will be backtracked partially tomorrow as many contribs can rely on it and the change could make some unifications fail (in particular with deep coercions). Let's try anyway! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | du filtrage. Cela permet de détecter les cas impossibles et de simuler les contraintes d'inversion exprimables sous la forme d'un assignement des arguments du constructeurs (cf le cas de Vtail dans Bvector.v). Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi) avec vi composé uniquement de constructeurs, et que le résultat final est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on construit le prédicat Q:=fun x1 .. xn y => match x1 .. xn y with | v1(z) .. vn(z) t => P(z) | _ .. _ _ => ?evar-speciale-cas-impossible end qui vérifiera bien que Q u1 .. un = P(w1,..,wp). En raison de limitations de l'unification (on aurait besoin d'eta conversion pour résoudre des problèmes du genre "terme rigide == match x with _ => ?evar end", et besoin d'instanciation par constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"), je n'ai pas réussi à traiter le cas général. Aussi, on adopte une stratégie pragmatique consistant à tester plusieurs prédicats possibles : - si un type final est donné, on essaie d'abord l'algorithme de Matthieu et sinon le nouvel algorithme (permet par exemple de traiter certains cas d'élimination dépendante de Bvector.v), - s'il n'y a pas de type final, on essaie d'abord le nouvel algo et sinon, on essaie avec un prédicat sans dépendance (permet de traiter des cas compliqués comme celui de par cas sur I' dans le fichier Case13.v de la test-suite). Dans la pratique, il y a beaucoup de changement dans le code de compile_case. - Par exemple, la compilation est maintenant toujours appelé avec un prédicat (là où l'on pouvait avoir None, on a maintenant toujours au moins une evar). - En revanche, le membre droit des clauses est maintenant optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une branche impossible au moment du calcul du prédicat de retour. - Aussi, on renonce aux PrLetIn et PrProd dans l'expression du predicat de retour mais il faut savoir que c'est maintenant la liste des tomatchs qui spécifie le contexte exact dans lequel le prédicat de retour est bien typé. - Et d'autres... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage a un SStream predicatifGravatar herbelin2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parenthèses manquantes pour se conformer à la doc (et au nouveau ↵Gravatar herbelin2002-10-21
| | | | | | PeanoSyntax.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux exemplesGravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)Gravatar herbelin2001-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ces fichiers décrivent des comportements peut-être souhaités mais ↵Gravatar herbelin2001-09-19
| | | | | | actuellement non implantés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1996 85f007b7-540e-0410-9357-904b9bb8a0f7
* Decomposition de CasesGravatar mohring2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1651 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe zarithGravatar herbelin2001-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test syntaxe avec motifs numériquesGravatar herbelin2001-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fichier de test pour les CasesGravatar herbelin2000-12-14
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1099 85f007b7-540e-0410-9357-904b9bb8a0f7