coqutil.Map.SortedListString.map cannot be extracted

[JasonGross]

This is currently blocking mit-plv/fiat-crypto#686 (cc @jadephilipoom )

If I do

Require Import Coq.extraction.Extraction.
Require Import coqutil.Map.SortedListString.
Extraction Language OCaml.
Recursive Extraction coqutil.Map.SortedListString.map.

I get:

type __ = Obj.t

type bool =
| True
| False

(** val negb : bool -> bool **)

let negb = function
| True -> False
| False -> True

type 'a option =
| Some of 'a
| None

type ('a, 'b) prod =
| Pair of 'a * 'b

(** val fst : ('a1, 'a2) prod -> 'a1 **)

let fst = function
| Pair (x, _) -> x

type 'a list =
| Nil
| Cons of 'a * 'a list

type comparison =
| Eq
| Lt
| Gt

(** val eqb : bool -> bool -> bool **)

let eqb b1 b2 =
  match b1 with
  | True -> b2
  | False -> (match b2 with
              | True -> False
              | False -> True)

(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **)

let rec fold_right f a0 = function
| Nil -> a0
| Cons (b, t) -> f b (fold_right f a0 t)

(** val find : ('a1 -> bool) -> 'a1 list -> 'a1 option **)

let rec find f = function
| Nil -> None
| Cons (x, tl) -> (match f x with
                   | True -> Some x
                   | False -> find f tl)

type positive =
| XI of positive
| XO of positive
| XH

type n =
| N0
| Npos of positive

module Pos =
 struct
  (** val succ : positive -> positive **)

  let rec succ = function
  | XI p -> XO (succ p)
  | XO p -> XI p
  | XH -> XO XH

  (** val add : positive -> positive -> positive **)

  let rec add x y =
    match x with
    | XI p ->
      (match y with
       | XI q -> XO (add_carry p q)
       | XO q -> XI (add p q)
       | XH -> XO (succ p))
    | XO p ->
      (match y with
       | XI q -> XI (add p q)
       | XO q -> XO (add p q)
       | XH -> XI p)
    | XH -> (match y with
             | XI q -> XO (succ q)
             | XO q -> XI q
             | XH -> XO XH)

  (** val add_carry : positive -> positive -> positive **)

  and add_carry x y =
    match x with
    | XI p ->
      (match y with
       | XI q -> XI (add_carry p q)
       | XO q -> XO (add_carry p q)
       | XH -> XI (succ p))
    | XO p ->
      (match y with
       | XI q -> XO (add_carry p q)
       | XO q -> XI (add p q)
       | XH -> XO (succ p))
    | XH -> (match y with
             | XI q -> XI (succ q)
             | XO q -> XO (succ q)
             | XH -> XI XH)

  (** val mul : positive -> positive -> positive **)

  let rec mul x y =
    match x with
    | XI p -> add y (XO (mul p y))
    | XO p -> XO (mul p y)
    | XH -> y

  (** val compare_cont : comparison -> positive -> positive -> comparison **)

  let rec compare_cont r x y =
    match x with
    | XI p ->
      (match y with
       | XI q -> compare_cont r p q
       | XO q -> compare_cont Gt p q
       | XH -> Gt)
    | XO p ->
      (match y with
       | XI q -> compare_cont Lt p q
       | XO q -> compare_cont r p q
       | XH -> Gt)
    | XH -> (match y with
             | XH -> r
             | _ -> Lt)

  (** val compare : positive -> positive -> comparison **)

  let compare =
    compare_cont Eq
 end

module N =
 struct
  (** val compare : n -> n -> comparison **)

  let compare n0 m =
    match n0 with
    | N0 -> (match m with
             | N0 -> Eq
             | Npos _ -> Lt)
    | Npos n' -> (match m with
                  | N0 -> Gt
                  | Npos m' -> Pos.compare n' m')

  (** val ltb : n -> n -> bool **)

  let ltb x y =
    match compare x y with
    | Lt -> True
    | _ -> False
 end

module Coq_N =
 struct
  (** val add : n -> n -> n **)

  let add n0 m =
    match n0 with
    | N0 -> m
    | Npos p -> (match m with
                 | N0 -> n0
                 | Npos q -> Npos (Pos.add p q))

  (** val mul : n -> n -> n **)

  let mul n0 m =
    match n0 with
    | N0 -> N0
    | Npos p -> (match m with
                 | N0 -> N0
                 | Npos q -> Npos (Pos.mul p q))
 end

type ascii =
| Ascii of bool * bool * bool * bool * bool * bool * bool * bool

(** val eqb0 : ascii -> ascii -> bool **)

let eqb0 a b =
  let Ascii (a0, a1, a2, a3, a4, a5, a6, a7) = a in
  let Ascii (b0, b1, b2, b3, b4, b5, b6, b7) = b in
  (match match match match match match match eqb a0 b0 with
                                       | True -> eqb a1 b1
                                       | False -> False with
                                 | True -> eqb a2 b2
                                 | False -> False with
                           | True -> eqb a3 b3
                           | False -> False with
                     | True -> eqb a4 b4
                     | False -> False with
               | True -> eqb a5 b5
               | False -> False with
         | True -> eqb a6 b6
         | False -> False with
   | True -> eqb a7 b7
   | False -> False)

(** val n_of_digits : bool list -> n **)

let rec n_of_digits = function
| Nil -> N0
| Cons (b, l') ->
  Coq_N.add (match b with
             | True -> Npos XH
             | False -> N0) (Coq_N.mul (Npos (XO XH)) (n_of_digits l'))

(** val n_of_ascii : ascii -> n **)

let n_of_ascii = function
| Ascii (a0, a1, a2, a3, a4, a5, a6, a7) ->
  n_of_digits (Cons (a0, (Cons (a1, (Cons (a2, (Cons (a3, (Cons (a4, (Cons (a5,
    (Cons (a6, (Cons (a7, Nil))))))))))))))))

type string =
| EmptyString
| String of ascii * string

module Coq_map =
 struct
  type ('key, 'value) map = { get : (__ -> 'key -> 'value option); empty : 
                              __; put : (__ -> 'key -> 'value -> __);
                              remove : (__ -> 'key -> __);
                              fold : (__ -> (__ -> 'key -> 'value -> __) -> __ ->
                                     __ -> __) }
 end

module Coq_parameters =
 struct
  type parameters =
    __ -> __ -> bool
    (* singleton inductive, whose constructor was Build_parameters *)

  type key = __

  type value = __

  (** val ltb : parameters -> key -> key -> bool **)

  let ltb parameters0 =
    parameters0
 end

(** val eqb1 :
    Coq_parameters.parameters -> Coq_parameters.key -> Coq_parameters.key -> bool **)

let eqb1 p k1 k2 =
  match negb (Coq_parameters.ltb p k1 k2) with
  | True -> negb (Coq_parameters.ltb p k2 k1)
  | False -> False

(** val put0 :
    Coq_parameters.parameters -> (Coq_parameters.key, Coq_parameters.value) prod
    list -> Coq_parameters.key -> Coq_parameters.value -> (Coq_parameters.key,
    Coq_parameters.value) prod list **)

let rec put0 p m k v =
  match m with
  | Nil -> Cons ((Pair (k, v)), Nil)
  | Cons (y, m') ->
    let Pair (k', v') = y in
    (match Coq_parameters.ltb p k k' with
     | True -> Cons ((Pair (k, v)), m)
     | False ->
       (match Coq_parameters.ltb p k' k with
        | True -> Cons ((Pair (k', v')), (put0 p m' k v))
        | False -> Cons ((Pair (k, v)), m')))

(** val remove0 :
    Coq_parameters.parameters -> (Coq_parameters.key, Coq_parameters.value) prod
    list -> Coq_parameters.key -> (Coq_parameters.key, Coq_parameters.value) prod
    list **)

let rec remove0 p m k =
  match m with
  | Nil -> Nil
  | Cons (y, m') ->
    let Pair (k', v') = y in
    (match Coq_parameters.ltb p k k' with
     | True -> m
     | False ->
       (match Coq_parameters.ltb p k' k with
        | True -> Cons ((Pair (k', v')), (remove0 p m' k))
        | False -> m'))

type rep =
  (Coq_parameters.key, Coq_parameters.value) prod list
  (* singleton inductive, whose constructor was Build_rep *)

(** val value0 :
    Coq_parameters.parameters -> rep -> (Coq_parameters.key, Coq_parameters.value)
    prod list **)

let value0 _ r =
  r

(** val map0 :
    Coq_parameters.parameters -> (Coq_parameters.key, Coq_parameters.value)
    Coq_map.map **)

let map0 p =
  let wrapped_put = fun m k v -> put0 p (value0 p m) k v in
  let wrapped_remove = fun m k -> remove0 p (value0 p m) k in
  { Coq_map.get = (fun m k ->
  match find (fun p0 -> eqb1 p k (fst p0)) (value0 p (Obj.magic m)) with
  | Some p0 -> let Pair (_, v) = p0 in Some v
  | None -> None); Coq_map.empty = (Obj.magic Nil); Coq_map.put =
  (Obj.magic wrapped_put); Coq_map.remove = (Obj.magic wrapped_remove);
  Coq_map.fold = (fun _ f r0 m ->
  fold_right (fun pat r -> let Pair (k, v) = pat in f r k v) r0
    (value0 p (Obj.magic m))) }

module Ascii =
 struct
  (** val ltb : ascii -> ascii -> bool **)

  let ltb c d =
    N.ltb (n_of_ascii c) (n_of_ascii d)
 end

(** val ltb0 : string -> string -> bool **)

let rec ltb0 a b =
  match a with
  | EmptyString -> (match b with
                    | EmptyString -> False
                    | String (_, _) -> True)
  | String (x, a') ->
    (match b with
     | EmptyString -> False
     | String (y, b') ->
       (match eqb0 x y with
        | True -> ltb0 a' b'
        | False -> Ascii.ltb x y))

(** val build_parameters : Coq_parameters.parameters **)

let build_parameters =
  Obj.magic ltb0

(** val map1 : (Coq_parameters.key, Coq_parameters.value) Coq_map.map **)

let map1 =
  map0 build_parameters

Running ocamlc foo.ml gives:

File "foo.ml", line 356, characters 4-8:
Error: The type of this expression, ('_weak1, '_weak2) Coq_map.map,
       contains type variables that cannot be generalized

[andres-erbsen]

:/. having never used ocaml extraction, I don't know what to look at here

[JasonGross]

I think this is the Coq bug rocq-prover/rocq#4875. I guess it's possible that enough Extraction Inline directives will fix it locally? The other approach (which I guess is sort-of similar to Extraction Inline) is to try to make the relevant things Notations rather than Definitions

[JasonGross]

Indeed, adding Extraction Inline coqutil.Map.SortedListString.map fixes the issue. idk if you want to record this anywhere or anything, or just close this issue, or what

[andres-erbsen]

is there a reason not to put that directive right after the definition?

[JasonGross]

I think you need to Require Import Coq.extraction.Extraction in order for the directive to be valid. Otherwise, no, no reason to not do it. (Unless for some reason you want it to not be inlined in other languages where not inlining won't result in an error, such as Haskell)

If you're fine with adding Require Import Coq.extraction.Extraction, then I'd suggest adding the directive right after the definition with a note referencing the Coq bug