split proof.ml in two + move Pure.goal to Goal.info

Author: fblanqui

src/handle/command.ml

@@ -6,6 +6,7 @@ open Common open Error open Pos
 open Core open Term open Sign open Sig_state open Print
 open Parsing open Syntax open Scope
 open Proof
+open Goal
 
 (** Type alias for a function that compiles a Lambdapi module. *)
 type compiler = Path.t -> Sign.t
@@ -582,7 +583,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       in
       (* Create the proof state. *)
       let pdata_state =
-        let proof_goals = Proof.add_goals_of_problem p [] in
+        let proof_goals = add_goals_of_problem p [] in
         if p_sym_def then
           (* Add a new focused goal and refine on it. *)
           let m = LibMeta.fresh p a 0 in

src/handle/proof.ml

@@ -1,137 +1,10 @@
-(** Proofs and tactics. *)
+(** Proof state. *)
 
-open Lplib open Base open Extra
+open Lplib open Base
 open Timed
-open Core open Term open Print
+open Core open Term
 open Common open Pos
-
-(** Type of goals. *)
-type goal_typ =
-  { goal_meta : meta  (** Goal metavariable. *)
-  ; goal_hyps : Env.t (** Precomputed scoping environment. *)
-  ; goal_type : term  (** Precomputed type. *) }
-
-type goal =
-  | Typ of goal_typ (** Typing goal. *)
-  | Unif of constr (** Unification goal. *)
-
-let is_typ : goal -> bool = function Typ _ -> true  | Unif _ -> false
-let is_unif : goal -> bool = function Typ _ -> false | Unif _ -> true
-
-let get_constr : goal -> constr =
-  function Unif c -> c | Typ _ -> invalid_arg (__FILE__ ^ "get_constr")
-
-let get_names : goal -> int StrMap.t = function
-  | Unif(c,_,_) -> Ctxt.names c
-  | Typ gt -> Env.names gt.goal_hyps
-
-module Goal = struct
-
-  type t = goal
-
-  (** [ctxt g] returns the typing context of the goal [g]. *)
-  let ctxt : goal -> ctxt = fun g ->
-    match g with
-    | Typ gt -> Env.to_ctxt gt.goal_hyps
-    | Unif (c,_,_) -> c
-
-  (** [env g] returns the scoping environment of the goal [g]. *)
-  let env : goal -> Env.t = fun g ->
-    match g with
-    | Unif (c,_,_) ->
-      let t, n = Ctxt.to_prod c mk_Type in
-      (try fst (Env.of_prod_nth c n t)
-       with Invalid_argument _ -> assert false)
-    | Typ gt -> gt.goal_hyps
-
-  (** [of_meta m] creates a goal from the meta [m]. *)
-  let of_meta : meta -> goal = fun m ->
-    let goal_hyps, goal_type =
-      try Env.of_prod_nth [] m.meta_arity !(m.meta_type)
-      with Invalid_argument _ -> assert false
-    in
-    Typ {goal_meta = m; goal_hyps; goal_type }
-
-  (** [simpl_opt f g] tries to simplify the goal [g] with the function [f]. *)
-  let simpl_opt : (ctxt -> term -> term option) -> goal -> goal option =
-    fun f g ->
-    match g with
-    | Typ gt ->
-        begin
-          match f (Env.to_ctxt gt.goal_hyps) gt.goal_type with
-          | None -> None
-          | Some goal_type -> Some(Typ {gt with goal_type})
-        end
-    | Unif (c,t,u) ->
-        begin
-          match f c t, f c u with
-          | Some t, Some u -> Some(Unif(c,t,u))
-          | _ -> None
-        end
-
-  (** [simpl f g] simplifies the goal [g] with the function [f]. *)
-  let simpl : (ctxt -> term -> term) -> goal -> goal = fun f g ->
-    match g with
-    | Typ gt ->
-        Typ {gt with goal_type = f (Env.to_ctxt gt.goal_hyps) gt.goal_type}
-    | Unif (c,t,u) -> Unif (c, f c t, f c u)
-
-  (** [hyps ppf g] prints on [ppf] the beta-normal forms of the hypotheses of
-      the goal [g]. *)
-  let hyps : int StrMap.t -> goal pp =
-    let hyps elt ppf l =
-      if l <> [] then
-        out ppf "%a---------------------------------------------\
-        ---------------------------------\n"
-        (List.pp (fun ppf -> out ppf "%a\n" elt) "") (List.rev l)
-    in
-    fun idmap ppf g ->
-    let term = term_in idmap in
-    match g with
-    | Typ gt ->
-      let elt ppf (s,(_,ty,def)) =
-        match def with
-        | None -> out ppf "%a: %a" uid s term (Eval.snf_beta ty)
-        | Some u -> out ppf "%a ≔ %a" uid s term u
-      in
-      hyps elt ppf gt.goal_hyps
-    | Unif (c,_,_) ->
-      let elt ppf (x,a,t) =
-        out ppf "%a: %a" var x term a;
-        match t with
-        | None -> ()
-        | Some t -> out ppf " ≔ %a" term t
-      in
-      hyps elt ppf c
-
-  (** [concl ppf g] prints on [ppf] the beta-normal form of the conclusion of
-      the goal [g]. *)
-  let concl : int StrMap.t -> goal pp = fun idmap ppf g ->
-    let term = term_in idmap in
-    match g with
-    | Typ gt ->
-        out ppf "?%d: %a" gt.goal_meta.meta_key
-          term (Eval.snf_beta gt.goal_type)
-    | Unif (_, t, u) -> out ppf "%a ≡ %a" term t term u
-
-  (** [pp ppf g] prints on [ppf] the beta-normal form of the goal [g] with its
-      hypotheses. *)
-  let pp ppf g =
-    let idmap = get_names g in hyps idmap ppf g; concl idmap ppf g
-
-  (** [pp_no_hyp ppf g] prints on [ppf] the beta-normal form of the conclusion
-      of the goal [g] without its hypotheses. *)
-  let pp_no_hyp ppf g = concl (get_names g) ppf g
-
-end
-
-(** [add_goals_of_problem p gs] extends the list of goals [gs] with the
-   metavariables and constraints of [p]. *)
-let add_goals_of_problem : problem -> goal list -> goal list = fun p gs ->
-  let gs = MetaSet.fold (fun m gs -> Goal.of_meta m :: gs) !p.metas gs in
-  let f gs c = Unif c :: gs in
-  let gs = List.fold_left f gs !p.to_solve in
-  List.fold_left f gs !p.unsolved
+open Goal
 
 (** Representation of the proof state of a theorem. *)
 type proof_state =
