l3-ENSL/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Split proof.ml with hlam.ml

Browse Source
This commit is contained in:
augustin64 2024-05-16 12:38:45 +02:00
parent 543da0b297
commit b26ea09640
4 changed files with 82 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
affichage.ml
View File

@ -1,6 +1,7 @@
open Lam open Lam
open Types open Types
open Proof open Proof
open Hlam
(* fonction d'affichage *) (* fonction d'affichage *)
let rec string_of_ty = function let rec string_of_ty = function

78
hlam.ml Normal file
View File

@ -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")

1
main.ml
View File

@ -2,6 +2,7 @@ open Parser_entry
open Affichage open Affichage
open Proof open Proof
open Types open Types
open Hlam
type entry = type entry =
Simple of (unit -> cmd) Simple of (unit -> cmd)

77
proof.ml
View File

@ -1,19 +1,7 @@
open Hlam
open Lam open Lam
open Types 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
type context = (id * id * hlam * Types.ty) list type context = (id * id * hlam * Types.ty) list
type goal = hlam * Types.ty * context type goal = hlam * Types.ty * context
type proof = goal option * goal list type proof = goal option * goal list
@ -39,23 +27,6 @@ let get_fresh_hyp () =
(hyp_id, var_id) (hyp_id, var_id)
(** replace ref's in a proof *) (** 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 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) | (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 None -> true
| Some _ -> false | 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 typecheck (e : lam) (expected_t : Types.ty) (cs : context) : bool =
let gam_of_ctx : context -> Types.gam = let gam_of_ctx : context -> Types.gam =
let f = fun (_, var_id, _, ty) -> (var_id, ty) in let f = fun (_, var_id, _, ty) -> (var_id, ty) in