Adapt to coq/coq#18143 (debug printing for relevances) (#347)

Co-authored-by: Yishuai Li <liyishuai.lys@alibaba-inc.com>

.gitignore

@@ -42,6 +42,7 @@ _build/
 quickChickTool.byte
 plugin/depDriver.ml
 plugin/genericLib.ml
+plugin/mergeTypes.ml
 plugin/driver.ml
 plugin/driver.mlg
 plugin/quickChick.ml
@@ -58,6 +59,7 @@ __pycache__
 .lia.cache
 plugin/compat.ml
 src/ExtractionQCCompat.v
+src/TacticsUtil.v
 src/QuickChick.v
 _CoqProject
 META

Makefile

@@ -80,6 +80,8 @@ tests:
 COMPATFILES:= \
 	plugin/depDriver.ml \
 	plugin/genericLib.ml \
+	plugin/mergeTypes.ml \
+	plugin/quickChick.mlg \
 	plugin/unifyQC.ml \
 	plugin/tactic_quickchick.mlg \
 	plugin/weightmap.mlg \

plugin/depDriver.ml.cppo

@@ -260,7 +260,11 @@ let compat_fromCApp1 (_, x) = x
  *)
 let dep_dispatch ind class_name : unit =
   match ind with 
+#if COQ_VERSION >= (8, 20, 0)
+  | { CAst.v = CLambdaN ([CLocalAssum ([{ CAst.v = Names.Name id; CAst.loc = _loc2 }], _, _kind, _type)], body); _ } -> (* {CAst.v = CApp ((_flag, constructor), args) }) } -> *)
+#else
   | { CAst.v = CLambdaN ([CLocalAssum ([{ CAst.v = Names.Name id; CAst.loc = _loc2 }], _kind, _type)], body); _ } -> (* {CAst.v = CApp ((_flag, constructor), args) }) } -> *)
+#endif
 
     let idu = Unknown.from_string (Names.Id.to_string id ^ "_") in
 

plugin/genericLib.ml.cppo

@@ -108,13 +108,20 @@ let gArg ?assumName:(an=hole) ?assumType:(at=hole) ?assumImplicit:(ai=false) ?as
     | _a -> failwith "This expression should be a name" in
   let max_implicit = Glob_term.MaxImplicit in
   CLocalAssum ( [CAst.make ?loc:(fst n) @@ snd n],
+#if COQ_VERSION >= (8, 20, 0)
+                  None,
+#endif
                   (if ag then Generalized (max_implicit, false)
                    else if ai then Default max_implicit else Default Glob_term.Explicit),
                   at )
 
 let arg_to_var (x : arg) =
   match x with
+#if COQ_VERSION >= (8, 20, 0)
+  | CLocalAssum ([{CAst.v = id; _}], _, _ ,_ ) -> id_of_name id
+#else
   | CLocalAssum ([{CAst.v = id; _}], _ ,_ ) -> id_of_name id
+#endif
   | _ -> qcfail "arg_to_var must be named"
 
 let str_lst_to_string sep (ss : string list) = 
@@ -622,7 +629,11 @@ let gApp ?explicit:(expl=false) c cs =
   else mkAppC (c, cs)
 
 let gProdWithArgs args f_body =
