Require Import MetaCoq.Template.All Strings.Ascii.
From Undecidability.L.Tactics Require Import Lproc Computable Lsimpl Lbeta Lrewrite.
Require Export Ring Arith Lia.
Import L_Notations.

Module Intern.

Ltac visibleHead t :=
  match t with
    ?h _ visibleHead h
  | _ t
  end.

Ltac fold_encs :=
  match goal with
    x:_ |- _
    revert x;fold_encs;intros x;
    let H := fresh "H" in
    try (assert (H:@enc _ _ x= @enc _ _ x) by reflexivity;
         try (unfold enc in H at 1; cbn in H;rewrite !H);clear H)
  | _ idtac
  end.

Ltac recRem P:=
  match goal with
  | |- context[ ?s]
    let rP := fresh "rP" in
    set (rP:=s);
    assert (proc rP);[unfold rP;solve [Lproc]|
                      set (P := rP);
                      assert (proc P);[unfold P;solve [Lproc]|]]
end.

Ltac recStepInit P:=
   once lazymatch eval lazy [P] in P with
   | ?rP
     once lazymatch goal with
     | |- eval _ _
       let rec loop :=
           once lazymatch goal with
           | |- ARS.star step (app P _) _ unfold P;apply rho_correct;now Lproc
           | |- ARS.star step (app _ _) _ eapply star_step_app_proper;[loop|reflexivity]
           end
       in
       eapply eval_helper;[loop|fold P; unfold rP]
     end
   end.

Ltac recStepNew P := recStepInit P.

