summaryrefslogtreecommitdiff
path: root/plugins/ring/ring.ml
blob: ae73069d90b74adf9e3192bd7e1c8db2b43b2780 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* ML part of the Ring tactic *)

open Pp
open Util
open Flags
open Term
open Names
open Libnames
open Nameops
open Reductionops
open Tacticals
open Tacexpr
open Tacmach
open Printer
open Equality
open Vernacinterp
open Vernacexpr
open Libobject
open Closure
open Tacred
open Tactics
open Pattern
open Hiddentac
open Nametab
open Quote
open Mod_subst

let mt_evd = Evd.empty
let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c

let ring_dir = ["Coq";"ring"]
let setoids_dir = ["Coq";"Setoids"]

let ring_constant = Coqlib.gen_constant_in_modules "Ring"
  [ring_dir@["LegacyRing_theory"];
   ring_dir@["Setoid_ring_theory"];
   ring_dir@["Ring_normalize"];
   ring_dir@["Ring_abstract"];
   setoids_dir@["Setoid"];
   ring_dir@["Setoid_ring_normalize"]]

(* Ring theory *)
let coq_Ring_Theory = lazy (ring_constant "Ring_Theory")
let coq_Semi_Ring_Theory = lazy (ring_constant "Semi_Ring_Theory")

(* Setoid ring theory *)
let coq_Setoid_Ring_Theory = lazy (ring_constant "Setoid_Ring_Theory")
let coq_Semi_Setoid_Ring_Theory = lazy(ring_constant "Semi_Setoid_Ring_Theory")

(* Ring normalize *)
let coq_SPplus = lazy (ring_constant "SPplus")
let coq_SPmult = lazy (ring_constant "SPmult")
let coq_SPvar = lazy (ring_constant "SPvar")
let coq_SPconst = lazy (ring_constant "SPconst")
let coq_Pplus = lazy (ring_constant "Pplus")
let coq_Pmult = lazy (ring_constant "Pmult")
let coq_Pvar = lazy (ring_constant "Pvar")
let coq_Pconst = lazy (ring_constant "Pconst")
let coq_Popp = lazy (ring_constant "Popp")
let coq_interp_sp = lazy (ring_constant "interp_sp")
let coq_interp_p = lazy (ring_constant "interp_p")
let coq_interp_cs = lazy (ring_constant "interp_cs")
let coq_spolynomial_simplify = lazy (ring_constant "spolynomial_simplify")
let coq_polynomial_simplify = lazy (ring_constant "polynomial_simplify")
let coq_spolynomial_simplify_ok = lazy(ring_constant "spolynomial_simplify_ok")
let coq_polynomial_simplify_ok = lazy (ring_constant "polynomial_simplify_ok")

(* Setoid theory *)
let coq_Setoid_Theory = lazy(ring_constant "Setoid_Theory")

let coq_seq_refl = lazy(ring_constant "Seq_refl")
let coq_seq_sym = lazy(ring_constant "Seq_sym")
let coq_seq_trans = lazy(ring_constant "Seq_trans")

(* Setoid Ring normalize *)
let coq_SetSPplus = lazy (ring_constant "SetSPplus")
let coq_SetSPmult = lazy (ring_constant "SetSPmult")
let coq_SetSPvar = lazy (ring_constant "SetSPvar")
let coq_SetSPconst = lazy (ring_constant "SetSPconst")
let coq_SetPplus = lazy (ring_constant "SetPplus")
let coq_SetPmult = lazy (ring_constant "SetPmult")
let coq_SetPvar = lazy (ring_constant "SetPvar")
let coq_SetPconst = lazy (ring_constant "SetPconst")
let coq_SetPopp = lazy (ring_constant "SetPopp")
let coq_interp_setsp = lazy (ring_constant "interp_setsp")
let coq_interp_setp = lazy (ring_constant "interp_setp")
let coq_interp_setcs = lazy (ring_constant "interp_setcs")
let coq_setspolynomial_simplify =
  lazy (ring_constant "setspolynomial_simplify")
let coq_setpolynomial_simplify =
  lazy (ring_constant "setpolynomial_simplify")
let coq_setspolynomial_simplify_ok =
  lazy (ring_constant "setspolynomial_simplify_ok")
let coq_setpolynomial_simplify_ok =
  lazy (ring_constant "setpolynomial_simplify_ok")

