diff --git a/Makefile b/Makefile index 0c203fd..26aaa5b 100644 --- a/Makefile +++ b/Makefile @@ -274,3 +274,23 @@ sys-purercdsub: $(SYS_PURERCDSUB) jenkins: cd regression; \ make run-jenkins + + +# quick lean experiments + +test10st.lean: tests/test10st.ott + bin/ott \ + -i tests/test10st.ott \ + -o tests/test10st.lean + cp tests/test10st.lean test-lean-project + +test7.lean: tests/tmp_test7.ott + bin/ott \ + -i tests/tmp_test7.ott \ + -o tests/test7.lean + cp tests/test7.lean test-lean-project + +tests/tmp_test7.ott: tests/test7.ott + rm -f tests/tmp_test7.ott + (sed -e 's/^r//g') < tests/test7.ott > tests/tmp_test7.ott + chmod ugo-w tests/tmp_test7.ott diff --git a/doc/top2.mng b/doc/top2.mng index b243dd3..0f92d54 100644 --- a/doc/top2.mng +++ b/doc/top2.mng @@ -843,6 +843,7 @@ For this, one can add a \mykw{coq}, \mykw{hol}, \mykw{isa}, or \mykw{ocaml} hom to the primary nonterminal root. In the example below, the user can write \texttt{T}, \texttt{T'} etc. in their Ott source, but the generated HOL type is \texttt{Typ}. +(TODO: this should work as stated for Lean, but such a hom also affects variable printing -- maybe that's a bug. Added a \mykw{lean-type} hom.) \begin{alltt} T \mysym{\mylb\mylb{}} \mykw{hol} Typ \mysym{\myrb\myrb{}}\mysym{,} S\mysym{,} U \mysym{::} 'T_' \mysym{::=} \mysym{\mylb\mylb{}} \mykw{com} type \mysym{\myrb\myrb{}} \mysym{|} T -> T' \mysym{::} \mysym{::} Fun \mysym{\mylb\mylb{}} \mykw{com} type of functions \mysym{\myrb\myrb{}} diff --git a/examples/1Bsemantics/.l1.aux b/examples/1Bsemantics/.l1.aux new file mode 100644 index 0000000..02364ab --- /dev/null +++ b/examples/1Bsemantics/.l1.aux @@ -0,0 +1 @@ +COQAUX1 4a24abe13b920db9d4882fac2ca00359 /home/pes20/repos/ott/examples/1Bsemantics/l1.v diff --git a/examples/1Bsemantics/Makefile b/examples/1Bsemantics/Makefile index 380572b..c891be2 100644 --- a/examples/1Bsemantics/Makefile +++ b/examples/1Bsemantics/Makefile @@ -1,9 +1,9 @@ -#OTT=../../bin/ott -OTT=ott +OTT=../../bin/ott +#OTT=ott l1: l1.ott - $(OTT) -pp_grammar -isa_syntax true l1.ott -o l1.tex -o l1.thy -o l1.lem -o l1.v + $(OTT) -pp_grammar -isa_syntax true l1.ott -o l1.tex -o l1.v -o l1.lean # -o l1.thy -o l1.lem $(OTT) -tex_wrap false l1.ott -o l1_nowrap.tex pdflatex l1.tex lem l1.lem -isa diff --git a/examples/1Bsemantics/l1.glob b/examples/1Bsemantics/l1.glob new file mode 100644 index 0000000..f1228b5 --- /dev/null +++ b/examples/1Bsemantics/l1.glob @@ -0,0 +1,216 @@ +DIGEST 4a24abe13b920db9d4882fac2ca00359 +Fl1 +R72:77 Stdlib.ZArith.ZArith <> <> lib +R132:135 Stdlib.Bool.Bool <> <> lib +R158:161 Stdlib.Lists.List <> <> lib +R191:204 Stdlib.Strings.String <> <> lib +def 252:259 <> location +R270:275 Stdlib.Strings.String <> string ind +ind 311:314 <> tloc +constr 354:364 <> TLoc_intref +R368:371 l1 <> tloc:1 ind +scheme 311:314 <> tloc_rect +scheme 311:314 <> tloc_ind +scheme 311:314 <> tloc_rec +scheme 311:314 <> tloc_sind +ind 385:394 <> operations +constr 426:432 <> Op_plus +constr 450:456 <> Op_gteq +R436:445 l1 <> operations:3 ind +R460:469 l1 <> operations:3 ind +scheme 385:394 <> operations_rect +scheme 385:394 <> operations_ind +scheme 385:394 <> operations_rec +scheme 385:394 <> operations_sind +ind 483:497 <> type_assumption +constr 534:539 <> TA_loc +R544:551 l1 <> location def +binder 542:542 <> l:7 +R561:564 l1 <> tloc ind +binder 555:559 <> tloc5:8 +scheme 483:497 <> type_assumption_rect +scheme 483:497 <> type_assumption_ind +scheme 483:497 <> type_assumption_rec +scheme 483:497 <> type_assumption_sind +ind 579:579 <> e +constr 612:616 <> E_num +constr 628:633 <> E_bool +constr 648:651 <> E_op +constr 686:689 <> E_if +constr 715:722 <> E_assign +constr 747:751 <> E_ref +constr 769:774 <> E_skip +constr 783:792 <> E_sequence +constr 811:817 <> E_while +R622:622 Corelib.Numbers.BinNums <> Z ind +binder 619:620 <> n5:11 +R639:642 Corelib.Init.Datatypes <> bool ind +binder 636:637 <> b5:12 +R657:657 l1 <> e:9 ind +binder 654:655 <> e1:13 +R664:673 l1 <> operations ind +binder 661:662 <> op:14 +R680:680 l1 <> e:9 ind +binder 677:678 <> e2:15 +R695:695 l1 <> e:9 ind +binder 692:693 <> e1:16 +R702:702 l1 <> e:9 ind +binder 699:700 <> e2:17 +R709:709 l1 <> e:9 ind +binder 706:707 <> e3:18 +R727:734 l1 <> location def +binder 725:725 <> l:19 +R741:741 l1 <> e:9 ind +binder 738:739 <> e5:20 +R756:763 l1 <> location def +binder 754:754 <> l:21 +R778:778 l1 <> e:9 ind +R798:798 l1 <> e:9 ind +binder 795:796 <> e1:22 +R805:805 l1 <> e:9 ind +binder 802:803 <> e2:23 +R823:823 l1 <> e:9 ind +binder 820:821 <> e1:24 +R830:830 l1 <> e:9 ind +binder 827:828 <> e2:25 +scheme 579:579 <> e_rect +scheme 579:579 <> e_ind +scheme 579:579 <> e_rec +scheme 579:579 <> e_sind +ind 845:847 <> typ +constr 874:878 <> T_int +constr 889:894 <> T_bool +constr 905:910 <> T_unit +R882:884 l1 <> typ:26 ind +R898:900 l1 <> typ:26 ind +R914:916 l1 <> typ:26 ind +scheme 845:847 <> typ_rect +scheme 845:847 <> typ_ind +scheme 845:847 <> typ_rec +scheme 845:847 <> typ_sind +def 947:955 <> is_v_of_e +R962:962 l1 <> e ind +binder 958:960 <> e_6:28 +R967:970 Corelib.Init.Datatypes <> bool ind +R983:985 l1 <> e_6:28 var +R997:1001 l1 <> E_num constr +R1011:1014 Corelib.Init.Datatypes <> true constr +R1022:1027 l1 <> E_bool constr +R1037:1040 Corelib.Init.Datatypes <> true constr +R1048:1051 l1 <> E_op constr +R1066:1070 Corelib.Init.Datatypes <> false constr +R1077:1080 l1 <> E_if constr +R1095:1099 Corelib.Init.Datatypes <> false constr +R1106:1113 l1 <> E_assign constr +R1124:1128 Corelib.Init.Datatypes <> false constr +R1135:1139 l1 <> E_ref constr +R1147:1151 Corelib.Init.Datatypes <> false constr +R1157:1162 l1 <> E_skip constr +R1168:1171 Corelib.Init.Datatypes <> true constr +R1179:1188 l1 <> E_sequence constr +R1200:1204 Corelib.Init.Datatypes <> false constr +R1211:1217 l1 <> E_while constr +R1229:1233 Corelib.Init.Datatypes <> false constr +ind 1286:1291 <> reduce +constr 1383:1389 <> op_plus +constr 1542:1548 <> op_gteq +constr 1702:1704 <> op1 +constr 1883:1885 <> op2 +constr 2064:2068 <> deref +constr 2209:2215 <> assign1 +constr 2339:2345 <> assign2 +constr 2511:2514 <> seq1 +constr 2602:2605 <> seq2 +constr 2770:2772 <> if1 +constr 2869:2871 <> if2 +constr 2969:2971 <> if3 +constr 3133:3137 <> while +ind 3275:3280 <> typing +constr 3352:3357 <> Ty_int +constr 3437:3443 <> Ty_bool +constr 3528:3537 <> Ty_op_plus +constr 3684:3693 <> Ty_op_gteq +constr 3841:3845 <> Ty_if +constr 4018:4026 <> Ty_assign +constr 4217:4224 <> Ty_deref +constr 4374:4380 <> Ty_skip +constr 4450:4455 <> Ty_seq +constr 4601:4608 <> Ty_while +R1296:1299 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R1295:1295 l1 <> e ind +R1319:1322 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R1300:1303 Corelib.Init.Datatypes <> list ind +R1314:1316 Corelib.Init.Datatypes <> ::type_scope:x_'*'_x not +R1306:1313 l1 <> location def +R1317:1317 Corelib.Numbers.BinNums <> Z ind +R1324:1327 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R1323:1323 l1 <> e ind +R1347:1350 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R1328:1331 Corelib.Init.Datatypes <> list ind +R1342:1344 Corelib.Init.Datatypes <> ::type_scope:x_'*'_x not +R1334:1341 l1 <> location def +R1345:1345 Corelib.Numbers.BinNums <> Z ind +R3304:3307 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R3284:3287 Corelib.Init.Datatypes <> list ind +R3289:3303 l1 <> type_assumption ind +R3309:3312 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R3308:3308 l1 <> e ind +R3316:3319 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R3313:3315 l1 <> typ ind +R1407:1407 Corelib.Numbers.BinNums <> Z ind +binder 1401:1402 <> n1:34 +binder 1404:1405 <> n2:35 +R1413:1416 Corelib.Init.Datatypes <> list ind +R1427:1429 Corelib.Init.Datatypes <> ::type_scope:x_'*'_x not +R1419:1426 l1 <> location def +R1430:1430 Corelib.Numbers.BinNums <> Z ind +binder 1411:1411 <> s:36 +R1439:1439 Corelib.Numbers.BinNums <> Z ind +binder 1435:1437 <> n_5:37 +R1449:1450 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R1468:1478 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R1459:1461 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R1454:1456 Stdlib.ZArith.BinInt <> ::Z_scope:x_'+'_x not +R1452:1453 l1 <> n1:34 var +R1457:1458 l1 <> n2:35 var +R1462:1464 l1 <> n_5:37 var +R1479:1484 l1 <> reduce:30 ind +R1537:1537 l1 <> s:36 var +R1526:1530 l1 <> E_num constr +R1532:1534 l1 <> n_5:37 var +R1523:1523 l1 <> s:36 var +R1487:1490 l1 <> E_op constr +R1493:1497 l1 <> E_num constr +R1499:1500 l1 <> n1:34 var +R1503:1509 l1 <> Op_plus constr +R1512:1516 l1 <> E_num constr +R1518:1519 l1 <> n2:35 var +R1566:1566 Corelib.Numbers.BinNums <> Z ind +binder 1560:1561 <> n1:38 +binder 1563:1564 <> n2:39 +R1572:1575 Corelib.Init.Datatypes <> list ind +R1586:1588 Corelib.Init.Datatypes <> ::type_scope:x_'*'_x not +R1578:1585 l1 <> location def +R1589:1589 Corelib.Numbers.BinNums <> Z ind +binder 1570:1570 <> s:40 +R1597:1600 Corelib.Init.Datatypes <> bool ind +binder 1594:1595 <> b5:41 +R1610:1611 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R1627:1638 Corelib.Init.Logic <> ::type_scope:x_'->'_x not +R1612:1612 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R1621:1624 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R1615:1618 Stdlib.ZArith.BinInt <> ::Z_scope:x_'>='_x not +R1613:1614 l1 <> n1:38 var +R1619:1620 l1 <> n2:39 var +R1625:1626 l1 <> b5:41 var +R1639:1644 l1 <> reduce:30 ind +R1697:1697 l1 <> s:40 var +R1686:1691 l1 <> E_bool constr +R1693:1694 l1 <> b5:41 var +R1683:1683 l1 <> s:40 var +R1647:1650 l1 <> E_op constr +R1653:1657 l1 <> E_num constr +R1659:1660 l1 <> n1:38 var +R1663:1669 l1 <> Op_gteq constr +R1672:1676 l1 <> E_num constr +R1678:1679 l1 <> n2:39 var diff --git a/examples/1Bsemantics/l1.lean b/examples/1Bsemantics/l1.lean new file mode 100644 index 0000000..f6ee0ba --- /dev/null +++ b/examples/1Bsemantics/l1.lean @@ -0,0 +1,188 @@ +/- generated by Ott 0.34 from: l1.ott -/ + + + + +set_option linter.unusedVariables false + +open Option + +def Location := String /- Store locations -/ +deriving instance BEq for Location + +inductive Operations where /- operations -/ + | op_plus : Operations + | op_gteq : Operations + + +inductive Tloc where /- types of locations -/ + | TLoc_intref : Tloc + + +inductive Expr where /- expressions -/ + | e_num : Int -> Expr + | e_bool : Bool -> Expr + | e_op : Expr -> Operations -> Expr -> Expr + | e_if : Expr -> Expr -> Expr -> Expr + | e_assign : Location -> Expr -> Expr + | e_ref : Location -> Expr + | e_skip : Expr + | e_sequence : Expr -> Expr -> Expr + | e_while : Expr -> Expr -> Expr + + +def Type_assumption := (Location×Tloc) + + +inductive Typ where /- types -/ + | t_int : Typ + | t_bool : Typ + | t_unit : Typ + +open Operations Expr Typ Tloc + +/- - subrules - -/ +def is_v_of_expr (e_5:Expr) : Bool := + match e_5 with + | (e_num n) => (true) + | (e_bool b) => (true) + | (e_op e1 op e2) => false + | (e_if e1 e2 e3) => false + | (e_assign l e) => false + | (e_ref l) => false + | e_skip => (true) + | (e_sequence e1 e2) => false + | (e_while e1 e2) => false + + +/- definitions -/ + + +/- defns Jop -/ +inductive reduce : (Expr × Store) -> (Expr × Store) -> Prop where /- defn reduce -/ +| op_plus: forall (n1:Int) (n2:Int) (s:List (Location × Int)) (n:Int), +( ( n1 + n2 = n ) ) + -> +reduce ( (e_op (e_num n1) op_plus (e_num n2)) , s ) ( (e_num n) , s ) + +| op_gteq: forall (n1:Int) (n2:Int) (s:List (Location × Int)) (b:Bool), +( (( n1 >= n2 )= b ) ) + -> +reduce ( (e_op (e_num n1) op_gteq (e_num n2)) , s ) ( (e_bool b) , s ) + +| op1: forall (e1:Expr) (op:Operations) (e2:Expr) (s:List (Location × Int)) (e1':Expr) (s':List (Location × Int)), +(reduce ( e1 , s ) ( e1' , s' ) ) + -> +reduce ( (e_op e1 op e2) , s ) ( (e_op e1' op e2) , s' ) + +| op2: forall (e1:Expr) (op:Operations) (e2:Expr) (s:List (Location × Int)) (e2':Expr) (s':List (Location × Int)), +(reduce ( e2 , s ) ( e2' , s' ) ) + -> +reduce ( (e_op e1 op e2) , s ) ( (e_op e1 op e2') , s' ) + +| deref: forall (l:Location) (s:List (Location × Int)) (n:Int), +( (List.lookup l s = some ( n )) ) + -> +reduce ( (e_ref l) , s ) ( (e_num n) , s ) + +| assign1: forall (l:Location) (n:Int) (s:List (Location × Int)), +true + -> +reduce ( (e_assign l (e_num n)) , s ) ( e_skip , (( l , n ):: s ) ) + +| assign2: forall (l:Location) (e:Expr) (s:List (Location × Int)) (e':Expr) (s':List (Location × Int)), +(reduce ( e , s ) ( e' , s' ) ) + -> +reduce ( (e_assign l e) , s ) ( (e_assign l e') , s' ) + +| seq1: forall (e:Expr) (s:List (Location × Int)), +true + -> +reduce ( (e_sequence e_skip e) , s ) ( e , s ) + +| seq2: forall (e1:Expr) (e2:Expr) (s:List (Location × Int)) (e1':Expr) (s':List (Location × Int)), +(reduce ( e1 , s ) ( e1' , s' ) ) + -> +reduce ( (e_sequence e1 e2) , s ) ( (e_sequence e1' e2) , s' ) + +| if1: forall (e1:Expr) (e2:Expr) (s:List (Location × Int)), +true + -> +reduce ( (e_if (e_bool true ) e1 e2) , s ) ( e1 , s ) + +| if2: forall (e1:Expr) (e2:Expr) (s:List (Location × Int)), +true + -> +reduce ( (e_if (e_bool false ) e1 e2) , s ) ( e2 , s ) + +| if3: forall (e:Expr) (e1:Expr) (e2:Expr) (s:List (Location × Int)) (e':Expr) (s':List (Location × Int)), +(reduce ( e , s ) ( e' , s' ) ) + -> +reduce ( (e_if e e1 e2) , s ) ( (e_if e' e1 e2) , s' ) + +| while: forall (e1:Expr) (e2:Expr) (s:List (Location × Int)), +true + -> +reduce ( (e_while e1 e2) , s ) ( (e_if e1 ( (e_sequence e2 (e_while e1 e2)) ) e_skip) , s ) + + +inductive typing : (List Type_assumption) -> Expr -> Typ -> Prop where /- defn typing -/ +| Ty_int: forall (G:(List Type_assumption)) (n:Int), +true + -> +typing G (e_num n) t_int + +| Ty_bool: forall (G:(List Type_assumption)) (b:Bool), +true + -> +typing G (e_bool b) t_bool + +| Ty_op_plus: forall (G:(List Type_assumption)) (e1:Expr) (e2:Expr), +(typing G e1 t_int) -> +(typing G e2 t_int) + -> +typing G (e_op e1 op_plus e2) t_int + +| Ty_op_gteq: forall (G:(List Type_assumption)) (e1:Expr) (e2:Expr), +(typing G e1 t_int) -> +(typing G e2 t_int) + -> +typing G (e_op e1 op_gteq e2) t_bool + +| Ty_if: forall (G:(List Type_assumption)) (e1:Expr) (e3:Expr) (T:Typ) (e2:Expr), +(typing G e1 t_bool) -> +(typing G e2 T) -> +(typing G e3 T) + -> +typing G (e_if e1 e1 e3) T + +| Ty_assign: forall (G:(List Type_assumption)) (l:Location) (e:Expr), +( (List.lookup l G = some ( TLoc_intref )) ) -> +(typing G e t_int) + -> +typing G (e_assign l e) t_unit + +| Ty_deref: forall (G:(List Type_assumption)) (l:Location), +( (List.lookup l G = some ( TLoc_intref )) ) + -> +typing G (e_ref l) t_int + +| Ty_skip: forall (G:(List Type_assumption)), +true + -> +typing G e_skip t_unit + +| Ty_seq: forall (G:(List Type_assumption)) (e1:Expr) (e2:Expr) (T:Typ), +(typing G e1 t_unit) -> +(typing G e2 T) + -> +typing G (e_sequence e1 e2) T + +| Ty_while: forall (G:(List Type_assumption)) (e1:Expr) (e2:Expr), +(typing G e1 t_bool) -> +(typing G e2 t_unit) + -> +typing G (e_while e1 e2) t_unit + + + diff --git a/examples/1Bsemantics/l1.ott b/examples/1Bsemantics/l1.ott index 0f6a8e0..4ee89a1 100644 --- a/examples/1Bsemantics/l1.ott +++ b/examples/1Bsemantics/l1.ott @@ -9,49 +9,68 @@ Open Scope string. }} +embed {{ lean +set_option linter.unusedVariables false + +open Option +}} + metavar n ::= {{ com Numeric literals }} {{ phantom }} {{ lex numeric }} {{ lem integer }} + {{ lean Int }} {{ coq Z }} -metavar location, l ::= +metavar Location {{ lean Location }}, l ::= {{ com Store locations }} {{ lem string }} + {{ coq stringb }} + {{ lean String }} + {{ lean-equality }} + +% think idiomatic Lean to capitalise that, but with `metavar location {{ lean Location }}` it hits a bug in which the lean hom isn't respected in the inductive rule printing, so I've just capitalised the metavar for now - which will probably be bad for other targets {{ coq string }} grammar -b :: 'B_' ::= {{ com booleans }} {{ phantom }} {{ lem bool }} {{ coq bool }} - | true :: :: true {{ lem true }} {{ coq true }} - | false :: :: false {{ lem false }} {{ coq false }} +b :: 'B_' ::= {{ com booleans }} {{ phantom }} {{ lem bool }} {{ coq bool }} {{ lean Bool }} + | true :: :: true {{ lem true }} {{ coq true }} {{ lean true }} + | false :: :: false {{ lem false }} {{ coq false }} {{ lean false }} -operations, op :: 'Op_' ::= {{ com operations }} +% is it nice to deeply embed the L1 bools like this or not? + +operations {{ lean Operations }}, op :: 'op_' ::= {{ com operations }} | + :: :: plus | >= :: :: gteq -e :: 'E_' ::= {{ com expressions }} +% all the other languages have constructors capitalised, but in Lean it seems conventional to have them lower-case. Ott doesn't support per-target constructor name prefixes, so in this file I've lower-cased them all for now. + +expr {{ lean Expr }}, e :: 'e_' ::= {{ com expressions }} | n :: :: num | b :: :: bool | e1 op e2 :: :: op | if e1 then e2 else e3 :: :: if - | l := e :: :: assign + | l := e1 :: :: assign | ! l :: :: ref | skip :: :: skip | e1 ; e2 :: :: sequence | while e1 do e2 :: :: while - | ( e ) :: M :: paren {{ ichlo ([[e]]) }} + | ( e ) :: M :: paren {{ ichlo ([[e]]) }} {{ lean ([[e]]) }} v :: 'V_' ::= {{ com values }} | n :: :: num | b :: :: bool | skip :: :: skip -store , s :: 'Store_' ::= {{ com stores }} {{ phantom }} {{ lem list (location * integer) }} {{ coq list (location * Z) }} - | empty :: :: empty {{ lem [] }} {{ coq [] }} - | s , l |-> n :: :: extend {{ lem (([[l]],[[n]])::[[s]]) }} {{ coq (([[l]],[[n]])::[[s]]) }} +store {{ lean Store }}, s :: 'store_' ::= {{ com stores }} {{ lem list (Location * integer) }} {{ coq list (Location * Z) }} {{ lean List (Location × Int) }} + | empty :: :: empty {{ lem [] }} {{ coq [] }} {{ lean [] }} + | s , l |-> n :: :: extend {{ lem (([[l]],[[n]])::[[s]]) }} {{ coq (([[l]],[[n]])::[[s]]) }} {{ lean (([[l]],[[n]])::[[s]]) }} -typ, T :: 'T_' ::= {{ com types }} +config {{ lean Config }}, c :: 'Config_' ::= {{ com configurations }} {{lem (expr*store) }} {{ coq (expr * store) }} {{ lean ([[Expr]] × [[Store]]) }} + | < e , s > :: :: config {{ lem ([[e]], [[s]]) }} {{ coq ([[e]], [[s]]) }} {{ lean ([[e]], [[s]]) }} + +typ {{ lean Typ }}, T :: 't_' ::= {{ com types }} | int :: :: int | bool :: :: bool | unit :: :: unit @@ -60,12 +79,12 @@ Tloc {{ isa tloc }} {{ coq tloc }} {{ hol tloc }} {{ lem tloc }} {{ ocaml tloc } | intref :: :: intref -type_assumption, ta :: 'TA_' ::= {{ com type assumption }} - | l : Tloc :: :: loc +type_assumption {{ lean Type_assumption }}, ta :: 'TA_' ::= {{ com type assumption }} {{ lean ([[Location]]×[[Tloc]]) }} + | l : Tloc :: :: loc {{ lean ([[l]], [[Tloc]]) }} -G {{ tex \Gamma }} :: G_ ::= {{ com type environments }} {{ phantom }} {{ lem list type_assumption }} {{ coq list type_assumption }} - | empty :: :: empty {{ lem [] }} {{ coq [] }} - | G , ta :: :: extend {{ lem ([[ta]]::[[G]]) }} {{ coq ([[ta]]::[[G]]) }} +G {{ tex \Gamma }} :: G_ ::= {{ com type environments }} {{ phantom }} {{ lem list type_assumption }} {{ coq list type_assumption }} {{ lean (List Type_assumption) }} + | empty :: :: empty {{ lem [] }} {{ coq [] }} {{ lean [] }} + | G , ta :: :: extend {{ lem ([[ta]]::[[G]]) }} {{ coq ([[ta]]::[[G]]) }} {{ lean ([[ta]]::[[G]]) }} terminals :: terminals_ ::= @@ -78,19 +97,21 @@ terminals :: terminals_ ::= | < :: :: la {{ tex \langle }} | > :: :: ra {{ tex \rangle }} +% for proof, would one really want subrules to generate functions, as Ott does, or more inductive relations? + subrules v <:: e grammar formula :: formula_ ::= | judgement :: :: judgement - | n1 + n2 = n3 :: :: sum {{ lem ([[n1]]+[[n2]]=[[n3]]) }} {{ coq ([[n1]]+[[n2]]=[[n3]]) }} - | n1 >= n2 = b :: :: leq {{ lem ([[n1]]>=[[n2]]=[[b]]) }} {{ coq ([[n1]]>=[[n2]]=[[b]]) }} - | s ( l ) = n :: :: lookup {{ lem (List.lookup [[l]] [[s]] =Just ([[n]])) }} {{ coq (List.lookup [[l]] [[s]] =Just ([[n]])) }} - | G ( l ) = Tloc :: :: type_lookup {{ lem (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }} {{ coq (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }} + | n1 + n2 = n3 :: :: sum {{ lem ([[n1]]+[[n2]]=[[n3]]) }} {{ coq ([[n1]]+[[n2]]=[[n3]]) }} {{ lean ([[n1]]+[[n2]]=[[n3]]) }} + | n1 >= n2 = b :: :: leq {{ lem ([[n1]]>=[[n2]]=[[b]]) }} {{ coq ([[n1]]>=[[n2]]=[[b]]) }} {{ lean (([[n1]]>=[[n2]])=[[b]]) }} + | s ( l ) = n :: :: lookup {{ lem (List.lookup [[l]] [[s]] =Just ([[n]])) }} {{ coq (List.lookup [[l]] [[s]] =Some ([[n]])) }} {{ lean (List.lookup [[l]] [[s]] = some ([[n]])) }} + | G ( l ) = Tloc :: :: type_lookup {{ lem (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }} {{ coq (lookup_location_type [[l]] [[G]] = Some ([[Tloc]])) }} {{ lean (List.lookup [[l]] [[G]] = some ([[Tloc]])) }} -% this is a bit ugly - to capture the different use of Gamma in L1 and L2 we have a list of a Lem variant type and two special-purpose lookup functions, with a wildcard pattern match in each. +% this is a bit ugly - to capture the different use of Gamma in L1 and L2 we have a list of a Lem variant type and two special-purpose lookup functions, with a wildcard pattern match in each. Not currently implemented for Lean. embed {{ lem let rec lookup_location_type l g = @@ -108,7 +129,7 @@ Jop :: '' ::= % Reductions. Want to allow lem hom to specify witness and animation info defn -< e , s > -> < e' , s' > :: :: reduce :: '' {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\langle[[e']],\,[[s']]\rangle$ }} by +c -> c' :: :: Reduce :: '' {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\langle[[e']],\,[[s']]\rangle$ }} by n1 + n2 = n ---------------------- :: op_plus @@ -160,7 +181,7 @@ defn defn -G |- e : T :: :: typing :: Ty_ by +G |- e : T :: :: Typing :: ty_ by ------------------ :: int G |- n : int diff --git a/examples/1Bsemantics/l1.v b/examples/1Bsemantics/l1.v new file mode 100644 index 0000000..bd08adf --- /dev/null +++ b/examples/1Bsemantics/l1.v @@ -0,0 +1,125 @@ +(* generated by Ott 0.34 from: l1.ott *) + +Require Import Arith. +Require Import Bool. +Require Import List. +Require Import Ott.ott_list_core. + + +Definition Location : Set := somestringtype. (* Store locations *) + +Inductive operations : Set := (* operations *) + | op_plus : operations + | op_gteq : operations. + +Inductive tloc : Set := (* types of locations *) + | TLoc_intref : tloc. + +Inductive expr : Set := (* expressions *) + | e_num (n5:someZarithtype) + | e_bool (b5:bool) + | e_op (e1:expr) (op:operations) (e2:expr) + | e_if (e1:expr) (e2:expr) (e3:expr) + | e_assign (l:Location) (e:expr) + | e_ref (l:Location) + | e_skip : expr + | e_sequence (e1:expr) (e2:expr) + | e_while (e1:expr) (e2:expr). + +Inductive type_assumption : Set := (* type assumption *) + | TA_loc (l:Location) (tloc5:tloc). + +Inductive typ : Set := (* types *) + | t_int : typ + | t_bool : typ + | t_unit : typ. + +(** subrules *) +Definition is_v_of_expr (e_5:expr) : bool := + match e_5 with + | (e_num n5) => (true) + | (e_bool b5) => (true) + | (e_op e1 op e2) => false + | (e_if e1 e2 e3) => false + | (e_assign l e) => false + | (e_ref l) => false + | e_skip => (true) + | (e_sequence e1 e2) => false + | (e_while e1 e2) => false +end. + +(* definitions *) + +(* defns Jop *) +Inductive reduce : (expr * store) -> (expr * store) -> Prop := (* defn reduce *) + | op_plus : forall (n1 n2:someZarithtype) (s:list (Location * integer)) (n_5:someZarithtype), + ( n1 + n2 = n_5 ) -> + reduce ( (e_op (e_num n1) op_plus (e_num n2)) , s ) ( (e_num n_5) , s ) + | op_gteq : forall (n1 n2:someZarithtype) (s:list (Location * integer)) (b5:bool), + ( n1 >= n2 = b5 ) -> + reduce ( (e_op (e_num n1) op_gteq (e_num n2)) , s ) ( (e_bool b5) , s ) + | op1 : forall (e1:expr) (op:operations) (e2:expr) (s:list (Location * integer)) (e1':expr) (s':list (Location * integer)), + reduce ( e1 , s ) ( e1' , s' ) -> + reduce ( (e_op e1 op e2) , s ) ( (e_op e1' op e2) , s' ) + | op2 : forall (e1:expr) (op:operations) (e2:expr) (s:list (Location * integer)) (e2':expr) (s':list (Location * integer)), + reduce ( e2 , s ) ( e2' , s' ) -> + reduce ( (e_op e1 op e2) , s ) ( (e_op e1 op e2') , s' ) + | deref : forall (l:Location) (s:list (Location * integer)) (n5:someZarithtype), + (List.lookup l s =Some ( n5 )) -> + reduce ( (e_ref l) , s ) ( (e_num n5) , s ) + | assign1 : forall (l:Location) (n5:someZarithtype) (s:list (Location * integer)), + reduce ( (e_assign l (e_num n5)) , s ) ( e_skip , (( l , n5 ):: s ) ) + | assign2 : forall (l:Location) (e:expr) (s:list (Location * integer)) (e':expr) (s':list (Location * integer)), + reduce ( e , s ) ( e' , s' ) -> + reduce ( (e_assign l e) , s ) ( (e_assign l e') , s' ) + | seq1 : forall (e:expr) (s:list (Location * integer)), + reduce ( (e_sequence e_skip e) , s ) ( e , s ) + | seq2 : forall (e1 e2:expr) (s:list (Location * integer)) (e1':expr) (s':list (Location * integer)), + reduce ( e1 , s ) ( e1' , s' ) -> + reduce ( (e_sequence e1 e2) , s ) ( (e_sequence e1' e2) , s' ) + | if1 : forall (e1 e2:expr) (s:list (Location * integer)), + reduce ( (e_if (e_bool true ) e1 e2) , s ) ( e1 , s ) + | if2 : forall (e1 e2:expr) (s:list (Location * integer)), + reduce ( (e_if (e_bool false ) e1 e2) , s ) ( e2 , s ) + | if3 : forall (e e1 e2:expr) (s:list (Location * integer)) (e':expr) (s':list (Location * integer)), + reduce ( e , s ) ( e' , s' ) -> + reduce ( (e_if e e1 e2) , s ) ( (e_if e' e1 e2) , s' ) + | while : forall (e1 e2:expr) (s:list (Location * integer)), + reduce ( (e_while e1 e2) , s ) ( (e_if e1 ( (e_sequence e2 (e_while e1 e2)) ) e_skip) , s ) +with typing : list type_assumption -> expr -> typ -> Prop := (* defn typing *) + | Ty_int : forall (G5:list type_assumption) (n5:someZarithtype), + typing G5 (e_num n5) t_int + | Ty_bool : forall (G5:list type_assumption) (b5:bool), + typing G5 (e_bool b5) t_bool + | Ty_op_plus : forall (G5:list type_assumption) (e1 e2:expr), + typing G5 e1 t_int -> + typing G5 e2 t_int -> + typing G5 (e_op e1 op_plus e2) t_int + | Ty_op_gteq : forall (G5:list type_assumption) (e1 e2:expr), + typing G5 e1 t_int -> + typing G5 e2 t_int -> + typing G5 (e_op e1 op_gteq e2) t_bool + | Ty_if : forall (G5:list type_assumption) (e1 e3:expr) (T:typ) (e2:expr), + typing G5 e1 t_bool -> + typing G5 e2 T -> + typing G5 e3 T -> + typing G5 (e_if e1 e1 e3) T + | Ty_assign : forall (G5:list type_assumption) (l:Location) (e:expr), + (lookup_location_type l G5 = Some ( TLoc_intref )) -> + typing G5 e t_int -> + typing G5 (e_assign l e) t_unit + | Ty_deref : forall (G5:list type_assumption) (l:Location), + (lookup_location_type l G5 = Some ( TLoc_intref )) -> + typing G5 (e_ref l) t_int + | Ty_skip : forall (G5:list type_assumption), + typing G5 e_skip t_unit + | Ty_seq : forall (G5:list type_assumption) (e1 e2:expr) (T:typ), + typing G5 e1 t_unit -> + typing G5 e2 T -> + typing G5 (e_sequence e1 e2) T + | Ty_while : forall (G5:list type_assumption) (e1 e2:expr), + typing G5 e1 t_bool -> + typing G5 e2 t_unit -> + typing G5 (e_while e1 e2) t_unit. + + diff --git a/out.tex b/out.tex new file mode 100644 index 0000000..109826a --- /dev/null +++ b/out.tex @@ -0,0 +1,137 @@ +% generated by Ott 0.34 from: tests/test10.ott +\documentclass[11pt]{article} +\usepackage{amsmath,amssymb} +\usepackage{supertabular} +\usepackage{geometry} +\usepackage{ifthen} +\usepackage{alltt}%hack +\geometry{a4paper,dvips,twoside,left=22.5mm,right=22.5mm,top=20mm,bottom=30mm} +\usepackage{color} +\newcommand{\ottdrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\ottdrulename{#4}}} +\newcommand{\ottusedrule}[1]{\[#1\]} +\newcommand{\ottpremise}[1]{ #1 \\} +\newenvironment{ottdefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{} +\newenvironment{ottfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}} +\newcommand{\ottfunclause}[2]{ #1 \equiv #2 \\} +\newcommand{\ottnt}[1]{\mathit{#1}} +\newcommand{\ottmv}[1]{\mathit{#1}} +\newcommand{\ottkw}[1]{\mathbf{#1}} +\newcommand{\ottsym}[1]{#1} +\newcommand{\ottcom}[1]{\text{#1}} +\newcommand{\ottdrulename}[1]{\textsc{#1}} +\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}} +\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}} +\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}} +\newcommand{\ottgrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}} +\newcommand{\ottmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}} +\newcommand{\ottrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}} +\newcommand{\ottprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$} +\newcommand{\ottfirstprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}} +\newcommand{\ottlongprodline}[2]{& & $#1$ & \multicolumn{4}{l}{$#2$}} +\newcommand{\ottfirstlongprodline}[2]{\ottlongprodline{#1}{#2}} +\newcommand{\ottbindspecprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}} +\newcommand{\ottprodnewline}{\\} +\newcommand{\ottinterrule}{\\[5.0mm]} +\newcommand{\ottafterlastrule}{\\} +\newcommand{\ottmetavars}{ +\ottmetavartabular{ + $ \mathit{var} ,\, \mathit{x} $ & \ottcom{term variable} \\ +}} + +\newcommand{\ottterm}{ +\ottrulehead{\ottnt{term} ,\ \ottnt{t}}{::=}{\ottcom{term}}\ottprodnewline +\ottfirstprodline{|}{\mathit{x}}{}{}{}{\ottcom{variable}}\ottprodnewline +\ottprodline{|}{\lambda \mathit{x} \ottsym{.} \ottnt{t}}{}{\textsf{bind}\; \mathit{x}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{lambda}}\ottprodnewline +\ottprodline{|}{\ottnt{t} \, \ottnt{t'}}{}{}{}{\ottcom{app}}\ottprodnewline +\ottprodline{|}{\ottsym{(} \ottnt{t} \ottsym{)}} {\textsf{S}}{}{}{}\ottprodnewline +\ottprodline{|}{\ottsym{\{} \ottnt{t} \ottsym{/} \mathit{x} \ottsym{\}} \ottnt{t'}} {\textsf{M}}{}{}{}} + +\newcommand{\ottval}{ +\ottrulehead{\ottnt{val} ,\ \ottnt{v}}{::=}{\ottcom{value}}\ottprodnewline +\ottfirstprodline{|}{\lambda \mathit{x} \ottsym{.} \ottnt{t}}{}{}{}{\ottcom{lambda}}} + +\newcommand{\ottterminals}{ +\ottrulehead{\ottnt{terminals}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{ \lambda }{}{}{}{}\ottprodnewline +\ottprodline{|}{ \longrightarrow }{}{}{}{}} + +\newcommand{\ottformula}{ +\ottrulehead{\ottnt{formula}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{judgement}}{}{}{}{}} + +\newcommand{\ottJop}{ +\ottrulehead{\ottnt{Jop}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{t_{{\mathrm{1}}}} \longrightarrow \ottnt{t_{{\mathrm{2}}}}}{}{}{}{\ottcom{$\ottnt{t_{{\mathrm{1}}}}$ reduces to $\ottnt{t_{{\mathrm{2}}}}$}}} + +\newcommand{\ottjudgement}{ +\ottrulehead{\ottnt{judgement}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{Jop}}{}{}{}{}} + +\newcommand{\ottuserXXsyntax}{ +\ottrulehead{\ottnt{user\_syntax}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\mathit{var}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{term}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{val}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{terminals}}{}{}{}{}} + +\newcommand{\ottgrammar}{\ottgrammartabular{ +\ottterm\ottinterrule +\ottval\ottinterrule +\ottterminals\ottinterrule +\ottformula\ottinterrule +\ottJop\ottinterrule +\ottjudgement\ottinterrule +\ottuserXXsyntax\ottafterlastrule +}} + +% defnss +% defns Jop +%% defn reduce +\newcommand{\ottdruleaxXXapp}[1]{\ottdrule[#1]{% +}{ +\ottsym{(} \lambda \mathit{x} \ottsym{.} \ottnt{t_{{\mathrm{1}}}} \ottsym{)} \, \ottnt{v_{{\mathrm{2}}}} \longrightarrow \ottsym{\{} \ottnt{v_{{\mathrm{2}}}} \ottsym{/} \mathit{x} \ottsym{\}} \ottnt{t_{{\mathrm{1}}}}}{% +{\ottdrulename{ax\_app}}{}% +}} + + +\newcommand{\ottdrulectxXXappXXfun}[1]{\ottdrule[#1]{% +\ottpremise{\ottnt{t_{{\mathrm{1}}}} \longrightarrow \ottnt{t'_{{\mathrm{1}}}}}% +}{ +\ottnt{t_{{\mathrm{1}}}} \, \ottnt{t} \longrightarrow \ottnt{t'_{{\mathrm{1}}}} \, \ottnt{t}}{% +{\ottdrulename{ctx\_app\_fun}}{}% +}} + + +\newcommand{\ottdrulectxXXappXXarg}[1]{\ottdrule[#1]{% +\ottpremise{\ottnt{t_{{\mathrm{1}}}} \longrightarrow \ottnt{t'_{{\mathrm{1}}}}}% +}{ +\ottnt{v} \, \ottnt{t_{{\mathrm{1}}}} \longrightarrow \ottnt{v} \, \ottnt{t'_{{\mathrm{1}}}}}{% +{\ottdrulename{ctx\_app\_arg}}{}% +}} + +\newcommand{\ottdefnreduce}[1]{\begin{ottdefnblock}[#1]{$\ottnt{t_{{\mathrm{1}}}} \longrightarrow \ottnt{t_{{\mathrm{2}}}}$}{\ottcom{$\ottnt{t_{{\mathrm{1}}}}$ reduces to $\ottnt{t_{{\mathrm{2}}}}$}} +\ottusedrule{\ottdruleaxXXapp{}} +\ottusedrule{\ottdrulectxXXappXXfun{}} +\ottusedrule{\ottdrulectxXXappXXarg{}} +\end{ottdefnblock}} + + +\newcommand{\ottdefnsJop}{ +\ottdefnreduce{}} + +\newcommand{\ottdefnss}{ +\ottdefnsJop +} + +\newcommand{\ottall}{\ottmetavars\\[0pt] +\ottgrammar\\[5.0mm] +\ottdefnss} + +\begin{document} +\ottall + +\begin{verbatim} +Definition rules: 3 good 0 bad +Definition rule clauses: 5 good 0 bad +\end{verbatim} +\end{document} diff --git a/out.thy b/out.thy new file mode 100644 index 0000000..4e6f6a7 --- /dev/null +++ b/out.thy @@ -0,0 +1,49 @@ +(* generated by Ott 0.34 from: tests/test10.ott *) +theory out +imports Main +begin + +type_synonym "var" = "string" \ \term variable\ +datatype "term" = \ \term\ + t_var "var" \ \variable\ + | t_lam "var" "term" \ \lambda\ + | t_app "term" "term" \ \app\ + + +(** subrules *) +primrec +is_val_of_term :: "term => bool" +where +"is_val_of_term (t_var x) = (False)" +| "is_val_of_term (t_lam x t) = ((True))" +| "is_val_of_term (t_app t t') = (False)" + + +(** substitutions *) +primrec +tsubst_term :: "term => var => term => term" +where +"tsubst_term t5 x5 (t_var x) = ((if x=x5 then t5 else (t_var x)))" +| "tsubst_term t5 x5 (t_lam x t) = (t_lam x (if x5 : set [x] then t else (tsubst_term t5 x5 t)))" +| "tsubst_term t5 x5 (t_app t t') = (t_app (tsubst_term t5 x5 t) (tsubst_term t5 x5 t'))" + +(** definitions *) +(* defns Jop *) +inductive reduce :: "term \ term \ bool" +where +(* defn reduce *) + +ax_appI: "\is_val_of_term v2\ \ +reduce ((t_app (t_lam x t1) v2)) ( (tsubst_term v2 x t1 ) )" + +| ctx_app_funI: "\reduce (t1) (t1')\ \ +reduce ((t_app t1 t)) ((t_app t1' t))" + +| ctx_app_argI: "\is_val_of_term v ; +reduce (t1) (t1')\ \ +reduce ((t_app v t1)) ((t_app v t1'))" + +end + + + diff --git a/out.v b/out.v new file mode 100644 index 0000000..ee420d4 --- /dev/null +++ b/out.v @@ -0,0 +1,61 @@ +(* generated by Ott 0.34 from: tests/test10.ott *) + +Require Import Arith. +Require Import Bool. +Require Import List. +Require Import Ott.ott_list_core. + + +Definition var : Set := nat. (* term variable *) +Lemma eq_var: forall (x y : var), {x = y} + {x <> y}. +Proof. + decide equality; auto with ott_coq_equality arith. +Defined. +#[export] Hint Resolve eq_var : ott_coq_equality. + +Inductive term : Set := (* term *) + | t_var (x:var) (* variable *) + | t_lam (x:var) (t:term) (* lambda *) + | t_app (t:term) (t':term) (* app *). + +(** subrules *) +Definition is_val_of_term (t5:term) : bool := + match t5 with + | (t_var x) => false + | (t_lam x t) => (true) + | (t_app t t') => false +end. + +(** library functions *) +Fixpoint list_mem A (eq:forall a b:A,{a=b}+{a<>b}) (x:A) (l:list A) {struct l} : bool := + match l with + | nil => false + | cons h t => if eq h x then true else list_mem A eq x t +end. +Arguments list_mem [A] _ _ _. + + +(** substitutions *) +Fixpoint tsubst_term (t5:term) (x5:var) (t_6:term) {struct t_6} : term := + match t_6 with + | (t_var x) => (if eq_var x x5 then t5 else (t_var x)) + | (t_lam x t) => t_lam x (if list_mem eq_var x5 (cons x nil) then t else (tsubst_term t5 x5 t)) + | (t_app t t') => t_app (tsubst_term t5 x5 t) (tsubst_term t5 x5 t') +end. + +(* definitions *) + +(* defns Jop *) +Inductive reduce : term -> term -> Prop := (* defn reduce *) + | ax_app : forall (x:var) (t1 v2:term), + Is_true (is_val_of_term v2) -> + reduce (t_app (t_lam x t1) v2) (tsubst_term v2 x t1 ) + | ctx_app_fun : forall (t1 t t1':term), + reduce t1 t1' -> + reduce (t_app t1 t) (t_app t1' t) + | ctx_app_arg : forall (v t1 t1':term), + Is_true (is_val_of_term v) -> + reduce t1 t1' -> + reduce (t_app v t1) (t_app v t1'). + + diff --git a/outScript.sml b/outScript.sml new file mode 100644 index 0000000..84d5821 --- /dev/null +++ b/outScript.sml @@ -0,0 +1,64 @@ +(* generated by Ott 0.34 from: tests/test10.ott *) +(* to compile: Holmake outTheory.uo *) +(* for interactive use: + app load ["pred_setTheory","finite_mapTheory","stringTheory","containerTheory","ottLib"]; +*) + +open HolKernel boolLib Parse bossLib ottLib; +infix THEN THENC |-> ## ; +local open arithmeticTheory stringTheory containerTheory pred_setTheory listTheory + finite_mapTheory in end; + +val _ = new_theory "out"; + +Type var = ``:string`` (* term variable *) +val _ = Hol_datatype ` +term := (* term *) + t_var of var (* variable *) + | t_lam of var => term (* lambda *) + | t_app of term => term (* app *) +`; + +(** subrules *) +val _ = ottDefine "is_val_of_term" ` + ( is_val_of_term (t_var x) = F) +/\ ( is_val_of_term (t_lam x t) = (T)) +/\ ( is_val_of_term (t_app t t') = F) +`; + +(** substitutions *) +val _ = ottDefine "tsubst_term" ` + ( tsubst_term t5 x5 (t_var x) = (if x=x5 then t5 else (t_var x))) +/\ ( tsubst_term t5 x5 (t_lam x t) = t_lam x (if MEM x5 [x] then t else (tsubst_term t5 x5 t))) +/\ ( tsubst_term t5 x5 (t_app t t') = t_app (tsubst_term t5 x5 t) (tsubst_term t5 x5 t')) +`; +(** definitions *) + +(* defns Jop *) +Inductive Jop: +(* defn reduce *) + +[ax_app:] (! (x:var) (t1:term) (v2:term) . +(clause_name "ax_app") /\ +((is_val_of_term v2)) + ==> +( ( reduce (t_app (t_lam x t1) v2) (tsubst_term v2 x t1 ) ))) + +[ctx_app_fun:] (! (t1:term) (t:term) (t1':term) . +(clause_name "ctx_app_fun") /\ +(( ( reduce t1 t1' ))) + ==> +( ( reduce (t_app t1 t) (t_app t1' t) ))) + +[ctx_app_arg:] (! (v:term) (t1:term) (t1':term) . +(clause_name "ctx_app_arg") /\ +((is_val_of_term v) /\ +( ( reduce t1 t1' ))) + ==> +( ( reduce (t_app v t1) (t_app v t1') ))) +End + +val _ = export_theory (); + + + diff --git a/revision_history.txt b/revision_history.txt index 9223f06..29e0af4 100644 --- a/revision_history.txt +++ b/revision_history.txt @@ -581,3 +581,5 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l 2024-12 @palmskog: only output plain comments in generated Coq code 2024-12-30 Version 0.34 + +2026-02-15 Peter Sewell: rudimentary Lean backend (generates well-typed Lean for examples/1Bsemantics/l1.ott; untested and probably broken for anything else) diff --git a/src/auxl.ml b/src/auxl.ml index 88ee363..b4a5e55 100644 --- a/src/auxl.ml +++ b/src/auxl.ml @@ -48,6 +48,7 @@ let mode_name m = match m with | Hol _ -> "HOL" | Lem _ -> "Lem" | Coq _ -> "Coq" + | Lean _ -> "Lean" | Twf _ -> "Twelf" | Caml _ -> "OCaml" | Lex _ -> "Lex" @@ -602,6 +603,7 @@ let hom_name_for_pp_mode m | Isa _ -> "isa" | Hol _ -> "hol" | Lem _ -> "lem" + | Lean _ -> "lean" | Coq _ -> "coq" | Twf _ -> "twf" | Caml _ -> "ocaml" @@ -629,6 +631,9 @@ let hom_spec_for_hom_name hn homs = let hom_spec_for_pp_mode m homs = hom_spec_for_hom_name (hom_name_for_pp_mode m) homs +let hom_spec_for_pp_mode_dash_type m homs = + hom_spec_for_hom_name (hom_name_for_pp_mode m ^ "-type") homs + let loc_of_symterm st = match st with | St_node (l,_) -> l | St_nonterm (l,_,_) -> l @@ -818,6 +823,7 @@ let split3 (l : ('a * 'b * 'c) list) : 'a list * 'b list * 'c list = let big_line_comment m s = match m with | Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> "(** "^s^" *)\n" + | Lean _ -> "/- - "^s^" - -/\n" | Twf _ -> "%%% "^s^" %%%\n\n" | Tex _ -> "% "^s^"\n" | Menhir _ | Lex _ | Ascii _ -> errorm m "big_line_comment" @@ -1604,7 +1610,7 @@ let pp_true m in_prop = else "true" | Hol _ -> "T" | Caml _ -> "true" - | Lem _ -> "true" + | Lem _ | Lean _ -> "true" | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_true" let pp_false m in_prop = @@ -1616,7 +1622,7 @@ let pp_false m in_prop = else "false" | Hol _ -> "F" | Caml _ -> "false" - | Lem _ -> "false" + | Lem _ | Lean _ -> "false" | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_false" let pp_and m in_prop = @@ -1629,6 +1635,7 @@ let pp_and m in_prop = then " /\\ " else " && " | Hol _ -> " /\\ " + | Lean _ -> " /\\ " | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_and" let pp_or m in_prop = @@ -1639,6 +1646,7 @@ let pp_or m in_prop = then " \\/ " else " || " | Hol _ -> " \\/ " + | Lean _ -> " \\/ " | Caml _ -> " || " | Lem _ -> " || " | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_or" @@ -1684,7 +1692,7 @@ let insert_append m l = ^ ( String.concat " <- " (List.map2 (fun s nl -> s ^ " " ^ nl) l list_nl) ) ^ final_append ) - | Caml _ | Tex _ | Ascii _ | Hol _ | Lem _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Caml _ | Tex _ | Ascii _ | Hol _ | Lem _ | Lean _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen (* skip a nonterm or a metavar in a list of elements *) let rec skip_nt_mv (es:element list) = diff --git a/src/context_pp.ml b/src/context_pp.ml index 0bcf113..3d87ad3 100644 --- a/src/context_pp.ml +++ b/src/context_pp.ml @@ -101,7 +101,7 @@ let pp_prod_context m xd lookup (hole:nonterm) (target:nontermroot) (r:rule) (p: let lhs_pat = Grammar_pp.pp_symterm m xd sie de lhs_st in let lhs = ( match m with - | Coq _ | Caml _ -> lhs_pat + | Coq _ | Lean _ | Caml _ -> lhs_pat | Isa _ | Hol _ | Lem _ | Twf _ -> lhs_pat ^ " " ^ Grammar_pp.pp_nonterm m xd hole | Lex _ | Menhir _ | Tex _ | Ascii _ -> assert false) in (* compute the rhs *) @@ -130,6 +130,12 @@ let pp_rule_context m xd lookup cr : int_func = ^ ") ("^fake_hole_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_hole ^")", "", " : " ^ (Grammar_pp.pp_nontermroot_ty m xd cr.cr_target) ^ " :=\n match "^ctx_var^" with\n") + | Lean _ -> + ((leanTODO "6" ( id + ^ " ("^ctx_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_ntr + ^ ") ("^fake_hole_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_hole ^")")), + "", + " : " ^ (Grammar_pp.pp_nontermroot_ty m xd cr.cr_target) ^ " :=\n match "^ctx_var^" with\n") | Isa _ -> ( id ^ " :: \"" ^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_ntr ^ " => " diff --git a/src/defns.ml b/src/defns.ml index 90727f6..3dd8808 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -79,7 +79,7 @@ let pp_subntr (m: pp_mode) (xd: syntaxdefn): (nontermroot * nontermroot * nonter Auxl.pp_is ntrl ntru ^ " " ^ Auxl.hide_isa_trailing_underscore m (( match m with Twf _ -> String.uppercase_ascii ntr' - | Coq _ | Isa _ | Hol _ | Lem _ -> ntr' + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ -> ntr' | Caml _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen ) ^ Grammar_pp.pp_suffix_with_sie m xd Bounds.sie_project suff) in ( match m with @@ -117,6 +117,11 @@ let pp_listsubntr : pp_mode -> syntaxdefn -> ((nontermroot * nontermroot * nonte ^ "(fun "^pp_pattern^" -> "^pp_subntr m xd subntr^") " ^ pp_squished_vars + | Lean _ -> + leanTODO "17" "List.all " + ^ "(fun "^pp_pattern^" -> "^pp_subntr m xd subntr^") " + ^ pp_squished_vars + | Coq co -> let ty_list = Str.split (Str.regexp "(\\|*\\|)") coq_type_pattern in if String.contains coq_type_pattern '*' @@ -245,7 +250,7 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = (Grammar_pp.pp_tex_DRULE_NAME_NAME m) (Auxl.pp_tex_escape dr.drule_name) pp_com - | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ -> + | Isa _ | Hol _ | Lem _ | Coq _ | Lean _ | Twf _ -> let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in (* find all the nonterms used at non-free types *) @@ -277,7 +282,7 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = List.map (pp_subntr m xd) nonlist_subntrs @ pp_listsubntr m xd list_subntrs in - (* collect all the isa/coq/hol variables that should be quantified *) + (* collect all the isa/coq/hol/lean variables that should be quantified *) (* for this clause *) let quantified_proof_assistant_vars = @@ -402,6 +407,44 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = output_string fd ppd_conclusion; output_string fd "\n\n" + + | Lean _ -> + Printf.fprintf fd "%s%s%s: " + (leanTODO "18" "") + "" (*("(*"^Location.pp_loc dr.drule_loc^"*)")*) + ("| " ^ dr.drule_name); +(* Lem currrently requires a forall even if there are no quantified variables, + and a "true ==>" if there are no premises *) +(* + (match quantified_proof_assistant_vars with + | [] -> () + | _ -> +*) + output_string fd "forall"; +(* the second version, with explicit type annotations, is pretty noisy, and probably not idiomatic. For l1.ott, we need it only for b:bool, where Lean type inference seems to get confused? *) +(* List.iter (fun (var,ty,_) -> Printf.fprintf fd " %s" (leanTODO "19" var)) + quantified_proof_assistant_vars; +*) List.iter (fun (var,ty,_) -> Printf.fprintf fd " (%s:%s)" var ty) + quantified_proof_assistant_vars; + output_string fd ",\n"; +(* +); +*) + if (snd ppd_premises)<>[] || ppd_subntrs<>[] then + begin + (* output_string fd " &&\n(";*) + iter_asep fd " ->\n" + (fun s -> output_string fd "("; output_string fd s; output_string fd ")") + (ppd_subntrs @ snd ppd_premises); + output_string fd "\n" + end + else + output_string fd "true\n"; + output_string fd " -> \n"; + output_string fd ppd_conclusion; + output_string fd "\n\n" + + | Coq co -> let rec remove_dupl l = match l with | [] -> [] @@ -484,6 +527,21 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un | Lem _ -> Printf.fprintf fd "(* defn %s *)\n\n" d.d_name; iter_sep (pp_processed_semiraw_rule fd m xd) "and\n" d.d_rules + | Lean _ -> + (*Printf.fprintf fd "/- defn %s -/\n\n" d.d_name;*) + + let prod_name = defnclass_wrapper ^ d.d_name in + + let type_defn = + let es = (Auxl.prod_of_prodname xd prod_name).prod_es in + let ss = (Auxl.option_map (Grammar_pp.pp_element m xd [] true) es) in + match ss with + | [] -> universe^" :=" + | [s] -> s ^ " -> "^universe^" :=" + | _ -> String.concat " -> " ss ^ " -> " ^ universe^" where" in + Printf.fprintf fd "%s%s : %s /- defn %s -/\n" defnclass_wrapper d.d_name type_defn d.d_name; + iter_nosep (fun psr -> pp_processed_semiraw_rule fd m xd "" psr) d.d_rules + | Coq co -> (* FZ factor this code ? *) let prod_name = defnclass_wrapper ^ d.d_name in @@ -626,6 +684,12 @@ let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = List.iter (output_string fd) !(co.coq_list_aux_defns.newly_defined); output_string fd ".\n" + | Lean co -> + Printf.fprintf fd "\n/- defns %s -/\ninductive " dc.dc_name; + iter_asep fd "\ninductive " + (fun d -> pp_defn fd m xd lookup dc.dc_wrapper universe d) + dc.dc_defns + | Twf wo -> let twf_type_of_defn : syntaxdefn -> defn -> string = fun xd d -> @@ -669,7 +733,7 @@ let pp_funclause (m:pp_mode) (xd:syntaxdefn) (fc:funclause) : string = ppd_lhs ^ " === " ^ ppd_rhs ^ "\n" | Tex _ -> Grammar_pp.pp_tex_FUNCLAUSE_NAME m^"{"^ppd_lhs^"}"^"{"^ppd_rhs^"}%\n" - | Isa _ | Hol _ | Lem _ | Coq _ | Caml _ | Twf _ | Lex _ | Menhir _ -> + | Isa _ | Hol _ | Lem _ | Coq _ | Lean _ | Caml _ | Twf _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_funclause" let rec insert_commas l = @@ -694,7 +758,7 @@ let pp_symterm_node_lhs m xd sie de st = with Not_found -> Auxl.int_error "pp_symterm_node_lhs" in let hom = match m with - | Coq _ | Caml _ | Lem _ (* LemTODO4: really? *) -> (insert_commas hom) + | Coq _ | Lean _ | Caml _ | Lem _ (* LemTODO4: really? *) -> (insert_commas hom) | Hol _ | Isa _ -> hom | Twf _ | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen in String.concat " " (Grammar_pp.apply_hom_spec m xd hom pes) @@ -850,7 +914,7 @@ let pp_fundefn (m:pp_mode) (xd:syntaxdefn) lookup (fd:fundefn) : string = ^ "\\end{"^Grammar_pp.pp_tex_FUNDEFN_BLOCK_NAME m ^"}" ^ "}\n\n" - | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Isa _ | Hol _ | Lem _ | Coq _ | Lean _ | Twf _ | Caml _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fundefn" let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : string = @@ -873,7 +937,7 @@ let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : stri (List.map (function fd -> Grammar_pp.tex_fundefn_name m fd.fd_name^"{}") fdc.fdc_fundefns)) ^ "}\n\n" - | Isa _ | Coq _ | Hol _ | Lem _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Caml _ -> let proof = let pp_proof h = ( match h with @@ -881,7 +945,7 @@ let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : stri | None -> None | _ -> Auxl.warning (Some fdc.fdc_loc) "malformed isa-proof/hol-proof hom"; Some "<<>>" ) in ( match m with - | Coq _ | Caml _ | Lem _ -> None + | Coq _ | Caml _ | Lem _ | Lean _ -> None | Isa _ -> pp_proof (Auxl.hom_spec_for_hom_name "isa-proof" fdc.fdc_homs) | Hol _ -> pp_proof (Auxl.hom_spec_for_hom_name "hol-proof" fdc.fdc_homs) | _ -> raise Auxl.ThisCannotHappen ) in @@ -951,6 +1015,9 @@ let pp_fun_or_reln_defnclass_list | Twf _ -> output_string fd "%%% definitions %%%\n\n"; List.iter (fun frdc -> pp_fun_or_reln_defnclass fd m xd lookup frdc) frdcs + | Lean _ -> + output_string fd "/- definitions -/\n\n"; + List.iter (fun frdc -> pp_fun_or_reln_defnclass fd m xd lookup frdc) frdcs | Coq co -> pp_auxiliary_list_rules fd m xd frdcs; output_string fd "(* definitions *)\n"; diff --git a/src/dependency.ml b/src/dependency.ml index 9b1a7a2..1ffd9fe 100644 --- a/src/dependency.ml +++ b/src/dependency.ml @@ -531,6 +531,15 @@ let coq_collapse m xd funcs = (f.r_fun_id, f.r_fun_dep, (f.r_fun_header, (collapse_clauses m f.r_fun_id f.r_fun_clauses), Footer_empty)) in List.map (collapse_func m) funcs.i_funcs +let lean_collapse m xd funcs = + let collapse_clause m id (_,lhs, rhs) = + " | " ^ lhs ^ " => " ^ rhs ^ "\n" in + let collapse_clauses m id clauses = + String.concat "" (List.map (collapse_clause m id) clauses) in + let collapse_func m f = + (f.r_fun_id, f.r_fun_dep, (f.r_fun_header, (collapse_clauses m f.r_fun_id f.r_fun_clauses), Footer_empty)) in + List.map (collapse_func m) funcs.i_funcs + let twf_collapse m xd funcs = let collapse_clause m id (pfx, lhs, rhs) = "" ^ id ^ "/" ^ pfx ^ " : " ^ id ^ " " ^ lhs ^ " " ^ rhs ^ ".\n" in @@ -574,6 +583,7 @@ let collapse m xd (funcs:int_funcs) : int_funcs_collapsed = | Hol _ -> hol_collapse m xd funcs | Lem _ -> lem_collapse m xd funcs | Coq _ -> coq_collapse m xd funcs + | Lean _ -> lean_collapse m xd funcs | Twf _ -> twf_collapse m xd funcs | Caml _ -> caml_collapse m xd funcs | Tex _ | Ascii _ -> Auxl.error None "internal: collapse of Tex-Ascii\n" @@ -668,6 +678,21 @@ let print m xd (sorting,refl) = ^ "end.\n\n" in String.concat "" (List.map print_block sorting) + | Lean _ -> + let print_block block = + if ((List.length block) = 1) + then + let (nt,((h1,h2,h3),s,_)) = List.hd block in + if (List.mem nt refl) + then "def " ^ h1 ^ h2 ^ h3 ^ s ^ "\n\n" + else "def " ^ h1 ^ h3 ^ s ^ (if String.compare h3 "" = 0 then "\n\n" else "\n\n") + else + "def " + ^ (String.concat "\nwith " + (List.map (fun (_,((h1,h2,h3),s,_)) -> h1 ^ h2 ^ h3 ^ s) block)) + ^ "\n\n" in + leanTODO "21" (String.concat "" (List.map print_block sorting)) + | Twf _ -> (* PLACEHOLDER CODE *) let print_block block = diff --git a/src/embed_pp.ml b/src/embed_pp.ml index 1ab5ef9..f0d46a4 100644 --- a/src/embed_pp.ml +++ b/src/embed_pp.ml @@ -56,6 +56,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) = output_string fd Grammar_pp.pp_DOUBLERIGHTBRACE; output_string fd "\n"; | (Coq _, "coq") + | (Lean _, "lean") | (Isa _, "isa") | (Hol _, "hol") | (Lem _, "lem") @@ -72,7 +73,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) = | (Isa io, "isa-lib") -> let x = io.isa_library in x := (fst !x, embed_strings (snd !x) es) - | (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) -> () + | (Coq _, _) | (Lean _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) -> () and pp_embed_spec fd m xd lookup es = List.iter (pp_embed_spec_el fd m xd lookup) es @@ -88,7 +89,7 @@ and pp_embed_spec_el fd m xd lookup ese = output_string fd Grammar_pp.pp_DOUBLERIGHTBRACKET ) | Tex xo when (match ese with Embed_inner (_,"TEX_NAME_PREFIX")->true | _->false) -> output_string fd xo.ppt_name_prefix - | Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Tex _ | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> ( match ese with | Embed_string (l,s) -> output_string fd s diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 6743c20..723bc79 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -51,7 +51,7 @@ pp_plain_nonterm nt pp_nonterm m xd nt - gives a normal Ascii/Tex/Coq/Isa pp of nt, depending on the mode m + gives a normal Ascii/Tex/Coq/Lean/Isa pp of nt, depending on the mode m and syntax defn xd. This is only really sensible for nt which are known not to contain a suffix item of the form Si_index i. @@ -87,13 +87,14 @@ let pp_source_location m l = | Ascii _ | Tex _ -> Printf.sprintf "%% %s\n" s | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ -> Printf.sprintf "(* %s *)\n" s + | Lean _ -> Printf.sprintf "/- %s -/\n" s | Lex _ | Menhir _ -> "" (* utilities *********************************************************** *) -let list_append m = match m with | Lem _ | Hol _ -> " ++ " | _ -> " @ " +let list_append m = match m with | Lem _ | Hol _ | Lean _ -> " ++ " | _ -> " @ " let pad n s = let m = n - String.length s in @@ -884,13 +885,14 @@ and pp_dots m xd n = | 1 -> pp_tex_DOTDOTDOT | 2 -> pp_tex_DOTDOTDOTDOT | _ -> raise ThisCannotHappen ) - | Caml _ | Hol _ | Lem _ | Isa _ | Coq _ | Twf _ | Lex _ | Menhir _ -> + | Caml _ | Hol _ | Lem _ | Isa _ | Coq _ | Lean _ | Twf _ | Lex _ | Menhir _ -> raise ThisCannotHappen and pp_uninterpreted m xd s = match m with | Ascii ao -> col_cyan ao ("(*"^s^"*)") | Caml _ | Coq _ | Isa _ | Hol _ | Lem _ | Lex _ | Menhir _ -> "(*"^s^"*)" + | Lean _ -> "/-"^s^"-/" | Twf _ -> "%{"^s^"}%" | Tex _ -> let es = Auxl.pp_tex_escape s in @@ -900,13 +902,13 @@ and pp_uninterpreted m xd s = and pp_maybe_quote_ident m xd s = match m with | Ascii ao -> quote_ident s - | Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> s + | Tex _ | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> s and pp_prod_flavour m xd pf = match m with | Ascii _ -> pp_BAR | Tex _ -> pp_tex_BAR - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen and pp_plain_terminal tm = tm @@ -915,6 +917,7 @@ and pp_terminal m xd tm = | Ascii ao -> col_green ao (quote_ident tm) | Tex _ -> pp_tex_terminal m xd tm | Coq _ -> tm + | Lean _-> tm | Isa _ -> pp_isa_terminal m xd tm | Hol _ -> tm | Lem _ -> tm @@ -927,6 +930,7 @@ and pp_terminal_unquoted m xd tm = | Ascii ao -> col_green ao tm | Tex _ -> pp_tex_terminal m xd tm | Coq _ -> tm + | Lean _ -> tm | Isa _ -> pp_isa_terminal m xd tm | Hol _ -> tm | Lem _ -> tm @@ -994,7 +998,11 @@ and pp_nonterm_with_sie_internal as_type m xd sie (ntr,suff) = else begin (* the per-ntr_name hom, if any *) let homs = List.assoc ntr r.rule_ntr_names in - let hso = Auxl.hom_spec_for_pp_mode m homs in + let hso = + if as_type then + Auxl.hom_spec_for_pp_mode_dash_type m homs + else + Auxl.hom_spec_for_pp_mode m homs in let pp_ntr = match hso with | None -> capitalize_if_twelf_non_type as_type m ntr @@ -1004,7 +1012,9 @@ and pp_nonterm_with_sie_internal as_type m xd sie (ntr,suff) = let auxparam_opt = try Some (List.assoc "auxparam" r.rule_homs) with Not_found -> None in let auxparam_prefix_opt = match as_type,m,auxparam_opt with - | true,Caml _,Some hs | true,Lem _,Some hs -> Some (String.concat "" (List.map (function | Hom_string s -> s | Hom_index _ | Hom_terminal _ | Hom_ln_free_index (_,_) -> Auxl.int_error("illegal auxparam hom "^String.concat ""(List.map pp_plain_hom_spec_el hs))) hs)) + | true,Caml _,Some hs | true,Lem _,Some hs -> + Some (String.concat "" + (List.map (function | Hom_string s -> s | Hom_index _ | Hom_terminal _ | Hom_ln_free_index (_,_) -> Auxl.int_error("illegal auxparam hom "^String.concat ""(List.map pp_plain_hom_spec_el hs))) hs)) | _,_,_ -> None in match m with @@ -1029,7 +1039,7 @@ and pp_nonterm_with_sie_internal as_type m xd sie (ntr,suff) = String.concat "" (apply_hom_spec m xd hs [Auxl.pp_tex_escape ntr^(pp_suffix_with_sie m xd sie suff)])) - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> let s0 = pp_ntr ^ (pp_suffix_with_sie m xd sie suff) in let s1 = if as_type then s0 @@ -1078,7 +1088,7 @@ and pp_metavar_with_sie_internal as_type m xd sie (mvr,suff) = (apply_hom_spec m xd hs [Auxl.pp_tex_escape mvr^(pp_suffix_with_sie m xd sie suff)])) - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> let s = pp_mvr ^ (pp_suffix_with_sie m xd sie suff) in if as_type then s else Auxl.hide_isa_trailing_underscore m s @@ -1092,7 +1102,7 @@ and pp_nt_or_mv_with_sie_internal as_type m xd sie (ntmv,suff) = and pp_nt_or_mv_with_de_with_sie_internal as_type m xd sie (de :dotenv) ((ntmvr,suff0) as ntmv) = match m with | Ascii _ | Tex _ -> pp_nt_or_mv_with_sie_internal as_type m xd sie ntmv - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> let (de1,de2) = de in match try Some(List.assoc ntmv de2) with Not_found -> None with | None -> pp_nt_or_mv_with_sie m xd sie ntmv @@ -1116,6 +1126,17 @@ and pp_nt_or_mv_with_de_with_sie_internal as_type m xd sie (de :dotenv) ((ntmvr, | None -> "" | Some suffi -> " - "^pp_plain_suffix_item suffi) ^ ")))" + | Lean _ -> +leanTODO "1" ( + "((fun "^de1i.de1_pattern^" |-> "^pp_nt_or_mv_with_sie m xd ((Si_var ("_",0))::sie) (ntmvr,suff)^")" + ^ " (List.nth " ^ de1i.de1_compound_id ^ " " + ^ "(" ^ pp_plain_suffix_item suffi + ^ + (match non_zero_lower_of_bound bound with + | None -> "" + | Some suffi -> " - "^pp_plain_suffix_item suffi) + ^ ")))" +) | Hol _ -> " ((\\ "^de1i.de1_pattern^" . "^pp_nt_or_mv_with_sie m xd ((Si_var ("_",0))::sie) (ntmvr,suff)^")" ^ " (EL " ^ " " @@ -1317,6 +1338,21 @@ and pp_metavardefn m xd mvd = ^ " = " ^ pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc ^ pp_com ^ "\n" + | Lean lno -> + let type_name = pp_metavarroot_ty m xd mvd.mvd_name in + "abbrev " + (* or "def "? but then we need type class instances... *) + ^ type_name + ^ " := " + ^ pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc + ^ pp_com ^ "\n" + ^ (match + try Some (List.assoc "lean-equality" mvd.mvd_rep) with Not_found -> None + with + | None -> "" + | Some eh -> "deriving instance BEq for " ^ type_name ^ "\n" + ) + | Twf _ -> "%abbrev " ^ pp_metavarroot_ty m xd mvd.mvd_name @@ -1346,6 +1382,11 @@ and pp_metavarrep m xd mvd_rep type_name loc = let hs = List.assoc "lem" mvd_rep in pp_hom_spec m xd hs with Not_found -> Auxl.warning (Some loc) ("undefined lem metavarrep for "^type_name^"\n"); "UNDEFINED" ) + | Lean lno -> + ( try + let hs = List.assoc "lean" mvd_rep in + pp_hom_spec m xd hs + with Not_found -> Auxl.warning (Some loc) ("undefined lean metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Coq co -> ( try let hs = List.assoc "coq" mvd_rep in @@ -1402,6 +1443,7 @@ and pp_com_es m xd homs es = ^ "}" | Isa _ -> " \\ \\" ^ String.concat "" (apply_hom_spec m xd hs ss) ^ "\\" | Coq _ | Hol _ | Lem _ | Caml _ | Lex _ -> " (* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" + | Lean _ -> " /- " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " -/" | Menhir _ -> "/* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " */" | Ascii _ | Twf _ -> "" @@ -1416,6 +1458,7 @@ and pp_com_strings m xd homs ss = ^ "}" | Isa _ -> " \\ \\" ^ String.concat "" (apply_hom_spec m xd hs ss) ^ "\\" | Coq _ | Hol _ | Lem _ | Caml _ | Lex _ -> " (* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" + | Lean _ -> " /- " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " -/" | Menhir _ -> "/* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " */" | Ascii _ | Twf _ -> "" @@ -1434,7 +1477,7 @@ and pp_homomorphism m xd (hn,hs) = (* (\* raise ThisCannotHappen *\) *) (* | (Hol ho, "hol") -> (pp_hom_spec m xd hs)^"\n\n" *) (* (\* raise ThisCannotHappen *\) *) - | (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Caml _,_) | (Lex _,_) | (Menhir _, _) -> "" + | (Coq _, _) | (Lean _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Caml _,_) | (Lex _,_) | (Menhir _, _) -> "" | (Tex _, _) -> Auxl.errorm m "pp_homomorphism" and pp_homomorphism_list m xd homs = @@ -1442,7 +1485,7 @@ and pp_homomorphism_list m xd homs = | Ascii ao -> String.concat " " (List.map (pp_homomorphism m xd) homs) | Tex xo -> raise ThisCannotHappen - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen and pp_hom_name m xd hn = pp_maybe_quote_ident m xd hn @@ -1473,7 +1516,7 @@ and pp_hom_spec_el m xd hse = | Hom_terminal s -> Auxl.errorm m "pp_hom_spec_el" | Hom_index i -> "UNIMPLEMENTED" | Hom_ln_free_index _ -> Auxl.errorm m "pp_hom_spec el") - | Isa _ | Hol _ | Lem _ -> + | Isa _ | Hol _ | Lem _ | Lean _ -> ( match hse with | Hom_string s -> s | Hom_terminal s -> s @@ -1538,7 +1581,7 @@ and pp_suffix_with_sie m xd sie suff = "_{" ^ String.concat "\\," (List.map (pp_suffix_item_with_sie m xd sie true) suff_subscript) ^ "}") - | (Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _) -> + | (Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _) -> (String.concat "" (List.map (pp_suffix_item_with_sie m xd sie false) suff)) @@ -1554,7 +1597,7 @@ and pp_suffix_item_with_sie m xd sie nosubscript suffi = ( (*List.nth sie i*) try List.nth sie i with Failure _ -> Si_num "999")) in if ao.ppa_ugly then "["^s^"]" else s - | (Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _) -> + | (Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _) -> ( match suffi with | Si_num s -> s | Si_punct s -> s @@ -1694,12 +1737,12 @@ and pp_bindspec m xd sie de bs = | Tex xo -> pp_tex_BIND ^ "\\; " ^ pp_mse_string m xd sie de mse ^ "\\; " ^ pp_tex_IN ^ "\\; " ^ pp_nonterm m xd nt - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | AuxFnDef (loc,f,mse) -> ( match m with | Ascii ao -> pp_auxfn m xd f ^ "" ^ pp_EQ ^ "" ^ pp_mse_string m xd sie de mse | Tex xo -> pp_auxfn m xd f ^ "" ^ pp_tex_EQ ^ "" ^ pp_mse_string m xd sie de mse - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | NamesEqual (loc,mse,mse') -> ( match m with | Ascii ao -> @@ -1710,7 +1753,7 @@ and pp_bindspec m xd sie de bs = pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse ^ "" ^ pp_tex_RPAREN ^ "\\," ^ pp_tex_EQ ^ "\\," ^ pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' ^ "" ^ pp_tex_RPAREN - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | NamesDistinct (loc,mse,mse') -> ( match m with | Ascii ao -> @@ -1722,7 +1765,7 @@ and pp_bindspec m xd sie de bs = ^ ""^pp_tex_RPAREN ^ "\\," ^ pp_tex_HASH ^ "\\," ^ pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' ^ ""^pp_tex_RPAREN - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | AllNamesDistinct (loc,mse) -> ( match m with | Ascii ao -> @@ -1731,7 +1774,7 @@ and pp_bindspec m xd sie de bs = | Tex xo -> pp_tex_DISTINCTNAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse ^ "" ^ pp_tex_RPAREN - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) and pp_bindspec_list m xd sie de bs = match m with @@ -1750,7 +1793,7 @@ and pp_bindspec_list m xd sie de bs = (* " $ \\\\ \n &&&& $ " *) (* (List.map (pp_bindspec m xd sie de) bs)) *) (* ^ (\* " $ & \\ $ " ^*\) pp_tex_BIND_RIGHT_DELIM ) *) - | Ascii _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Ascii _ | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen and pp_plain_mse mse = match mse with @@ -1786,14 +1829,14 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter ( match m with | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse" | Ascii _ | Tex _ -> (* "\\{" ^*) pp_metavar_with_sie m xd sie mv (* ^ "\\}" *) - | Isa _ | Hol _ | Lem _ | Caml _ -> "["^pp_metavar_with_sie m xd sie mv^"]" + | Isa _ | Lean _ | Hol _ | Lem _ | Caml _ -> "["^pp_metavar_with_sie m xd sie mv^"]" | Coq _ -> "(cons " ^ pp_metavar_with_sie m xd sie mv ^ " nil)" | Twf _ -> "(natlist/cons " ^ pp_metavar_with_sie m xd sie mv ^ " natlist/nil)" ), [], [] | NonTermExp nt -> ( match m with | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse" | Ascii _ | Tex _ -> (* "\\{" ^*) pp_nonterm_with_sie m xd sie nt (* ^ "\\}" *) - | Isa _ | Hol _ | Lem _ | Caml _ -> "["^pp_nonterm_with_sie m xd sie nt^"]" + | Isa _ | Lean _ | Hol _ | Lem _ | Caml _ -> "["^pp_nonterm_with_sie m xd sie nt^"]" | Coq _ -> "(cons " ^ pp_nonterm_with_sie m xd sie nt ^ " nil)" | Twf _ -> "(natlist/cons " ^ pp_nonterm_with_sie m xd sie nt ^ " natlist/nil)" ), [], [] | MetaVarListExp (mv,b) -> @@ -1852,7 +1895,7 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter | Tex xo -> ( pp_auxfn m xd f ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_nonterm_with_sie m xd sie nt ^ "" ^ pp_tex_RPAREN ), [], [] - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ -> let ntrp = pp_nontermroot_ty m xd (Auxl.promote_ntr xd (Auxl.primary_ntr_of_ntr xd (fst nt))) in ( "(" ^ Auxl.auxfn_name f ntrp ntrp ^ " " ^ pp_nonterm_with_sie m xd sie nt^")" ), [], [] ) @@ -2033,6 +2076,7 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter | Twf _ -> raise TwelfNotImplemented | Caml _ -> ( "(List.flatten (List.map "^Auxl.auxfn_name f ntrp ntrp ^" ("^pp_ntlist^")))" ), [], [] + | Lean _ -> (leanTODO "2" ( "(List.flatten (List.map "^Auxl.auxfn_name f ntrp ntrp ^" ("^pp_ntlist^")))" )), [], [] | Lem _ -> let ntrp_s = pp_nontermroot m xd ntrp in ( lemTODO "9" " (List.concat (List.map "^Auxl.auxfn_name f ntrp_s ntrp_s ^" ("^pp_ntlist^")))" ), [], [] @@ -2156,6 +2200,7 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter f1 @ f2) | Caml _ -> ( pp_mse_string m xd sie de mse ^list_append m^ pp_mse_string m xd sie de mse' ), [], [] | Lem _ -> ( pp_mse_string m xd sie de mse ^list_append m^ pp_mse_string m xd sie de mse' ), [], [] + | Lean _ -> ( pp_mse_string m xd sie de mse ^list_append m^ pp_mse_string m xd sie de mse' ), [], [] | Hol _ -> ( "("^pp_mse_string m xd sie de mse ^list_append m^ pp_mse_string m xd sie de mse' ^")"), [], [] | Coq _ -> let (s1,d1,f1) = pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse in @@ -2169,7 +2214,7 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse" | Ascii ao -> pp_EMPTY, [], [] | Tex xo -> pp_tex_EMPTY, [], [] - | Isa _ | Hol _ | Lem _ | Caml _ -> "[]", [], [] + | Isa _ | Lean _ | Hol _ | Lem _ | Caml _ -> "[]", [], [] | Coq _ -> "nil", [], [] | Twf _ -> "natlist/nil", [], [] ) @@ -2225,7 +2270,7 @@ and pp_element m xd sie in_type e = pp_tex_LEFTBRACKET ^ " " ^ String.concat " " (Auxl.option_map (pp_element m xd sie in_type) es) ^ " " ^ pp_tex_RIGHTBRACKET ) - | Coq _ | Caml _ | Hol _ | Lem _ | Twf _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Caml _ | Hol _ | Lem _ | Twf _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | Lang_sugaroption tm -> Some (pp_terminal m xd tm) | Lang_list elb -> @@ -2256,7 +2301,7 @@ and pp_element m xd sie in_type e = | Lang_sugaroption _ | Lang_list _ -> None) - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ -> let check_conflict v t = if String.compare v t = 0 then Some "_", t @@ -2278,6 +2323,10 @@ and pp_element m xd sie in_type e = ( match pp_elements m xd sie es true false true true with | None -> None | Some s -> Some (None, "(option "^s^")") ) + | Lean _ -> + ( match pp_elements m xd sie es true false true true with + | None -> None + | Some s -> Some (None, "(option "^s^")") ) | Isa _ | Hol _ | Lem _ | Caml _ -> ( match pp_elements m xd sie es true false true true with | None -> None @@ -2298,6 +2347,10 @@ and pp_element m xd sie in_type e = ( match pp_elements m xd sie elb.elb_es true false true true with | None -> Some (None, "list unit") | Some s -> Some (None, "list "^s) ) + | Lean _ -> + ( match pp_elements m xd sie elb.elb_es true false true true with + | None -> Some (None, "List ()") + | Some s -> Some (None, "List "^s) ) | Isa _ | Hol _ -> ( match pp_elements m xd sie elb.elb_es true false true true with | None -> Some (None, "unit list") @@ -2324,6 +2377,14 @@ and pp_element m xd sie in_type e = Some ("(_:"^t^")") | Coq co, Some (v,t) when (not co.coq_names_in_rules) || in_type -> Some t + + | Lean lno, Some (Some v,t) when lno.lean_names_in_rules && (not in_type) -> + Some ("("^v^":"^t^")") + | Lean lno, Some (None,t) when lno.lean_names_in_rules && (not in_type) -> + Some ("(_:"^t^")") + | Lean lno, Some (v,t) when (not lno.lean_names_in_rules) || in_type -> + Some t + | _, Some (v,t) -> Some t) @@ -2331,7 +2392,7 @@ and pp_elements m xd sie es paren toplevel in_list in_type = match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> Some (String.concat " " (Auxl.option_map (pp_element m xd sie in_type) es) ) - | Coq _ | Caml _ | Lem _ -> + | Coq _ | Lean _ | Caml _ | Lem _ -> lemTODOmo m "10" (*really? *) ( let ss = (Auxl.option_map (pp_element m xd sie in_type) es) in let separator = @@ -2339,11 +2400,13 @@ and pp_elements m xd sie es paren toplevel in_list in_type = ( match m with | Caml _ | Lem _ -> " * " | Coq co when co.coq_expand_lists -> "_" - | Coq co when not (co.coq_expand_lists) -> "*" + | Coq co when not (co.coq_expand_lists) -> "*" + | Lean _ -> " × " | _ -> "_" ) else ( match m with | Coq co when co.coq_names_in_rules -> " " + | Lean lno when lno.lean_names_in_rules -> " -> " | _ -> " -> " ) in let s = String.concat separator ss in ( match List.length ss with @@ -2510,6 +2573,14 @@ and pp_prod m xd rnn rpw p = (* returns a string option *) if co.coq_names_in_rules then Some (" | " ^ p.prod_name ^ " " ^ s ^ pp_com) else Some (" | " ^ p.prod_name ^ " : " ^ s ^ " -> " ^ pp_nontermroot_ty m xd rnn ^ pp_com) ) + | Lean _ -> + if p.prod_meta then + None + else + ( match pp_elements m xd [] (apply_hom_order m xd p) (*p.prod_es*) false true false false with + | None -> Some (" | " ^ p.prod_name ^ " : " ^ pp_nontermroot_ty m xd rnn ^ pp_com) + | Some s -> + Some (" | " ^ p.prod_name ^ " : " ^ s ^ " -> " ^ pp_nontermroot_ty m xd rnn ^ pp_com) ) | Twf _ -> if p.prod_meta then None @@ -2629,14 +2700,14 @@ and pp_rule m xd r = (* returns a string option *) (pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper) r.rule_ps)) ^ "") - | Hol _ | Lem _| Caml _ -> + | Hol _ | Lem _ | Lean _ | Caml _ -> if r.rule_meta || r.rule_phantom then None else Some - (strip_surrounding_parens (pp_nontermroot_ty m xd r.rule_ntr_name) ^ " = "^pp_com^"\n" + (strip_surrounding_parens (pp_nontermroot_ty m xd r.rule_ntr_name) ^ (match m with Lean _ -> " where" | _ -> " = ")^pp_com^"\n" ^ (match m with Lem _ -> " | " | _ -> " ") - ^ String.concat " | " + ^ String.concat (match m with Lean _ -> " " | _ -> " | ") (List.map (function s -> s^"\n") (Auxl.option_map @@ -2731,7 +2802,7 @@ and pp_rule_list m xd rs = (* and we generate a type abbreviation *) | [Ntr ntr] when (None<>Auxl.hom_spec_for_pp_mode m(Auxl.rule_of_ntr xd ntr).rule_homs - && match m with Isa _ | Coq _ | Hol _ | Lem _ | Caml _ -> true | _ -> false) + && match m with Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Caml _ -> true | _ -> false) -> (* PS hack to turn off printing of phantom nonterms which would otherwise turn into type abbreviations. Please check - maybe this should be before dependency analysis??? *) if (Auxl.rule_of_ntr xd ntr).rule_phantom then "" else @@ -2775,6 +2846,11 @@ and pp_rule_list m xd rs = ^ strip_surrounding_parens (pp_nontermroot_ty m xd ntr) ^ " = " ^ pp_hom_spec m xd hs ^ "\n\n" + | Lean _ -> + "\ndef " + ^ strip_surrounding_parens (pp_nontermroot_ty m xd ntr) ^ " := " + ^ pp_hom_spec m xd hs + ^ "\n\n" | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "int_rule_list_dep" ) (* or not, in which case we generate an inductive type definition *) | b -> @@ -2818,6 +2894,15 @@ and pp_rule_list m xd rs = let coq_equality_code = !pp_internal_coq_buffer in pp_internal_coq_buffer := ""; def ^ coq_equality_code + | Lean _ -> + let def = int_rule_list_dep m xd rs (fun rs -> "\ninductive ") "\nwhere " "" in + let lean_equality_code = + "open " ^ String.concat " " (Auxl.option_map (fun r -> if r.rule_meta || r.rule_phantom || (try (List.assoc "lean" r.rule_homs);true with Not_found -> false) then None else Some (pp_nontermroot_ty m xd r.rule_ntr_name)) rs) ^ "\n" in + + (*let coq_equality_code = !pp_internal_coq_buffer in + pp_internal_coq_buffer := "";*) + def ^ (*^ coq_equality_code*) + lean_equality_code | Twf wo -> int_rule_list_dep m xd rs (fun rs -> "") "\n" "" | Caml oo -> @@ -2962,7 +3047,7 @@ and pp_syntaxdefn m xd = ^ (if ao.ppa_show_deps then (pp_plain_top_sort m xd ^ pp_plain_dep_graph m xd) else "") - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ -> String.concat "" (List.map (pp_metavardefn m xd) xd.xd_mds) ^ pp_rule_list m xd xd.xd_rs | Tex _ -> @@ -3008,6 +3093,12 @@ and pp_variable m xd mvrp var = (Auxl.mvd_of_mvr xd mvrp).mvd_rep with | None -> var | Some hs -> String.concat "" (apply_hom_spec m xd hs [var])) + | Lean _ -> + (match Auxl.hom_spec_for_hom_name + "leanvar" + (Auxl.mvd_of_mvr xd mvrp).mvd_rep with + | None -> var + | Some hs -> String.concat "" (apply_hom_spec m xd hs [var])) | Tex _ -> (match Auxl.hom_spec_for_hom_name "texvar" @@ -3172,7 +3263,7 @@ and pp_symterm_node_body m xd sie de stnb : string = let include_terminals = match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> true - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ -> false + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ -> false | Caml oo -> oo.ppo_include_terminals in let pp_es' () = pp_symterm_elements' m xd sie de include_terminals prod_es stnb.st_es in let pp_es () = pp_symterm_elements m xd sie de include_terminals prod_es stnb.st_es in @@ -3183,7 +3274,7 @@ and pp_symterm_node_body m xd sie de stnb : string = ( match stnb.st_prod_name with | "formula_dots" -> String.concat " \\quad " (pp_es()) | _ -> pp_tex_insert_spacing (pp_es'())) - | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Caml _ -> + | Isa _ | Hol _ | Lem _ | Coq _ | Lean _ | Twf _ | Caml _ -> ( match stnb.st_prod_name with (* special case pp for proof assistant judgement forms *) @@ -3201,7 +3292,9 @@ and pp_symterm_node_body m xd sie de stnb : string = | Some(hs,arity,prec) -> pp_symterm_element_judge_isa_fancy m xd sie de hs p'' stnb'') | Coq co -> - pp_symterm_element_judge_coq_plain m xd sie de p'' stnb'' + pp_symterm_element_judge_coq_plain m xd sie de p'' stnb'' + | Lean lno -> + pp_symterm_element_judge_lean_plain m xd sie de p'' stnb'' | Twf wo -> pp_symterm_element_judge_twf_plain m xd sie de p'' stnb'' | Hol ho -> @@ -3273,6 +3366,18 @@ and pp_symterm_node_body m xd sie de stnb : string = ^ ")" ) ) + | Lean _ -> + ( match stnb.st_es with + | [] -> stnb.st_prod_name + | _ -> + leanTODO "3" ( + "(" + ^ "List.all " + ^ "(" ^ String.concat " " (pp_es()) ^ ")" + ^ "(fun b |-> b)" + ^ ")" + ) + ) | Coq co -> let dl = ("formula: " ^(String.concat " -- " @@ -3491,7 +3596,7 @@ and pp_symterm_node_body m xd sie de stnb : string = ^ String.concat "" (apply_hom_spec m xd hs (pp_es())) ^")") - | Coq _ | Twf _ -> + | Coq _ | Lean _ | Twf _ -> ( match stnb.st_es with | [] -> promoted_pn | _ -> @@ -3568,6 +3673,11 @@ and pp_symterm_element_judge_coq_plain m xd sie de p'' stnb'' = stnb''.st_prod_name ^ " " ^ String.concat " " pp_es'' +and pp_symterm_element_judge_lean_plain m xd sie de p'' stnb'' = + let pp_es'' = pp_symterm_elements m xd sie de false p''.prod_es stnb''.st_es in + stnb''.st_prod_name ^ " " + ^ String.concat " " pp_es'' + and pp_symterm_element_judge_hol_plain m xd sie de p'' stnb'' = let pp_es'' = pp_symterm_elements m xd sie de false p''.prod_es stnb''.st_es in " ( " @@ -3647,7 +3757,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * let include_terminals = match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> true - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ -> false + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ -> false | Caml oo -> oo.ppo_include_terminals in let tmopt' = ( match tmopt with @@ -3660,6 +3770,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * | Isa _ -> ["[]",TTC_dummy] | Caml _ -> ["[]",TTC_dummy] | Lem _ -> ["[]",TTC_dummy] + | Lean _ -> ["[]",TTC_dummy] | Coq co -> if co.coq_expand_lists then ["Nil_list_"^(String.concat "_" (elements_to_string prod_es)),TTC_dummy ] @@ -3676,7 +3787,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * Auxl.list_concat tmopt' (List.map (pp_symterm_list_item m xd sie de tmopt include_terminals prod_es) stlis) in (match m with Ascii ao when ao.ppa_ugly -> [col_magenta ao "[slb",TTC_dummy] @ ss @ [col_magenta ao "slb]",TTC_dummy] | _ -> ss) - | Isa _ | Caml _ | Coq _ | Hol _ | Lem _ | Twf _ -> + | Isa _ | Caml _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ -> let pp_stlis = List.map (function xs->List.map fst xs) (List.map (pp_symterm_list_item m xd sie de tmopt include_terminals prod_es) stlis) in (List.map (function s -> (s,TTC_dummy)) (match m with @@ -3704,6 +3815,12 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * (Auxl.list_concat [ "++" ] pp_stlis) ^ ")")] + | Lean _ -> + [ leanTODO "4" ("(" + ^ String.concat " " + (Auxl.list_concat [ "++" ] + pp_stlis) + ^ ")")] | Coq co -> (* FZ use Auxl.list_app_coq *) let l = List.flatten @@ -3745,7 +3862,7 @@ and pp_symterm_list_item m xd sie (de :dotenv) tmopt include_terminals prod_es s (match m with | Ascii ao -> if ao.ppa_ugly then [col_magenta ao "[stli_single",TTC_dummy] @ pp_es' @ [col_magenta ao "stli_single]",TTC_dummy] else pp_es' | Tex _ -> pp_es' - | Caml _ | Isa _ | Hol _ | Lem _ -> + | Caml _ | Isa _ | Hol _ | Lem _ | Lean _ -> ["[(" ^ String.concat "," pp_es ^ ")]",TTC_dummy] | Coq co -> if co.coq_expand_lists then @@ -3845,11 +3962,11 @@ and pp_symterm_list_body m xd sie (de :dotenv) tmopt include_terminals prod_es s ^ "}",TTC_comp] ) - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ -> (List.map (function s -> (s,TTC_dummy)) (match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise ThisCannotHappen - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ -> (* interim placeholder code - not remotely right *) (* FZ I hope that this comment is outdated *) let es = stlb.stl_elements in @@ -3899,7 +4016,11 @@ and pp_symterm_list_body m xd sie (de :dotenv) tmopt include_terminals prod_es s ^ de1i.de1_compound_id ^ ")"] | Lem _ -> - [lemTODO "14" ("(List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " + [lemTODO "7" ("(List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " + ^ de1i.de1_compound_id + ^ ")")] + | Lean _ -> + [leanTODO "5" ("(List.map (fun "^de1i.de1_pattern^" => "^pp_body^") " ^ de1i.de1_compound_id ^ ")")] | Coq co -> @@ -4282,6 +4403,7 @@ let pp_pp_mode m = match m with | Isa _ -> "Isa" | Hol _ -> "Hol" | Lem _ -> "Lem" + | Lean _ -> "Lean" | Twf _ -> "Twf" | Ascii _ -> "Ascii" | Tex _ -> "Tex" diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml index 48c1b59..d578cb8 100644 --- a/src/grammar_typecheck.ml +++ b/src/grammar_typecheck.ml @@ -404,30 +404,30 @@ let subrule (xd:syntaxdefn) (include_meta_prods:bool) let allowable_hom_data = [ - ( Hu_root , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml"], + ( Hu_root , (["isa";"coq";"lean";"lean-type";"hol";"lem";(*"twf";*)"tex";"ocaml"], "nonterminal, metavar or indexvar root")); - ( Hu_metavar , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";"lex";"texvar";"isavar";"holvar";"lemvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"], + ( Hu_metavar , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";"lean-equality";"lex";"texvar";"isavar";"holvar";"lemvar";"leanvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"], "metavar declaration")); - ( Hu_rule , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"], + ( Hu_rule , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ichlL"; "ic";"ch";"ih";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"], "rule")); ( Hu_rule_meta, (["com"], "special rule")); - ( Hu_prod , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"texlong";"ocaml";"com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih"; + ( Hu_prod , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"texlong";"ocaml";"com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ichlL";"ic";"ch";"ih"; "disambiguate";"prec";"leftassoc";"rightassoc";"menhir";"quotient-remove";"menhir-prec";"pp";"pp-raw"], "production")); ( Hu_prod_tm , (["isa"; "tex";"lex"; "com"; "prec";"leftassoc";"rightassoc"],"production of the terminals grammar")); ( Hu_drule , ([ "com"],"definition rule")); ( Hu_defn , ([ "tex"; "com";"isasyn";"isaprec";"disambiguate";"lemwcf"],"definition")); ( Hu_defnclass, (["coq-universe"],"defns block")); - ( Hu_fundefn , (["isa";"coq";"hol";"lem";(*"twf";*)"tex"; "com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"coq-struct"],"function definition")); + ( Hu_fundefn , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex"; "com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ichlL";"ic";"ch";"ih";"coq-struct"],"function definition")); ( Hu_fundefnclass, ([(* "isa-proof";*)"hol-proof"],"funs block")); ( Hu_subrule, (["isa-proof"],"subrule definition")); ( Hu_subst, (["isa-proof"],"substitution definition")); ( Hu_freevar, (["isa-proof";"isa-set"],"free variable definition")); - (* ( Hu_embed , (["isa";"coq";"hol";"lem";(\*"twf";*\)"tex";"ocaml";"isa-auxfn-proof";"isa-subrule-proof"],"embed section")); *) + (* ( Hu_embed , (["isa";"coq";"lean";"hol";"lem";(\*"twf";*\)"tex";"ocaml";"isa-auxfn-proof";"isa-subrule-proof"],"embed section")); *) ( Hu_deadcode, ([], "Internal error: Hu_deadcode")); ] -let embed_allowable_homs = ["coq";"coq-lib";"coq-preamble"; +let embed_allowable_homs = ["coq";"lean";"coq-lib";"coq-preamble";"lean-preamble"; "isa";"isa-import";"isa-auxfn-proof";"isa-subrule-proof";"isa-lib";"isa-preamble"; "hol";"hol-preamble"; "lem";"lem-preamble"; @@ -436,7 +436,7 @@ let embed_allowable_homs = ["coq";"coq-lib";"coq-preamble"; "ocaml";"ocaml-preamble"; "menhir"] -let list_form_allowable_homs =["isa";"coq";"hol";"lem";"ic";"ch";"ih";"ich";"ichl";"icho";"ichlo";(*"icht";*)"coq-struct";"ocaml"] +let list_form_allowable_homs =["isa";"coq";"lean";"hol";"lem";"ic";"ch";"ih";"ich";"ichl";"ichlL";"icho";"ichlo";(*"icht";*)"coq-struct";"ocaml"] let cd_disambiguate_hom name rhs hs = try @@ -677,6 +677,8 @@ and cd_homs_icho (c: cd_env) (hs: homomorphism list) : homomorphism list = ("isa",hs)::("hol",hs)::("coq",hs)::("ocaml",hs)::(cd_homs_icho c hs') else if hn = "ichl" then ("isa",hs)::("hol",hs)::("coq",hs)::("lem",hs)::(cd_homs_icho c hs') + else if hn = "ichlL" then + ("isa",hs)::("hol",hs)::("coq",hs)::("lem",hs)::("lean",hs)::(cd_homs_icho c hs') else if hn = "ichlo" then ("isa",hs)::("hol",hs)::("coq",hs)::("lem",hs)::("ocaml",hs)::(cd_homs_icho c hs') else @@ -818,6 +820,7 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ (fun h -> match h with Hom_index _ -> true | _ -> false) (List.assoc "order" homs) in let oh_coq = ( "coq", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in + let oh_lean= ( "lean", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_isa = ( "isa", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_hol = let of_s = if List.length oh = 0 then "" else " of " in @@ -826,7 +829,7 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ (* let oh_lem = ( "lem", (Hom_string ("("^prod_name))::bracket_commas oh @[Hom_string ")"] ) in *) let oh_lem = ( "lem", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in (* LemTODO25: *) - homs @ [oh_coq; oh_isa; oh_hol; oh_caml; oh_lem] + homs @ [oh_coq; oh_lean; oh_isa; oh_hol; oh_caml; oh_lem] with Not_found -> homs in let cd_order_funmeta prod_name homs elems = @@ -842,12 +845,13 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ elems)) [] in let oh_coq = ( "coq", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in + let oh_lean= ( "lean", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_isa = ( "isa", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_hol = ( "hol", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_lem = ( "lem", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_caml= ( "ocaml", (Hom_string ("("^prod_name))::oh @[Hom_string ")"] ) in let oh_ord = ( "order", oh ) in - List.filter (fun x -> fst x <> "order") homs @ [oh_coq; oh_lem; oh_isa; oh_hol; oh_caml; oh_ord] + List.filter (fun x -> fst x <> "order") homs @ [oh_coq; oh_lean; oh_lem; oh_isa; oh_hol; oh_caml; oh_ord] in let es = cd_elements c p.raw_prod_es in let hu = if rn="terminals" then Hu_prod_tm else Hu_prod in @@ -1931,7 +1935,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b r.raw_rule_homs) in let rule_homs = if r.raw_rule_ntr_name = "formula" then - [("coq", [Hom_string "Prop"]); ("hol", [Hom_string "bool"]); + [("coq", [Hom_string "Prop"]); ("lean", [Hom_string "Prop"]); ("hol", [Hom_string "bool"]); ("lem", [Hom_string "bool"]); ("isa", [Hom_string "bool"]); ("ocaml", [Hom_string "bool"])] else rule_homs in @@ -1966,6 +1970,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b | "tex-wrap-pre" | "tex-wrap-post" -> Some (l,hn,he) | "coq-preamble" -> Some (l,"coq",he) + | "lean-preamble" -> Some (l,"lean",he) | "isa-preamble" -> Some (l,"isa",he) | "hol-preamble" -> Some (l,"hol",he) | "lem-preamble" -> Some (l,"lem",he) diff --git a/src/main.ml b/src/main.ml index 0c67e50..8219caa 100644 --- a/src/main.ml +++ b/src/main.ml @@ -59,6 +59,9 @@ let lem_filter_filename_dsts = ref ([] : string list) let coq_filter_filenames = ref ([] : (string * string) list) let coq_filter_filename_srcs = ref ([] : string list) let coq_filter_filename_dsts = ref ([] : string list) +let lean_filter_filenames = ref ([] : (string * string) list) +let lean_filter_filename_srcs = ref ([] : string list) +let lean_filter_filename_dsts = ref ([] : string list) let twf_filter_filenames = ref ([] : (string * string) list) let twf_filter_filename_srcs = ref ([] : string list) let twf_filter_filename_dsts = ref ([] : string list) @@ -93,6 +96,7 @@ let coq_expand_lists = ref false let coq_lngen = ref false let coq_names_in_rules = ref true let coq_use_filter_fn = ref false +let lean_names_in_rules = ref true let merge_fragments = ref false let picky_multiple_parses = ref false let caml_include_terminals = ref false @@ -128,6 +132,10 @@ let options = Arg.align [ Arg.Tuple[Arg.String (fun s -> coq_filter_filename_srcs := s :: !coq_filter_filename_srcs); Arg.String (fun s -> coq_filter_filename_dsts := s :: !coq_filter_filename_dsts)], " Files to Coq filter" ); + ( "-lean_filter", + Arg.Tuple[Arg.String (fun s -> lean_filter_filename_srcs := s :: !lean_filter_filename_srcs); + Arg.String (fun s -> lean_filter_filename_dsts := s :: !lean_filter_filename_dsts)], + " Files to Lean filter" ); ( "-hol_filter", Arg.Tuple[Arg.String (fun s -> hol_filter_filename_srcs := s :: !hol_filter_filename_srcs); Arg.String (fun s -> hol_filter_filename_dsts := s :: !hol_filter_filename_dsts)], @@ -248,6 +256,9 @@ let options = Arg.align [ Arg.Bool (fun b -> coq_use_filter_fn := b), "<"^string_of_bool !coq_use_filter_fn^"> Use list_filter instead of list_minus2 in substitutions" ); (* options for OCaml output *) + ( "-lean_names_in_rules", + Arg.Bool (fun b -> lean_names_in_rules := b), + "<"^string_of_bool !lean_names_in_rules^"> Copy user names in rule definitions" ); ( "-ocaml_include_terminals", Arg.Bool (fun b -> caml_include_terminals := b), "<"^string_of_bool !caml_include_terminals^"> Include terminals in OCaml output (experimental!)" ); @@ -318,6 +329,7 @@ let _ = hol_filter_filenames := List.combine (!hol_filter_filename_srcs) (!hol_f let _ = lem_filter_filenames := List.combine (!lem_filter_filename_srcs) (!lem_filter_filename_dsts) let _ = isa_filter_filenames := List.combine (!isa_filter_filename_srcs) (!isa_filter_filename_dsts) let _ = coq_filter_filenames := List.combine (!coq_filter_filename_srcs) (!coq_filter_filename_dsts) +let _ = lean_filter_filenames := List.combine (!lean_filter_filename_srcs) (!lean_filter_filename_dsts) let _ = twf_filter_filenames := List.combine (!twf_filter_filename_srcs) (!twf_filter_filename_dsts) let _ = caml_filter_filenames := List.combine (!caml_filter_filename_srcs) (!caml_filter_filename_dsts) @@ -325,6 +337,7 @@ let types_of_extensions = [ "ott","ott"; "tex","tex"; "v", "coq"; + "lean", "lean"; "thy","isa"; "sml","hol"; "lem","lem"; @@ -345,7 +358,7 @@ let file_type name = with _ -> None -let non_tex_output_types = ["coq"; "isa"; "hol"; "lem"; "twf"; "ocaml"] +let non_tex_output_types = ["coq"; "lean"; "isa"; "hol"; "lem"; "twf"; "ocaml"] let output_types = "tex" :: "lex" :: "menhir" :: non_tex_output_types let input_types = "ott" :: output_types @@ -373,7 +386,7 @@ let classify_file_argument arg = (* *) (* values, containing first all the ott source files from the end of *) (* the command line, if any, then all the explicit -in and -out arguments, *) -(* and finally any -tex/-coq/-hol/-isabelle/-lem/-ocaml arguments *) +(* and finally any -tex/-coq/-lean/-hol/-isabelle/-lem/-ocaml arguments *) let all_file_arguments = List.map classify_file_argument (List.rev (!file_arguments)) @@ -392,7 +405,7 @@ let targets_in ts = let targets_non_tex = targets_in non_tex_output_types let targets = targets_in output_types -let targets_for_non_picky = targets_in [(*"lex";"ocaml";*)"hol";"lem";"isa";"twf";"coq";"tex"] +let targets_for_non_picky = targets_in [(*"lex";"ocaml";*)"hol";"lem";"isa";"twf";"coq";"lean";"tex"] (* collect the source filenames *) let source_filenames = @@ -424,6 +437,8 @@ let m_isa = Isa { ppi_isa_primrec = !isa_primrec; ppi_generate_lemmas = !isa_generate_lemmas } let m_hol = Hol { hol_library = ref ("",[]); } let m_lem = Lem { lem_library = ref ("",[]); } +let m_lean = Lean { lean_library = ref ("",[]); + lean_names_in_rules = !lean_names_in_rules} let m_twf = Twf { twf_current_defn = ref ""; twf_library = ref ("",[]) } let m_coq = Coq { coq_expand_lists = !coq_expand_lists; @@ -527,6 +542,7 @@ let _ = "isa",m_isa; "twf",m_twf; "coq",m_coq ; + "lean",m_lean ; "tex",m_tex ]) targets_for_non_picky) @@ -774,6 +790,8 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = System_pp.pp_systemdefn_core_io m_hol sd lookup fi !merge_fragments | "lem" -> System_pp.pp_systemdefn_core_io m_lem sd lookup fi !merge_fragments + | "lean" -> + System_pp.pp_systemdefn_core_io m_lean sd lookup fi !merge_fragments | "twf" -> System_pp.pp_systemdefn_core_io m_twf sd lookup fi !merge_fragments | "ocaml" -> @@ -856,6 +874,7 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = (List.iter (filter m_tex) (!tex_filter_filenames)); (List.iter (filter m_coq) (!coq_filter_filenames)); + (List.iter (filter m_lean) (!lean_filter_filenames)); (List.iter (filter m_isa) (!isa_filter_filenames)); (List.iter (filter m_hol) (!hol_filter_filenames)); (List.iter (filter m_lem) (!lem_filter_filenames)); diff --git a/src/ott.byt b/src/ott.byt new file mode 100755 index 0000000..44b5d87 Binary files /dev/null and b/src/ott.byt differ diff --git a/src/subrules_pp.ml b/src/subrules_pp.ml index 002ccec..df5858c 100644 --- a/src/subrules_pp.ml +++ b/src/subrules_pp.ml @@ -308,6 +308,11 @@ let pp_subrules m xd srs : int_funcs_collapsed = [ lemTODO "15" (" (List.all (fun "^de1i.de1_pattern^" -> "^conjuncted_conjuncts^") " ^ de1i.de1_compound_id ^ ")")], deps, [] + | Lean _ -> + [ leanTODO "7" (" (List.all " + ^ de1i.de1_compound_id ^ " " + ^ "(fun "^de1i.de1_pattern^" => "^conjuncted_conjuncts^") " + ^ ")")], deps, [] | Coq co when not co.coq_expand_lists -> let e = if List.length (Str.split (Str.regexp "(\\|,\\|)") de1i.de1_pattern) = 1 @@ -424,7 +429,7 @@ let pp_subrules m xd srs : int_funcs_collapsed = dep := deps @ !dep; funcs := !funcs @ new_funcs; match m with - | Coq _ | Hol _ | Lem _| Isa _ | Caml _ -> + | Coq _ | Lean _ | Hol _ | Lem _| Isa _ | Caml _ -> if conjuncts = [] then Auxl.pp_true m false else String.concat (Auxl.pp_and m false) conjuncts @@ -434,7 +439,7 @@ let pp_subrules m xd srs : int_funcs_collapsed = pls in match m with - | Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> + | Coq _ | Lean _ | Hol _ | Lem _ | Isa _ | Caml _ -> let rhs = if rhss = [] then Auxl.pp_false m false @@ -484,6 +489,18 @@ let pp_subrules m xd srs : int_funcs_collapsed = " : " ^ (if co.coq_expand_lists then "Prop :=\n" else "bool :=\n") ^ " match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " with\n" ) + | Lean _ -> + let nts_used = Context_pp.nts_used_in_lhss m xd ru in +(* let nts_used = Auxl.nts_used_in_rule ru in *) + let fresh_var_ntr = Auxl.secondary_ntr xd sru in + let fresh_var = Auxl.fresh_nt nts_used (fresh_var_ntr,[]) in (* FZ Substs_pp *) + ( Auxl.pp_is srl sru + ^ " (" ^ Grammar_pp.pp_nonterm m xd fresh_var + ^ ":" ^ Grammar_pp.pp_nontermroot_ty m xd sru ^ ")", + "", + " : " + ^ ("Bool :=\n") + ^ " match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " with\n" ) | Twf _ -> ( Auxl.pp_is srl sru ^ " : " ^ Grammar_pp.pp_nontermroot_ty m xd sru diff --git a/src/substs_pp.ml b/src/substs_pp.ml index 6ab8213..ae31740 100644 --- a/src/substs_pp.ml +++ b/src/substs_pp.ml @@ -62,6 +62,12 @@ let pp_list_minus_lem = ^ " | h::t -> if (List.elem h l2) then list_minus t l2 else h::(list_minus t l2)\n" ^ " end\n" ^ "\n") +let pp_list_minus_lean = + ("def list_minus [BEq a] (l1:List a) (l2:List a) : (List a) :=\n" + ^ " match l1 with\n" + ^ " | [] => []\n" + ^ " | h::t => if List.elem h l2 then list_minus t l2 else h::(list_minus t l2)\n" + ^ "\n") let pp_list_minus_isa = ( "primrec\n" ^ "list_minus :: \"'a list => 'a list => 'a list\"\n" @@ -120,6 +126,14 @@ let pp_list_assoc_coq = ^ "end.\n" ^ "Arguments list_assoc [A B] _ _ _.\n\n") +let pp_list_assoc_lean = + "def list_assoc [DecidableEq a] (l:List (a × b)) (x:a) : Option b :=\n" + ^ "match l with\n" + ^ "| [] => none\n" + ^ "| (x',y')::t => if x=x' then some y' else list_assoc t x\n\n" + + + (* this is a temporary workaround, to be replaced when the Lem library List.assoc have been updated to return an option type *) let pp_list_assoc_lem = @@ -146,12 +160,12 @@ let pp_list_all_cong_lemma_isa = let pp_list_mem m = match m with | Coq co -> Auxl.add_to_lib co.coq_library "list_mem" pp_list_mem_coq - | Caml _ | Hol _ | Lem _ | Isa _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ + | Caml _ | Hol _ | Lem _ | Lean _ | Isa _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_list_mem" let pp_list_filter m = match m with | Coq co -> Auxl.add_to_lib co.coq_library "list_filter" pp_list_filter_coq - | Isa _ | Hol _ | Lem _ | Caml _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_list_filter" let pp_list_minus m = match m with @@ -159,6 +173,7 @@ let pp_list_minus m = match m with | Lem oo -> Auxl.add_to_lib oo.lem_library "list_minus" pp_list_minus_lem | Isa io -> Auxl.add_to_lib io.isa_library "list_minus" pp_list_minus_isa | Hol ho -> () + | Lean lno -> Auxl.add_to_lib lno.lean_library "list_minus" pp_list_minus_lean | Coq co -> pp_list_mem m; Auxl.add_to_lib co.coq_library "list_minus" pp_list_minus_coq @@ -168,7 +183,7 @@ let pp_list_minus2 m = match m with | Coq co -> pp_list_mem m; Auxl.add_to_lib co.coq_library "list_minus2" pp_list_minus2_coq - | Caml _ | Hol _ | Lem _ | Isa _ | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ + | Caml _ | Hol _ | Lem _ | Lean _ | Isa _ | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_list_minus2" let pp_list_assoc m = match m with @@ -176,6 +191,7 @@ let pp_list_assoc m = match m with | Hol ho -> () | Lem lo -> Auxl.add_to_lib lo.lem_library "list_assoc" pp_list_assoc_lem | Coq co -> Auxl.add_to_lib co.coq_library "list_assoc" pp_list_assoc_coq + | Lean lno -> Auxl.add_to_lib lno.lean_library "list_assoc" pp_list_assoc_lean | Caml _ | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_list_assoc" @@ -320,6 +336,16 @@ let pp_auxfn_clauses m xd f ntr ntmvr = "", " : list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr ^ " :=\n" ^ " match " ^ Grammar_pp.pp_nonterm m xd pat_var ^ " with\n" ) + | Lean _ -> + let nts_used = Context_pp.nts_used_in_lhss m xd (Auxl.rule_of_ntr xd ntr) in + let fresh_var_ntr = Auxl.secondary_ntr xd ntr in + let pat_var = Auxl.fresh_nt nts_used (fresh_var_ntr,[]) in + ( (leanTODO "8" (Auxl.auxfn_name f ntrn ntrn (* FZ *) + ^ " (" ^ Grammar_pp.pp_nonterm m xd pat_var + ^ ":" ^ Grammar_pp.pp_nontermroot_ty m xd ntr ^ ")")), + "", + " : List " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr ^ " :=\n" + ^ " match " ^ Grammar_pp.pp_nonterm m xd pat_var ^ " with\n" ) | Lem _ | Caml _ -> let nts_used = Context_pp.nts_used_in_lhss m xd (Auxl.rule_of_ntr xd ntr) in @@ -593,6 +619,11 @@ let rec pp_subst_symterm ^ that_s ^ " " ^ "(" ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^ ")" + | Lean _ -> + leanTODO "9" " List.elem " + ^ that_s + ^ " " + ^ "(" ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^ ")" | Coq _ -> pp_list_mem m; "list_mem " @@ -667,6 +698,23 @@ let rec pp_subst_symterm ^ nt_s ^ ")" ) + | Lean _ -> + leanTODO "10" ( + "(" + ^ Auxl.subst_name subst.sb_name dep_name ^ " " + ^ (match bound_things_glommed with + | Empty -> sub_var + | _ -> + "(List.filter " + ^ sub_var ^ " " + ^ "(fun ("^ that_s ^","^ this_s ^") => " + ^ "not ("^that_in_bound_things()^")" + ^ ")" + ^")") + ^ " " + ^ nt_s + ^ ")" + ) | Coq co -> "(" ^ Auxl.subst_name subst.sb_name dep_name ^ " " @@ -927,6 +975,7 @@ and pp_subst_symterm_list_body ("", "Cons_"^suf^" "^lp^" "^rp, "Cons_"^suf^" " ^ rhs ^ " (" ^ id ^ " " ^ common_lhs ^ " "^rp^")" ) ] } ]) + | Lean _ -> (leanTODO "11" "",[]) | Caml _ -> ("",[]) @@ -1052,6 +1101,18 @@ and pp_subst_symterm_list_body ^ de1i.de1_compound_id ^ ")", [] ) + | Lean _ -> + let l = Str.split (Str.regexp "(\\|,\\|)") de1i.de1_pattern in + if List.length l = 1 then + ( leanTODO "12" ("(List.map (fun ("^de1i.de1_pattern^":" ^ de1i.de1_coq_type_of_pattern ^ ") => "^pp_body^") " + ^ de1i.de1_compound_id + ^ ")"), [] ) + else + ( leanTODO "13" ("(List.map (fun (pat_:" ^ de1i.de1_coq_type_of_pattern ^ ") => match pat_ with " (* FZ freshen pat_ *) + ^ "| " ^ de1i.de1_pattern^" => " ^pp_body^" ) " + ^ de1i.de1_compound_id + ^ ")"), [] ) + | Caml _ -> ( "(List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " ^ de1i.de1_compound_id @@ -1086,7 +1147,7 @@ let pp_subst_prod let lhs_pat = Grammar_pp.pp_symterm m xd sie de lhs_st in let lhs = ( match m with - | Coq _ | Caml _ | Lem _ -> lhs_pat + | Coq _ | Lean _ | Caml _ | Lem _ -> lhs_pat | Isa _ | Hol _ | Twf _ -> (* Auxl.subst_name subst.sb_name rule_ntr_name ^ " " *) ( if subst.sb_multiple then sub_var @@ -1112,7 +1173,7 @@ let pp_subst_prod let substituted_singleton_rhs thing_s = ( match m with - | Coq _ | Isa _ | Hol _ | Lem _ | Caml _ -> + | Coq _ | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> let ssr = if subst.sb_multiple then (match m with @@ -1149,6 +1210,19 @@ let pp_subst_prod ^ " -> " ^ Grammar_pp.pp_nonterm m xd this_var ^ " end)" ) + | Lean _ -> + pp_list_assoc m; + (* tentative hol code for multiple subst *) + leanTODO "14" ( + "(match list_assoc " + ^ sub_var ^ " " + ^ thing_s + ^ " with " + ^ "| none => " ^ lhs_pat + ^ "| some " ^ Grammar_pp.pp_nonterm m xd this_var + ^ " => " ^ Grammar_pp.pp_nonterm m xd this_var + ^ " )" + ) | Coq coq_opt -> pp_list_assoc m; "(match list_assoc " (* A B eq *) @@ -1176,7 +1250,7 @@ let pp_subst_prod let that_s = Grammar_pp.pp_nt_or_mv m xd that_var in let eq_s = ( match m with - | Isa _ | Hol _ | Lem _ | Caml _ -> thing_s ^ "=" ^ that_s + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> thing_s ^ "=" ^ that_s | Twf _ -> raise Auxl.ThisCannotHappen | Coq _ -> ( if Auxl.require_locally_nameless xd @@ -1389,6 +1463,23 @@ let pp_subst_rule : subst -> pp_mode -> syntaxdefn -> nontermroot list -> rule - " {struct " ^ Grammar_pp.pp_nonterm m xd in_var ^"}", " : " ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " :=\n" ^ " match " ^ Grammar_pp.pp_nonterm m xd in_var ^ " with\n" ) ) + | Lean _ -> + ( (id + ^ ( if subst.sb_multiple + then + (leanTODO "15" (" (" ^ sub_var ^ ":List (" + ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that + ^ "×" ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this ^ "))" )) + else + (leanTODO "16" ( " (" ^ Grammar_pp.pp_nonterm m xd this_var ^ ":" + ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this ^")" + ^ " (" ^ Grammar_pp.pp_nt_or_mv m xd that_var ^ ":" + ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that ^ ")" ) + ^ " (" ^ Grammar_pp.pp_nonterm m xd in_var ^ ":" + ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^")"))), + ""(*" {struct " ^ Grammar_pp.pp_nonterm m xd in_var ^"}"*), + " : " ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " :=\n" + ^ " match " ^ Grammar_pp.pp_nonterm m xd in_var ^ " with\n" ) | Lem _ | Caml _ -> @@ -1499,7 +1590,7 @@ let pp_freevar_rule_const (fv : freevar) (m: pp_mode) (xd: syntaxdefn) (** fv for a symterm *) (** **************** *) -let list_append m = match m with | Lem _ | Hol _ -> " ++ " | _ -> " @ " +let list_append m = match m with | Lem _ | Hol _ | Lean _ -> " ++ " | _ -> " @ " (* todo: is there a better idiom than this insane list of arguments? *) let rec pp_fv_symterm @@ -1541,7 +1632,7 @@ let rec pp_fv_symterm let call = Auxl.fv_name fv.fv_name id (* (Auxl.promote_ntr xd ntrp) *) ^ " " ^ nt_s in ( match m with | Twf _ -> Some call - | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ -> Some ("("^call^")") + | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ | Lean _ -> Some ("("^call^")") | Tex _ | Ascii _ | Lex _ | Menhir _ -> assert false)) else None in @@ -1575,13 +1666,13 @@ let rec pp_fv_symterm | Isa _ when has_isa_set_hom fv -> "(" ^ s ^ " - set " ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^")" - | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ -> + | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ | Lean _ -> pp_list_minus m; "(list_minus " ^ (match m with (* HACK is the name eq_thing always correct? *) | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> Auxl.errorm m "list_minus" - | Isa _ | Hol _ | Lem _ | Caml _ -> "" + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> "" | Coq _ -> "eq_" ^ (Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that) ^ " " ) ^ s ^" " ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^")") ) @@ -1622,7 +1713,7 @@ and pp_fv_symterm_element then Some (match m with - | Isa _ | Hol _ | Lem _ | Caml _ -> ("["^mv_s^"]") + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> ("["^mv_s^"]") | Coq _ -> ("(cons "^mv_s^" nil)") | Twf _ -> ("(natlist/cons "^mv_s^" natlist/nil)") | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fv_symterm_element" @@ -1717,7 +1808,7 @@ and pp_fv_symterm_list_body (* TODO optimise the output in the common case of a list of singletons *) match m with | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fv_symterm_list_body" - | Isa _ | Coq _ | Hol _ | Lem _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Caml _ -> let pp_body_elements, funcs = let body_options, funcs = List.split @@ -1733,7 +1824,7 @@ and pp_fv_symterm_list_body ( match m with | Coq _ -> Auxl.insert_append m pp_body_elements | Isa _ when has_isa_set_hom fv -> String.concat " \\ " pp_body_elements - | _ -> String.concat (list_append m) pp_body_elements ) in + | (Lean _ | _) -> String.concat (list_append m) pp_body_elements ) in if List.length pp_body_elements = 1 then tmp else "(" ^ tmp ^ ")" in @@ -1826,6 +1917,12 @@ and pp_fv_symterm_list_body ("(List.concat (List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " ^ de1i.de1_compound_id ^ "))"), funcs + | Lean _ -> + let pp_body = String.concat (leanTODO "17" " ++ ") pp_body_elements in + Some + ("(List.concat (List.map (fun "^de1i.de1_pattern^" => "^pp_body^") " + ^ de1i.de1_compound_id + ^ "))"), funcs | Coq co when co.coq_expand_lists -> let var_list = Str.split (Str.regexp "(\\|,\\|)") de1i.de1_pattern in let args = @@ -1903,7 +2000,7 @@ let pp_freevar_prod let rhs = (match m with | Isa _ when (List.exists (fun (x,_) -> x = "isa-set") fv.fv_homs) -> "{"^thing_s^"}" - | Isa _ | Hol _ | Lem _ | Caml _ -> ("["^thing_s^"]") + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> ("["^thing_s^"]") | Coq co -> if not !(co.coq_locally_nameless) then "(cons "^thing_s^" nil)" @@ -1950,7 +2047,7 @@ let pp_freevar_prod | [] -> (match m with | Isa _ when has_isa_set_hom fv -> "{}" - | Isa _ | Hol _ | Lem _ | Caml _ -> "[]" + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> "[]" | Coq co -> if not !(co.coq_locally_nameless) then "nil" @@ -1960,7 +2057,7 @@ let pp_freevar_prod | _ -> ( match m with | Isa _ when has_isa_set_hom fv -> String.concat " \\ " rhs_elements - | Isa _ | Caml _ | Lem _ -> String.concat (list_append m) rhs_elements + | Isa _ | Caml _ | Lem _ | Lean _ -> String.concat (list_append m) rhs_elements | Hol _ -> String.concat " ++ " rhs_elements | Coq co -> if not !(co.coq_locally_nameless) @@ -2032,6 +2129,22 @@ let pp_freevar_rule : freevar -> pp_mode -> syntaxdefn -> nontermroot list -> ru | Lem _ -> " list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that ) ^ " =\n match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " with\n" + + | Lean _ -> + let nts_used = Context_pp.nts_used_in_lhss m xd r in + let fresh_var_ntr = Auxl.secondary_ntr xd r.rule_ntr_name in + let fresh_var = Auxl.fresh_nt nts_used (fresh_var_ntr,[]) in + let ntrn = Grammar_pp.pp_nontermroot m xd r.rule_ntr_name in + + lemTODOm m "24" ( + Auxl.fv_name fv.fv_name ntrn (* r.rule_ntr_name *) + ^ " (" ^ Grammar_pp.pp_nonterm m xd fresh_var + ^ ":" ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name + ^ ") "), + "", + ": " + ^ " List " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that + ^ " :=\n match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " with\n" | Twf _ -> ( Auxl.fv_name fv.fv_name r.rule_ntr_name ^ " : " diff --git a/src/system_pp.ml b/src/system_pp.ml index 88f3b2e..9598d8c 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -77,6 +77,7 @@ let pp_functions_locally_nameless fd m sd xd_transformed = | Hol ho -> fst (!(ho.hol_library)) | Lem lo -> fst (!(lo.lem_library)) | Coq co -> fst (!(co.coq_library)) + | Lean lno -> fst (!(lno.lean_library)) | Twf wo -> fst (!(wo.twf_library)) | Caml oo-> fst (!(oo.caml_library)) | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_functions") in @@ -151,6 +152,7 @@ let pp_functions fd m sd lookup = | Isa io -> fst (!(io.isa_library)) | Hol ho -> fst (!(ho.hol_library)) | Lem lo -> fst (!(lo.lem_library)) + | Lean lno -> fst (!(lno.lean_library)) | Coq co -> fst (!(co.coq_library)) | Twf wo -> fst (!(wo.twf_library)) | Caml oo ->fst (!(oo.caml_library)) @@ -187,6 +189,7 @@ let pp_library fd m = | Isa io -> pp_lib io.isa_library | Hol ho -> pp_lib ho.hol_library | Lem lo -> pp_lib lo.lem_library + | Lean lno -> pp_lib lno.lean_library | Coq co -> pp_lib co.coq_library | Twf wo -> pp_lib wo.twf_library | Caml oo-> pp_lib oo.caml_library @@ -378,6 +381,9 @@ let pp_systemdefn fd m sd lookup fn = Printf.fprintf fd "val _ = new_theory \"%s\";\n" fn; pp_systemdefn_core fd m sd lookup; output_string fd "\nval _ = export_theory ();\n" + | Lean lno -> + Printf.fprintf fd "/- generated by Ott %s from: %s -/\n" Version.n sd.sources; + pp_systemdefn_core fd m sd lookup | Coq co -> (* FZ keeping for now locally_nameless repr separated from the main *) if Auxl.require_locally_nameless sd.syntax @@ -481,6 +487,15 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments = | true -> ["Arith"; "Bool"; "List"] | false -> ["Arith"; "Bool"; "List"; "Ott.ott_list_core"])) ^ "\n\n" )] + | Lean lno -> + [ Embed_string (dummy_loc, + "/- generated by Ott " ^ Version.n ^ " from: " ^ file_sources ^ " -/\n\n" +(* ^ String.concat "\n" (List.map (fun th -> "Require Import " ^ th ^ ".") + ( match co.coq_expand_lists with + | true -> ["Arith"; "Bool"; "List"] + | false -> ["Arith"; "Bool"; "List"; "Ott.ott_list_core"])) +*) + ^ "\n\n" )] | Twf wo -> [ Embed_string (dummy_loc, "%% generated by Ott "^Version.n^" from: "^file_sources^" \n" )] diff --git a/src/types.ml b/src/types.ml index f770b73..238f1dc 100644 --- a/src/types.ml +++ b/src/types.ml @@ -816,6 +816,9 @@ and pp_coq_opts = coq_lngen : bool; coq_use_filter_fn : bool; coq_names_in_rules : bool } (* co *) +and pp_lean_opts = + { lean_library : (string * string list) ref; + lean_names_in_rules : bool } (* lno *) and pp_isa_opts = { ppi_isa_primrec : bool; ppi_isa_inductive : bool; @@ -859,6 +862,7 @@ type pp_yacc_opts = unit (* yo *) type pp_mode = (* m *) | Coq of pp_coq_opts + | Lean of pp_lean_opts | Isa of pp_isa_opts | Hol of pp_hol_opts | Lem of pp_lem_opts @@ -963,6 +967,12 @@ let lemTODOm m s1 s2 = match m with Lem _ -> lemTODO s1 s2 | _ -> s2 let lemTODOmo m s1 s2o = match s2o with None -> None | Some s2 -> Some (lemTODOm m s1 s2) +(** ************************ *) +(** lean debug *) +(** ************************ *) +let lean_debug = ref false +let leanTODO s1 s2 = if !lean_debug then "(* leanTODO "^s1^"*) "^s2 else s2 + (* from grammar_typecheck *) diff --git a/test-lean-project/.github/workflows/lean_action_ci.yml b/test-lean-project/.github/workflows/lean_action_ci.yml new file mode 100644 index 0000000..c48bd68 --- /dev/null +++ b/test-lean-project/.github/workflows/lean_action_ci.yml @@ -0,0 +1,14 @@ +name: Lean Action CI + +on: + push: + pull_request: + workflow_dispatch: + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v5 + - uses: leanprover/lean-action@v1 diff --git a/test-lean-project/.gitignore b/test-lean-project/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/test-lean-project/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/test-lean-project/Main.lean b/test-lean-project/Main.lean new file mode 100644 index 0000000..927a977 --- /dev/null +++ b/test-lean-project/Main.lean @@ -0,0 +1,4 @@ +import TestLeanProject + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/test-lean-project/README.md b/test-lean-project/README.md new file mode 100644 index 0000000..46f2e58 --- /dev/null +++ b/test-lean-project/README.md @@ -0,0 +1 @@ +# test-lean-project \ No newline at end of file diff --git a/test-lean-project/TestLeanProject.lean b/test-lean-project/TestLeanProject.lean new file mode 100644 index 0000000..9bcb910 --- /dev/null +++ b/test-lean-project/TestLeanProject.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `TestLeanProject` library. +-- Import modules here that should be built as part of the library. +import TestLeanProject.Basic diff --git a/test-lean-project/TestLeanProject/Basic.lean b/test-lean-project/TestLeanProject/Basic.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/test-lean-project/TestLeanProject/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/test-lean-project/lake-manifest.json b/test-lean-project/lake-manifest.json new file mode 100644 index 0000000..5a1fa0b --- /dev/null +++ b/test-lean-project/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "«test-lean-project»", + "lakeDir": ".lake"} diff --git a/test-lean-project/lakefile.toml b/test-lean-project/lakefile.toml new file mode 100644 index 0000000..619d459 --- /dev/null +++ b/test-lean-project/lakefile.toml @@ -0,0 +1,10 @@ +name = "test-lean-project" +version = "0.1.0" +defaultTargets = ["test-lean-project"] + +[[lean_lib]] +name = "TestLeanProject" + +[[lean_exe]] +name = "test-lean-project" +root = "Main" diff --git a/test-lean-project/lean-toolchain b/test-lean-project/lean-toolchain new file mode 100644 index 0000000..5249182 --- /dev/null +++ b/test-lean-project/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.27.0 diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/_digests b/tests/menhir_tests/test10menhir_with_aux_args/_build/_digests new file mode 100644 index 0000000..5fbf358 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/_digests @@ -0,0 +1,21 @@ +"Resource: /home/pes20/repos/ott/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_parser.mly": "\1409\222S\024w\194\136\156sF\206\152\131\164j" +"Rule: ocaml: menhir dependencies (%=test10menhir_with_aux_parser )": "A\029\135\200\234\164>'3>*\177\179\154\196\r" +"Rule: ocaml dependencies ml (%=test10menhir_with_aux_ast )": "\231\145\231\239t\240Z\022&\127a\243*\167'\163" +"Rule: ocaml: ml -> cmo & cmi (%=test10menhir_with_aux_lexer )": "\198FOv\187\226SFx\189W\011\"X\180\242" +"Rule: ocaml: menhir (%=test10menhir_with_aux_parser )": "m\193r@\220\195mV\221\182\144\189\012\190\231," +"Rule: ocaml: ml & cmi -> cmo (%=test10menhir_with_aux_parser )": "\031\006=9w\157dPZ\154\253<\025\178,\224" +"Resource: /home/pes20/repos/ott/tests/menhir_tests/test10menhir_with_aux_args/main.ml": "\000\023\190\194\191\205\185\016s\214\187\232\246\159%|" +"Resource: /home/pes20/repos/ott/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_lexer.mll": "\235/\157_\190,\194T+\203\250\170*\002\185P" +"Rule: ocaml dependencies mli (%=test10menhir_with_aux_parser )": "]\189\173^\187\247^\235\017P\164\1993\175t\210" +"Rule: ocaml: cmo* -> byte (%=main )": "\198\177,\209\190D6A\149\012\136+'\r\128\149" +"Rule: ocaml: ml -> cmo & cmi (%=main )": "_\204I\193\172@\228nk6).\2087L\208" +"Rule: ocamllex (%=test10menhir_with_aux_lexer )": "\nN\205E?\191\235z\216\222\004\\\173}\204[" +"Rule: ocaml dependencies ml (%=test10menhir_with_aux_lexer )": "\196\170G\138\234\231\249a\212\2354\138\003\241y\145" +"Rule: ocaml: ml -> cmo & cmi (%=test10menhir_with_aux_ast )": "\2274S\174\209\218\015*U\012s\181\212\139Z\185" +"Rule: ocaml dependencies ml (%=main )": "\156>~\212:Q\166\242\007w\165\149\170*.\244" +"Resource: /home/pes20/repos/ott/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_parser_pp.ml": "<\207n\004m,\197\t\208\155H\135\175=\1691" +"Rule: ocaml: mli -> cmi (%=test10menhir_with_aux_parser )": "xV\185S\016\214T\024\012*o\145\251\249\217\244" +"Rule: ocaml dependencies ml (%=test10menhir_with_aux_parser_pp )": "\n\241\016\018\014'\191}\165\246\161\220=\152@\203" +"Rule: ocaml: ml -> cmo & cmi (%=test10menhir_with_aux_parser_pp )": "'\193\002\193\167\030\199z\028\157O\161j\242JJ" +"Resource: /home/pes20/repos/ott/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_ast.ml": "x\164b\156NS\147\235\179e\132\140].\251k" +"Rule: ocaml dependencies ml (%=test10menhir_with_aux_parser )": "M\251\002\174V\216\231\130^\192\029#\001H\023\255" diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/_log b/tests/menhir_tests/test10menhir_with_aux_args/_build/_log new file mode 100644 index 0000000..c46a288 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/_log @@ -0,0 +1,42 @@ +### Starting build. +# Target: ocamlfind ocamlc -config, tags: { } +ocamlfind ocamlc -config +# Target: main.ml.depends, tags: { package(pprint), extension:ml, file:main.ml, ocaml, ocamldep, quiet } +ocamlfind ocamldep -package pprint -modules main.ml > main.ml.depends +# Target: test10menhir_with_aux_ast.ml.depends, tags: { package(pprint), extension:ml, file:test10menhir_with_aux_ast.ml, ocaml, ocamldep, quiet } +ocamlfind ocamldep -package pprint -modules test10menhir_with_aux_ast.ml > test10menhir_with_aux_ast.ml.depends +# Target: test10menhir_with_aux_lexer.mll, tags: { package(pprint), extension:mll, file:test10menhir_with_aux_lexer.mll, lexer, ocaml, ocamllex, quiet } +/home/pes20/.opam/5.2.0/bin/ocamllex.opt -q test10menhir_with_aux_lexer.mll +# Target: test10menhir_with_aux_lexer.ml.depends, tags: { package(pprint), extension:ml, file:test10menhir_with_aux_lexer.ml, ocaml, ocamldep, quiet } +ocamlfind ocamldep -package pprint -modules test10menhir_with_aux_lexer.ml > test10menhir_with_aux_lexer.ml.depends +# Target: test10menhir_with_aux_parser.mly.depends, tags: { package(pprint), extension:mly, file:test10menhir_with_aux_parser.mly, infer, menhir_ocamldep, ocaml, ocamldep, quiet } +menhir --infer --raw-depend --ocamldep 'ocamlfind ocamldep -modules' test10menhir_with_aux_parser.mly > test10menhir_with_aux_parser.mly.depends ++ menhir --infer --raw-depend --ocamldep 'ocamlfind ocamldep -modules' test10menhir_with_aux_parser.mly > test10menhir_with_aux_parser.mly.depends +File "test10menhir_with_aux_parser.mly", line 23, characters 0-1: +Warning: symbol l is unreachable from any of the start symbol(s). +# Target: test10menhir_with_aux_ast.cmo, tags: { package(pprint), byte, compile, extension:cmo, extension:ml, file:test10menhir_with_aux_ast.cmo, file:test10menhir_with_aux_ast.ml, implem, ocaml, quiet } +ocamlfind ocamlc -c -package pprint -o test10menhir_with_aux_ast.cmo test10menhir_with_aux_ast.ml +# Target: test10menhir_with_aux_parser.mly, tags: { package(pprint), byte, compile, extension:ml, extension:mly, file:test10menhir_with_aux_parser.ml, file:test10menhir_with_aux_parser.mly, infer, menhir, ocaml, parser, quiet } +menhir --infer --ocamlc 'ocamlfind ocamlc -package pprint' --infer test10menhir_with_aux_parser.mly ++ menhir --infer --ocamlc 'ocamlfind ocamlc -package pprint' --infer test10menhir_with_aux_parser.mly +File "test10menhir_with_aux_parser.mly", line 23, characters 0-1: +Warning: symbol l is unreachable from any of the start symbol(s). +# Target: test10menhir_with_aux_parser.mli.depends, tags: { package(pprint), extension:mli, file:test10menhir_with_aux_parser.mli, ocaml, ocamldep, quiet } +ocamlfind ocamldep -package pprint -modules test10menhir_with_aux_parser.mli > test10menhir_with_aux_parser.mli.depends +# Target: test10menhir_with_aux_parser.cmi, tags: { package(pprint), byte, compile, extension:mli, file:test10menhir_with_aux_parser.mli, interf, ocaml, quiet } +ocamlfind ocamlc -c -package pprint -o test10menhir_with_aux_parser.cmi test10menhir_with_aux_parser.mli +# Target: test10menhir_with_aux_parser_pp.ml.depends, tags: { package(pprint), extension:ml, file:test10menhir_with_aux_parser_pp.ml, ocaml, ocamldep, quiet } +ocamlfind ocamldep -package pprint -modules test10menhir_with_aux_parser_pp.ml > test10menhir_with_aux_parser_pp.ml.depends +# Target: test10menhir_with_aux_lexer.cmo, tags: { package(pprint), byte, compile, extension:cmo, extension:ml, file:test10menhir_with_aux_lexer.cmo, file:test10menhir_with_aux_lexer.ml, implem, ocaml, quiet } +ocamlfind ocamlc -c -package pprint -o test10menhir_with_aux_lexer.cmo test10menhir_with_aux_lexer.ml +# Target: test10menhir_with_aux_parser_pp.cmo, tags: { package(pprint), byte, compile, extension:cmo, extension:ml, file:test10menhir_with_aux_parser_pp.cmo, file:test10menhir_with_aux_parser_pp.ml, implem, ocaml, quiet } +ocamlfind ocamlc -c -package pprint -o test10menhir_with_aux_parser_pp.cmo test10menhir_with_aux_parser_pp.ml +# Target: main.cmo, tags: { package(pprint), byte, compile, extension:cmo, extension:ml, file:main.cmo, file:main.ml, implem, ocaml, quiet } +ocamlfind ocamlc -c -package pprint -o main.cmo main.ml +# Target: test10menhir_with_aux_parser.ml.depends, tags: { package(pprint), extension:ml, file:test10menhir_with_aux_parser.ml, ocaml, ocamldep, quiet } +ocamlfind ocamldep -package pprint -modules test10menhir_with_aux_parser.ml > test10menhir_with_aux_parser.ml.depends +# Target: test10menhir_with_aux_parser.cmo, tags: { package(pprint), byte, compile, extension:cmo, extension:ml, file:test10menhir_with_aux_parser.cmo, file:test10menhir_with_aux_parser.ml, implem, ocaml, quiet } +ocamlfind ocamlc -c -package pprint -o test10menhir_with_aux_parser.cmo test10menhir_with_aux_parser.ml +# Target: main.byte, tags: { package(pprint), byte, dont_link_with, extension:byte, file:main.byte, link, ocaml, program, quiet } +ocamlfind ocamlc -linkpkg -package pprint test10menhir_with_aux_ast.cmo test10menhir_with_aux_parser.cmo test10menhir_with_aux_lexer.cmo test10menhir_with_aux_parser_pp.cmo main.cmo -o main.byte +# Compilation successful. diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/main.ml b/tests/menhir_tests/test10menhir_with_aux_args/_build/main.ml new file mode 100644 index 0000000..130dd45 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/main.ml @@ -0,0 +1,58 @@ +open Test10menhir_with_aux_ast + +module Lexer = Test10menhir_with_aux_lexer +module Parser = Test10menhir_with_aux_parser +module PP = Test10menhir_with_aux_parser_pp + + +(* +let rec pp_term t : string = + match t with + | T_var x -> Printf.sprintf "%s" x + | T_lam (x,t) -> Printf.sprintf "\\%s. %s" x (pp_term t) + | T_app (t,t') -> Printf.sprintf "(%s %s)" (pp_term t) (pp_term t') + | T_paren t -> Printf.sprintf "(%s)" (pp_term t) +*) + +let () = Printf.printf "enter lambda calculus terms, in the grammar t ::= x | t t | \\x.t | (t)\n" + +let process (line : string) = + let linebuf = Lexing.from_string line in + try + (* Run the parser on this line of input. *) + let t = (Parser.term_start Lexer.token linebuf) in + Printf.printf " "; PPrint.ToChannel.compact stdout (PP.pp_raw_term t); Printf.printf "\n"; + Printf.printf " "; PPrint.ToChannel.compact stdout (PP.pp_term t); Printf.printf "\n" + with + | Lexer.Error msg -> + Printf.fprintf stdout "%s" msg + | Parser.Error -> + Printf.fprintf stdout "%s^\nAt offset %d: syntax error.\n" (String.make (Lexing.lexeme_start linebuf) ' ') (Lexing.lexeme_start linebuf) + +(* +let process (optional_line : string option) = + match optional_line with + | None -> + () + | Some line -> + process line + +let rec repeat channel = + (* Attempt to read one line. *) + let optional_line, continue = Lexer.line channel in + process optional_line; + if continue then + repeat channel + +let () = + repeat (Lexing.from_channel stdin) + *) + +let rec foo () = + let s = read_line () in + process s; flush stdout; + foo () + +let () = foo () + + diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/main.ml.depends b/tests/menhir_tests/test10menhir_with_aux_args/_build/main.ml.depends new file mode 100644 index 0000000..ab1db90 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/main.ml.depends @@ -0,0 +1 @@ +main.ml: Lexing PPrint Printf String Test10menhir_with_aux_ast Test10menhir_with_aux_lexer Test10menhir_with_aux_parser Test10menhir_with_aux_parser_pp diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_ast.ml b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_ast.ml new file mode 100644 index 0000000..c700224 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_ast.ml @@ -0,0 +1,35 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) + +type var = string (* term variable *) + +type l = + | Unknown + | Int of string * l option + | Generated of l + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + +let pp_lexing_position p = + Printf.sprintf "file \"%s\" line %d char %d" + p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol) + +let rec pp_l l = match l with + | Unknown -> "no location information available" + | Generated l -> Printf.sprintf "Generated: %s" (pp_l l) + | Range(p1,p2) -> Printf.sprintf "Range: %s to %s" (pp_lexing_position p1) (pp_lexing_position p2) + | Int(s,lo) -> Printf.sprintf "Int: %s %s" s (match lo with Some l -> pp_l l | None -> "none") + + +type +term = + T_app of term * term * l + | T_foo of term * l + | T_var of var * l + | T_paren of term * l + | T_lambda of var * term * l + + + diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_ast.ml.depends b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_ast.ml.depends new file mode 100644 index 0000000..f7036a6 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_ast.ml.depends @@ -0,0 +1 @@ +test10menhir_with_aux_ast.ml: Lexing Printf diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.ml b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.ml new file mode 100644 index 0000000..a0530eb --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.ml @@ -0,0 +1,236 @@ +# 2 "test10menhir_with_aux_lexer.mll" + +open Test10menhir_with_aux_parser +exception Error of string + +# 7 "test10menhir_with_aux_lexer.ml" +let __ocaml_lex_tables = { + Lexing.lex_base = + "\000\000\245\255\058\000\116\000\248\255\249\255\250\255\251\255\ + \252\255\001\000\254\255\255\255\001\000\253\255\193\000\251\000\ + "; + Lexing.lex_backtrk = + "\255\255\255\255\009\000\009\000\255\255\255\255\255\255\255\255\ + \255\255\010\000\255\255\255\255\255\255\255\255\009\000\008\000\ + "; + Lexing.lex_default = + "\001\000\000\000\255\255\255\255\000\000\000\000\000\000\000\000\ + \000\000\255\255\000\000\000\000\012\000\000\000\255\255\255\255\ + "; + Lexing.lex_trans = + "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\011\000\010\000\013\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \011\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \006\000\005\000\000\000\000\000\000\000\000\000\004\000\009\000\ + \012\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\002\000\002\000\002\000\002\000\002\000\003\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\000\000\007\000\000\000\000\000\000\000\ + \000\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\014\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \008\000\255\255\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \015\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000"; + Lexing.lex_check = + "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\000\000\000\000\012\000\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \000\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \000\000\000\000\255\255\255\255\255\255\255\255\000\000\000\000\ + \009\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\255\255\000\000\255\255\255\255\255\255\ + \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ + \000\000\000\000\000\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\255\255\255\255\255\255\ + \255\255\255\255\255\255\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\002\000\002\000\002\000\ + \002\000\002\000\002\000\002\000\002\000\003\000\003\000\003\000\ + \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ + \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ + \003\000\003\000\003\000\003\000\003\000\003\000\003\000\255\255\ + \255\255\255\255\255\255\255\255\255\255\003\000\003\000\003\000\ + \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ + \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ + \003\000\003\000\003\000\003\000\003\000\003\000\003\000\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \000\000\012\000\014\000\014\000\014\000\014\000\014\000\014\000\ + \014\000\014\000\014\000\014\000\014\000\014\000\014\000\014\000\ + \014\000\014\000\014\000\014\000\014\000\014\000\014\000\014\000\ + \014\000\014\000\014\000\014\000\255\255\255\255\255\255\255\255\ + \255\255\255\255\014\000\014\000\014\000\014\000\014\000\014\000\ + \014\000\014\000\014\000\014\000\014\000\014\000\014\000\014\000\ + \014\000\014\000\014\000\014\000\014\000\014\000\014\000\014\000\ + \014\000\014\000\014\000\014\000\015\000\015\000\015\000\015\000\ + \015\000\015\000\015\000\015\000\015\000\015\000\015\000\015\000\ + \015\000\015\000\015\000\015\000\015\000\015\000\015\000\015\000\ + \015\000\015\000\015\000\015\000\015\000\015\000\255\255\255\255\ + \255\255\255\255\255\255\255\255\015\000\015\000\015\000\015\000\ + \015\000\015\000\015\000\015\000\015\000\015\000\015\000\015\000\ + \015\000\015\000\015\000\015\000\015\000\015\000\015\000\015\000\ + \015\000\015\000\015\000\015\000\015\000\015\000\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ + \255\255\255\255\255\255\255\255"; + Lexing.lex_base_code = + ""; + Lexing.lex_backtrk_code = + ""; + Lexing.lex_default_code = + ""; + Lexing.lex_trans_code = + ""; + Lexing.lex_check_code = + ""; + Lexing.lex_code = + ""; +} + +let rec token lexbuf = + __ocaml_lex_token_rec lexbuf 0 +and __ocaml_lex_token_rec lexbuf __ocaml_lex_state = + match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with + | 0 -> +# 9 "test10menhir_with_aux_lexer.mll" + ( token lexbuf ) +# 172 "test10menhir_with_aux_lexer.ml" + + | 1 -> +# 11 "test10menhir_with_aux_lexer.mll" + ( Lexing.new_line lexbuf; token lexbuf ) +# 177 "test10menhir_with_aux_lexer.ml" + + | 2 -> +# 13 "test10menhir_with_aux_lexer.mll" + ( Lexing.new_line lexbuf; token lexbuf ) +# 182 "test10menhir_with_aux_lexer.ml" + + | 3 -> +# 15 "test10menhir_with_aux_lexer.mll" + ( EOF ) +# 187 "test10menhir_with_aux_lexer.ml" + + | 4 -> +# 17 "test10menhir_with_aux_lexer.mll" + ( BACKSLASH ) +# 192 "test10menhir_with_aux_lexer.ml" + + | 5 -> +# 19 "test10menhir_with_aux_lexer.mll" + ( LPAREN ) +# 197 "test10menhir_with_aux_lexer.ml" + + | 6 -> +# 21 "test10menhir_with_aux_lexer.mll" + ( RPAREN ) +# 202 "test10menhir_with_aux_lexer.ml" + + | 7 -> +# 23 "test10menhir_with_aux_lexer.mll" + ( DOT ) +# 207 "test10menhir_with_aux_lexer.ml" + + | 8 -> +# 25 "test10menhir_with_aux_lexer.mll" + ( FOO ) +# 212 "test10menhir_with_aux_lexer.ml" + + | 9 -> +let +# 26 "test10menhir_with_aux_lexer.mll" + var +# 218 "test10menhir_with_aux_lexer.ml" += Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in +# 27 "test10menhir_with_aux_lexer.mll" + ( VAR ( var) ) +# 222 "test10menhir_with_aux_lexer.ml" + + | 10 -> +# 29 "test10menhir_with_aux_lexer.mll" + ( raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) ) +# 227 "test10menhir_with_aux_lexer.ml" + + | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; + __ocaml_lex_token_rec lexbuf __ocaml_lex_state + +;; + +# 32 "test10menhir_with_aux_lexer.mll" + + +# 237 "test10menhir_with_aux_lexer.ml" diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.ml.depends b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.ml.depends new file mode 100644 index 0000000..52e7b7e --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.ml.depends @@ -0,0 +1 @@ +test10menhir_with_aux_lexer.ml: Lexing Printf Test10menhir_with_aux_parser diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.mll b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.mll new file mode 100644 index 0000000..5208b7f --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_lexer.mll @@ -0,0 +1,35 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) +{ +open Test10menhir_with_aux_parser +exception Error of string +} + +rule token = parse +| [' ' '\t'] + { token lexbuf } +| ' +' + { Lexing.new_line lexbuf; token lexbuf } +| "//" [^'\n']* '\n' + { Lexing.new_line lexbuf; token lexbuf } +| eof + { EOF } +| "\\" + { BACKSLASH } +| "(" + { LPAREN } +| ")" + { RPAREN } +| "." + { DOT } +| "Foo" + { FOO } +| ['a'-'z''A'-'Z']+ as var + { VAR ( var) } +| _ + { raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) } + + +{ +} + diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.ml b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.ml new file mode 100644 index 0000000..1a9908c --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.ml @@ -0,0 +1,456 @@ + +module MenhirBasics = struct + + exception Error + + let _eRR = + fun _s -> + raise Error + + type token = + | VAR of ( +# 11 "test10menhir_with_aux_parser.mly" + (string) +# 15 "test10menhir_with_aux_parser.ml" + ) + | RPAREN + | LPAREN + | FOO + | EOF + | DOT + | BACKSLASH + +end + +include MenhirBasics + +# 2 "test10menhir_with_aux_parser.mly" + +open Test10menhir_with_aux_ast + +# 32 "test10menhir_with_aux_parser.ml" + +type ('s, 'r) _menhir_state = + | MenhirState00 : ('s, _menhir_box_term_start) _menhir_state + (** State 00. + Stack shape : . + Start symbol: term_start. *) + + | MenhirState02 : (('s, _menhir_box_term_start) _menhir_cell1_LPAREN, _menhir_box_term_start) _menhir_state + (** State 02. + Stack shape : LPAREN. + Start symbol: term_start. *) + + | MenhirState03 : (('s, _menhir_box_term_start) _menhir_cell1_FOO, _menhir_box_term_start) _menhir_state + (** State 03. + Stack shape : FOO. + Start symbol: term_start. *) + + | MenhirState06 : (('s, _menhir_box_term_start) _menhir_cell1_BACKSLASH _menhir_cell0_VAR, _menhir_box_term_start) _menhir_state + (** State 06. + Stack shape : BACKSLASH VAR. + Start symbol: term_start. *) + + | MenhirState08 : (('s, _menhir_box_term_start) _menhir_cell1_lhs, _menhir_box_term_start) _menhir_state + (** State 08. + Stack shape : lhs. + Start symbol: term_start. *) + + +and ('s, 'r) _menhir_cell1_lhs = + | MenhirCell1_lhs of 's * ('s, 'r) _menhir_state * (Test10menhir_with_aux_ast.term) * Lexing.position + +and ('s, 'r) _menhir_cell1_BACKSLASH = + | MenhirCell1_BACKSLASH of 's * ('s, 'r) _menhir_state * Lexing.position + +and ('s, 'r) _menhir_cell1_FOO = + | MenhirCell1_FOO of 's * ('s, 'r) _menhir_state * Lexing.position + +and ('s, 'r) _menhir_cell1_LPAREN = + | MenhirCell1_LPAREN of 's * ('s, 'r) _menhir_state * Lexing.position + +and 's _menhir_cell0_VAR = + | MenhirCell0_VAR of 's * ( +# 11 "test10menhir_with_aux_parser.mly" + (string) +# 77 "test10menhir_with_aux_parser.ml" +) * Lexing.position * Lexing.position + +and _menhir_box_term_start = + | MenhirBox_term_start of (Test10menhir_with_aux_ast.term) [@@unboxed] + +let _menhir_action_01 = + fun _endpos_x_ _startpos_x_ x -> + let _endpos = _endpos_x_ in + let _symbolstartpos = _startpos_x_ in + ( +# 39 "test10menhir_with_aux_parser.mly" + ( (*Case 2*) T_var(x,Range(_symbolstartpos,_endpos)) ) +# 90 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_02 = + fun _endpos__3_ _startpos__1_ t -> + let _endpos = _endpos__3_ in + let _symbolstartpos = _startpos__1_ in + ( +# 41 "test10menhir_with_aux_parser.mly" + ( (*Case 2*) T_paren(t,Range(_symbolstartpos,_endpos)) ) +# 100 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_03 = + fun _endpos_t_ _startpos__1_ t x -> + let _endpos = _endpos_t_ in + let _symbolstartpos = _startpos__1_ in + ( +# 57 "test10menhir_with_aux_parser.mly" + ( (*Case 2*) T_lambda(x,t,Range(_symbolstartpos,_endpos)) ) +# 110 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_04 = + fun at -> + ( +# 45 "test10menhir_with_aux_parser.mly" + ( (*Case 1*) at ) +# 118 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_05 = + fun _endpos_at_prime_ _startpos_lhs_ at_prime lhs -> + let _endpos = _endpos_at_prime_ in + let _symbolstartpos = _startpos_lhs_ in + ( +# 47 "test10menhir_with_aux_parser.mly" + ( (*Case 1*) T_app(lhs, at_prime, Range(_symbolstartpos,_endpos)) ) +# 128 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_06 = + fun at -> + ( +# 51 "test10menhir_with_aux_parser.mly" + ( (*Case 1*) at ) +# 136 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_07 = + fun lambda -> + ( +# 53 "test10menhir_with_aux_parser.mly" + ( (*Case 1*) lambda ) +# 144 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_08 = + fun at -> + ( +# 29 "test10menhir_with_aux_parser.mly" + ( (*Case 1*) at ) +# 152 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_09 = + fun _endpos_rhs_prime_ _startpos_lhs_ lhs rhs_prime -> + let _endpos = _endpos_rhs_prime_ in + let _symbolstartpos = _startpos_lhs_ in + ( +# 31 "test10menhir_with_aux_parser.mly" + ( (*Case 2*) T_app(lhs,rhs_prime,Range(_symbolstartpos,_endpos)) ) +# 162 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_10 = + fun lambda -> + ( +# 33 "test10menhir_with_aux_parser.mly" + ( (*Case 1*) lambda ) +# 170 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_11 = + fun _endpos_term_ _startpos__1_ term -> + let _endpos = _endpos_term_ in + let _symbolstartpos = _startpos__1_ in + ( +# 35 "test10menhir_with_aux_parser.mly" + ( (*Case 2*) T_foo(term,Range(_symbolstartpos,_endpos)) ) +# 180 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_action_12 = + fun term -> + ( +# 21 "test10menhir_with_aux_parser.mly" + ( term ) +# 188 "test10menhir_with_aux_parser.ml" + : (Test10menhir_with_aux_ast.term)) + +let _menhir_print_token : token -> string = + fun _tok -> + match _tok with + | BACKSLASH -> + "BACKSLASH" + | DOT -> + "DOT" + | EOF -> + "EOF" + | FOO -> + "FOO" + | LPAREN -> + "LPAREN" + | RPAREN -> + "RPAREN" + | VAR _ -> + "VAR" + +let _menhir_fail : unit -> 'a = + fun () -> + Printf.eprintf "Internal failure -- please contact the parser generator's developers.\n%!"; + assert false + +include struct + + [@@@ocaml.warning "-4-37"] + + let _menhir_run_18 : type ttv_stack. ttv_stack -> _ -> _ -> _menhir_box_term_start = + fun _menhir_stack _v _tok -> + match (_tok : MenhirBasics.token) with + | EOF -> + let term = _v in + let _v = _menhir_action_12 term in + MenhirBox_term_start _v + | _ -> + _eRR () + + let rec _menhir_run_01 : type ttv_stack. ttv_stack -> _ -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s -> + let _startpos = _menhir_lexbuf.Lexing.lex_start_p in + let _endpos = _menhir_lexbuf.Lexing.lex_curr_p in + let _tok = _menhir_lexer _menhir_lexbuf in + let (_endpos_x_, _startpos_x_, x) = (_endpos, _startpos, _v) in + let _v = _menhir_action_01 _endpos_x_ _startpos_x_ x in + _menhir_goto_atomic_term _menhir_stack _menhir_lexbuf _menhir_lexer _endpos_x_ _startpos_x_ _v _menhir_s _tok + + and _menhir_goto_atomic_term : type ttv_stack. ttv_stack -> _ -> _ -> _ -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _startpos _v _menhir_s _tok -> + match _menhir_s with + | MenhirState00 -> + _menhir_run_13 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _startpos _v _menhir_s _tok + | MenhirState02 -> + _menhir_run_13 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _startpos _v _menhir_s _tok + | MenhirState03 -> + _menhir_run_13 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _startpos _v _menhir_s _tok + | MenhirState06 -> + _menhir_run_13 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _startpos _v _menhir_s _tok + | MenhirState08 -> + _menhir_run_11 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok + + and _menhir_run_13 : type ttv_stack. ttv_stack -> _ -> _ -> _ -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _startpos _v _menhir_s _tok -> + match (_tok : MenhirBasics.token) with + | BACKSLASH | LPAREN | VAR _ -> + let (_startpos_at_, at) = (_startpos, _v) in + let _v = _menhir_action_04 at in + _menhir_goto_lhs _menhir_stack _menhir_lexbuf _menhir_lexer _startpos_at_ _v _menhir_s _tok + | EOF | RPAREN -> + let (_endpos_at_, at) = (_endpos, _v) in + let _v = _menhir_action_08 at in + _menhir_goto_term _menhir_stack _menhir_lexbuf _menhir_lexer _endpos_at_ _v _menhir_s _tok + | _ -> + _eRR () + + and _menhir_goto_lhs : type ttv_stack. ttv_stack -> _ -> _ -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _startpos _v _menhir_s _tok -> + let _menhir_stack = MenhirCell1_lhs (_menhir_stack, _menhir_s, _v, _startpos) in + match (_tok : MenhirBasics.token) with + | VAR _v_0 -> + _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer _v_0 MenhirState08 + | LPAREN -> + _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer MenhirState08 + | BACKSLASH -> + _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer MenhirState08 + | _ -> + _menhir_fail () + + and _menhir_run_02 : type ttv_stack. ttv_stack -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s -> + let _startpos = _menhir_lexbuf.Lexing.lex_start_p in + let _menhir_stack = MenhirCell1_LPAREN (_menhir_stack, _menhir_s, _startpos) in + let _menhir_s = MenhirState02 in + let _tok = _menhir_lexer _menhir_lexbuf in + match (_tok : MenhirBasics.token) with + | VAR _v -> + _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s + | LPAREN -> + _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | FOO -> + _menhir_run_03 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | BACKSLASH -> + _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | _ -> + _eRR () + + and _menhir_run_03 : type ttv_stack. ttv_stack -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s -> + let _startpos = _menhir_lexbuf.Lexing.lex_start_p in + let _menhir_stack = MenhirCell1_FOO (_menhir_stack, _menhir_s, _startpos) in + let _menhir_s = MenhirState03 in + let _tok = _menhir_lexer _menhir_lexbuf in + match (_tok : MenhirBasics.token) with + | VAR _v -> + _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s + | LPAREN -> + _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | FOO -> + _menhir_run_03 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | BACKSLASH -> + _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | _ -> + _eRR () + + and _menhir_run_04 : type ttv_stack. ttv_stack -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s -> + let _startpos = _menhir_lexbuf.Lexing.lex_start_p in + let _menhir_stack = MenhirCell1_BACKSLASH (_menhir_stack, _menhir_s, _startpos) in + let _tok = _menhir_lexer _menhir_lexbuf in + match (_tok : MenhirBasics.token) with + | VAR _v -> + let _startpos = _menhir_lexbuf.Lexing.lex_start_p in + let _endpos = _menhir_lexbuf.Lexing.lex_curr_p in + let _menhir_stack = MenhirCell0_VAR (_menhir_stack, _v, _startpos, _endpos) in + let _tok = _menhir_lexer _menhir_lexbuf in + (match (_tok : MenhirBasics.token) with + | DOT -> + let _menhir_s = MenhirState06 in + let _tok = _menhir_lexer _menhir_lexbuf in + (match (_tok : MenhirBasics.token) with + | VAR _v -> + _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s + | LPAREN -> + _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | FOO -> + _menhir_run_03 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | BACKSLASH -> + _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | _ -> + _eRR ()) + | _ -> + _eRR ()) + | _ -> + _eRR () + + and _menhir_goto_term : type ttv_stack. ttv_stack -> _ -> _ -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _menhir_s _tok -> + match _menhir_s with + | MenhirState00 -> + _menhir_run_18 _menhir_stack _v _tok + | MenhirState02 -> + _menhir_run_15 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok + | MenhirState03 -> + _menhir_run_14 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok + | MenhirState06 -> + _menhir_run_07 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok + | _ -> + _menhir_fail () + + and _menhir_run_15 : type ttv_stack. (ttv_stack, _menhir_box_term_start) _menhir_cell1_LPAREN -> _ -> _ -> _ -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok -> + match (_tok : MenhirBasics.token) with + | RPAREN -> + let _endpos_0 = _menhir_lexbuf.Lexing.lex_curr_p in + let _tok = _menhir_lexer _menhir_lexbuf in + let MenhirCell1_LPAREN (_menhir_stack, _menhir_s, _startpos__1_) = _menhir_stack in + let (t, _endpos__3_) = (_v, _endpos_0) in + let _v = _menhir_action_02 _endpos__3_ _startpos__1_ t in + _menhir_goto_atomic_term _menhir_stack _menhir_lexbuf _menhir_lexer _endpos__3_ _startpos__1_ _v _menhir_s _tok + | _ -> + _eRR () + + and _menhir_run_14 : type ttv_stack. (ttv_stack, _menhir_box_term_start) _menhir_cell1_FOO -> _ -> _ -> _ -> _ -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok -> + let MenhirCell1_FOO (_menhir_stack, _menhir_s, _startpos__1_) = _menhir_stack in + let (_endpos_term_, term) = (_endpos, _v) in + let _v = _menhir_action_11 _endpos_term_ _startpos__1_ term in + _menhir_goto_term _menhir_stack _menhir_lexbuf _menhir_lexer _endpos_term_ _v _menhir_s _tok + + and _menhir_run_07 : type ttv_stack. (ttv_stack, _menhir_box_term_start) _menhir_cell1_BACKSLASH _menhir_cell0_VAR -> _ -> _ -> _ -> _ -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok -> + let MenhirCell0_VAR (_menhir_stack, x, _, _) = _menhir_stack in + let MenhirCell1_BACKSLASH (_menhir_stack, _menhir_s, _startpos__1_) = _menhir_stack in + let (_endpos_t_, t) = (_endpos, _v) in + let _v = _menhir_action_03 _endpos_t_ _startpos__1_ t x in + _menhir_goto_lambda _menhir_stack _menhir_lexbuf _menhir_lexer _endpos_t_ _v _menhir_s _tok + + and _menhir_goto_lambda : type ttv_stack. ttv_stack -> _ -> _ -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _menhir_s _tok -> + match _menhir_s with + | MenhirState00 -> + _menhir_run_12 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _menhir_s _tok + | MenhirState02 -> + _menhir_run_12 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _menhir_s _tok + | MenhirState03 -> + _menhir_run_12 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _menhir_s _tok + | MenhirState06 -> + _menhir_run_12 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _menhir_s _tok + | MenhirState08 -> + _menhir_run_10 _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok + + and _menhir_run_12 : type ttv_stack. ttv_stack -> _ -> _ -> _ -> _ -> (ttv_stack, _menhir_box_term_start) _menhir_state -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _menhir_s _tok -> + let (_endpos_lambda_, lambda) = (_endpos, _v) in + let _v = _menhir_action_10 lambda in + _menhir_goto_term _menhir_stack _menhir_lexbuf _menhir_lexer _endpos_lambda_ _v _menhir_s _tok + + and _menhir_run_10 : type ttv_stack. (ttv_stack, _menhir_box_term_start) _menhir_cell1_lhs -> _ -> _ -> _ -> _ -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok -> + let (_endpos_lambda_, lambda) = (_endpos, _v) in + let _v = _menhir_action_07 lambda in + _menhir_goto_rhs _menhir_stack _menhir_lexbuf _menhir_lexer _endpos_lambda_ _v _tok + + and _menhir_goto_rhs : type ttv_stack. (ttv_stack, _menhir_box_term_start) _menhir_cell1_lhs -> _ -> _ -> _ -> _ -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok -> + let MenhirCell1_lhs (_menhir_stack, _menhir_s, lhs, _startpos_lhs_) = _menhir_stack in + let (_endpos_rhs_prime_, rhs_prime) = (_endpos, _v) in + let _v = _menhir_action_09 _endpos_rhs_prime_ _startpos_lhs_ lhs rhs_prime in + _menhir_goto_term _menhir_stack _menhir_lexbuf _menhir_lexer _endpos_rhs_prime_ _v _menhir_s _tok + + and _menhir_run_11 : type ttv_stack. (ttv_stack, _menhir_box_term_start) _menhir_cell1_lhs -> _ -> _ -> _ -> _ -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer _endpos _v _tok -> + match (_tok : MenhirBasics.token) with + | BACKSLASH | LPAREN | VAR _ -> + let MenhirCell1_lhs (_menhir_stack, _menhir_s, lhs, _startpos_lhs_) = _menhir_stack in + let (_endpos_at_prime_, at_prime) = (_endpos, _v) in + let _v = _menhir_action_05 _endpos_at_prime_ _startpos_lhs_ at_prime lhs in + _menhir_goto_lhs _menhir_stack _menhir_lexbuf _menhir_lexer _startpos_lhs_ _v _menhir_s _tok + | EOF | RPAREN -> + let (_endpos_at_, at) = (_endpos, _v) in + let _v = _menhir_action_06 at in + _menhir_goto_rhs _menhir_stack _menhir_lexbuf _menhir_lexer _endpos_at_ _v _tok + | _ -> + _eRR () + + let _menhir_run_00 : type ttv_stack. ttv_stack -> _ -> _ -> _menhir_box_term_start = + fun _menhir_stack _menhir_lexbuf _menhir_lexer -> + let _menhir_s = MenhirState00 in + let _tok = _menhir_lexer _menhir_lexbuf in + match (_tok : MenhirBasics.token) with + | VAR _v -> + _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s + | LPAREN -> + _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | FOO -> + _menhir_run_03 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | BACKSLASH -> + _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s + | _ -> + _eRR () + +end + +let term_start = + fun _menhir_lexer _menhir_lexbuf -> + let _menhir_stack = () in + let MenhirBox_term_start v = _menhir_run_00 _menhir_stack _menhir_lexbuf _menhir_lexer in + v diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.ml.depends b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.ml.depends new file mode 100644 index 0000000..a149121 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.ml.depends @@ -0,0 +1 @@ +test10menhir_with_aux_parser.ml: Lexing Printf Test10menhir_with_aux_ast diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mli b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mli new file mode 100644 index 0000000..25c9044 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mli @@ -0,0 +1,19 @@ + +(* The type of tokens. *) + +type token = + | VAR of (string) + | RPAREN + | LPAREN + | FOO + | EOF + | DOT + | BACKSLASH + +(* This exception is raised by the monolithic API functions. *) + +exception Error + +(* The monolithic API. *) + +val term_start: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Test10menhir_with_aux_ast.term) diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mli.depends b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mli.depends new file mode 100644 index 0000000..884028f --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mli.depends @@ -0,0 +1 @@ +test10menhir_with_aux_parser.mli: Lexing Test10menhir_with_aux_ast diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mly b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mly new file mode 100644 index 0000000..f9cc517 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mly @@ -0,0 +1,58 @@ +/* generated by Ott 0.34 from: test10menhir_with_aux.ott */ +%{ +open Test10menhir_with_aux_ast +%} + +%token BACKSLASH (* BACKSLASH *) +%token LPAREN (* ( *) +%token RPAREN (* ) *) +%token DOT (* . *) +%token FOO (* Foo *) +%token VAR (* metavarroot var *) +%token EOF (* added by Ott *) + +%start term_start + + +%% + +term_start: +| term = term EOF + { term } + +l: +| (* :: Unknown *) + { (*Case 1*) Unknown } + +term: +| at = atomic_term (* at :: T_at *) + { (*Case 1*) at } +| lhs = lhs rhs_prime = rhs (* lhs rhs' :: T_app *) + { (*Case 2*) T_app(lhs,rhs_prime,Range($symbolstartpos,$endpos)) } +| lambda = lambda (* lambda :: T_fn *) + { (*Case 1*) lambda } +| FOO term = term (* Foo term :: T_foo *) + { (*Case 2*) T_foo(term,Range($symbolstartpos,$endpos)) } + +atomic_term: +| x = VAR (* x :: T_var *) + { (*Case 2*) T_var(x,Range($symbolstartpos,$endpos)) } +| LPAREN t = term RPAREN (* ( t ) :: T_paren *) + { (*Case 2*) T_paren(t,Range($symbolstartpos,$endpos)) } + +lhs: +| at = atomic_term (* at :: T_at_lhs *) + { (*Case 1*) at } +| lhs = lhs at_prime = atomic_term (* lhs at' :: T_app_lhs *) + { (*Case 1*) T_app(lhs, at_prime, Range($symbolstartpos,$endpos)) } + +rhs: +| at = atomic_term (* at :: T_at_rhs *) + { (*Case 1*) at } +| lambda = lambda (* lambda :: T_fn_rhs *) + { (*Case 1*) lambda } + +lambda: +| BACKSLASH x = VAR DOT t = term (* \ x . t :: T_lambda *) + { (*Case 2*) T_lambda(x,t,Range($symbolstartpos,$endpos)) } + diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mly.depends b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mly.depends new file mode 100644 index 0000000..6ca42b3 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser.mly.depends @@ -0,0 +1,2 @@ +test10menhir_with_aux_parser.ml: Lexing Test10menhir_with_aux_ast +test10menhir_with_aux_parser.mli: Lexing Test10menhir_with_aux_ast diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser_pp.ml b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser_pp.ml new file mode 100644 index 0000000..0dea08e --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser_pp.ml @@ -0,0 +1,27 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) +open PPrint +open Test10menhir_with_aux_ast + +let rec pp_raw_var x = string "\"" ^^ string x ^^ string "\"" + +and pp_raw_l l = pp_l l + +and pp_raw_term x = match x with +| T_app(lhs,rhs_prime,ott_menhir_loc) -> string "T_app" ^^ string "(" ^^ pp_raw_term lhs ^^ string "," ^^ pp_raw_term rhs_prime ^^ string ")" +| T_foo(term,ott_menhir_loc) -> string "T_foo" ^^ string "(" ^^ pp_raw_term term ^^ string ")" +| T_var(x,ott_menhir_loc) -> string "T_var" ^^ string "(" ^^ pp_raw_var x ^^ string ")" +| T_paren(t,ott_menhir_loc) -> string "T_paren" ^^ string "(" ^^ pp_raw_term t ^^ string ")" +| T_lambda(x,t,ott_menhir_loc) -> string "T_lambda" ^^ string "(" ^^ pp_raw_var x ^^ string "," ^^ pp_raw_term t ^^ string ")" + + +let rec pp_var x = string x ^^ string "" + +and pp_l l = pp_l l + +and pp_term x = match x with +| T_app(lhs,rhs_prime,ott_menhir_loc) -> group(string "" ^^ pp_term lhs ^^ break 1 ^^ pp_term rhs_prime ^^ string "") +| T_foo(term,ott_menhir_loc) -> group(string "" ^^ string "Foo" ^^ break 1 ^^ nest 2 (pp_term term) ^^ string "") +| T_var(x,ott_menhir_loc) -> pp_var x +| T_paren(t,ott_menhir_loc) -> group(string "" ^^ string "(" ^^ break 1 ^^ nest 2 (pp_term t) ^^ break 1 ^^ string ")" ^^ string "") +| T_lambda(x,t,ott_menhir_loc) -> group(string "" ^^ string "\\" ^^ break 1 ^^ pp_var x ^^ break 1 ^^ string "." ^^ break 1 ^^ nest 2 (pp_term t) ^^ string "") + diff --git a/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser_pp.ml.depends b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser_pp.ml.depends new file mode 100644 index 0000000..1bf0090 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/_build/test10menhir_with_aux_parser_pp.ml.depends @@ -0,0 +1 @@ +test10menhir_with_aux_parser_pp.ml: PPrint Test10menhir_with_aux_ast diff --git a/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux.tex b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux.tex new file mode 100644 index 0000000..3a59a41 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux.tex @@ -0,0 +1,95 @@ +% generated by Ott 0.34 from: test10menhir_with_aux.ott +\documentclass[11pt]{article} +\usepackage{amsmath,amssymb} +\usepackage{supertabular} +\usepackage{geometry} +\usepackage{ifthen} +\usepackage{alltt}%hack +\geometry{a4paper,dvips,twoside,left=22.5mm,right=22.5mm,top=20mm,bottom=30mm} +\usepackage{color} +\newcommand{\ottdrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\ottdrulename{#4}}} +\newcommand{\ottusedrule}[1]{\[#1\]} +\newcommand{\ottpremise}[1]{ #1 \\} +\newenvironment{ottdefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{} +\newenvironment{ottfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}} +\newcommand{\ottfunclause}[2]{ #1 \equiv #2 \\} +\newcommand{\ottnt}[1]{\mathit{#1}} +\newcommand{\ottmv}[1]{\mathit{#1}} +\newcommand{\ottkw}[1]{\mathbf{#1}} +\newcommand{\ottsym}[1]{#1} +\newcommand{\ottcom}[1]{\text{#1}} +\newcommand{\ottdrulename}[1]{\textsc{#1}} +\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}} +\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}} +\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}} +\newcommand{\ottgrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}} +\newcommand{\ottmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}} +\newcommand{\ottrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}} +\newcommand{\ottprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$} +\newcommand{\ottfirstprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}} +\newcommand{\ottlongprodline}[2]{& & $#1$ & \multicolumn{4}{l}{$#2$}} +\newcommand{\ottfirstlongprodline}[2]{\ottlongprodline{#1}{#2}} +\newcommand{\ottbindspecprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}} +\newcommand{\ottprodnewline}{\\} +\newcommand{\ottinterrule}{\\[5.0mm]} +\newcommand{\ottafterlastrule}{\\} +\newcommand{\ottmetavars}{ +\ottmetavartabular{ + $ \mathit{var} ,\, \mathit{x} $ & \ottcom{term variable} \\ +}} + +\newcommand{\ottl}{ +\ottrulehead{\ottnt{l}}{::=}{\ottcom{Source location}}\ottprodnewline +\ottfirstprodline{|}{}{}{}{}{}} + +\newcommand{\ottterm}{ +\ottrulehead{\ottnt{term} ,\ \ottnt{v} ,\ \ottnt{t}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{t} \, \ottnt{t}' \, \ottnt{l}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottsym{\{} \ottnt{t} \ottsym{/} \mathit{x} \ottsym{\}} \ottnt{t'} \, \ottnt{l}} {\textsf{M}}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{Foo} \, \ottnt{term} \, \ottnt{l}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\mathit{x} \, \ottnt{l}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottsym{(} \ottnt{t} \ottsym{)} \ottnt{l}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\lambda \mathit{x} \ottsym{.} \ottnt{t} \, \ottnt{l}}{}{}{}{}} + +\newcommand{\ottterminals}{ +\ottrulehead{\ottnt{terminals}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{ \lambda }{}{}{}{}\ottprodnewline +\ottprodline{|}{ \longrightarrow }{}{}{}{}} + +\newcommand{\ottformula}{ +\ottrulehead{\ottnt{formula}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{judgement}}{}{}{}{}} + +\newcommand{\ottjudgement}{ +\ottrulehead{\ottnt{judgement}}{::=}{}} + +\newcommand{\ottuserXXsyntax}{ +\ottrulehead{\ottnt{user\_syntax}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\mathit{var}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{l}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{term}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{terminals}}{}{}{}{}} + +\newcommand{\ottgrammar}{\ottgrammartabular{ +\ottl\ottinterrule +\ottterm\ottinterrule +\ottterminals\ottinterrule +\ottformula\ottinterrule +\ottjudgement\ottinterrule +\ottuserXXsyntax\ottafterlastrule +}} + +% defnss +\newcommand{\ottdefnss}{ +} + +\newcommand{\ottall}{\ottmetavars\\[0pt] +\ottgrammar\\[5.0mm] +\ottdefnss} + +\begin{document} +\ottall + +\begin{verbatim} +\end{verbatim} +\end{document} diff --git a/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_ast.ml b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_ast.ml new file mode 100644 index 0000000..c700224 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_ast.ml @@ -0,0 +1,35 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) + +type var = string (* term variable *) + +type l = + | Unknown + | Int of string * l option + | Generated of l + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + +let pp_lexing_position p = + Printf.sprintf "file \"%s\" line %d char %d" + p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol) + +let rec pp_l l = match l with + | Unknown -> "no location information available" + | Generated l -> Printf.sprintf "Generated: %s" (pp_l l) + | Range(p1,p2) -> Printf.sprintf "Range: %s to %s" (pp_lexing_position p1) (pp_lexing_position p2) + | Int(s,lo) -> Printf.sprintf "Int: %s %s" s (match lo with Some l -> pp_l l | None -> "none") + + +type +term = + T_app of term * term * l + | T_foo of term * l + | T_var of var * l + | T_paren of term * l + | T_lambda of var * term * l + + + diff --git a/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_lexer.mll b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_lexer.mll new file mode 100644 index 0000000..5208b7f --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_lexer.mll @@ -0,0 +1,35 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) +{ +open Test10menhir_with_aux_parser +exception Error of string +} + +rule token = parse +| [' ' '\t'] + { token lexbuf } +| ' +' + { Lexing.new_line lexbuf; token lexbuf } +| "//" [^'\n']* '\n' + { Lexing.new_line lexbuf; token lexbuf } +| eof + { EOF } +| "\\" + { BACKSLASH } +| "(" + { LPAREN } +| ")" + { RPAREN } +| "." + { DOT } +| "Foo" + { FOO } +| ['a'-'z''A'-'Z']+ as var + { VAR ( var) } +| _ + { raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) } + + +{ +} + diff --git a/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_parser.mly b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_parser.mly new file mode 100644 index 0000000..f9cc517 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_parser.mly @@ -0,0 +1,58 @@ +/* generated by Ott 0.34 from: test10menhir_with_aux.ott */ +%{ +open Test10menhir_with_aux_ast +%} + +%token BACKSLASH (* BACKSLASH *) +%token LPAREN (* ( *) +%token RPAREN (* ) *) +%token DOT (* . *) +%token FOO (* Foo *) +%token VAR (* metavarroot var *) +%token EOF (* added by Ott *) + +%start term_start + + +%% + +term_start: +| term = term EOF + { term } + +l: +| (* :: Unknown *) + { (*Case 1*) Unknown } + +term: +| at = atomic_term (* at :: T_at *) + { (*Case 1*) at } +| lhs = lhs rhs_prime = rhs (* lhs rhs' :: T_app *) + { (*Case 2*) T_app(lhs,rhs_prime,Range($symbolstartpos,$endpos)) } +| lambda = lambda (* lambda :: T_fn *) + { (*Case 1*) lambda } +| FOO term = term (* Foo term :: T_foo *) + { (*Case 2*) T_foo(term,Range($symbolstartpos,$endpos)) } + +atomic_term: +| x = VAR (* x :: T_var *) + { (*Case 2*) T_var(x,Range($symbolstartpos,$endpos)) } +| LPAREN t = term RPAREN (* ( t ) :: T_paren *) + { (*Case 2*) T_paren(t,Range($symbolstartpos,$endpos)) } + +lhs: +| at = atomic_term (* at :: T_at_lhs *) + { (*Case 1*) at } +| lhs = lhs at_prime = atomic_term (* lhs at' :: T_app_lhs *) + { (*Case 1*) T_app(lhs, at_prime, Range($symbolstartpos,$endpos)) } + +rhs: +| at = atomic_term (* at :: T_at_rhs *) + { (*Case 1*) at } +| lambda = lambda (* lambda :: T_fn_rhs *) + { (*Case 1*) lambda } + +lambda: +| BACKSLASH x = VAR DOT t = term (* \ x . t :: T_lambda *) + { (*Case 2*) T_lambda(x,t,Range($symbolstartpos,$endpos)) } + diff --git a/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_parser_pp.ml b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_parser_pp.ml new file mode 100644 index 0000000..0dea08e --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_args/test10menhir_with_aux_parser_pp.ml @@ -0,0 +1,27 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) +open PPrint +open Test10menhir_with_aux_ast + +let rec pp_raw_var x = string "\"" ^^ string x ^^ string "\"" + +and pp_raw_l l = pp_l l + +and pp_raw_term x = match x with +| T_app(lhs,rhs_prime,ott_menhir_loc) -> string "T_app" ^^ string "(" ^^ pp_raw_term lhs ^^ string "," ^^ pp_raw_term rhs_prime ^^ string ")" +| T_foo(term,ott_menhir_loc) -> string "T_foo" ^^ string "(" ^^ pp_raw_term term ^^ string ")" +| T_var(x,ott_menhir_loc) -> string "T_var" ^^ string "(" ^^ pp_raw_var x ^^ string ")" +| T_paren(t,ott_menhir_loc) -> string "T_paren" ^^ string "(" ^^ pp_raw_term t ^^ string ")" +| T_lambda(x,t,ott_menhir_loc) -> string "T_lambda" ^^ string "(" ^^ pp_raw_var x ^^ string "," ^^ pp_raw_term t ^^ string ")" + + +let rec pp_var x = string x ^^ string "" + +and pp_l l = pp_l l + +and pp_term x = match x with +| T_app(lhs,rhs_prime,ott_menhir_loc) -> group(string "" ^^ pp_term lhs ^^ break 1 ^^ pp_term rhs_prime ^^ string "") +| T_foo(term,ott_menhir_loc) -> group(string "" ^^ string "Foo" ^^ break 1 ^^ nest 2 (pp_term term) ^^ string "") +| T_var(x,ott_menhir_loc) -> pp_var x +| T_paren(t,ott_menhir_loc) -> group(string "" ^^ string "(" ^^ break 1 ^^ nest 2 (pp_term t) ^^ break 1 ^^ string ")" ^^ string "") +| T_lambda(x,t,ott_menhir_loc) -> group(string "" ^^ string "\\" ^^ break 1 ^^ pp_var x ^^ break 1 ^^ string "." ^^ break 1 ^^ nest 2 (pp_term t) ^^ string "") + diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/_build/_digests b/tests/menhir_tests/test10menhir_with_aux_rules/_build/_digests new file mode 100644 index 0000000..3cf9497 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/_build/_digests @@ -0,0 +1,3 @@ +"Rule: ocaml dependencies ml (%=main )": "\031\003U\156\162\251\rmzV\197#\238\182\b;" +"Resource: /home/pes20/repos/ott/tests/menhir_tests/test10menhir_with_aux_rules/main.ml": "fk.\229r{\205@\161\020\b\148^C\n\137" +"Resource: /home/pes20/repos/ott/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_ast.ml": "rWX\212\142\163G\025\r7\022\254\255@\029w" diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/_build/_log b/tests/menhir_tests/test10menhir_with_aux_rules/_build/_log new file mode 100644 index 0000000..5385579 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/_build/_log @@ -0,0 +1,14 @@ +### Starting build. +# Target: ocamlfind ocamlc -config, tags: { } +ocamlfind ocamlc -config +# Target: main.ml.depends, tags: { package(pprint), extension:ml, file:main.ml, ocaml, ocamldep, quiet } +ocamlfind ocamldep -package pprint -modules main.ml > main.ml.depends +# Target: test10menhir_with_aux_ast.ml.depends, tags: { package(pprint), extension:ml, file:test10menhir_with_aux_ast.ml, ocaml, ocamldep, quiet } +ocamlfind ocamldep -package pprint -modules test10menhir_with_aux_ast.ml > test10menhir_with_aux_ast.ml.depends ++ ocamlfind ocamldep -package pprint -modules test10menhir_with_aux_ast.ml > test10menhir_with_aux_ast.ml.depends +File "test10menhir_with_aux_ast.ml", line 27, characters 9-11: +27 | term_aux := + ^^ +Error: Syntax error +Command exited with code 2. +# Compilation unsuccessful. diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/_build/main.ml b/tests/menhir_tests/test10menhir_with_aux_rules/_build/main.ml new file mode 100644 index 0000000..39ca044 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/_build/main.ml @@ -0,0 +1,59 @@ +open Test10menhir_with_aux_ast + +module Lexer = Test10menhir_with_aux_lexer +module Parser = Test10menhir_with_aux_parser +module PP = Test10menhir_with_aux_parser_pp + + +(* +let rec pp_term t : string = + match t with + | T_var x -> Printf.sprintf "%s" x + | T_lam (x,t) -> Printf.sprintf "\\%s. %s" x (pp_term t) + | T_app (t,t') -> Printf.sprintf "(%s %s)" (pp_term t) (pp_term t') + | T_paren t -> Printf.sprintf "(%s)" (pp_term t) +*) + +let () = Printf.printf "enter lambda calculus terms, in the grammar t ::= x | t t | \\x.t | (t)\n" + +let process (line : string) = + let linebuf = Lexing.from_string line in + try + (* Run the parser on this line of input. *) + let t = (Parser.term_start Lexer.token linebuf) in + Printf.printf " "; PPrint.ToChannel.compact stdout (PP.pp_raw_term t); Printf.printf "\n"; + (* Printf.printf " "; PPrint.ToChannel.compact stdout (PP.pp_term t); Printf.printf "\n"*) + Printf.printf " "; PPrint.ToChannel.pretty 1.0 80 stdout (PP.pp_term t); Printf.printf "\n" + with + | Lexer.Error msg -> + Printf.fprintf stdout "%s" msg + | Parser.Error -> + Printf.fprintf stdout "%s^\nAt offset %d: syntax error.\n" (String.make (Lexing.lexeme_start linebuf) ' ') (Lexing.lexeme_start linebuf) + +(* +let process (optional_line : string option) = + match optional_line with + | None -> + () + | Some line -> + process line + +let rec repeat channel = + (* Attempt to read one line. *) + let optional_line, continue = Lexer.line channel in + process optional_line; + if continue then + repeat channel + +let () = + repeat (Lexing.from_channel stdin) + *) + +let rec foo () = + let s = read_line () in + process s; flush stdout; + foo () + +let () = foo () + + diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/_build/main.ml.depends b/tests/menhir_tests/test10menhir_with_aux_rules/_build/main.ml.depends new file mode 100644 index 0000000..ab1db90 --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/_build/main.ml.depends @@ -0,0 +1 @@ +main.ml: Lexing PPrint Printf String Test10menhir_with_aux_ast Test10menhir_with_aux_lexer Test10menhir_with_aux_parser Test10menhir_with_aux_parser_pp diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/_build/test10menhir_with_aux_ast.ml b/tests/menhir_tests/test10menhir_with_aux_rules/_build/test10menhir_with_aux_ast.ml new file mode 100644 index 0000000..12c50bf --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/_build/test10menhir_with_aux_ast.ml @@ -0,0 +1,38 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) + +type var = string (* term variable *) + +type l = + | Unknown + | Int of string * l option + | Generated of l + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + +let pp_lexing_position p = + Printf.sprintf "file \"%s\" line %d char %d" + p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol) + +let rec pp_l l = match l with + | Unknown -> "no location information available" + | Generated l -> Printf.sprintf "Generated: %s" (pp_l l) + | Range(p1,p2) -> Printf.sprintf "Range: %s to %s" (pp_lexing_position p1) (pp_lexing_position p2) + | Int(s,lo) -> Printf.sprintf "Int: %s %s" s (match lo with Some l -> pp_l l | None -> "none") + + +type +term_aux := + T_app of term * term + | T_foo of term + | T_var of var + | T_paren of term + | T_lambda of var * term + +and term := + T_aux of term_aux * l + + + diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/_build/test10menhir_with_aux_ast.ml.depends b/tests/menhir_tests/test10menhir_with_aux_rules/_build/test10menhir_with_aux_ast.ml.depends new file mode 100644 index 0000000..486fb9b --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/_build/test10menhir_with_aux_ast.ml.depends @@ -0,0 +1 @@ +test10menhir_with_aux_ast.ml: diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux.tex b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux.tex new file mode 100644 index 0000000..875361c --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux.tex @@ -0,0 +1,101 @@ +% generated by Ott 0.34 from: test10menhir_with_aux.ott +\documentclass[11pt]{article} +\usepackage{amsmath,amssymb} +\usepackage{supertabular} +\usepackage{geometry} +\usepackage{ifthen} +\usepackage{alltt}%hack +\geometry{a4paper,dvips,twoside,left=22.5mm,right=22.5mm,top=20mm,bottom=30mm} +\usepackage{color} +\newcommand{\ottdrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\ottdrulename{#4}}} +\newcommand{\ottusedrule}[1]{\[#1\]} +\newcommand{\ottpremise}[1]{ #1 \\} +\newenvironment{ottdefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{} +\newenvironment{ottfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}} +\newcommand{\ottfunclause}[2]{ #1 \equiv #2 \\} +\newcommand{\ottnt}[1]{\mathit{#1}} +\newcommand{\ottmv}[1]{\mathit{#1}} +\newcommand{\ottkw}[1]{\mathbf{#1}} +\newcommand{\ottsym}[1]{#1} +\newcommand{\ottcom}[1]{\text{#1}} +\newcommand{\ottdrulename}[1]{\textsc{#1}} +\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}} +\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}} +\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}} +\newcommand{\ottgrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}} +\newcommand{\ottmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}} +\newcommand{\ottrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}} +\newcommand{\ottprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$} +\newcommand{\ottfirstprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}} +\newcommand{\ottlongprodline}[2]{& & $#1$ & \multicolumn{4}{l}{$#2$}} +\newcommand{\ottfirstlongprodline}[2]{\ottlongprodline{#1}{#2}} +\newcommand{\ottbindspecprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}} +\newcommand{\ottprodnewline}{\\} +\newcommand{\ottinterrule}{\\[5.0mm]} +\newcommand{\ottafterlastrule}{\\} +\newcommand{\ottmetavars}{ +\ottmetavartabular{ + $ \mathit{var} ,\, \mathit{x} $ & \ottcom{term variable} \\ +}} + +\newcommand{\ottl}{ +\ottrulehead{\ottnt{l}}{::=}{\ottcom{Source location}}\ottprodnewline +\ottfirstprodline{|}{}{}{}{}{}} + +\newcommand{\otttermXXaux}{ +\ottrulehead{\ottnt{term\_aux}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{t} \, \ottnt{t}'}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottsym{\{} \ottnt{t} \ottsym{/} \mathit{x} \ottsym{\}} \ottnt{t'}} {\textsf{M}}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{Foo} \, \ottnt{term}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\mathit{x}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottsym{(} \ottnt{t} \ottsym{)}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\lambda \mathit{x} \ottsym{.} \ottnt{t}}{}{}{}{}} + +\newcommand{\ottterm}{ +\ottrulehead{\ottnt{term} ,\ \ottnt{v} ,\ \ottnt{t}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{term\_aux} \, \ottnt{l}}{}{}{}{}} + +\newcommand{\ottterminals}{ +\ottrulehead{\ottnt{terminals}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{ \lambda }{}{}{}{}\ottprodnewline +\ottprodline{|}{ \longrightarrow }{}{}{}{}} + +\newcommand{\ottformula}{ +\ottrulehead{\ottnt{formula}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{judgement}}{}{}{}{}} + +\newcommand{\ottjudgement}{ +\ottrulehead{\ottnt{judgement}}{::=}{}} + +\newcommand{\ottuserXXsyntax}{ +\ottrulehead{\ottnt{user\_syntax}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\mathit{var}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{l}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{term\_aux}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{term}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{terminals}}{}{}{}{}} + +\newcommand{\ottgrammar}{\ottgrammartabular{ +\ottl\ottinterrule +\otttermXXaux\ottinterrule +\ottterm\ottinterrule +\ottterminals\ottinterrule +\ottformula\ottinterrule +\ottjudgement\ottinterrule +\ottuserXXsyntax\ottafterlastrule +}} + +% defnss +\newcommand{\ottdefnss}{ +} + +\newcommand{\ottall}{\ottmetavars\\[0pt] +\ottgrammar\\[5.0mm] +\ottdefnss} + +\begin{document} +\ottall + +\begin{verbatim} +\end{verbatim} +\end{document} diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_ast.ml b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_ast.ml new file mode 100644 index 0000000..12c50bf --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_ast.ml @@ -0,0 +1,38 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) + +type var = string (* term variable *) + +type l = + | Unknown + | Int of string * l option + | Generated of l + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + +let pp_lexing_position p = + Printf.sprintf "file \"%s\" line %d char %d" + p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol) + +let rec pp_l l = match l with + | Unknown -> "no location information available" + | Generated l -> Printf.sprintf "Generated: %s" (pp_l l) + | Range(p1,p2) -> Printf.sprintf "Range: %s to %s" (pp_lexing_position p1) (pp_lexing_position p2) + | Int(s,lo) -> Printf.sprintf "Int: %s %s" s (match lo with Some l -> pp_l l | None -> "none") + + +type +term_aux := + T_app of term * term + | T_foo of term + | T_var of var + | T_paren of term + | T_lambda of var * term + +and term := + T_aux of term_aux * l + + + diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_lexer.mll b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_lexer.mll new file mode 100644 index 0000000..5208b7f --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_lexer.mll @@ -0,0 +1,35 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) +{ +open Test10menhir_with_aux_parser +exception Error of string +} + +rule token = parse +| [' ' '\t'] + { token lexbuf } +| ' +' + { Lexing.new_line lexbuf; token lexbuf } +| "//" [^'\n']* '\n' + { Lexing.new_line lexbuf; token lexbuf } +| eof + { EOF } +| "\\" + { BACKSLASH } +| "(" + { LPAREN } +| ")" + { RPAREN } +| "." + { DOT } +| "Foo" + { FOO } +| ['a'-'z''A'-'Z']+ as var + { VAR ( var) } +| _ + { raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) } + + +{ +} + diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_parser.mly b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_parser.mly new file mode 100644 index 0000000..1e9ea5a --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_parser.mly @@ -0,0 +1,58 @@ +/* generated by Ott 0.34 from: test10menhir_with_aux.ott */ +%{ +open Test10menhir_with_aux_ast +%} + +%token BACKSLASH (* BACKSLASH *) +%token LPAREN (* ( *) +%token RPAREN (* ) *) +%token DOT (* . *) +%token FOO (* Foo *) +%token VAR (* metavarroot var *) +%token EOF (* added by Ott *) + +%start term_start + + +%% + +term_start: +| term = term EOF + { term } + +l: +| (* :: Unknown *) + { (*Case 1*) Unknown } + +term: +| at = atomic_term (* at :: T_at *) + { (*Case 1*) at } +| lhs = lhs rhs_prime = rhs (* lhs rhs' :: T_app *) + { T_aux((*Case 2*) T_app(lhs,rhs_prime),Range($symbolstartpos,$endpos) ) } +| lambda = lambda (* lambda :: T_fn *) + { (*Case 1*) lambda } +| FOO term = term (* Foo term :: T_foo *) + { T_aux((*Case 2*) T_foo(term),Range($symbolstartpos,$endpos) ) } + +atomic_term: +| x = VAR (* x :: T_var *) + { T_aux((*Case 2*) T_var(x),Range($symbolstartpos,$endpos) ) } +| LPAREN t = term RPAREN (* ( t ) :: T_paren *) + { T_aux((*Case 2*) T_paren(t),Range($symbolstartpos,$endpos) ) } + +lhs: +| at = atomic_term (* at :: T_at_lhs *) + { (*Case 1*) at } +| lhs = lhs at_prime = atomic_term (* lhs at' :: T_app_lhs *) + { (*Case 1*) T_aux(T_app(lhs, at_prime), Range($symbolstartpos,$endpos)) } + +rhs: +| at = atomic_term (* at :: T_at_rhs *) + { (*Case 1*) at } +| lambda = lambda (* lambda :: T_fn_rhs *) + { (*Case 1*) lambda } + +lambda: +| BACKSLASH x = VAR DOT t = term (* \ x . t :: T_lambda *) + { T_aux((*Case 2*) T_lambda(x,t),Range($symbolstartpos,$endpos) ) } + diff --git a/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_parser_pp.ml b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_parser_pp.ml new file mode 100644 index 0000000..6d4200e --- /dev/null +++ b/tests/menhir_tests/test10menhir_with_aux_rules/test10menhir_with_aux_parser_pp.ml @@ -0,0 +1,27 @@ +(* generated by Ott 0.34 from: test10menhir_with_aux.ott *) +open PPrint +open Test10menhir_with_aux_ast + +let rec pp_raw_var x = string "\"" ^^ string x ^^ string "\"" + +and pp_raw_l l = pp_l l + +and pp_raw_term x = match x with +| T_aux(T_app(lhs,rhs_prime),ott_menhir_loc) -> string "[" ^^ string (pp_raw_l ott_menhir_loc) ^^ string "]" ^^ string "T_app" ^^ string "(" ^^ pp_raw_term lhs ^^ string "," ^^ pp_raw_term rhs_prime ^^ string ")" +| T_aux(T_foo(term),ott_menhir_loc) -> string "[" ^^ string (pp_raw_l ott_menhir_loc) ^^ string "]" ^^ string "T_foo" ^^ string "(" ^^ pp_raw_term term ^^ string ")" +| T_aux(T_var(x),ott_menhir_loc) -> string "[" ^^ string (pp_raw_l ott_menhir_loc) ^^ string "]" ^^ string "T_var" ^^ string "(" ^^ pp_raw_var x ^^ string ")" +| T_aux(T_paren(t),ott_menhir_loc) -> string "[" ^^ string (pp_raw_l ott_menhir_loc) ^^ string "]" ^^ string "T_paren" ^^ string "(" ^^ pp_raw_term t ^^ string ")" +| T_aux(T_lambda(x,t),ott_menhir_loc) -> string "[" ^^ string (pp_raw_l ott_menhir_loc) ^^ string "]" ^^ string "T_lambda" ^^ string "(" ^^ pp_raw_var x ^^ string "," ^^ pp_raw_term t ^^ string ")" + + +let rec pp_var x = string x ^^ string "" + +and pp_l l = pp_l l + +and pp_term x = match x with +| T_aux(T_app(lhs,rhs_prime),ott_menhir_loc) -> group(string "" ^^ pp_term lhs ^^ break 1 ^^ pp_term rhs_prime ^^ string "") +| T_aux(T_foo(term),ott_menhir_loc) -> group(string "" ^^ string "Foo" ^^ break 1 ^^ nest 2 (pp_term term) ^^ string "") +| T_aux(T_var(x),ott_menhir_loc) -> pp_var x +| T_aux(T_paren(t),ott_menhir_loc) -> group(string "" ^^ string "(" ^^ break 1 ^^ nest 2 (pp_term t) ^^ break 1 ^^ string ")" ^^ string "") +| T_aux(T_lambda(x,t),ott_menhir_loc) -> group(string "" ^^ string "\\" ^^ break 1 ^^ pp_var x ^^ break 1 ^^ string "." ^^ break 1 ^^ nest 2 (pp_term t) ^^ string "") + diff --git a/tests/test10st.ott b/tests/test10st.ott index 62216fd..b9cc2a6 100644 --- a/tests/test10st.ott +++ b/tests/test10st.ott @@ -1,39 +1,41 @@ metavar termvar, x ::= - {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lem string }} {{ ocaml int }} + {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lem string }} {{ ocaml int }} {{ lean String }} {{ tex \mathit{[[termvar]]} }} {{ com term variable }} metavar typvar, X ::= - {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lem string }} {{ ocaml int }} + {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lem string }} {{ ocaml int }} {{ lean String }} {{ tex \mathit{[[typvar]]} }} {{ com type variable }} grammar - t :: 't_' ::= {{ com term }} + t {{ lean-type Term }} :: 't_' ::= {{ com term }} | x :: :: Var {{ com variable }} | \ x . t :: :: Lam (+ bind x in t +) {{ com abstraction }} | t t' :: :: App {{ com application }} - | ( t ) :: S :: paren {{ ichl [[t]] }} {{ ocaml int }} - | { t / x } t' :: M :: tsub {{ ichl ( tsubst_t [[t]] [[x]] [[t']] ) }} {{ ocaml int }} + | ( t ) :: S :: paren {{ ichlL [[t]] }} {{ ocaml int }} + | { t / x } t' :: M :: tsub {{ ichlL ( tsubst_t [[t]] [[x]] [[t']] ) }} {{ ocaml int }} v :: 'v_' ::= {{ com value }} | \ x . t :: :: Lam {{ com abstraction }} - T :: T_ ::= {{ com type }} + T {{ lean-type Typ }} :: T_ ::= {{ com type }} | X :: :: var {{ com variable }} | T -> T' :: :: arrow {{ com function }} - | ( T ) :: S :: paren {{ ichl [[T]] }} {{ ocaml int }} + | ( T ) :: S :: paren {{ ichlL [[T]] }} {{ ocaml int }} - G {{ tex \Gamma }} :: G_ ::= {{ isa (termvar*T) list }} {{ coq list (termvar*T) }} {{ ocaml (termvar*T) list }} {{ lem list (termvar*T) }} + G {{ tex \Gamma }} :: G_ ::= {{ isa (termvar*T) list }} {{ coq list (termvar*T) }} {{ ocaml (termvar*T) list }} {{ lem list (termvar*T) }} {{ lean List (termvar×Typ) }} {{ hol (termvar#T) list }} {{ com type environment }} | empty :: :: em {{ isa Nil }} {{ coq G_nil }} {{ hol [] }} {{ lem [] }} + {{ lean [] }} | G , x : T :: :: vn {{ isa ([[x]],[[T]])#[[G]] }} {{ coq (cons ([[x]],[[T]]) [[G]]) }} {{ hol (([[x]],[[T]])::[[G]]) }} {{ lem (([[x]],[[T]])::[[G]]) }} + {{ lean (([[x]],[[T]])::[[G]]) }} terminals :: 'terminals_' ::= | \ :: :: lambda {{ tex \lambda }} @@ -49,12 +51,14 @@ grammar {{ coq (not [[formula]]) }} {{ hol (~[[formula]]) }} {{ lem (not [[formula]]) }} + {{ lean (not [[formula]]) }} | x = x' :: :: eqv - {{ ichl [[x]]=[[x']] }} + {{ ichlL [[x]]=[[x']] }} | x : T in G :: :: xTG {{ isa ? G1 G2. [[G]] = G1 @ ([[x]],[[T]])#[[G2]] & [[x]]~:fst ` set G1 }} {{ coq (bound [[x]] [[T]] [[G]]) }} {{ lem (bound [[x]] [[T]] [[G]]) }} + {{ lean (bound [[x]] [[T]] [[G]]) }} {{ hol ? G1 G2. ([[G]] = G1 ++ ([[x]],[[T]])::[[G2]]) /\ ~(MEM [[x]] (MAP FST G1)) }} embed @@ -72,6 +76,12 @@ let rec bound x t0 g = | [] -> false end }} +{{ lean +def bound (x:termvar) (t0:Typ) (g:G) := + match g with + | (x',t')::g' => if x=x' then t0=t' else bound x t0 g' + | [] => false +}} subrules v <:: t diff --git a/tests/test10st.v b/tests/test10st.v new file mode 100644 index 0000000..0b1c262 --- /dev/null +++ b/tests/test10st.v @@ -0,0 +1,111 @@ +(* generated by Ott 0.34 from: test10st.ott *) + +Require Import Arith. +Require Import Bool. +Require Import List. +Require Import Ott.ott_list_core. + + +Definition termvar : Set := nat. (* term variable *) +Lemma eq_termvar: forall (x y : termvar), {x = y} + {x <> y}. +Proof. + decide equality; auto with ott_coq_equality arith. +Defined. +#[export] Hint Resolve eq_termvar : ott_coq_equality. +Definition typvar : Set := nat. (* type variable *) +Lemma eq_typvar: forall (x y : typvar), {x = y} + {x <> y}. +Proof. + decide equality; auto with ott_coq_equality arith. +Defined. +#[export] Hint Resolve eq_typvar : ott_coq_equality. + +Inductive T : Set := (* type *) + | T_var (X:typvar) (* variable *) + | T_arrow (T5:T) (T':T) (* function *). + +Inductive t : Set := (* term *) + | t_Var (x:termvar) (* variable *) + | t_Lam (x:termvar) (t5:t) (* abstraction *) + | t_App (t5:t) (t':t) (* application *). + +Definition G : Set := list (termvar*T). +Notation G_nil := (@nil (termvar*T)). +Definition bound x T0 G := + exists G1, exists G2, + (G = List.app G1 (List.cons (x,T0) G2)) /\ + ~In x (List.map (@fst termvar T) G1). + + +(** subrules *) +Definition is_v_of_t (t_6:t) : bool := + match t_6 with + | (t_Var x) => false + | (t_Lam x t5) => (true) + | (t_App t5 t') => false +end. + +(** library functions *) +Fixpoint list_mem A (eq:forall a b:A,{a=b}+{a<>b}) (x:A) (l:list A) {struct l} : bool := + match l with + | nil => false + | cons h t => if eq h x then true else list_mem A eq x t +end. +Arguments list_mem [A] _ _ _. + +Fixpoint list_minus A (eq:forall a b:A,{a=b}+{a<>b}) (l1:list A) (l2:list A) {struct l1} : list A := + match l1 with + | nil => nil + | cons h t => if (list_mem (A:=A) eq h l2) then list_minus A eq t l2 else cons h (list_minus A eq t l2) +end. +Arguments list_minus [A] _ _ _. + + +(** free variables *) +Fixpoint fv_t (t_6:t) : list termvar := + match t_6 with + | (t_Var x) => (cons x nil) + | (t_Lam x t5) => ((list_minus eq_termvar (fv_t t5) (cons x nil))) + | (t_App t5 t') => (app (fv_t t5) (fv_t t')) +end. + + +(** substitutions *) +Fixpoint tsubst_t (t_6:t) (x5:termvar) (t__7:t) {struct t__7} : t := + match t__7 with + | (t_Var x) => (if eq_termvar x x5 then t_6 else (t_Var x)) + | (t_Lam x t5) => t_Lam x (if list_mem eq_termvar x5 (cons x nil) then t5 else (tsubst_t t_6 x5 t5)) + | (t_App t5 t') => t_App (tsubst_t t_6 x5 t5) (tsubst_t t_6 x5 t') +end. + +(* definitions *) + +(* defns Jtype *) +Inductive GtT : G -> t -> T -> Prop := (* defn GtT *) + | GtT_value_name : forall (G5:G) (x:termvar) (T5:T), + (bound x T5 G5 ) -> + GtT G5 (t_Var x) T5 + | GtT_apply : forall (G5:G) (t5 t':t) (T2 T1:T), + GtT G5 t5 (T_arrow T1 T2) -> + GtT G5 t' T1 -> + GtT G5 (t_App t5 t') T2 + | GtT_lambda : forall (G5:G) (x1:termvar) (t5:t) (T1 T_5:T), + GtT (cons ( x1 , T1 ) G5 ) t5 T_5 -> + GtT G5 (t_Lam x1 t5) (T_arrow T1 T_5). +(* definitions *) + +(* defns Jop *) +Inductive reduce : t -> t -> Prop := (* defn reduce *) + | ax_app : forall (x:termvar) (t12 v2:t), + Is_true (is_v_of_t v2) -> + reduce (t_App (t_Lam x t12) v2) ( tsubst_t v2 x t12 ) + | ctx_app_fun : forall (t1 t_5 t1':t), + reduce t1 t1' -> + reduce (t_App t1 t_5) (t_App t1' t_5) + | ctx_app_arg : forall (v5 t1 t1':t), + Is_true (is_v_of_t v5) -> + reduce t1 t1' -> + reduce (t_App v5 t1) (t_App v5 t1'). +Hint Constructors reduce GtT : rules. + + + diff --git a/tests/test7.ott b/tests/test7.ott index b8e6061..2bac4b6 100644 --- a/tests/test7.ott +++ b/tests/test7.ott @@ -11,29 +11,30 @@ ideally also: can be replaced by a single one. << metavar typevar, X ::= - {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lem string }} {{ lex Alphanum }} + {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lem string }} {{ lean String }} {{ lex Alphanum }} {{ tex \mathit{[[typevar]]} }} {{ com type variable }} - {{ isavar ''[[typevar]]'' }} {{ holvar "[[typevar]]" }} {{ lemvar "[[typevar]]" }} {{ texvar \mathrm{[[typevar]]} }} + {{ isavar ''[[typevar]]'' }} {{ holvar "[[typevar]]" }} {{ lemvar "[[typevar]]" }} {{ leanvar "[[typevar]]" }} {{ texvar \mathrm{[[typevar]]} }} {{ ocamlvar "[[typevar]]" }} metavar termvar, x ::= - {{ isa string }} {{ coq nat }} {{ hol string }} {{ lem string }} {{ coq-equality }} {{ lex alphanum }} + {{ isa string }} {{ coq nat }} {{ hol string }} {{ lem string }} {{ lean String }} {{ coq-equality }} {{ lex alphanum }} {{ tex \mathit{[[termvar]]} }} {{ com term variable }} {{ isavar ''[[termvar]]'' }} {{ holvar "[[termvar]]" }} {{ lemvar "[[typevar]]" }} + {{ leanvar "[[typevar]]" }} {{ texvar \mathrm{[[termvar]]} }} {{ ocamlvar "[[termvar]]" }} rmetavar label, l, k ::= -r {{ isa string }} {{ coq nat }} {{ hol string }} {{ lem string }} {{ lex alphanum }} {{ tex \mathit{[[label]]} }} -r {{ com field label }} {{ isavar ''[[label]]'' }} {{ holvar "[[label]]" }} {{ lemvar "[[typevar]]" }} +r {{ isa string }} {{ coq nat }} {{ hol string }} {{ lem string }} {{ lean String }} {{ lex alphanum }} {{ tex \mathit{[[label]]} }} +r {{ com field label }} {{ isavar ''[[label]]'' }} {{ holvar "[[label]]" }} {{ lemvar "[[typevar]]" }} {{ leanvar "[[typevar]]" }} r {{ ocamlvar "[[label]]" }} -indexvar index, i, j, n, m ::= {{ isa nat }} {{ coq nat }} {{ hol num }} {{ lem num}} {{ lex numeral }} +indexvar index, i, j, n, m ::= {{ isa nat }} {{ coq nat }} {{ hol num }} {{ lem num}} {{ lean Nat}} {{ lex numeral }} {{ com indices }} grammar -T {{ hol Typ }}, S, U :: 'Ty_' ::= {{ com type }} +T {{ hol Typ }} {{ lean-type Typ }}, S, U :: 'Ty_' ::= {{ com type }} | X :: :: Var {{ com type variable }} | Top :: :: Top {{ com maximum type }} | T -> T' :: :: Fun {{ com type of functions }} @@ -43,8 +44,8 @@ r | { l1 : T1 , .. , ln : Tn } :: :: Rec {{ com record }} %R | { } :: :: Rec_empty {{ com empty record }} %R | { Trb } :: :: Rec_ne {{ com nonempty record }} % {{ com record type }} - | ( T ) :: S :: paren {{ ichl [[T]] }} - | [ X |-> T ] T' :: M :: sub {{ ichl (Tsubst_T [[T]] [[X]] [[T']]) }} + | ( T ) :: S :: paren {{ ichlL [[T]] }} + | [ X |-> T ] T' :: M :: sub {{ ichlL (Tsubst_T [[T]] [[X]] [[T']]) }} %R Trb :: 'Trb_' ::= %R | l : T :: :: rb1 @@ -61,11 +62,11 @@ t :: 't_' ::= {{ com term r | { l1 = t1 , .. , ln = tn } :: :: Rec {{ com record }} r | t . l :: :: Proj {{ com projection }} r | let p = t in t' :: :: Let (+ bind b(p) in t' +){{ com pattern binding}} - | ( t ) :: S :: paren {{ ichl [[t]] }} - | [ x |-> t ] t' :: M :: tsub {{ ichl ( tsubst_t [[t]] [[x]] [[t']] ) }} - | [ X |-> T ] t :: M :: Tsub {{ ichl ( Tsubst_t [[T]] [[X]] [[t]] ) }} + | ( t ) :: S :: paren {{ ichlL [[t]] }} + | [ x |-> t ] t' :: M :: tsub {{ ichlL ( tsubst_t [[t]] [[x]] [[t']] ) }} + | [ X |-> T ] t :: M :: Tsub {{ ichlL ( Tsubst_t [[T]] [[X]] [[t]] ) }} % | E [ t ] :: M :: ctx -r | s t :: M :: tsubs {{ ichl ( m_t_subst_t [[s]] [[t]] ) }} +r | s t :: M :: tsubs {{ ichlL ( m_t_subst_t [[s]] [[t]] ) }} r p :: 'P_' ::= {{ com pattern }} r | x : T :: :: Var (+ b = x +) {{ com variable pattern }} @@ -90,12 +91,12 @@ G {{ tex \Gamma }}, D {{ tex \Delta }} :: 'G_' ::= {{ com type environment }} | empty :: :: empty | G , X <: T :: :: type | G , x : T :: :: term -%r | G , G' :: M :: comma {{ ichl TODO }} -r | G1 , .. , Gn :: M :: dots {{ ichl (flatten_G [[G1..Gn]]) }} +%r | G , G' :: M :: comma {{ ichlL TODO }} +r | G1 , .. , Gn :: M :: dots {{ ichlL (flatten_G [[G1..Gn]]) }} -rs {{ tex \sigma }} :: 'S_' ::= {{ com multiple term substitution }} {{ isa (termvar*t) list }} {{ hol (termvar#t) list }} {{ coq list (termvar*t) }} {{ lem list (termvar*t) }} -r | [ x |-> t ] :: :: singleton {{ ih [ ([[x]],[[t]]) ] }} {{ coq (cons ([[x]],[[t]]) nil) }} {{ lem [ ([[x]],[[t]]) ] }} -r | s1 , ... , sn :: :: list {{ isa List.concat [[s1...sn]] }} {{ hol (FLAT [[s1...sn]]) }} {{ coq (List.flat_map (fun x => x) [[s1...sn]]) }} {{ lem (List.flatten [[s1...sn]]) }} +rs {{ tex \sigma }} :: 'S_' ::= {{ com multiple term substitution }} {{ isa (termvar*t) list }} {{ hol (termvar#t) list }} {{ coq list (termvar*t) }} {{ lem list (termvar*t) }} {{ lean List (termvar×t) }} +r | [ x |-> t ] :: :: singleton {{ ih [ ([[x]],[[t]]) ] }} {{ coq (cons ([[x]],[[t]]) nil) }} {{ lem [ ([[x]],[[t]]) ] }} {{ lean [ ([[x]],[[t]]) ] }} +r | s1 , ... , sn :: :: list {{ isa List.concat [[s1...sn]] }} {{ hol (FLAT [[s1...sn]]) }} {{ coq (List.flat_map (fun x => x) [[s1...sn]]) }} {{ lem (List.flatten [[s1...sn]]) }} {{ lean (List.flatten [[s1...sn]]) }} terminals :: terminals_ ::= | \ :: :: lambda {{ tex \lambda }} @@ -113,13 +114,14 @@ r | \/ :: :: vee {{ tex \vee }} formula :: formula_ ::= | judgement :: :: judgement -% | G = G' :: :: Geq {{ ichl [[G]] = [[G']] }} - | x = x' :: :: xeq {{ ichl [[x]] = [[x']] }} - | X = X' :: :: Xeq {{ ichl [[X]] = [[X']] }} - | ( formula ) :: :: paren {{ ichl ( [[formula]] ) }} +% | G = G' :: :: Geq {{ ichlL [[G]] = [[G']] }} + | x = x' :: :: xeq {{ ichlL [[x]] = [[x']] }} + | X = X' :: :: Xeq {{ ichlL [[X]] = [[X']] }} + | ( formula ) :: :: paren {{ ichlL ( [[formula]] ) }} | not formula :: :: not {{ isa Not( [[formula]] ) }} {{ coq not( [[formula]] ) }} {{ lem not( [[formula]] ) }} + {{ lean not( [[formula]] ) }} {{ hol ~( [[formula]] ) }} {{ tex \neg [[ formula]] }} % | x isin dom ( G ) :: :: xin {{ isa ? T. ([[x]],T,[[G]]):tin }} @@ -132,6 +134,7 @@ r {{ isa ![[i]] . ((1::nat)<=[[i]] & [[i]]<=[[m]]) r {{ hol ![[i]] . (1<=[[i]] /\ [[i]]<=[[m]]) ==> [[formula]] }} r {{ coq (forall [[i]], (1<=[[i]] /\ [[i]] <= m) -> [[formula]]) }} r {{ lem (forall [[i]]. (1<=[[i]] && [[i]] <= m) --> [[formula]]) }} +r {{ lean (forall [[i]]. (1<=[[i]] && [[i]] <= m) --> [[formula]]) }} r | exists i isin 1 -- m . formula :: :: exists r {{ tex \exists [[i]] \in 1 .. [[m]]. [[formula]] }} @@ -139,13 +142,15 @@ r {{ isa ?[[i]]. ((1::nat)<=[[i]] & i<=[[m]]) ==> r {{ hol ?[[i]] . (1<=[[i]] /\ [[i]]<=[[m]]) ==> [[formula]] }} r {{ coq exists [[i]], (1<=[[i]] /\ [[i]] <= [[m]]) -> [[formula]] }} r {{ lem (exists [[i]]. (1<=[[i]] && [[i]] <= m) && [[formula]]) }} +r {{ lean (exists [[i]]. (1<=[[i]] && [[i]] <= m) && [[formula]]) }} r | formula /\ formula' :: :: and {{ isa ([[formula]] & [[formula']]) }} r {{ hol ([[formula]] /\ [[formula']]) }} r {{ coq ([[formula]] /\ [[formula']]) }} r {{ lem ([[formula]] && [[formula']]) }} +r {{ lean ([[formula]] && [[formula']]) }} -r | l = l' :: :: leq {{ ichl ([[l]]=[[l']]) }} +r | l = l' :: :: leq {{ ichlL ([[l]]=[[l']]) }} % would be nice to write the above as {{ isa ?[[T]]. [[X<:T isin G]] }} @@ -217,6 +222,17 @@ r let rec flatten_G [] = [[empty]] r and flatten_G ([[G]]::Gs) = append_G [[G]] (flatten_G Gs) r }} r +r {{ lean +r (** embedded definitions of operations on type environments **) +r val append_G : G -> G -> G +r let rec append_G [[G]] [[empty]] = [[G]] +r and append_G [[G]] [[G',X<:T]] = (let [[G'']] = append_G [[G]] [[G']] in [[G'',X<:T]]) +r and append_G [[G]] [[G',x:T]] = (let [[G'']] = append_G [[G]] [[G']] in [[G'',x:T]]) +r val flatten_G : List G -> G +r let rec flatten_G [] = [[empty]] +r and flatten_G ([[G]]::Gs) = append_G [[G]] (flatten_G Gs) +r }} +r defns Judgement_in :: '' ::= diff --git a/tests/test_lists_1.ott b/tests/test_lists_1.ott index c375358..8f8b1cd 100644 --- a/tests/test_lists_1.ott +++ b/tests/test_lists_1.ott @@ -1,23 +1,25 @@ %% Some examples of usage of lists %% (trying to gather the interesting cases from minicaml) -indexvar i, j, k, l, m, n ::= -metavar x ::= +indexvar i, j, k, l, m, n ::= {{ lean natish }} +metavar x ::= {{ lean natish }} grammar t, term :: t_ ::= | x :: :: x | letrec lb1 and ... and lbn in t :: :: letrec + lb, letrec_binding :: lb_ ::= | x = t :: :: simple b, binding :: b_ ::= | x :: :: x + E, environment :: E_ ::= | b1 , .. , bn :: :: concrete - | nil :: M :: nil {{ ich wibble }} - | E1 , .... , En :: M :: concat {{ ich wibble }} + | nil :: M :: nil {{ ich wibble }} {{ lean wibble }} + | E1 , .... , En :: M :: concat {{ ich wibble }} {{ lean wobble }} defns Typing :: Typing_ ::= diff --git a/tests/test_lists_defn_list_form_1.ott b/tests/test_lists_defn_list_form_1.ott index a072c79..928c6b8 100644 --- a/tests/test_lists_defn_list_form_1.ott +++ b/tests/test_lists_defn_list_form_1.ott @@ -1,7 +1,7 @@ %% Test of a defn production containing a list form -indexvar i, j, k, l, m, n ::= {{ coq nat }} -metavar x ::= {{ coq nat }} +indexvar i, j, k, l, m, n ::= {{ coq nat }} {{ lean natish }} +metavar x ::= {{ coq nat }} {{ lean natish }} grammar e :: e_ ::= | ( x1 , .. , xn ) :: :: tuple