diff options
-rw-r--r-- | AAC.v | 4 | ||||
-rw-r--r-- | CHANGELOG | 5 | ||||
-rw-r--r-- | Caveats.v | 2 | ||||
-rw-r--r-- | Instances.v | 22 | ||||
-rw-r--r-- | Makefile | 326 | ||||
-rw-r--r-- | README.txt | 7 | ||||
-rw-r--r-- | Tutorial.v | 2 | ||||
-rw-r--r-- | aac.mlpack | 7 | ||||
-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.txt | 5 | ||||
-rwxr-xr-x | make_makefile | 62 | ||||
-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
@@ -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". @@ -1,3 +1,8 @@ + +AAC_tactics 0.3 : +----------------- +- New release for Coq 8.4 + AAC_tactics 0.2-pl2 : ----------------- @@ -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. @@ -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 @@ -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 -------- @@ -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 @@ -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_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 @@ -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 |