From b26ea09640236159d9837d5172ac8fe3f0334e0d Mon Sep 17 00:00:00 2001
From: augustin64 <me.git@augustin64.fr>
Date: Thu, 16 May 2024 12:38:45 +0200
Subject: [PATCH] Split proof.ml with hlam.ml

---
 affichage.ml |  1 +
 hlam.ml      | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++
 main.ml      |  1 +
 proof.ml     | 79 ++--------------------------------------------------
 4 files changed, 82 insertions(+), 77 deletions(-)
 create mode 100644 hlam.ml

diff --git a/affichage.ml b/affichage.ml
index 24f9c3d..ec929f9 100644
--- a/affichage.ml
+++ b/affichage.ml
@@ -1,6 +1,7 @@
 open Lam
 open Types
 open Proof
+open Hlam
 
 (* fonction d'affichage *)
 let rec string_of_ty = function
diff --git a/hlam.ml b/hlam.ml
new file mode 100644
index 0000000..5b3281c
--- /dev/null
+++ b/hlam.ml
@@ -0,0 +1,78 @@
+open Lam
+
+exception TacticFailed of string
+
+type hlam = (* hollow lam *)
+  HFun of (id * Types.ty) * hlam
+  | HApp of hlam * hlam
+  | HVar of id
+  | HExf of hlam * Types.ty
+  | HPair of hlam * hlam
+  | HLeft of hlam
+  | HRight of hlam
+  | Ref of hlam ref
+  | Hole
+
+
+let clean_hlam assoc (h : hlam) : hlam =
+  let rec clean (h : hlam) : hlam= match h with
+    HFun ((s, t), h) -> HFun ((s, t), clean h)
+    | Hole -> Hole
+    | HApp (h1, h2) -> HApp (clean h1, clean h2)
+    | HVar s -> HVar s
+    | HExf (h, t) -> HExf (clean h, t)
+    | HPair (h1, h2) -> HPair (clean h1, clean h2)
+    | HLeft h -> HLeft (clean h)
+    | HRight h -> HRight (clean h)
+    | Ref (hr) ->
+      match List.assq_opt hr !assoc with
+        None -> let new_h = ref (clean !hr)
+          in (assoc := (hr, new_h)::!assoc;
+          Ref new_h)
+        | Some new_h -> Ref new_h
+  in clean h
+
+let fill (hole : hlam) (e : hlam) : unit =
+  match hole with
+  Ref h -> h := e
+  | _ -> raise (TacticFailed "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)
+  | Pair (l1, l2) ->
+    HPair (hlam_of_lam l1, hlam_of_lam l2)
+  | Left l ->
+    HLeft (hlam_of_lam l)
+  | Right l ->
+    HRight (hlam_of_lam l)
+
+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)
+  | HPair (h1, h2) ->
+    Pair (lam_of_hlam h1, lam_of_hlam h2)
+  | HLeft h ->
+    Left (lam_of_hlam h)
+  | HRight h ->
+    Right (lam_of_hlam h)
+  | Ref e_ref -> lam_of_hlam !e_ref
+  | Hole -> raise (TacticFailed "can not translate unclosed terms")
diff --git a/main.ml b/main.ml
index 4e6d6d5..d57f53b 100644
--- a/main.ml
+++ b/main.ml
@@ -2,6 +2,7 @@ open Parser_entry
 open Affichage
 open Proof
 open Types
+open Hlam
 
 type entry =
   Simple of (unit -> cmd)
diff --git a/proof.ml b/proof.ml
index 133deaf..ed311c6 100644
--- a/proof.ml
+++ b/proof.ml
@@ -1,18 +1,6 @@
+open Hlam
 open Lam
-open Types
-
-exception TacticFailed of string
-
-type hlam = (* hollow lam *)
-  HFun of (id * Types.ty) * hlam
-  | HApp of hlam * hlam
-  | HVar of id
-  | HExf of hlam * Types.ty
-  | HPair of hlam * hlam
-  | HLeft of hlam
-  | HRight of hlam
-  | Ref of hlam ref
-  | Hole
+  open Types
 
 type context = (id * id * hlam * Types.ty) list
 type goal = hlam * Types.ty * context
@@ -39,23 +27,6 @@ let get_fresh_hyp () =
   (hyp_id, var_id)
 
 (** replace ref's in a proof *)
-let clean_hlam assoc (h : hlam) : hlam =
-  let rec clean (h : hlam) : hlam= match h with
-    HFun ((s, t), h) -> HFun ((s, t), clean h)
-    | Hole -> Hole
-    | HApp (h1, h2) -> HApp (clean h1, clean h2)
-    | HVar s -> HVar s
-    | HExf (h, t) -> HExf (clean h, t)
-    | HPair (h1, h2) -> HPair (clean h1, clean h2)
-    | HLeft h -> HLeft (clean h)
-    | HRight h -> HRight (clean h)
-    | Ref (hr) ->
-      match List.assq_opt hr !assoc with
-        None -> let new_h = ref (clean !hr)
-          in (assoc := (hr, new_h)::!assoc;
-          Ref new_h)
-        | Some new_h -> Ref new_h
-  in clean h
 let rec clean_context assoc (c : context) : context = match c with
   [] -> []
   | (s1, s2, h, t)::q -> (s1, s2, clean_hlam assoc h, t)::(clean_context assoc q)
@@ -73,52 +44,6 @@ let goal_is_over ((g, _) : proof) : bool =
   None -> true
   | Some _ -> false
 
-let fill (hole : hlam) (e : hlam) : unit =
-  match hole with
-  Ref h -> h := e
-  | _ -> raise (TacticFailed "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)
-  | Pair (l1, l2) ->
-    HPair (hlam_of_lam l1, hlam_of_lam l2)
-  | Left l ->
-    HLeft (hlam_of_lam l)
-  | Right l ->
-    HRight (hlam_of_lam l)
-
-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)
-  | HPair (h1, h2) ->
-    Pair (lam_of_hlam h1, lam_of_hlam h2)
-  | HLeft h ->
-    Left (lam_of_hlam h)
-  | HRight h ->
-    Right (lam_of_hlam h)
-  | Ref e_ref -> lam_of_hlam !e_ref
-  | Hole -> raise (TacticFailed "can not translate unclosed terms")
-
-
 let typecheck (e : lam) (expected_t : Types.ty) (cs : context) : bool =
   let gam_of_ctx : context -> Types.gam =
     let f = fun (_, var_id, _, ty) -> (var_id, ty) in