(* Ring abstract *)
let coq_ASPplus = lazy (ring_constant "ASPplus")
let coq_ASPmult = lazy (ring_constant "ASPmult")
let coq_ASPvar = lazy (ring_constant "ASPvar")
let coq_ASP0 = lazy (ring_constant "ASP0")
let coq_ASP1 = lazy (ring_constant "ASP1")
let coq_APplus = lazy (ring_constant "APplus")
let coq_APmult = lazy (ring_constant "APmult")
let coq_APvar = lazy (ring_constant "APvar")
let coq_AP0 = lazy (ring_constant "AP0")
let coq_AP1 = lazy (ring_constant "AP1")
let coq_APopp = lazy (ring_constant "APopp")
let coq_interp_asp = lazy (ring_constant "interp_asp")
let coq_interp_ap = lazy (ring_constant "interp_ap")
let coq_interp_acs = lazy (ring_constant "interp_acs")
let coq_interp_sacs = lazy (ring_constant "interp_sacs")
let coq_aspolynomial_normalize = lazy (ring_constant "aspolynomial_normalize")
let coq_apolynomial_normalize = lazy (ring_constant "apolynomial_normalize")
let coq_aspolynomial_normalize_ok =
  lazy (ring_constant "aspolynomial_normalize_ok")
let coq_apolynomial_normalize_ok =
  lazy (ring_constant "apolynomial_normalize_ok")

(* Logic --> to be found in Coqlib *)
open Coqlib

let mkLApp(fc,v) = mkApp(Lazy.force fc, v)

(*********** Useful types and functions ************)

module OperSet =
  Set.Make (struct
	      type t = global_reference
	      let compare = (RefOrdered.compare : t->t->int)
	    end)

type morph =
    { plusm : constr;
      multm : constr;
      oppm : constr option;
    }

type theory =
    { th_ring : bool;                  (* false for a semi-ring *)
      th_abstract : bool;
      th_setoid : bool;                (* true for a setoid ring *)
      th_equiv : constr option;
      th_setoid_th : constr option;
      th_morph : morph option;
      th_a : constr;                   (* e.g. nat *)
      th_plus : constr;
      th_mult : constr;
      th_one : constr;
      th_zero : constr;
      th_opp : constr option;          (* None if semi-ring *)
      th_eq : constr;
      th_t : constr;                   (* e.g. NatTheory *)
      th_closed : ConstrSet.t;         (* e.g. [S; O] *)
                                       (* Must be empty for an abstract ring *)
    }

(* Theories are stored in a table which is synchronised with the Reset
   mechanism. *)

module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)

let theories_map = ref Cmap.empty

let theories_map_add (c,t) = theories_map := Cmap.add c t !theories_map
let theories_map_find c = Cmap.find c !theories_map
let theories_map_mem c = Cmap.mem c !theories_map

let _ =
  Summary.declare_summary "tactic-ring-table"
    { Summary.freeze_function = (fun () -> !theories_map);
      Summary.unfreeze_function = (fun t -> theories_map := t);
      Summary.init_function = (fun () -> theories_map := Cmap.empty) }

(* declare a new type of object in the environment, "tactic-ring-theory"
   The functions theory_to_obj and obj_to_theory do the conversions
   between theories and environement objects. *)


let subst_morph subst morph =
  let plusm' = subst_mps subst morph.plusm in
  let multm' = subst_mps subst morph.multm in
  let oppm' = Option.smartmap (subst_mps subst) morph.oppm in
    if plusm' == morph.plusm
      && multm' == morph.multm
      && oppm' == morph.oppm then
	morph
    else
      { plusm = plusm' ;
	multm = multm' ;
	oppm = oppm' ;
      }

