example for 407

.github/workflows/users.yml

@@ -30,12 +30,12 @@ jobs:
           env:
             OPAMWITHTEST: false
 
-        - run: opam pin --ignore-constraints-on elpi            add rocq-elpi              https://github.com/LPCIC/coq-elpi.git#elpi-3.7
-        - run: opam pin --ignore-constraints-on elpi            add coq-elpi               https://github.com/LPCIC/coq-elpi.git#elpi-3.7
+        - run: opam pin --ignore-constraints-on elpi            add rocq-elpi              https://github.com/LPCIC/coq-elpi.git#master
+        - run: opam pin --ignore-constraints-on elpi            add coq-elpi               https://github.com/LPCIC/coq-elpi.git#master
         - run: opam pin --ignore-constraints-on elpi            add rocq-stdlib            https://github.com/rocq-prover/stdlib.git#master
         - run: opam pin --ignore-constraints-on elpi            add coq-stdlib             https://github.com/rocq-prover/stdlib.git#master
         - run: opam pin --ignore-constraints-on elpi,coq-stdlib add coq-trocq-std          https://github.com/rocq-community/trocq.git#master
-        - run: opam pin --ignore-constraints-on elpi            add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#hierarchy-builder.elpi-3.7
+        - run: opam pin --ignore-constraints-on elpi            add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#master
         - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-boot     https://github.com/math-comp/math-comp.git#master
         - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-order    https://github.com/math-comp/math-comp.git#master
         - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master

tests/sources/bug_407.ml

@@ -0,0 +1,41 @@
+open Elpi.API
+
+let global = Ast.Loc.initial "init"
+let base_str = 
+  {| kind foo type. 
+     external symbol mk_t : int -> foo = "1".
+
+     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;
+        assert(c == mk_t_c)
+      | _ -> exit 1
+    end r.assignments
+  | _ -> exit 1
+  end

tests/sources/dune

@@ -18,4 +18,5 @@
 (executable (name sepcomp_tyid2)  (modules sepcomp_tyid2)  (libraries sepcomp))
 (executable (name sepcomp_hover)  (modules sepcomp_hover)  (libraries sepcomp))
 (executable (name sepcomp_extend_sig)  (modules sepcomp_extend_sig)  (libraries sepcomp))
-(executable (name sepcomp_extend_sig2)  (modules sepcomp_extend_sig2)  (libraries sepcomp))
+(executable (name sepcomp_extend_sig2)  (modules sepcomp_extend_sig2)  (libraries sepcomp))
+(executable (name bug_407)  (modules bug_407)  (libraries elpi))

tests/suite/elpi_api.ml

@@ -83,3 +83,8 @@ let () = declare "sepcomp_extend_sig2"
   ~expectation:Test.Success
   ()
 
+let () = declare "bug_407"
+  ~source_dune:"bug_407.exe"
+  ~description:"misleading API"
+  ~expectation:Test.Success
+  ()