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 * Types.ty (* l (M : t) *)
  | HRight of hlam * Types.ty (* r (M : t) *)
  | 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, t) -> HLeft (clean h, t)
    | HRight (h, t) -> HRight (clean h, t)
    | 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 (e1, e2) ->
    HPair (hlam_of_lam e1, hlam_of_lam e2)
  | Left (e, t) ->
    HLeft (hlam_of_lam e, t)
  | Right (e, t) ->
    HRight (hlam_of_lam 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)
  | HPair (e1, e2) ->
    Pair (lam_of_hlam e1, lam_of_hlam e2)
  | HLeft (e, t) ->
    Left (lam_of_hlam e, t)
  | HRight (e, t) ->
    Right (lam_of_hlam e, t)
  | Ref e_ref -> lam_of_hlam !e_ref
  | Hole -> raise (TacticFailed "can not translate unclosed terms")