@@ -149,7 +22,7 @@ let goals : proof_state pp = fun ppf ps ->
   match ps.proof_goals with
   | [] -> out ppf "No goal."
   | g::gs ->
-      let idmap = get_names g in
+      let idmap = Goal.get_names g in
       out ppf "%a0. %a" (Goal.hyps idmap) g (Goal.concl idmap) g;
       let goal ppf i g = out ppf "\n%d. %a" (i+1) Goal.pp_no_hyp g in
       List.iteri (goal ppf) gs

src/handle/rewrite.ml

@@ -3,7 +3,7 @@
 open Lplib
 open Common open Pos open Error open Debug
 open Core open Term open Print
-open Proof
+open Goal
 
 (** Logging function for the rewrite tactic. *)
 let log = Logger.make 'r' "rewr" "the rewrite tactic"

src/handle/tactic.ml

@@ -6,6 +6,7 @@ open Parsing open Syntax
 open Core open Term open Print
 open Proof
 open Timed
+open Goal
 
 (** Logging function for tactics. *)
 let log = Logger.make 't' "tact" "tactics"
@@ -132,7 +133,7 @@ let tac_refine : ?check:bool ->
     log (Color.gre "%a ≔ %a") meta gt.goal_meta term t;
   LibMeta.set p gt.goal_meta (bind_mvar (Env.vars gt.goal_hyps) t);
   (* Convert the metas and constraints of [p] not in [gs] into new goals. *)
-  tac_solve pos {ps with proof_goals = Proof.add_goals_of_problem p gs}
+  tac_solve pos {ps with proof_goals = add_goals_of_problem p gs}
 
 (** [ind_data t] returns the [ind_data] structure of [s] if [t] is of the
    form [s t1 .. tn] with [s] an inductive type. Fails otherwise. *)
