Stream: Coq devs & plugin devs

Topic: native compilation and universe polymorphism


view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 12:50):

Is that me or nobody ever tried to run native compute on universe polymorphic data? I am seeing stuff that is outright wrong in the implementation and that just can't work.

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 12:51):

For instance, we have this call

  let ml_of_level l =
    match Univ.Level.var_index l with
    | Some i ->
      (* FIXME: use a proper cast function *)
       let univ = MLprimitive (MLmagic, [|MLlocal (Option.get instance)|]) in
       MLprimitive (MLarrayget, [|univ; MLint i|])
    | None -> let i = push_symbol (SymbLevel l) in get_level_code i
  in

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 12:51):

But MLarrayget expects a persistent array as its argument, not an OCaml array

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 12:52):

how can this even work?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 12:53):

There are also ominous FIXMEs here and there, like

    let accu =
      let args =
        if Int.equal (Univ.AbstractContext.size u) 0 then
          [|get_ind_code j; MLarray [||]|]
        else [|get_ind_code j|]
      in
      (* FIXME: pass universes here *)
      Glet(name, MLprimitive (Mk_ind, args))
    in

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 12:54):

IIUC the code we just don't even pass any instance to the inductive there when it's polymorphic

view this post on Zulip Guillaume Melquiond (Oct 19 2022 at 13:31):

No, MLarrayget is plain Array.get, so it takes an OCaml array.

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 13:38):

Right, I got confused with the Arrayget primitive constructor.

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 13:39):

The other snippet still seems very suspicious though


Last updated: Dec 07 2023 at 14:02 UTC