let subst_set subst cset =
  let same = ref true in
  let copy_subst c newset =
    let c' = subst_mps subst c in
      if not (c' == c) then same := false;
      ConstrSet.add c' newset
  in
  let cset' = ConstrSet.fold copy_subst cset ConstrSet.empty in
    if !same then cset else cset'

let subst_theory subst th =
  let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in
  let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in
  let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in
  let th_a' = subst_mps subst th.th_a in
  let th_plus' = subst_mps subst th.th_plus in
  let th_mult' = subst_mps subst th.th_mult in
  let th_one' = subst_mps subst th.th_one in
  let th_zero' = subst_mps subst th.th_zero in
  let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in
  let th_eq' = subst_mps subst th.th_eq in
  let th_t' = subst_mps subst th.th_t in
  let th_closed' = subst_set subst th.th_closed in
    if th_equiv' == th.th_equiv
      && th_setoid_th' == th.th_setoid_th
      && th_morph' == th.th_morph
      && th_a' == th.th_a
      && th_plus' == th.th_plus
      && th_mult' == th.th_mult
      && th_one' == th.th_one
      && th_zero' == th.th_zero
      && th_opp' == th.th_opp
      && th_eq' == th.th_eq
      && th_t' == th.th_t
      && th_closed' == th.th_closed
    then
      th
    else
    { th_ring = th.th_ring ;
      th_abstract = th.th_abstract ;
      th_setoid = th.th_setoid ;
      th_equiv = th_equiv' ;
      th_setoid_th = th_setoid_th' ;
      th_morph = th_morph' ;
      th_a = th_a' ;
      th_plus = th_plus' ;
      th_mult = th_mult' ;
      th_one = th_one' ;
      th_zero = th_zero' ;
      th_opp = th_opp' ;
      th_eq = th_eq' ;
      th_t = th_t' ;
      th_closed = th_closed' ;
    }


let subst_th (subst,(c,th as obj)) =
  let c' = subst_mps subst c in
  let th' = subst_theory subst th in
    if c' == c && th' == th then obj else
      (c',th')


let theory_to_obj : constr * theory -> obj =
  let cache_th (_,(c, th)) = theories_map_add (c,th) in
  declare_object {(default_object "tactic-ring-theory") with
		    open_function = (fun i o -> if i=1 then cache_th o);
                    cache_function = cache_th;
		    subst_function = subst_th;
		    classify_function = (fun x -> Substitute x) }

(* from the set A, guess the associated theory *)
(* With this simple solution, the theory to use is automatically guessed *)
(* But only one theory can be declared for a given Set *)

let guess_theory a =
  try
    theories_map_find a
  with Not_found ->
    errorlabstrm "Ring"
      (str "No Declared Ring Theory for " ++
	 pr_lconstr a ++ fnl () ++
	 str "Use Add [Semi] Ring to declare it")

(* Looks up an option *)

let unbox = function
  | Some w -> w
  | None -> anomaly "Ring : Not in case of a setoid ring."

(* Protects the convertibility test against undue exceptions when using it
   with untyped terms *)

let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false


(* Add a Ring or a Semi-Ring to the database after a type verification *)

let implement_theory env t th args =
  is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args))

(* (\* The following test checks whether the provided morphism is the default *)
(*    one for the given operation. In principle the test is too strict, since *)
(*    it should possible to provide another proof for the same fact (proof *)
(*    irrelevance). In particular, the error message is be not very explicative. *\) *)
let states_compatibility_for env plus mult opp morphs =
 let check op compat = true in
(*   is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem *)
(*    compat in *)
 check plus morphs.plusm &&
 check mult morphs.multm &&
 (match (opp,morphs.oppm) with
     None, None -> true
   | Some opp, Some compat -> check opp compat
   | _,_ -> assert false)

