Lean experiment

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

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{}}

examples/1Bsemantics/.l1.aux

@@ -0,0 +1 @@
+COQAUX1 4a24abe13b920db9d4882fac2ca00359 /home/pes20/repos/ott/examples/1Bsemantics/l1.v

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

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