Revive OCaml frontend

Makefile

@@ -4,19 +4,19 @@ export OCAMLRUNPARAM=b
 all:
 	@echo 'note: running unit tests only'
 	@echo 'use make test to run fast integration tests, and make test-all to run all tests'
-	dune build src test @runtest --display=short
+	dune build src test @runtest
 
 .PHONY: test
 test:
-	TEST=1 dune test --display=short
+	TEST=1 dune test
 
 .PHONY: test-all
 test-all:
-	TEST_ALL=1 dune test --display=short
+	TEST_ALL=1 dune test
 
 .PHONY: w
 w:
-	dune build src @runtest -w --display=short
+	dune build src @runtest -w
 
 debug-menhir:
 	echo 'parse_term: TRUE' | menhir --dump --explain --interpret --interpret-show-cst --trace src/parse/parser.mly

src/heifer/dune

@@ -3,5 +3,7 @@
  (public_name heifer)
  ; heifer is often used interactively, so linkall is given here.
  ; this also avoids having to list all transitive dependencies in mdx
+ (inline_tests)
+ (preprocess (pps ppx_expect))
  (library_flags (-linkall))
- (libraries core parsing prover))
+ (libraries core ocamlfrontend parsing prover))

src/heifer/extra_tactics.ml

@@ -0,0 +1,20 @@
+open Util.Strings
+open Prover.Interactive.State
+open Prover
+
+let read_file filename =
+  let ic = open_in filename in
+  let s = In_channel.input_all ic in
+  close_in ic;
+  let sdefns, obs = Ocamlfrontend.get_definitions_and_obligations s in
+  List.iter (fun (s, d) -> declare_defn { sym_name = s } d) sdefns;
+  let new_goals =
+    List.map
+      (fun (ass, ob) ->
+        let assumptions = List.mapi (fun i a -> (Format.asprintf "H%d" i, a)) ass |> SMap.of_list in
+        Pctx.create ~assumptions ob)
+      obs
+  in
+  add_goals new_goals;
+  set_mode Mode_goal;
+  print_proof_state ()

src/heifer/extra_tactics_test.ml

@@ -0,0 +1,43 @@
+open Prover.Interactive.State
+open Prover.Interactive
+open Extra_tactics
+
+let%expect_test "read_file" =
+  let filename = "test_obs.ml" in
+  let oc = open_out filename in
+  output_string oc {|
+let f x
+(*@ 1 @*)
+= 1
+
+let g x
+(*@ 1 @*)
+= f x
+|};
+  close_out oc;
+  reset_proof_state ();
+  read_file filename;
+  forall_intro ();
+  refl ();
+  Sys.remove filename;
+  [%expect
+    {|
+    f declared
+    g declared
+
+    ────────────────────────────────────────────────────────────
+    forall x. 1 <: 1
+    (1 more goals)
+
+
+    x
+    ────────────────────────────────────────────────────────────
+       1
+    <: 1
+    (1 more goals)
+
+
+    H0: forall x. f x <: 1
+    ────────────────────────────────────────────────────────────
+    forall x. f x <: 1
+    |}]

src/heifer/heifer.ml

@@ -10,11 +10,13 @@ module Interactive = struct
 
   include Prover.Interactive.State
   include Prover.Interactive
+  include Extra_tactics
 
   let () = Format.set_margin !Prover.Prover_options.line_length
 
   module Statistics = struct
     let start_time = ref (Unix.gettimeofday ())
+
     let reset () =
       start_time := Unix.gettimeofday ();
       Why3_prover.reset_statistics ()

src/ocamlfrontend/core_lang.ml

