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 st.ET.s <- v
  22   else EU.raise_error ET.ENews
  23
  24 let toggle_entry = function
  25   | [0]       -> st.ET.r <- EU.list_toggle_all st.ET.r
  26   | [0;m]     -> st.ET.r <- EU.list_toggle m st.ET.r
  27   | [0;m;1]   ->
  28     let r = EU.list_nth m st.ET.r in
  29     r.ET.o <- EU.list_toggle_all r.ET.o
  30   | [0;m;1;n] ->
  31     let r = EU.list_nth m st.ET.r in
  32     r.ET.o <- EU.list_toggle n r.ET.o
  33   | [0;m;2]   ->
  34     let r = EU.list_nth m st.ET.r in
  35     r.ET.n <- EU.list_toggle_all r.ET.n
  36   | [0;m;2;n] ->
  37     let r = EU.list_nth m st.ET.r in
  38     r.ET.n <- EU.list_toggle n r.ET.n
  39   | [1]        -> st.ET.t <- EU.list_toggle_all st.ET.t
  40   | [1;m]      -> st.ET.t <- EU.list_toggle m st.ET.t
  41   | [2]        -> st.ET.w <- EU.list_toggle_all st.ET.w
  42   | [2;m]      -> st.ET.w <- EU.list_toggle m st.ET.w
  43   | _          -> EU.raise_error ET.ENoEntry
  44
  45 let add_role () =
  46   let ts,os = EU.list_split st.ET.t in
  47   let ws,ns = EU.list_split st.ET.w in
  48   if os = [] && ns = [] then () else
  49   begin match EU.list_select None st.ET.r with
  50   | None   ->
  51     let r = {ET.v = st.ET.s; ET.o = os; ET.n = ns} in
  52     st.ET.r <- EU.roles_union [false, r] st.ET.r
  53   | Some r ->
  54     if r.ET.v <> st.ET.s then EU.raise_error ET.EWrongVersion else
  55     r.ET.o <- EU.objs_union os r.ET.o;
  56     r.ET.n <- EU.names_union ns r.ET.n;
  57   end;
  58   st.ET.t <- ts; st.ET.w <- ws
  59
  60 let read_waiting fname =
  61   if st.ET.s = [] then EU.raise_error ET.ENoStage else
  62   let ich = Scanf.Scanning.open_in fname in
  63   let w = EI.read_names ich [] in
  64   Scanf.Scanning.close_in ich;
  65   st.ET.w <- EU.names_union st.ET.w (List.rev w)
  66
  67 let read_status () =
  68   if st.ET.s <> [] then EU.raise_error (ET.EStage st.ET.s) else
  69   let fname = Filename.concat !EG.wd "roles.osn" in
  70   let ich = open_in fname in
  71   let tmp = EI.read_status ich in
  72   close_in ich;
  73   st.ET.r <- tmp.ET.r;
  74   st.ET.s <- tmp.ET.s;
  75   st.ET.t <- tmp.ET.t;
  76   st.ET.w <- tmp.ET.w
  77
  78 let write_status () =
  79   let fname = Filename.concat !EG.wd "roles.osn" in
  80   let och = open_out fname in
  81   EO.out_status och st;
  82   close_out och