1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
(*
** ATS-extsolve:
** For solving ATS-constraints
** with external SMT-solvers
*)
(* ****** ****** *)
(*
** Author: Hongwei Xi
** Authoremail: gmhwxiATgmailDOTcom
** Start time: May, 2015
*)
(* ****** ****** *)
//
#define
ATS_PACKNAME
"PATSOLVE_COMMARG"
//
(* ****** ****** *)
datatype
commarg =
| CAhelp of (string)
| CAgitem of (string)
| CAinput of (string)
| CAoutput of (string)
| CAscript of (string)
| CAargend of ((*void*))
// end of [commarg]
(* ****** ****** *)
//
typedef
commarglst = List0 (commarg)
vtypedef
commarglst_vt = List0_vt (commarg)
//
(* ****** ****** *)
//
fun
fprint_commarg
(out: FILEref, ca: commarg): void
//
overload fprint with fprint_commarg
//
(* ****** ****** *)
//
fun
patsolve_cmdline
{n:nat}
(argc: int(n), argv: !argv(n)): commarglst_vt
//
(* ****** ****** *)
//
fun
patsolve_commarglst(arglst: commarglst_vt): void
//
(* ****** ****** *)
(* end of [patsolve_commarg.sats] *)
|
