(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

Require Import List.
Require Import LegacyRing.
Require Export LegacyField_Compl.
Require Export LegacyField_Theory.

(**** Interpretation A --> ExprA ****)

Ltac get_component a s := eval cbv beta iota delta [a] in (a s).

Ltac body_of s := eval cbv beta iota delta [s] in s.

Ltac mem_assoc var lvar :=
  match constr:lvar with
  | nil => constr:false
  | ?X1 :: ?X2 =>
      match constr:(X1 = var) with
      | (?X1 = ?X1) => constr:true
      | _ => mem_assoc var X2
      end
  end.

Ltac number lvar :=
  let rec number_aux lvar cpt :=
    match constr:lvar with
    | (@nil ?X1) => constr:(@nil (prod X1 nat))
    | ?X2 :: ?X3 =>
        let l2 := number_aux X3 (S cpt) in
        constr:((X2,cpt) :: l2)
    end
  in number_aux lvar 0.

Ltac build_varlist FT trm :=
  let rec seek_var lvar trm :=
    let AT := get_component A FT
    with AzeroT := get_component Azero FT
    with AoneT := get_component Aone FT
    with AplusT := get_component Aplus FT
    with AmultT := get_component Amult FT
    with AoppT := get_component Aopp FT
    with AinvT := get_component Ainv FT in
    match constr:trm with
    | AzeroT => lvar
    | AoneT => lvar
    | (AplusT ?X1 ?X2) =>
        let l1 := seek_var lvar X1 in
        seek_var l1 X2
    | (AmultT ?X1 ?X2) =>
        let l1 := seek_var lvar X1 in
        seek_var l1 X2
    | (AoppT ?X1) => seek_var lvar X1
    | (AinvT ?X1) => seek_var lvar X1
    | ?X1 =>
        let res := mem_assoc X1 lvar in
        match constr:res with
        | true => lvar
        | false => constr:(X1 :: lvar)
        end
    end in
  let AT := get_component A FT in
  let lvar := seek_var (@nil AT) trm in
  number lvar.

Ltac assoc elt lst :=
  match constr:lst with
  | nil => fail
  | (?X1,?X2) :: ?X3 =>
      match constr:(elt = X1) with
      | (?X1 = ?X1) => constr:X2
      | _ => assoc elt X3
      end
  end.

Ltac interp_A FT lvar trm :=
  let AT := get_component A FT
  with AzeroT := get_component Azero FT
  with AoneT := get_component Aone FT
  with AplusT := get_component Aplus FT
  with AmultT := get_component Amult FT
  with AoppT := get_component Aopp FT
  with AinvT := get_component Ainv FT in
  match constr:trm with
  | AzeroT => constr:EAzero
  | AoneT => constr:EAone
  | (AplusT ?X1 ?X2) =>
      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
      constr:(EAplus e1 e2)
  | (AmultT ?X1 ?X2) =>
      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
      constr:(EAmult e1 e2)
  | (AoppT ?X1) =>
      let e := interp_A FT lvar X1 in
      constr:(EAopp e)
  | (AinvT ?X1) => let e := interp_A FT lvar X1 in
                   constr:(EAinv e)
  | ?X1 => let idx := assoc X1 lvar in
           constr:(EAvar idx)
  end.

(************************)
(*    Simplification    *)
(************************)

(**** Generation of the multiplier ****)

Ltac remove e l :=
  match constr:l with
  | nil => l
  | e :: ?X2 => constr:X2
  | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl)
  end.

Ltac union l1 l2 :=
  match constr:l1 with
  | nil => l2
  | ?X2 :: ?X3 =>
      let nl2 := remove X2 l2 in
      let nl := union X3 nl2 in
      constr:(X2 :: nl)
  end.

Ltac raw_give_mult trm :=
  match constr:trm with
  | (EAinv ?X1) => constr:(X1 :: nil)
  | (EAopp ?X1) => raw_give_mult X1
  | (EAplus ?X1 ?X2) =>
      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
      union l1 l2
  | (EAmult ?X1 ?X2) =>
      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
      eval compute in (app l1 l2)
  | _ => constr:(@nil ExprA)
  end.

Ltac give_mult trm :=
  let ltrm := raw_give_mult trm in
  constr:(mult_of_list ltrm).

(**** Associativity ****)