let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset =
  if theories_map_mem a then errorlabstrm "Add Semi Ring"
    (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++
       pr_lconstr a);
  let env = Global.env () in
    if (want_ring & want_setoid & (
	not (implement_theory env t coq_Setoid_Ring_Theory
	  [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])
        ||
	not (implement_theory env (unbox asetth) coq_Setoid_Theory
	  [| a; (unbox aequiv) |]) ||
        not (states_compatibility_for env aplus amult aopp (unbox amorph))
        )) then
      errorlabstrm "addring" (str "Not a valid Setoid-Ring theory");
    if (not want_ring & want_setoid & (
        not (implement_theory env t coq_Semi_Setoid_Ring_Theory
	  [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) ||
	not (implement_theory env (unbox asetth) coq_Setoid_Theory
	  [| a; (unbox aequiv) |]) ||
        not (states_compatibility_for env aplus amult aopp (unbox amorph))))
    then
      errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory");
    if (want_ring & not want_setoid &
	not (implement_theory env t coq_Ring_Theory
	  [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])) then
      errorlabstrm "addring" (str "Not a valid Ring theory");
    if (not want_ring & not want_setoid &
	not (implement_theory env t coq_Semi_Ring_Theory
	  [| a; aplus; amult; aone; azero; aeq |])) then
      errorlabstrm "addring" (str "Not a valid Semi-Ring theory");
    Lib.add_anonymous_leaf
      (theory_to_obj
	 (a, { th_ring = want_ring;
	       th_abstract = want_abstract;
	       th_setoid = want_setoid;
	       th_equiv = aequiv;
	       th_setoid_th = asetth;
	       th_morph = amorph;
	       th_a = a;
	       th_plus = aplus;
	       th_mult = amult;
	       th_one = aone;
	       th_zero = azero;
	       th_opp = aopp;
	       th_eq = aeq;
	       th_t = t;
	       th_closed = cset }))

(******** The tactic itself *********)

(*
   gl : goal sigma
   th : semi-ring theory (concrete)
   cl : constr list [c1; c2; ...]

Builds
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

module Constrhash = Hashtbl.Make
  (struct type t = constr
	  let equal = eq_constr
	  let hash = hash_constr
   end)

let build_spolynom gl th lc =
  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  (* aux creates the spolynom p by a recursive destructuration of c
     and builds the varmap with side-effects *)
  let rec aux c =
    match (kind_of_term (strip_outer_cast c)) with
      | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_SPplus, [|th.th_a; aux c1; aux c2 |])
      | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_SPmult, [|th.th_a; aux c1; aux c2 |])
      | _ when closed_under th.th_closed c ->
	  mkLApp(coq_SPconst, [|th.th_a; c |])
      | _ ->
	  try Constrhash.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in
	    begin
	      incr counter;
	      varlist := c :: !varlist;
	      Constrhash.add varhash c newvar;
	      newvar
	    end
  in
  let lp = List.map aux lc in
  let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
  List.map
    (fun p ->
       (mkLApp (coq_interp_sp,
               [|th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]),
	mkLApp (coq_interp_cs,
               [|th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp (coq_spolynomial_simplify,
			    [| th.th_a; th.th_plus; th.th_mult;
			       th.th_one; th.th_zero;
			       th.th_eq; p|])) |]),
	mkLApp (coq_spolynomial_simplify_ok,
	        [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
		  th.th_eq; v; th.th_t; p |])))
    lp

(*
   gl : goal sigma
   th : ring theory (concrete)
   cl : constr list [c1; c2; ...]

Builds
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_polynom gl th lc =
  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  let rec aux c =
    match (kind_of_term (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_Pplus, [|th.th_a; aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_Pmult, [|th.th_a; aux c1; aux c2 |])
      (* The special case of Z.sub *)
      | App (binop, [|c1; c2|])
	  when safe_pf_conv_x gl c
            (mkApp (th.th_plus, [|c1; mkApp(unbox th.th_opp, [|c2|])|])) ->
	    mkLApp(coq_Pplus,
                  [|th.th_a; aux c1;
	            mkLApp(coq_Popp, [|th.th_a; aux c2|]) |])
      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
	  mkLApp(coq_Popp, [|th.th_a; aux c1|])
      | _ when closed_under th.th_closed c ->
	  mkLApp(coq_Pconst, [|th.th_a; c |])
      | _ ->
	  try Constrhash.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in
	    begin
	      incr counter;
	      varlist := c :: !varlist;
	      Constrhash.add varhash c newvar;
	      newvar
	    end
  in
  let lp = List.map aux lc in
  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
  List.map
    (fun p ->
       (mkLApp(coq_interp_p,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero;
                 (unbox th.th_opp); v; p |])),
	mkLApp(coq_interp_cs,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_polynomial_simplify,
			    [| th.th_a; th.th_plus; th.th_mult;
			       th.th_one; th.th_zero;
			       (unbox th.th_opp); th.th_eq; p |])) |]),
	mkLApp(coq_polynomial_simplify_ok,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |]))
    lp

