228 lines
7.0 KiB
OCaml
228 lines
7.0 KiB
OCaml
open Hlam
|
|
open Lam
|
|
open Types
|
|
|
|
type context = (id * id * hlam * Types.ty) list
|
|
type goal = hlam * Types.ty * context
|
|
type proof = goal option * goal list
|
|
|
|
type tactic =
|
|
TExact_term of lam
|
|
| TExact_proof of id
|
|
| TAssumption
|
|
| TIntros
|
|
| TIntro
|
|
| TCut of ty
|
|
| TApply of id
|
|
| TSplit
|
|
| TRight
|
|
| TLeft
|
|
| TTry of tactic
|
|
|
|
let hyp_count = ref 0
|
|
let get_fresh_hyp () =
|
|
let n = string_of_int !hyp_count in
|
|
incr hyp_count;
|
|
let hyp_id = "H" ^ n in
|
|
let var_id = "x_" ^ n in
|
|
(hyp_id, var_id)
|
|
|
|
(** replace ref's in a proof *)
|
|
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)
|
|
let clean_goal assoc ((h, t, c) : goal) : goal =
|
|
(clean_hlam assoc h, t, clean_context assoc c)
|
|
let clean_proof ((g, gs) : proof) : (hlam ref * hlam ref) list ref * proof =
|
|
let assoc = ref [] in
|
|
let g' = match g with
|
|
| Some g -> Some (clean_goal assoc g)
|
|
| None -> None
|
|
in assoc, (g', List.map (clean_goal assoc) gs)
|
|
|
|
(* typecheck e t cs types e against t in the typing environment defined
|
|
by cs *)
|
|
let typecheck (e : lam) (expected_t : Types.ty) (cs : context) : bool =
|
|
let gam_of_ctx : context -> Types.gam =
|
|
(fun (_, var_id, _, ty) -> (var_id, ty)) |>
|
|
List.map
|
|
in
|
|
let g = gam_of_ctx cs in
|
|
try Typing.typecheck g e expected_t
|
|
with Typing.Could_not_infer -> raise (TacticFailed "couldn't not infer all variable types")
|
|
|
|
let rec get_term_by_id (hyp : id) : context -> hlam option =
|
|
function
|
|
[] -> None
|
|
| (hyp',_, h, _) :: _ when hyp' = hyp -> Some h
|
|
| _ :: cs -> get_term_by_id hyp cs
|
|
|
|
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 get_goal : goal option -> hlam * ty * context =
|
|
function
|
|
None -> raise (TacticFailed "no current goal")
|
|
| Some g -> g
|
|
|
|
let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
|
|
let (h, expected_t, cs) = get_goal g in
|
|
if typecheck e expected_t cs
|
|
then
|
|
begin
|
|
fill h (hlam_of_lam e);
|
|
next_goal gs
|
|
end
|
|
else raise (TacticFailed "type mismatch")
|
|
|
|
let tact_exact_proof ((g, gs) : proof) (hyp : id) : proof =
|
|
let (h, expected_t, cs) = get_goal g in
|
|
match get_term_by_id hyp cs with
|
|
Some h' ->
|
|
if typecheck (lam_of_hlam h') expected_t cs
|
|
then
|
|
begin
|
|
fill h h';
|
|
next_goal gs
|
|
end
|
|
else raise (TacticFailed "type mismatch")
|
|
| None -> raise (TacticFailed "")
|
|
|
|
let tact_assumption ((g, gs) : proof) : proof =
|
|
let (h, goal_ty, cs) = get_goal g in
|
|
match get_term_by_type goal_ty cs with
|
|
None -> raise (TacticFailed "no such hypothesis")
|
|
| Some h' ->
|
|
fill h h';
|
|
next_goal gs
|
|
|
|
let tact_intro ((g, gs) : proof) : proof =
|
|
let (h, goal_ty, cs) = get_goal g in
|
|
match goal_ty with
|
|
Arr (t1, t2) ->
|
|
let (hyp_id, var_id) = get_fresh_hyp () in
|
|
let cs = (hyp_id, var_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
|
|
| _ -> raise (TacticFailed "expected an implication")
|
|
|
|
let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
|
|
let (h, goal_ty, cs) = get_goal g in
|
|
(* 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 =
|
|
(* check if hypothesis suits apply *)
|
|
let rec is_implied (goal_ty : ty) (t : ty) : bool =
|
|
match t with
|
|
t when t = goal_ty -> true
|
|
| Arr (_, t2) -> is_implied goal_ty t2
|
|
| _ -> false
|
|
in
|
|
(* supposes is_implied goal_ty impl_ty
|
|
goal_ty : conclusion of the implication
|
|
impl_ty : type of the implication
|
|
impl_h : building the term we will apply to goal_h
|
|
goal_h : hole of the current goal
|
|
h : current hole of impl_h*)
|
|
let rec generate_goals (goal_ty : ty) (impl_ty : ty) (impl_h : hlam)
|
|
(goal_h : hlam) (h : hlam) (cs : context) (gs : goal list) : proof =
|
|
match impl_ty with
|
|
Arr (t1, t2) when t2 = goal_ty ->
|
|
let sub_h = Ref (ref Hole) in
|
|
let _ = fill h sub_h in
|
|
let _ = fill goal_h impl_h in
|
|
Some (sub_h, t1, cs), gs
|
|
| Arr (t1, t2) ->
|
|
(* transforms impl_h from ((f ?x_0) ?) to (((f ?x_0) ?x_1) ?)
|
|
where ? is h and ?x_i are holes associated with
|
|
the proof of x_i*)
|
|
let sub_h = Ref (ref Hole) in (* proof of t1 *)
|
|
let new_h = Ref (ref Hole) in (* proof of t2 *)
|
|
let _ = fill h sub_h in
|
|
let impl_h = HApp (impl_h, new_h) in
|
|
let gs = (sub_h, t1, cs) :: gs in (* add the proof of t1 to goals *)
|
|
generate_goals goal_ty t2 impl_h goal_h new_h cs gs (* generate_goals for the proof of t2 *)
|
|
| _ -> failwith "impossible"
|
|
in
|
|
let rec get_hyp : context -> (hlam * ty) = function
|
|
[] -> raise (TacticFailed "no such hypothesis in context")
|
|
| (hyp_id', _, h', t') :: _ when hyp_id = hyp_id' -> (h', t')
|
|
| _ :: cs -> get_hyp cs
|
|
in
|
|
let (goal_h, goal_ty, cs) = get_goal g in
|
|
let impl_h, impl_ty = get_hyp cs in
|
|
let new_h = Ref (ref Hole) in
|
|
let impl_h_2 = HApp (impl_h, new_h) in
|
|
if is_implied goal_ty impl_ty
|
|
then generate_goals goal_ty impl_ty impl_h_2 goal_h new_h cs gs
|
|
else raise (TacticFailed "not an implication")
|
|
|
|
let tact_intros : proof -> proof =
|
|
let rec push (p : proof) =
|
|
try
|
|
let p = tact_intro p in
|
|
push p
|
|
with TacticFailed _ -> p
|
|
in push
|
|
|
|
let tact_split ((g, gs) : proof) : proof =
|
|
let (h, goal_ty, cs) = get_goal g in
|
|
match goal_ty with
|
|
| And(t1, t2) ->
|
|
let h1 = Ref (ref Hole) in
|
|
let h2 = Ref (ref Hole) in
|
|
fill h (HPair (h1, h2));
|
|
Some (h1, t1, cs), (h2, t2, cs)::gs
|
|
| _ -> raise (TacticFailed "Not a conjonction")
|
|
|
|
|
|
let tact_right ((g, gs) : proof) : proof =
|
|
let (h, goal_ty, cs) = get_goal g in
|
|
match goal_ty with
|
|
| Or(_, t_r) as t ->
|
|
let new_h = Ref (ref Hole) in
|
|
fill h (HRight (new_h, t));
|
|
Some (new_h, t_r, cs), gs
|
|
| _ -> raise (TacticFailed "Not a disjunction")
|
|
|
|
let tact_left ((g, gs) : proof) : proof =
|
|
let (h, goal_ty, cs) = get_goal g in
|
|
match goal_ty with
|
|
| Or(t_l, _) as t->
|
|
let new_h = Ref (ref Hole) in
|
|
fill h (HLeft (new_h, t));
|
|
Some (new_h, t_l, cs), gs
|
|
| _ -> raise (TacticFailed "Not a disjunction")
|
|
|
|
(* applies tactic to proof, returns (new_proof, true if p changed) *)
|
|
let rec apply_tactic (p : proof) (t : tactic) : proof * bool =
|
|
match t with
|
|
TExact_term e -> tact_exact_term p e, true
|
|
| TExact_proof hyp -> tact_exact_proof p hyp, true
|
|
| TIntros -> tact_intros p, true
|
|
| TIntro -> tact_intro p, true
|
|
| TAssumption -> tact_assumption p, true
|
|
| TCut t -> tact_cut p t, true
|
|
| TApply h -> tact_apply p h, true
|
|
| TSplit -> tact_split p, true
|
|
| TRight -> tact_right p, true
|
|
| TLeft -> tact_left p, true
|
|
| TTry t -> try apply_tactic p t with TacticFailed _ -> p, false
|
|
|