Ignore:
Timestamp:
Mar 14, 2013, 10:37:39 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/structuredTraces.ml

    r2827 r2873  
    17041704    (observables_trace_any_label s flag st1 st2 tll dummy)
    17051705
     1706type trace_any_any_free =
     1707| Taaf_base of __
     1708| Taaf_step of __ * __ * __ * trace_any_any
     1709| Taaf_step_jump of __ * __ * __ * trace_any_any
     1710
     1711(** val trace_any_any_free_rect_Type4 :
     1712    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
     1713    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
     1714    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
     1715let rec trace_any_any_free_rect_Type4 s h_taaf_base h_taaf_step h_taaf_step_jump x_17448 x_17447 = function
     1716| Taaf_base s0 -> h_taaf_base s0
     1717| Taaf_step (s1, s2, s3, x_17452) -> h_taaf_step s1 s2 s3 x_17452 __ __
     1718| Taaf_step_jump (s1, s2, s3, x_17456) ->
     1719  h_taaf_step_jump s1 s2 s3 x_17456 __ __ __
     1720
     1721(** val trace_any_any_free_rect_Type5 :
     1722    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
     1723    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
     1724    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
     1725let rec trace_any_any_free_rect_Type5 s h_taaf_base h_taaf_step h_taaf_step_jump x_17461 x_17460 = function
     1726| Taaf_base s0 -> h_taaf_base s0
     1727| Taaf_step (s1, s2, s3, x_17465) -> h_taaf_step s1 s2 s3 x_17465 __ __
     1728| Taaf_step_jump (s1, s2, s3, x_17469) ->
     1729  h_taaf_step_jump s1 s2 s3 x_17469 __ __ __
     1730
     1731(** val trace_any_any_free_rect_Type3 :
     1732    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
     1733    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
     1734    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
     1735let rec trace_any_any_free_rect_Type3 s h_taaf_base h_taaf_step h_taaf_step_jump x_17474 x_17473 = function
     1736| Taaf_base s0 -> h_taaf_base s0
     1737| Taaf_step (s1, s2, s3, x_17478) -> h_taaf_step s1 s2 s3 x_17478 __ __
     1738| Taaf_step_jump (s1, s2, s3, x_17482) ->
     1739  h_taaf_step_jump s1 s2 s3 x_17482 __ __ __
     1740
     1741(** val trace_any_any_free_rect_Type2 :
     1742    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
     1743    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
     1744    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
     1745let rec trace_any_any_free_rect_Type2 s h_taaf_base h_taaf_step h_taaf_step_jump x_17487 x_17486 = function
     1746| Taaf_base s0 -> h_taaf_base s0
     1747| Taaf_step (s1, s2, s3, x_17491) -> h_taaf_step s1 s2 s3 x_17491 __ __
     1748| Taaf_step_jump (s1, s2, s3, x_17495) ->
     1749  h_taaf_step_jump s1 s2 s3 x_17495 __ __ __
     1750
     1751(** val trace_any_any_free_rect_Type1 :
     1752    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
     1753    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
     1754    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
     1755let rec trace_any_any_free_rect_Type1 s h_taaf_base h_taaf_step h_taaf_step_jump x_17500 x_17499 = function
     1756| Taaf_base s0 -> h_taaf_base s0
     1757| Taaf_step (s1, s2, s3, x_17504) -> h_taaf_step s1 s2 s3 x_17504 __ __
     1758| Taaf_step_jump (s1, s2, s3, x_17508) ->
     1759  h_taaf_step_jump s1 s2 s3 x_17508 __ __ __
     1760
     1761(** val trace_any_any_free_rect_Type0 :
     1762    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
     1763    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
     1764    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
     1765let rec trace_any_any_free_rect_Type0 s h_taaf_base h_taaf_step h_taaf_step_jump x_17513 x_17512 = function
     1766| Taaf_base s0 -> h_taaf_base s0
     1767| Taaf_step (s1, s2, s3, x_17517) -> h_taaf_step s1 s2 s3 x_17517 __ __
     1768| Taaf_step_jump (s1, s2, s3, x_17521) ->
     1769  h_taaf_step_jump s1 s2 s3 x_17521 __ __ __
     1770
     1771(** val trace_any_any_free_inv_rect_Type4 :
     1772    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
     1773    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1774    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1775    __ -> __ -> 'a1) -> 'a1 **)
     1776let trace_any_any_free_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
     1777  let hcut = trace_any_any_free_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
     1778  hcut __ __ __
     1779
     1780(** val trace_any_any_free_inv_rect_Type3 :
     1781    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
     1782    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1783    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1784    __ -> __ -> 'a1) -> 'a1 **)
     1785let trace_any_any_free_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
     1786  let hcut = trace_any_any_free_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
     1787  hcut __ __ __
     1788
     1789(** val trace_any_any_free_inv_rect_Type2 :
     1790    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
     1791    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1792    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1793    __ -> __ -> 'a1) -> 'a1 **)
     1794let trace_any_any_free_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
     1795  let hcut = trace_any_any_free_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
     1796  hcut __ __ __
     1797
     1798(** val trace_any_any_free_inv_rect_Type1 :
     1799    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
     1800    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1801    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1802    __ -> __ -> 'a1) -> 'a1 **)
     1803let trace_any_any_free_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
     1804  let hcut = trace_any_any_free_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
     1805  hcut __ __ __
     1806
     1807(** val trace_any_any_free_inv_rect_Type0 :
     1808    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
     1809    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1810    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
     1811    __ -> __ -> 'a1) -> 'a1 **)
     1812let trace_any_any_free_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
     1813  let hcut = trace_any_any_free_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
     1814  hcut __ __ __
     1815
     1816(** val trace_any_any_free_jmdiscr :
     1817    abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free
     1818    -> __ **)
     1819let trace_any_any_free_jmdiscr a1 a2 a3 x y =
     1820  Logic.eq_rect_Type2 x
     1821    (match x with
     1822     | Taaf_base a0 -> Obj.magic (fun _ dH -> dH __)
     1823     | Taaf_step (a0, a10, a20, a30) ->
     1824       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
     1825     | Taaf_step_jump (a0, a10, a20, a30) ->
     1826       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
     1827
     1828(** val taaf_non_empty :
     1829    abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool **)
     1830let taaf_non_empty s s1 s2 = function
     1831| Taaf_base x -> Bool.False
     1832| Taaf_step (x, x0, x1, x2) -> Bool.True
     1833| Taaf_step_jump (x, x0, x1, x2) -> Bool.True
     1834
     1835(** val taa_append_taa :
     1836    abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
     1837    trace_any_any **)
     1838let rec taa_append_taa s st1 st2 st3 taa =
     1839  (match taa with
     1840   | Taa_base st1' -> (fun st30 taa2 -> taa2)
     1841   | Taa_step (st1', st2', st3', tl) ->
     1842     (fun st30 taa2 -> Taa_step (st1', st2', st30,
     1843       (taa_append_taa s st2' st3' st30 tl taa2)))) st3
     1844
     1845(** val taaf_to_taa :
     1846    abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any **)
     1847let taaf_to_taa s s1 s2 taaf =
     1848  (match taaf with
     1849   | Taaf_base s0 -> (fun _ -> Taa_base s0)
     1850   | Taaf_step (s10, s20, s3, taa) ->
     1851     (fun _ ->
     1852       taa_append_taa s s10 s20 s3 taa (Taa_step (s20, s3, s3, (Taa_base
     1853         s3))))
     1854   | Taaf_step_jump (s10, s20, s3, taa) ->
     1855     (fun _ -> assert false (* absurd case *))) __
     1856
     1857(** val taaf_append_tal :
     1858    abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
     1859    trace_any_any_free -> trace_any_label -> trace_any_label **)
     1860let taaf_append_tal s st1 fl st2 st3 taaf =
     1861  taa_append_tal s st1 fl st2 st3 (taaf_to_taa s st1 st2 taaf)
     1862
     1863(** val taaf_append_taa :
     1864    abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any
     1865    -> trace_any_any **)
     1866let taaf_append_taa s st1 st2 st3 taaf =
     1867  taa_append_taa s st1 st2 st3 (taaf_to_taa s st1 st2 taaf)
     1868
     1869(** val taaf_cons :
     1870    abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
     1871    trace_any_any_free **)
     1872let taaf_cons s s1 s2 s3 tl =
     1873  (match tl with
     1874   | Taaf_base s20 -> (fun _ _ -> Taaf_step (s1, s1, s20, (Taa_base s1)))
     1875   | Taaf_step (s20, s30, s4, taa) ->
     1876     (fun _ _ -> Taaf_step (s1, s30, s4, (Taa_step (s1, s20, s30, taa))))
     1877   | Taaf_step_jump (s20, s30, s4, taa) ->
     1878     (fun _ _ -> Taaf_step_jump (s1, s30, s4, (Taa_step (s1, s20, s30,
     1879       taa))))) __ __
     1880
     1881(** val taaf_append_taaf :
     1882    abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
     1883    trace_any_any_free -> trace_any_any_free **)
     1884let taaf_append_taaf s st1 st2 st3 taaf1 taaf2 =
     1885  (match taaf2 with
     1886   | Taaf_base s1 -> (fun taaf10 _ -> taaf10)
     1887   | Taaf_step (s1, s2, s3, taa) ->
     1888     (fun taaf10 _ -> Taaf_step (st1, s2, s3,
     1889       (taaf_append_taa s st1 s1 s2 taaf10 taa)))
     1890   | Taaf_step_jump (s2, s3, s4, taa) ->
     1891     (fun taaf10 _ -> Taaf_step_jump (st1, s3, s4,
     1892       (taaf_append_taa s st1 s2 s3 taaf10 taa)))) taaf1 __
     1893
Note: See TracChangeset for help on using the changeset viewer.