Commit 6181688e authored by MARCHE Claude's avatar MARCHE Claude Committed by Clément Fumex

itp: syntax for maps

parent 03260ff1
......@@ -22,4 +22,13 @@ theory int.Int
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
end
\ No newline at end of file
end
theory map.Map
syntax function get "%1[%2]"
syntax function ([]) "%1[%2]"
syntax function set "{%1 with [%2] = %3}"
syntax function ([<-]) "{%1 with [%2] = %3}"
end
......@@ -35,7 +35,7 @@ ML=$(patsubst %,%.ml,$(MLALL))
CMX=$(patsubst %,%.cmx,$(MLALL))
OCAMLC=ocamlopt.opt
INCLUDES=-I $(BD) $(INCLUDEALL) -I ../../../plugins/tptp
LIBS=unix.cmxa nums.cmxa $(BIGINTLIB).cmxa dynlink.cmxa str.cmxa menhirLib.cmx zip.cmxa why3.cmxa why3extract.cmxa tptp_ast.cmx tptp_typing.cmx tptp_parser.cmx tptp_lexer.cmx
LIBS=unix.cmxa $(BIGINTLIB).cmxa dynlink.cmxa str.cmxa menhirLib.cmx zip.cmxa why3.cmxa why3extract.cmxa tptp_ast.cmx tptp_typing.cmx tptp_parser.cmx tptp_lexer.cmx
LIBSOLD=$(BD)/why3__BuiltIn.cmx $(BD)/int__Int.cmx $(BD)/array__Array.cmx
WHY3FLAGS=-L . --debug ignore_unused_vars
MLFLAGS=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment