Compatibility with 8.11

.circleci/config.yml

@@ -107,6 +107,12 @@ workflows:
   version: 2
   build:
     jobs:
+      - opam:
+          name: OPAM 8.11
+          coq: 8.11-ocaml-4.09-flambda
+      - dune:
+          name: Dune 8.11
+          coq: 8.11-ocaml-4.09-flambda
       - opam:
           name: OPAM 8.12
           coq: 8.12-ocaml-4.09-flambda

compat.pl

@@ -15,54 +15,92 @@
 my $coq_version = `coqc -print-version`;
 $coq_version =~ s/([\d.]+).*/$1/;
 
-if ($coq_version lt '8.12' || '8.14' le $coq_version) {
+if ($coq_version lt '8.11' || '8.14' le $coq_version) {
   print STDERR "Warning: This version of Coq is not supported: $coq_version";
-  print STDERR "Currently supported versions of Coq: 8.13, 8.12.\n"
+  print STDERR "Currently supported versions of Coq: 8.13, 8.12, 8.11.\n"
 }
 
 sub writefile {
   my ($filename, $contents) = @_;
   open(my $file, '>', $filename);
+  print $file "(* THIS FILE IS GENERATED BY compat.pl *)\n";
   print $file $contents;
   close $file;
 }
 
 # Generate file plugin/compat.ml
 sub compat_ml {
+  my $compat_ml;
 
-  my $compat_ml = '(* THIS FILE IS GENERATED BY compat.pl *)
-let number (x : NumTok.Signed.t) : Constrexpr.prim_token = Constrexpr.Number x
-let from_Number : Constrexpr.prim_token -> NumTok.Signed.t option = function
-  | Constrexpr.Number x -> Some x
+  if ('8.12' le $coq_version) {
+    my $Number = ('8.13' le $coq_version) ? 'Constrexpr.Number' : 'Constrexpr.Numeral';
+
+    $compat_ml = "
+let number (n : int) : Constrexpr.prim_token = $Number (NumTok.Signed.of_int_string (string_of_int n))
+
+let from_nonnegative_Number : Constrexpr.prim_token -> int option = function
+  | $Number (NumTok.SPlus, i) ->
+    (match NumTok.Unsigned.to_nat i with
+    | Some n -> Some (int_of_string n)
+    | None -> None)
+  | _ -> None
+
+let max_implicit = Glob_term.MaxImplicit
+
+let from_CNotation = function
+  | Constrexpr.CNotation (_, _, cns) -> Some cns
+  | _ -> None
+
+let extern_constr_ e evd evar = Constrextern.extern_constr e evd (EConstr.mkEvar (evar, []))
+";
+
+  } else {
+
+    $compat_ml = '
+let number (n : int) : Constrexpr.prim_token =
+  if n >= 0 then Constrexpr.Numeral (Constrexpr.SPlus, NumTok.int (string_of_int n))
+  else Constrexpr.Numeral (Constrexpr.SMinus, NumTok.int (string_of_int (-n)))
+
+let from_nonnegative_Number : Constrexpr.prim_token -> int option = function
+  | Constrexpr.Numeral (Constrexpr.SPlus, NumTok.{int=n;frac="";exp=""}) ->
+    Some (int_of_string n)
   | _ -> None
+
+let max_implicit = Glob_term.Implicit
+
+let from_CNotation = function
+  | Constrexpr.CNotation (_, cns) -> Some cns
+  | _ -> None
+
+let extern_constr_ e evd evar = Constrextern.extern_constr false e evd (EConstr.mkEvar (evar, [||]))
 ';
 
-  # Since 8.13: Constrexpr.Number
-  # Before:     Constrexpr.Numeral
-  if ($coq_version lt '8.13') {
-    $compat_ml =~ s/Constrexpr\.Number/Constrexpr.Numeral/g;
   }
 
   return $compat_ml;
 }
 
 # Generate file src/ExtractionQCCompat.ml
 sub extractionqccompat_v {
+  # Hexadecimal.int and Numeral.int don't exist before 8.11
+  if ($coq_version lt '8.12') {
+    return '';
+  }
 
-  my $extractionqccompat_v = '(* THIS FILE IS GENERATED BY compat.pl *)
-From Coq Require Import Extraction.
+  my $Number_int = ('8.13' le $coq_version) ? 'Number.int' : 'Numeral.int';
 
-Extract Inductive Number.int => "((Obj.t -> Obj.t) -> (Obj.t -> Obj.t) -> Obj.t) (* __int *)"
-  [ "(fun x dec _ -> dec (Obj.magic x))"
-    "(fun y _ hex -> hex (Obj.magic y))"
-  ] "(fun i dec hex -> Obj.magic i dec hex)".
-';
+  my $extractionqccompat_v = "
+From Coq Require Import Extraction.
 
-  # Since 8.13: Number.int
-  # Before:     Numeral.int
-  if ($coq_version lt '8.13') {
-    $extractionqccompat_v =~ s/Number\.int/Numeral.int/g;
-  }
+Extract Inductive Hexadecimal.int => \"((Obj.t -> Obj.t) -> (Obj.t -> Obj.t) -> Obj.t) (* Hexadecimal.int *)\"
+  [ \"(fun x pos _ -> pos (Obj.magic x))\"
+    \"(fun y _ neg -> neg (Obj.magic y))\"
+  ] \"(fun i pos neg -> Obj.magic i pos neg)\".
+Extract Inductive $Number_int => \"((Obj.t -> Obj.t) -> (Obj.t -> Obj.t) -> Obj.t) (* $Number_int *)\"
+  [ \"(fun x dec _ -> dec (Obj.magic x))\"
+    \"(fun y _ hex -> hex (Obj.magic y))\"
+  ] \"(fun i dec hex -> Obj.magic i dec hex)\".
+";
 
   return $extractionqccompat_v;
 }

coq-quickchick.opam

@@ -15,7 +15,7 @@ install: [
 ]
 depends: [
   "ocaml" {>= "4.07"}
-  "coq" {>= "8.12"}
+  "coq" {>= "8.11"}
   "coq-ext-lib"
   "coq-mathcomp-ssreflect"
   "ocamlbuild"

plugin/driver.mlg

@@ -44,8 +44,8 @@ let dispatch cn ind name1 name2 =
     match c with
     | {CAst.v = CRef (r, _) ; _} -> string_of_qualid r
     | _ -> failwith "Usage: Derive <class_name> for <inductive_name> OR  Derive (<class_name>, ... , <class_name>) for <inductive_name>" in
-  let ss = match cn with
-     | { CAst.v = CNotation (_,_,([a],[b],_,_)); _ } -> begin
+  let ss = match Compat.from_CNotation cn.CAst.v with
+     | Some ([a],[b],_,_) -> begin
          let c = convert_reference_to_string a in
          let cs = List.map convert_reference_to_string b in
          c :: cs

plugin/genericLib.ml

@@ -84,8 +84,8 @@ let gArg ?assumName:(an=hole) ?assumType:(at=hole) ?assumImplicit:(ai=false) ?as
     | { CAst.v = CHole (_v,_,_); loc } -> (loc,Anonymous)
     | _a -> failwith "This expression should be a name" in
   CLocalAssum ( [CAst.make ?loc:(fst n) @@ snd n],
-                  (if ag then Generalized (Glob_term.MaxImplicit, false)
-                   else if ai then Default Glob_term.MaxImplicit else Default Glob_term.Explicit),
+                  (if ag then Generalized (Compat.max_implicit, false)
+                   else if ai then Default Compat.max_implicit else Default Glob_term.Explicit),
                   at )
 
 let arg_to_var (x : arg) =
@@ -844,11 +844,8 @@ let dtTupleType =
 
 (* Int *)
 
-let mkNumber n =
-  Compat.number (NumTok.Signed.of_int_string (string_of_int n))
-
 let nat_scope ast = CAst.make @@ CDelimiters ("nat", ast)
-let gInt n = nat_scope (CAst.make @@ CPrim (mkNumber n))
+let gInt n = nat_scope (CAst.make @@ CPrim (Compat.number n))
 let gSucc x = gApp (gInject "Coq.Init.Datatypes.S") [x]
 let rec maximum = function
   | [] -> failwith "maximum called with empty list"

plugin/tactic_quickchick.mlg

@@ -25,7 +25,7 @@ let quickchick_goal =
     Printf.printf "So far so good\n"; flush stdout;
 
     (* Externalize it *)
-    let ct = Constrextern.extern_constr e evd (EConstr.mkEvar (evar , [])) in
+    let ct = Compat.extern_constr_ e evd evar in
 
     (* Construct : show (quickCheck (_ : ct)) *)
     let qct =

plugin/weightmap.mlg

@@ -33,23 +33,18 @@ let register_weights (l : (constructor * weight_ast) list) =
 let convert_constr_to_weight c = 
   match c.CAst.v with
   | CPrim p ->
-    (match Compat.from_Number p with
-    | Some  (NumTok.SPlus,i) ->
-      (match NumTok.Unsigned.to_nat i with
-      | Some n -> WNum (int_of_string n)
-      | None -> failwith "QC: Numeric weights should be positive integers.")
-    | Some (NumTok.SMinus,_) ->
-      failwith "QC: Numeric weights should be greater than 0."
-    | None -> failwith "QC: match failure."
+    (match Compat.from_nonnegative_Number p with
+    | Some n -> WNum n
+    | None -> failwith "QC: Numeric weights should be positive integers."
     )
   | CRef (r, _) ->
      if string_of_qualid r = "size" then WSize
      else failwith "QC: Expected number or 'size'."
   | _ -> failwith "QC: match failure."
 
 let convert_constr_to_cw_pair c : (constructor * weight_ast) = 
-  match c with 
-  | { CAst.v = CNotation (_,_,([a],[[b]],_,_)); _ } -> begin
+  match Compat.from_CNotation c.CAst.v with
+  | Some ([a],[[b]],_,_) -> begin
       let ctr = 
         match a with 
         | { CAst.v = CRef (r, _); _ } -> injectCtr (string_of_qualid r)
@@ -78,8 +73,8 @@ VERNAC COMMAND EXTEND QuickChickWeights CLASSIFIED AS SIDEFF
   | ["QuickChickWeights" constr(c)] -> 
      {
        let weight_assocs = 
-         match c with 
-         | { CAst.v = CNotation (_,_,([a],[b],_,_)); _ } -> begin
+         match Compat.from_CNotation c.CAst.v with
+         | Some ([a],[b],_,_) -> begin
              let c = convert_constr_to_cw_pair a in
              let cs = List.map convert_constr_to_cw_pair b in
              c :: cs

quickchick.opam

@@ -14,7 +14,7 @@ depends: [
   "ocaml"                   { >= "4.05.0" }
   "dune"                    { >= "1.9.0"  }
   "menhir"                  {     build   }
-  "coq"                     { >= "8.12"    }
+  "coq"                     { >= "8.11"    }
   "coq-ext-lib"
   "coq-mathcomp-ssreflect"
   "coq-simple-io"           {  = "dev"    }

src/ExtractionQC.v

@@ -20,10 +20,6 @@ Extract Inductive Decimal.int => "((Obj.t -> Obj.t) -> (Obj.t -> Obj.t) -> Obj.t
   [ "(fun x pos _ -> pos (Obj.magic x))"
     "(fun y _ neg -> neg (Obj.magic y))"
   ] "(fun i pos neg -> Obj.magic i pos neg)".
-Extract Inductive Hexadecimal.int => "((Obj.t -> Obj.t) -> (Obj.t -> Obj.t) -> Obj.t) (* Hexadecimal.int *)"
-  [ "(fun x pos _ -> pos (Obj.magic x))"
-    "(fun y _ neg -> neg (Obj.magic y))"
-  ] "(fun i pos neg -> Obj.magic i pos neg)".
 
 Extract Constant show_nat =>
   "(fun i ->