Ltac destructRefine :=
  once lazymatch goal with
    |- ?R ?s _
    match s with
    | context C [match ?x with _ _ end]
      let t := type of x in
      refine (_:R _ (( y:t ltac:(destruct y)) x));
      
      once lazymatch goal with
        |- (?R' ?i ? ?) tryif is_evar i then
          refine (_:R' (( (y:t) ltac:(destruct y)) x ) )
        else idtac
      | _ idtac
      end;
      once lazymatch goal with
       | |- ? ?i ?s ?t
         let i':= eval cbn in i in
             refine (_: i' s t) + match goal with |- ?G let G' := constr:( i' s t) in idtac "could not refine" G "with" G' end
       | _ idtac
      end;
      let eq := fresh "eq" in destruct x eqn:eq
    end
  end.

Ltac shelveIfUnsolved msg:= first[let n:= numgoals in guard n=0|
                                  match goal with
                                    |- ?G idtac "Could not solve some subgoal("msg"):";idtac G;shelve
                                  end].

Ltac ugly_fix_fix IH n :=
  
  once lazymatch eval cbn in n with
    0 fix IH 1
  | 1 fix IH 4
  | 2 fix IH 7
  | 3 fix IH 10
  | _ let m := eval cbn in (1+3*n) in
            fail 1000 "please add '| "n" fix IH"m"'" " in the definition of Ltac-tactic ugly_fix_fix!"
  end.

Ltac cstep' extractSimp:=
  let x := fresh "x" in
  once lazymatch goal with
  | |- computes _ _ (match ?x with _ _ end)
    let eq := fresh "eq" in destruct x eqn:eq
  | |- computes (TyArr ? ?) ?f ?intF
    let fRep := constr:(ltac:(quote_term f ( x exact x))) in
    once lazymatch fRep with
      
      Ast.tFix (_::_::_) fail 1000 "mutual recursion not supported"
    | Ast.tFix [BasicAst.mkdef _ _ _ _ ?recArg] 0
      (let P := fresh "P" in
      recRem P;
      eapply computesExpStart;[solve [Lproc]|];
      let n:= (eval cbn in (S recArg)) in
      let rec step n:=
          (once lazymatch n with
           | S ?n
              eexists;
              eapply computesExpStep;[try recStep P;extractSimp;shelveIfUnsolved "pos5"|Lproc;shelveIfUnsolved "pos6"|];
              
              let x := fresh "x" in
              let xInt := fresh x "Int" in
              let xInts := fresh x "Ints" in
              intros x xInt xInts;
              change xInt with (@ext _ _ x (Build_computable xInts));
              once lazymatch type of xInts with
                computes (@TyB _ ?reg) _ _
                rewrite (ext_is_enc (Build_computable xInts)) in *;
                clear xInt xInts;assert (xInt:True) by constructor; assert (xInts:True) by constructor
              | computes (TyArr _ _) _ _ idtac
              end;
              step n;
              revert x xInt xInts
           | 0 idtac
           end) in
      step n;
        let IH := fresh "IH" P in
        ugly_fix_fix IH recArg;
          let rec loop n :=
              once lazymatch n with
                0 intros [] ? ?
              | S ?n' intros ? ? ?;loop n'
              end in
          loop recArg;
          eexists;
          (split;[try recStepNew P;extractSimp;shelveIfUnsolved "pos7"|]))

    
    | _
      let xInt := fresh x "Int" in
      let xNorm := fresh x "Norm" in
      let xInts := fresh x "Ints" in
      let vProc := fresh "vProc" in
      
      eapply computesTyArr;[try Lproc;shelveIfUnsolved "pos1"|idtac];
      intros x xInt xInts;
      change xInt with (@ext _ _ x (Build_computable xInts));
      once lazymatch with
        TyB _ rewrite (ext_is_enc (Build_computable xInts)) in *;
                clear xInt xInts;assert (xInt:True) by constructor; assert (xInts:True) by constructor
      | _ idtac
      end;
      eexists;split;[extractSimp;shelveIfUnsolved "pos2" | intros vProc]
    end

  | |- computes (TyB _) _ ?t has_no_evar t;apply computesTyB

  | |- computes _ _ (@ext _ _) apply extCorrect

  end.

Tactic Notation "progress'" tactic(t) :=
  once lazymatch goal with
    | |- ?R ?s _ idtac "now";print_goal;
    t tt;idtac"then";print_goal;
    once lazymatch goal with
      |- R s _ fail "noprogress"
    | |- _ idtac
    end
  end.

Ltac extractCorrectCrush :=
  idtac;
   try Lsimpl;try Lreflexivity;
   try repeat' (repeat' Intern.destructRefine;Lsimpl;try Lreflexivity);
  try Lreflexivity.

Ltac extractSimple :=
  lazymatch goal with
    |- eval _ _ extractCorrectCrush
  | |- ?G idtac "cstep found unexpected" G
  end;try (idtac;[idtac "could not simplify some occuring term, shelved instead"];shelve).

Ltac cstep := cstep' extractSimple.

Ltac computable_match:=
  intros;
  once lazymatch goal with
  | |- ?R ?lhs ?rhs
    once lazymatch lhs with
    | context C [@enc _ ?reg ?x]
      induction x;
      let encf := (eval hnf in (@enc _ reg)) in
      change (@enc _ reg) with encf;
      cbn -[enc];
      repeat change encf with (@enc _ reg);
      fold_encs;
      once lazymatch goal with
      | |- _ >(<= _ ) _ Lreduce;try Lreflexivity
      | |- _ >(_) _ repeat progress Lbeta;try Lreflexivity
      | |- _ >* _ Lreduce;try Lreflexivity
      | |- eval _ _ Lreduce;try Lreflexivity
      
      | |- _ == _ repeat Lsimpl';try reflexivity'
      end
    end
  end.

Ltac infer_instances :=
  repeat match goal with
         | [ |- context [ int_ext ?t ] ] first [change (int_ext t) with (ext t) | fail 3 "Could not fold int-instance for " t]
         end.

Ltac computable_prepare t :=
  let h := visibleHead t in
  tryif is_const h then unfold h else idtac.

Ltac computable_using_noProof Lter:=
  once lazymatch goal with
  | [ |- computable ?t ]
    eexists Lter;unfold Lter;try clear Lter;
    let t' := eval hnf in t in
        let h := visibleHead t' in
        try unfold h;computable_prepare t;infer_instances
  end.

Ltac extractAs s :=
  once lazymatch goal with
  | [ H : @extracted _ |- _ ] idtac "WARNING: extraction is buggy if used while a term of type 'extracted _' is in Context"
  | [ |- computable ?t ]
    (run_template_program (tmExtract None t)
                         ( e pose (s:= ( e : extracted t))))
  end.

Ltac extractThis t s :=
    (run_template_program (tmExtract None t)
                         ( e pose (s:= ( e : extracted t)))).

End Intern.

Import Intern.

Ltac register_inj :=
  abstract (intros x; induction x; let y := fresh "y" in destruct y;simpl; intros eq;
    try (injection eq || discriminate eq);intros;f_equal;auto;try apply inj_enc;try easy).

Ltac register_proc :=
  solve [
  let x := fresh "x" in
  (((intros x;induction x || intros *);
    cbn; fold_encs;Lproc
                        ))].

Ltac register encf := refine (@mk_encodable _ encf _);[
                          (((let x := fresh "x" in induction x || intros);(let f := Intern.visibleHead encf in unfold f;cbn [f]);
                            Lproc
                        ))].

Tactic Notation "computable" "using" open_constr(Lter) :=
  computable_using_noProof Lter;repeat cstep.

Tactic Notation "computable" "instead" open_constr(t) :=
  let s := fresh "s" in
  extractThis t s; computable using s.

Tactic Notation "computable" "infer" :=
  once lazymatch goal with
  | [ |- computable ?t ]
    let e := constr:(int_ext t) in let e' := eval unfold int_ext in e in computable using e'
  end.

Tactic Notation "extract" :=
  unshelve
    let term := fresh "used_term" in
    extractAs term;computable using term.

Tactic Notation "extract" "constructor":=
  let term := fresh "used_term" in
        once lazymatch goal with
        | [ |- computable ?t ]
          run_template_program (tmExtractConstr' None t)
                                 ( e pose (term:= ( e : extracted t)); computable using term)
   end.

Tactic Notation "extract" "match" := computable_match.

Lemma cast_computable X Y `{encodable Y} (cast : X Y) :
  let _ := registerAs cast in
  computable cast.
Proof.
  cbn.
  pose (t:=lam 0).
  computable using t.
Qed.


Ltac computable_casted_result :=
  match goal with
    |- @computable _ _ _
    simple notypeclasses refine (cast_registeredAs _ _);
    [ | | |
      cbn - [registerAs];reflexivity| ];
    cbn
  end.