summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-09-20 09:41:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-09-20 09:41:14 +0200
commit8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e (patch)
treeddabcfad1c52bf730690b1be7c900f25dcdf0ec3
parent9216cffaaa1ef137ef5bdb5b290a930cc6198850 (diff)
Imported Upstream version 0.3upstream/0.3
-rw-r--r--AAC.v4
-rw-r--r--CHANGELOG5
-rw-r--r--Caveats.v2
-rw-r--r--Instances.v22
-rw-r--r--Makefile326
-rw-r--r--README.txt7
-rw-r--r--Tutorial.v2
-rw-r--r--aac.mlpack7
-rw-r--r--coq.ml (renamed from AAC_coq.ml)7
-rw-r--r--coq.mli (renamed from AAC_coq.mli)0
-rw-r--r--helper.ml (renamed from AAC_helper.ml)0
-rw-r--r--helper.mli (renamed from AAC_helper.mli)0
-rw-r--r--magic.txt5
-rwxr-xr-xmake_makefile62
-rw-r--r--matcher.ml (renamed from AAC_matcher.ml)6
-rw-r--r--matcher.mli (renamed from AAC_matcher.mli)6
-rw-r--r--print.ml (renamed from AAC_print.ml)32
-rw-r--r--print.mli (renamed from AAC_print.mli)8
-rw-r--r--rewrite.ml4 (renamed from AAC_rewrite.ml)206
-rw-r--r--rewrite.mli (renamed from AAC_rewrite.mli)0
-rw-r--r--search_monad.ml (renamed from AAC_search_monad.ml)0
-rw-r--r--search_monad.mli (renamed from AAC_search_monad.mli)0
-rw-r--r--theory.ml (renamed from AAC_theory.ml)304
-rw-r--r--theory.mli (renamed from AAC_theory.mli)28
24 files changed, 346 insertions, 693 deletions
diff --git a/AAC.v b/AAC.v
index 0f5e85d..a16f1a0 100644
--- a/AAC.v
+++ b/AAC.v
@@ -82,7 +82,7 @@ Proof.
Qed.
Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E}
- {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4.
+ {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4 := {}.
@@ -1132,4 +1132,4 @@ Section t.
End t.
-Declare ML Module "aac_tactics".
+Declare ML Module "aac".
diff --git a/CHANGELOG b/CHANGELOG
index 84b2aae..13e9a02 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+
+AAC_tactics 0.3 :
+-----------------
+- New release for Coq 8.4
+
AAC_tactics 0.2-pl2 :
-----------------
diff --git a/Caveats.v b/Caveats.v
index 0d0d5ca..a7967cc 100644
--- a/Caveats.v
+++ b/Caveats.v
@@ -13,8 +13,6 @@
with the path to the [aac_tactics] library
*)
-Add Rec LoadPath "." as AAC_tactics.
-Add ML Path ".".
Require Import AAC.
Require Instances.
diff --git a/Instances.v b/Instances.v
index bb309fe..8ddf9e4 100644
--- a/Instances.v
+++ b/Instances.v
@@ -19,7 +19,7 @@ Proof. intros x y ->. reflexivity. Qed.
(* At the moment, all the instances are exported even if they are packaged into modules. Even using LocalInstances in fact*)
Module Peano.
- Require Import Arith NArith Max.
+ Require Import Arith NArith Max Min.
Instance aac_plus_Assoc : Associative eq plus := plus_assoc.
Instance aac_plus_Comm : Commutative eq plus := plus_comm.
@@ -82,7 +82,7 @@ End Lists.
Module N.
- Require Import NArith Nminmax.
+ Require Import NArith.
Open Scope N_scope.
Instance aac_Nplus_Assoc : Associative eq Nplus := Nplus_assoc.
Instance aac_Nplus_Comm : Commutative eq Nplus := Nplus_comm.
@@ -101,13 +101,13 @@ Module N.
Instance aac_zero_max : Unit eq Nmax 0 := Build_Unit eq Nmax 0 N.max_0_l N.max_0_r.
(* We also provide liftings from le to eq *)
- Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.T.le_refl N.T.le_trans.
+ Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.le_refl N.le_trans.
Instance lift_le_eq : AAC_lift Nle eq := Build_AAC_lift eq_equivalence _.
End N.
Module P.
- Require Import NArith Pminmax.
+ Require Import NArith.
Open Scope positive_scope.
Instance aac_Pplus_Assoc : Associative eq Pplus := Pplus_assoc.
Instance aac_Pplus_Comm : Commutative eq Pplus := Pplus_comm.
@@ -115,18 +115,18 @@ Module P.
Instance aac_Pmult_Comm : Commutative eq Pmult := Pmult_comm.
Instance aac_Pmult_Assoc : Associative eq Pmult := Pmult_assoc.
- Instance aac_Pmin_Comm : Commutative eq Pmin := P.min_comm.
- Instance aac_Pmin_Assoc : Associative eq Pmin := P.min_assoc.
+ Instance aac_Pmin_Comm : Commutative eq Pmin := Pos.min_comm.
+ Instance aac_Pmin_Assoc : Associative eq Pmin := Pos.min_assoc.
- Instance aac_Pmax_Comm : Commutative eq Pmax := P.max_comm.
- Instance aac_Pmax_Assoc : Associative eq Pmax := P.max_assoc.
+ Instance aac_Pmax_Comm : Commutative eq Pmax := Pos.max_comm.
+ Instance aac_Pmax_Assoc : Associative eq Pmax := Pos.max_assoc.
Instance aac_one : Unit eq Pmult 1 := Build_Unit eq Pmult 1 _ Pmult_1_r.
intros; reflexivity. Qed. (* TODO : add this lemma in the stdlib *)
- Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 P.max_1_l P.max_1_r.
+ Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 Pos.max_1_l Pos.max_1_r.
(* We also provide liftings from le to eq *)
- Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple P.T.le_refl P.T.le_trans.
+ Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple Pos.le_refl Pos.le_trans.
Instance lift_le_eq : AAC_lift Ple eq := Build_AAC_lift eq_equivalence _.
End P.
@@ -148,7 +148,7 @@ Module Q.
Instance aac_zero_Qplus : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r.
(* We also provide liftings from le to eq *)
- Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Q.T.le_refl Q.T.le_trans.
+ Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Qle_refl Qle_trans.
Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _.
End Q.
diff --git a/Makefile b/Makefile
index a56d4b6..1043ce9 100644
--- a/Makefile
+++ b/Makefile
@@ -1,319 +1,29 @@
-#############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.3 ##
-#############################################################################
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-#
-# This Makefile was generated by the command line :
-# coq_makefile -R . AAC_tactics -opt MLIFILES = $(MLFILES:.ml=.mli) AAC_coq.ml AAC_helper.ml AAC_search_monad.ml AAC_matcher.ml AAC_theory.ml AAC_print.ml AAC_rewrite.ml AAC.v Instances.v Tutorial.v Caveats.v -f magic.txt
-#
+FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli rewrite.mli \
+ coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \
+ aac.mlpack \
+ AAC.v Instances.v Tutorial.v Caveats.v
-#
-# This Makefile may take 3 arguments passed as environment variables:
-# - COQBIN to specify the directory where Coq binaries resides;
-# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.
-COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
-CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')"
-ifndef CAMLP4BIN
- CAMLP4BIN:=$(CAMLBIN)
-endif
+ARGS := -R . AAC_tactics
-CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)
+.PHONY: coq clean
-##########################
-# #
-# Libraries definitions. #
-# #
-##########################
+world: all doc
-OCAMLLIBS:=
-COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \
- -I $(COQLIB)/library -I $(COQLIB)/parsing \
- -I $(COQLIB)/pretyping -I $(COQLIB)/interp \
- -I $(COQLIB)/proofs -I $(COQLIB)/tactics \
- -I $(COQLIB)/toplevel \
+all: Makefile.coq
+ $(MAKE) -f Makefile.coq all
+coq: Makefile.coq
+ $(MAKE) -f Makefile.coq
+doc: Makefile.coq
+ $(MAKE) -f Makefile.coq html
+Makefile.coq: Makefile $(VS)
+ coq_makefile $(ARGS) $(FILES) -o Makefile.coq
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-COQLIBS:= -R . AAC_tactics
-COQDOCLIBS:=-R . AAC_tactics
-
-##########################
-# #
-# Variables definitions. #
-# #
-##########################
-
-ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
-OPT:=
-COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
-ifdef CAMLBIN
- COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)
-endif
-COQC:=$(COQBIN)coqc
-COQDEP:=$(COQBIN)coqdep -c
-GALLINA:=$(COQBIN)gallina
-COQDOC:=$(COQBIN)coqdoc
-COQMKTOP:=$(COQBIN)coqmktop
-CAMLLIB:=$(shell $(CAMLBIN)ocamlc -where)
-CAMLC:=$(CAMLBIN)ocamlc -c -rectypes
-CAMLOPTC:=$(CAMLBIN)ocamlopt -c -rectypes
-CAMLLINK:=$(CAMLBIN)ocamlc -rectypes
-CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes
-GRAMMARS:=grammar.cma
-CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
-CAMLP4OPTIONS:=
-MLIFILES=$(MLFILES:.ml=.mli)
-PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
-
-###################################
-# #
-# Definition of the "all" target. #
-# #
-###################################
-
-VFILES:=AAC.v\
- Instances.v\
- Tutorial.v\
- Caveats.v
-VOFILES:=$(VFILES:.v=.vo)
-GLOBFILES:=$(VFILES:.v=.glob)
-VIFILES:=$(VFILES:.v=.vi)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-MLFILES:=AAC_coq.ml\
- AAC_helper.ml\
- AAC_search_monad.ml\
- AAC_matcher.ml\
- AAC_theory.ml\
- AAC_print.ml\
- AAC_rewrite.ml
-CMOFILES:=$(MLFILES:.ml=.cmo)
-CMIFILES:=$(MLFILES:.ml=.cmi)
-CMXFILES:=$(MLFILES:.ml=.cmx)
-CMXSFILES:=$(MLFILES:.ml=.cmxs)
-OFILES:=$(MLFILES:.ml=.o)
-
-all: $(VOFILES) $(CMOFILES) $(CMXSFILES) doc\
- aac_tactics.cmxs\
- aac_tactics.cmxa\
- aac_tactics.cma\
- .depend
-spec: $(VIFILES)
-
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
- $(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all-gal.ps: $(VFILES)
- $(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all.pdf: $(VFILES)
- $(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all-gal.pdf: $(VFILES)
- $(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-
-
-###################
-# #
-# Custom targets. #
-# #
-###################
-
-doc: $(MLIFILES)
- mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc
-
-aac_tactics.cmxs: $(CMXFILES)
- $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)
-
-aac_tactics.cmxa: $(CMXFILES)
- $(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES)
-
-aac_tactics.cma: $(CMOFILES)
- $(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)
-
-.depend: $(MLIFILES)
- $(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend
-
-####################
-# #
-# Special targets. #
-# #
-####################
-
-.PHONY: all opt byte archclean clean install depend html
-
-%.cmi: %.mli
- $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.cmo: %.ml
- $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<
-
-%.cmx: %.ml
- $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<
-
-%.cmxs: %.ml
- $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<
-
-%.cmo: %.ml4
- $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-%.cmx: %.ml4
- $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-%.cmxs: %.ml4
- $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<
-
-%.ml.d: %.ml
- $(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $(PP) "$<" > "$@"
-
-%.vo %.glob: %.v
- $(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-%.vi: %.v
- $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-%.g: %.v
- $(GALLINA) $<
-
-%.tex: %.v
- $(COQDOC) -latex $< -o $@
-
-%.html: %.v %.glob
- $(COQDOC) -html $< -o $@
-
-%.g.tex: %.v
- $(COQDOC) -latex -g $< -o $@
-
-%.g.html: %.v %.glob
- $(COQDOC) -html -g $< -o $@
-
-%.v.d: %.v
- $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-byte:
- $(MAKE) all "OPT:=-byte"
-
-opt:
- $(MAKE) all "OPT:=-opt"
-
-install:
- mkdir -p $(COQLIB)/user-contrib
- (for i in $(VOFILES); do \
- install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
- install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
- done)
- (for i in $(CMOFILES); do \
- install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
- install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
- done)
- (for i in $(CMIFILES); do \
- install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
- install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
- done)
- (for i in $(CMXSFILES); do \
- install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
- install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
- done)
-
-clean:
- rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~
- rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
- rm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)
- - rm -rf html
- - rm -rf doc
- - rm -f aac_tactics.cmxs
- - rm -f aac_tactics.cmxa
- - rm -f aac_tactics.cma
- - rm -f .depend
-
-archclean:
- rm -f *.cmx *.o
-
-
-printenv:
- @echo CAMLC = $(CAMLC)
- @echo CAMLOPTC = $(CAMLOPTC)
- @echo CAMLP4LIB = $(CAMLP4LIB)
-
-.dummy: magic.txt
- mv -f Makefile Makefile.bak
- $(COQBIN)coq_makefile -f magic.txt -o Makefile
-
-
--include $(VFILES:.v=.v.d)
-.SECONDARY: $(VFILES:.v=.v.d)
-
--include $(MLFILES:.ml=.ml.d)
-.SECONDARY: $(MLFILES:.ml=.ml.d)
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-
-
-# override inadequate coq_makefile auto-regeneration
-Makefile: make_makefile magic.txt files.txt
- ./make_makefile
-
-# We want to keep the proofs in Caveats and the Tutorial
-world: $(VOFILES) doc
- - mkdir -p html
- $(COQDOC) -toc -utf8 -html -g $(COQDOCLIBS) -d html $(VFILES)
- $(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Tutorial.v
- $(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Caveats.v
-
-# additional dependencies for AAC (since aac_tactics.cmxs/cma are not
-# around the first time we run make, coqdep issues a warning and
-# ignores this dependency)
-# (one can safely select one of theses dependencies according to
-# coq' compilation mode--bytecode or native)
-AAC.vo: aac_tactics.cmxa aac_tactics.cmxs aac_tactics.cma
-
-# .depend contains dependencies for .mli files
--include .depend
-.SECONDARY: .depend
+clean:: Makefile.coq
+ $(MAKE) -f Makefile.coq clean
+ rm -f Makefile.coq .depend
diff --git a/README.txt b/README.txt
index ae945cc..d308f70 100644
--- a/README.txt
+++ b/README.txt
@@ -18,11 +18,10 @@ equations, modulo associativity and commutativity of some operators.
INSTALLATION
============
-This plugin should work with Coq v8.3, as released on the 14th of
-October 2010.
+This plugin should work with Coq v8.4
-- run [./make_makefile] in the top-level directory to generate a Makefile
-- run [make world] to build the plugin and the documentation
+- running [make] in the top-level directory will generate a Makefile
+ (using coq_makefile), and will build the plugin and its documentation
Option 1
--------
diff --git a/Tutorial.v b/Tutorial.v
index 8b4c753..76006ca 100644
--- a/Tutorial.v
+++ b/Tutorial.v
@@ -311,7 +311,7 @@ Section Peano.
can specify which equivalence relation to use by declaring
instances of the [AAC_lift] type class: *)
- Instance lift_le_eq : AAC_lift le eq.
+ Instance lift_le_eq : AAC_lift le eq := {}.
(** (This instance is automatically inferred because [eq] is always a
valid candidate, here for [le].) *)
diff --git a/aac.mlpack b/aac.mlpack
new file mode 100644
index 0000000..0c12567
--- /dev/null
+++ b/aac.mlpack
@@ -0,0 +1,7 @@
+Coq
+Helper
+Search_monad
+Matcher
+Theory
+Print
+Rewrite
diff --git a/AAC_coq.ml b/coq.ml
index b3ee180..7371913 100644
--- a/AAC_coq.ml
+++ b/coq.ml
@@ -27,7 +27,7 @@ let init_constant dir s = find_constant contrib_name dir s
in the goal *)
let nowhere =
{ Tacexpr.onhyps = Some [];
- Tacexpr.concl_occs = Rawterm.no_occurrences_expr
+ Tacexpr.concl_occs = Glob_term.no_occurrences_expr
}
let cps_mk_letin
@@ -164,7 +164,7 @@ end
module Pos = struct
- let path = ["Coq" ; "NArith"; "BinPos"]
+ let path = ["Coq" ; "PArith"; "BinPos"]
let typ = lazy (init_constant path "positive")
let xI = lazy (init_constant path "xI")
let xO = lazy (init_constant path "xO")
@@ -577,8 +577,9 @@ let rewrite ?(abort=false)hypinfo subst k =
Equality.general_rewrite_bindings
hypinfo.l2r
Termops.all_occurrences
+ true (* tell if existing evars must be frozen for instantiation *)
false
- (rew,Rawterm.NoBindings)
+ (rew,Glob_term.NoBindings)
true
else
Tacticals.tclIDTAC
diff --git a/AAC_coq.mli b/coq.mli
index a0f2ce0..a0f2ce0 100644
--- a/AAC_coq.mli
+++ b/coq.mli
diff --git a/AAC_helper.ml b/helper.ml
index 637def1..637def1 100644
--- a/AAC_helper.ml
+++ b/helper.ml
diff --git a/AAC_helper.mli b/helper.mli
index f4e4454..f4e4454 100644
--- a/AAC_helper.mli
+++ b/helper.mli
diff --git a/magic.txt b/magic.txt
deleted file mode 100644
index d1c9191..0000000
--- a/magic.txt
+++ /dev/null
@@ -1,5 +0,0 @@
--custom "mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc" "$(MLIFILES)" doc
--custom "$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxs
--custom "$(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxa
--custom "$(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)" "$(CMOFILES)" aac_tactics.cma
--custom "$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend" "$(MLIFILES)" .depend
diff --git a/make_makefile b/make_makefile
deleted file mode 100755
index 1cef3d3..0000000
--- a/make_makefile
+++ /dev/null
@@ -1,62 +0,0 @@
-#!/bin/sh
-# - set variable MLIFILES so that it can be used in custom targets to
-# build documentation and dependencies for .mli files
-# - remove useless ' -I . .../plugins/ ' lines so that we can read something in the compilation log
-# - rename the rule for Makefile auto-regeneration, and replace it with an appropriate command
-# - patch the rule for cleaning doc
-# - include the .depend custom target, to take .mli dependencies into account
-# - added some hackish settings of Variables, in order to be able to install the plugin in user-contrib (coq_makefile should define a "INSTALL" variables that we can modify, instead of copying 4 times the same code in install !)
-
-set -e
-
-if [ -f `ocamlc -where`/dynlink.cmxa ]; then
- BEST=opt
- CMXA=aac_tactics.cmxa
- CMXS=aac_tactics.cmxs
-else
- BEST=byte
- if which ocamlopt >/dev/null; then
- CMXA=aac_tactics.cmxa
- fi
-fi
-
-(
-coq_makefile -R . AAC_tactics -$BEST MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \
- | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g;s|\.opt||g'
-cat <<EOF
-
-
-# override inadequate coq_makefile auto-regeneration
-Makefile: make_makefile magic.txt files.txt
- ./make_makefile
-
-# We want to keep the proofs in Caveats and the Tutorial
-world: \$(VOFILES) doc
- - mkdir -p html
- \$(COQDOC) -toc -utf8 -html -g \$(COQDOCLIBS) -d html \$(VFILES)
- \$(COQDOC) --no-index --no-externals -s -utf8 -html \$(COQDOCLIBS) -d html Tutorial.v
- \$(COQDOC) --no-index --no-externals -s -utf8 -html \$(COQDOCLIBS) -d html Caveats.v
-
-# additional dependencies for AAC (since aac_tactics.cmxs/cma are not
-# around the first time we run make, coqdep issues a warning and
-# ignores this dependency)
-# (one can safely select one of theses dependencies according to
-# coq' compilation mode--bytecode or native)
-AAC.vo: $CMXA $CMXS aac_tactics.cma
-
-# .depend contains dependencies for .mli files
--include .depend
-.SECONDARY: .depend
-
-EOF
-) > Makefile
-
-
-
-# TOTHINK: coq_makefile est bête, [make all] compile systématiquement
-# les .cmxs associés à chaque module, alors que ça ne sert à rien,
-# seul aac_rewrite.cmxs compte
-
-# problemes lorsqu'un module porte un meme nom qu'un module predefini
-# (matching par exemple), prendre garde si ce probleme s'etend a la
-# confusion module/nom de librairie
diff --git a/AAC_matcher.ml b/matcher.ml
index 5d738e0..55a64b7 100644
--- a/AAC_matcher.ml
+++ b/matcher.ml
@@ -38,10 +38,10 @@ struct
let printing = false
end
-module Debug = AAC_helper.Debug (Control)
+module Debug = Helper.Debug (Control)
open Debug
-module Search = AAC_search_monad (* a handle *)
+module Search = Search_monad (* a handle *)
type symbol = int
type var = int
@@ -116,7 +116,7 @@ module Terms : sig
A term in normal form is the canonical representative of the
equivalence class of all the terms that are equal modulo
- Associativity and Commutativity. Outside the {!AAC_matcher} module,
+ Associativity and Commutativity. Outside the {!Matcher} module,
one does not need to access the actual representation of this
type. *)
diff --git a/AAC_matcher.mli b/matcher.mli
index 896a2a9..a6b6f46 100644
--- a/AAC_matcher.mli
+++ b/matcher.mli
@@ -22,7 +22,7 @@
subject must make a perfect match against the pattern ([x+x] does
not match [a+a+b] ).
- We use a search monad {!AAC_search_monad} to perform non-deterministic
+ We use a search monad {!Search_monad} to perform non-deterministic
choices in an almost transparent way.
We also provide a function {!subterm} for finding a match that is
@@ -175,7 +175,7 @@ end
while x+x+y does not match a+b+c, since this would require to
assign 1 to x).
*)
-val matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t AAC_search_monad.m
+val matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t Search_monad.m
(** [subterm p t] computes a set of solutions to the given
subterm-matching problem.
@@ -185,5 +185,5 @@ val matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t AAC_sea
problem). The context is actually a {!Terms.t} where the variables
are yet to be instantiated by one of the associated substitutions
*)
-val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t AAC_search_monad.m) AAC_search_monad.m
+val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t Search_monad.m) Search_monad.m
diff --git a/AAC_print.ml b/print.ml
index 512efa3..1ceb786 100644
--- a/AAC_print.ml
+++ b/print.ml
@@ -9,7 +9,7 @@
(* A very basic way to interact with the envs, to choose a possible
solution *)
open Pp
-open AAC_matcher
+open Matcher
type named_env = (Names.name * Terms.t) list
@@ -31,9 +31,9 @@ let pp_env pt : named_env -> Pp.std_ppcmds = fun env ->
(** {pp_envm} prints a collection of possible environments, and number
them. This number must remain compatible with the parameters given to
{!aac_rewrite} *)
-let pp_envm pt : named_env AAC_search_monad.m -> Pp.std_ppcmds = fun m ->
+let pp_envm pt : named_env Search_monad.m -> Pp.std_ppcmds = fun m ->
let _,s =
- AAC_search_monad.fold
+ Search_monad.fold
(fun env (n,acc) ->
n+1, h 0 (str (Printf.sprintf "%i:\t[" n) ++pp_env pt env ++ str "]") ++ fnl () :: acc
) m (0,[])
@@ -41,20 +41,20 @@ let pp_envm pt : named_env AAC_search_monad.m -> Pp.std_ppcmds = fun m ->
List.fold_left (fun acc s -> s ++ acc) (str "") (s)
let trivial_substitution envm =
- match AAC_search_monad.choose envm with
+ match Search_monad.choose envm with
| None -> true (* assert false *)
| Some l -> l=[]
(** {pp_all} prints a collection of possible contexts and related
possibles substitutions, giving a number to each. This number must
remain compatible with the parameters of {!aac_rewrite} *)
-let pp_all pt : (int * Terms.t * named_env AAC_search_monad.m) AAC_search_monad.m -> Pp.std_ppcmds = fun m ->
- let _,s = AAC_search_monad.fold
+let pp_all pt : (int * Terms.t * named_env Search_monad.m) Search_monad.m -> Pp.std_ppcmds = fun m ->
+ let _,s = Search_monad.fold
(fun (size,context,envm) (n,acc) ->
let s = str (Printf.sprintf "occurence %i: transitivity through " n) in
let s = s ++ pt context ++ str "\n" in
let s = if trivial_substitution envm then s else
- s ++ str (Printf.sprintf "%i possible(s) substitution(s)" (AAC_search_monad.count envm) )
+ s ++ str (Printf.sprintf "%i possible(s) substitution(s)" (Search_monad.count envm) )
++ fnl () ++ pp_envm pt envm
in
n+1, s::acc
@@ -64,19 +64,19 @@ let pp_all pt : (int * Terms.t * named_env AAC_search_monad.m) AAC_search_monad.
(** The main printing function. {!print} uses the debruijn_env the
rename the variables, and rebuilds raw Coq terms (for the context, and
the terms in the environment). In order to do so, it requires the
-information gathered by the {!AAC_theory.Trans} module.*)
+information gathered by the {!Theory.Trans} module.*)
let print rlt ir m (context : Term.rel_context) goal =
- if AAC_search_monad.count m = 0
+ if Search_monad.count m = 0
then
(
Tacticals.tclFAIL 0 (Pp.str "No subterm modulo AC") goal
)
else
let _ = Pp.msgnl (Pp.str "All solutions:") in
- let m = AAC_search_monad.(>>) m
+ let m = Search_monad.(>>) m
(fun (i,t,envm) ->
- let envm = AAC_search_monad.(>>) envm ( fun env ->
- let l = AAC_matcher.Subst.to_list env in
+ let envm = Search_monad.(>>) envm ( fun env ->
+ let l = Matcher.Subst.to_list env in
let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in
let l =
List.map (fun (v,t) ->
@@ -84,16 +84,16 @@ let print rlt ir m (context : Term.rel_context) goal =
(name,t)
) l
in
- AAC_search_monad.return l
+ Search_monad.return l
)
in
- AAC_search_monad.return (i,t,envm)
+ Search_monad.return (i,t,envm)
)
in
- let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in
+ let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in
let _ = Pp.msgnl
(pp_all
- (fun t -> Printer.pr_constr (AAC_theory.Trans.raw_constr_of_t ir rlt context t) ) m
+ (fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t ir rlt context t) ) m
)
in
Tacticals.tclIDTAC goal
diff --git a/AAC_print.mli b/print.mli
index bacd806..5b3dc15 100644
--- a/AAC_print.mli
+++ b/print.mli
@@ -13,11 +13,11 @@
(** The main printing function. {!print} uses the [Term.rel_context]
to rename the variables, and rebuilds raw Coq terms (for the given
context, and the terms in the environment). In order to do so, it
- requires the information gathered by the {!AAC_theory.Trans} module.*)
+ requires the information gathered by the {!Theory.Trans} module.*)
val print :
- AAC_coq.Relation.t ->
- AAC_theory.Trans.ir ->
- (int * AAC_matcher.Terms.t * AAC_matcher.Subst.t AAC_search_monad.m) AAC_search_monad.m ->
+ Coq.Relation.t ->
+ Theory.Trans.ir ->
+ (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m ->
Term.rel_context ->
Proof_type.tactic
diff --git a/AAC_rewrite.ml b/rewrite.ml4
index be286f9..6229262 100644
--- a/AAC_rewrite.ml
+++ b/rewrite.ml4
@@ -15,11 +15,11 @@ module Control = struct
let time = false
end
-module Debug = AAC_helper.Debug (Control)
+module Debug = Helper.Debug (Control)
open Debug
let time_tac msg tac =
- if Control.time then AAC_coq.tclTIME msg tac else tac
+ if Control.time then Coq.tclTIME msg tac else tac
let tac_or_exn tac exn msg = fun gl ->
try tac gl with e ->
@@ -30,9 +30,9 @@ let tac_or_exn tac exn msg = fun gl ->
except if a another one was previously raised *)
let push_anomaly msg = function
| Util.Anomaly _ as e -> raise e
- | _ -> AAC_coq.anomaly msg
+ | _ -> Coq.anomaly msg
-module M = AAC_matcher
+module M = Matcher
open Term
open Names
@@ -41,18 +41,18 @@ open Proof_type
(** The various kind of relation we can encounter, as a hierarchy *)
type rew_relation =
- | Bare of AAC_coq.Relation.t
- | Transitive of AAC_coq.Transitive.t
- | Equivalence of AAC_coq.Equivalence.t
+ | Bare of Coq.Relation.t
+ | Transitive of Coq.Transitive.t
+ | Equivalence of Coq.Equivalence.t
(** {!promote try to go higher in the aforementionned hierarchy} *)
-let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) =
- try AAC_coq.Equivalence.cps_from_relation rlt
+let promote (rlt : Coq.Relation.t) (k : rew_relation -> Proof_type.tactic) =
+ try Coq.Equivalence.cps_from_relation rlt
(fun e -> k (Equivalence e))
with
| Not_found ->
begin
- try AAC_coq.Transitive.cps_from_relation rlt
+ try Coq.Transitive.cps_from_relation rlt
(fun trans -> k (Transitive trans))
with
|Not_found -> k (Bare rlt)
@@ -70,7 +70,7 @@ let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) =
p <= q |- left >= right : failure
*)
-(** aac_lift : the ideal type beyond AAC.v/AAC_lift
+(** aac_lift : the ideal type beyond AAC.v/Lift
A base relation r, together with an equivalence relation, and the
proof that the former lifts to the later. Howver, we have to
@@ -78,44 +78,44 @@ let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) =
lift connects the two things *)
type aac_lift =
{
- r : AAC_coq.Relation.t;
- e : AAC_coq.Equivalence.t;
+ r : Coq.Relation.t;
+ e : Coq.Equivalence.t;
lift : Term.constr
}
type rewinfo =
{
- hypinfo : AAC_coq.Rewrite.hypinfo;
+ hypinfo : Coq.Rewrite.hypinfo;
in_left : bool; (** are we rewriting in the left hand-sie of the goal *)
pattern : constr;
subject : constr;
- morph_rlt : AAC_coq.Relation.t; (** the relation we look for in morphism *)
- eqt : AAC_coq.Equivalence.t; (** the equivalence we use as workbase *)
- rlt : AAC_coq.Relation.t; (** the relation in the goal *)
+ morph_rlt : Coq.Relation.t; (** the relation we look for in morphism *)
+ eqt : Coq.Equivalence.t; (** the equivalence we use as workbase *)
+ rlt : Coq.Relation.t; (** the relation in the goal *)
lifting: aac_lift
}
-let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tactic) : Proof_type.tactic =
- AAC_coq.cps_evar_relation rlt.AAC_coq.Relation.carrier (fun e ->
+let infer_lifting (rlt: Coq.Relation.t) (k : lift:aac_lift -> Proof_type.tactic) : Proof_type.tactic =
+ Coq.cps_evar_relation rlt.Coq.Relation.carrier (fun e ->
let lift_ty =
- mkApp (Lazy.force AAC_theory.Stubs.lift,
+ mkApp (Lazy.force Theory.Stubs.lift,
[|
- rlt.AAC_coq.Relation.carrier;
- rlt.AAC_coq.Relation.r;
+ rlt.Coq.Relation.carrier;
+ rlt.Coq.Relation.r;
e
|]
) in
- AAC_coq.cps_resolve_one_typeclass ~error:"Cannot infer a lifting"
+ Coq.cps_resolve_one_typeclass ~error:"Cannot infer a lifting"
lift_ty (fun lift goal ->
- let x = rlt.AAC_coq.Relation.carrier in
- let r = rlt.AAC_coq.Relation.r in
- let eq = (AAC_coq.nf_evar goal e) in
- let equiv = AAC_coq.lapp AAC_theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in
+ let x = rlt.Coq.Relation.carrier in
+ let r = rlt.Coq.Relation.r in
+ let eq = (Coq.nf_evar goal e) in
+ let equiv = Coq.lapp Theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in
let lift =
{
r = rlt;
- e = AAC_coq.Equivalence.make x eq equiv;
+ e = Coq.Equivalence.make x eq equiv;
lift = lift;
}
in
@@ -124,16 +124,16 @@ let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tac
(** Builds a rewinfo, once and for all *)
let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) : Proof_type.tactic=
- let l2r = hypinfo.AAC_coq.Rewrite.l2r in
+ let l2r = hypinfo.Coq.Rewrite.l2r in
infer_lifting rlt
(fun ~lift ->
let eq = lift.e in
k {
hypinfo = hypinfo;
in_left = in_left;
- pattern = if l2r then hypinfo.AAC_coq.Rewrite.left else hypinfo.AAC_coq.Rewrite.right;
+ pattern = if l2r then hypinfo.Coq.Rewrite.left else hypinfo.Coq.Rewrite.right;
subject = if in_left then left else right;
- morph_rlt = AAC_coq.Equivalence.to_relation eq;
+ morph_rlt = Coq.Equivalence.to_relation eq;
eqt = eq;
lifting = lift;
rlt = rlt
@@ -146,34 +146,34 @@ let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic )
(** Build the reifiers, the reified terms, and the evaluation fonction *)
-let handle eqt zero envs (t : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) k =
+let handle eqt zero envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) k =
- let (x,r,_) = AAC_coq.Equivalence.split eqt in
- AAC_theory.Trans.mk_reifier (AAC_coq.Equivalence.to_relation eqt) zero envs
+ let (x,r,_) = Coq.Equivalence.split eqt in
+ Theory.Trans.mk_reifier (Coq.Equivalence.to_relation eqt) zero envs
(fun (maps, reifier) ->
(* fold through a term and reify *)
- let t = AAC_theory.Trans.reif_constr_of_t reifier t in
- let t' = AAC_theory.Trans.reif_constr_of_t reifier t' in
+ let t = Theory.Trans.reif_constr_of_t reifier t in
+ let t' = Theory.Trans.reif_constr_of_t reifier t' in
(* Some letins *)
- let eval = (mkApp (Lazy.force AAC_theory.Stubs.eval, [|x;r; maps.AAC_theory.Trans.env_sym; maps.AAC_theory.Trans.env_bin; maps.AAC_theory.Trans.env_units|])) in
+ let eval = (mkApp (Lazy.force Theory.Stubs.eval, [|x;r; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_bin; maps.Theory.Trans.env_units|])) in
- AAC_coq.cps_mk_letin "eval" eval (fun eval ->
- AAC_coq.cps_mk_letin "left" t (fun t ->
- AAC_coq.cps_mk_letin "right" t' (fun t' ->
+ Coq.cps_mk_letin "eval" eval (fun eval ->
+ Coq.cps_mk_letin "left" t (fun t ->
+ Coq.cps_mk_letin "right" t' (fun t' ->
k maps eval t t'))))
(** [by_aac_reflexivity] is a sub-tactic that closes a sub-goal that
is merely a proof of equality of two terms modulo AAC *)
let by_aac_reflexivity zero
- eqt envs (t : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) : Proof_type.tactic =
+ eqt envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) : Proof_type.tactic =
handle eqt zero envs t t'
(fun maps eval t t' ->
- let (x,r,e) = AAC_coq.Equivalence.split eqt in
- let decision_thm = AAC_coq.lapp AAC_theory.Stubs.decide_thm
+ let (x,r,e) = Coq.Equivalence.split eqt in
+ let decision_thm = Coq.lapp Theory.Stubs.decide_thm
[|x;r;e;
- maps.AAC_theory.Trans.env_sym;
- maps.AAC_theory.Trans.env_bin;
- maps.AAC_theory.Trans.env_units;
+ maps.Theory.Trans.env_sym;
+ maps.Theory.Trans.env_bin;
+ maps.Theory.Trans.env_units;
t;t';
|]
in
@@ -185,8 +185,8 @@ let by_aac_reflexivity zero
(Tacticals.tclTHENLIST
[
convert ;
- tac_or_exn apply_tac AAC_coq.user_error "unification failure";
- tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) AAC_coq.anomaly "vm_compute failure";
+ tac_or_exn apply_tac Coq.user_error "unification failure";
+ tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) Coq.anomaly "vm_compute failure";
Tacticals.tclORELSE Tactics.reflexivity
(Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
])
@@ -197,20 +197,20 @@ let by_aac_normalise zero lift ir t t' =
let rlt = lift.r in
handle eqt zero ir t t'
(fun maps eval t t' ->
- let (x,r,e) = AAC_coq.Equivalence.split eqt in
- let normalise_thm = AAC_coq.lapp AAC_theory.Stubs.lift_normalise_thm
+ let (x,r,e) = Coq.Equivalence.split eqt in
+ let normalise_thm = Coq.lapp Theory.Stubs.lift_normalise_thm
[|x;r;e;
- maps.AAC_theory.Trans.env_sym;
- maps.AAC_theory.Trans.env_bin;
- maps.AAC_theory.Trans.env_units;
- rlt.AAC_coq.Relation.r;
+ maps.Theory.Trans.env_sym;
+ maps.Theory.Trans.env_bin;
+ maps.Theory.Trans.env_units;
+ rlt.Coq.Relation.r;
lift.lift;
t;t';
|]
in
(* This convert is required to deal with evars in a proper
way *)
- let convert_to = mkApp (rlt.AAC_coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in
+ let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in
let convert = Tactics.convert_concl convert_to Term.VMcast in
let apply_tac = Tactics.apply normalise_thm in
(Tacticals.tclTHENLIST
@@ -224,19 +224,19 @@ let by_aac_normalise zero lift ir t t' =
(** A handler tactic, that reifies the goal, and infer the liftings,
and then call its continuation *)
let aac_conclude
- (k : Term.constr -> aac_lift -> AAC_theory.Trans.ir -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) = fun goal ->
+ (k : Term.constr -> aac_lift -> Theory.Trans.ir -> Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic) = fun goal ->
let (equation : Term.types) = Tacmach.pf_concl goal in
- let envs = AAC_theory.Trans.empty_envs () in
+ let envs = Theory.Trans.empty_envs () in
let left, right,r =
- match AAC_coq.match_as_equation goal equation with
- | None -> AAC_coq.user_error "The goal is not an applied relation"
+ match Coq.match_as_equation goal equation with
+ | None -> Coq.user_error "The goal is not an applied relation"
| Some x -> x in
try infer_lifting r
(fun ~lift goal ->
- let eq = AAC_coq.Equivalence.to_relation lift.e in
- let tleft,tright, goal = AAC_theory.Trans.t_of_constr goal eq envs (left,right) in
- let goal, ir = AAC_theory.Trans.ir_of_envs goal eq envs in
+ let eq = Coq.Equivalence.to_relation lift.e in
+ let tleft,tright, goal = Theory.Trans.t_of_constr goal eq envs (left,right) in
+ let goal, ir = Theory.Trans.ir_of_envs goal eq envs in
let concl = Tacmach.pf_concl goal in
let _ = pr_constr "concl "concl in
let evar_map = Tacmach.project goal in
@@ -246,7 +246,7 @@ let aac_conclude
goal
)goal
with
- | Not_found -> AAC_coq.user_error "No lifting from the goal's relation to an equivalence"
+ | Not_found -> Coq.user_error "No lifting from the goal's relation to an equivalence"
open Libnames
open Tacinterp
@@ -273,17 +273,17 @@ let aac_normalise = fun goal ->
let aac_reflexivity = fun goal ->
aac_conclude
(fun zero lift ir t t' ->
- let x,r = AAC_coq.Relation.split (lift.r) in
- let r_reflexive = (AAC_coq.Classes.mk_reflexive x r) in
- AAC_coq.cps_resolve_one_typeclass ~error:"The goal's relation is not reflexive"
+ let x,r = Coq.Relation.split (lift.r) in
+ let r_reflexive = (Coq.Classes.mk_reflexive x r) in
+ Coq.cps_resolve_one_typeclass ~error:"The goal's relation is not reflexive"
r_reflexive
(fun reflexive ->
let lift_reflexivity =
- mkApp (Lazy.force (AAC_theory.Stubs.lift_reflexivity),
+ mkApp (Lazy.force (Theory.Stubs.lift_reflexivity),
[|
x;
r;
- lift.e.AAC_coq.Equivalence.eq;
+ lift.e.Coq.Equivalence.eq;
lift.lift;
reflexive
|])
@@ -297,28 +297,28 @@ let aac_reflexivity = fun goal ->
)
) goal
-(** A sub-tactic to lift the rewriting using AAC_lift *)
-let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq.Equivalence.t): tactic =
+(** A sub-tactic to lift the rewriting using Lift *)
+let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equivalence.t): tactic =
fun goal ->
(* catch the equation and the two members*)
let concl = Tacmach.pf_concl goal in
- let (left, right, _ ) = match AAC_coq.match_as_equation goal concl with
+ let (left, right, _ ) = match Coq.match_as_equation goal concl with
| Some x -> x
- | None -> AAC_coq.user_error "The goal is not an equation"
+ | None -> Coq.user_error "The goal is not an equation"
in
let lift_transitivity =
let thm =
if in_left
then
- Lazy.force AAC_theory.Stubs.lift_transitivity_left
+ Lazy.force Theory.Stubs.lift_transitivity_left
else
- Lazy.force AAC_theory.Stubs.lift_transitivity_right
+ Lazy.force Theory.Stubs.lift_transitivity_right
in
mkApp (thm,
[|
- preorder.AAC_coq.Relation.carrier;
- preorder.AAC_coq.Relation.r;
- using_eq.AAC_coq.Equivalence.eq;
+ preorder.Coq.Relation.carrier;
+ preorder.Coq.Relation.r;
+ using_eq.Coq.Equivalence.eq;
lifting;
step;
left;
@@ -335,15 +335,15 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq
let core_aac_rewrite ?abort
rewinfo
subst
- (by_aac_reflexivity : AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic)
+ (by_aac_reflexivity : Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic)
(tr : constr) t left : tactic =
pr_constr "transitivity through" tr;
let tran_tac =
lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt
in
- AAC_coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew ->
+ Coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew ->
Tacticals.tclTHENSV
- (tac_or_exn (tran_tac) AAC_coq.anomaly "Unable to make the transitivity step")
+ (tac_or_exn (tran_tac) Coq.anomaly "Unable to make the transitivity step")
(
if rewinfo.in_left
then [| by_aac_reflexivity left t ; rew |]
@@ -355,21 +355,21 @@ exception NoSolutions
(** Choose a substitution from a
- [(int * Terms.t * Env.env AAC_search_monad.m) AAC_search_monad.m ] *)
+ [(int * Terms.t * Env.env Search_monad.m) Search_monad.m ] *)
(* WARNING: Beware, since the printing function can change the order of the
printed monad, this function has to be updated accordingly *)
let choose_subst subterm sol m=
try
let (depth,pat,envm) = match subterm with
| None -> (* first solution *)
- List.nth ( List.rev (AAC_search_monad.to_list m)) 0
+ List.nth ( List.rev (Search_monad.to_list m)) 0
| Some x ->
- List.nth ( List.rev (AAC_search_monad.to_list m)) x
+ List.nth ( List.rev (Search_monad.to_list m)) x
in
let env = match sol with
None ->
- List.nth ( (AAC_search_monad.to_list envm)) 0
- | Some x -> List.nth ( (AAC_search_monad.to_list envm)) x
+ List.nth ( (Search_monad.to_list envm)) 0
+ | Some x -> List.nth ( (Search_monad.to_list envm)) x
in
pat, env
with
@@ -378,49 +378,49 @@ let choose_subst subterm sol m=
(** rewrite the constr modulo AC from left to right in the left member
of the goal *)
let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ~occ_subterm ~occ_sol ?extra : Proof_type.tactic = fun goal ->
- let envs = AAC_theory.Trans.empty_envs () in
+ let envs = Theory.Trans.empty_envs () in
let (concl : Term.types) = Tacmach.pf_concl goal in
let (_,_,rlt) as concl =
- match AAC_coq.match_as_equation goal concl with
- | None -> AAC_coq.user_error "The goal is not an applied relation"
+ match Coq.match_as_equation goal concl with
+ | None -> Coq.user_error "The goal is not an applied relation"
| Some (left, right, rlt) -> left,right,rlt
in
let check_type x =
- Tacmach.pf_conv_x goal x rlt.AAC_coq.Relation.carrier
+ Tacmach.pf_conv_x goal x rlt.Coq.Relation.carrier
in
- AAC_coq.Rewrite.get_hypinfo rew ~l2r ?check_type:(Some check_type)
+ Coq.Rewrite.get_hypinfo rew ~l2r ?check_type:(Some check_type)
(fun hypinfo ->
dispatch in_left concl hypinfo
(
fun rewinfo ->
let goal =
match extra with
- | Some t -> AAC_theory.Trans.add_symbol goal rewinfo.morph_rlt envs t
+ | Some t -> Theory.Trans.add_symbol goal rewinfo.morph_rlt envs t
| None -> goal
in
let pattern, subject, goal =
- AAC_theory.Trans.t_of_constr goal rewinfo.morph_rlt envs
+ Theory.Trans.t_of_constr goal rewinfo.morph_rlt envs
(rewinfo.pattern , rewinfo.subject)
in
- let goal, ir = AAC_theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in
+ let goal, ir = Theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in
- let units = AAC_theory.Trans.ir_to_units ir in
- let m = AAC_matcher.subterm ?strict units pattern subject in
+ let units = Theory.Trans.ir_to_units ir in
+ let m = Matcher.subterm ?strict units pattern subject in
(* We sort the monad in increasing size of contet *)
- let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in
+ let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in
if show
then
- AAC_print.print rewinfo.morph_rlt ir m (hypinfo.AAC_coq.Rewrite.context)
+ Print.print rewinfo.morph_rlt ir m (hypinfo.Coq.Rewrite.context)
else
try
let pat,subst = choose_subst occ_subterm occ_sol m in
- let tr_step = AAC_matcher.Subst.instantiate subst pat in
- let tr_step_raw = AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in
+ let tr_step = Matcher.Subst.instantiate subst pat in
+ let tr_step_raw = Theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in
- let conv = (AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.AAC_coq.Rewrite.context)) in
- let subst = AAC_matcher.Subst.to_list subst in
+ let conv = (Theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.Coq.Rewrite.context)) in
+ let subst = Matcher.Subst.to_list subst in
let subst = List.map (fun (x,y) -> x, conv y) subst in
let by_aac_reflexivity = (by_aac_reflexivity rewinfo.subject rewinfo.eqt ir) in
core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject
@@ -435,7 +435,7 @@ let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
) goal
-open Rewrite
+open Coq.Rewrite
open Tacmach
open Tacticals
open Tacexpr
@@ -446,7 +446,7 @@ open Genarg
let rec add k x = function
| [] -> [k,x]
| k',_ as ky::q ->
- if k'=k then AAC_coq.user_error ("redondant argument ("^k^")")
+ if k'=k then Coq.user_error ("redondant argument ("^k^")")
else ky::add k x q
let get k l = try Some (List.assoc k l) with Not_found -> None
diff --git a/AAC_rewrite.mli b/rewrite.mli
index d195075..d195075 100644
--- a/AAC_rewrite.mli
+++ b/rewrite.mli
diff --git a/AAC_search_monad.ml b/search_monad.ml
index 09a6455..09a6455 100644
--- a/AAC_search_monad.ml
+++ b/search_monad.ml
diff --git a/AAC_search_monad.mli b/search_monad.mli
index 7e2a910..7e2a910 100644
--- a/AAC_search_monad.mli
+++ b/search_monad.mli
diff --git a/AAC_theory.ml b/theory.ml
index 55b9e21..3fa35bf 100644
--- a/AAC_theory.ml
+++ b/theory.ml
@@ -20,7 +20,7 @@ module Control = struct
let time = false
end
-module Debug = AAC_helper.Debug (Control)
+module Debug = Helper.Debug (Control)
open Debug
(** {1 HMap : Specialized Hashtables based on constr} *)
@@ -42,54 +42,54 @@ module Stubs = struct
let path = ac_theory_path@["Internal"]
(** The constants from the inductive type *)
- let _Tty = lazy (AAC_coq.init_constant path "T")
- let vTty = lazy (AAC_coq.init_constant path "vT")
+ let _Tty = lazy (Coq.init_constant path "T")
+ let vTty = lazy (Coq.init_constant path "vT")
- let rsum = lazy (AAC_coq.init_constant path "sum")
- let rprd = lazy (AAC_coq.init_constant path "prd")
- let rsym = lazy (AAC_coq.init_constant path "sym")
- let runit = lazy (AAC_coq.init_constant path "unit")
+ let rsum = lazy (Coq.init_constant path "sum")
+ let rprd = lazy (Coq.init_constant path "prd")
+ let rsym = lazy (Coq.init_constant path "sym")
+ let runit = lazy (Coq.init_constant path "unit")
- let vnil = lazy (AAC_coq.init_constant path "vnil")
- let vcons = lazy (AAC_coq.init_constant path "vcons")
- let eval = lazy (AAC_coq.init_constant path "eval")
+ let vnil = lazy (Coq.init_constant path "vnil")
+ let vcons = lazy (Coq.init_constant path "vcons")
+ let eval = lazy (Coq.init_constant path "eval")
- let decide_thm = lazy (AAC_coq.init_constant path "decide")
- let lift_normalise_thm = lazy (AAC_coq.init_constant path "lift_normalise")
+ let decide_thm = lazy (Coq.init_constant path "decide")
+ let lift_normalise_thm = lazy (Coq.init_constant path "lift_normalise")
let lift =
- lazy (AAC_coq.init_constant ac_theory_path "AAC_lift")
+ lazy (Coq.init_constant ac_theory_path "AAC_lift")
let lift_proj_equivalence=
- lazy (AAC_coq.init_constant ac_theory_path "aac_lift_equivalence")
+ lazy (Coq.init_constant ac_theory_path "aac_lift_equivalence")
let lift_transitivity_left =
- lazy(AAC_coq.init_constant ac_theory_path "lift_transitivity_left")
+ lazy(Coq.init_constant ac_theory_path "lift_transitivity_left")
let lift_transitivity_right =
- lazy(AAC_coq.init_constant ac_theory_path "lift_transitivity_right")
+ lazy(Coq.init_constant ac_theory_path "lift_transitivity_right")
let lift_reflexivity =
- lazy(AAC_coq.init_constant ac_theory_path "lift_reflexivity")
+ lazy(Coq.init_constant ac_theory_path "lift_reflexivity")
end
module Classes = struct
module Associative = struct
let path = ac_theory_path
- let typ = lazy (AAC_coq.init_constant path "Associative")
- let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) =
- mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier;
- rlt.AAC_coq.Relation.r;
+ let typ = lazy (Coq.init_constant path "Associative")
+ let ty (rlt : Coq.Relation.t) (value : Term.constr) =
+ mkApp (Lazy.force typ, [| rlt.Coq.Relation.carrier;
+ rlt.Coq.Relation.r;
value
|] )
let infer goal rlt value =
let ty = ty rlt value in
- AAC_coq.resolve_one_typeclass goal ty
+ Coq.resolve_one_typeclass goal ty
end
module Commutative = struct
let path = ac_theory_path
- let typ = lazy (AAC_coq.init_constant path "Commutative")
- let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) =
- mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier;
- rlt.AAC_coq.Relation.r;
+ let typ = lazy (Coq.init_constant path "Commutative")
+ let ty (rlt : Coq.Relation.t) (value : Term.constr) =
+ mkApp (Lazy.force typ, [| rlt.Coq.Relation.carrier;
+ rlt.Coq.Relation.r;
value
|] )
@@ -97,30 +97,30 @@ module Classes = struct
module Proper = struct
let path = ac_theory_path @ ["Internal";"Sym"]
- let typeof = lazy (AAC_coq.init_constant path "type_of")
- let relof = lazy (AAC_coq.init_constant path "rel_of")
- let mk_typeof : AAC_coq.Relation.t -> int -> constr = fun rlt n ->
- let x = rlt.AAC_coq.Relation.carrier in
- mkApp (Lazy.force typeof, [| x ; AAC_coq.Nat.of_int n |])
- let mk_relof : AAC_coq.Relation.t -> int -> constr = fun rlt n ->
- let (x,r) = AAC_coq.Relation.split rlt in
- mkApp (Lazy.force relof, [| x;r ; AAC_coq.Nat.of_int n |])
+ let typeof = lazy (Coq.init_constant path "type_of")
+ let relof = lazy (Coq.init_constant path "rel_of")
+ let mk_typeof : Coq.Relation.t -> int -> constr = fun rlt n ->
+ let x = rlt.Coq.Relation.carrier in
+ mkApp (Lazy.force typeof, [| x ; Coq.Nat.of_int n |])
+ let mk_relof : Coq.Relation.t -> int -> constr = fun rlt n ->
+ let (x,r) = Coq.Relation.split rlt in
+ mkApp (Lazy.force relof, [| x;r ; Coq.Nat.of_int n |])
let ty rlt op ar =
let typeof = mk_typeof rlt ar in
let relof = mk_relof rlt ar in
- AAC_coq.Classes.mk_morphism typeof relof op
+ Coq.Classes.mk_morphism typeof relof op
let infer goal rlt op ar =
let ty = ty rlt op ar in
- AAC_coq.resolve_one_typeclass goal ty
+ Coq.resolve_one_typeclass goal ty
end
module Unit = struct
let path = ac_theory_path
- let typ = lazy (AAC_coq.init_constant path "Unit")
- let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) (unit : Term.constr)=
- mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier;
- rlt.AAC_coq.Relation.r;
+ let typ = lazy (Coq.init_constant path "Unit")
+ let ty (rlt : Coq.Relation.t) (value : Term.constr) (unit : Term.constr)=
+ mkApp (Lazy.force typ, [| rlt.Coq.Relation.carrier;
+ rlt.Coq.Relation.r;
value;
unit
|] )
@@ -131,9 +131,9 @@ end
(* Non empty lists *)
module NEList = struct
let path = ac_theory_path @ ["Internal"]
- let typ = lazy (AAC_coq.init_constant path "list")
- let nil = lazy (AAC_coq.init_constant path "nil")
- let cons = lazy (AAC_coq.init_constant path "cons")
+ let typ = lazy (Coq.init_constant path "list")
+ let nil = lazy (Coq.init_constant path "nil")
+ let cons = lazy (Coq.init_constant path "cons")
let cons ty h t =
mkApp (Lazy.force cons, [| ty; h ; t |])
let nil ty x =
@@ -149,11 +149,11 @@ end
(** a [mset] is a ('a * pos) list *)
let mk_mset ty (l : (constr * int) list) =
- let pos = Lazy.force AAC_coq.Pos.typ in
+ let pos = Lazy.force Coq.Pos.typ in
let pair (x : constr) (ar : int) =
- AAC_coq.Pair.of_pair ty pos (x, AAC_coq.Pos.of_int ar)
+ Coq.Pair.of_pair ty pos (x, Coq.Pos.of_int ar)
in
- let pair_ty = AAC_coq.lapp AAC_coq.Pair.typ [| ty ; pos|] in
+ let pair_ty = Coq.lapp Coq.Pair.typ [| ty ; pos|] in
let rec aux = function
| [ ] -> assert false
| [x,ar] -> NEList.nil pair_ty (pair x ar)
@@ -162,10 +162,10 @@ let mk_mset ty (l : (constr * int) list) =
aux l
module Sigma = struct
- let sigma = lazy (AAC_coq.init_constant ac_theory_path "sigma")
- let sigma_empty = lazy (AAC_coq.init_constant ac_theory_path "sigma_empty")
- let sigma_add = lazy (AAC_coq.init_constant ac_theory_path "sigma_add")
- let sigma_get = lazy (AAC_coq.init_constant ac_theory_path "sigma_get")
+ let sigma = lazy (Coq.init_constant ac_theory_path "sigma")
+ let sigma_empty = lazy (Coq.init_constant ac_theory_path "sigma_empty")
+ let sigma_add = lazy (Coq.init_constant ac_theory_path "sigma_add")
+ let sigma_get = lazy (Coq.init_constant ac_theory_path "sigma_get")
let add ty n x map =
mkApp (Lazy.force sigma_add,[|ty; n; x ; map|])
@@ -184,7 +184,7 @@ module Sigma = struct
List.fold_left
(fun acc (i,t) ->
assert (i > 0);
- add ty (AAC_coq.Pos.of_int i) ( t) acc)
+ add ty (Coq.Pos.of_int i) ( t) acc)
(empty ty)
q
in to_fun ty (t) map
@@ -197,20 +197,20 @@ end
module Sym = struct
type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr}
let path = ac_theory_path @ ["Internal";"Sym"]
- let typ = lazy (AAC_coq.init_constant path "pack")
- let mkPack = lazy (AAC_coq.init_constant path "mkPack")
- let value = lazy (AAC_coq.init_constant path "value")
- let null = lazy (AAC_coq.init_constant path "null")
- let mk_pack (rlt: AAC_coq.Relation.t) s =
- let (x,r) = AAC_coq.Relation.split rlt in
+ let typ = lazy (Coq.init_constant path "pack")
+ let mkPack = lazy (Coq.init_constant path "mkPack")
+ let value = lazy (Coq.init_constant path "value")
+ let null = lazy (Coq.init_constant path "null")
+ let mk_pack (rlt: Coq.Relation.t) s =
+ let (x,r) = Coq.Relation.split rlt in
mkApp (Lazy.force mkPack, [|x;r; s.ar;s.value;s.morph|])
let null rlt =
- let x = rlt.AAC_coq.Relation.carrier in
- let r = rlt.AAC_coq.Relation.r in
+ let x = rlt.Coq.Relation.carrier in
+ let r = rlt.Coq.Relation.r in
mkApp (Lazy.force null, [| x;r;|])
- let mk_ty : AAC_coq.Relation.t -> constr = fun rlt ->
- let (x,r) = AAC_coq.Relation.split rlt in
+ let mk_ty : Coq.Relation.t -> constr = fun rlt ->
+ let (x,r) = Coq.Relation.split rlt in
mkApp (Lazy.force typ, [| x; r|] )
end
@@ -222,29 +222,29 @@ module Bin =struct
}
let path = ac_theory_path @ ["Internal";"Bin"]
- let typ = lazy (AAC_coq.init_constant path "pack")
- let mkPack = lazy (AAC_coq.init_constant path "mk_pack")
+ let typ = lazy (Coq.init_constant path "pack")
+ let mkPack = lazy (Coq.init_constant path "mk_pack")
- let mk_pack: AAC_coq.Relation.t -> pack -> Term.constr = fun (rlt) s ->
- let (x,r) = AAC_coq.Relation.split rlt in
+ let mk_pack: Coq.Relation.t -> pack -> Term.constr = fun (rlt) s ->
+ let (x,r) = Coq.Relation.split rlt in
let comm_ty = Classes.Commutative.ty rlt s.value in
mkApp (Lazy.force mkPack , [| x ; r;
s.value;
s.compat ;
s.assoc;
- AAC_coq.Option.of_option comm_ty s.comm
+ Coq.Option.of_option comm_ty s.comm
|])
- let mk_ty : AAC_coq.Relation.t -> constr = fun rlt ->
- let (x,r) = AAC_coq.Relation.split rlt in
+ let mk_ty : Coq.Relation.t -> constr = fun rlt ->
+ let (x,r) = Coq.Relation.split rlt in
mkApp (Lazy.force typ, [| x; r|] )
end
module Unit = struct
let path = ac_theory_path @ ["Internal"]
- let unit_of_ty = lazy (AAC_coq.init_constant path "unit_of")
- let unit_pack_ty = lazy (AAC_coq.init_constant path "unit_pack")
- let mk_unit_of = lazy (AAC_coq.init_constant path "mk_unit_for")
- let mk_unit_pack = lazy (AAC_coq.init_constant path "mk_unit_pack")
+ let unit_of_ty = lazy (Coq.init_constant path "unit_of")
+ let unit_pack_ty = lazy (Coq.init_constant path "unit_pack")
+ let mk_unit_of = lazy (Coq.init_constant path "mk_unit_for")
+ let mk_unit_pack = lazy (Coq.init_constant path "mk_unit_pack")
type unit_of =
{
@@ -259,15 +259,15 @@ module Unit = struct
}
let ty_unit_of rlt e_bin u =
- let (x,r) = AAC_coq.Relation.split rlt in
+ let (x,r) = Coq.Relation.split rlt in
mkApp ( Lazy.force unit_of_ty, [| x; r; e_bin; u |])
let ty_unit_pack rlt e_bin =
- let (x,r) = AAC_coq.Relation.split rlt in
+ let (x,r) = Coq.Relation.split rlt in
mkApp (Lazy.force unit_pack_ty, [| x; r; e_bin |])
let mk_unit_of rlt e_bin u unit_of =
- let (x,r) = AAC_coq.Relation.split rlt in
+ let (x,r) = Coq.Relation.split rlt in
mkApp (Lazy.force mk_unit_of , [| x;
r;
e_bin ;
@@ -277,10 +277,10 @@ module Unit = struct
|])
let mk_pack rlt e_bin pack : Term.constr =
- let (x,r) = AAC_coq.Relation.split rlt in
+ let (x,r) = Coq.Relation.split rlt in
let ty = ty_unit_of rlt e_bin pack.u_value in
let mk_unit_of = mk_unit_of rlt e_bin pack.u_value in
- let u_desc =AAC_coq.List.of_list ( ty ) (List.map mk_unit_of pack.u_desc) in
+ let u_desc =Coq.List.of_list ( ty ) (List.map mk_unit_of pack.u_desc) in
mkApp (Lazy.force mk_unit_pack, [|x;r;
e_bin ;
pack.u_value;
@@ -386,7 +386,7 @@ module Trans = struct
units. Otherwise, we do not have the ability to rewrite [0 = a +
a] in [a = ...]*)
module Gather : sig
- val gather : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_coq.goal_sigma
+ val gather : Coq.goal_sigma -> Coq.Relation.t -> envs -> Term.constr -> Coq.goal_sigma
end
= struct
@@ -404,37 +404,37 @@ module Trans = struct
end
- let get_unit (rlt : AAC_coq.Relation.t) op goal :
- (AAC_coq.goal_sigma * constr * constr ) option=
- let x = (rlt.AAC_coq.Relation.carrier) in
- let unit, goal = AAC_coq.evar_unit goal x in
+ let get_unit (rlt : Coq.Relation.t) op goal :
+ (Coq.goal_sigma * constr * constr ) option=
+ let x = (rlt.Coq.Relation.carrier) in
+ let unit, goal = Coq.evar_unit goal x in
let ty =Classes.Unit.ty rlt op unit in
let result =
try
- let t,goal = AAC_coq.resolve_one_typeclass goal ty in
+ let t,goal = Coq.resolve_one_typeclass goal ty in
Some (goal,t,unit)
with Not_found -> None
in
match result with
| None -> None
| Some (goal,s,unit) ->
- let unit = AAC_coq.nf_evar goal unit in
+ let unit = Coq.nf_evar goal unit in
Some (goal, unit, s)
(** gives back the class and the operator *)
- let is_bin (rlt: AAC_coq.Relation.t) (op: constr) ( goal: AAC_coq.goal_sigma)
- : (AAC_coq.goal_sigma * Bin.pack) option =
+ let is_bin (rlt: Coq.Relation.t) (op: constr) ( goal: Coq.goal_sigma)
+ : (Coq.goal_sigma * Bin.pack) option =
let assoc_ty = Classes.Associative.ty rlt op in
let comm_ty = Classes.Commutative.ty rlt op in
let proper_ty = Classes.Proper.ty rlt op 2 in
try
- let proper , goal = AAC_coq.resolve_one_typeclass goal proper_ty in
- let assoc, goal = AAC_coq.resolve_one_typeclass goal assoc_ty in
+ let proper , goal = Coq.resolve_one_typeclass goal proper_ty in
+ let assoc, goal = Coq.resolve_one_typeclass goal assoc_ty in
let comm , goal =
try
- let comm, goal = AAC_coq.resolve_one_typeclass goal comm_ty in
+ let comm, goal = Coq.resolve_one_typeclass goal comm_ty in
Some comm, goal
with Not_found ->
None, goal
@@ -448,7 +448,7 @@ module Trans = struct
Some (goal,bin)
with |Not_found -> None
- let is_bin (rlt : AAC_coq.Relation.t) (op : constr) (goal : AAC_coq.goal_sigma)=
+ let is_bin (rlt : Coq.Relation.t) (op : constr) (goal : Coq.goal_sigma)=
match is_bin rlt op goal with
| None -> None
| Some (goal, bin_pack) ->
@@ -469,13 +469,13 @@ module Trans = struct
(** {is_morphism} try to infer the kind of operator we are
dealing with *)
- let is_morphism goal (rlt : AAC_coq.Relation.t) (papp : Term.constr) (ar : int) : (AAC_coq.goal_sigma * pack ) option =
+ let is_morphism goal (rlt : Coq.Relation.t) (papp : Term.constr) (ar : int) : (Coq.goal_sigma * pack ) option =
let typeof = Classes.Proper.mk_typeof rlt ar in
let relof = Classes.Proper.mk_relof rlt ar in
- let m = AAC_coq.Classes.mk_morphism typeof relof papp in
+ let m = Coq.Classes.mk_morphism typeof relof papp in
try
- let m,goal = AAC_coq.resolve_one_typeclass goal m in
- let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in
+ let m,goal = Coq.resolve_one_typeclass goal m in
+ let pack = {Sym.ar = (Coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in
Some (goal, Sym pack)
with
| Not_found -> None
@@ -493,7 +493,7 @@ module Trans = struct
let args = Array.sub ca (n-2) 2 in
Some (papp, args )
- let fold goal (rlt : AAC_coq.Relation.t) envs t ca cont =
+ let fold goal (rlt : Coq.Relation.t) envs t ca cont =
let fold_morphism t ca =
let nb_params = Array.length ca in
let rec aux n =
@@ -526,9 +526,9 @@ module Trans = struct
(* update in place the envs of known stuff, using memoization. We
have to memoize failures, here. *)
- let gather goal (rlt : AAC_coq.Relation.t ) envs t : AAC_coq.goal_sigma =
+ let gather goal (rlt : Coq.Relation.t ) envs t : Coq.goal_sigma =
let rec aux goal x =
- match AAC_coq.decomp_term x with
+ match Coq.decomp_term x with
| App (t,ca) ->
fold goal rlt envs t ca (aux )
| _ -> goal
@@ -541,7 +541,7 @@ module Trans = struct
constants). *)
module Parse :
sig
- val t_of_constr : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> constr -> AAC_matcher.Terms.t * AAC_coq.goal_sigma
+ val t_of_constr : Coq.goal_sigma -> Coq.Relation.t -> envs -> constr -> Matcher.Terms.t * Coq.goal_sigma
end
= struct
@@ -562,21 +562,21 @@ module Trans = struct
This functions is prevented to go through [ar < 0] by the fact
that a constant is a morphism. But not an eva. *)
- let is_morphism goal (rlt : AAC_coq.Relation.t) (papp : Term.constr) (ar : int) : (AAC_coq.goal_sigma * pack ) option =
+ let is_morphism goal (rlt : Coq.Relation.t) (papp : Term.constr) (ar : int) : (Coq.goal_sigma * pack ) option =
let typeof = Classes.Proper.mk_typeof rlt ar in
let relof = Classes.Proper.mk_relof rlt ar in
- let m = AAC_coq.Classes.mk_morphism typeof relof papp in
+ let m = Coq.Classes.mk_morphism typeof relof papp in
try
- let m,goal = AAC_coq.resolve_one_typeclass goal m in
- let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in
+ let m,goal = Coq.resolve_one_typeclass goal m in
+ let pack = {Sym.ar = (Coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in
Some (goal, Sym pack)
with
| e -> None
exception NotReflexive
- let discriminate goal envs (rlt : AAC_coq.Relation.t) t ca : AAC_coq.goal_sigma * pack * constr * constr array =
+ let discriminate goal envs (rlt : Coq.Relation.t) t ca : Coq.goal_sigma * pack * constr * constr array =
let nb_params = Array.length ca in
- let rec fold goal ar :AAC_coq.goal_sigma * pack * constr * constr array =
+ let rec fold goal ar :Coq.goal_sigma * pack * constr * constr array =
begin
assert (0 <= ar && ar <= nb_params);
let p_app = mkApp (t, Array.sub ca 0 (nb_params - ar)) in
@@ -618,7 +618,7 @@ module Trans = struct
let discriminate goal envs rlt x =
try
- match AAC_coq.decomp_term x with
+ match Coq.decomp_term x with
| App (t,ca) ->
discriminate goal envs rlt t ca
| _ -> discriminate goal envs rlt x [| |]
@@ -633,11 +633,11 @@ module Trans = struct
of the term [cstr]. Doing so, it modifies the environment of
known stuff [envs], and eventually creates fresh
evars. Therefore, we give back the goal updated accordingly *)
- let t_of_constr goal (rlt: AAC_coq.Relation.t ) envs : constr -> AAC_matcher.Terms.t * AAC_coq.goal_sigma =
+ let t_of_constr goal (rlt: Coq.Relation.t ) envs : constr -> Matcher.Terms.t * Coq.goal_sigma =
let r_goal = ref (goal) in
let rec aux x =
- match AAC_coq.decomp_term x with
- | Rel i -> AAC_matcher.Terms.Var i
+ match Coq.decomp_term x with
+ | Rel i -> Matcher.Terms.Var i
| _ ->
let goal, pack , p_app, ca = discriminate (!r_goal) envs rlt x in
r_goal := goal;
@@ -648,16 +648,16 @@ module Trans = struct
begin match pack.Bin.comm with
| Some _ ->
assert (Array.length ca = 2);
- AAC_matcher.Terms.Plus ( k, aux ca.(0), aux ca.(1))
+ Matcher.Terms.Plus ( k, aux ca.(0), aux ca.(1))
| None ->
assert (Array.length ca = 2);
- AAC_matcher.Terms.Dot ( k, aux ca.(0), aux ca.(1))
+ Matcher.Terms.Dot ( k, aux ca.(0), aux ca.(1))
end
| Unit _ ->
assert (Array.length ca = 0);
- AAC_matcher.Terms.Unit ( k)
+ Matcher.Terms.Unit ( k)
| Sym _ ->
- AAC_matcher.Terms.Sym ( k, Array.map aux ca)
+ Matcher.Terms.Sym ( k, Array.map aux ca)
in
(
fun x -> let r = aux x in r, !r_goal
@@ -689,12 +689,12 @@ module Trans = struct
bin : (int * Bin.pack) list ;
units : (int * Unit.pack) list;
sym : (int * Term.constr) list ;
- matcher_units : AAC_matcher.ext_units
+ matcher_units : Matcher.ext_units
}
let ir_to_units ir = ir.matcher_units
- let ir_of_envs goal (rlt : AAC_coq.Relation.t) envs =
+ let ir_of_envs goal (rlt : Coq.Relation.t) envs =
let add x y l = (x,y)::l in
let nil = [] in
let sym ,
@@ -729,7 +729,7 @@ module Trans = struct
)
([],[]) bin
in
- {AAC_matcher.unit_for = unit_for; AAC_matcher.is_ac = is_ac}
+ {Matcher.unit_for = unit_for; Matcher.is_ac = is_ac}
in
let units : (int * Unit.pack) list =
@@ -745,7 +745,7 @@ module Trans = struct
if unit_of.Unit.uf_u = u
then
{unit_of with
- Unit.uf_idx = (AAC_coq.Pos.of_int nop)} :: acc
+ Unit.uf_idx = (Coq.Pos.of_int nop)} :: acc
else
acc
)
@@ -779,7 +779,7 @@ module Trans = struct
(** [raw_constr_of_t_debruijn] rebuilds a term in the raw
representation, without products on top, and maybe escaping free
debruijn indices (in the case of a pattern for example). *)
- let raw_constr_of_t_debruijn ir (t : AAC_matcher.Terms.t) : Term.constr * int list =
+ let raw_constr_of_t_debruijn ir (t : Matcher.Terms.t) : Term.constr * int list =
let add_set,get =
let r = ref [] in
let rec add x = function
@@ -794,31 +794,31 @@ module Trans = struct
find the wrong kind of pack in the maps *)
let rec aux t =
match t with
- | AAC_matcher.Terms.Plus (s,l,r) ->
+ | Matcher.Terms.Plus (s,l,r) ->
begin match Hashtbl.find ir.packer s with
| Bin (s,_) ->
mkApp (s.Bin.value , [|(aux l);(aux r)|])
| _ -> Printf.printf "erreur:%i\n%!"s;
assert false
end
- | AAC_matcher.Terms.Dot (s,l,r) ->
+ | Matcher.Terms.Dot (s,l,r) ->
begin match Hashtbl.find ir.packer s with
| Bin (s,_) ->
mkApp (s.Bin.value, [|(aux l);(aux r)|])
| _ -> assert false
end
- | AAC_matcher.Terms.Sym (s,t) ->
+ | Matcher.Terms.Sym (s,t) ->
begin match Hashtbl.find ir.packer s with
| Sym s ->
mkApp (s.Sym.value, Array.map aux t)
| _ -> assert false
end
- | AAC_matcher.Terms.Unit x ->
+ | Matcher.Terms.Unit x ->
begin match Hashtbl.find ir.packer x with
| Unit s -> s
| _ -> assert false
end
- | AAC_matcher.Terms.Var i -> add_set i;
+ | Matcher.Terms.Var i -> add_set i;
mkRel (i)
in
let t = aux t in
@@ -873,15 +873,15 @@ module Trans = struct
(* Note : this function can fail if the user is using the wrong
relation, like proving a = b, while the classes are defined with
another relation (==) *)
- let build_reif_params goal (rlt : AAC_coq.Relation.t) (zero) :
- reif_params * AAC_coq.goal_sigma =
- let carrier = rlt.AAC_coq.Relation.carrier in
+ let build_reif_params goal (rlt : Coq.Relation.t) (zero) :
+ reif_params * Coq.goal_sigma =
+ let carrier = rlt.Coq.Relation.carrier in
let bin_null =
try
- let op,goal = AAC_coq.evar_binary goal carrier in
+ let op,goal = Coq.evar_binary goal carrier in
let assoc,goal = Classes.Associative.infer goal rlt op in
let compat,goal = Classes.Proper.infer goal rlt op 2 in
- let op = AAC_coq.nf_evar goal op in
+ let op = Coq.nf_evar goal op in
{
Bin.value = op;
Bin.compat = compat;
@@ -892,11 +892,11 @@ module Trans = struct
in
let zero, goal =
try
- let evar_op,goal = AAC_coq.evar_binary goal carrier in
- let evar_unit, goal = AAC_coq.evar_unit goal carrier in
+ let evar_op,goal = Coq.evar_binary goal carrier in
+ let evar_unit, goal = Coq.evar_unit goal carrier in
let query = Classes.Unit.ty rlt evar_op evar_unit in
- let _, goal = AAC_coq.resolve_one_typeclass goal query in
- AAC_coq.nf_evar goal evar_unit, goal
+ let _, goal = Coq.resolve_one_typeclass goal query in
+ Coq.nf_evar goal evar_unit, goal
with _ -> zero, goal in
let sym_null = Sym.null rlt in
let unit_null = Unit.default zero in
@@ -932,7 +932,7 @@ module Trans = struct
(** [build_sigma_maps] given a envs and some reif_params, we are
able to build the sigmas *)
- let build_sigma_maps (rlt : AAC_coq.Relation.t) zero ir (k : sigmas * sigma_maps -> Proof_type.tactic ) : Proof_type.tactic = fun goal ->
+ let build_sigma_maps (rlt : Coq.Relation.t) zero ir (k : sigmas * sigma_maps -> Proof_type.tactic ) : Proof_type.tactic = fun goal ->
let rp,goal = build_reif_params goal rlt zero in
let renumbered_sym, to_local, to_global = renumber ir.sym in
let env_sym = Sigma.of_list
@@ -940,7 +940,7 @@ module Trans = struct
(rp.sym_null)
renumbered_sym
in
- AAC_coq.cps_mk_letin "env_sym" env_sym
+ Coq.cps_mk_letin "env_sym" env_sym
(fun env_sym ->
let bin = (List.map ( fun (n,s) -> n, Bin.mk_pack rlt s) ir.bin) in
let env_bin =
@@ -949,7 +949,7 @@ module Trans = struct
(Bin.mk_pack rlt rp.bin_null)
bin
in
- AAC_coq.cps_mk_letin "env_bin" env_bin
+ Coq.cps_mk_letin "env_bin" env_bin
(fun env_bin ->
let units = (List.map (fun (n,s) -> n, Unit.mk_pack rlt env_bin s)ir.units) in
let env_units =
@@ -959,7 +959,7 @@ module Trans = struct
units
in
- AAC_coq.cps_mk_letin "env_units" env_units
+ Coq.cps_mk_letin "env_units" env_units
(fun env_units ->
let sigmas =
{
@@ -967,7 +967,7 @@ module Trans = struct
env_bin = env_bin ;
env_units = env_units;
} in
- let f = List.map (fun (x,_) -> (x,AAC_coq.Pos.of_int x)) in
+ let f = List.map (fun (x,_) -> (x,Coq.Pos.of_int x)) in
let sigma_maps =
{
sym_to_pos = (let sym = f renumbered_sym in fun x -> (List.assoc (to_local x) sym));
@@ -1006,7 +1006,7 @@ module Trans = struct
| n -> let n = n-1 in
mkApp( vcons,
[|
- (AAC_coq.Nat.of_int n);
+ (Coq.Nat.of_int n);
v.(ar - 1 - n);
(aux (n))
|]
@@ -1014,9 +1014,9 @@ module Trans = struct
in aux ar
(* TODO: use a do notation *)
- let mk_reif_builders (rlt: AAC_coq.Relation.t) (env_sym:constr) (k: reif_builders -> Proof_type.tactic) =
- let x = (rlt.AAC_coq.Relation.carrier) in
- let r = (rlt.AAC_coq.Relation.r) in
+ let mk_reif_builders (rlt: Coq.Relation.t) (env_sym:constr) (k: reif_builders -> Proof_type.tactic) =
+ let x = (rlt.Coq.Relation.carrier) in
+ let r = (rlt.Coq.Relation.r) in
let x_r_env = [|x;r;env_sym|] in
let tty = mkApp (Lazy.force Stubs._Tty, x_r_env) in
@@ -1025,17 +1025,17 @@ module Trans = struct
let rsym = mkApp (Lazy.force Stubs.rsym, x_r_env) in
let vnil = mkApp (Lazy.force Stubs.vnil, x_r_env) in
let vcons = mkApp (Lazy.force Stubs.vcons, x_r_env) in
- AAC_coq.cps_mk_letin "tty" tty
+ Coq.cps_mk_letin "tty" tty
(fun tty ->
- AAC_coq.cps_mk_letin "rsum" rsum
+ Coq.cps_mk_letin "rsum" rsum
(fun rsum ->
- AAC_coq.cps_mk_letin "rprd" rprd
+ Coq.cps_mk_letin "rprd" rprd
(fun rprd ->
- AAC_coq.cps_mk_letin "rsym" rsym
+ Coq.cps_mk_letin "rsym" rsym
(fun rsym ->
- AAC_coq.cps_mk_letin "vnil" vnil
+ Coq.cps_mk_letin "vnil" vnil
(fun vnil ->
- AAC_coq.cps_mk_letin "vcons" vcons
+ Coq.cps_mk_letin "vcons" vcons
(fun vcons ->
let r ={
rsum =
@@ -1074,21 +1074,21 @@ module Trans = struct
(** [reif_constr_of_t reifier t] rebuilds the term [t] in the
reified form. We use the [reifier] to minimise the size of the
terms (we make as much lets as possible)*)
- let reif_constr_of_t (sm,rb) (t:AAC_matcher.Terms.t) : constr =
+ let reif_constr_of_t (sm,rb) (t:Matcher.Terms.t) : constr =
let rec aux = function
- | AAC_matcher.Terms.Plus (s,l,r) ->
+ | Matcher.Terms.Plus (s,l,r) ->
let idx = sm.bin_to_pos s in
rb.rsum idx (aux l) (aux r)
- | AAC_matcher.Terms.Dot (s,l,r) ->
+ | Matcher.Terms.Dot (s,l,r) ->
let idx = sm.bin_to_pos s in
rb.rprd idx (aux l) (aux r)
- | AAC_matcher.Terms.Sym (s,t) ->
+ | Matcher.Terms.Sym (s,t) ->
let idx = sm.sym_to_pos s in
rb.rsym idx (Array.map aux t)
- | AAC_matcher.Terms.Unit s ->
+ | Matcher.Terms.Unit s ->
let idx = sm.units_to_pos s in
rb.runit idx
- | AAC_matcher.Terms.Var i ->
+ | Matcher.Terms.Var i ->
anomaly "call to reif_constr_of_t on a term with variables."
in aux t
end
diff --git a/AAC_theory.mli b/theory.mli
index 2f57446..cc9a617 100644
--- a/AAC_theory.mli
+++ b/theory.mli
@@ -21,7 +21,7 @@
*)
(** Both in OCaml and Coq, we represent finite multisets using
- weighted lists ([('a*int) list]), see {!AAC_matcher.mset}.
+ weighted lists ([('a*int) list]), see {!Matcher.mset}.
[mk_mset ty l] constructs a Coq multiset from an OCaml multiset
[l] of Coq terms of type [ty] *)
@@ -57,16 +57,16 @@ sig
(** [mk_pack rlt (ar,value,morph)] *)
- val mk_pack: AAC_coq.Relation.t -> pack -> Term.constr
+ val mk_pack: Coq.Relation.t -> pack -> Term.constr
- (** [null] builds a dummy (identity) symbol, given an {!AAC_coq.Relation.t} *)
- val null: AAC_coq.Relation.t -> Term.constr
+ (** [null] builds a dummy (identity) symbol, given an {!Coq.Relation.t} *)
+ val null: Coq.Relation.t -> Term.constr
end
(** We need to export some Coq stubs out of this module. They are used
- by the main tactic, see {!AAC_rewrite} *)
+ by the main tactic, see {!Rewrite} *)
module Stubs : sig
val lift : Term.constr Lazy.t
val lift_proj_equivalence : Term.constr Lazy.t
@@ -96,7 +96,7 @@ module Trans : sig
(** This module provides facilities to interpret a term with
arbitrary operators as an instance of an abstract syntax tree
- {!AAC_matcher.Terms.t}.
+ {!Matcher.Terms.t}.
For each Coq application [f x_1 ... x_n], this amounts to
deciding whether one of the partial applications [f x_1
@@ -125,7 +125,7 @@ module Trans : sig
val empty_envs : unit -> envs
- (** {2 Reification: from Coq terms to AST {!AAC_matcher.Terms.t} } *)
+ (** {2 Reification: from Coq terms to AST {!Matcher.Terms.t} } *)
(** [t_of_constr goal rlt envs (left,right)] builds the abstract
@@ -136,11 +136,11 @@ module Trans : sig
evars; this is why we give back the [goal], accordingly
updated. *)
- val t_of_constr : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> (Term.constr * Term.constr) -> AAC_matcher.Terms.t * AAC_matcher.Terms.t * AAC_coq.goal_sigma
+ val t_of_constr : Coq.goal_sigma -> Coq.Relation.t -> envs -> (Term.constr * Term.constr) -> Matcher.Terms.t * Matcher.Terms.t * Coq.goal_sigma
(** [add_symbol] adds a given binary symbol to the environment of
known stuff. *)
- val add_symbol : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_coq.goal_sigma
+ val add_symbol : Coq.goal_sigma -> Coq.Relation.t -> envs -> Term.constr -> Coq.goal_sigma
(** {2 Reconstruction: from AST back to Coq terms }
@@ -151,8 +151,8 @@ module Trans : sig
the reflexive decision procedure. *)
type ir
- val ir_of_envs : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> AAC_coq.goal_sigma * ir
- val ir_to_units : ir -> AAC_matcher.ext_units
+ val ir_of_envs : Coq.goal_sigma -> Coq.Relation.t -> envs -> Coq.goal_sigma * ir
+ val ir_to_units : ir -> Matcher.ext_units
(** {2 Building raw, natural, terms} *)
@@ -160,7 +160,7 @@ module Trans : sig
reconstruct the named products on top of it. In particular, this
allow us to print the context put around the left (or right)
hand side of a pattern. *)
- val raw_constr_of_t : ir -> AAC_coq.Relation.t -> (Term.rel_context) ->AAC_matcher.Terms.t -> Term.constr
+ val raw_constr_of_t : ir -> Coq.Relation.t -> (Term.rel_context) ->Matcher.Terms.t -> Term.constr
(** {2 Building reified terms} *)
@@ -188,10 +188,10 @@ module Trans : sig
reify each term successively.*)
type reifier
- val mk_reifier : AAC_coq.Relation.t -> Term.constr -> ir -> (sigmas * reifier -> Proof_type.tactic) -> Proof_type.tactic
+ val mk_reifier : Coq.Relation.t -> Term.constr -> ir -> (sigmas * reifier -> Proof_type.tactic) -> Proof_type.tactic
(** [reif_constr_of_t reifier t] rebuilds the term [t] in the
reified form. *)
- val reif_constr_of_t : reifier -> AAC_matcher.Terms.t -> Term.constr
+ val reif_constr_of_t : reifier -> Matcher.Terms.t -> Term.constr
end