-
Notifications
You must be signed in to change notification settings - Fork 45
/
ecParsetree.ml
1312 lines (1084 loc) · 37 KB
/
ecParsetree.ml
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* -------------------------------------------------------------------- *)
open EcBigInt
open EcMaps
open EcSymbols
open EcLocation
open EcUtils
(* -------------------------------------------------------------------- *)
exception ParseError of EcLocation.t * string option
(* -------------------------------------------------------------------- *)
type side = [`Left | `Right]
type oside = side option
let side2str (side : side) =
match side with
| `Left -> "left"
| `Right -> "right"
let negside (side : side) : side =
match side with `Left -> `Right | `Right -> `Left
let sideif (side : side) xt xf =
match side with `Left -> xt | `Right -> xf
(* -------------------------------------------------------------------- *)
let qsymb_of_symb (x : symbol) : qsymbol = ([], x)
(* -------------------------------------------------------------------- *)
type psymbol = symbol located
type pqsymbol = qsymbol located
type pmsymbol = (psymbol * ((pmsymbol located) list) option) list
type pgamepath = (pmsymbol * psymbol) located
type osymbol_r = psymbol option
type osymbol = osymbol_r located
(* -------------------------------------------------------------------- *)
type pty_r =
| PTunivar
| PTtuple of pty list
| PTnamed of pqsymbol
| PTvar of psymbol
| PTapp of pqsymbol * pty list
| PTfun of pty * pty
| PTglob of pmsymbol located
and pty = pty_r located
type ptyannot_r =
| TVIunamed of pty list
| TVInamed of (psymbol * pty) list
and ptyannot = ptyannot_r located
type plpattern_r =
| LPSymbol of psymbol
| LPTuple of osymbol list
| LPRecord of (pqsymbol * psymbol) list
and plpattern = plpattern_r located
type ppattern =
| PPApp of (pqsymbol * ptyannot option) * osymbol list
type ptybinding = osymbol list * pty
and ptybindings = ptybinding list
and pexpr_r =
| PEcast of pexpr * pty (* type cast *)
| PEint of zint (* int. literal *)
| PEdecimal of (zint * (int * zint)) (* dec. literal *)
| PEident of pqsymbol * ptyannot option (* symbol *)
| PEapp of pexpr * pexpr list (* op. application *)
| PElet of plpattern * pexpr_wty * pexpr (* let binding *)
| PEtuple of pexpr list (* tuple constructor *)
| PEif of pexpr * pexpr * pexpr (* _ ? _ : _ *)
| PEmatch of pexpr * (ppattern * pexpr) list (* match *)
| PEforall of ptybindings * pexpr (* forall quant. *)
| PEexists of ptybindings * pexpr (* exists quant. *)
| PElambda of ptybindings * pexpr (* lambda abstraction *)
| PErecord of pexpr option * pexpr rfield list (* record *)
| PEproj of pexpr * pqsymbol (* projection *)
| PEproji of pexpr * int (* tuple projection *)
| PEscope of pqsymbol * pexpr (* scope selection *)
and pexpr = pexpr_r located
and pexpr_wty = pexpr * pty option
and 'a rfield = {
rf_name : pqsymbol;
rf_tvi : ptyannot option;
rf_value : 'a;
}
(* -------------------------------------------------------------------- *)
type plvalue_r =
| PLvSymbol of pqsymbol
| PLvTuple of plvalue list
| PLvProji of plvalue * int
| PLvMap of pqsymbol * ptyannot option * pexpr
and plvalue = plvalue_r located
type 'a funargs = {
fa_classical : 'a list;
fa_quantum : plvalue list;
}
type pinstr_r =
| PSident of psymbol
| PSasgn of plvalue * pexpr
| PSunitary of pqrref * [`Expr | `Fun] * [`Plain | `Xor of pqsymbol option] * pexpr
| PSmeasure of plvalue * pqrref * pexpr
| PSrnd of plvalue * pexpr
| PScall of plvalue option * pgamepath * pexpr funargs
| PSif of pscond * pscond list * pstmt
| PSwhile of pscond
| PSmatch of pexpr * psmatch
| PSassert of pexpr
and pqrref =
(plvalue * psymbol option) list located
and psmatch = [
| `Full of (ppattern * pstmt) list
| `If of (ppattern * pstmt) * pstmt option
]
and pscond = pexpr * pstmt
and pinstr = pinstr_r located
and pstmt = pinstr list
(* -------------------------------------------------------------------- *)
type is_local = [ `Local | `Global]
type locality = [`Declare | `Local | `Global]
(* -------------------------------------------------------------------- *)
type quantum = [`Quantum | `Classical]
(* -------------------------------------------------------------------- *)
type pmodule_type = pqsymbol
type ptyparams = (psymbol * pqsymbol list) list
type ptydname = (ptyparams * psymbol) located
type ptydecl = {
pty_name : psymbol;
pty_tyvars : ptyparams;
pty_body : ptydbody;
pty_locality : locality;
}
and ptydbody =
| PTYD_Abstract of pqsymbol list
| PTYD_Alias of pty
| PTYD_Record of precord
| PTYD_Datatype of pdatatype
and pdatatype = (psymbol * pty list) list
and precord = (psymbol * pty) list
(* -------------------------------------------------------------------- *)
type f_or_mod_ident =
| FM_FunOrVar of pgamepath
| FM_Mod of pmsymbol located
(* A memory restricition. *)
type pmod_restr_mem =
| PMempty
| PMquantum
| PMclassical
| PMvar of f_or_mod_ident
| PMunion of pmod_restr_mem * pmod_restr_mem
| PMinter of pmod_restr_mem * pmod_restr_mem
| PMdiff of pmod_restr_mem * pmod_restr_mem
(* -------------------------------------------------------------------- *)
type pmemory = psymbol
type phoarecmp = EcFol.hoarecmp
type glob_or_var =
| GVglob of pmsymbol located * pqsymbol list
| GVvar of pqsymbol
type pformula = pformula_r located
and pformula_r =
| PFhole
| PFcast of pformula * pty
| PFint of zint
| PFdecimal of (zint * (int * zint))
| PFtuple of pformula list
| PFident of pqsymbol * ptyannot option
| PFref of psymbol * pffilter list
| PFmem of psymbol
| PFside of pformula * symbol located
| PFapp of pformula * pformula list
| PFif of pformula * pformula * pformula
| PFmatch of pformula * (ppattern * pformula) list
| PFlet of plpattern * (pformula * pty option) * pformula
| PFforall of pgtybindings * pformula
| PFexists of pgtybindings * pformula
| PFlambda of ptybindings * pformula
| PFrecord of pformula option * pformula rfield list
| PFproj of pformula * pqsymbol
| PFproji of pformula * int
| PFglob of pmsymbol located
| PFeqveq of glob_or_var list * (pmsymbol pair) option
| PFeqf of pformula list
| PFlsless of pgamepath
| PFscope of pqsymbol * pformula
| PFhoareF of pformula * pgamepath * pformula
| PFehoareF of pformula * pgamepath * pformula
| PFequivF of pequiv_cond * (pgamepath * pgamepath) * pequiv_cond
| PFeagerF of pformula * (pstmt * pgamepath * pgamepath * pstmt) * pformula
| PFprob of pgamepath * (pformula list) * pmemory * pformula
| PFBDhoareF of pformula * pgamepath * pformula * phoarecmp * pformula
and pequiv_cond = pformula * pqe
and pqe = pqeq located list
and pqeq =
| QEQglobal
| QEQ1 of plvalue
| QEQ2 of plvalue * plvalue
and pmemtype_el = ([`Single|`Tuple] * (psymbol list)) located * pty
and pmemtype = pmemtype_el list
and pgtybinding = osymbol list * pgty
and pgtybindings = pgtybinding list
and pgscbinding = psymbol list * pty
and pgscbindings = pgscbinding list
and pgty =
| PGTY_Type of pty
| PGTY_ModTy of pmodule_type_restr
| PGTY_Mem of pmemtype option
and pffilter =
| PFRange of bool * pfrange list
| PFMatch of bool * psymbol * pformula
| PFMatchBuild of bool * psymbol list * pformula * pformula
| PFKeep of bool * bool * bool * pffilter_pattern
and pffilter_pattern = [
| `Pattern of pformula
| `VarSet of (pqsymbol * psymbol option) list
]
and pfrange = [
| `Single of pfindex
| `Range of pfindex option pair
]
and pfindex = [ `Index of int | `Match of pformula * int option]
(* if [pmty_mem] is [None], there are no user-supplied restriction, which is
different from the user supplying an empty restriction.
In the former case, we keep the restriction we obtain by type-checking,
while in the latter case, we replace the type-checking restriction by an
empty restriction. *)
and pmodule_type_restr =
{ pmty_pq : pqsymbol;
pmty_mem : pmod_restr option; }
(* -------------------------------------------------------------------- *)
(* qident optionally taken in a (implicit) module parameters. *)
and qident_inparam = { inp_in_params : bool;
inp_qident : pqsymbol; }
and poracles = qident_inparam list
and pmod_restr_el = {
pmre_name : psymbol;
pmre_orcls : poracles option; (* None means no restriction *)
}
and pmod_restr = {
pmr_mem : pmod_restr_mem;
pmr_procs : pmod_restr_el list;
}
(* -------------------------------------------------------------------- *)
and pmodule_sig =
| Pmty_struct of pmodule_sig_struct
and pmodule_sig_struct = {
pmsig_params : (psymbol * pmodule_type) list;
pmsig_body : pmodule_sig_struct_body;
pmsig_restr : pmod_restr option;
}
and pmodule_sig_struct_body = pmodule_sig_item list
and minclude_proc = [
| `MInclude of psymbol list
| `MExclude of psymbol list
]
and pmodule_sig_item = [
| `Include of pmodule_type * minclude_proc option * qident_inparam list option
| `FunctionDecl of pfunction_decl
]
and pvariable_decl = {
pvd_name : psymbol;
pvd_type : pty;
}
and fun_params =
{ fp_classical : (osymbol * pty) list; fp_quantum : (osymbol * pty) list }
and pfunction_decl = {
pfd_name : psymbol;
pfd_tyargs : fun_params;
pfd_tyresult : pty;
pfd_uses : pmod_restr_el;
}
(* -------------------------------------------------------------------- *)
and pmodule_def_or_decl = {
ptm_locality : locality;
ptm_def : [`Concrete of pmodule_def | `Abstract of pmodule_decl];
}
and pmodule_decl = {
ptm_name : psymbol;
ptm_modty : pmodule_type_restr;
}
and pmodule_def = {
ptm_header : pmodule_header;
ptm_body : pmodule_expr;
}
and pmodule_header =
| Pmh_ident of psymbol
| Pmh_params of (pmodule_header * pmodule_params) located
| Pmh_cast of pmodule_header * pqsymbol list
and pmodule_params = (psymbol * pmodule_type) list
and pmodule_expr_r =
| Pm_ident of pmsymbol
| Pm_struct of pstructure
and pmodule_expr = pmodule_expr_r located
and pstructure = pstructure_item located list
and pstructure_item =
| Pst_mod of (psymbol * pqsymbol list * pmodule_expr)
| Pst_var of (quantum * psymbol list * pty)
| Pst_fun of (pfunction_decl * pfunction_body)
| Pst_alias of (psymbol * pgamepath)
| Pst_include of (pmsymbol located * bool * minclude_proc option)
| Pst_import of (pmsymbol located) list
and pfunction_body = {
pfb_locals : pfunction_local list;
pfb_body : pstmt;
pfb_return : pexpr option;
}
and pfunction_local = {
pfl_quantum : quantum;
pfl_names : ([`Single | `Tuple] * (psymbol list)) located;
pfl_type : pty option;
pfl_init : pexpr option;
}
type pinterface = {
pi_name : psymbol;
pi_sig : pmodule_sig;
pi_locality : is_local;
}
(* -------------------------------------------------------------------- *)
let rec pf_ident ?(raw = false) f =
match unloc f with
| PFident ({ pl_desc = ([], x) }, _) -> Some x
| PFtuple [f] when not raw -> pf_ident ~raw f
| _ -> None
(* -------------------------------------------------------------------- *)
type ptyvardecls =
(psymbol * pqsymbol list) list
type pop_def =
| PO_abstr of pty
| PO_concr of pty * pformula
| PO_case of pty * pop_branch list
| PO_reft of pty * (psymbol * pformula)
and pop_branch = {
pop_patterns : pop_pattern list;
pop_body : pexpr;
}
and pop_pattern = {
pop_name : psymbol;
pop_pattern : ppattern;
}
type poperator = {
po_kind : [`Op | `Const];
po_name : psymbol;
po_aliases: psymbol list;
po_tags : psymbol list;
po_tyvars : ptyvardecls option;
po_args : ptybindings * ptybindings option;
po_def : pop_def;
po_ax : osymbol_r;
po_nosmt : bool;
po_locality : locality;
}
and pprocop = {
ppo_name : psymbol;
ppo_target : pgamepath;
ppo_locality : locality;
}
type ppred_def =
| PPabstr of pty list
| PPconcr of ptybindings * pformula
| PPind of ppind
and ppind_ctor = {
pic_name : psymbol;
pic_bds : pgtybindings;
pic_spec : pformula list;
}
and ppind = ptybindings * (ppind_ctor list)
type ppredicate = {
pp_name : psymbol;
pp_tyvars : (psymbol * pqsymbol list) list option;
pp_def : ppred_def;
pp_locality : locality;
}
(* -------------------------------------------------------------------- *)
type pnotation = {
nt_name : psymbol;
nt_tv : ptyvardecls option;
nt_bd : (psymbol * pty) list;
nt_args : (psymbol * (psymbol list * pty option)) list;
nt_codom : pty;
nt_body : pexpr;
nt_local : is_local;
}
(* -------------------------------------------------------------------- *)
type abrvopt = [`Printing]
type abrvopts = (bool * abrvopt) list
type pabbrev = {
ab_name : psymbol;
ab_tv : ptyvardecls option;
ab_args : ptybindings;
ab_def : pty * pexpr;
ab_opts : abrvopts;
ab_local : is_local;
}
(* -------------------------------------------------------------------- *)
type 'a ppt_head =
| FPNamed of pqsymbol * ptyannot option
| FPCut of 'a
type ppt_arg =
| EA_none
| EA_form of pformula
| EA_mem of pmemory
| EA_mod of pmsymbol located
| EA_proof of (pformula option) gppterm
and 'a gppterm = {
fp_mode : [`Implicit | `Explicit];
fp_head : 'a ppt_head;
fp_args : ppt_arg located list
}
type ppterm = (pformula option) gppterm
type pcutdef = {
ptcd_name : pqsymbol;
ptcd_tys : ptyannot option;
ptcd_args : ppt_arg located list;
}
(* λ mem → formula *)
type pmpred_args = (osymbol * pformula) list
(* -------------------------------------------------------------------- *)
type preduction = {
pbeta : bool; (* β-reduction *)
pdelta : pqsymbol list option; (* definition unfolding *)
pzeta : bool; (* let-reduction *)
piota : bool; (* case/if-reduction *)
peta : bool; (* η-reduction *)
plogic : bool; (* logical simplification *)
pmodpath : bool; (* modpath normalization *)
puser : bool; (* user reduction *)
}
(* -------------------------------------------------------------------- *)
type cp_match = [ `If | `While | `Assign | `Sample | `Call ]
type cp_base = [ `ByPos of int | `ByMatch of int option * cp_match ]
type codepos1 = int * cp_base
type codepos = (codepos1 * int) list * codepos1
type docodepos1 = codepos1 doption option
(* -------------------------------------------------------------------- *)
type swap_kind =
| SKbase of int * int * int
| SKmove of int
| SKmovei of int * int
| SKmoveinter of int * int * int
type interleave_info = oside * (int * int) * ((int * int) list) * int
type pipattern =
| PtAny
| PtAsgn of psymbol list
| PtIf of pspattern * [`NoElse | `MaybeElse | `Else of pspattern]
| PtWhile of pspattern
and pspattern = unit
type call_info =
| CI_spec of (pformula * pformula)
| CI_inv of pformula
| CI_upto of (pformula * pformula * pformula option)
type p_app_xt_info =
| PAppNone
| PAppSingle of pformula
| PAppMult of (pformula option) tuple5
type ('a, 'b, 'c) rnd_tac_info =
| PNoRndParams
| PSingleRndParam of 'c
| PTwoRndParams of 'a * 'a
| PMultRndParams of ('a tuple5) * 'b
type rnd_tac_info_f =
(pformula, pformula option, pformula) rnd_tac_info
type semrndpos = (bool * codepos1) doption
type tac_dir = Backs | Fwds
type pfel_spec_preds = (pgamepath * pformula) list
(* -------------------------------------------------------------------- *)
type pim_repeat_kind =
| IM_R_Repeat of int option pair
| IM_R_May of int option
type pim_repeat =
bool * pim_repeat_kind
type anchor =
| Without_anchor
| With_anchor
type pim_regexp =
| IM_Any
| IM_Parens of pim_regexp
| IM_Assign
| IM_Sample
| IM_Call
| IM_If of pim_block option * pim_block option
| IM_While of pim_block option
| IM_Named of psymbol * pim_regexp option
| IM_Repeat of pim_repeat * pim_regexp
| IM_Seq of pim_regexp list
| IM_Choice of pim_regexp list
and pim_block = anchor pair * pim_regexp
(* -------------------------------------------------------------------- *)
type trans_kind =
| TKfun of pgamepath
| TKstmt of side * pstmt
| TKparsedStmt of side * pim_block * pstmt
type trans_formula =
| TFform of pformula * pformula * pformula * pformula
| TFeq
type trans_info =
trans_kind * trans_formula
(* -------------------------------------------------------------------- *)
type eager_info =
| LE_done of psymbol
| LE_todo of psymbol * pstmt * pstmt * pformula * pformula
(* -------------------------------------------------------------------- *)
type bdh_split =
| BDH_split_bop of pformula * pformula * pformula option
| BDH_split_or_case of pformula * pformula * pformula
| BDH_split_not of pformula option * pformula
(* -------------------------------------------------------------------- *)
type fun_info = [
| `Def
| `Code
| `Abs of pformula
| `Upto of pformula * pformula * pformula option
]
(* -------------------------------------------------------------------- *)
type app_info =
oside * tac_dir * codepos1 doption *
(pformula * pqe option, pformula) doption_ * p_app_xt_info
(* -------------------------------------------------------------------- *)
type pcond_info = [
| `Head of oside
| `Seq of oside * codepos1 option pair * pformula
| `SeqOne of side * codepos1 option * pformula * pformula
]
(* -------------------------------------------------------------------- *)
type while_info = {
wh_inv : pformula;
wh_vrnt : pformula option;
wh_bds : [`Bd of pformula pair] option;
}
(* -------------------------------------------------------------------- *)
type async_while_info = {
asw_test : (pexpr * pformula) pair;
asw_pred : pformula * pformula;
asw_inv : pformula;
}
(* -------------------------------------------------------------------- *)
type inlineopt = [`UseTuple of bool] option
type inline_pat1 = [
| `InlineXpath of pgamepath
| `InlinePat of pmsymbol located * (psymbol list * psymbol option)
| `InlineAll
]
type inline_pat = ([ `DIFF | `UNION] * inline_pat1) list
type inline_info = [
| `ByName of oside * inlineopt * (inline_pat * int list option)
| `CodePos of (oside * inlineopt * codepos)
(* | `All of oside * inlineopt *)
]
(* -------------------------------------------------------------------- *)
type outline_kind =
| OKstmt of pstmt
| OKproc of pgamepath * pexpr option
type outline_info = {
outline_side: side;
outline_start: codepos1;
outline_end: codepos1;
outline_kind: outline_kind;
}
(* -------------------------------------------------------------------- *)
type fel_info = {
pfel_cntr : pformula;
pfel_asg : pformula;
pfel_q : pformula;
pfel_event : pformula;
pfel_specs : pfel_spec_preds;
pfel_inv : pformula option;
}
(* -------------------------------------------------------------------- *)
type deno_ppterm = (pformula option pair) gppterm
type conseq_info =
| CQI_bd of phoarecmp option * pformula
type conseq_pec = pformula option * pqe option
type conseq_ppterm = (conseq_pec pair * (conseq_info) option) gppterm
(* -------------------------------------------------------------------- *)
type sim_info = {
sim_pos : codepos1 pair option;
sim_hint : (pgamepath option pair * pformula) list * pformula option;
sim_eqs : pformula option
}
(* -------------------------------------------------------------------- *)
type rw_eqv_info = {
rw_eqv_side : side;
rw_eqv_dir : [`LtoR | `RtoL];
rw_eqv_pos : codepos1;
rw_eqv_lemma : ppterm;
rw_eqv_proc : (pexpr list located * pexpr option) option;
}
(* -------------------------------------------------------------------- *)
type pcqoption = [ `Frame ]
type pcqoptions = (bool * pcqoption) list
(* -------------------------------------------------------------------- *)
type crushmode = { cm_simplify : bool; cm_solve : bool; }
(* -------------------------------------------------------------------- *)
type matchmode = [
| `DSided of [ `Eq | `ConstrSynced ]
| `SSided of side
]
(* -------------------------------------------------------------------- *)
type phltactic =
| Pskip
| Prepl_stmt of trans_info
| Pfun of fun_info
| Papp of app_info
| Pwp of docodepos1
| Psp of docodepos1
| Pwhile of (oside * while_info)
| Pasyncwhile of async_while_info
| Pfission of (oside * codepos * (int * (int * int)))
| Pfusion of (oside * codepos * (int * (int * int)))
| Punroll of (oside * codepos * bool)
| Psplitwhile of (pexpr * oside * codepos)
| Pcall of oside * call_info gppterm
| Pcallconcave of (pformula * call_info gppterm)
| Prcond of (oside * bool * codepos1)
| Prmatch of (oside * symbol * codepos1)
| Pcond of pcond_info
| Pmatch of matchmode
| Pswap of ((oside * swap_kind) located list)
| Pcfold of (oside * codepos * int option)
| Pinline of inline_info
| Poutline of outline_info
| Pinterleave of interleave_info located
| Pkill of (oside * codepos * int option)
| Pasgncase of (oside * codepos)
| Prnd of oside * semrndpos option * rnd_tac_info_f
| Prndsem of bool * oside * codepos1
| Punitary of oside
| Pqinit of oside
| Pmeasure of oside
| Palias of (oside * codepos * osymbol_r)
| Pweakmem of (oside * psymbol * (osymbol * pty) list)
| Pset of (oside * codepos * bool * psymbol * pexpr)
| Pconseq of (pcqoptions * (conseq_ppterm option tuple3))
| Pconseqauto of crushmode
| Pconcave of (pformula option tuple2 gppterm * pformula)
| Phrex_elim
| Phrex_intro of (pformula list * bool)
| Phecall of (oside * (pqsymbol * ptyannot option * pformula list))
| Pexfalso
| Pbydeno of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option))
| PPr of (pformula * pformula) option
| Pbyupto
| Pfel of (codepos1 * fel_info)
| Phoare
| Pprbounded
| Psim of crushmode option* sim_info
| Ptrans_stmt of trans_info
| Prw_equiv of rw_eqv_info
| Psymmetry
| Pbdhoare_split of bdh_split
(* Eager *)
| Peager_seq of (eager_info * codepos1 pair * pformula)
| Peager_if
| Peager_while of (eager_info)
| Peager_fun_def
| Peager_fun_abs of (eager_info * pformula)
| Peager_call of (call_info gppterm)
| Peager of (eager_info * pformula)
(* Relation between logic *)
| Pbd_equiv of (side * pformula * pformula)
(* Automation *)
| Pauto
| Plossless
(* -------------------------------------------------------------------- *)
type include_exclude = [ `Include | `Exclude ]
type pdbmap1 = {
pht_flag : include_exclude;
pht_kind : [ `Theory | `Lemma ];
pht_name : pqsymbol;
}
and pdbhint = pdbmap1 list
(* -------------------------------------------------------------------- *)
type pprover_list = {
pp_use_only : string located list;
pp_add_rm : (include_exclude * string located) list;
}
let empty_pprover_list = {
pp_use_only = [];
pp_add_rm = [];
}
type pprover_infos = {
pprov_max : int option;
pprov_timeout : int option;
pprov_cpufactor : int option;
pprov_names : pprover_list option;
pprov_quorum : int option;
pprov_verbose : int option option;
pprov_version : [`Lazy | `Full] option;
plem_all : bool option;
plem_max : int option option;
plem_iterate : bool option;
plem_wanted : pdbhint option;
plem_unwanted : pdbhint option;
plem_dumpin : string located option;
plem_selected : bool option;
psmt_debug : bool option;
}
let empty_pprover = {
pprov_max = None;
pprov_timeout = None;
pprov_cpufactor = None;
pprov_names = None;
pprov_quorum = None;
pprov_verbose = None;
pprov_version = None;
plem_all = None;
plem_max = None;
plem_iterate = None;
plem_wanted = None;
plem_unwanted = None;
plem_dumpin = None;
plem_selected = None;
psmt_debug = None;
}
(* -------------------------------------------------------------------- *)
type trepeat = [`All | `Maybe] * int option
type tfocus1 = (int option) pair
type tfocus = (tfocus1 list option) pair
type rwarg = (tfocus located) option * rwarg1 located
and rwarg1 =
| RWSimpl of [`Default | `Variant]
| RWDelta of (rwoptions * pformula)
| RWRw of (rwoptions * (rwside * ppterm) list)
| RWPr of (psymbol * pformula option)
| RWDone of [`Default | `Variant] option
| RWSmt of (bool * pprover_infos)
| RWApp of ppterm
| RWTactic of rwtactic
and rwoptions = rwside * trepeat option * rwocc * pformula option
and rwside = [`LtoR | `RtoL]
and rwocc = rwocci option
and rwocci = [`Inclusive of Sint.t | `Exclusive of Sint.t | `All]
and rwtactic = [`Ring | `Field]
(* -------------------------------------------------------------------- *)
let norm_rwocci (x : rwocci) =
match x with
| `Inclusive x -> Some (`Inclusive, x)
| `Exclusive x -> Some (`Exclusive, x)
| `All -> None
let norm_rwocc (x : rwocc) =
obind norm_rwocci x
(* -------------------------------------------------------------------- *)
type intropattern1 =
| IPCore of ipcore
| IPDup
| IPCase of (icasemode * intropattern list)
| IPView of ppterm
| IPRw of (rwocc * rwside * (int option) option)
| IPDelta of ((rwside * rwocc) * pformula)
| IPSubst of (rwside * (int option) option)
| IPClear of psymbol list
| IPDone of [`Default | `Variant] option
| IPSmt of (bool * pprover_infos)
| IPSubstTop of (int option * [`LtoR | `RtoL] option)
| IPSimplify of [`Default | `Variant]
| IPCrush of crushmode
| IPBreak
and intropattern = (intropattern1 located) list
and ipcore = [
| `Revert
| `Clear
| `Named of string
| `Anonymous of (int option) option
]
and icasemode =
[`One | `Full of (bool * bool) * bool * icasemode_full option]
and icasemode_full =
[`AtMost of int | `AsMuch]
type genpattern =
[ `ProofTerm of ppterm
| `Form of (rwocc * pformula)
| `LetIn of psymbol ]
type prevert = {
pr_clear : psymbol list;
pr_genp : genpattern list;
}
type prevertv = {
pr_rev : prevert;
pr_view : ppterm list;
}
let prevert0 = { pr_clear = []; pr_genp = []; }
let prevertv0 = { pr_rev = prevert0; pr_view = []; }
(* -------------------------------------------------------------------- *)
type ppgoption = [
| `Delta of [`Case | `Split] option
| `Split
| `Solve
| `Subst
| `Disjunctive
]
type ppgoptions = (bool * ppgoption) list
(* -------------------------------------------------------------------- *)
type pcaseoption = [ `Ambient ]
type pcaseoptions = (bool * pcaseoption) list
(* -------------------------------------------------------------------- *)
type apply_info = [
| `ApplyIn of ppterm * psymbol
| `Apply of ppterm list * [`Apply|`Exact|`Alpha]
| `Top of [`Apply|`Exact|`Alpha]
| `Alpha of ppterm
| `ExactType of pqsymbol
]
(* -------------------------------------------------------------------- *)
type pgenhave = psymbol * intropattern option * psymbol list * pformula
(* -------------------------------------------------------------------- *)
type logtactic =
| Preflexivity
| Passumption
| Psmt of pprover_infos
| Psplit
| Pfield of psymbol list
| Pring of psymbol list
| Palg_norm
| Pexists of ppt_arg located list
| Pleft
| Pright
| Ptrivial
| Pcongr
| Pelim of (prevert * pqsymbol option)
| Papply of (apply_info * prevert option)
| Pcut of pcut
| Pcutdef of (intropattern * pcutdef)
| Pmove of prevertv
| Pclear of psymbol list
| Prewrite of (rwarg list * osymbol_r)
| Prwnormal of pformula * pqsymbol list
| Psubst of pformula list
| Psimplify of preduction
| Pcbv of preduction
| Pchange of pformula
| Ppose of (psymbol * ptybinding list * rwocc * pformula)
| Pmemory of psymbol
| Pgenhave of pgenhave
| Pwlog of (psymbol list * bool * pformula)
(* -------------------------------------------------------------------- *)
and ptactic_core_r =