Merge pull request #220 from LPCIC/uv-chr

improve chr defrosting

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) ||

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)
 

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

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 _) ->

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

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).

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