aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
AgeCommit message (Collapse)Author
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
The removed code isn't used locally and isn't exported in the signature
2014-02-28Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an ↵Pierre Boutillier
infinite loop.
2014-02-28Dead code elimionation in reductionopsPierre Boutillier
2014-02-24Ensuring that the module Stack is opaque inside Reductionops.Pierre-Marie Pédrot
2014-02-24cbn understands ArgumentsPierre Boutillier
(excepts list of args that must be constructors
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
syntax mentionning simpl remains
2014-02-24No more translation array <-> list in Reductionops.StackPierre Boutillier
2014-02-24Reductionops.Stack.strip* are ready to deal with ShiftPierre Boutillier
2014-02-24Reductionops.Stack.app_node is secretPierre Boutillier
2014-02-24app_node, stack, state printersPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2013-11-08Removing partial applications in Reductionops.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17071 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-05Preventing useless allocations in Reductionops.instance.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17063 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
But for vm, the kernel should be functional now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29[Reductionops.append_stack_app]: do not allocate a useless array.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16952 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Various optimizations in Constr, such as term sharing and allocationppedrot
avoiding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16911 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Removing association lists in Reductionops. Btw, defining the dual of theppedrot
domain operation on maps. The efficiency should just be improved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16737 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-19- Fix uncaught exception NotASort from reductionops, moving decomp_sort to ↵msozeau
retyping.ml - In unification's w_merge, assign the evars in the same order they were found. Might create rare incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16632 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Fix bug #2989: make unification.ml able to deal with canonical structure in ↵pboutill
any context + reindenting noise git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16354 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-23Minor code cleaning in CArray / CList.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-14Typo in an error messageletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16303 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05More monomorphization.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-28compare_stack_shape before ise_stack2 in evar_convpboutill
+ revert r16130 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16258 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-25Evarconv: When doing a iota of a fixpoint, use constant name instead of ↵pboutill
fixpoint definition + Help the use of #trace on evar_conv_appr_x git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Dir_path --> DirPathletouzey
Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Added backtrace information to anomaliesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16161 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-24Reductionops: whd_state_gen can take and answers a cst_stack toopboutill
+ cst_stack is kept en a meta/evar is "unfold". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16142 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-21Awful heuristic to refold mutual fixpoint in reductionopspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16110 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-21Fixup and comment reductionopspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16109 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Reductionops reduction machine can refold constantpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16107 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-28Reductionops uses Closure.redspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16009 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-22Monomorphization (pretyping)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-25Fix eta contraction in Reductionopspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15650 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-20Reductionops refactoringpboutill
Semantic changes are : - whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack didn't. - Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and cofix. - simpl uses its own whd_ function that do not touch at matched term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15634 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12tacred uses stack_reduction_function instead of state_reduction_functionpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15614 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 10:15:07 +0000