REPL grouping works if there is no error #90
Conversation
There was a problem hiding this comment.
The order of definitions is reversed (see detailed comments).
Moreover, the problem of looping REPL (bug mentioned in the PR comment, and #83) probably comes from the fact, that single user input is not treated as a monolith somewhere in the pipeline. If some definition is split into two definitions fun () -> Cons(def1, fun () -> Conf(def2, ...)) and checking of def1 succeeds, but def2 fails, then the evaluator (see Eval.eval_repl) calls the failing thunk again, which in this scenario deterministically returns def2 instead of asking the user for another input. Therefore, thunks describing user input in REPL must be never split into smaller ones. In order to achieve this, the group of definitions should be propagated to type-checker and checked as a monolith. Fortunately, we already have the infrastructure for that (we can use TypeInference.Def.check_defs instead of TypeInferece.Def.check_def).
src/Parser/Main.ml
Outdated
| | Raw.REPL_Def def -> | ||
| Seq.Cons(Desugar.tr_def def, repl_seq imported) | ||
| | Raw.REPL_Defs defs -> | ||
| (List.fold_left (fun ac def () -> Seq.Cons(Desugar.tr_def def, ac)) (repl_seq imported) defs) () |
There was a problem hiding this comment.
Using fold_left for appending lists naturally gives us rev_append instead of append. The same problem occurs here: definitions are reversed during parsing. This can be exhibited by the following input to REPL.
> let x = ()
let y = x ;;
<stdin>:2:9: fatal error: Unbound variable x
>
On the other hand, the following input work, but it shouldn't.
> let y = x
let x = () ;;
>
BTW, we try to keep source in good old 80-column style. This line is too long.
|
I made suggested change and it seems to work. |
src/Lang/Surface.ml
Outdated
| @@ -301,6 +301,9 @@ and def_data = | |||
| (** Print type, evaluate, and print the expression, provided by a user in | |||
| REPL. *) | |||
|
|
|||
| | DReplDefs of def list | |||
| (** Group of REPL definitions *) | |||
There was a problem hiding this comment.
Why do you add a new constructor? It is easier to modify ERepl to accept list of definitions.
|
New changes were added. |
src/Lang/Surface.ml
Outdated
| @@ -232,7 +232,7 @@ and expr_data = | |||
| | EAnnot of expr * type_expr | |||
| (** Type annotation *) | |||
|
|
|||
| | ERepl of def Seq.t | |||
| | ERepl of def list Seq.t | |||
| (** REPL. It is a lazy sequence of definitions provided by a user. *) | |||
There was a problem hiding this comment.
A documentation comment could be updated here.
src/Parser/Main.ml
Outdated
|
|
||
| | Raw.REPL_Import import -> | ||
| let imported, defs = Import.import_one imported import in | ||
| Seq.append (List.to_seq defs) (repl_seq imported) () | ||
| Seq.append (List.to_seq (List.map (fun x -> [x]) defs)) (repl_seq imported) () |
There was a problem hiding this comment.
Getting rid of Seq.append and changing it to single monolithic Seq.Cons hopefully fix #83. If it's a change of single line (that should be modified anyway) we should try.
|
Updated version fixes #83 |
This commit should resolve #82.
I have made minimal changes to make it work when there are no type errors. There is a problem with infinite loop:
But the other order works:
Changes in Parser/Main.ml have effect of inserting semicolons between lets and I guess that lazy handling of REPL definitions takes all those lets in one go. But I don't understand the codebase enough to tell why the loop error occurs.