[Ur] project to a fieldname list

[Adam Chlipala]

Gergely Buday wrote:
>>> my idea is to write a function that projectds records to a given set
>>> of names. Is it doable in Ur/Web?
>>>        
>> I'm not sure exactly what you're asking for.  Does the [---] operator do the
>> trick?  Its first argument is a value of record type, and its second
>> argument is a constructor of kind [{Type}], specifying which fields to
>> remove from the record.
>>      
> It is clear what is record.1 . I would like to have
>
>    record.[1,2,3,4]
>
> independently what other fields does r have.
>    

Perhaps I wasn't clear enough about what I was suggesting.  Consider 
this function that wraps the built-in [---] operator:

(* *)
fun projection [fs1 ::: {Type}] [fs2 ::: {Type}] [fs1 ~ fs2] (r : $(fs1 
++ fs2)) : $fs2 = r --- _
(* *)

Here is a simple example of using it:

(* *)
type r1 = {A : int, B : float, C : string}
type r2 = {A : int, C : string}

val r1 : r1 = {A = 1, B = 2.0, C = "x"}
val r2 : r2 = projection r1
(* *)

Is that what you're looking to do?  If so, you can cut out the named 
function and simply write [r1 --- _] in the last line (and in other 
related contexts).