@@ -560,7 +561,7 @@ let rec handle :
               LibMeta.set p gt.goal_meta (bind_mvar (Env.vars env) u);
               (*let g = Goal.of_meta m in*)
               let g = Typ {goal_meta=m; goal_hyps=e'; goal_type=v} in
-              {ps with proof_goals = g :: Proof.add_goals_of_problem p gs}
+              {ps with proof_goals = g :: add_goals_of_problem p gs}
             end else fatal pos "The unification constraints for %a \
                             to be typable are not satisfiable." term t
       end
@@ -705,7 +706,7 @@ let handle :
   | [] -> fatal pos "No remaining goals."
   | g::_ ->
     if Logger.log_enabled() then
-      log ("Goal %a%a") Proof.Goal.pp_no_hyp g Pretty.tactic tac;
+      log ("Goal %a%a") Goal.pp_no_hyp g Pretty.tactic tac;
     handle ss sym_pos prv ps tac, None
 
 (** [handle sym_pos prv r tac n] applies the tactic [tac] from the previous

src/handle/why3_tactic.ml

@@ -5,7 +5,7 @@ open Timed
 open Common open Error
 open Core open Term open Print
 open Fol
-open Proof
+open Goal
 
 (** Logging function for external prover calling with Why3. *)
 let log = Logger.make 'y' "why3" "why3 provers"

src/handle/why3_tactic.mli

@@ -15,4 +15,4 @@ val timeout : int ref
 (** [handle ss pos ps prover_name gt] runs the Why3 prover corresponding to
     [prover_name] (if given or a default one otherwise) on the goal type [gt],
     and fails if no proof is found. *)
-val handle: Sig_state.t -> Pos.popt -> string option -> Proof.goal_typ -> unit
+val handle: Sig_state.t -> Pos.popt -> string option -> Goal.goal_typ -> unit

src/lsp/lp_doc.ml

@@ -12,6 +12,7 @@
 
 open Common
 open Lplib
+open Handle
 
 module LSP = Lsp_base
 
@@ -24,7 +25,7 @@ type doc_node =
   { ast   : Pure.Command.t
   ; exec  : bool
   (*; tactics : Proof.Tactic.t list*)
-  ; goals : (Pure.goal list * Pos.popt) list
+  ; goals : (Goal.info list * Pos.popt) list
   }
 
 (* Private. A doc is a list of nodes for now. The first element in

src/lsp/lsp_base.ml

@@ -38,20 +38,19 @@ let mk_range (p : Pos.pos) : J.t =
   `Assoc ["start", `Assoc ["line", `Int (line1 - 1); "character", `Int col1];
           "end",   `Assoc ["line", `Int (line2 - 1); "character", `Int col2]]
 
-let json_of_goal (hyps, concl) =
+let json_of_goal (hyps, typ_goal, lhs, rhs) =
   let json_of_hyp (s,t) = `Assoc ["hname", `String s; "htype", `String t] in
-  match concl with
-  | Pure.Typ (meta, typ) ->
+  if typ_goal then
     `Assoc [
       "typeofgoal", `String "Typ"
-    ; "gid", `String meta
+    ; "gid", `String lhs
     ; "hyps", `List (List.map json_of_hyp hyps)
-    ; "type", `String typ]
-  | Pure.Unif (t,u) ->
+    ; "type", `String rhs]
+  else
     `Assoc [
       "typeofgoal", `String "Unif"
     ; "hyps", `List (List.map json_of_hyp hyps)
-    ; "constr", `String (t ^ " ≡ " ^ u)]
+    ; "constr", `String (lhs ^ " ≡ " ^ rhs)]
 
 let json_of_goals ?logs goals =
   let logs = match logs with None -> "" | Some s -> s in

src/lsp/lsp_base.mli

@@ -11,6 +11,7 @@
 (************************************************************************)
 
 open Common
+open Handle
 
 module J = Yojson.Basic
 
@@ -23,7 +24,7 @@ val mk_reply : id:int -> result:J.t -> J.t
 val mk_diagnostics
   : uri:string
   -> version: int
-  -> (Pos.pos * int * string * Pure.goal list option) list
+  -> (Pos.pos * int * string * Goal.info list option) list
   -> J.t
 
-val json_of_goals : ?logs:string -> Pure.goal list option -> J.t
+val json_of_goals : ?logs:string -> Goal.info list option -> J.t

src/pure/pure.ml

@@ -81,54 +81,11 @@ type proof_finalizer = Sig_state.t -> Proof.proof_state -> Sig_state.t
 type proof_state =
   Time.t * Sig_state.t * Proof.proof_state * proof_finalizer * bool * Pos.popt
 
-type conclusion =
-  | Typ of string * string
-  | Unif of string * string
-
-type goal = (string * string) list * conclusion
-
-let string_of_goal : Proof.goal -> goal =
-  let buf = Buffer.create 80 in
-  let fmt = Format.formatter_of_buffer buf in
-  let to_string f x =
-    f fmt x;
-    Format.pp_print_flush fmt ();
-    let res = Buffer.contents buf in
-    Buffer.clear buf;
-    res
-  in
-  fun g ->
-  let open Print in
-  let ids = Proof.get_names g in
-  let term = term_in ids in
-  let env_elt (s,(_,ty,def)) =
-    let ty = to_string term (Eval.snf_beta ty) in
-    s,
-    match def with
-    | None -> ty
-    | Some d -> "≔ "^to_string term d
-  in
-  let ctx_elt (x,ty,def) =
-    let ty = to_string term (Eval.snf_beta ty) in
-    to_string var x,
-    match def with
-    | None -> ty
-    | Some d -> "≔ "^to_string term d
-  in
-  match g with
-  | Proof.Typ gt ->
-      let meta = "?"^to_string int gt.goal_meta.meta_key in
-      let typ = to_string term (Eval.snf_beta gt.goal_type) in
-      List.rev_map env_elt gt.goal_hyps, Typ (meta, typ)
-  | Proof.Unif (c,t,u) ->
-      let t = to_string term t and u = to_string term u in
-      List.rev_map ctx_elt c, Unif (t,u)
-
-let current_goals : proof_state -> goal list =
+let current_goals : proof_state -> Goal.info list =
   fun (time, st, ps, _, _, _) ->
   Time.restore time;
   Print.sig_state := st;
-  List.map string_of_goal ps.proof_goals
+  List.map Goal.to_info ps.proof_goals
 
 type command_result =
   | Cmd_OK    of state * string option