pieuvre/proof.ml

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