Grouping REPL definitions (#90)

This commit also fixes buggy behavior of `import` in REPL (#83)

---------

Co-authored-by: Piotr Polesiuk <[email protected]>

src/DblParser/Main.ml

@@ -32,14 +32,15 @@ let rec repl_seq imported () =
 
   | Raw.REPL_Expr e ->
     let def = make_nowhere (Lang.Surface.DReplExpr(Desugar.tr_expr e)) in
-    Seq.Cons(def, repl_seq imported)
+    Seq.Cons([def], repl_seq imported)
 
-  | Raw.REPL_Def def ->
-    Seq.Cons(Desugar.tr_def def, repl_seq imported)
+  | Raw.REPL_Defs defs ->
+      let defs = List.map Desugar.tr_def defs in
+      Seq.Cons(defs, repl_seq imported)
 
   | Raw.REPL_Import import ->
     let imported, defs = Import.import_one imported import in
-    Seq.append (List.to_seq defs) (repl_seq imported) ()
+    Seq.Cons(defs, repl_seq imported)
 
   | exception Parsing.Parse_error ->
     Error.fatal (Error.unexpected_token

src/DblParser/Raw.ml

@@ -304,8 +304,8 @@ type repl_cmd =
   | REPL_Expr of expr
     (** Evaluate given expression *)
 
-  | REPL_Def  of def
-    (** Provide a new definition in a REPL session *)
+  | REPL_Defs of def list
+    (** Provide a new group of definitions in a REPL session *)
 
   | REPL_Import of import
     (** Import a module *)

src/DblParser/YaccParser.mly

@@ -588,8 +588,8 @@ file
 ;
 
 repl
-: EOF               { REPL_Exit      }
-| expr SEMICOLON2   { REPL_Expr   $1 }
-| def SEMICOLON2    { REPL_Def    $1 }
-| import SEMICOLON2 { REPL_Import $1 }
+: EOF                  { REPL_Exit      }
+| expr SEMICOLON2      { REPL_Expr   $1 }
+| def_list1 SEMICOLON2 { REPL_Defs   $1 }
+| import SEMICOLON2    { REPL_Import $1 }
 ;

src/Lang/Surface.ml

@@ -232,8 +232,10 @@ and expr_data =
   | EAnnot of expr * type_expr
     (** Type annotation *)
 
-  | ERepl of def Seq.t
-    (** REPL. It is a lazy sequence of definitions provided by a user. *)
+  | ERepl of def list Seq.t
+    (** REPL. It is a lazy sequence of groups of definitions provided by a
+      user. Each group is treated as a monolith: if one of them fails, the
+      other have no effect. *)
 
 (** Explicit instantiation of named parameters in polymorphic expression *)
 and inst = (name * expr) node

src/TypeInference/Expr.ml

@@ -155,7 +155,7 @@ let rec check_repl_def_seq ~tcfix env ienv def_seq tp eff =
           (e, Infered tp, Impure)
       in
       let (e, Checked, _) =
-        check_def env ienv def (Check tp) eff { run = cont } in
+        check_defs env ienv def (Check tp) eff { run = cont } in
       e
   in
   let e =