implémentation de la tactique Check pour envoyer la preuve à Coq

dune

@@ -1,6 +1,6 @@
 (executable
  (name main)
- (libraries str))
+ (libraries str unix))
 
 (ocamllex lexer)
 (menhir

lexer.mll

@@ -32,6 +32,7 @@ rule token = parse
   | "Goal"          { GOAL }
   | "Undo"          { UNDO }
   | "Qed"           { QED }
+  | "Check"          { CHECK }
   | "exact"         { EXACT }
   | "assumption"    { ASSUMPTION }
   | "intros"        { INTROS }

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

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 }

parser_entry.ml

@@ -6,6 +6,7 @@ type cmd =
   Goal of ty
   | Undo
   | Qed
+  | Check
 
 type instr =
   Cmd of cmd

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