src/asta.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                  Lucca Hirschi, ?   *)
   6 (*                  ?   *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
   9 (*  Recherche Scientifique. All rights reserved.  This file is         *)
  10 (*  distributed under the terms of the GNU Lesser General Public       *)
  11 (*  License, with the special exception on linking described in file   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 type state = State.t
  17
  18 type label = QNameSet.t
  19
  20 type formula = Formula.t
  21
  22 module Transition =
  23 struct
  24   type t = state * label * formula
  25
  26   let compare (st,la,f) (st',la',f') =
  27     let x_1 = State.compare st st' in
  28     if x_1 != 0 then x_1
  29     else let x_2 = QNameSet.compare la la' in
  30          if x_2 != 0 then x_2
  31          else Formula.compare f f'
  32   let st (st,la,f) = st
  33   let la (st,la,f) = la
  34   let fo (st,la,f) = f
  35   let print fmt (st,la,f) =
  36     Format.fprintf fmt "(%a,%s,%a)"
  37       State.print st
  38       "TODO la"
  39       Formula.print f
  40 end
  41
  42 module  SetT =
  43 struct
  44   include Set.Make(Transition)
  45 end
  46
  47 type t = {
  48   mutable reco : StateSet.t;
  49   mutable selec : StateSet.t;
  50   mutable bottom : StateSet.t;
  51   mutable top : StateSet.t;
  52   mutable trans : SetT.t;
  53 }
  54
  55 exception Not_found_transition
  56 exception Transition_not_injective
  57
  58 let transition asta st lab =
  59   let filter (s,l,f) =
  60     (State.compare s st = 0) && (QNameSet.compare l lab = 0) in
  61   let tr_set = SetT.elements (SetT.filter filter asta.trans) in
  62   match tr_set with
  63     | [] -> raise Not_found_transition
  64     | x::y::z -> raise Transition_not_injective
  65     | [l] -> Transition.fo l
  66
  67 let transitions asta st =
  68   let filter (s,l,f) = State.compare s st = 0 in
  69   let rec remove_states l = match l with
  70     | [] -> []
  71     | (a,s,l) :: tl -> (s,l) :: (remove_states tl) in
  72   remove_states (SetT.elements (SetT.filter filter asta.trans))
  73
  74 let dummy = {
  75   reco = StateSet.empty;
  76   selec = StateSet.empty;
  77   bottom = StateSet.empty;
  78   top = StateSet.empty;
  79   trans = SetT.empty;
  80 }
  81
  82
  83 let print fmt asta =
  84   let pp = Format.fprintf fmt in
  85   pp "Recognizing states: ";
  86   StateSet.print fmt asta.reco;
  87   pp "\nSelecting states: ";
  88   StateSet.print fmt asta.selec;
  89   pp "\nBottom states: ";
  90   StateSet.print fmt asta.bottom;
  91   pp "\nTop states: ";
  92   StateSet.print fmt asta.top;
  93   pp "\nTransitions: \n";
  94   Format.fprintf fmt "{@[<hov 2> %a @]}" (* todo: check boxes *)
  95     (Pretty.print_list ~sep:"@, " (Transition.print))
  96     (SetT.elements (asta.trans))
  97
  98
  99 let to_file out asta = ()