From 4719e2c836f615fc13250183c8afc3bb40931e31 Mon Sep 17 00:00:00 2001
From: Marwan <marwan.azizi@ens-lyon.fr>
Date: Fri, 17 May 2024 21:28:02 +0200
Subject: [PATCH] =?UTF-8?q?impl=C3=A9mentation=20de=20la=20tactique=20Chec?=
 =?UTF-8?q?k=20pour=20envoyer=20la=20preuve=20=C3=A0=20Coq?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 dune            |  2 +-
 lexer.mll       |  1 +
 main.ml         | 61 ++++++++++++++++++++++++++++++++++++++++++++++++-
 parser.mly      |  3 ++-
 parser_entry.ml |  1 +
 types.ml        |  2 +-
 6 files changed, 66 insertions(+), 4 deletions(-)

diff --git a/dune b/dune
index 55542a5..f9498d6 100644
--- a/dune
+++ b/dune
@@ -1,6 +1,6 @@
 (executable
  (name main)
- (libraries str))
+ (libraries str unix))
 
 (ocamllex lexer)
 (menhir
diff --git a/lexer.mll b/lexer.mll
index b836aa9..6e785dd 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -32,6 +32,7 @@ rule token = parse
   | "Goal"          { GOAL }
   | "Undo"          { UNDO }
   | "Qed"           { QED }
+  | "Check"          { CHECK }
   | "exact"         { EXACT }
   | "assumption"    { ASSUMPTION }
   | "intros"        { INTROS }
diff --git a/main.ml b/main.ml
index e5c7de6..a420b3a 100644
--- a/main.ml
+++ b/main.ml
@@ -3,6 +3,8 @@ open Affichage
 open Proof
 open Types
 open Hlam
+open Lam
+
 
 type entry =
   Simple of (unit -> instr)
@@ -11,6 +13,8 @@ type entry =
 
 type interactive_state = (hlam * ty) option * proof
 
+module StringMap = Map.Make(String)
+
 let parse_lam t =
   match Parser.main Lexer.token t with
   | Lam l -> l
@@ -55,6 +59,49 @@ let alpha_get_lam where_from =
         )
     | _ -> failwith "Alpha-equivalence: nombre de delimiteurs incorrect"
 
+let check_via_coq (e : lam) (t : ty) : unit =
+  (* fill a map to track all types used in the proof *)
+  let rec fill_ty_map (m : int StringMap.t) = function
+    TVar x -> StringMap.add x 0 m
+    | Arr(t1, t2) | Or(t1, t2) | And(t1, t2) ->
+      let m1 = fill_ty_map m t1 in
+      fill_ty_map m1 t2
+    | Bot -> m
+  (* generate the "forall A B.." *)
+  in let intro_of_ty (m : int StringMap.t) : string * int =
+    let tys = StringMap.to_list m in
+    let n = List.length tys in
+    let s = List.fold_left (fun acc x -> (fst x ^ " ") ^ acc) "" tys in
+    if n = 0
+    then ("", 0)
+    else ("forall " ^ s ^ ", ", n)
+  (* generate the right amount of intro. to introduce type variables*)
+  in let rec repeat_intro n =
+    if n = 0
+    then ""
+    else "intro. " ^ repeat_intro (n-1)
+  in
+  let m = fill_ty_map StringMap.empty t in
+  let (ty_vars, intro_n) = intro_of_ty m in
+  let goal_ty = string_of_ty t in
+  let proof_term = "(" ^ string_of_expr e ^ ")" in
+  let checker_file = open_out "checker.v" in
+  let _ =
+  Printf.fprintf checker_file "Goal %s%s.\n%s\n exact %s.\n"
+  ty_vars goal_ty (repeat_intro intro_n) proof_term;
+  close_out checker_file in
+  (* start Coq in interactive mode and send it the proof term
+     while blocking coqtop to print on stdout *)
+  let r = Unix.system "coqtop < checker.v > log 2>&1" in
+  match r with
+  Unix.WEXITED x ->
+    if x = 0
+    then print_error "Validated by Coq." ""
+    else print_error "Couldn't not validate proof." ""
+  | _ -> print_error "Coq failed." ""
+
+
+
 (** Interactive loop
   - cg : current top goal : type and reference to lambda-term
   - g, gs : next goals
@@ -87,7 +134,7 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
               |> beta_reduce in
               if Typing.typecheck [] l t then begin
                 print_string "Ok";
-                [None, (None, [])] |> interactive get_instr
+                (cg, (g, gs))::sq |> interactive get_instr
               end else begin
                 print_error "Typing failed" "";
                 print_expr l;
@@ -96,6 +143,18 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
                 (cg, (g, gs))::sq |> interactive get_instr
               end
             end
+          | Check -> begin match cg with
+            None ->
+              print_error "No current goal" "";
+              (cg, (g, gs))::sq |> interactive get_instr
+            | Some (h, t) ->
+              begin try
+                let l = lam_of_hlam h in
+                check_via_coq l t
+              with _ -> print_error "Proof is not over" "";
+              end;
+              (cg, (g, gs))::sq |> interactive get_instr;
+          end
         end
       | Tact t ->
         (cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive get_instr
diff --git a/parser.mly b/parser.mly
index cc7e38c..929ee46 100644
--- a/parser.mly
+++ b/parser.mly
@@ -15,7 +15,7 @@ open Parser_entry
 %token <string> VARID
 %token <string> TYID
 
-%token GOAL UNDO QED
+%token GOAL UNDO QED CHECK
 %token EXACT ASSUMPTION INTRO INTROS CUT APPLY
 %token LEFT RIGHT SPLIT TRY
 %token L R
@@ -42,6 +42,7 @@ command:
   | GOAL t=ty             { Goal t }
   | UNDO                  { Undo }
   | QED                   { Qed }
+  | CHECK                 { Check }
 
 tactic:
   | EXACT e=expression    { TExact_term e }
diff --git a/parser_entry.ml b/parser_entry.ml
index a1578ec..32f334b 100644
--- a/parser_entry.ml
+++ b/parser_entry.ml
@@ -6,6 +6,7 @@ type cmd =
   Goal of ty
   | Undo
   | Qed
+  | Check
 
 type instr =
   Cmd of cmd
diff --git a/types.ml b/types.ml
index 6b319be..5d88039 100644
--- a/types.ml
+++ b/types.ml
@@ -1,7 +1,7 @@
 type ty_id = string
 
 type ty =
-  TVar of ty_id
+  TVar of string
   | Arr of ty * ty
   | And of ty * ty
   | Or of ty * ty