From dab61fe5c57e9001783d351b93db7b2bdacb4eb3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Tue, 6 Feb 2024 13:44:34 +0100
Subject: [PATCH 1/2] CHR: term (uvar X [...]) is defrost as (X ...)

---
 src/runtime.ml                  | 10 ++++++++++
 tests/sources/mk-evar-meta.elpi | 15 +++++++++++++++
 tests/suite/elpi_specific.ml    |  7 +++++++
 3 files changed, 32 insertions(+)
 create mode 100644 tests/sources/mk-evar-meta.elpi

diff --git a/src/runtime.ml b/src/runtime.ml
index 863613538..cdf04db25 100644
--- a/src/runtime.ml
+++ b/src/runtime.ml
@@ -3161,10 +3161,20 @@ end = struct (* {{{ *)
           let tl' = daux d tl in
           if hd == hd' && tl == tl' then orig
           else Cons(hd',tl')
+      | App(c,UVar(r,lvl,ano),a) when !!r != C.dummy ->
+          daux d (App(c,deref_uv ~to_:d ~from:lvl ano !!r,a))
+      | App(c,AppUVar(r,lvl,args),a) when !!r != C.dummy ->
+          daux d (App(c,deref_appuv ~to_:d ~from:lvl args !!r,a))
       | App(c,Const x,[args]) when c == Global_symbols.uvarc ->
           let r = C.Map.find x f.c2uv in
           let args = lp_list_to_list ~depth:d args in
           mkAppUVar r 0 (smart_map (daux d) args)
+      | App(c,UVar(r,_,_),[args]) when c == Global_symbols.uvarc ->
+          let args = lp_list_to_list ~depth:d args in
+          mkAppUVar r 0 (smart_map (daux d) args)
+      | App(c,AppUVar(r,_,_),[args]) when c == Global_symbols.uvarc ->
+          let args = lp_list_to_list ~depth:d args in
+          mkAppUVar r 0 (smart_map (daux d) args)
       | App(c,x,xs) as orig ->
           let x' = daux d x in
           let xs' = smart_map (daux d) xs in
diff --git a/tests/sources/mk-evar-meta.elpi b/tests/sources/mk-evar-meta.elpi
new file mode 100644
index 000000000..3f9696fa8
--- /dev/null
+++ b/tests/sources/mk-evar-meta.elpi
@@ -0,0 +1,15 @@
+main :-
+  (pi x y z\ sigma X XL\ mk-uvar [y] X XL, print "1)" X "/" XL, var XL X [y]).
+
+  
+type mk-uvar list A -> B -> C -> o.
+mk-uvar L U UL :- declare_constraint (mk-uvar L U UL) [_].
+
+constraint mk-uvar {
+
+  rule \ (mk-uvar L U UL) | (meta-mk-uvar L U UL X XL) <=> (U = X, UL = XL).
+
+}
+
+type meta-mk-uvar list A -> B -> C -> D -> E -> o.
+meta-mk-uvar L (uvar _ _) (uvar _ _) X XL :- X = (uvar D []), XL = (uvar D L).
\ No newline at end of file
diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml
index fe69b9c0f..ba07ea1b1 100644
--- a/tests/suite/elpi_specific.ml
+++ b/tests/suite/elpi_specific.ml
@@ -303,6 +303,13 @@ let () = declare "graft_replace_err"
   ~expectation:Test.(FailureOutput (Str.regexp "name attribute"))
   ()
 
+let () = declare "mk_uv_meta"
+  ~source_elpi:"mk-evar-meta.elpi"
+  ~description:"uvar surgery at the meta level"
+  ~typecheck:true
+  ~expectation:Test.Success
+  ()
+
 let mk_tmp_file =
   let tmp = ref 0 in
   let dir = Filename.get_temp_dir_name () in

From 1f9a108b7a1c2514b2066c2dbff8931f85e9bfc8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Tue, 6 Feb 2024 13:44:49 +0100
Subject: [PATCH 2/2] nicer error message for wrong multi pi

---
 src/compiler.ml        | 4 +---
 src/parser/ast.ml      | 4 ++++
 src/parser/ast.mli     | 2 ++
 src/parser/grammar.mly | 4 ++++
 4 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/compiler.ml b/src/compiler.ml
index 545e6ce4c..3d4e9a336 100644
--- a/src/compiler.ml
+++ b/src/compiler.ml
@@ -990,9 +990,7 @@ let preterm_of_ast ?(on_type=false) loc ~depth:arg_lvl macro state ast =
   let spy_spill c =
     spilling := !spilling || c == D.Global_symbols.spillc in
 
-  let is_uvar_name f = 
-     let c = (F.show f).[0] in
-     ('A' <= c && c <= 'Z') in
+  let is_uvar_name f =  F.is_uvar_name f in
     
   let is_discard f =
     F.(equal f dummyname) ||
diff --git a/src/parser/ast.ml b/src/parser/ast.ml
index 12ebe8c1f..a45c00716 100644
--- a/src/parser/ast.ml
+++ b/src/parser/ast.ml
@@ -50,6 +50,10 @@ module Func = struct
 
   end
 
+  let is_uvar_name s =
+    let c = s.[0] in
+    ('A' <= c && c <= 'Z')
+
   include Self
   module Map = Map.Make(Self)
 
diff --git a/src/parser/ast.mli b/src/parser/ast.mli
index 39b13a4e8..b9d001768 100644
--- a/src/parser/ast.mli
+++ b/src/parser/ast.mli
@@ -32,6 +32,8 @@ module Func : sig
   val dummyname : t
   val spillf : t
 
+  val is_uvar_name : t -> bool
+
   val from_string : string -> t
 
   module Map : Map.S with type key = t
diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly
index 4773e8142..001eca261 100644
--- a/src/parser/grammar.mly
+++ b/src/parser/grammar.mly
@@ -26,6 +26,10 @@ let desugar_multi_binder loc = function
   | App(Const hd as binder,args)
     when Func.equal hd Func.pif || Func.equal hd Func.sigmaf && List.length args > 1 ->
       let last, rev_rest = let l = List.rev args in List.hd l, List.tl l in
+      let () = match last with
+        | Lam _ -> ()
+        | Const x when Func.is_uvar_name x -> ()
+        | _ -> raise (ParseError(loc,"The last argument of 'pi' or 'sigma' must be a function or a unification variable, while it is: " ^ Ast.Term.show last)) in
       let names = List.map (function
         | Const x -> Func.show x
         | (App _ | Lam _ | CData _ | Quoted _) ->