TD6 : solution for exercise 5 (extraction + lexer + parser)

solutions/td6.v

@@ -34,7 +34,7 @@ Definition stack := list nat.
 
 (* Exercise 3 *)
 
-Fixpoint exec_inst (i:inst) (stk:stack) : stack :=
+Definition exec_inst (i:inst) (stk:stack) : stack :=
  match i with
  | PUSH n => n::stk
  | ADD => match stk with
@@ -131,3 +131,9 @@ Lemma compile_okbis :
 Proof.
  intros. apply compile_ok.
 Qed.
+
+(* Exercise 5 : extraction *)
+
+Require Extraction.
+
+Extraction "td6/expr.ml" eval exec_prog compile.

solutions/td6/Makefile

+all:
+	dune build @all
+
+run:
+	dune exec ./calc.exe
+
+clean:
+	dune clean

solutions/td6/README.md

+TD6 : Little lexer/parser of arithmetical expressions
+=====================================================
+
+- `expr.ml` and `expr.mli` are obtained from `../td6.v` by extraction
+- to compile, install `ocaml`, `dune` and `menhir` then do `make`
+- to run : `make run`
+
+Example of session:
+
+```sh
+$ make run
+dune exec ./calc.exe
+expr? 3*5+7        
+eval: 22 compiled: 22 
+```

solutions/td6/calc.ml

+open Expr
+
+let rec n2i = function O -> 0 | S n -> 1+n2i n
+
+let process linebuf =
+  Format.printf "expr? %!";
+  try
+    let e = Parser.main Lexer.token linebuf in
+    let n = Expr.eval e in
+    let n' =
+      match Expr.exec_prog (Expr.compile e) Nil with
+      | Cons (n,_) -> n
+      | Nil -> failwith "empty stack"
+    in
+    Printf.printf "eval: %d compiled: %d \n%!" (n2i n) (n2i n')
+  with
+  | Failure msg ->
+      Printf.fprintf stderr "%s%!" msg
+  | Parser.Error ->
+      Printf.fprintf stderr "At offset %d: syntax error.\n%!" (Lexing.lexeme_start linebuf)
+
+let () =
+  process (Lexing.from_channel stdin)
+

solutions/td6/dune

+(ocamllex (modules lexer))
+
+(menhir (modules parser))
+
+(executable (name calc))

solutions/td6/dune-project

+(lang dune 1.6)
+(using menhir 2.0)

solutions/td6/expr.ml

+
+type nat =
+| O
+| S of nat
+
+type 'a list =
+| Nil
+| Cons of 'a * 'a list
+
+(** val app : 'a1 list -> 'a1 list -> 'a1 list **)
+
+let rec app l m =
+  match l with
+  | Nil -> m
+  | Cons (a, l1) -> Cons (a, (app l1 m))
+
+(** val add : nat -> nat -> nat **)
+
+let rec add n m =
+  match n with
+  | O -> m
+  | S p -> S (add p m)
+
+(** val mul : nat -> nat -> nat **)
+
+let rec mul n m =
+  match n with
+  | O -> O
+  | S p -> add m (mul p m)
+
+type expr =
+| Num of nat
+| Plus of expr * expr
+| Mult of expr * expr
+
+(** val eval : expr -> nat **)
+
+let rec eval = function
+| Num n -> n
+| Plus (e0, e') -> add (eval e0) (eval e')
+| Mult (e0, e') -> mul (eval e0) (eval e')
+
+type inst =
+| PUSH of nat
+| ADD
+| MUL
+
+type prog = inst list
+
+type stack = nat list
+
+(** val exec_inst : inst -> stack -> stack **)
+
+let exec_inst i stk =
+  match i with
+  | PUSH n -> Cons (n, stk)
+  | ADD ->
+    (match stk with
+     | Nil -> Nil
+     | Cons (e1, l) ->
+       (match l with
+        | Nil -> Nil
+        | Cons (e2, stk') -> Cons ((add e1 e2), stk')))
+  | MUL ->
+    (match stk with
+     | Nil -> Nil
+     | Cons (e1, l) ->
+       (match l with
+        | Nil -> Nil
+        | Cons (e2, stk') -> Cons ((mul e1 e2), stk')))
+
+(** val exec_prog : prog -> stack -> stack **)
+
+let rec exec_prog p stk =
+  match p with
+  | Nil -> stk
+  | Cons (i, p') -> let stk' = exec_inst i stk in exec_prog p' stk'
+
+(** val compile : expr -> prog **)
+
+let rec compile = function
+| Num n -> Cons ((PUSH n), Nil)
+| Plus (e0, e') -> app (compile e0) (app (compile e') (Cons (ADD, Nil)))
+| Mult (e0, e') -> app (compile e0) (app (compile e') (Cons (MUL, Nil)))

solutions/td6/expr.mli

+
+type nat =
+| O
+| S of nat
+
+type 'a list =
+| Nil
+| Cons of 'a * 'a list
+
+val app : 'a1 list -> 'a1 list -> 'a1 list
+
+val add : nat -> nat -> nat
+
+val mul : nat -> nat -> nat
+
+type expr =
+| Num of nat
+| Plus of expr * expr
+| Mult of expr * expr
+
+val eval : expr -> nat
+
+type inst =
+| PUSH of nat
+| ADD
+| MUL
+
+type prog = inst list
+
+type stack = nat list
+
+val exec_inst : inst -> stack -> stack
+
+val exec_prog : prog -> stack -> stack
+
+val compile : expr -> prog

solutions/td6/lexer.mll

+{
+  open Parser
+}
+
+rule token = parse
+| [' ' '\t']
+    { token lexbuf }
+| ['0'-'9']+ as i
+    { INT (int_of_string i) }
+| '+'
+    { PLUS }
+| '*'
+    { TIMES }
+| '('
+    { LPAREN }
+| ')'
+    { RPAREN }
+| '\n'
+    { EOL }
+| eof
+    { EOL }
+| _
+    { failwith (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf)) }
+

solutions/td6/parser.mly

+%{
+open Expr
+
+let rec i2n = function 0 -> O | n -> S (i2n (n-1))
+%}
+
+%token <int> INT
+%token PLUS TIMES
+%token LPAREN RPAREN
+%token EOL
+
+%left PLUS        /* lowest precedence */
+%left TIMES       /* medium precedence */
+
+%start <Expr.expr> main
+
+%%
+
+main:
+| e = expr EOL
+    { e }
+
+expr:
+| i = INT
+    { Num (i2n i) }
+| LPAREN e = expr RPAREN
+    { e }
+| e1 = expr PLUS e2 = expr
+    { Plus (e1,e2) }
+| e1 = expr TIMES e2 = expr
+    { Mult (e1,e2) }
+