+#if COQ_VERSION >= (8, 20, 0)
+  let xvs = List.map (fun (CLocalAssum ([{CAst.v = n;_}], _, _, _)) ->
+#else
   let xvs = List.map (fun (CLocalAssum ([{CAst.v = n;_}], _, _)) ->
+#endif
                       match n with
                       | Name x -> x
                       | _ -> make_up_name ()
@@ -631,7 +642,11 @@ let gProdWithArgs args f_body =
   mkCProdN args fun_body
 
 let gFunWithArgs args f_body =
+#if COQ_VERSION >= (8, 20, 0)
+  let xvs = List.map (fun (CLocalAssum ([{CAst.v = n;_}], _, _, _)) ->
+#else
   let xvs = List.map (fun (CLocalAssum ([{CAst.v = n;_}], _, _)) ->
+#endif
                       match n with
                       | Name x -> x
                       | _ -> make_up_name ()
@@ -647,7 +662,11 @@ let gFun xss (f_body : var list -> coq_expr) =
   | _ ->
   let xvs = List.map (fun x -> fresh_name x) xss in
   (* TODO: optional argument types for xss *)
+#if COQ_VERSION >= (8, 20, 0)
+  let binder_list = List.map (fun x -> CLocalAssum ([CAst.make @@ Name x], None, Default Glob_term.Explicit, hole)) xvs in
+#else
   let binder_list = List.map (fun x -> CLocalAssum ([CAst.make @@ Name x], Default Glob_term.Explicit, hole)) xvs in
+#endif
   let fun_body = f_body xvs in
   mkCLambdaN binder_list fun_body 
 
@@ -657,14 +676,22 @@ let gFunTyped xts (f_body : var list -> coq_expr) =
   | _ ->
   let xvs = List.map (fun (x,t) -> (fresh_name x,t)) xts in
   (* TODO: optional argument types for xss *)
+#if COQ_VERSION >= (8, 20, 0)
+  let binder_list = List.map (fun (x,t) -> CLocalAssum ([CAst.make @@ Name x], None, Default Glob_term.Explicit, t)) xvs in
+#else
   let binder_list = List.map (fun (x,t) -> CLocalAssum ([CAst.make @@ Name x], Default Glob_term.Explicit, t)) xvs in
+#endif
   let fun_body = f_body (List.map fst xvs) in
   mkCLambdaN binder_list fun_body 
 
 (* with Explicit/Implicit annotations *)  
 let gRecFunInWithArgs ?structRec:(rec_id=None) ?assumType:(typ=hole) (fs : string) args (f_body : (var * var list) -> coq_expr) (let_body : var -> coq_expr) = 
   let fv  = fresh_name fs in
+#if COQ_VERSION >= (8, 20, 0)
+  let xvs = List.map (fun (CLocalAssum ([{CAst.v = n;_}], _, _, _)) ->
+#else
   let xvs = List.map (fun (CLocalAssum ([{CAst.v = n;_}], _, _)) ->
+#endif
                       match n with
                       | Name x -> x
                       | _ -> make_up_name ()
@@ -674,7 +701,11 @@ let gRecFunInWithArgs ?structRec:(rec_id=None) ?assumType:(typ=hole) (fs : strin
     | None -> None
     | Some id -> Some (CAst.make @@ CStructRec (CAst.make id)) in
   CAst.make @@ CLetIn (CAst.make @@ Name fv,
+#if COQ_VERSION >= (8, 20, 0)
+    CAst.make @@ CFix(CAst.make fv,[(CAst.make fv, None, rec_wf, args, typ, fix_body)]), None,
+#else
     CAst.make @@ CFix(CAst.make fv,[(CAst.make fv, rec_wf, args, typ, fix_body)]), None,
+#endif
     let_body fv)
 
 let gRecFunIn ?structRec:(rec_id=None) ?assumType:(typ = hole) (fs : string) (xss : string list) (f_body : (var * var list) -> coq_expr) (let_body : var -> coq_expr) =
@@ -1183,11 +1214,19 @@ let defineTypedConstant s c typ =
 (* Declare an instance *)
 let create_names_for_anon a =
   match a with 
+#if COQ_VERSION >= (8, 20, 0)
+  | CLocalAssum ([{CAst.v = n; loc}], r, x, y) ->
+#else
   | CLocalAssum ([{CAst.v = n; loc}], x, y) ->
+#endif
      begin match n with
            | Name x -> (x, a)
            | Anonymous -> let n = make_up_name () in
+#if COQ_VERSION >= (8, 20, 0)
+                          (n, CLocalAssum ([CAst.make ?loc:loc @@ Names.Name n], r, x, y))
+#else
                           (n, CLocalAssum ([CAst.make ?loc:loc @@ Names.Name n], x, y))
+#endif
      end
   | _ -> failwith "Non RawAssum in create_names"
 
@@ -1531,4 +1570,4 @@ let find_typeclass_bindings typeclass_name ctr =
     ) db;
     !result
 
-
+

plugin/mergeTypes.ml → plugin/mergeTypes.ml.cppo

@@ -444,7 +444,11 @@ type relation
 
 let extract_relation ind : relation * int =
   match ind with 
+#if COQ_VERSION >= (8, 20, 0)
+  | { CAst.v = CLambdaN ([CLocalAssum ([{ CAst.v = Names.Name id1; CAst.loc = _loc2 }], _, _kind, _type)], body1); _ } ->
+#else
   | { CAst.v = CLambdaN ([CLocalAssum ([{ CAst.v = Names.Name id1; CAst.loc = _loc2 }], _kind, _type)], body1); _ } ->
+#endif
     (* Extract (x1,x2,...) if any, P and arguments *)
     let (p1, args1) =
       match body1 with 

plugin/quickChick.mlg → plugin/quickChick.mlg.cppo

@@ -411,7 +411,11 @@ let qcFuzz_main prop_def temp_dir execn prop_mlf prop_mlif warnings prop fuzzLoo
   let unit_type =
     CAst.make @@ CRef (qualid_of_string "Coq.Init.Datatypes.unit", None) in
   let unit_arg =
+#if COQ_VERSION >= (8, 20, 0)
+    CLocalAssum ( [ CAst.make (Name (fresh_name "x")) ], None, Default Glob_term.Explicit, unit_type ) in
+#else
     CLocalAssum ( [ CAst.make (Name (fresh_name "x")) ], Default Glob_term.Explicit, unit_type ) in
+#endif
   let pair_ctr =
     CAst.make @@ CRef (qualid_of_string "Coq.Init.Datatypes.pair", None) in
   let show_expr cexpr =