Consistent handling of constructors with no parameters

3 files changed, 11 insertions, 9 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index b7641438..7a9ae1cd 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -834,12 +834,14 @@ let rec to_exp mode env v : (exp tannot * lenv) =
   | V_list(vals) -> let (es,env') = mapf vals env in (E_aux (E_list es) annot, env')
   | V_ctor id t ckind vals -> 
     let annotation = mk_annot true (Just ckind) in
-    (match vals with
-    | V_lit (L_aux L_unit _) -> (E_aux (E_id id) annotation, env)
-    | V_track (V_lit (L_aux L_unit _)) _ -> (E_aux (E_id id) annotation, env)
-    | V_tuple vals -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env')
-    | V_track (V_tuple vals) _ -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env')
-    | V_track _ _ -> 
+    (match (vals,ckind) with
+    | (V_lit (L_aux L_unit _), C_Union) -> (E_aux (E_app id []) annotation, env)
+    | (V_lit (L_aux L_unit _), C_Enum _) -> (E_aux (E_id id) annotation, env)
+    | (V_track (V_lit (L_aux L_unit _)) _, C_Union) -> (E_aux (E_app id []) annotation, env)
+    | (V_track (V_lit (L_aux L_unit _)) _, C_Enum _) -> (E_aux (E_id id) annotation, env)
+    | (V_tuple vals,_) -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env')
+    | (V_track (V_tuple vals) _,_) -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env')
+    | (V_track _ _,_) -> 
       if mode.track_values 
       then begin let (fid,env') = fresh_var env in
                  let env' = add_to_env (fid,vals) env' in
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 0ecd6fe7..72f5ba7c 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -376,7 +376,7 @@ let decode_to_istate top_level value =
 	 top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
       match (instr_decoded,error) with
 	| (Just instr,_) ->
-	  let (arg,_) = Interp.to_exp mode Interp.eenv instr in
+	  (*let (arg,_) = Interp.to_exp mode Interp.eenv instr in*)
 	  Instr instr_external
 	    (IState (Interp.Thunk_frame
 		       (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
diff --git a/src/type_check.ml b/src/type_check.ml
index 6c332e0b..f1b44395 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -476,8 +476,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	let t,cs,ef,_ = subst params false t cs ef in
         (match t.t with
         | Tfn({t = Tid "unit"},t',IP_none,ef) -> 
-          let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t' 
-	    (rebuild (Base(([],{t=Tfn(unit_t,t',IP_none,ef)}),Constructor,cs,ef,bounds))) expect_t in
+	  let e = E_aux(E_app(id, []), (l, (Base(([],{t=Tfn(unit_t,t',IP_none,ef)}), Constructor, cs, ef, bounds)))) in
+          let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t' e expect_t in
           (e',t',t_env,cs@cs',nob,union_effects ef ef')
         | Tfn(t1,t',IP_none,e) -> 
           typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none")