Unclear how to use constants defined via `declare_global_symbol`

[abakst]

Hi there,

I have the following small example: I want to send a query to elpi & then inspect the structure of the solution to
construct a term in OCaml (i.e., decode from an elpi term to some ocaml type).

open Elpi.API

let global = Ast.Loc.initial "init"
let base_str = 
  {| kind foo type. 
     type mk_t int -> foo.

     type is_t foo -> int -> (pred).
     is_t (mk_t N) N.
  |}

let is_t_c = RawData.Constants.declare_global_symbol "is_t"
let mk_t_c = RawData.Constants.declare_global_symbol "mk_t"
let query = 
  Ast.Term.mkAppGlobal ~loc:global ~hdloc:global is_t_c
    (Ast.Term.mkVar ~loc:global ~hdloc:global (Ast.Name.from_string "X") []) 
    [Ast.Term.mkOpaque ~loc:global (RawOpaqueData.int.cino 4)]

let () = begin 
  let flags = { Compile.default_flags with Compile.print_units = true } in
  let elpi = Setup.init 
    ~builtins:[Elpi.Builtin.std_builtins]
    ~flags:(Compile.to_setup_flags flags)
    ~file_resolver:(Parse.std_resolver ~paths:[] ()) () in
  let base = Parse.program_from ~elpi ~loc:global ~digest:(Digest.string "") (Lexing.from_string base_str) in
  let pgm = Compile.program ~flags ~elpi base in
  let query = Compile.optimize @@ RawQuery.compile_term pgm (fun st -> st, query) in
  match Execute.once query with
  | Execute.Success r ->
    Setup.StrMap.iter begin fun k v ->
      match RawData.look ~depth:0 v with
      | RawData.App (c, _, _) ->
        Format.printf "Solution: %a, %d, %d\n"
          (Pp.term r.pp_ctx) v
          c
          mk_t_c
      | _ -> exit 1
    end r.assignments
  | _ -> exit 1
  end

You can see that I declare a constant mk_t_c corresponding to mk_t. However, when I run the program, I get output like:

Solution: mk_t 4, -418, -73

so it is clear I can not simply compare the view's App's constant against the one that I declare in my program.

I am assuming that that this approach must not be the right way to go about decoding the solution term, but I'm at a loss for the right way to do it. In the general case, I do expect there to be unsolved unification variables - does that matter? Is there an example I can reference? The tini-ml example that is checked in seems stale & also stops short of the decode step.

Thank you!

[gares]

Thanks for reporting, there is surely a missing check in the compiler, since you are not supposed to declare symbols available in ocaml that way.

I'm not on my pc right now to give you a poc. But you can look at booleans for example, they are marked as external symbols. Or look in coq elpi for symbols like app fun match...

If you do that, the numbers will match.

[abakst]

Ah, I think I get it. Any of these declarations must be treated as builtin, is that correct? i.e. if I wish to use AlgebraicData to define the conversion, then I should include the conversion via MLData in a Builtin.declaration list when compiling the program & query?

[gares]

Here an example of how to expose an OCaml data type in a more orthodox way:

open Elpi.API

let global = Ast.Loc.initial "init"
let base_str = 
  {| 
     type is_t foo -> int -> (pred).
     is_t (mk_t N) N.
  |}

type foo = T of int

let foo : foo Conversion.t = let open AlgebraicData in declare {
  ty = Conversion.TyName "foo";
  doc = "doc";
  pp = (fun fmt _ -> Format.fprintf fmt "TODO");
  constructors = [
    K("mk_t",
      "doc",
      A(BuiltInData.int,N),
      B (fun n -> T n),
      M (fun ~ok ~ko -> function T n -> ok n | _ -> ko ())
      )]
  } |> ContextualConversion.(!<)

let is_t_c = RawData.Constants.declare_global_symbol "is_t"

let query = 
  Ast.Term.mkAppGlobal ~loc:global ~hdloc:global is_t_c
    (Ast.Term.mkVar ~loc:global ~hdloc:global (Ast.Name.from_string "X") []) 
    [Ast.Term.mkOpaque ~loc:global (RawOpaqueData.int.cino 4)]

let my_builtins = BuiltIn.(declare ~file_name:"mybuiltins.elpi" [MLData foo])

let () = begin 
  let flags = { Compile.default_flags with Compile.print_units = true } in
  let elpi = Setup.init 
    ~builtins:[Elpi.Builtin.std_builtins;my_builtins]
    ~flags:(Compile.to_setup_flags flags)
    ~file_resolver:(Parse.std_resolver ~paths:[] ()) () in
  let base = Parse.program_from ~elpi ~loc:global ~digest:(Digest.string "") (Lexing.from_string base_str) in
  let pgm = Compile.program ~flags ~elpi base in
  let query = Compile.optimize @@ RawQuery.compile_term pgm (fun st -> st, query) in
  match Execute.once query with
  | Execute.Success r ->
    Setup.StrMap.iter begin fun k v ->
      match foo.Conversion.readback ~depth:0 r.state v with
      | _, T x, _ ->
        Format.printf "Solution: %d\n" x
      | _ -> exit 1
    end r.assignments
  | _ -> exit 1
  end

[abakst]

Thank you! That makes sense.