matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module EG = RolesGlobal
  13 module EI = RolesInput
  14 module EO = RolesOutput
  15 module EU = RolesUtils
  16 module ET = RolesTypes
  17
  18 let st = EU.new_status
  19
  20 let new_stage v =
  21   if st.ET.w = [] then begin
  22     if EU.compare_versions st.ET.s v <> 0 then begin
  23       st.ET.s <- v; st.ET.m <- true
  24     end
  25   end else EU.raise_error ET.EWaiting
  26
  27 let select_entry = function
  28   | [0]       -> st.ET.r <- EU.list_select_all st.ET.r
  29   | [0;m]     -> st.ET.r <- EU.list_select m st.ET.r
  30   | [0;m;1]   ->
  31     let r = EU.list_nth m st.ET.r in
  32     r.ET.o <- EU.list_select_all r.ET.o
  33   | [0;m;1;n] ->
  34     let r = EU.list_nth m st.ET.r in
  35     r.ET.o <- EU.list_select n r.ET.o
  36   | [0;m;2]   ->
  37     let r = EU.list_nth m st.ET.r in
  38     r.ET.n <- EU.list_select_all r.ET.n
  39   | [0;m;2;n] ->
  40     let r = EU.list_nth m st.ET.r in
  41     r.ET.n <- EU.list_select n r.ET.n
  42   | [1]       -> st.ET.t <- EU.list_select_all st.ET.t
  43   | [1;m]     -> st.ET.t <- EU.list_select m st.ET.t
  44   | [2]       -> st.ET.w <- EU.list_select_all st.ET.w
  45   | [2;m]     -> st.ET.w <- EU.list_select m st.ET.w
  46   | _         -> EU.raise_error ET.ENoEntry
  47
  48 let expand_entry = function
  49   | [0]   -> EU.roles_expand_all st.ET.r
  50   | [0;m] -> EU.roles_expand m st.ET.r
  51   | _     -> EU.raise_error ET.ENoEntry
  52
  53 let add_role () =
  54   let ts,os = EU.list_split st.ET.t in
  55   let ws,ns = EU.list_split st.ET.w in
  56   if os = [] && ns = [] then () else
  57   begin match EU.list_find_selected None st.ET.r with
  58   | None   ->
  59     let r = {ET.x = false; ET.v = st.ET.s; ET.o = os; ET.n = ns} in
  60     st.ET.r <- EU.roles_union [false, r] st.ET.r
  61   | Some r ->
  62     if r.ET.v <> st.ET.s then EU.raise_error ET.EWrongVersion else
  63     r.ET.o <- EU.objs_union os r.ET.o;
  64     r.ET.n <- EU.names_union ns r.ET.n;
  65   end;
  66   st.ET.t <- ts; st.ET.w <- ws; st.ET.m <- true
  67
  68 let add_tops v =
  69   if EU.exists_role_deleted st.ET.s st.ET.r || st.ET.t <> []
  70   then EU.raise_error ET.ETops else
  71   let ds, ts = EU.get_tops v st.ET.r in
  72   if ds <> [] then begin
  73     let r = {ET.x = false; ET.v = st.ET.s; ET.o = ds; ET.n = []} in
  74     st.ET.r <- EU.roles_union [false, r] st.ET.r
  75   end;
  76   if ts <> [] then st.ET.t <- ts;
  77   if ds <> [] || ts <> [] then st.ET.m <- true
  78
  79 let rec add_matching () =
  80   match EU.match_names 0 0 st.ET.t st.ET.w with
  81   | None          -> ()
  82   | Some  (ti,wi) ->
  83     select_entry [1;ti];
  84     select_entry [2;wi];
  85     add_role ();
  86     add_matching ()
  87
  88 let remove_roles () =
  89   let rs, os, ns = EU.roles_split st.ET.s st.ET.r in
  90   if os = [] && ns = [] then () else begin
  91     st.ET.t <- EU.objs_union os st.ET.t;
  92     st.ET.w <- EU.names_union ns st.ET.w;
  93     st.ET.r <- rs; st.ET.m <- true
  94   end
  95
  96 let read_waiting fname =
  97   if st.ET.s = [] then EU.raise_error ET.ENoStage else
  98   let ich = Scanf.Scanning.open_in fname in
  99   let ws = EI.read_rev_names ich [] in
 100   Scanf.Scanning.close_in ich;
 101   let map ws w = EU.names_union ws [w] in
 102   st.ET.w <- List.fold_left map st.ET.w ws;
 103   if ws <> [] then st.ET.m <- true
 104
 105 let read_status () =
 106   if st.ET.s <> [] then EU.raise_error (ET.EStage st.ET.s) else
 107   let fname = Filename.concat !EG.cwd "roles.osn" in
 108   let ich = open_in fname in
 109   let tmp = EI.read_status ich in
 110   close_in ich;
 111   st.ET.m <- tmp.ET.m;
 112   st.ET.r <- tmp.ET.r;
 113   st.ET.s <- tmp.ET.s;
 114   st.ET.t <- tmp.ET.t;
 115   st.ET.w <- tmp.ET.w
 116
 117 let write_status () =
 118   let fname = Filename.concat !EG.cwd "roles.osn" in
 119   let och = open_out fname in
 120   EO.out_status och st;
 121   close_out och;
 122   st.ET.m <- false
 123
 124 let print_status () =
 125   EO.out_status stdout st
 126
 127 let visit_status
 128   before_r each_r before after after_r stage
 129   before_t each_t after_t before_w each_w after_w =
 130   let visit_tw _ _ = () in
 131   let visit_r p r =
 132     if r.ET.x then begin
 133       before ();
 134       EU.list_visit before_t each_t visit_tw after_t EU.string_of_obj (1::p) r.ET.o;
 135       EU.list_visit before_w each_w visit_tw after_w EU.string_of_name (2::p) r.ET.n;
 136       after ()
 137     end
 138   in
 139   EU.list_visit before_r each_r visit_r after_r EU.string_of_role [0] st.ET.r;
 140   stage (EU.string_of_version st.ET.s) st.ET.m;
 141   EU.list_visit before_t each_t visit_tw after_t EU.string_of_obj [1] st.ET.t;
 142   EU.list_visit before_w each_w visit_tw after_w EU.string_of_name [2] st.ET.w