runtime: move turns discard into UVar (fix #30)

src/API.ml

@@ -432,7 +432,6 @@ module RawData = struct
     (* Optimizations *)
     | Cons of term * term                 (* :: *)
     | Nil                                 (* [] *)
-    | Discard                             (* _  *)
     (* FFI *)
     | Builtin of builtin * term list      (* call to a built-in predicate *)
     | CData of RawOpaqueData.t                    (* external data *)
@@ -448,6 +447,9 @@ module RawData = struct
         UnifVar ({ lvl; handle = Ref ub},args)
     | ED.Term.AppUVar(ub,lvl,args) ->
         UnifVar ({ lvl; handle = Ref ub},args)
+    | ED.Term.Discard ->
+        let ub = ED.oref ED.Term.Constants.dummy in
+        UnifVar ({ lvl = 0; handle = Ref ub},ED.Term.Constants.mkinterval 0 depth 0)
     | x -> Obj.magic x (* HACK: view is a "subtype" of Term.term *)
 
   let kool = function
@@ -620,9 +622,6 @@ module FlexibleData = struct
     embed = (fun ~depth _ _ s (k,args) -> s, RawData.mkUnifVar k ~args s, []);
     readback = (fun ~depth _ _ state t ->
       match RawData.look ~depth t with
-      | RawData.Discard ->
-          let state, k = Elpi.make ~lvl:depth state in
-          state, (k,[]), []
       | RawData.UnifVar(k,args) ->
           state, (k,args), []
       | _ -> raise (Conversion.TypeErr (TyName "uvar",depth,t)));

src/API.mli

@@ -764,7 +764,6 @@ module RawData : sig
     (* Optimizations *)
     | Cons of term * term                 (* :: *)
     | Nil                                 (* [] *)
-    | Discard                             (* _  *)
     (* FFI *)
     | Builtin of builtin * term list      (* call to a built-in predicate *)
     | CData of RawOpaqueData.t            (* opaque data *)

src/builtin.ml

@@ -61,7 +61,6 @@ let rec eval depth t =
      f []
   | (Nil | Cons _ as x) ->
       type_error ("Lists cannot be evaluated: " ^ RawPp.Debug.show_term (kool x))
-  | Discard -> type_error "_ cannot be evaluated"
   | CData _ as x -> kool x
 ;;
 
@@ -183,7 +182,6 @@ let occurs x d t =
      | Builtin (_, vs)                  -> auxs vs
      | Cons (v1, v2)                    -> aux v1 || aux v2
      | Nil
-     | Discard
      | CData _                          -> false
    and auxs = function
      | []      -> false
@@ -738,7 +736,6 @@ let name_or_constant name condition = (); fun x out ~depth _ _ state ->
   | NoData -> raise No_clause
   | Data x ->
       match look ~depth x with
-      | Discard -> assert false
       | Const n when condition n ->
           if out = [] then !: x +? None
           else !: x +! [Some x; Some mkNil]
@@ -763,8 +760,6 @@ let name_or_constant name condition = (); fun x out ~depth _ _ state ->
 
 let rec same_term ~depth t1 t2 =
   match look ~depth t1, look ~depth t2 with
-  | Discard, UnifVar _ -> true
-  | UnifVar _, Discard -> true
   | UnifVar(b1,xs), UnifVar(b2,ys) -> FlexibleData.Elpi.equal b1 b2 && same_term_list ~depth xs ys
   | App(c1,x,xs), App(c2,y,ys) -> c1 == c2 && same_term ~depth x y && same_term_list ~depth xs ys
   | Const c1, Const c2 -> c1 == c2

src/runtime.ml

@@ -731,7 +731,10 @@ let rec move ~adepth:argsdepth e ?avoid ?(depth=0) ~from ~to_ t =
        let tl' = maux e depth tl in
        if hd == hd' && tl == tl' then x else Cons(hd',tl')
     | Nil -> x
-    | Discard -> x
+    | Discard when avoid = None -> x
+    | Discard ->
+       let r = oref C.dummy in
+       UVar(r,to_,0)
 
     (* fast path with no deref... *)
     | UVar _ when delta == 0 && avoid == None -> x
@@ -1179,7 +1182,6 @@ let bind r gamma l a d delta b left t e =
     | App (c,t,ts) -> App (cst c b delta, bind b delta w t, List.map (bind b delta w) ts)
     | Cons(hd,tl) -> Cons(bind b delta w hd, bind b delta w tl)
     | Nil -> t
-    | Discard -> t
     | Builtin (c, tl) -> Builtin(c, List.map (bind b delta w) tl)
     | CData _ -> t
     (* deref_uv *)
@@ -1192,7 +1194,7 @@ let bind r gamma l a d delta b left t e =
     | AppUVar ({ contents = t }, from, args) when t != C.dummy ->
         bind b delta w (deref_appuv ~from ~to_:((if left then b else a)+d+w) args t)
     (* pruning *)
-    | (UVar _ | AppUVar _ | Arg _ | AppArg _) as orig ->
+    | (UVar _ | AppUVar _ | Arg _ | AppArg _ | Discard) as orig ->
         (* We deal with all flexible terms in a uniform way *)
         let r, lvl, (is_llam, args), orig_args = match orig with
           | UVar(r,lvl,0) -> r, lvl, (true, []), []
@@ -1203,6 +1205,9 @@ let bind r gamma l a d delta b left t e =
               r', (lvl+args),  (true,[]), []
           | AppUVar (r,lvl, orig_args) ->
               r, lvl, is_llam lvl orig_args a b (d+w) left e, orig_args
+          | Discard ->
+              let r = oref C.dummy in
+              r, a+d+w, (true,[]), []
           | Arg (i,0) ->
               let r = oref C.dummy in
               let v = UVar(r,a,0) in

tests/sources/heap_discard.elpi

@@ -0,0 +1,5 @@
+main :-
+  X = [_,2],
+  X = [1,2],
+  not(X = [2,2]),
+  pi a b\ Y b = [_], b = _.

tests/sources/same_term.elpi

@@ -1,6 +1,6 @@
 main :-
   3 == 3,
-  [X, _] == [X, Y],
+  not([X, _] == [X, Y]),
   not(X == Y),
   (x\ x) == (y\ y),
   ID = (x\x),

tests/suite/elpi_specific.ml

@@ -184,3 +184,10 @@ let () = declare "list_comma"
   ~typecheck:true
   ~expectation:Test.Success
   ()
+
+let () = declare "heap_discard"
+  ~source_elpi:"heap_discard.elpi"
+  ~description:"heapification of _"
+  ~typecheck:true
+  ~expectation:Test.Success
+  ()