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.sn = [] then begin
  22     if EU.stage_compare st.ET.ss v <> 0 then begin
  23       st.ET.ss <- v; st.ET.sm <- true
  24     end
  25   end else EU.raise_error ET.EWaiting
  26
  27 let select_entry = function
  28   | [0]       -> List.iter EU.robj_select st.ET.sr
  29   | [0;m]     -> EU.list_nth EU.robj_select m st.ET.sr
  30   | [0;m;1]   ->
  31     let pred r = List.iter EU.oobj_select r.ET.ro in
  32     EU.list_nth pred m st.ET.sr
  33   | [0;m;1;n] ->
  34     let pred r = EU.list_nth EU.oobj_select n r.ET.ro in
  35     EU.list_nth pred m st.ET.sr
  36   | [0;m;2]   ->
  37     let pred r = List.iter EU.nobj_select r.ET.rn in
  38     EU.list_nth pred m st.ET.sr
  39   | [0;m;2;n] ->
  40     let pred r = EU.list_nth EU.nobj_select n r.ET.rn in
  41     EU.list_nth pred m st.ET.sr
  42   | [1]       -> List.iter EU.oobj_select st.ET.so
  43   | [1;n]     -> EU.list_nth EU.oobj_select n st.ET.so
  44   | [2]       -> List.iter EU.nobj_select st.ET.sn
  45   | [2;n]     -> EU.list_nth EU.nobj_select n st.ET.sn
  46   | _         -> EU.raise_error ET.ENoEntry
  47
  48 let select_entry p =
  49   EU.pointer_visit select_entry [] p
  50
  51 let expand_entry = function
  52   | [0]   -> List.iter EU.robj_expand st.ET.sr
  53   | [0;m] -> EU.list_nth EU.robj_expand m st.ET.sr
  54   | _     -> EU.raise_error ET.ENoEntry
  55
  56 let expand_entry p =
  57   EU.pointer_visit expand_entry [] p
  58
  59 let make_tops () =
  60   if EU.stage_compare st.ET.ss [] = 0 then EU.raise_error ET.ENoStage else
  61   if st.ET.so <> [] then EU.raise_error ET.ETops else
  62   if st.ET.sn <> [] then begin
  63     st.ET.so <- List.map (EU.oobj_of_nobj st.ET.ss) st.ET.sn;
  64     st.ET.sm <- true
  65   end
  66
  67 let add_role () =
  68   let ts, os = EU.list_split EU.oobj_selected EU.oobj_select st.ET.so in
  69   let ws, ns = EU.list_split EU.nobj_selected EU.nobj_select st.ET.sn in
  70   if os = [] && ns = [] then () else
  71   let add r =
  72     r.ET.ro <- EU.oobj_union os r.ET.ro;
  73     r.ET.rn <- EU.nobj_union ns r.ET.rn;
  74     r.ET.rb <- false
  75   in
  76   let is_selected _ r = r.ET.rb && EU.stage_compare r.ET.rs st.ET.ss = 0 in
  77   let is_new _ r = r.ET.ro = [] && EU.stage_compare r.ET.rs st.ET.ss = 0 in
  78   let is_deleted _ r = r.ET.rn = [] && EU.stage_compare r.ET.rs st.ET.ss = 0 in
  79   begin
  80     if EU.list_apply is_selected add 0 st.ET.sr then () else
  81     if os = [] && EU.list_apply is_new add 0 st.ET.sr then () else
  82     if ns = [] && EU.list_apply is_deleted add 0 st.ET.sr then () else
  83     let r = {ET.rb = false; ET.rx = false; ET.rs = st.ET.ss; ET.ro = os; ET.rn = ns} in
  84     st.ET.sr <- EU.robj_union st.ET.sr [r]
  85   end;
  86   st.ET.so <- ts; st.ET.sn <- ws; st.ET.sm <- true
  87
  88 let add_tops v =
  89   let prop _ r = EU.stage_compare r.ET.rs v = 0 && r.ET.rn = [] in
  90   if EU.list_apply prop ignore 0 st.ET.sr || st.ET.so <> []
  91   then EU.raise_error ET.ETops else
  92   let ds, ts = EU.robj_tops v st.ET.sr in
  93   if ds <> [] then begin
  94     let r = {ET.rb = false; ET.rx = false; ET.rs = st.ET.ss; ET.ro = ds; ET.rn = []} in
  95     st.ET.sr <- EU.robj_union [r] st.ET.sr
  96   end;
  97   if ts <> [] then st.ET.so <- ts;
  98   if ds <> [] || ts <> [] then st.ET.sm <- true
  99
 100 let rec add_matching () =
 101   match EU.oobj_match 0 0 st.ET.so st.ET.sn with
 102   | None          -> ()
 103   | Some  (ti,wi) ->
 104     select_entry [ET.One 1; ET.One ti];
 105     select_entry [ET.One 2; ET.One wi];
 106     add_role ();
 107     add_matching ()
 108
 109 let remove_roles () =
 110   let rs, os, ns = EU.robj_split st.ET.ss st.ET.sr in
 111   if os = [] && ns = [] then () else begin
 112     st.ET.so <- EU.oobj_union os st.ET.so;
 113     st.ET.sn <- EU.nobj_union ns st.ET.sn;
 114     st.ET.sr <- rs; st.ET.sm <- true
 115   end
 116
 117 let read_waiting fname =
 118   if EU.stage_compare st.ET.ss [] = 0 then EU.raise_error ET.ENoStage else
 119   let ich = Scanf.Scanning.open_in fname in
 120   let ws = EI.read_rev_nobjs ich [] in
 121   Scanf.Scanning.close_in ich;
 122   let map ws w = EU.nobj_union ws [w] in
 123   st.ET.sn <- List.fold_left map st.ET.sn ws;
 124   if ws <> [] then st.ET.sm <- true
 125
 126 let read_status () =
 127   if EU.stage_compare st.ET.ss [] <> 0 then EU.raise_error (ET.EStage st.ET.ss) else
 128   let fname = Filename.concat !EG.cwd "roles.osn" in
 129   let ich = open_in fname in
 130   let tmp = EI.read_status ich in
 131   close_in ich;
 132   st.ET.sm <- tmp.ET.sm;
 133   st.ET.sr <- tmp.ET.sr;
 134   st.ET.ss <- tmp.ET.ss;
 135   st.ET.so <- tmp.ET.so;
 136   st.ET.sn <- tmp.ET.sn
 137
 138 let write_status () =
 139   let fname = Filename.concat !EG.cwd "roles.osn" in
 140   let och = open_out fname in
 141   EO.out_status och st;
 142   close_out och;
 143   st.ET.sm <- false
 144
 145 let print_status () =
 146   EO.out_status stdout st
 147
 148 let visit_status
 149   before_r each_r before after after_r stage
 150   before_t each_t after_t before_w each_w after_w =
 151   let visit_tw _ _ = () in
 152   let visit_r p r =
 153     before r.ET.rx (r.ET.ro=[]) (r.ET.rn=[]);
 154     if r.ET.rx then begin
 155       EU.list_visit before_t each_t visit_tw after_t EU.oobj_selected EU.key_of_oobj EU.string_of_oobj (ET.One 1::p) r.ET.ro;
 156       EU.list_visit before_w each_w visit_tw after_w EU.nobj_selected EU.key_of_nobj EU.string_of_nobj (ET.One 2::p) r.ET.rn
 157     end;
 158     after r.ET.rx
 159   in
 160   EU.list_visit before_r each_r visit_r after_r EU.robj_selected EU.key_of_robj EU.string_of_robj [ET.One 0] st.ET.sr;
 161   stage (EU.string_of_stage st.ET.ss) st.ET.sm;
 162   EU.list_visit before_t each_t visit_tw after_t EU.oobj_selected EU.key_of_oobj EU.string_of_oobj [ET.One 1] st.ET.so;
 163   EU.list_visit before_w each_w visit_tw after_w EU.nobj_selected EU.key_of_nobj EU.string_of_nobj [ET.One 2] st.ET.sn