@@ -0,0 +1,73 @@
+type pattern =
+  | PVar of string
+  | PConstr of string * pattern list
+  | PAny
+  | PInt of int
+
+type expr =
+  | Var of string
+  | Int of int
+  | Fun of string list * expr
+  | Apply of expr * expr list
+  | Let of string * expr * expr
+  | If of expr * expr * expr
+  | Sequence of expr * expr
+  | Shift of string * expr
+  | Reset of expr
+  | Perform of string * expr option
+  | Resume of expr list
+  | Match of expr * (pattern * expr) list
+  | WithSpec of expr * string * string
+
+type verification_unit = {
+  pure_functions : (string * expr) list;
+  program_functions : (string * expr) list;
+}
+
+let rec dump_pattern ppf p =
+  match p with
+  | PVar x -> Format.fprintf ppf "%S" x
+  | PConstr (c, args) ->
+      Format.fprintf ppf "%s(%a)" c
+        (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf ", ") dump_pattern)
+        args
+  | PAny -> Format.fprintf ppf "_"
+  | PInt i -> Format.fprintf ppf "%d" i
+
+let rec dump_term ppf t =
+  match t with
+  | Var x -> Format.fprintf ppf "Var %S" x
+  | Int i -> Format.fprintf ppf "Int %d" i
+  | Fun (xs, body) ->
+      Format.fprintf ppf "Fun ([%a], %a)"
+        (Format.pp_print_list
+           ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ")
+           (fun ppf x -> Format.fprintf ppf "%S" x))
+        xs dump_term body
+  | Apply (f, args) ->
+      Format.fprintf ppf "Apply (%a, [%a])" dump_term f
+        (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ") dump_term)
+        args
+  | Let (x, t1, t2) -> Format.fprintf ppf "Let (%S, %a, %a)" x dump_term t1 dump_term t2
+  | If (c, t1, t2) -> Format.fprintf ppf "If (%a, %a, %a)" dump_term c dump_term t1 dump_term t2
+  | Sequence (t1, t2) -> Format.fprintf ppf "Sequence (%a, %a)" dump_term t1 dump_term t2
+  | Shift (k, body) -> Format.fprintf ppf "Shift (%S, %a)" k dump_term body
+  | Reset t -> Format.fprintf ppf "Reset (%a)" dump_term t
+  | Perform (eff, arg) ->
+      Format.fprintf ppf "Perform (%S, %a)" eff
+        (fun ppf arg ->
+          match arg with
+          | None -> Format.fprintf ppf "None"
+          | Some t -> Format.fprintf ppf "Some (%a)" dump_term t)
+        arg
+  | Resume args ->
+      Format.fprintf ppf "Resume ([%a])"
+        (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ") dump_term)
+        args
+  | Match (t, cases) ->
+      Format.fprintf ppf "Match (%a, [%a])" dump_term t
+        (Format.pp_print_list
+           ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ")
+           (fun ppf (p, e) -> Format.fprintf ppf "(%a, %a)" dump_pattern p dump_term e))
+        cases
+  | WithSpec (t, s, name) -> Format.fprintf ppf "WithSpec (%a, %S, %S)" dump_term t s name

src/ocamlfrontend/core_lang.mli

@@ -0,0 +1,31 @@
+
+type pattern =
+  | PVar of string
+  | PConstr of string * pattern list
+  | PAny  (** [_] *)
+  | PInt of int
+
+(** OCaml programs *)
+type expr =
+  | Var of string
+  | Int of int
+  | Fun of string list * expr
+  | Apply of expr * expr list
+  | Let of string * expr * expr
+  | If of expr * expr * expr
+  | Sequence of expr * expr
+  | Shift of string * expr
+  | Reset of expr
+  | Perform of string * expr option
+  | Resume of expr list
+  | Match of expr * (pattern * expr) list
+  | WithSpec of expr * string * string (* the :: operator, as an expr *)
+
+(** Analogous to a compilation unit; all the structure we get from a source file *)
+type verification_unit = {
+  pure_functions : (string * expr) list;
+  program_functions : (string * expr) list;
+}
+
+val dump_pattern : Format.formatter -> pattern -> unit
+val dump_term : Format.formatter -> expr -> unit

src/ocamlfrontend/dune

@@ -0,0 +1,9 @@
+
+(library
+ (name ocamlfrontend)
+ (public_name heifer.ocamlfrontend)
+ (inline_tests)
+ (libraries compiler-libs.common heifer.core bindlib str heifer.parsing)
+ (preprocess (pps ppx_expect)))
+
+(env (dev (flags (:standard -warn-error -A))))

src/ocamlfrontend/forward_rules.ml

@@ -0,0 +1,60 @@
+open Core_lang
+open Core.Syntax
+
+let resolve_to_primitive f args =
+  match (f, args) with
+  | Core_lang.Var op, [arg1; arg2] ->
+      (match op with
+      | "+" -> Some (Mk.binop Plus arg1 arg2)
+      | "-" -> Some (Mk.binop Minus arg1 arg2)
+      | "*" | "*." ->
+          (* there is no separation logic in core lang, so this seems okay *)
+          Some (Mk.binop Times arg1 arg2)
+      | "=" -> Some (Mk.binop Eq arg1 arg2)
+      | "<>" -> Some (Mk.binop Neq arg1 arg2)
+      | "<" -> Some (Mk.binop Lt arg1 arg2)
+      | "<=" -> Some (Mk.binop Le arg1 arg2)
+      | ">" -> Some (Mk.binop Gt arg1 arg2)
+      | ">=" -> Some (Mk.binop Ge arg1 arg2)
+      | "::" -> Some (Mk.binop Cons arg1 arg2)
+      | _ -> None)
+  | Var op, [arg] ->
+      (match op with
+      | "not" -> Some (Mk.unop Not arg)
+      | "~-" | "-" -> Some (Mk.unop Neg arg)
+      | _ -> None)
+  | _ -> None
+
+let rec convert_box (env : (string * term Bindlib.var) list) (t : expr) : term Bindlib.box =
+  match t with
+  | Var x ->
+      (match List.assoc_opt x env with
+      | Some v -> Mk.var v
+      | None -> Mk.symbol { sym_name = x })
+  | Int i -> Mk.int i
+  | Fun (xs, body) ->
+      let vars = Array.map (fun x -> Bindlib.new_var (fun v -> Var v) x) (Array.of_list xs) in
+      let env' = List.combine xs (Array.to_list vars) @ env in
+      let body' = convert_box env' body in
+      Mk.fun_ (Bindlib.bind_mvar vars body')
+  | Apply (f, args) ->
+      let f_box = convert_box env f in
+      let args_box = List.map (convert_box env) args in
+      resolve_to_primitive f args_box
+      |> Option.value ~default:(Mk.apply f_box (Bindlib.box_list args_box))
+  | Let (x, t1, t2) ->
+      let v = Bindlib.new_var (fun v -> Var v) x in
+      let t1' = convert_box env t1 in
+      let t2' = convert_box ((x, v) :: env) t2 in
+      Mk.bind t1' (Bindlib.bind_var v t2')
+  | Sequence (t1, t2) -> Mk.sequence (convert_box env t1) (convert_box env t2)
+  | Shift (k, body) ->
+      let v = Bindlib.new_var (fun v -> Var v) k in
+      let body' = convert_box ((k, v) :: env) body in
+      Mk.shift (Bindlib.bind_var v body')
+  | Reset t1 -> Mk.reset (convert_box env t1)
+  | WithSpec (t, _spec, _name) -> convert_box env t
+  | Match _ | If _ | Perform _ | Resume _ ->
+      failwith "conversion to Syntax.term not yet supported for this construct"
+
+let apply (t : expr) : term = Bindlib.unbox (convert_box [] t)

src/ocamlfrontend/forward_rules.mli

@@ -0,0 +1,4 @@
+open Core.Syntax
+open Core_lang
+
+val apply : expr -> term