API tools faq
paste
Guest User

Untitled

a guest
Sep 12th, 2018
92
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
OCaml 13.86 KB | None | 0 0
raw download clone embed print report
  1. structure INY_Simulation : sig
  2.  
  3.   val compute_sa :
  4.  
  5.     (IntInf.int, unit) RBT.rbt *
  6.  
  7.       ((IntInf.int, unit) RBT.rbt *
  8.  
  9.         (((IntInf.int, (IntInf.int, (IntInf.int, unit) RBT.rbt) RBT.rbt)
  10.  
  11.             RBT.rbt,
  12.  
  13.            (IntInf.int, (IntInf.int, IntInf.int) RBT.rbt) RBT.rbt)
  14.  
  15.            LTSByLTS_DLTS.lTS_choice *
  16.  
  17.           ((IntInf.int, unit) RBT.rbt *
  18.  
  19.             ((IntInf.int, unit) RBT.rbt * unit NFAByLTS.nfa_props_ext)))) ->
  20.  
  21.       ((IntInf.int * IntInf.int), unit) RBT.rbt
  22.  
  23. end = struct
  24.  
  25.  
  26.  
  27. fun compute_sa a_impl =
  28.  
  29.   StdInst.rr_diff
  30.  
  31.     (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  32.  
  33.       (Arith.equal_nat, Arith.linorder_nat))
  34.  
  35.     (SetGA.cart (RBTSetImpl.rs_iteratei Arith.linorder_nat)
  36.  
  37.       (RBTSetImpl.rs_iteratei Arith.linorder_nat)
  38.  
  39.       (RBTSetImpl.rs_empty
  40.  
  41.         (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  42.  
  43.           (Arith.equal_nat, Arith.linorder_nat)))
  44.  
  45.       (RBTSetImpl.rs_ins_dj
  46.  
  47.         (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  48.  
  49.           (Arith.equal_nat, Arith.linorder_nat)))
  50.  
  51.       (Product_Type.fst a_impl) (Product_Type.fst a_impl))
  52.  
  53.     (Product_Type.fst
  54.  
  55.       let
  56.  
  57.         val (a, (aa, ba)) =
  58.  
  59.           RBTSetImpl.rs_iteratei Arith.linorder_nat
  60.  
  61.             (Product_Type.fst (Product_Type.snd a_impl)) (fn _ => true)
  62.  
  63.             (fn x => fn (a, (aa, ba)) =>
  64.  
  65.               RBTSetImpl.rs_iteratei Arith.linorder_nat
  66.  
  67.                 (Product_Type.fst a_impl) (fn _ => true)
  68.  
  69.                 (fn xa => fn (ab, (ac, bc)) =>
  70.  
  71.                   let
  72.  
  73.                     val xb =
  74.  
  75.                       RBTMapImpl.rm_update
  76.  
  77.                         (Misc.linorder_prod
  78.  
  79.                           (Arith.equal_nat, Arith.linorder_nat)
  80.  
  81.                           (Arith.equal_nat, Arith.linorder_nat))
  82.  
  83.                         (xa, x) 0 ac;
  84.  
  85.                     val xc =
  86.  
  87.                       RBTMapImpl.rm_update
  88.  
  89.                         (Misc.linorder_prod
  90.  
  91.                           (Arith.equal_nat, Arith.linorder_nat)
  92.  
  93.                           (Arith.equal_nat, Arith.linorder_nat))
  94.  
  95.                         (xa, x) (RBTSetImpl.rs_empty Arith.linorder_nat ()) bc;
  96.  
  97.                     val xd =
  98.  
  99.                       RBTSetImpl.rs_iteratei Arith.linorder_nat
  100.  
  101.                         (Product_Type.fst a_impl) (fn _ => true)
  102.  
  103.                         (fn xba => fn ad =>
  104.  
  105.                           RBTMapImpl.rm_update
  106.  
  107.                             (Misc.linorder_prod
  108.  
  109.                               (Arith.equal_nat, Arith.linorder_nat)
  110.  
  111.                               (Product_Type.equal_prod Arith.equal_nat
  112.  
  113.                                  Arith.equal_nat,
  114.  
  115.                                 Misc.linorder_prod
  116.  
  117.                                   (Arith.equal_nat, Arith.linorder_nat)
  118.  
  119.                                   (Arith.equal_nat, Arith.linorder_nat)))
  120.  
  121.                             (x, (xa, xba)) 0 ad)
  122.  
  123.                         ab;
  124.  
  125.                   in
  126.  
  127.                     (xd, (xb, xc))
  128.  
  129.                   end)
  130.  
  131.                 (a, (aa, ba)))
  132.  
  133.             (RBTMapImpl.rm_empty
  134.  
  135.                (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  136.  
  137.                  (Product_Type.equal_prod Arith.equal_nat Arith.equal_nat,
  138.  
  139.                    Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  140.  
  141.                      (Arith.equal_nat, Arith.linorder_nat)))
  142.  
  143.                (),
  144.  
  145.               (RBTMapImpl.rm_empty
  146.  
  147.                  (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  148.  
  149.                    (Arith.equal_nat, Arith.linorder_nat))
  150.  
  151.                  (),
  152.  
  153.                 RBTMapImpl.rm_empty
  154.  
  155.                   (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  156.  
  157.                     (Arith.equal_nat, Arith.linorder_nat))
  158.  
  159.                   ()));
  160.  
  161.         val (ab, bb) =
  162.  
  163.           (case Product_Type.fst (Product_Type.snd (Product_Type.snd a_impl))
  164.  
  165.             of LTSByLTS_DLTS.Lts ab =>
  166.  
  167.               RBT_TripleSetImpl.rs_ts_it Arith.linorder_nat Arith.linorder_nat
  168.  
  169.                 Arith.linorder_nat ab
  170.  
  171.             | LTSByLTS_DLTS.Dlts ab =>
  172.  
  173.               RBT_DLTSImpl.rs_dlts_it Arith.linorder_nat Arith.linorder_nat ab)
  174.  
  175.             (fn _ => true)
  176.  
  177.             (fn x => fn (ab, b) =>
  178.  
  179.               let
  180.  
  181.                 val (aaa, (aba, bb)) = x;
  182.  
  183.               in
  184.  
  185.                 ((case RBTMapImpl.rm_lookup
  186.  
  187.                          (Misc.linorder_prod
  188.  
  189.                            (Arith.equal_nat, Arith.linorder_nat)
  190.  
  191.                            (Arith.equal_nat, Arith.linorder_nat))
  192.  
  193.                          (aaa, aba) ab
  194.  
  195.                    of NONE => ab
  196.  
  197.                    | SOME xa =>
  198.  
  199.                      RBTMapImpl.rm_update
  200.  
  201.                        (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  202.  
  203.                          (Arith.equal_nat, Arith.linorder_nat))
  204.  
  205.                        (aaa, aba) (IntInf.+ (xa, (1 : IntInf.int))) ab),
  206.  
  207.                   (case RBTMapImpl.rm_lookup
  208.  
  209.                           (Misc.linorder_prod
  210.  
  211.                             (Arith.equal_nat, Arith.linorder_nat)
  212.  
  213.                             (Arith.equal_nat, Arith.linorder_nat))
  214.  
  215.                           (bb, aba) b
  216.  
  217.                     of NONE => b
  218.  
  219.                     | SOME xa =>
  220.  
  221.                       RBTMapImpl.rm_update
  222.  
  223.                         (Misc.linorder_prod
  224.  
  225.                           (Arith.equal_nat, Arith.linorder_nat)
  226.  
  227.                           (Arith.equal_nat, Arith.linorder_nat))
  228.  
  229.                         (bb, aba) (RBTSetImpl.rs_ins Arith.linorder_nat aaa xa)
  230.  
  231.                         b))
  232.  
  233.               end)
  234.  
  235.             (aa, ba);
  236.  
  237.         val xb =
  238.  
  239.           let
  240.  
  241.             val ac =
  242.  
  243.               RBTSetImpl.rs_iteratei Arith.linorder_nat
  244.  
  245.                 (Product_Type.fst (Product_Type.snd a_impl)) (fn _ => true)
  246.  
  247.                 (fn x => fn ac =>
  248.  
  249.                   RBTSetImpl.rs_iteratei Arith.linorder_nat
  250.  
  251.                     (Product_Type.fst a_impl) (fn _ => true)
  252.  
  253.                     (fn xa => fn sa =>
  254.  
  255.                       (if not (Option.equal_option Arith.equal_nat
  256.  
  257.                                 (RBTMapImpl.rm_lookup
  258.  
  259.                                   (Misc.linorder_prod
  260.  
  261.                                     (Arith.equal_nat, Arith.linorder_nat)
  262.  
  263.                                     (Arith.equal_nat, Arith.linorder_nat))
  264.  
  265.                                   (xa, x) ab)
  266.  
  267.                                 (SOME 0))
  268.  
  269.                         then RBTSetImpl.rs_iteratei Arith.linorder_nat
  270.  
  271.                                (Product_Type.fst a_impl) (fn _ => true)
  272.  
  273.                                (fn xb => fn sb =>
  274.  
  275.                                  (if Option.equal_option Arith.equal_nat
  276.  
  277.                                        (RBTMapImpl.rm_lookup
  278.  
  279.  (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  280.  
  281.    (Arith.equal_nat, Arith.linorder_nat))
  282.  
  283.  (xb, x) ab)
  284.  
  285.                                        (SOME 0)
  286.  
  287.                                    then RBTSetImpl.rs_ins
  288.  
  289.   (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  290.  
  291.     (Arith.equal_nat, Arith.linorder_nat))
  292.  
  293.   (xa, xb) sb
  294.  
  295.                                    else sb))
  296.  
  297.                                sa
  298.  
  299.                         else sa))
  300.  
  301.                     ac)
  302.  
  303.                 (RBTSetImpl.rs_empty
  304.  
  305.                   (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  306.  
  307.                     (Arith.equal_nat, Arith.linorder_nat))
  308.  
  309.                   ());
  310.  
  311.           in
  312.  
  313.             RBTSetImpl.rs_union
  314.  
  315.               (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  316.  
  317.                 (Arith.equal_nat, Arith.linorder_nat))
  318.  
  319.               (SetGA.cart (RBTSetImpl.rs_iteratei Arith.linorder_nat)
  320.  
  321.                 (RBTSetImpl.rs_iteratei Arith.linorder_nat)
  322.  
  323.                 (RBTSetImpl.rs_empty
  324.  
  325.                   (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  326.  
  327.                     (Arith.equal_nat, Arith.linorder_nat)))
  328.  
  329.                 (RBTSetImpl.rs_ins_dj
  330.  
  331.                   (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  332.  
  333.                     (Arith.equal_nat, Arith.linorder_nat)))
  334.  
  335.                 (Product_Type.fst
  336.  
  337.                   (Product_Type.snd
  338.  
  339.                     (Product_Type.snd
  340.  
  341.                       (Product_Type.snd (Product_Type.snd a_impl)))))
  342.  
  343.                 (StdInst.rr_diff Arith.linorder_nat (Product_Type.fst a_impl)
  344.  
  345.                   (Product_Type.fst
  346.  
  347.                     (Product_Type.snd
  348.  
  349.                       (Product_Type.snd
  350.  
  351.                         (Product_Type.snd (Product_Type.snd a_impl)))))))
  352.  
  353.               ac
  354.  
  355.           end;
  356.  
  357.         val (ac, (ad, _)) =
  358.  
  359.           While_Combinator.whilea
  360.  
  361.             (fn (_, (c, _)) =>
  362.  
  363.               not (RBTSetImpl.rs_isEmpty
  364.  
  365.                     (Product_Type.equal_prod Arith.equal_nat Arith.equal_nat,
  366.  
  367.                       Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  368.  
  369.                         (Arith.equal_nat, Arith.linorder_nat))
  370.  
  371.                     c))
  372.  
  373.             (fn (ac, (aaa, baa)) =>
  374.  
  375.               let
  376.  
  377.                 val (aba, bba) =
  378.  
  379.                   Option.the
  380.  
  381.                     (RBTSetImpl.rs_sel
  382.  
  383.                       (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  384.  
  385.                         (Arith.equal_nat, Arith.linorder_nat))
  386.  
  387.                       aaa (fn _ => true));
  388.  
  389.                 val (aca, (ad, bd)) =
  390.  
  391.                   RBTSetImpl.rs_iteratei Arith.linorder_nat
  392.  
  393.                     (Product_Type.fst (Product_Type.snd a_impl)) (fn _ => true)
  394.  
  395.                     (fn x => fn (ad, (aab, bab)) =>
  396.  
  397.                       let
  398.  
  399.                         val (abb, (aca, bc)) =
  400.  
  401.                           RBTSetImpl.rs_iteratei Arith.linorder_nat
  402.  
  403.                             (case RBTMapImpl.rm_lookup
  404.  
  405.                                     (Misc.linorder_prod
  406.  
  407.                                       (Arith.equal_nat, Arith.linorder_nat)
  408.  
  409.                                       (Arith.equal_nat, Arith.linorder_nat))
  410.  
  411.                                     (bba, x) bb
  412.  
  413.                               of NONE =>
  414.  
  415.                                 RBTSetImpl.rs_empty Arith.linorder_nat ()
  416.  
  417.                               | SOME s => s)
  418.  
  419.                             (fn _ => true)
  420.  
  421.                             (fn xa => fn (ae, (aac, bac)) =>
  422.  
  423.                               let
  424.  
  425.                                 val xaa =
  426.  
  427.                                   (case RBTMapImpl.rm_lookup
  428.  
  429.   (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  430.  
  431.     (Product_Type.equal_prod Arith.equal_nat Arith.equal_nat,
  432.  
  433.       Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  434.  
  435.         (Arith.equal_nat, Arith.linorder_nat)))
  436.  
  437.   (x, (aba, xa)) bac
  438.  
  439.                                     of NONE => bac
  440.  
  441.                                     | SOME n =>
  442.  
  443.                                       RBTMapImpl.rm_update
  444.  
  445. (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  446.  
  447.   (Product_Type.equal_prod Arith.equal_nat Arith.equal_nat,
  448.  
  449.     Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  450.  
  451.       (Arith.equal_nat, Arith.linorder_nat)))
  452.  
  453. (x, (aba, xa)) (IntInf.+ (n, (1 : IntInf.int))) bac);
  454.  
  455.                               in
  456.  
  457.                                 (if Option.equal_option Arith.equal_nat
  458.  
  459.                                       (RBTMapImpl.rm_lookup
  460.  
  461. (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  462.  
  463.   (Product_Type.equal_prod Arith.equal_nat Arith.equal_nat,
  464.  
  465.     Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  466.  
  467.       (Arith.equal_nat, Arith.linorder_nat)))
  468.  
  469. (x, (aba, xa)) xaa)
  470.  
  471.                                       (RBTMapImpl.rm_lookup
  472.  
  473. (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  474.  
  475.   (Arith.equal_nat, Arith.linorder_nat))
  476.  
  477. (xa, x) ab)
  478.  
  479.                                   then let
  480.  
  481.  val (abb, bbb) =
  482.  
  483.    RBTSetImpl.rs_iteratei Arith.linorder_nat
  484.  
  485.      (case RBTMapImpl.rm_lookup
  486.  
  487.              (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  488.  
  489.                (Arith.equal_nat, Arith.linorder_nat))
  490.  
  491.              (aba, x) bb
  492.  
  493.        of NONE => RBTSetImpl.rs_empty Arith.linorder_nat () | SOME s => s)
  494.  
  495.      (fn _ => true)
  496.  
  497.      (fn xc => fn (af, b) =>
  498.  
  499.        (if not (RBTSetImpl.rs_memb
  500.  
  501.                  (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  502.  
  503.                    (Arith.equal_nat, Arith.linorder_nat))
  504.  
  505.                  (xc, xa) af)
  506.  
  507.          then (RBTSetImpl.rs_ins_dj
  508.  
  509.                  (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  510.  
  511.                    (Arith.equal_nat, Arith.linorder_nat))
  512.  
  513.                  (xc, xa) af,
  514.  
  515.                 RBTSetImpl.rs_ins_dj
  516.  
  517.                   (Misc.linorder_prod (Arith.equal_nat, Arith.linorder_nat)
  518.  
  519.                     (Arith.equal_nat, Arith.linorder_nat))
  520.  
  521.                   (xc, xa) b)
  522.  
  523.          else (af, b)))
  524.  
  525.      (ae, aac);
  526.  
  527.                                        in
  528.  
  529.  (abb, (bbb, xaa))
  530.  
  531.                                        end
  532.  
  533.                                   else (ae, (aac, xaa)))
  534.  
  535.                               end)
  536.  
  537.                             (ad, (aab, bab));
  538.  
  539.                       in
  540.  
  541.                         (abb, (aca, bc))
  542.  
  543.                       end)
  544.  
  545.                     (ac, (aaa, baa));
  546.  
  547.               in
  548.  
  549.                 (aca, (RBTSetImpl.rs_delete
  550.  
  551.                          (Misc.linorder_prod
  552.  
  553.                            (Arith.equal_nat, Arith.linorder_nat)
  554.  
  555.                            (Arith.equal_nat, Arith.linorder_nat))
  556.  
  557.                          (aba, bba) ad,
  558.  
  559.                         bd))
  560.  
  561.               end)
  562.  
  563.             (xb, (xb, a));
  564.  
  565.       in
  566.  
  567.         (ac, ad)
  568.  
  569.       end);
  570.  
  571.  
  572.  
  573. end; (*struct INY_Simulation*)
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!