(*
   gl : goal sigma
   th : semi-ring theory (abstract)
   cl : constr list [c1; c2; ...]

Builds
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_aspolynom gl th lc =
  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  (* aux creates the aspolynom p by a recursive destructuration of c
     and builds the varmap with side-effects *)
  let rec aux c =
    match (kind_of_term (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_ASPplus, [| aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_ASPmult, [| aux c1; aux c2 |])
      | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0
      | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1
      | _ ->
	  try Constrhash.find varhash c
	  with Not_found ->
	    let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in
	    begin
	      incr counter;
	      varlist := c :: !varlist;
	      Constrhash.add varhash c newvar;
	      newvar
	    end
  in
  let lp = List.map aux lc in
  let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
  List.map
    (fun p ->
       (mkLApp(coq_interp_asp,
               [| th.th_a; th.th_plus; th.th_mult;
		  th.th_one; th.th_zero; v; p |]),
	mkLApp(coq_interp_acs,
               [| th.th_a; th.th_plus; th.th_mult;
		  th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_aspolynomial_normalize,[|p|])) |]),
	mkLApp(coq_spolynomial_simplify_ok,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
		  th.th_eq; v; th.th_t; p |])))
    lp

(*
   gl : goal sigma
   th : ring theory (abstract)
   cl : constr list [c1; c2; ...]

Builds
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_apolynom gl th lc =
  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  let rec aux c =
    match (kind_of_term (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_APplus, [| aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_APmult, [| aux c1; aux c2 |])
      (* The special case of Z.sub *)
      | App (binop, [|c1; c2|])
	  when safe_pf_conv_x gl c
            (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|]) |])) ->
	    mkLApp(coq_APplus,
                   [|aux c1; mkLApp(coq_APopp,[|aux c2|]) |])
      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
	  mkLApp(coq_APopp, [| aux c1 |])
      | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
      | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
      | _ ->
	  try Constrhash.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(coq_APvar, [| path_of_int !counter |]) in
	    begin
	      incr counter;
	      varlist := c :: !varlist;
	      Constrhash.add varhash c newvar;
	      newvar
	    end
  in
  let lp = List.map aux lc in
  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
  List.map
    (fun p ->
       (mkLApp(coq_interp_ap,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one;
		  th.th_zero; (unbox th.th_opp); v; p |]),
	mkLApp(coq_interp_sacs,
	       [| th.th_a; th.th_plus; th.th_mult;
		  th.th_one; th.th_zero; (unbox th.th_opp); v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_apolynomial_normalize, [|p|])) |]),
	mkLApp(coq_apolynomial_normalize_ok,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |])))
    lp

(*
   gl : goal sigma
   th : setoid ring theory (concrete)
   cl : constr list [c1; c2; ...]

Builds
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_setpolynom gl th lc =
  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  let rec aux c =
    match (kind_of_term (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_SetPplus, [|th.th_a; aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_SetPmult, [|th.th_a; aux c1; aux c2 |])
      (* The special case of Z.sub *)
      | App (binop, [|c1; c2|])
	  when safe_pf_conv_x gl c
	    (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|])|])) ->
	      mkLApp(coq_SetPplus,
                     [| th.th_a; aux c1;
			mkLApp(coq_SetPopp, [|th.th_a; aux c2|]) |])
      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
	  mkLApp(coq_SetPopp, [| th.th_a; aux c1 |])
      | _ when closed_under th.th_closed c ->
	  mkLApp(coq_SetPconst, [| th.th_a; c |])
      | _ ->
	  try Constrhash.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in
	    begin
	      incr counter;
	      varlist := c :: !varlist;
	      Constrhash.add varhash c newvar;
	      newvar
	    end
  in
  let lp = List.map aux lc in
  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
  List.map
    (fun p ->
       (mkLApp(coq_interp_setp,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero;
                  (unbox th.th_opp); v; p |]),
	mkLApp(coq_interp_setcs,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_setpolynomial_simplify,
			    [| th.th_a; th.th_plus; th.th_mult;
			       th.th_one; th.th_zero;
			       (unbox th.th_opp); th.th_eq; p |])) |]),
	mkLApp(coq_setpolynomial_simplify_ok,
	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
                  th.th_mult; th.th_one; th.th_zero;(unbox th.th_opp);
                  th.th_eq; (unbox th.th_setoid_th);
		  (unbox th.th_morph).plusm; (unbox th.th_morph).multm;
		  (unbox (unbox th.th_morph).oppm); v; th.th_t; p |])))
    lp

