diff --git a/Makefile.in b/Makefile.in
index a91f8cd88312f86b41a763f6e8e892faa809130b..002776e3ec68dc5e029e6477b682618ecbd5fcee 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1663,6 +1663,7 @@ TRYWHY3_FULL_PACK = \
alt-ergo-worker.js \
ace-builds/src-min-noconflict/ace.js \
ace-builds/src-min-noconflict/mode-why3.js \
+ ace-builds/src-min-noconflict/mode-coma.js \
ace-builds/src-min-noconflict/mode-python.js \
ace-builds/src-min-noconflict/mode-c_cpp.js \
ace-builds/src-min-noconflict/theme-chrome.js
@@ -1688,7 +1689,7 @@ src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/trywhy3.con
`find stdlib -name "*.mlw" -exec printf " --file=%s:/%s" {} {} ";"` \
+dynlink.js +toplevel.js $<
-src/trywhy3/why3_worker.byte: $(WHY3CMA) $(PYTHONCMO) $(MICROCCMO) \
+src/trywhy3/why3_worker.byte: $(WHY3CMA) $(PYTHONCMO) $(MICROCCMO) $(COMACMO) \
$(addprefix src/trywhy3/, bindings.cmo worker_proto.cmo why3_worker.cmo)
$(OCAMLFIND) ocamlc $(filter-out -thread,$(BFLAGS)) -package js_of_ocaml -o $@ -linkpkg $^
diff --git a/src/trywhy3/mode-coma.js b/src/trywhy3/mode-coma.js
new file mode 100644
index 0000000000000000000000000000000000000000..d0012b46363fbd7a1f17c48b4c4766661610632e
--- /dev/null
+++ b/src/trywhy3/mode-coma.js
@@ -0,0 +1,240 @@
+ace.define("ace/mode/coma_highlight_rules",["require","exports","module","ace/lib/oop","ace/mode/text_highlight_rules"], function(require, exports, module) {
+"use strict";
+
+var oop = require("../lib/oop");
+var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
+
+var ComaHighlightRules = function() {
+
+ // keep synchronized with src/parser/lexer.mll
+ var keywords = (
+ "abstract|absurd|alias|any|as|assert|assume|at|axiom|" +
+ "begin|break|by|check|clone|coinductive|constant|continue|" +
+ "diverges|do|done|downto|" +
+ "else|end|ensures|epsilon|exception|exists|export|" +
+ "false|float|for|forall|fun|function|ghost|goal|" +
+ "if|import|in|inductive|invariant|label|lemma|let|" +
+ "match|meta|module|mutable|not|old|" +
+ "partial|predicate|private|pure|" +
+ "raise|raises|range|reads|rec|ref|requires|return|returns|" +
+ "scope|so|then|theory|to|true|try|type|use|val|variant|" +
+ "while|with|writes"
+ );
+
+ var builtinConstants = ("true|false");
+
+ var builtinFunctions = ("");
+
+ var keywordMapper = this.createKeywordMapper({
+ "variable.language": "this",
+ "keyword": keywords,
+ "constant.language": builtinConstants,
+ "support.function": builtinFunctions
+ }, "identifier");
+
+ var decimalInteger = "(?:(?:[1-9]\\d*)|(?:0))";
+ var octInteger = "(?:0[oO]?[0-7]+)";
+ var hexInteger = "(?:0[xX][\\dA-Fa-f]+)";
+ var binInteger = "(?:0[bB][01]+)";
+ var integer = "(?:" + decimalInteger + "|" + octInteger + "|" + hexInteger + "|" + binInteger + ")";
+
+ var exponent = "(?:[eE][+-]?\\d+)";
+ var fraction = "(?:\\.\\d+)";
+ var intPart = "(?:\\d+)";
+ var pointFloat = "(?:(?:" + intPart + "?" + fraction + ")|(?:" + intPart + "\\.))";
+ var exponentFloat = "(?:(?:" + pointFloat + "|" + intPart + ")" + exponent + ")";
+ var floatNumber = "(?:" + exponentFloat + "|" + pointFloat + ")";
+
+ this.$rules = {
+ "start" : [
+ { token : [ "paren.lparen", "text", "paren.rparen" ],
+ regex : "([(])([*])([)])"
+ },
+ { //black magic from Rust mode to handle nested comments.
+ token : "comment.start",
+ regex : "\\(\\*",
+ stateName : "comment",
+ push : [
+ {
+ token: 'comment.start',
+ regex : "\\(\\*",
+ push : 'comment'
+ },
+ {
+ token: 'comment.end',
+ regex: "\\*\\)",
+ next: 'pop'
+ },
+ {
+ defaultToken: 'comment'
+ }
+ ]
+ },
+ {
+ token : "string", // single line
+ regex : '["](?:(?:\\\\.)|(?:[^"\\\\]))*?["]'
+ },
+ {
+ token : "string", // single char
+ regex : "'.'"
+ },
+ {
+ token : "string", // " string
+ regex : '"',
+ next : "qstring"
+ },
+ {
+ token : "constant.numeric", // float
+ regex : floatNumber
+ },
+ {
+ token : "constant.numeric", // integer
+ regex : integer + "\\b"
+ },
+ {
+ token : keywordMapper,
+ regex : "[a-zA-Z_$][a-zA-Z0-9_$]*\\b"
+ },
+ {
+ token : "keyword.operator",
+ regex : "&&|\\|\\||/\\\\|\\\\/|->|<->"
+ },
+ {
+ token : "paren.lparen",
+ regex : "[[({]"
+ },
+ {
+ token : "paren.rparen",
+ regex : "[\\])}]"
+ },
+ {
+ token : "text",
+ regex : "\\s+"
+ }
+ ],
+ "qstring" : [
+ {
+ token : "string",
+ regex : '"',
+ next : "start"
+ }, {
+ token : "string",
+ regex : '[^"]'
+ }
+ ]
+ };
+
+ this.normalizeRules();
+};
+
+oop.inherits(ComaHighlightRules, TextHighlightRules);
+
+exports.ComaHighlightRules = ComaHighlightRules;
+});
+
+ace.define("ace/mode/matching_brace_outdent",["require","exports","module","ace/range"], function(require, exports, module) {
+"use strict";
+
+var Range = require("../range").Range;
+
+var MatchingBraceOutdent = function() {};
+
+(function() {
+
+ this.checkOutdent = function(line, input) {
+ if (! /^\s+$/.test(line))
+ return false;
+
+ return /^\s*\}/.test(input);
+ };
+
+ this.autoOutdent = function(doc, row) {
+ var line = doc.getLine(row);
+ var match = line.match(/^(\s*\})/);
+
+ if (!match) return 0;
+
+ var column = match[1].length;
+ var openBracePos = doc.findMatchingBracket({row: row, column: column});
+
+ if (!openBracePos || openBracePos.row == row) return 0;
+
+ var indent = this.$getIndent(doc.getLine(openBracePos.row));
+ doc.replace(new Range(row, 0, row, column-1), indent);
+ };
+
+ this.$getIndent = function(line) {
+ return line.match(/^\s*/)[0];
+ };
+
+}).call(MatchingBraceOutdent.prototype);
+
+exports.MatchingBraceOutdent = MatchingBraceOutdent;
+});
+
+ace.define("ace/mode/coma",["require","exports","module","ace/lib/oop","ace/mode/text","ace/mode/coma_highlight_rules","ace/mode/matching_brace_outdent","ace/range"], function(require, exports, module) {
+"use strict";
+
+var oop = require("../lib/oop");
+var TextMode = require("./text").Mode;
+var ComaHighlightRules = require("./coma_highlight_rules").ComaHighlightRules;
+var MatchingBraceOutdent = require("./matching_brace_outdent").MatchingBraceOutdent;
+var Range = require("../range").Range;
+
+var Mode = function() {
+ this.HighlightRules = ComaHighlightRules;
+
+ this.$outdent = new MatchingBraceOutdent();
+};
+oop.inherits(Mode, TextMode);
+
+var indenter = /(?:[({[=:]|[-=]>|\b(?:else|try|with))\s*$/;
+
+(function() {
+
+ this.toggleCommentLines = function(state, doc, startRow, endRow) {
+ var i, line;
+ var outdent = true;
+ var re = /^\s*\(\*(.*)\*\)/;
+
+ for (i=startRow; i<= endRow; i++) {
+ if (!re.test(doc.getLine(i))) {
+ outdent = false;
+ break;
+ }
+ }
+
+ var range = new Range(0, 0, 0, 0);
+ for (i=startRow; i<= endRow; i++) {
+ line = doc.getLine(i);
+ range.start.row = i;
+ range.end.row = i;
+ range.end.column = line.length;
+
+ doc.replace(range, outdent ? line.match(re)[1] : "(*" + line + "*)");
+ }
+ };
+
+ this.getNextLineIndent = function(state, line, tab) {
+ var indent = this.$getIndent(line);
+ var tokens = this.getTokenizer().getLineTokens(line, state).tokens;
+
+ if (!(tokens.length && tokens[tokens.length - 1].type === 'comment') &&
+ state === 'start' && indenter.test(line))
+ indent += tab;
+ return indent;
+ };
+
+ this.checkOutdent = function(state, line, input) {
+ return this.$outdent.checkOutdent(line, input);
+ };
+
+ this.autoOutdent = function(state, doc, row) {
+ this.$outdent.autoOutdent(doc, row);
+ };
+ this.blockComment = {start: "(*", end: "*)", nestable: true};
+ this.$id = "ace/mode/coma";
+}).call(Mode.prototype);
+
+exports.Mode = Mode;
+});
diff --git a/src/trywhy3/trywhy3.ml b/src/trywhy3/trywhy3.ml
index a1273304d93da310156a328b1acf73710503d9d8..c6ebe3085094e7e2ebbe36e307cf2d56af5d4e13 100644
--- a/src/trywhy3/trywhy3.ml
+++ b/src/trywhy3/trywhy3.ml
@@ -403,6 +403,7 @@ module FormatList = struct
let mode =
match lang with
| "python" -> !!"python"
+ | "coma" -> !!"coma"
| "micro-C" -> !!"c_cpp"
| _ -> !!"why3" in
let mode = !!"ace/mode/" ## concat mode in
diff --git a/src/trywhy3/why3_worker.ml b/src/trywhy3/why3_worker.ml
index 96c7d15b524c48ab539ca23ec5a241a86eda0d34..9ba79a85f2270495a4bb3bd33577e2f19d58e400 100644
--- a/src/trywhy3/why3_worker.ml
+++ b/src/trywhy3/why3_worker.ml
@@ -79,11 +79,11 @@ module Task =
type task_info = {
task : task_kind;
- parent_id : id;
- mutable status : status;
- mutable subtasks : id list;
- loc : why3_loc list;
- expl : string;
+ parent_id : id;
+ mutable status : status;
+ mutable subtasks : id list;
+ loc : why3_loc list;
+ expl : string;
pretty : string;
}
@@ -102,7 +102,6 @@ module Task =
Some (a,b,c,d)
else None
-
let warnings = ref []
let clear_warnings () = warnings := []
let () =
@@ -111,7 +110,6 @@ module Task =
let _, a, b,_, _ = Loc.get loc in
warnings := ((a-1,b), msg) :: !warnings)
-
let premise_kind = function
| { Term. t_node = Term.Tnot _; t_loc = None } -> "why3-loc-neg-premise"
| _ -> "why3-loc-premise"
@@ -170,11 +168,11 @@ module Task =
in
let task_info =
{ task = Task task;
- parent_id = parent_id;
- status = StNew;
- subtasks = [];
- loc = id_loc @ (collect_locs task);
- expl = expl;
+ parent_id = parent_id;
+ status = StNew;
+ subtasks = [];
+ loc = id_loc @ (collect_locs task);
+ expl = expl;
pretty = task_text task;
}
in
@@ -185,8 +183,8 @@ module Task =
let th_id = gen_id () in
let tasks = Why3Task.split_theory th None None in
let task_ids = List.fold_left (fun acc t ->
- let tid = register_task th_id t in
- tid:: acc) [] tasks in
+ let tid = register_task th_id t in
+ tid:: acc) [] tasks in
Hashtbl.add task_table th_id {
task = Theory th;
parent_id = 0;
@@ -206,26 +204,26 @@ module Task =
let rec loop id st acc =
match get_info_opt id with
| Some info when info.status <> st ->
- info.status <- st;
+ info.status <- st;
let acc = (UpdateStatus (st, id)) :: acc in
begin
match get_info_opt info.parent_id with
None -> acc
| Some par_info ->
- let has_new, has_unknown =
- List.fold_left
- (fun (an, au) id ->
- let info = Hashtbl.find task_table id in
- (an || info.status = StNew), (au || info.status = StUnknown))
- (false, false) par_info.subtasks
- in
- let par_status =
+ let has_new, has_unknown =
+ List.fold_left
+ (fun (an, au) id ->
+ let info = Hashtbl.find task_table id in
+ (an || info.status = StNew), (au || info.status = StUnknown))
+ (false, false) par_info.subtasks
+ in
+ let par_status =
if has_new then StNew
else if has_unknown then StUnknown
else StValid
- in
- if par_info.status <> par_status then
- loop info.parent_id par_status acc
+ in
+ if par_info.status <> par_status then
+ loop info.parent_id par_status acc
else acc
end
| _ -> acc
@@ -266,12 +264,12 @@ let rec why3_prove ?(steps= ~-1) id =
let rec why3_split t orig id steps unfold =
let open Task in
match Trans.apply split_trans orig with
- | [] -> ()
- | [ child ] when Why3.Task.task_equal child orig ->
- if unfold then why3_split t (Trans.apply Inlining.goal orig) id steps false
- | subtasks ->
- t.subtasks <- List.map (fun t -> register_task id t) subtasks;
- List.iter (fun i -> why3_prove i ~steps) t.subtasks
+ | [] -> ()
+ | [ child ] when Why3.Task.task_equal child orig ->
+ if unfold then why3_split t (Trans.apply Inlining.goal orig) id steps false
+ | subtasks ->
+ t.subtasks <- List.map (fun t -> register_task id t) subtasks;
+ List.iter (fun i -> why3_prove i ~steps) t.subtasks
let why3_split steps id =
let open Task in
@@ -367,14 +365,14 @@ let why3_run f format lang code =
| Loc.Located(loc,e') ->
let msg =
Pp.sprintf "error %a: %a" Loc.pp_position_no_file loc
- Exn_printer.exn_printer e'
+ Exn_printer.exn_printer e'
in
let _, bl, bc, el, ec = Loc.get loc in
W.send (ErrorLoc ((bl-1, bc, el-1, ec),msg))
| e ->
W.send (Error (Pp.sprintf
- "unexpected exception: %a (%s)" Exn_printer.exn_printer e
- (Printexc.to_string e)))
+ "unexpected exception: %a (%s)" Exn_printer.exn_printer e
+ (Printexc.to_string e)))
let handle_message = function
| Transform (Split steps, id) -> why3_split steps id