Ltac apply_assoc FT lvar trm :=
  let t := eval compute in (assoc trm) in
  match constr:(t = trm) with
  | (?X1 = ?X1) => idtac
  | _ =>
      rewrite <- (assoc_correct FT trm); change (assoc trm) with t
  end.

(**** Distribution *****)

Ltac apply_distrib FT lvar trm :=
  let t := eval compute in (distrib trm) in
  match constr:(t = trm) with
  | (?X1 = ?X1) => idtac
  | _ =>
      rewrite <- (distrib_correct FT trm);
       change (distrib trm) with t
  end.

(**** Multiplication by the inverse product ****)

Ltac grep_mult := match goal with
                  | id:(interp_ExprA _ _ _ <> _) |- _ => id
                  end.

Ltac weak_reduce :=
  match goal with
  |  |- context [(interp_ExprA ?X1 ?X2 _)] =>
      cbv beta iota zeta
       delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero
             Aone Aplus Amult Aopp Ainv]
  end.

Ltac multiply mul :=
  match goal with
  |  |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) =>
      let AzeroT := get_component Azero FT in
      cut (interp_ExprA FT X2 mul <> AzeroT);
       [ intro; (let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id))
       | weak_reduce;
          (let AoneT := get_component Aone ltac:(body_of FT)
           with AmultT := get_component Amult ltac:(body_of FT) in
           try
             match goal with
             |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
             end; clear FT X2) ]
  end.

Ltac apply_multiply FT lvar trm :=
  let t := eval compute in (multiply trm) in
  match constr:(t = trm) with
  | (?X1 = ?X1) => idtac
  | _ =>
      rewrite <- (multiply_correct FT trm);
       change (multiply trm) with t
  end.

(**** Permutations and simplification ****)

Ltac apply_inverse mul FT lvar trm :=
  let t := eval compute in (inverse_simplif mul trm) in
  match constr:(t = trm) with
  | (?X1 = ?X1) => idtac
  | _ =>
      rewrite <- (inverse_correct FT trm mul);
       [ change (inverse_simplif mul trm) with t | assumption ]
  end.
(**** Inverse test ****)

Ltac strong_fail tac := first [ tac | fail 2 ].

Ltac inverse_test_aux FT trm :=
  let AplusT := get_component Aplus FT
  with AmultT := get_component Amult FT
  with AoppT := get_component Aopp FT
  with AinvT := get_component Ainv FT in
  match constr:trm with
  | (AinvT _) => fail 1
  | (AoppT ?X1) =>
      strong_fail ltac:(inverse_test_aux FT X1; idtac)
  | (AplusT ?X1 ?X2) =>
      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
  | (AmultT ?X1 ?X2) =>
      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
  | _ => idtac
  end.

Ltac inverse_test FT :=
  let AplusT := get_component Aplus FT in
  match goal with
  |  |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
  end.

(**** Field itself ****)

Ltac apply_simplif sfun :=
  match goal with
  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) =>
  sfun X1 X2 X3
  end;
   match goal with
   |  |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) =>
   sfun X1 X2 X3
   end.

Ltac unfolds FT :=
  match get_component Aminus FT with
  | Some ?X1 => unfold X1
  | _ => idtac
  end;
  match get_component Adiv FT with
  | Some ?X1 => unfold X1
  | _ => idtac
  end.

Ltac reduce FT :=
  let AzeroT := get_component Azero FT
  with AoneT := get_component Aone FT
  with AplusT := get_component Aplus FT
  with AmultT := get_component Amult FT
  with AoppT := get_component Aopp FT
  with AinvT := get_component Ainv FT in
  (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] ||
     compute).