(*
   gl : goal sigma
   th : semi setoid ring theory (concrete)
   cl : constr list [c1; c2; ...]

Builds
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_setspolynom gl th lc =
  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  let rec aux c =
    match (kind_of_term (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_SetSPplus, [|th.th_a; aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_SetSPmult, [| th.th_a; aux c1; aux c2 |])
      | _ when closed_under th.th_closed c ->
	  mkLApp(coq_SetSPconst, [| th.th_a; c |])
      | _ ->
	  try Constrhash.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in
	    begin
	      incr counter;
	      varlist := c :: !varlist;
	      Constrhash.add varhash c newvar;
	      newvar
	    end
  in
  let lp = List.map aux lc in
  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
  List.map
    (fun p ->
       (mkLApp(coq_interp_setsp,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]),
	mkLApp(coq_interp_setcs,
               [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_setspolynomial_simplify,
			    [| th.th_a; th.th_plus; th.th_mult;
			       th.th_one; th.th_zero;
			       th.th_eq; p |])) |]),
	mkLApp(coq_setspolynomial_simplify_ok,
	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
                  th.th_mult; th.th_one; th.th_zero; th.th_eq;
                  (unbox th.th_setoid_th);
		  (unbox th.th_morph).plusm;
                  (unbox th.th_morph).multm; v; th.th_t; p |])))
    lp

module SectionPathSet =
  Set.Make(struct
	     type t = full_path
	     let compare = Pervasives.compare
	   end)

(* Avec l'uniformisation des red_kind, on perd ici sur la structure
   SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *)
let constants_to_unfold =
(*  List.fold_right SectionPathSet.add *)
  let transform s =
    let sp = path_of_string s in
    let dir, id = repr_path sp in
      Libnames.encode_con dir id
  in
  List.map transform
    [ "Coq.ring.Ring_normalize.interp_cs";
      "Coq.ring.Ring_normalize.interp_var";
      "Coq.ring.Ring_normalize.interp_vl";
      "Coq.ring.Ring_abstract.interp_acs";
      "Coq.ring.Ring_abstract.interp_sacs";
      "Coq.quote.Quote.varmap_find";
      (* anciennement des Local devenus Definition *)
      "Coq.ring.Ring_normalize.ics_aux";
      "Coq.ring.Ring_normalize.ivl_aux";
      "Coq.ring.Ring_normalize.interp_m";
      "Coq.ring.Ring_abstract.iacs_aux";
      "Coq.ring.Ring_abstract.isacs_aux";
      "Coq.ring.Setoid_ring_normalize.interp_cs";
      "Coq.ring.Setoid_ring_normalize.interp_var";
      "Coq.ring.Setoid_ring_normalize.interp_vl";
      "Coq.ring.Setoid_ring_normalize.ics_aux";
      "Coq.ring.Setoid_ring_normalize.ivl_aux";
      "Coq.ring.Setoid_ring_normalize.interp_m";
    ]
(*    SectionPathSet.empty *)

(* Unfolds the functions interp and find_btree in the term c of goal gl *)
open RedFlags
let polynom_unfold_tac =
  let flags =
    (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
  reduct_in_concl (cbv_norm_flags flags,DEFAULTcast)

let polynom_unfold_tac_in_term gl =
  let flags =
    (mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold)))
  in
  cbv_norm_flags flags (pf_env gl) (project gl)

(* lc : constr list *)
(* th : theory associated to t *)
(* op : clause (None for conclusion or Some id for hypothesis id) *)
(* gl : goal  *)
(* Does the rewriting c_i -> (interp R RC v (polynomial_simplify p_i))
   where the ring R, the Ring theory RC, the varmap v and the polynomials p_i
   are guessed and such that c_i = (interp R RC v p_i) *)
