extraction mode: adding level to environment in unquote_universe

[aa755]

There seems to be a discrepancy in how unquote_level is instantiated in extraction mode and in template-coq (live-coq) mode.

The extraction mode implementation is here and looks like:

  let unquote_level (trm : Univ0.Level.t) : Univ.Level.t =
    match trm with
    | Univ0.Level.Coq_lProp -> Univ.Level.prop
    | Univ0.Level.Coq_lSet -> Univ.Level.set
    | Univ0.Level.Level s ->
      let s = unquote_string s in
      let comps = CString.split '.' s in
      let last, dp = CList.sep_last comps in
      let dp = DirPath.make (List.map Id.of_string comps) in
      let idx = int_of_string last in
      Univ.Level.make dp idx
    | Univ0.Level.Var n -> Univ.Level.var (unquote_int n)

Clearly from the types, it does not thread the environment (Evd. evar_map). In contrast, the template-coq version, implemented here, threads the environment and makes a non-trivial change to it (the tLevel case calls get_level which can add a universe to the environment):

let get_level evm s =
  if CString.string_contains ~where:s ~what:"." then
    match List.rev (CString.split '.' s) with
    | [] -> CErrors.anomaly (str"Invalid universe name " ++ str s ++ str".")
    | n :: dp ->
       let num = int_of_string n in
       let dp = DirPath.make (List.map Id.of_string dp) in
       let l = Univ.Level.make dp num in
       try
         let evm = Evd.add_global_univ evm l in
         if !strict_unquote_universe_mode then
           CErrors.user_err ~hdr:"unquote_level" (str ("Level "^s^" is not a declared level and you are in Strict Unquote Universe Mode."))
         else (Feedback.msg_info (str"Fresh universe " ++ Level.pr l ++ str" was added to the context.");
               evm, l)
       with
       | UGraph.AlreadyDeclared -> evm, l
  else
    try
      evm, Evd.universe_of_name evm (Id.of_string s)
    with Not_found ->
         try
           let univ, k = Nametab.locate_universe (Libnames.qualid_of_string s) in
           evm, Univ.Level.make univ k
         with Not_found ->
           CErrors.user_err ~hdr:"unquote_level" (str ("Level "^s^" is not a declared level."))

let unquote_level evm trm (* of type level *) : Evd.evar_map * Univ.Level.t =
  let (h,args) = app_full trm [] in
  if Constr.equal h lProp then
    match args with
    | [] -> evm, Univ.Level.prop
    | _ -> bad_term_verb trm "unquote_level"
  else if Constr.equal h lSet then
    match args with
    | [] -> evm, Univ.Level.set
    | _ -> bad_term_verb trm "unquote_level"
  else if Constr.equal h tLevel then
    match args with
    | s :: [] -> debug (fun () -> str "Unquoting level " ++ pr_constr trm);
                 get_level evm (unquote_string s)
    | _ -> bad_term_verb trm "unquote_level"
  else if Constr.equal h tLevelVar then
    match args with
    | l :: [] -> evm, Univ.Level.var (unquote_nat l)
    | _ -> bad_term_verb trm "unquote_level"
  else
    not_supported_verb trm "unquote_level"

Should the extraction version be fixed to thread/update the context in a similar way?

[gmalecha]

They should definitely do the same thing.

[mattam82]

Yes it should do the same. It might be reasonable to have a strict mode of unquoting where universes cannot be created as well, ensuring reproducible results

[mattam82]

To be clear, it should be the second version used in ‘live-coq’