[WIP] Strange compiler bug

src/main.ml

@@ -115,6 +115,29 @@ let check () =
   else if s > !size_limit then
     raise Out_of_space
 
+let do_task
+    (module S : Msat.External.S
+     with type St.formula = Expr.atom) s =
+  match s.Dolmen.Statement.descr with
+  | Dolmen.Statement.Def (id, t) -> Type.new_def id t
+  | Dolmen.Statement.Decl (id, t) -> Type.new_decl id t
+  | Dolmen.Statement.Consequent t ->
+    let f = Type.new_formula t in
+    let cnf = Expr.Formula.make_cnf f in
+    S.assume cnf
+  | Dolmen.Statement.Antecedent t ->
+    let f = Expr.Formula.make_not @@ Type.new_formula t in
+    let cnf = Expr.Formula.make_cnf f in
+    S.assume cnf
+  | Dolmen.Statement.Prove ->
+    begin match S.solve () with
+      | S.Sat _ -> ()
+      | S.Unsat _ -> ()
+    end
+  | _ ->
+    Format.printf "Command not supported:@\n%a@."
+      Dolmen.Statement.print s
+
 let main () =
   (* Administrative duties *)
   Arg.parse argspec input_file usage;

src/util/type.ml

@@ -103,7 +103,7 @@ let def_term id ty_args args body =
 (* ************************************************************************ *)
 
 (* Make a new empty environment *)
-let empty_env ?(expect=Nothing) = {
+let empty_env ?(expect=Nothing) () = {
   type_vars = M.empty;
   term_vars = M.empty;
   term_lets = M.empty;
@@ -595,7 +595,8 @@ let rec parse_fun ty_args t_args env = function
 (* High-level parsing functions *)
 (* ************************************************************************ *)
 
-let new_decl env t id =
+let new_decl id t =
+  let env = empty_env () in
   Log.debugf 5 "Typing declaration: %s : %a"
     (fun k -> k id.Id.name Ast.print t);
   begin match parse_sig env t with
@@ -604,7 +605,8 @@ let new_decl env t id =
       decl_term id (Expr.Id.term_fun id.Id.name vars args ret)
   end
 
-let new_def env t id =
+let new_def id t =
+  let env = empty_env () in
   Log.debugf 5 "Typing definition: %s = %a"
     (fun k -> k id.Id.name Ast.print t);
   begin match parse_fun [] [] env t with
@@ -612,7 +614,8 @@ let new_def env t id =
     | `Term (ty_args, t_args, body) -> def_term id ty_args t_args body
   end
 
-let new_formula env t =
+let new_formula t =
+  let env = empty_env () in
   Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t);
   let res = parse_formula env t in
   res