wip

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))))

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

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;

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;

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

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 =

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