Syntactic sugar for explicit instantiations with (effectful) functions (#269)

Added syntactic sugar for explicit instantiations with (effectful) functions, thus solving #228 and #232.
Added 2 tests for this new feature.

Author: wojciechdomin

src/DblParser/Desugar.ml

@@ -197,7 +197,7 @@ and tr_scheme_field (fld : Raw.ty_field) =
     make (SA_Val(n, scheme_wildcard fld.pos))
   | FldNameVal(n, tp) ->
     make (SA_Val(n, tr_scheme_expr tp))
-  | FldNameAnnot _ | FldModule _ | FldOpen ->
+  | FldNameAnnot _ | FldModule _ | FldOpen | FldNameFn _ | FldNameEffectFn _ ->
     assert false
 
 (** Translate a type expression as a type variable with kind annotation *)
@@ -377,6 +377,8 @@ and tr_named_pattern ~public (fld : Raw.field) =
   | FldModule { data = NPName name; _ } -> make (NP_Module(public, name))
   | FldModule _ -> Error.fatal (Error.desugar_error fld.pos)
   | FldOpen     -> make (NP_Open public)
+  | FldNameFn _ | FldNameEffectFn _ -> 
+    Error.fatal (Error.desugar_error fld.pos)
 
 (** Translate a parameter declaration *)
 let tr_param_decl (fld : Raw.field) =
@@ -392,8 +394,8 @@ let tr_param_decl (fld : Raw.field) =
     Either.Right (n, ident_of_name n, None)
   | FldNameAnnot(n, sch) ->
     Either.Right (n, ident_of_name n, Some (tr_scheme_expr sch))
-
-  | FldTypeVal _ | FldNameVal _ | FldModule _ | FldOpen ->
+  | FldTypeVal _ | FldNameVal _ | FldModule _ | FldOpen 
+  | FldNameFn _ | FldNameEffectFn _ ->
     Error.fatal (Error.desugar_error fld.pos)
 
 (** Translate an expression as a let-pattern. *)
@@ -675,6 +677,13 @@ and tr_explicit_inst (fld : Raw.field) =
   | FldOpen -> make IOpen
   | FldNameAnnot _ | FldType(_, Some _) ->
     Error.fatal (Error.desugar_error fld.pos)
+  | FldNameFn (n, es, e) ->
+    make (IVal(n, tr_poly_expr_def ({pos = fld.pos; data = EFn(es, e)})))
+  | FldNameEffectFn (n, label, es, resumption, e) ->
+    make (IVal(n, tr_poly_expr_def
+      { pos = fld.pos;
+        data = EEffect({label; args = es; resumption; body = e})
+      }))
 
 and tr_def ?(public=false) (def : Raw.def) =
   let pos = def.pos in

src/DblParser/Raw.ml

@@ -78,6 +78,12 @@ type ('tp, 'e) field_data =
   | FldNameVal of name * 'e
     (** Named implicit parameter together with a value *)
 
+  | FldNameFn of name * 'e list * 'e 
+    (** Explicit instantiation with a function *)
+
+  | FldNameEffectFn of name * 'e option * 'e list * 'e option * 'e
+    (** Explicit instantiation with an effectful function *)
+
   | FldNameAnnot of name * 'tp
     (** type-annotated implicit parameter *)
 

src/DblParser/YaccParser.mly

@@ -103,7 +103,6 @@ op_50
 
 op_60
 : OP_60 { make $1  }
-| EQ    { make "=" }
 ;
 
 
@@ -485,6 +484,11 @@ field
 | UID                   { make (FldType($1, None))    }
 | UID EQ ty_expr        { make (FldTypeVal($1, $3))   }
 | UID COLON kind_expr   { make (FldType($1, Some $3)) }
+| name expr_250_list1 EQ expr_no_comma
+    { make (FldNameFn($1, $2, $4)) }
+| effect_label_opt KW_EFFECT name
+  expr_250_list1 effect_resumption_opt EQ expr_no_comma
+    { make (FldNameEffectFn($3, $1, $4, $5, $7)) }
 | name                  { make (FldName $1)           }
 | name EQ expr_no_comma { make (FldNameVal($1, $3))   }
 | name COLON ty_expr    { make (FldNameAnnot($1, $3)) }

test/ok/ok0140_explicitFunctionInstantiation.fram

@@ -0,0 +1,9 @@
+data Triples X Y Z = Triple of  X, Y, Z
+
+let _ = 
+  let f {type X, type Y, foo : X -> Y -> Triples X Y Y, bar : X ->[] X} x y =
+    foo (bar x) y
+  in
+  match f {foo x y = (Triple x y y), bar (x : Unit) = x} () () with
+  | Triple _ _ _ => ()
+  end 

test/ok/ok0141_explicitEffectfulFunctionInstantiation.fram

@@ -0,0 +1,12 @@
+data BT E = 
+  { flip : Unit ->[E] Bool
+  , fail : {type X} -> Unit ->[E] X
+  }
+
+let fun1 {E} (s : BT E) =
+	s.fail ()
+
+let _ = handle ~bt = BT
+  { effect flip () / r = r True; r False
+  , effect fail () = ()
+  } in fun1 ~bt