-
Notifications
You must be signed in to change notification settings - Fork 4
/
athena.grm
executable file
·1788 lines (1485 loc) · 114 KB
/
athena.grm
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
(*==================================================
Athena's Yacc grammar.
===================================================*)
structure A = AbstractSyntax
structure N = Names
structure S = Symbol
structure MS = ModSymbol
type pos = int * int
fun getPos((l,p)) = {line=l,pos=p,file=(!Paths.current_file)}
%%
%term EOF | PICK_ANY | PICK_WITNESS | PICK_WITNESSES | CHECK | DCHECK | ELSE | THEN | LOGICAL_AND | LOGICAL_OR | OP | EXPAND_INPUT |
PRIVATE_ID of string | PRIVATE | OPEN_MODULE | EXTEND_MODULE | ANY_ID of string | RE_STAR | RE_PLUS | RE_OPTIONAL | RE_LIT | RE_REP | RE_RANGE |
ID of string | STRING of int list | SOME_FUNCTION | SOME_METHOD | EXIT_ATHENA | FROM | FOR | START_LOAD | END_LOAD | TRANSFORM_OUTPUT |
CHARACTER of int | LOAD_FILE | DIF_ELSE | NAME | SOME_TERM | COLON | OVERLOAD | OVERLOAD_INV | MODULE | DEFINE_STAR | DEFINE_MEMOIZED |
SOME_ATOM | SOME_PROP | QMARK | EXCL_MARK | QUOTE_WORD |QUOTE_SYMBOL | EXPAND_NEXT_PROOF | LEFT_CURLY_BRACE | RIGHT_CURLY_BRACE |
BACK_QUOTE_SYMBOL | LETREC | DLETREC | SPLIT_PAT | BY | PRINT_STACK_TRACE | SEMI_COLON | CONCLUDE | DOUBLE_LEFT_CURLY_BRACE | DOUBLE_RIGHT_CURLY_BRACE |
LPAREN | RPAREN | COMMA | CLAIM | LEFT_BRACKET | RIGHT_BRACKET | SET | ARROW | WILDCARD | SOME_CHAR |
FUNCTION | METHOD | MATCH | LET | LET_UPPER | DLET | TRY | DTRY | APPLY_METHOD | SOME_VAR | SEQ | DSEQ | SOME_VECTOR | MAP_BEGIN | MAP_END |
EQUAL_SIGN | ASSERT | ASSERT_CLOSE | ASSUME | ASSUME_LET | SUPPOSE_ABSURD | SUPPOSE_ABSURD_LET | ON | PROVE |
DMATCH | EITHER | ABSURD | MP | DN | EQUIV | LEFT_IFF | RIGHT_IFF | BOTH | ASGN | BY_CASES | FUN |
META_ID | SOME_SYMBOL | LEFT_AND | RIGHT_AND | CD | VAL_OF | VAR | FUN_ARROW | DATATYPE | DATATYPES | DEFINE_SORT |
SOME_LIST | SOME_CELL | SOME_SUB | SOME_TABLE | SOME_MAP | DEFINE | POUND | STRUCTURE | STRUCTURES | DOMAIN | WHERE | PROVIDED |
DECLARE | DDECLARE | DIRECTIVE_PREFIX | EGEN | BEGIN | WHILE | CLEAR | THE | DEFINE_SYMBOL | DOMAINS | OVER |
EGEN_UNIQUE | LEIBNIZ | EQ_REFLEX | SOME_QUANT | USPEC | FETCH | RETRACT | DEFINE_FUN | ADD_DEMON | ADD_DEMONS |
SOME_PROP_CON | UNEQUAL_TERMS | INDUCTION | STRUCTURE_CASES | LIST | CELL | RULE | GEN_OVER | WITH_PREDICATE | WITH_KEYS |
WITH_WITNESS | MAKE_CELL | REF | USE_TERM_PARSER | USE_PROP_PARSER | END | SPECIALIZE | SET_FLAG |
EX_GENERALIZE | DATATYPE_CASES | DATATYPE_CASES_ON_TERM | SUBSORT | SUBSORTS | VECTOR_INIT | VECTOR_SUB | VECTOR_SET |
SET_CNF_CONVERTER | GET_CNF_CONVERTER | ANY_PAT | SET_PRECEDENCE | LEFT_ASSOC | RIGHT_ASSOC | BIN_OP | ADD_PATH
%nonterm input_stream of A.user_input list
| input_list of A.user_input list
| module of A.module_entry
| moduleExtension of A.module_entry
| user_input of A.user_input
| core_user_input of A.user_input
| directive of A.directive
| ath_structure of A.absyn_structure
| ath_datatype of A.absyn_structure
| infix_ath_datatype of A.absyn_structure
| infix_ath_structure of A.absyn_structure
| ath_structures of A.absyn_structure list
| ath_datatypes of A.absyn_structure list
| infix_ath_datatypes of A.absyn_structure list
| ath_struc_clause of A.absyn_structure
| infix_ath_struc_clause of A.absyn_structure
| rec_ath_struc_clause of A.absyn_structure
| one_or_more_rec_ath_struc_clauses of A.absyn_structure list
| one_or_more_rec_ath_datatype_clauses of A.absyn_structure list
| ath_structure_profile of A.absyn_structure_profile
| ath_domain of A.absyn_domain
| ath_domains of A.absyn_domain list
| subsort of A.mod_symbol * A.pos * A.mod_symbol * A.pos
| subsorts of (A.mod_symbol * A.pos) list * (A.mod_symbol * A.pos)
| ath_constant_sym of A.absyn_fsym list
| ath_fsym of A.absyn_fsym list
| ath_structure_constructor of A.absyn_structure_constructor
| one_or_more_ath_structure_constructors of A.absyn_structure_constructor list
| infix_one_or_more_ath_structure_constructors of A.absyn_structure_constructor list
| one_or_more_type_vars of A.param list
| athena_object_type of A.absyn_term
| user_sort of A.absyn_term
| one_or_more_user_sorts of A.absyn_term list
| selector_tagged_athena_object_type of (A.param option * A.absyn_term)
| one_or_more_athena_object_types of A.absyn_term list
| one_or_more_selector_tagged_athena_object_types of (A.param option * A.absyn_term) list
| athena_object_type_list of A.absyn_term list
| selector_tagged_athena_object_type_list of (A.param option * A.absyn_term) list
| param of A.param
| param_no_dots of A.param
| map_binding of A.phrase
| map_bindings of A.phrase list
| input_transformer_declaration of A.expression list
| possibly_wildcard_param of A.possibly_wildcard_param
| possibly_wildcard_param_no_dots of A.possibly_wildcard_param
| possibly_wildcard_param_list of A.possibly_wildcard_param list
| possibly_wildcard_param_list_no_dots of A.possibly_wildcard_param list
| possibly_typed_param of A.possibly_typed_param
| possibly_typed_param_no_dots of A.possibly_typed_param
| possibly_typed_params of A.possibly_typed_param list
| possibly_typed_params_no_dots of A.possibly_typed_param list
| param_option of S.symbol option
| param_option_no_dots of S.symbol option
| params of A.param list
| one_or_more_params_maybe_with_reps of A.param list
| one_or_more_params_maybe_with_reps_no_dots of A.param list
| one_or_more_params of A.param list
| one_or_more_params_no_dots of A.param list
| one_or_more_comma_separated_params of A.param list
| comma_separated_possible_obtype_params of A.param list
| possible_obtype_params of A.param list
| bracket_enclosed_possible_obtype_params of A.param list
| one_or_more_ids of string list
| expression of A.expression
| any_id of string
| one_or_more_expressions of A.expression list
| comma_separated_expression_list of A.expression list
| comma_separated_phrase_list of A.phrase list
| opt_comma_separated_phrase_list of A.phrase list
| one_or_more_phrases of A.phrase list
| deduction of A.deduction
| inference of A.deduction
| possibly_named_inference of A.optBinding
| inference_list of A.optBinding list
| inference_block of A.deduction
| case_clause of A.case_clause
| case_clauses of A.case_clause list
| deductions of A.deduction list
| one_or_more_separated_deductions of A.deduction list
| one_or_more_separated_expressions of A.expression list
| one_or_more_deductions of A.deduction list
| phrase of A.phrase
| phrases of A.phrase list
| infix_def_block of A.possibly_typed_param * A.expression
| infix_def_blocks of (A.possibly_typed_param * A.expression) list
| def_block of A.possibly_typed_param * A.expression
| def_blocks of (A.possibly_typed_param * A.expression) list
| definitions of (A.possibly_typed_param * A.expression) list
| pattern of A.pattern
| struc_pattern of A.pattern
| patterns of A.pattern list
| struc_patterns of A.pattern list
| check_clause of A.check_clause
| infix_check_clause of A.check_clause
| infix_check_clauses of A.check_clause list
| check_clauses of A.check_clause list
| dcheck_clause of A.dcheck_clause
| infix_dcheck_clause of A.dcheck_clause
| infix_dcheck_clauses of A.dcheck_clause list
| dcheck_clauses of A.dcheck_clause list
| condition of A.condition
| one_or_more_patterns of A.pattern list
| two_or_more_patterns of A.pattern list
| match_clause of A.match_clause
| match_clauses of A.match_clause list
| dmatch_clause of A.dmatch_clause
| infix_dmatch_clause of A.dmatch_clause
| infix_match_clause of A.match_clause
| sep_infix_match_clause of A.match_clause
| sep_infix_dmatch_clause of A.dmatch_clause
| sep_infix_match_clauses of A.match_clause list
| sep_infix_dmatch_clauses of A.dmatch_clause list
| infix_match_clauses of A.match_clause list
| dmatch_clauses of A.dmatch_clause list
| infix_dmatch_clauses of A.dmatch_clause list
| binding of A.binding
| binding_assignment of A.binding
| bindings of A.binding list
| semicolon_separated_bindings of A.binding list
| semicolon_separated_phrases of A.phrase list
| semicolon_separated_deductions of A.deduction list
| semicolon_separated_expressions of A.expression list
| assignment of A.binding
| assignments of A.binding list
| symbol_definition of A.absyn_symbol_definition
| athena_var of AthTermVar.ath_term_var
| ath_var of A.expression
| athena_meta_id of A.expression
| one_or_more_athena_vars of AthTermVar.ath_term_var list
| declaration_prec_assoc of {overload_sym:A.param option,precedence:int option,assoc:bool option,input_transformer: A.expression list option}
| sb_declaration_prec_assoc of {overload_sym:A.param option,precedence:int option,assoc:bool option,input_transformer: A.expression list option}
| associativity of bool
| one_mod_symbol of A.mod_symbol * A.pos
| one_or_more_mod_symbols of (A.mod_symbol * A.pos) list
| one_or_more_mod_symbols_infix of (A.mod_symbol * A.pos) list
| single_logical_or of unit
| phrase_pair of (A.phrase * A.phrase * A.pos * A.pos * A.pos)
| phrase_pair_list of (A.phrase * A.phrase * A.pos * A.pos * A.pos) list
| lcb of unit | rcb of unit
| param_asgn_exp_list of (A.param * A.expression) list
%pos int * int
%verbose
%start input_stream
%eop EOF
%noshift EOF
%name Athena
%keyword ASSUME SUPPOSE_ABSURD MATCH DMATCH EITHER FUNCTION METHOD
%prefer LPAREN
%value ID ("bogus")
%%
input_stream: input_list (input_list)
single_logical_or: ID (let val res = if ID = "|" then () else raise
A.SyntaxError("the character | was expected here",SOME(getPos IDleft))
in res end)
input_list: user_input ([user_input])
| user_input input_list (user_input::input_list)
user_input : core_user_input (core_user_input)
| core_user_input SEMI_COLON (core_user_input)
core_user_input: ath_structure (A.structureInput(ath_structure))
| ath_datatype (A.structureInput(ath_datatype))
| infix_ath_datatype (A.structureInput(infix_ath_datatype))
| ath_datatypes (A.structuresInput(ath_datatypes))
| infix_ath_datatypes (A.structuresInput(infix_ath_datatypes))
| ath_structures (A.structuresInput(ath_structures))
| module (A.moduleInput(module))
| moduleExtension (A.moduleExtension(moduleExtension))
| ath_domain (A.domainInput(ath_domain))
| ath_domains (A.domainsInput(ath_domains))
| subsort (A.subSortDeclaration(subsort))
| subsorts (A.subSortsDeclaration(subsorts))
| ath_fsym (A.functionSymbolInput(ath_fsym))
| ath_constant_sym (A.constantSymbolInput(ath_constant_sym))
| phrase (A.phraseInput(phrase))
| symbol_definition (A.symbolDefinitionInput(symbol_definition))
| directive (A.direcInput(directive))
directive: LPAREN LOAD_FILE expression RPAREN
(A.loadFile(expression,getPos(LOAD_FILEleft)))
| LPAREN ADD_PATH expression RPAREN
(A.addPath(expression, getPos(ADD_PATHleft)))
| LPAREN EXPAND_INPUT LPAREN one_or_more_phrases RPAREN phrase RPAREN
(A.expandInput(one_or_more_phrases,phrase,getPos(EXPAND_INPUTleft)))
| EXPAND_INPUT comma_separated_phrase_list phrase
(A.expandInput(comma_separated_phrase_list,phrase,getPos(EXPAND_INPUTleft)))
| LPAREN TRANSFORM_OUTPUT phrase phrase RPAREN
(A.transformOutput(phrase1,phrase2,{first_arg_pos=getPos(phrase1left),second_arg_pos=getPos(phrase2left),
overall_pos=getPos(LPARENleft)}))
| TRANSFORM_OUTPUT phrase phrase
(A.transformOutput(phrase1,phrase2,{first_arg_pos=getPos(phrase1left),second_arg_pos=getPos(phrase2left),
overall_pos=getPos(TRANSFORM_OUTPUTleft)}))
| LPAREN OVERLOAD phrase phrase RPAREN (A.overload([(phrase1,phrase2,getPos(LPARENleft),
getPos(phrase1left),getPos(phrase2left))],getPos(OVERLOADleft),{inverted=false}))
| LPAREN OVERLOAD_INV phrase phrase RPAREN (A.overload([(phrase1,phrase2,getPos(LPARENleft),
getPos(phrase1left),getPos(phrase2left))],getPos(OVERLOAD_INVleft),{inverted=true}))
| OVERLOAD phrase phrase (A.overload([(phrase1,phrase2,getPos(OVERLOADleft),
getPos(phrase1left),getPos(phrase2left))],getPos(OVERLOADleft),{inverted=false}))
| OVERLOAD_INV phrase phrase (A.overload([(phrase1,phrase2,getPos(OVERLOAD_INVleft),
getPos(phrase1left),getPos(phrase2left))],getPos(OVERLOAD_INVleft),{inverted=true}))
| LPAREN OVERLOAD phrase_pair_list RPAREN (A.overload(phrase_pair_list,getPos(OVERLOADleft),{inverted=false}))
| LPAREN OVERLOAD_INV phrase_pair_list RPAREN (A.overload(phrase_pair_list,getPos(OVERLOAD_INVleft),{inverted=true}))
| OVERLOAD phrase_pair_list (A.overload(phrase_pair_list,getPos(OVERLOADleft),{inverted=false}))
| LPAREN ADD_DEMON expression RPAREN (A.addDemon(expression,getPos(ADD_DEMONleft)))
| LPAREN ADD_DEMONS one_or_more_expressions RPAREN (A.addDemons(one_or_more_expressions,getPos(ADD_DEMONSleft)))
| ADD_DEMON expression (A.addDemon(expression,getPos(ADD_DEMONleft)))
| LPAREN SET_FLAG param STRING RPAREN
(let val str = String.implode(map (Char.chr) STRING)
in
A.setFlag(param,(str,getPos(STRINGleft)))
end)
| SET_FLAG param STRING
(let val str = String.implode(map (Char.chr) STRING)
in
A.setFlag(param,(str,getPos(STRINGleft)))
end)
| LOAD_FILE expression
(A.loadFile(expression,getPos(LOAD_FILEleft)))
| ADD_PATH expression
(A.addPath(expression, getPos(ADD_PATHleft)))
| LPAREN USE_TERM_PARSER param RPAREN (A.useTermParser({tp_name=param,file=(!Paths.current_file)}))
| LPAREN USE_PROP_PARSER param RPAREN (A.usePropParser({pp_name=param,file=(!Paths.current_file)}))
| LPAREN EXPAND_NEXT_PROOF RPAREN (A.expandNextProof(getPos(LPARENleft)))
| EXPAND_NEXT_PROOF (A.expandNextProof(getPos(EXPAND_NEXT_PROOFleft)))
| LPAREN EXIT_ATHENA RPAREN (A.exitAthena(getPos(LPARENleft)))
| EXIT_ATHENA (A.exitAthena(getPos(EXIT_ATHENAleft)))
| LPAREN PRINT_STACK_TRACE RPAREN (A.printStackTrace(getPos(PRINT_STACK_TRACEleft)))
| LPAREN SET_PRECEDENCE one_mod_symbol expression RPAREN (A.setPrecedence([one_mod_symbol],expression))
| LPAREN SET_PRECEDENCE LPAREN one_or_more_mod_symbols RPAREN expression RPAREN (A.setPrecedence(one_or_more_mod_symbols,expression))
| SET_PRECEDENCE one_mod_symbol expression (A.setPrecedence([one_mod_symbol],expression))
| SET_PRECEDENCE LPAREN one_or_more_mod_symbols RPAREN expression (A.setPrecedence(one_or_more_mod_symbols,expression))
| LPAREN LEFT_ASSOC one_or_more_mod_symbols RPAREN (A.setAssoc(one_or_more_mod_symbols,true))
| LEFT_ASSOC one_or_more_mod_symbols (A.setAssoc(one_or_more_mod_symbols,true))
| LPAREN RIGHT_ASSOC one_or_more_mod_symbols RPAREN (A.setAssoc(one_or_more_mod_symbols,false))
| RIGHT_ASSOC one_or_more_mod_symbols (A.setAssoc(one_or_more_mod_symbols,false))
| PRINT_STACK_TRACE (A.printStackTrace(getPos(PRINT_STACK_TRACEleft)))
| LPAREN OPEN_MODULE one_mod_symbol RPAREN (A.openModule([one_mod_symbol]))
| LPAREN OPEN_MODULE one_or_more_mod_symbols RPAREN (A.openModule(one_or_more_mod_symbols))
| OPEN_MODULE one_or_more_mod_symbols_infix (A.openModule(one_or_more_mod_symbols_infix))
| LPAREN ASSERT one_or_more_expressions RPAREN
(A.assert(one_or_more_expressions))
| LPAREN ASSERT_CLOSE one_or_more_expressions RPAREN
(A.assertClose(one_or_more_expressions))
| LPAREN ASSERT_CLOSE param_asgn_exp_list RPAREN
(A.assertCloseAsgn(param_asgn_exp_list))
| LPAREN ASSERT param ASGN expression RPAREN
(A.assertAsgn(param,expression))
| ASSERT param ASGN expression
(A.assertAsgn(param,expression))
| ASSERT_CLOSE param_asgn_exp_list
(A.assertCloseAsgn(param_asgn_exp_list))
| ASSERT comma_separated_expression_list
(A.assert(comma_separated_expression_list))
| ASSERT_CLOSE comma_separated_expression_list
(A.assertClose(comma_separated_expression_list))
| LPAREN RETRACT one_or_more_expressions RPAREN
(A.retract(one_or_more_expressions))
| RETRACT comma_separated_expression_list
(A.retract(comma_separated_expression_list))
| LPAREN DEFINE_SORT ID phrase RPAREN (let val sym = S.symbol(ID)
val _ = A.checkNoDots(ID,getPos IDleft)
in
A.sortDefinition(sym,phrase,false)
end)
| DEFINE_SORT ID ASGN phrase (let val sym = S.symbol(ID)
val _ = A.checkNoDots(ID,getPos IDleft)
in
A.sortDefinition(sym,phrase,false)
end)
| LPAREN DEFINE ID phrase RPAREN (let
val sym = S.symbol(ID)
val _ = A.checkNoDots(ID,getPos IDleft)
in
A.definition(sym,phrase,false)
end)
| LPAREN PRIVATE DEFINE ID phrase RPAREN (A.checkNoDots(ID,getPos IDleft);A.definition(S.symbol(ID),phrase,true))
| DEFINE LPAREN ID possibly_wildcard_param_list RPAREN ASGN expression
(A.checkNoDots(ID,getPos IDleft);
A.definitions([A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=NONE},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)})],false))
| DEFINE LPAREN ID possibly_wildcard_param_list RPAREN ASGN deduction
(A.checkNoDots(ID,getPos
IDleft);
A.definitions([A.makeMethodDefinition({meth_name={name=S.symbol(ID),
pos=getPos IDleft,
sort_as_sym_term=NONE,
sort_as_fterm=NONE,
sort_as_exp=NONE,
op_tag=NONE},
meth_params=possibly_wildcard_param_list,
meth_body=deduction,
pos=getPos IDleft,
file=(!Paths.current_file)})],false))
| DEFINE_MEMOIZED LPAREN ID possibly_wildcard_param_list RPAREN ASGN expression
(A.checkNoDots(ID,getPos IDleft);
if (length(possibly_wildcard_param_list) < 1)
then raise A.SyntaxError("Procedures of zero arguments cannot be memoized",SOME (A.posOfExp(expression)))
else ();
let val p:A.phrase = A.makeMemoizedFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=NONE},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)})
val _ = print("\nThe memoized definition was desugared into this: " ^ (A.unparsePhrase p))
in
A.definition(Symbol.symbol(ID),p,false)
end)
| LPAREN DEFINE LEFT_BRACKET patterns RIGHT_BRACKET phrase RPAREN (A.definitionLst(patterns,NONE,phrase,getPos LEFT_BRACKETleft,false))
| LPAREN DEFINE LPAREN ID NAME LEFT_BRACKET patterns RIGHT_BRACKET RPAREN phrase RPAREN
(A.definitionLst(patterns,SOME(Symbol.symbol ID),phrase,getPos LEFT_BRACKETleft,false))
| LPAREN PRIVATE DEFINE LEFT_BRACKET patterns RIGHT_BRACKET phrase RPAREN (A.definitionLst(patterns,NONE,phrase,getPos LEFT_BRACKETleft,true))
| LPAREN PRIVATE DEFINE LPAREN ID NAME LEFT_BRACKET patterns RIGHT_BRACKET RPAREN phrase RPAREN
(A.definitionLst(patterns,SOME(Symbol.symbol ID),phrase,getPos LEFT_BRACKETleft,true))
| DEFINE ID ASGN phrase (A.checkNoDots(ID,getPos IDleft);A.definition(S.symbol(ID),phrase,false))
| PRIVATE DEFINE ID ASGN phrase (A.checkNoDots(ID,getPos IDleft);A.definition(S.symbol(ID),phrase,true))
| DEFINE LEFT_BRACKET patterns RIGHT_BRACKET ASGN phrase (A.definitionLst(patterns,NONE,phrase,getPos LEFT_BRACKETleft,false))
| DEFINE LPAREN ID NAME LEFT_BRACKET patterns RIGHT_BRACKET RPAREN ASGN phrase (A.definitionLst(patterns,SOME(Symbol.symbol ID),
phrase,getPos LEFT_BRACKETleft,false))
| PRIVATE DEFINE LEFT_BRACKET patterns RIGHT_BRACKET ASGN phrase (A.definitionLst(patterns,NONE,phrase,getPos LEFT_BRACKETleft,true))
| PRIVATE DEFINE LPAREN ID NAME LEFT_BRACKET patterns RIGHT_BRACKET RPAREN ASGN phrase
(A.definitionLst(patterns,SOME(Symbol.symbol ID),phrase,getPos LEFT_BRACKETleft,true))
| CLEAR (A.clear_assum_base)
| LPAREN CLEAR RPAREN (A.clear_assum_base)
| LPAREN DEFINE def_blocks RPAREN (A.definitions(def_blocks,false))
| DEFINE_STAR infix_def_blocks (A.definitions(infix_def_blocks,false))
| PRIVATE LPAREN DEFINE def_blocks RPAREN (A.definitions(def_blocks,true))
| LPAREN RULE LPAREN ID possibly_wildcard_param_list RPAREN expression RPAREN
(A.ruleDefinition(S.symbol(ID),A.functionExp({params=possibly_wildcard_param_list,
body=expression,pos=getPos IDleft})))
| RULE LPAREN ID possibly_wildcard_param_list RPAREN ASGN expression
(A.ruleDefinition(S.symbol(ID),A.functionExp({params=possibly_wildcard_param_list,
body=expression,pos=getPos IDleft})))
param_asgn_exp_list: param ASGN expression ([(param,expression)])
| param ASGN expression param_asgn_exp_list ((param,expression)::param_asgn_exp_list)
one_mod_symbol: any_id (let val id_pos = getPos(any_idleft)
in
(A.makeMS(any_id,SOME id_pos),id_pos)
end)
one_or_more_mod_symbols: one_mod_symbol ([one_mod_symbol])
| one_mod_symbol one_or_more_mod_symbols (one_mod_symbol::one_or_more_mod_symbols)
one_or_more_mod_symbols_infix: one_mod_symbol ([one_mod_symbol])
| one_mod_symbol COMMA one_or_more_mod_symbols_infix
(one_mod_symbol::one_or_more_mod_symbols_infix)
def_block: LPAREN ID possibly_wildcard_param_list RPAREN expression
(A.checkNoDots(ID,getPos IDleft);
A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=NONE},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)}))
| LPAREN ID possibly_wildcard_param_list RPAREN ASGN expression
(A.checkNoDots(ID,getPos IDleft);
A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=NONE},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)}))
| LPAREN ID COLON LPAREN OP ID RPAREN possibly_wildcard_param_list RPAREN expression
(A.checkNoDots(ID,getPos IDleft);
case Int.fromString(ID2) of
SOME(i) =>
(A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=SOME(i,~1)},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)}))
| _ => Data.genEx("Operator annotation error: invalid arity",
SOME(getPos ID2left),(!Paths.current_file)))
| LPAREN ID COLON LPAREN OP ID RPAREN possibly_wildcard_param_list RPAREN ASGN expression
(A.checkNoDots(ID,getPos IDleft);
case Int.fromString(ID2) of
SOME(i) =>
(A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=SOME(i,~1)},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)}))
| _ => Data.genEx("Operator annotation error: invalid arity",
SOME(getPos ID2left),(!Paths.current_file)))
| LPAREN ID COLON LPAREN OP ID ID RPAREN possibly_wildcard_param_list RPAREN expression
(A.checkNoDots(ID1,getPos ID1left);
(case (Int.fromString(ID2),Int.fromString(ID3)) of
(SOME(i),SOME(j)) =>
(A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=SOME(i,j)},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)}))
| _ => Data.genEx("Operator annotation error",
SOME(getPos ID2left),(!Paths.current_file))))
| LPAREN ID possibly_wildcard_param_list RPAREN deduction
(A.checkNoDots(ID,getPos IDleft);
A.makeMethodDefinition({meth_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=NONE},
meth_params=possibly_wildcard_param_list,
meth_body=deduction,pos= getPos IDleft,file=(!Paths.current_file)}))
infix_def_block: LPAREN ID possibly_wildcard_param_list RPAREN ASGN expression
(A.checkNoDots(ID,getPos IDleft);
A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=NONE},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)}))
| LPAREN ID COLON LPAREN OP ID RPAREN possibly_wildcard_param_list RPAREN ASGN expression
(A.checkNoDots(ID,getPos IDleft);
case Int.fromString(ID2) of
SOME(i) =>
(A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=SOME(i,~1)},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)}))
| _ => Data.genEx("Operator annotation error: invalid arity",
SOME(getPos ID2left),(!Paths.current_file)))
| LPAREN ID COLON LPAREN OP ID ID RPAREN possibly_wildcard_param_list RPAREN ASGN expression
(A.checkNoDots(ID1,getPos ID1left);
(case (Int.fromString(ID2),Int.fromString(ID3)) of
(SOME(i),SOME(j)) =>
(A.makeFunDefinition({fun_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=SOME(i,j)},
fun_params=possibly_wildcard_param_list,
fun_body=expression,pos=getPos IDleft,file=(!Paths.current_file)}))
| _ => Data.genEx("Operator annotation error",
SOME(getPos ID2left),(!Paths.current_file))))
| LPAREN ID possibly_wildcard_param_list RPAREN ASGN deduction
(A.checkNoDots(ID,getPos IDleft);
A.makeMethodDefinition({meth_name={name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE,op_tag=NONE},
meth_params=possibly_wildcard_param_list,
meth_body=deduction,pos= getPos IDleft,file=(!Paths.current_file)}))
lcb: LEFT_CURLY_BRACE ()
rcb: RIGHT_CURLY_BRACE ()
module: LPAREN MODULE param input_list RPAREN (if Symbol.symEq(#name(param),Names.top_module_symbol) then
raise A.SyntaxError("The name Top cannot be used for a module",SOME(getPos paramleft))
else
{module_name=param,module_file=ref(!Paths.current_file),module_contents=input_list}:A.module_entry)
| MODULE param lcb input_list rcb (if Symbol.symEq(#name(param),Names.top_module_symbol) then
raise A.SyntaxError("The name Top cannot be used for a module",SOME(getPos paramleft))
else {module_name=param,module_file=ref(!Paths.current_file),module_contents=input_list}:A.module_entry)
moduleExtension: LPAREN EXTEND_MODULE param input_list RPAREN ({module_name=param,module_file=ref(!Paths.current_file),module_contents=input_list}:A.module_entry)
| EXTEND_MODULE param lcb input_list rcb ({module_name=param,module_file=ref(!Paths.current_file),module_contents=input_list}:A.module_entry)
def_blocks: def_block ([def_block])
| def_block def_blocks (def_block::def_blocks)
infix_def_blocks: infix_def_block ([infix_def_block])
| infix_def_block LOGICAL_AND infix_def_blocks (infix_def_block::infix_def_blocks)
one_or_more_athena_vars: athena_var ([athena_var])
| athena_var one_or_more_athena_vars (athena_var::one_or_more_athena_vars)
any_id: ID (ID) | PRIVATE_ID (PRIVATE_ID)
map_binding: phrase ASGN phrase (A.exp(A.listExp({members=[phrase1,phrase2],pos=getPos(phrase1left)})))
map_bindings: ([])
| map_binding ([map_binding])
| map_binding COMMA map_bindings (map_binding::map_bindings)
expression: any_id (let val id_pos = getPos(any_idleft)
val mod_sym = A.makeMS(any_id,SOME id_pos)
val (mods,s) = MS.split(mod_sym)
in
A.idExp({msym=mod_sym,mods=mods,sym=s,no_mods=null(mods),pos=id_pos})
end)
| DOUBLE_LEFT_CURLY_BRACE one_or_more_expressions DOUBLE_RIGHT_CURLY_BRACE (hd one_or_more_expressions)
| LPAREN OP expression RPAREN (A.opExp({op_exp=expression,pos=getPos LPARENleft}))
| ID COLON user_sort (let val id_pos = getPos(IDleft)
in
A.taggedConSym({name=A.makeMS(ID,SOME id_pos),pos=id_pos,sort_as_tagged_symterm=user_sort,sort_as_fterm=NONE})
end)
| LPAREN RPAREN (A.unitExp({pos=getPos LPARENleft}))
| CHARACTER (A.charExp({code=CHARACTER,pos=getPos CHARACTERleft}))
| STRING (A.stringExp({str=STRING,pos=getPos STRINGleft,mem_index=(~1)}))
| ath_var (ath_var)
| athena_meta_id (athena_meta_id)
| LPAREN phrase LOGICAL_AND phrase RPAREN (A.logicalAndExp({args=[phrase1,phrase2],pos=getPos LOGICAL_ANDleft}))
| LPAREN LOGICAL_AND one_or_more_phrases RPAREN
(A.logicalAndExp({args=one_or_more_phrases,pos=getPos LOGICAL_ANDleft}))
| LPAREN LOGICAL_OR one_or_more_phrases RPAREN
(A.logicalOrExp({args=one_or_more_phrases,pos=getPos LOGICAL_ORleft}))
| LPAREN phrase LOGICAL_OR phrase RPAREN (A.logicalOrExp({args=[phrase1,phrase2],pos=getPos LOGICAL_ORleft}))
| LPAREN MAKE_CELL phrase RPAREN (A.cellExp({contents=phrase,pos=getPos MAKE_CELLleft}))
| MAKE_CELL phrase (A.cellExp({contents=phrase,pos=getPos MAKE_CELLleft}))
| LPAREN REF expression RPAREN (A.refExp({cell_exp=expression,pos=getPos REFleft}))
| REF expression (A.refExp({cell_exp=expression,pos=getPos REFleft}))
| LPAREN SET expression phrase RPAREN (A.setCellExp({cell_exp=expression,
set_phrase=phrase,pos=getPos SETleft}))
| SET expression phrase (A.setCellExp({cell_exp=expression,
set_phrase=phrase,pos=getPos SETleft}))
| LPAREN VECTOR_INIT expression phrase RPAREN (A.vectorInitExp({length_exp=expression,
init_val=phrase,pos=getPos VECTOR_INITleft}))
| VECTOR_INIT expression phrase (A.vectorInitExp({length_exp=expression,
init_val=phrase,pos=getPos VECTOR_INITleft}))
| LPAREN VECTOR_SET expression expression phrase RPAREN (A.vectorSetExp({vector_exp=expression1,
index_exp=expression2,
new_val=phrase,pos=getPos VECTOR_SETleft}))
| VECTOR_SET expression expression phrase (A.vectorSetExp({vector_exp=expression1,
index_exp=expression2,
new_val=phrase,pos=getPos VECTOR_SETleft}))
| LPAREN VECTOR_SUB expression expression RPAREN (A.vectorSubExp({vector_exp=expression1,
index_exp=expression2,
pos=getPos VECTOR_SUBleft}))
| VECTOR_SUB expression expression (A.vectorSubExp({vector_exp=expression1,
index_exp=expression2,
pos=getPos VECTOR_SUBleft}))
| FUNCTION LPAREN possibly_wildcard_param_list_no_dots RPAREN expression
(let val infix_flag = (length(possibly_wildcard_param_list_no_dots) = 2)
in A.functionExp({params=possibly_wildcard_param_list_no_dots,body=expression,
pos=getPos FUNCTIONleft})
end)
| LPAREN FUNCTION LPAREN possibly_wildcard_param_list_no_dots RPAREN expression RPAREN
(let val infix_flag = (length(possibly_wildcard_param_list_no_dots) = 2)
in A.functionExp({params=possibly_wildcard_param_list_no_dots,body=expression,
pos=getPos FUNCTIONleft})
end)
| LPAREN WITH_KEYS LPAREN params RPAREN expression expression RPAREN
(A.desugarWithKeys(params,expression1,expression2,getPos WITH_KEYSleft))
| WITH_KEYS one_or_more_comma_separated_params FROM expression expression
(A.desugarWithKeys(one_or_more_comma_separated_params,expression1,expression2,getPos WITH_KEYSleft))
| LPAREN phrase phrases RPAREN (A.appExp({proc=phrase,args=phrases,alt_exp=ref(NONE),pos=getPos LPARENleft}))
| LEFT_BRACKET phrases RIGHT_BRACKET (A.listExp({members=phrases,pos=getPos LEFT_BRACKETleft}))
| LEFT_BRACKET expression FOR pattern OVER expression RIGHT_BRACKET (A.desugarListComprehension(expression1,pattern,expression2,NONE))
| LEFT_BRACKET expression FOR pattern OVER expression PROVIDED expression RIGHT_BRACKET (A.desugarListComprehension(expression1,pattern,expression2,SOME(expression3)))
| MAP_BEGIN map_bindings MAP_END (A.makeMapExp(map_bindings,getPos(MAP_BEGINleft)))
| LPAREN METHOD LPAREN possibly_wildcard_param_list_no_dots RPAREN deduction RPAREN
(A.methodExp({params=possibly_wildcard_param_list_no_dots,body=deduction,pos=getPos METHODleft,
name=ref("")}))
| METHOD LPAREN possibly_wildcard_param_list_no_dots RPAREN deduction
(A.methodExp({params=possibly_wildcard_param_list_no_dots,body=deduction,pos=getPos METHODleft,
name=ref("")}))
| LPAREN TRY one_or_more_expressions RPAREN
(A.tryExp({choices=one_or_more_expressions,pos=getPos TRYleft}))
| TRY lcb one_or_more_separated_expressions rcb
(A.tryExp({choices=one_or_more_separated_expressions,pos=getPos TRYleft}))
| LPAREN CHECK check_clauses RPAREN
(A.checkExp({clauses=check_clauses,pos=getPos CHECKleft}))
| CHECK lcb infix_check_clauses rcb
(A.checkExp({clauses=infix_check_clauses,pos=getPos CHECKleft}))
| MATCH phrase lcb infix_match_clauses rcb
(A.matchExp({discriminant=phrase,clauses=infix_match_clauses,pos=getPos MATCHleft}))
| LPAREN MATCH phrase match_clauses RPAREN
(A.matchExp({discriminant=phrase,clauses=match_clauses,pos=getPos MATCHleft}))
| LET lcb semicolon_separated_bindings rcb expression (A.letExp({bindings=semicolon_separated_bindings,body=expression,pos=getPos LETleft}))
| LETREC lcb semicolon_separated_bindings rcb expression (A.letRecExp({bindings=semicolon_separated_bindings,body=expression,pos=getPos LETRECleft}))
| LPAREN LET LPAREN bindings RPAREN expression RPAREN
(A.letExp({bindings=bindings,body=expression,pos=getPos LETleft}))
| LPAREN LETREC LPAREN bindings RPAREN expression RPAREN
(A.letRecExp({bindings=bindings,body=expression,pos=getPos LETRECleft}))
| LPAREN SEQ one_or_more_phrases RPAREN
(A.beginExp({members=one_or_more_phrases,pos=getPos SEQleft}))
| LPAREN WHILE phrase phrase RPAREN
(A.whileExp({test=phrase1,body=phrase2,pos=getPos WHILEleft}))
| WHILE phrase phrase
(A.whileExp({test=phrase1,body=phrase2,pos=getPos WHILEleft}))
deduction: LPAREN expression BY deduction RPAREN (A.byDed({wanted_res=expression,body=deduction,conc_name=NONE,
pos=getPos LPARENleft}))
| LPAREN CONCLUDE expression deduction RPAREN (A.byDed({wanted_res=expression,body=deduction,conc_name=NONE,
pos=getPos LPARENleft}))
| CONCLUDE expression deduction (A.byDed({wanted_res=expression,body=deduction,conc_name=NONE,
pos=getPos CONCLUDEleft}))
| LPAREN CONCLUDE param_no_dots ASGN expression deduction RPAREN (A.byDed({wanted_res=expression,body=deduction,conc_name=SOME param_no_dots,
pos=getPos LPARENleft}))
| CONCLUDE param_no_dots ASGN expression deduction (A.byDed({wanted_res=expression,body=deduction,conc_name=SOME param_no_dots,
pos=getPos CONCLUDEleft}))
| inference_block (inference_block)
| ASSUME phrase deduction
(A.assumeDed({assumption=phrase,body=deduction,pos=getPos ASSUMEleft}))
| SUPPOSE_ABSURD phrase deduction
(A.absurdDed({hyp=phrase,body=deduction,pos=getPos SUPPOSE_ABSURDleft}))
| ASSUME assignments deduction
(A.infixAssumeDed({bindings=assignments,body=deduction,pos=getPos ASSUMEleft}))
| SUPPOSE_ABSURD ID ASGN phrase deduction
(A.checkNoDots(ID,getPos IDleft);
A.absurdLetDed({named_hyp={bpat=A.idPat({name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,op_tag=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE}),
def=phrase,pos=getPos IDleft},
body=deduction,pos=getPos SUPPOSE_ABSURDleft}))
| BY_CASES phrase BEGIN case_clauses END
(A.byCasesDed({disj=phrase,from_exps=NONE,
arms=case_clauses,pos=getPos BY_CASESleft}))
| BY_CASES phrase lcb case_clauses rcb
(A.byCasesDed({disj=phrase,from_exps=NONE,
arms=case_clauses,pos=getPos BY_CASESleft}))
| BY_CASES phrase FROM comma_separated_expression_list BEGIN case_clauses END
(A.byCasesDed({disj=phrase,from_exps=SOME(comma_separated_expression_list),
arms=case_clauses,pos=getPos BY_CASESleft}))
| BY_CASES phrase FROM comma_separated_expression_list lcb case_clauses rcb
(A.byCasesDed({disj=phrase,from_exps=SOME(comma_separated_expression_list),
arms=case_clauses,pos=getPos BY_CASESleft}))
| PICK_ANY possibly_typed_params_no_dots deduction
(A.pickAnyDed({eigenvars=A.checkForDuplicateParams(possibly_typed_params_no_dots),
body=deduction,pos=getPos PICK_ANYleft}))
| PICK_WITNESS ID FOR phrase param_option deduction
(A.checkNoDots(ID,getPos IDleft);
A.pickWitnessDed({ex_gen=phrase,var_id=S.symbol(ID),inst_id=param_option,body=deduction,
pos=getPos PICK_WITNESSleft}))
| PICK_WITNESSES one_or_more_params_no_dots FOR phrase param_option_no_dots deduction
(A.pickWitnessesDed({ex_gen=phrase,var_ids=A.getParamNames(one_or_more_params_no_dots),
inst_id=param_option_no_dots,body=deduction,
pos=getPos PICK_WITNESSESleft}))
| INDUCTION phrase BEGIN infix_dmatch_clauses END
(let val res = A.inductionDed({prop=phrase,
clauses=infix_dmatch_clauses,pos=getPos INDUCTIONleft})
in
res
end)
| INDUCTION phrase lcb infix_dmatch_clauses rcb
(let val res = A.inductionDed({prop=phrase,
clauses=infix_dmatch_clauses,pos=getPos INDUCTIONleft})
in
res
end)
| STRUCTURE_CASES phrase BEGIN infix_dmatch_clauses END
(let val res = A.structureCasesDed({prop=phrase,term=NONE,
clauses=infix_dmatch_clauses,pos=getPos STRUCTURE_CASESleft})
in
res
end)
| STRUCTURE_CASES phrase lcb infix_dmatch_clauses rcb
(let val res = A.structureCasesDed({prop=phrase,term=NONE,
clauses=infix_dmatch_clauses,pos=getPos STRUCTURE_CASESleft})
in
res
end)
| DATATYPE_CASES phrase BEGIN infix_dmatch_clauses END
(let val res = A.structureCasesDed({prop=phrase,term=NONE,
clauses=infix_dmatch_clauses,pos=getPos DATATYPE_CASESleft})
in
res
end)
| DATATYPE_CASES phrase lcb infix_dmatch_clauses rcb
(let val res = A.structureCasesDed({prop=phrase,term=NONE,
clauses=infix_dmatch_clauses,pos=getPos DATATYPE_CASESleft})
in
res
end)
| DATATYPE_CASES phrase ON expression lcb infix_dmatch_clauses rcb
(let val res = A.structureCasesDed({prop=phrase,term=SOME(expression),
clauses=infix_dmatch_clauses,pos=getPos DATATYPE_CASESleft})
in
res
end)
| LPAREN ASSUME ID ASGN phrase deduction RPAREN
(A.checkNoDots(ID,getPos IDleft);
A.assumeLetDed({bindings=[({bpat=A.idPat({name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,op_tag=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE}),
def=phrase,pos=getPos IDleft})],body=deduction,
pos=getPos ASSUMEleft}))
| LPAREN ASSUME phrase deduction RPAREN
(A.assumeDed({assumption=phrase,body=deduction,pos=getPos ASSUMEleft}))
| LPAREN ASSUME_LET binding deduction RPAREN
(A.assumeLetDed({bindings=[binding],body=deduction,
pos=getPos ASSUME_LETleft}))
| LPAREN SUPPOSE_ABSURD phrase deduction RPAREN
(A.absurdDed({hyp=phrase,body=deduction,pos=getPos SUPPOSE_ABSURDleft}))
| LPAREN SUPPOSE_ABSURD_LET binding deduction RPAREN
(A.absurdLetDed({named_hyp=binding,body=deduction,pos=getPos SUPPOSE_ABSURD_LETleft}))
| LPAREN DCHECK dcheck_clauses RPAREN
(A.checkDed({clauses=dcheck_clauses,pos=getPos DCHECKleft}))
| LPAREN EXCL_MARK expression phrases RPAREN
(case expression of
A.idExp({msym,...}) =>
if Basic.isMember(MS.name(msym),["prim-mp", "prim-both"]) andalso length(phrases) = 2 then
(A.BMethAppDed({method=expression,arg1=hd phrases, arg2 = hd(tl(phrases)), pos=getPos LPARENleft}))
else
if Basic.isMember(MS.name(msym),["prim-conj-intro"]) andalso length(phrases) = 1 then
(A.UMethAppDed({method=expression,arg=hd phrases, pos=getPos LPARENleft}))
else
(A.methodAppDed({method=expression,args=phrases,pos=getPos LPARENleft}))
| _ => (A.methodAppDed({method=expression,args=phrases,pos=getPos LPARENleft})))
| LPAREN APPLY_METHOD expression phrases RPAREN
(A.methodAppDed({method=expression,args=phrases,pos=getPos expressionleft}))
| LPAREN DMATCH phrase dmatch_clauses RPAREN
(A.matchDed({discriminant=phrase,clauses=dmatch_clauses,pos=getPos DMATCHleft}))
| LPAREN DLET LPAREN bindings RPAREN deduction RPAREN
(A.letDed({bindings=bindings,body=deduction,pos=getPos DLETleft}))
| LPAREN DLETREC LPAREN bindings RPAREN deduction RPAREN
(A.letRecDed({bindings=bindings,body=deduction,pos=getPos DLETRECleft}))
| LET lcb semicolon_separated_bindings rcb deduction
(A.letDed({bindings=semicolon_separated_bindings,body=deduction,pos=getPos LETleft}))
| DLET lcb semicolon_separated_bindings rcb deduction
(A.letDed({bindings=semicolon_separated_bindings,body=deduction,pos=getPos DLETleft}))
| LETREC lcb semicolon_separated_bindings rcb deduction (A.letRecDed({bindings=semicolon_separated_bindings,body=deduction,pos=getPos LETRECleft}))
| DLETREC lcb semicolon_separated_bindings rcb deduction (A.letRecDed({bindings=semicolon_separated_bindings,body=deduction,pos=getPos DLETRECleft}))
| TRY lcb one_or_more_separated_deductions rcb
(A.tryDed({choices=one_or_more_separated_deductions,pos=getPos TRYleft}))
| MATCH phrase BEGIN infix_dmatch_clauses END
(A.matchDed({discriminant=phrase,clauses=infix_dmatch_clauses,pos=getPos MATCHleft}))
| MATCH phrase lcb infix_dmatch_clauses rcb
(A.matchDed({discriminant=phrase,clauses=infix_dmatch_clauses,pos=getPos MATCHleft}))
| DMATCH phrase lcb infix_dmatch_clauses rcb
(A.matchDed({discriminant=phrase,clauses=infix_dmatch_clauses,pos=getPos DMATCHleft}))
| CHECK lcb infix_dcheck_clauses rcb
(A.checkDed({clauses=infix_dcheck_clauses,pos=getPos CHECKleft}))
| DCHECK lcb infix_dcheck_clauses rcb
(A.checkDed({clauses=infix_dcheck_clauses,pos=getPos DCHECKleft}))
| LPAREN DTRY one_or_more_deductions RPAREN
(A.tryDed({choices=one_or_more_deductions,pos=getPos DTRYleft}))
| TRY BEGIN one_or_more_separated_deductions END
(A.tryDed({choices=one_or_more_separated_deductions,pos=getPos TRYleft}))
| LPAREN DSEQ one_or_more_deductions RPAREN
(A.beginDed({members=one_or_more_deductions,pos=getPos DSEQleft}))
| LPAREN GEN_OVER expression deduction RPAREN
(A.genOverDed({eigenvar_exp=expression,body=deduction,pos=getPos GEN_OVERleft}))
| GEN_OVER expression deduction
(A.genOverDed({eigenvar_exp=expression,body=deduction,pos=getPos GEN_OVERleft}))
| LPAREN PICK_ANY possibly_typed_params_no_dots deduction RPAREN
(A.pickAnyDed({eigenvars=A.checkForDuplicateParams(possibly_typed_params_no_dots),
body=deduction,pos=getPos PICK_ANYleft}))
| LPAREN WITH_WITNESS expression phrase deduction RPAREN
(A.withWitnessDed({eigenvar_exp=expression,ex_gen=phrase,body=deduction,
pos=getPos WITH_WITNESSleft}))
| LPAREN PICK_WITNESS ID phrase param_option_no_dots deduction RPAREN
(A.checkNoDots(ID,getPos IDleft);
A.pickWitnessDed({ex_gen=phrase,var_id=S.symbol(ID),inst_id=param_option_no_dots,body=deduction,
pos=getPos PICK_WITNESSleft}))
| LPAREN PICK_WITNESSES LPAREN one_or_more_params_no_dots RPAREN phrase param_option_no_dots deduction RPAREN
(A.pickWitnessesDed({ex_gen=phrase,var_ids=A.getParamNames(one_or_more_params_no_dots),
inst_id=param_option_no_dots,body=deduction,
pos=getPos PICK_WITNESSESleft}))
| LPAREN INDUCTION phrase dmatch_clauses RPAREN
(let val res = A.inductionDed({prop=phrase,
clauses=dmatch_clauses,pos=getPos INDUCTIONleft})
in
res
end)
| LPAREN STRUCTURE_CASES phrase dmatch_clauses RPAREN
(let val res = A.structureCasesDed({prop=phrase,term=NONE,
clauses=dmatch_clauses,pos=getPos STRUCTURE_CASESleft})
in
res
end)
| LPAREN DATATYPE_CASES phrase dmatch_clauses RPAREN
(let val res = A.structureCasesDed({prop=phrase,term=NONE,
clauses=dmatch_clauses,pos=getPos DATATYPE_CASESleft})
in
res
end)
| LPAREN DATATYPE_CASES phrase ON expression dmatch_clauses RPAREN
(let val res = A.structureCasesDed({prop=phrase,term=SOME(expression),
clauses=dmatch_clauses,pos=getPos DATATYPE_CASESleft})
in
res
end)
phrase_pair: LPAREN phrase phrase RPAREN ((phrase1,phrase2,getPos(LPARENleft), getPos(phrase1left), getPos(phrase2left)))
phrase_pair_list: phrase_pair ([phrase_pair])
| phrase_pair phrase_pair_list (phrase_pair::phrase_pair_list)
comma_separated_expression_list: expression ([expression])
| expression COMMA comma_separated_expression_list
(expression::comma_separated_expression_list)
comma_separated_phrase_list: phrase ([phrase])
| phrase COMMA comma_separated_phrase_list
(phrase::comma_separated_phrase_list)
opt_comma_separated_phrase_list: phrase ([phrase])
| phrase COMMA opt_comma_separated_phrase_list
(phrase::opt_comma_separated_phrase_list)
| phrase opt_comma_separated_phrase_list
(phrase::opt_comma_separated_phrase_list)
inference: expression FROM comma_separated_phrase_list
(A.methodAppDed({method=A.idExp({msym=A.mSym N.spfPrimMethod_symbol,mods=[],sym=N.spfPrimMethod_symbol,no_mods=true,pos=getPos FROMleft}),
args=[A.exp(expression),
A.exp(A.listExp({members=comma_separated_phrase_list,pos=getPos FROMright}))],
pos=A.posOfExp(expression)}))
| expression BY expression ON comma_separated_phrase_list
(A.byDed({wanted_res=expression1,conc_name=NONE,body=A.methodAppDed({method=expression2,
args=comma_separated_phrase_list,pos=A.posOfExp(expression)}),pos=getPos BYleft}))
| expression ON comma_separated_phrase_list
(A.methodAppDed({method=expression,args=comma_separated_phrase_list,pos=A.posOfExp(expression)}))
| deduction (deduction)
possibly_named_inference: inference ({param=NONE,def=A.ded(inference),pos=A.posOfDed(inference)})
| ID ASGN inference
({param=SOME(A.someParam({name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,op_tag=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE})),
def=A.ded(inference),pos=A.posOfDed(inference)})
| ANY_PAT ASGN inference
({param=SOME(A.wildCard(getPos ANY_PATleft)),
def=A.ded(inference),pos=A.posOfDed(inference)})
| ID ASGN expression
({param=SOME(A.someParam({name=S.symbol(ID),pos=getPos IDleft,sort_as_sym_term=NONE,op_tag=NONE,
sort_as_fterm=NONE,sort_as_exp=NONE})),
def=A.exp(expression),pos=A.posOfExp(expression)})
| ID COLON LPAREN OP ID RPAREN ASGN expression
(case Int.fromString(ID2) of
SOME(i) =>
({param=SOME(A.someParam({name=S.symbol(ID1),pos=getPos IDleft,sort_as_sym_term=NONE,
op_tag=SOME(i,~1),sort_as_fterm=NONE,sort_as_exp=NONE})),
def=A.exp(expression),pos=A.posOfExp(expression)})
| _ => Data.genEx("Operator annotation error: invalid arity",
SOME(getPos ID2left),(!Paths.current_file)))
| ID COLON LPAREN OP ID ID RPAREN ASGN expression
(case (Int.fromString(ID2),Int.fromString(ID3)) of
(SOME(i),SOME(j)) =>
({param=SOME(A.someParam({name=S.symbol(ID1),pos=getPos ID1left,sort_as_sym_term=NONE,op_tag=SOME(i,j),
sort_as_fterm=NONE,sort_as_exp=NONE})),
def=A.exp(expression),pos=A.posOfExp(expression)})
| _ => Data.genEx("Operator annotation error",
SOME(getPos ID2left),(!Paths.current_file)))
| ANY_PAT ASGN expression
({param=SOME(A.wildCard(getPos ANY_PATleft)),
def=A.exp(expression),pos=A.posOfExp(expression)})
inference_list: possibly_named_inference ([possibly_named_inference])
| possibly_named_inference SEMI_COLON inference_list
(possibly_named_inference::inference_list)
case_clause: expression ARROW deduction ({case_name=NONE,alt=expression,proof=deduction})
| param ASGN expression ARROW deduction ({case_name=SOME(param),alt=expression,proof=deduction})
case_clauses: case_clause ([case_clause])
| case_clause single_logical_or case_clauses (case_clause::case_clauses)
inference_block: BEGIN inference_list END
(case rev(inference_list) of
(b:A.optBinding as {param,def=A.ded(d),pos})::rest =>
A.letDed({bindings=A.getBindings(rev (rest)),body=d,pos=getPos BEGINleft})
| (b as {param,def=A.exp(e),pos})::_ =>
raise A.SyntaxError("expression found in the tail position of"^
"\na begin-end inference block---a deduction is"^
" required in that position",SOME pos))
| lcb inference_list rcb
(case rev(inference_list) of
(b:A.optBinding as {param,def=A.ded(d),pos})::rest =>
A.letDed({bindings=A.getBindings(rev (rest)),body=d,pos=getPos lcbleft})
| (b as {param,def=A.exp(e),pos})::_ =>
raise A.SyntaxError("expression found in the tail position of"^
"\na begin-end inference block---a deduction is"^
" required in that position",SOME pos))
deductions: ([])
| deduction deductions (deduction::deductions)
phrase: expression (A.exp(expression))
| deduction (A.ded(deduction))
phrases: ([])
| phrase phrases (phrase::phrases)