second example

semantics/Makefile

@@ -95,6 +95,7 @@ endif
 ######################
 
 VFILES:=example.v\
+  example2.v\
   program.v\
   tactics.v\
   types.v

semantics/_CoqProject

 -R . SPLSemantics
 example.v
+example2.v
 program.v
 tactics.v
 types.v

semantics/example2.v

+Require Import List ZArith String.
+Require Import program types tactics.
+Import List.ListNotations.
+Local Open Scope Z_scope.
+Local Open Scope string_scope.
+
+(* // This is ex-should-work/compile-example4.spl
+ * [Int] l = [];
+ *
+ * mult(n) :: Int -> Int {
+ *     Int i = 0;
+ *     Int x = 1;
+ *     while (i < n) {
+ *         x = x * l.hd;
+ *         l = l.tl;
+ *          i = i + 1;
+ *     }
+ *     return x;
+ * }
+ *
+ * seq(n) :: Int -> [Int] {
+ *     Int i = 2;
+ *     l = 1 : [];
+ *     while (i <= n) {
+ *         l = i : l;
+ *         i = i + 1;
+ *     }
+ *     return l;
+ * }
+ *
+ * fac(n) :: Int -> Int {
+ *     Int n2 = n;
+ *     if (n2 < 2) {
+ *         n2 = 1;
+ *     }
+ *     seq(n2);
+ *     return mult(n2);
+ * }
+ *
+ * main() :: -> Void {
+ *     fac(6);
+ * } *)
+
+
+Definition var_l := ENil.
+Definition type_var_l := (TList TInt).
+Definition fun_mult := (SVal "i" (ENum 0) (SVal "x" (ENum 1) (SSeq (SWhile (EBinOp LT (EFieldSel (FVar "i")) (EFieldSel (FVar "n"))) (SSeq (SAssign (FVar "x") (EBinOp Mul (EFieldSel (FVar "x")) (EFieldSel (FHd (FVar "l"))))) (SSeq (SAssign (FVar "l") (EFieldSel (FTl (FVar "l")))) (SSeq (SAssign (FVar "i") (EBinOp Add (EFieldSel (FVar "i")) (ENum 1))) SSkip)))) (SSeq (SReturn (Some (EFieldSel (FVar "x")))) SSkip)))).
+Definition type_fun_mult := (TFun [TInt] TInt).
+Definition fun_seq := (SVal "i" (ENum 2) (SSeq (SAssign (FVar "l") (EBinOp Cons (ENum 1) ENil)) (SSeq (SWhile (EBinOp LEq (EFieldSel (FVar "i")) (EFieldSel (FVar "n"))) (SSeq (SAssign (FVar "l") (EBinOp Cons (EFieldSel (FVar "i")) (EFieldSel (FVar "l")))) (SSeq (SAssign (FVar "i") (EBinOp Add (EFieldSel (FVar "i")) (ENum 1))) SSkip))) (SSeq (SReturn (Some (EFieldSel (FVar "l")))) SSkip)))).
+Definition type_fun_seq := (TFun [TInt] (TList TInt)).
+Definition fun_fac := (SVal "n2" (EFieldSel (FVar "n")) (SSeq (SIf (EBinOp LT (EFieldSel (FVar "n2")) (ENum 2)) (SSeq (SAssign (FVar "n2") (ENum 1)) SSkip) SSkip) (SSeq (SFunCall "seq" [(EFieldSel (FVar "n2"))]) (SSeq (SReturn (Some (EFunCall "mult" [(EFieldSel (FVar "n2"))]))) SSkip)))).
+Definition type_fun_fac := (TFun [TInt] TInt).
+Definition fun_main := (SSeq (SFunCall "fac" [(ENum 6)]) SSkip).
+Definition type_fun_main := (TFun [] TVoid).
+Definition the_program := (PVal "l" var_l (PFun "mult" ["n"] fun_mult (PFun "seq" ["n"] fun_seq (PFun "fac" ["n"] fun_fac (PFun "main" [] fun_main PEnd))))).
+
+Theorem program_typed : prog_type empty_env the_program.
+Proof.
+  solve_var type_var_l.
+  solve_fun type_fun_mult.
+    solve_stmt_val TInt.
+    solve_stmt_val TInt.
+    solve_assign TInt.
+    solve_assign (TList TInt).
+    solve_assign TInt.
+    solve_binop_explicit TInt TInt.
+  solve_fun type_fun_seq.
+    solve_stmt_val TInt.
+    solve_assign (TList TInt).
+    solve_assign (TList TInt).
+    solve_assign TInt.
+    solve_binop_explicit TInt TInt.
+  solve_fun type_fun_fac.
+    solve_stmt_val TInt.
+    solve_assign TInt.
+    solve_simple_stmt_funcall [TInt] (TList TInt).
+    solve_simple_funcall [TInt].
+  solve_fun type_fun_main.
+    solve_simple_stmt_funcall [TInt] TInt.
+Qed.