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

(* $Id$ *)

Require Export Bool.
Require Export Ring_theory.
Require Export Quote.
Require Export Ring_normalize.
Require Export Ring_abstract.

Declare ML Module "ring".

Grammar tactic simple_tactic : ast :=
  ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))].

Syntax tactic level 0:
  ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] 
| ring_e [ << (Ring) >> ] -> ["Ring"].
 
Grammar vernac vernac : ast := 
  addring [ "Add" "Ring" 
     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
     constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t)
     "[" ne_constrarg_list($l) "]" "." ] 
  -> [(AddRing $a $aplus $amult $aone $azero $aopp $aeq $t
     ($LIST $l))]

| addsemiring [ "Add" "Semi" "Ring" 
      	       	 constrarg($a) constrarg($aplus) constrarg($amult) 
                 constrarg($aone) constrarg($azero) constrarg($aeq) 
                 constrarg($t) 
      	       	 "[" ne_constrarg_list($l) "]" "." ] 
  -> [(AddSemiRing $a $aplus $amult $aone $azero $aeq $t
      	   ($LIST $l))]
| addabstractring [ "Add" "Abstract" "Ring" 
      	     constrarg($a) constrarg($aplus) constrarg($amult)
             constrarg($aone) constrarg($azero) constrarg($aopp)
             constrarg($aeq) constrarg($t) "." ] 
  -> [(AddAbstractRing $a $aplus $amult $aone $azero $aopp $aeq $t)]

| addabstractsemiring [ "Add" "Abstract" "Semi" "Ring" 
      	       	 constrarg($a) constrarg($aplus) constrarg($amult) 
                 constrarg($aone) constrarg($azero) constrarg($aeq) 
                 constrarg($t) "." ] 
  -> [(AddAbstractSemiRing $a $aplus $amult $aone $azero $aeq $t )]
| addsetoidring [ "Add" "Setoid" "Ring"
      	    constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus) constrarg($amult) 
	    constrarg($aone) constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($pm)
	    constrarg($mm) constrarg($om) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
  -> [(AddSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aopp $aeq $pm $mm $om $t
      	 ($LIST $l))]
| addsetoidsemiring [ "Add" "Semi" "Setoid" "Ring" 
      	  constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus)
	  constrarg($amult) constrarg($aone) constrarg($azero) constrarg($aeq) 
          constrarg($pm) constrarg($mm) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
  -> [(AddSemiRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
      	   ($LIST $l))]
.

(* As an example, we provide an instantation for bool. *)
(* Other instatiations are given in ArithRing and ZArithRing in the
   same directory *)

Definition BoolTheory : (Ring_Theory xorb andb true false [b:bool]b eqb).
Split; Simpl.
NewDestruct n; NewDestruct m; Reflexivity.
NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
NewDestruct n; NewDestruct m; Reflexivity.
NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
NewDestruct n; Reflexivity.
NewDestruct n; Reflexivity.
NewDestruct n; Reflexivity.
NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
NewDestruct x; NewDestruct y; Reflexivity Orelse Simpl; Tauto.
Defined.

Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ].