+ Scanf.sscanf s "%u" A.mk_and
+
+let process_centralized conf =
+ let preamble = L.get_preamble conf in
+ if R.has "xoa.objects" && R.has "xoa.notations" then begin
+ let ooch = L.open_out preamble (R.get_string "xoa.objects") in
+ let noch = L.open_out preamble (R.get_string "xoa.notations") in
+ List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
+ L.out_include ooch (R.get_string "xoa.notations" ^ ".ma");
+ List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex");
+ List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or");
+ List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and");
+ close_out noch; close_out ooch
+ end
+
+let generate (p, o, n) d =
+ let oname, nname = match d with
+ | A.Exists (c, v) ->
+ let oname = Printf.sprintf "%s/ex_%u_%u" o c v in
+ let nname = Printf.sprintf "%s/ex_%u_%u" n c v in
+ oname, nname
+ | A.Or c ->
+ let oname = Printf.sprintf "%s/or_%u" o c in
+ let nname = Printf.sprintf "%s/or_%u" n c in
+ oname, nname
+ | A.And c ->
+ let oname = Printf.sprintf "%s/and_%u" o c in
+ let nname = Printf.sprintf "%s/and_%u" n c in
+ oname, nname
+ in
+ if !incremental && L.exists_out oname && L.exists_out nname then () else
+ begin
+ let ooch = L.open_out p oname in
+ let noch = L.open_out p nname in
+ List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
+ L.out_include ooch (nname ^ ".ma");
+ E.generate ooch noch d;
+ close_out noch; close_out ooch
+ end
+
+let process_distributed conf =
+ let preamble = L.get_preamble conf in
+ if R.has "xoa.objects" && R.has "xoa.notations" then begin
+ let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in
+ List.iter (generate st) (R.get_list unm_ex "xoa.ex");
+ List.iter (generate st) (R.get_list unm_or "xoa.or");
+ List.iter (generate st) (R.get_list unm_and "xoa.and");
+ end