let raw_polynom th op lc gl =
  (* first we sort the terms : if t' is a subterm of t it must appear
     after t in the list. This is to avoid that the normalization of t'
     modifies t in a non-desired way *)
  let lc = sort_subterm gl lc in
  let ltriplets =
    if th.th_setoid then
      if th.th_ring
      then build_setpolynom gl th lc
      else build_setspolynom gl th lc
    else
      if th.th_ring then
	if th.th_abstract
	then build_apolynom gl th lc
	else build_polynom gl th lc
      else
	if th.th_abstract
	then build_aspolynom gl th lc
	else build_spolynom gl th lc in
  let polynom_tac =
    List.fold_right2
      (fun ci (c'i, c''i, c'i_eq_c''i) tac ->
         let c'''i =
	   if !term_quality then polynom_unfold_tac_in_term gl c''i else c''i
	 in
         if !term_quality && safe_pf_conv_x gl c'''i ci then
	   tac (* convertible terms *)
         else if th.th_setoid
	 then
           (tclORELSE
              (tclORELSE
		 (h_exact c'i_eq_c''i)
		 (h_exact (mkLApp(coq_seq_sym,
				  [| th.th_a; (unbox th.th_equiv);
                                     (unbox th.th_setoid_th);
				     c'''i; ci; c'i_eq_c''i |]))))
	      (tclTHENS
		 (tclORELSE
                   (Equality.general_rewrite true
		     Termops.all_occurrences true false c'i_eq_c''i)
                   (Equality.general_rewrite false
		     Termops.all_occurrences true false c'i_eq_c''i))
                 [tac]))
	 else
           (tclORELSE
              (tclORELSE
		 (h_exact c'i_eq_c''i)
		 (h_exact (mkApp(build_coq_eq_sym (),
				 [|th.th_a; c'''i; ci; c'i_eq_c''i |]))))
	      (tclTHENS
		 (elim_type
		    (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |])))
		 [ tac;
                   h_exact c'i_eq_c''i ]))
)
      lc ltriplets polynom_unfold_tac
  in
  polynom_tac gl

let guess_eq_tac th =
  (tclORELSE reflexivity
     (tclTHEN
	polynom_unfold_tac
        (tclTHEN
	   (* Normalized sums associate on the right *)
	   (tclREPEAT
	      (tclTHENFIRST
		 (apply (mkApp(build_coq_f_equal2 (),
		               [| th.th_a; th.th_a; th.th_a;
				  th.th_plus |])))
		 reflexivity))
	   (tclTRY
	      (tclTHENLAST
		 (apply (mkApp(build_coq_f_equal2 (),
			       [| th.th_a; th.th_a; th.th_a;
				  th.th_plus |])))
		 reflexivity)))))

let guess_equiv_tac th =
  (tclORELSE (apply (mkLApp(coq_seq_refl,
			    [| th.th_a; (unbox th.th_equiv);
			       (unbox th.th_setoid_th)|])))
     (tclTHEN
	polynom_unfold_tac
	(tclREPEAT
	   (tclORELSE
	      (apply (unbox th.th_morph).plusm)
	      (apply (unbox th.th_morph).multm)))))

let match_with_equiv c = match (kind_of_term c) with
  | App (e,a) ->
      if (List.mem e []) (*  (Setoid_replace.equiv_list ())) *)
      then Some (decompose_app c)
      else None
  | _ -> None

let polynom lc gl =
  Coqlib.check_required_library ["Coq";"ring";"LegacyRing"];
  match lc with
   (* If no argument is given, try to recognize either an equality or
      a declared relation with arguments c1 ... cn,
      do "Ring c1 c2 ... cn" and then try to apply the simplification
      theorems declared for the relation *)
    | [] ->
	(try
	  match Hipattern.match_with_equation (pf_concl gl) with
	   | _,_,Hipattern.PolymorphicLeibnizEq (t,c1,c2) ->
	       let th = guess_theory t in
	       (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
	   | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2)
	       when safe_pf_conv_x gl t1 t2 ->
	       let th = guess_theory t1 in
	       (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
	   | _ -> raise Exit
	  with Hipattern.NoEquationFound | Exit ->
	          (match match_with_equiv (pf_concl gl) with
		     | Some (equiv, c1::args) ->
			 let t = (pf_type_of gl c1) in
			 let th = (guess_theory t) in
			   if List.exists
			     (fun c2 -> not (safe_pf_conv_x gl t (pf_type_of gl c2))) args
			   then
			     errorlabstrm "Ring :"
			       (str" All terms must have the same type");
			   (tclTHEN (raw_polynom th None (c1::args)) (guess_equiv_tac th)) gl
		     | _ -> errorlabstrm "polynom :"
			 (str" This goal is not an equality nor a setoid equivalence")))
    (* Elsewhere, guess the theory, check that all terms have the same type
       and apply raw_polynom *)
    | c :: lc' ->
	let t = pf_type_of gl c in
	let th = guess_theory t in
	  if List.exists
	    (fun c1 -> not (safe_pf_conv_x gl t (pf_type_of gl c1))) lc'
	  then
	    errorlabstrm "Ring :"
	      (str" All terms must have the same type");
	  (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl