From 7195fc244fa90709d80374ffea7b5956a2724e86 Mon Sep 17 00:00:00 2001
From: Marwan <marwan.azizi@ens-lyon.fr>
Date: Thu, 25 Apr 2024 10:11:08 +0200
Subject: [PATCH] =?UTF-8?q?ajout=20du=20syst=C3=A8me=20de=20preuve=20et=20?=
 =?UTF-8?q?impl=C3=A9mentation=20des=20tactiques=20exact,=20intro,=20cut?=
 =?UTF-8?q?=20et=20apply?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Makefile |   2 +-
 proof.ml | 131 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 132 insertions(+), 1 deletion(-)
 create mode 100644 proof.ml

diff --git a/Makefile b/Makefile
index a03c10b..c7e1974 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-pieuvre: main.ml lam.ml affichage.ml lexer.mll parser.mly
+pieuvre: main.ml proof.ml lam.ml affichage.ml lexer.mll parser.mly
 	dune build
 	cp _build/default/main.exe pieuvre
 	chmod +w pieuvre
diff --git a/proof.ml b/proof.ml
new file mode 100644
index 0000000..87ae43f
--- /dev/null
+++ b/proof.ml
@@ -0,0 +1,131 @@
+open Lam
+open Types
+
+type hlam = (* hollow lam *)
+  HFun of (id * Types.ty) * hlam
+  | HApp of hlam * hlam
+  | HVar of id
+  | HExf of hlam * Types.ty
+  | Ref of hlam ref
+  | Hole
+
+type context = (id * hlam * Types.ty) list
+type goal = hlam * Types.ty * context
+type proof = goal option * goal list
+
+let count = ref 0
+let get_fresh_hyp () =
+  let n = string_of_int !count in
+  let hyp_id = "H" ^ n in
+  let var_id = "x_" ^ n in
+  (hyp_id, var_id)
+
+let proof_is_over ((g, _) : proof) : bool =
+  match g with
+  None -> true
+  | Some _ -> false
+
+let fill (hole : hlam) (e : hlam) : unit =
+  match hole with
+  Ref h -> h := e
+  | _ -> failwith "not fillable"
+
+let rec hlam_of_lam : lam -> hlam = function
+  Fun ((x, t), e) ->
+    let e = hlam_of_lam e in
+    HFun ((x, t), e)
+  | App (e1, e2) ->
+    let e1 = hlam_of_lam e1 in
+    let e2 = hlam_of_lam e2 in
+    HApp (e1, e2)
+  | Var x -> HVar x
+  | Exf (e, t) ->
+    let e = hlam_of_lam e in
+    HExf (e, t)
+
+let rec lam_of_hlam : hlam -> lam = function
+  HFun ((x, t), e) ->
+    let e = lam_of_hlam e in
+    Fun ((x, t), e)
+  | HApp (e1, e2) ->
+    let e1 = lam_of_hlam e1 in
+    let e2 = lam_of_hlam e2 in
+    App (e1, e2)
+  | HVar x -> Var x
+  | HExf (e, t) ->
+    let e = lam_of_hlam e in
+    Exf (e, t)
+  | Ref e_ref -> lam_of_hlam !e_ref
+  | Hole -> failwith "can not translate unclosed terms"
+
+let rec get_term_by_type (ty : Types.ty) : context -> hlam option =
+  function
+  [] -> None
+  | (_, h, ty') :: _ when ty' = ty -> Some h
+  | _ :: cs -> get_term_by_type ty cs
+
+let next_goal (gs : goal list) : (goal option * goal list) =
+  match gs with
+  [] -> None, []
+  | g :: gs -> Some g, gs
+
+let tact_exact ((g, gs) : proof) (e : lam) : proof =
+  match g with
+  None -> failwith "no current goal"
+  | Some (h, _, _) ->
+    fill h (hlam_of_lam e);
+    next_goal gs
+
+let tact_assumption ((g, gs) : proof) : proof =
+  match g with
+  None -> failwith "no current goal"
+  | Some (h, goal_ty, cs) ->
+    match get_term_by_type goal_ty cs with
+    None -> (* failwith "assumption failed" *) (g, gs)
+    | Some h' ->
+      fill h h';
+      next_goal gs
+
+let tact_intro ((g, gs) : proof) : proof =
+  match g with
+  None -> failwith "no current goal"
+  | Some (h, goal_ty, cs) ->
+    match goal_ty with
+    Arr (t1, t2) ->
+      let (hyp_id, var_id) = get_fresh_hyp () in
+      let cs = (hyp_id, HVar var_id, t1) :: cs in
+      let new_h = Ref (ref Hole) in
+      fill h (HFun ((var_id, t1), new_h));
+      Some (new_h, t2, cs), gs
+    | _ -> (* failwith "expected function" *) (g, gs)
+
+let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
+  match g with
+  None -> failwith "no current goal"
+  | Some (h, goal_ty, cs) ->
+    (* subgoal 2 : new_t -> goal_ty *)
+    let arrow_h = Ref (ref Hole) in
+    let arrow_goal = (arrow_h, Arr (new_t, goal_ty), cs) in
+    let gs = arrow_goal :: gs in
+    (* subgoal 1 (main goal) : new_t *)
+    let new_h = Ref (ref Hole) in
+    fill h (HApp (arrow_h, new_h));
+    Some (new_h, new_t, cs), gs
+
+let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
+  let rec get_hyp = function
+    [] -> failwith "no such hypothesis in context"
+    | (hyp_id', h', t') :: _ when hyp_id = hyp_id' -> (h', t')
+    | _ :: cs -> get_hyp cs
+  in
+  match g with
+  None -> failwith "no current goal"
+  | Some (h, goal_ty, cs) ->
+    let h', t' = get_hyp cs in
+    match t' with
+    Arr (t1, t2) when t2 = goal_ty ->
+      let new_h = Ref (ref Hole) in
+      fill h (HApp (h', new_h));
+      Some (new_h, t1, cs), gs
+    | Arr _ -> (* failwith "wrong types" *) (g, gs)
+    | _ -> (* failwith "expected ->" *) (g, gs)