Ltac field_gen_aux FT :=
  let AplusT := get_component Aplus FT in
  match goal with
  |  |- (?X1 = ?X2) =>
      let lvar := build_varlist FT (AplusT X1 X2) in
      let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in
      let mul := give_mult (EAplus trm1 trm2) in
      cut
        (let ft := FT in
         let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
        [ compute; auto
        | intros ft vm; apply_simplif apply_distrib;
           apply_simplif apply_assoc; multiply mul;
           [ apply_simplif apply_multiply;
              apply_simplif ltac:(apply_inverse mul);
              (let id := grep_mult in
               clear id; weak_reduce; clear ft vm; first
              [ inverse_test FT; legacy ring | field_gen_aux FT ])
           | idtac ] ]
  end.

Ltac field_gen FT :=
  unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT.

(*****************************)
(*    Term Simplification    *)
(*****************************)

(**** Minus and division expansions ****)

Ltac init_exp FT trm :=
  let e :=
   (match get_component Aminus FT with
    | Some ?X1 => eval cbv beta delta [X1] in trm
    | _ => trm
    end) in
  match get_component Adiv FT with
  | Some ?X1 => eval cbv beta delta [X1] in e
  | _ => e
  end.

(**** Inverses simplification ****)

Ltac simpl_inv trm :=
  match constr:trm with
  | (EAplus ?X1 ?X2) =>
      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
      constr:(EAplus e1 e2)
  | (EAmult ?X1 ?X2) =>
      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
      constr:(EAmult e1 e2)
  | (EAopp ?X1) => let e := simpl_inv X1 in
                   constr:(EAopp e)
  | (EAinv ?X1) => SimplInvAux X1
  | ?X1 => constr:X1
  end
 with SimplInvAux trm :=
  match constr:trm with
  | (EAinv ?X1) => simpl_inv X1
  | (EAmult ?X1 ?X2) =>
      let e1 := simpl_inv (EAinv X1) with e2 := simpl_inv (EAinv X2) in
      constr:(EAmult e1 e2)
  | ?X1 => let e := simpl_inv X1 in
           constr:(EAinv e)
  end.

(**** Monom simplification ****)

Ltac map_tactic fcn lst :=
  match constr:lst with
  | nil => lst
  | ?X2 :: ?X3 =>
      let r := fcn X2 with t := map_tactic fcn X3 in
      constr:(r :: t)
  end.

Ltac build_monom_aux lst trm :=
  match constr:lst with
  | nil => eval compute in (assoc trm)
  | ?X1 :: ?X2 => build_monom_aux X2 (EAmult trm X1)
  end.

Ltac build_monom lnum lden :=
  let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in
  let ltot := eval compute in (app lnum ildn) in
  let trm := build_monom_aux ltot EAone in
  match constr:trm with
  | (EAmult _ ?X1) => constr:X1
  | ?X1 => constr:X1
  end.

Ltac simpl_monom_aux lnum lden trm :=
  match constr:trm with
  | (EAmult (EAinv ?X1) ?X2) =>
      let mma := mem_assoc X1 lnum in
      match constr:mma with
      | true =>
          let newlnum := remove X1 lnum in
          simpl_monom_aux newlnum lden X2
      | false => simpl_monom_aux lnum (X1 :: lden) X2
      end
  | (EAmult ?X1 ?X2) =>
      let mma := mem_assoc X1 lden in
      match constr:mma with
      | true =>
          let newlden := remove X1 lden in
          simpl_monom_aux lnum newlden X2
      | false => simpl_monom_aux (X1 :: lnum) lden X2
      end
  | (EAinv ?X1) =>
      let mma := mem_assoc X1 lnum in
      match constr:mma with
      | true =>
          let newlnum := remove X1 lnum in
          build_monom newlnum lden
      | false => build_monom lnum (X1 :: lden)
      end
  | ?X1 =>
      let mma := mem_assoc X1 lden in
      match constr:mma with
      | true =>
          let newlden := remove X1 lden in
          build_monom lnum newlden
      | false => build_monom (X1 :: lnum) lden
      end
  end.

Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm.

Ltac simpl_all_monomials trm :=
  match constr:trm with
  | (EAplus ?X1 ?X2) =>
      let e1 := simpl_monom X1 with e2 := simpl_all_monomials X2 in
      constr:(EAplus e1 e2)
  | ?X1 => simpl_monom X1
  end.

(**** Associativity and distribution ****)

Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)).

(**** The tactic Field_Term ****)

Ltac eval_weak_reduce trm :=
  eval
   cbv beta iota zeta
    delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus
          Amult Aopp Ainv] in trm.

Ltac field_term FT exp :=
  let newexp := init_exp FT exp in
  let lvar := build_varlist FT newexp in
  let trm := interp_A FT lvar newexp in
  let tma := eval compute in (assoc trm) in
  let tsmp :=
   simpl_all_monomials
    ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
  let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
  (replace exp with trep; [ legacy ring trep | field_gen FT ]).