diff --git a/dune b/dune index c5091d875..00afbc5bc 100644 --- a/dune +++ b/dune @@ -8,6 +8,6 @@ (env (dev - (flags (:standard -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A))) + (flags (:standard -w -9 -w -32 -w -27 -warn-error -A))) (fatalwarnings - (flags (:standard -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error +A)))) + (flags (:standard -w -9 -w -32 -w -27 -warn-error +A)))) diff --git a/src/compiler.ml b/src/compiler.ml index 557c8c24b..57c478e2c 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -672,6 +672,7 @@ and block = | Namespace of string * pbody | Shorten of F.t Ast.Structured.shorthand list * pbody | Constraints of (F.t,ScopedTerm.t) Ast.Structured.block_constraint * pbody + | Accumulated of pbody [@@deriving show, ord] end @@ -892,7 +893,7 @@ end = struct (* {{{ *) let p, chr1, rest = aux_run ns [] [] [] [] [] [] [] accs rest in if chr1 <> [] then error "CHR cannot be declared inside an anonymous block"; - aux_end_block loc ns (cl2b clauses @ blocks) + aux_end_block loc ns (Accumulated p :: cl2b clauses @ blocks) [] macros types tabbrs modes chr accs rest | Program.Constraint (loc, ctx_filter, clique) :: rest -> if chr <> [] then @@ -920,15 +921,18 @@ end = struct (* {{{ *) | Program.Accumulated (_,[]) :: rest -> aux_run ns blocks clauses macros types tabbrs modes chr accs rest - | Program.Accumulated (loc,(digest,a) :: more) :: rest -> + | Program.Accumulated (loc,(filename,digest,a) :: more) :: rest -> let rest = Program.Accumulated (loc, more) :: rest in let digest = String.concat "." (digest :: List.map F.show ns) in - if StrSet.mem digest accs then + if StrSet.mem digest accs then begin + (* Printf.eprintf "skip: %s\n%!" filename; *) aux_run ns blocks clauses macros types tabbrs modes chr accs rest - else + end else begin + (* Printf.eprintf "acc: %s -> %d\n%!" filename (List.length a); *) aux_run ns blocks clauses macros types tabbrs modes chr (StrSet.add digest accs) (Program.Begin loc :: a @ Program.End loc :: rest) + end | Program.Clause c :: rest -> let c = structure_clause_attributes c in @@ -1233,6 +1237,14 @@ end = struct state, types, type_abbrevs, modes, F.Set.union defs p.Scoped.symbols, Scoped.Constraints({ctx_filter; clique; rules},p) :: compiled_rest + | Accumulated p :: rest -> + let state, _, p = compile_program macros state p in + let state, types, type_abbrevs, modes, defs, compiled_rest = + compile_body macros types type_abbrevs modes defs state rest in + state, types, type_abbrevs, modes, + F.Set.union defs p.Scoped.symbols, + Scoped.Accumulated p :: compiled_rest + in let state, toplevel_macros, pbody = compile_program F.Map.empty state p in @@ -2259,7 +2271,13 @@ end (* }}} *) let types, type_abbrevs, modes, clauses, chr = compile_block types type_abbrevs modes clauses chr subst body in compile_block types type_abbrevs modes clauses chr subst rest - + | Scoped.Accumulated { types = t; type_abbrevs = ta; modes = m; body; symbols = _ } :: rest -> + let types = merge_types (apply_subst_types subst t) types in + let type_abbrevs = merge_type_abbrevs type_abbrevs (apply_subst_type_abbrevs subst ta) in + let modes = merge_modes (apply_subst_modes subst m) modes in + let types, type_abbrevs, modes, clauses, chr = + compile_block types type_abbrevs modes clauses chr subst body in + compile_block types type_abbrevs modes clauses chr subst rest let compile_body { Scoped.types; type_abbrevs; modes; symbols; body } = compile_block types type_abbrevs modes [] [] empty_subst body diff --git a/src/parser/ast.ml b/src/parser/ast.ml index 073d5b106..cba645d03 100644 --- a/src/parser/ast.ml +++ b/src/parser/ast.ml @@ -229,7 +229,7 @@ module Program = struct | Shorten of Loc.t * (Func.t * Func.t) list (* prefix suffix *) | End of Loc.t - | Accumulated of Loc.t * (Digest.t * decl list) list + | Accumulated of Loc.t * (string * Digest.t * decl list) list (* data *) | Clause of (Term.t, raw_attribute list) Clause.t @@ -313,6 +313,7 @@ and block = | Namespace of Func.t * program | Shorten of Func.t shorthand list * program | Constraints of (Func.t,Term.t) block_constraint * program + | Accumulated of program and attribute = { insertion : insertion option; id : string option; diff --git a/src/parser/ast.mli b/src/parser/ast.mli index 0fc9feeb0..6a2a3b68c 100644 --- a/src/parser/ast.mli +++ b/src/parser/ast.mli @@ -156,7 +156,7 @@ module Program : sig | Shorten of Loc.t * (Func.t * Func.t) list (* prefix suffix *) | End of Loc.t - | Accumulated of Loc.t * (Digest.t * decl list) list + | Accumulated of Loc.t * (string * Digest.t * decl list) list (* data *) | Clause of (Term.t, raw_attribute list) Clause.t @@ -209,6 +209,7 @@ and block = | Namespace of Func.t * program | Shorten of Func.t shorthand list * program | Constraints of (Func.t,Term.t) block_constraint * program + | Accumulated of program and attribute = { insertion : insertion option; id : string option; diff --git a/src/parser/parse.ml b/src/parser/parse.ml index eda58107f..c9c33cb00 100644 --- a/src/parser/parse.ml +++ b/src/parser/parse.ml @@ -32,7 +32,7 @@ end module Make(C : Config) = struct -let parse_ref : (?cwd:string -> string -> (Digest.t * Ast.Program.decl list) list) ref = +let parse_ref : (?cwd:string -> string -> (string * Digest.t * Ast.Program.decl list) list) ref = ref (fun ?cwd:_ _ -> assert false) module Grammar = Grammar.Make(struct @@ -42,11 +42,10 @@ let message_of_state s = try Error_messages.message s with Not_found -> "syntax let chunk s (p1,p2) = String.sub s p1.Lexing.pos_cnum (p2.Lexing.pos_cnum - p1.Lexing.pos_cnum) -let parse grammar digest lexbuf = +let parse grammar lexbuf = let buffer, lexer = MenhirLib.ErrorReports.wrap Lexer.token in try - let p = grammar lexer lexbuf in - digest, p + grammar lexer lexbuf with | Ast.Term.NotInProlog(loc,message) -> raise (Parser_config.ParseError(loc,message^"\n")) @@ -77,15 +76,15 @@ let () = else [filename,digest] in to_parse |> List.map (fun (filename,digest) -> if Hashtbl.mem already_parsed digest then - digest, [] + filename, digest, [] else let ic = open_in filename in let lexbuf = Lexing.from_channel ic in lexbuf.Lexing.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = dest }; Hashtbl.add already_parsed digest true; - let ast = parse Grammar.program digest lexbuf in + let ast = parse Grammar.program lexbuf in close_in ic; - ast)) + filename, digest,ast)) let to_lexing_loc { Util.Loc.source_name; line; line_starts_at; source_start; _ } = { Lexing.pos_fname = source_name; @@ -102,7 +101,7 @@ let lexing_set_position lexbuf loc = let goal_from ~loc lexbuf = lexing_set_position lexbuf loc; - snd @@ parse Grammar.goal "" lexbuf + parse Grammar.goal lexbuf let goal ~loc ~text = let lexbuf = Lexing.from_string text in @@ -111,11 +110,11 @@ let goal ~loc ~text = let program_from ~loc lexbuf = Hashtbl.clear already_parsed; lexing_set_position lexbuf loc; - snd @@ parse Grammar.program "" lexbuf + parse Grammar.program lexbuf let program ~file = Hashtbl.clear already_parsed; - List.(concat (map snd @@ !parse_ref file)) + List.(concat (map (fun (_,_,x) -> x) @@ !parse_ref file)) module Internal = struct let infix_SYMB = Grammar.infix_SYMB diff --git a/src/parser/parser_config.ml b/src/parser/parser_config.ml index ce2cac9e6..c60c49e6c 100644 --- a/src/parser/parser_config.ml +++ b/src/parser/parser_config.ml @@ -12,7 +12,7 @@ exception ParseError of Util.Loc.t * string resolution is not a parser business *) module type ParseFile = sig - val parse_file : ?cwd:string -> string -> (Digest.t * Ast.Program.decl list) list + val parse_file : ?cwd:string -> string -> (string * Digest.t * Ast.Program.decl list) list end let rec substrings i len_s s = diff --git a/src/runtime.ml b/src/runtime.ml index ac98a5b36..24de8e3f1 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -4285,7 +4285,7 @@ let execute_once ?max_steps ?delay_outside_fragment exec = ;; let execute_loop ?delay_outside_fragment exec ~more ~pp = - let { search; next_solution; get; destroy } = make_runtime ?delay_outside_fragment exec in + let { search; next_solution; get; destroy = _ } = make_runtime ?delay_outside_fragment exec in let k = ref noalts in let do_with_infos f = let time0 = Unix.gettimeofday() in