Commits on May 4, 2016
  1. Fix Haskell extraction for terms over 45 characters long

    The Haskell extraction code would allow line-wrapping of the Haskell
    type definition, which would lead to unparseable Haskell code when the
    linebreak occured just before the type name.  In particular, with a term
    name of 46 characters or more, the following Coq code:
      Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt.
      Extraction Language Haskell.
      Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.
    would produce:
      xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx ::
      xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx =
    which failed to compile with GHC (according to Haskell's indentation
    rules, the "Unit" line must be indented to be treated as a continuation
    of the previous line).
    This patch always forces the type onto a separate line, and ensures that
    it is always indented by 2 spaces (just like the body of each definition).
    zeldovich committed with letouzey Feb 8, 2016
Commits on Mar 14, 2016
  1. Disable warning 31 when generating coqtop from coqmktop.

    This is a backport of ffc1353 to fix compilation of Coq 8.4 with
    OCaml 4.03 beta 1.
    maximedenes committed Mar 14, 2016
Commits on Feb 16, 2016
  1. Warn when including functors with restricted signature (fix for #3746).

     Indeed, this kind of include may lead to the creation of axioms.
     For compatibility, we only put a warning here, instead of a error in 8.5.
     Behave: this test below is partial, since [mod_type_alg] isn't always
     properly filled (but changing that would have impact on extracted code).
    letouzey committed Dec 23, 2015
Commits on Jan 13, 2016
  1. v8.4: Fix for #4467 (missing shadowing of variables in cases pattern).

    Backported from trunk, including a weak form of the fix for buggy test
    Topconstr.is_constructor (weak form because too complicated to manage
    a dependency of Topconstr into Syntax_def).
    herbelin committed Jan 13, 2016
Commits on Dec 16, 2015
  1. Extraction: slightly better heuristic for Obj.magic simplifications

     On an application (f args) where the head is magic, we first remove Obj.magic
     on arguments before continuing with simplifications (that may push magic down
     inside the arguments).
     For instance, starting with ((Obj.magic f) (Obj.magic (g h))), we now end
     with ((Obj.magic f) (g h)) instead of ((Obj.magic f) ((Obj.magic g) h))) as
    letouzey committed Dec 16, 2015
  2. Extraction: fixed beta-red with Obj.magic (#2795 again) + other simpl…

     Unfortunately, my first attempt at replacing (Obj.magic (fun x -> u) v)
     by ((fun x -> Obj.magic u) v) was badly typed, as seen in FingerTree:
     the argument v should also be magic now, otherwise it might not have
     the same type as x.
     This optimization is now correctly done, and to mitigate the potential inflation
     of Obj.magic, I've added a few simplification rules to avoid redundant magics,
     push them down inside terms, favor the form (Obj.magic f x y z), etc.
    letouzey committed Dec 15, 2015
Commits on Dec 15, 2015
  1. Extraction: replace unused variable names by _ in funs and matchs (fi…

    …x #2842)
     This is done via a unique pass which seems roughly linear in practice,
     even on big developments like CompCert. There's a List.nth in an env at
     each MLrel, that could be made logarithmic if necessary via Okasaki's
     skew list for instance.
     Another approach would be to keep names (as a form of documentation), but
     prefix them by _ to please OCaml's warnings. For now, let's be radical and
     use the _ pattern.
    letouzey committed Dec 15, 2015
Commits on Dec 14, 2015
  1. Extraction: allow basic beta-reduction even through a MLmagic (fix #2…

     This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have
     to properly investigate the interaction between all the other optimizations
     and MLmagic. But well, at least this precise bug is fixed now.
    letouzey committed Dec 14, 2015
  2. Extraction: fix a pretty-print issue

     Some explicit '\n' in Pp.str were interacting badly with Format boxes
     in Compcert, leading to right-flushed "sig..end" blocks in some .mli
    letouzey committed Dec 14, 2015
  3. Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)

     The ind_equiv field wasn't correctly set, due to some kernel names
     glitches (canonical vs. user). The fix is to take into account the
     delta_resolver while traversing module structures.
    letouzey committed Dec 14, 2015
Commits on Nov 22, 2015
Commits on Nov 16, 2015
  1. v8.4: Reverting "compare stacks head first!" which is breaking the

    compilation. Bruno is obviously unresponsive about it.
    This reverts commit bd3cc60.
    herbelin committed Nov 16, 2015
Commits on Nov 7, 2015
Commits on Oct 26, 2015
Commits on Oct 24, 2015
  1. v8.4: Fixing a loop in checking hints with holes.

    For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc46).
    herbelin committed Oct 24, 2015
Commits on Oct 15, 2015
  1. compare stacks head first!

    barras committed Oct 15, 2015
Commits on Oct 14, 2015
  1. minor update of checker/include

    barras committed Oct 14, 2015
  2. Remove dead code in lazy reduction machine.

    maximedenes committed with barras Sep 13, 2015
Commits on Sep 9, 2015
  1. Backport fix for bug 4294

    ... on modules and "with" dropping universe constraints.
    mattam82 committed Sep 9, 2015
  2. Fix a bug in 31 bit arithmetic, leading to failing conversion tests.

    On 64 bits architectures, integers could have some of their 32 msb set to 1
    internally in the VM. When read back to a Coq term, this was not observable. But
    an equality test would fail. From the user point of view, the symptom was that
    vm_compute; reflexivity would succeed but the subsequent Qed would fail.
    Bug reported by Tahina Ramananandro.
    maximedenes committed Sep 6, 2015
  3. Fixed critical bug in 31 bit arithmetic of VM

    ADDMULDIVINT31 was missing pops in some cases
    catalin-hritcu committed with maximedenes Sep 6, 2015
Commits on Jul 28, 2015
  1. v8.4: Fixing bug #4289 (hash-consing only user part of constant not

    compatible with a unique bound module name counter which is not
    synchronous with the backtracking).
    herbelin committed Jul 28, 2015
Commits on Jul 16, 2015
  1. Fixing #4177 (find_projectable was liable to ask to instantiate an ev…

    …ar twice).
    Backport from v8.5 (which trunk follows).
    herbelin committed Jul 16, 2015
Commits on Jun 23, 2015
  1. Define Any in Haskell extraction when Tunknown is used.

    Commit 84c2433 introduced the Any type alias as the Haskell extracted
    version of MiniML's Tunknown.  However, the code to define the Any
    type alias was generated conditional on usf.magic.  As it turns out,
    sometimes Tunknown appears even if usf.magic is false (i.e., even if
    MLmagic does not appear anywhere in the AST).  This produced Haskell
    code that would not compile; e.g.:
      % coqtop
      Coq < Extraction Language Haskell.
      Coq < Extraction Library Datatypes.
      The file Datatypes.hs has been created by extraction.
      % ghc Datatypes.hs
      [1 of 1] Compiling Datatypes        ( Datatypes.hs, Datatypes.o )
      Datatypes.hs:261:17: Not in scope: type constructor or class `Any'
      Datatypes.hs:261:24: Not in scope: type constructor or class `Any'
    The fix is straightforward: produce the code that defines the Any type
    alias if usf.tunknown is true.
    zeldovich committed with letouzey Mar 28, 2015
  2. Do not revert parameter lists when extracting singleton types to Hask…

    …ell. (Fix for bugs #3470 and #3694)
    silene committed with letouzey Mar 21, 2015