Interpreter: handle conversion to runtime of defaults//options

This case is really acrobatic, because we are interfacing code compiled to
OCaml (from lcalc) with code from dcalc, and the two have a different
representation for default terms. It... seems to work though.

A more reasonable solution, if there are problems with this or it reveals too
fragile, would be to enforce interpreting at the lcalc level as soon as you want
to link compiled modules.

compiler/shared_ast/interpreter.ml

@@ -529,7 +529,13 @@ let rec runtime_to_val :
            (Array.to_list (Obj.obj o))),
       m )
   | TArrow (targs, tret) -> ECustom { obj = o; targs; tret }, m
-  | TDefault ty -> runtime_to_val eval_expr ctx m ty o
+  | TDefault ty -> (
+    (* This case is only valid for ASTs including default terms; but the typer
+       isn't aware so we need some additional dark arts. *)
+    match (Obj.obj o : 'a Runtime.Eoption.t) with
+    | Runtime.Eoption.ENone () -> Obj.magic EEmpty, m
+    | Runtime.Eoption.ESome o -> Obj.magic (runtime_to_val eval_expr ctx m ty o)
+    )
   | TAny -> assert false
 
 and val_to_runtime :
@@ -543,7 +549,6 @@ and val_to_runtime :
     Obj.t =
  fun eval_expr ctx ty v ->
   match Mark.remove ty, Mark.remove v with
-  | _, EEmpty -> raise Runtime.Empty
   | TLit TBool, ELit (LBool b) -> Obj.repr b
   | TLit TUnit, ELit LUnit -> Obj.repr ()
   | TLit TInt, ELit (LInt i) -> Obj.repr i
@@ -610,7 +615,11 @@ and val_to_runtime :
             curry (runtime_to_val eval_expr ctx m targ x :: acc) targs)
     in
     curry [] targs
-  | TDefault ty, _ -> val_to_runtime eval_expr ctx ty v
+  | TDefault ty, _ -> (
+    match v with
+    | EEmpty, _ -> Obj.repr (Runtime.Eoption.ENone ())
+    | EPureDefault e, _ | e ->
+      Obj.repr (Runtime.Eoption.ESome (val_to_runtime eval_expr ctx ty e)))
   | TClosureEnv, v ->
     (* By construction, a closure environment can only be consumed from the same
        scope where it was built (compiled or not) ; for this reason, we can