Add type checker ("OCaml + printf" by Rodionov Maxim and Zaikin Vladi…

…mir) (Kakadu#67)

* project initialization

Signed-off-by: Maxim Rodionov <[email protected]>

* chore: update .gitignore and .ocamlformat

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: add AST

Signed-off-by: Maxim Rodionov <[email protected]>

* chore: fix linter's comments and delete unnecessary file

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: add an example of representing a factorial using the written types

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: an example of representing a factorial check by compiler

Signed-off-by: Maxim Rodionov <[email protected]>

* test: add cram test for output

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: update AST and an example of representing a factorial

Removed types related to printf, corrected documentation, changed definition of Exp_fun and Exp_apply.

Signed-off-by: Maxim Rodionov <[email protected]>

* docs: add authors' emails

Signed-off-by: Friend-zva <[email protected]>

* refactor: rename 'REPL.ml' to 'main.ml'

Signed-off-by: Friend-zva <[email protected]>

* fix: unused depends

Signed-off-by: Friend-zva <[email protected]>

* feat: add 'parse_constant'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: add base 'parse_pattern', 'parse_expression' and 'parse_binding'

Signed-off-by: Vladimir Zaikin <[email protected]>

* docs: rename 'Str' -> 'Struct' and fix typos

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: add parsing of 'structure', 'structure_item' and refactor some functions
Added 'parse_structure', 'parse_struct_value', 'parse_value_binding_list', 'parse_ident' and renamed 'skip_many' to 'ws'.

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: expand 'parse_expression' and 'parse_pattern'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: add 'parse_expression'

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'chain_left_associative' and 'parse_exp_match'

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: some funs and args in parsing 'expression' and 'pattern'

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: react to zanuda warnings

Change execation parser.
Add 'expect_test' for parser to '/tests/test_parser.ml' and delete 'parser_binding.t'.
Add '.mli' for 'parser.ml' and 'test_parser.ml'.

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: 'parse_pattern', update 'parser.mli' and remove unimplemented functions

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: add parser tests

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: REPL

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: error handling

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: REPL

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: error handling

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: delete dir 'main', add test for parser via REPL

Signed-off-by: Maxim Rodionov <[email protected]>

* chore: remove stanza 'modules' in dune files, edit the test

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'factorial.ml' -> 'factorial.txt'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: missing spaces and types

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: 'parse_exp_let', 'ws1', rewrite 'parse_ident' and parse of tuple with let*

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: replace all liftn with let*

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'parse_expression' and some variable names

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: a test for 'Exp_let'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: 'parse_exp_apply' and a test for it

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: 'parse_exp_apply_op'

Signed-off-by: Vladimir Zaikin <[email protected]>

* docs: add more info to 'README.md'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: 'parse_exp_construct', 'parse_pat_construct', some code refactor
Removed unnecessary code, added a function 'is_empty' due to linter comments.

Signed-off-by: Maxim Rodionov <[email protected]>

* test: for 'Exp_construct'

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'ws1' -> 'keyword' and some typos

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: 'parse_exp_sequence', 'parse_bool_exp', 'parse_bool_pat'

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: prevent backtracking for 'parse_structure'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: 'parse_chain_right_associative' and some typos

Signed-off-by: Maxim Rodionov <[email protected]>

* test: for 'parse_chain_right_associative' and for REPL

Signed-off-by: Maxim Rodionov <[email protected]>

* chore: correct the order of tests

Signed-off-by: Maxim Rodionov <[email protected]>

* test: small refactor

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: simplify some checks and concatenation

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: add 'parse_exp_fun' and a test for it

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: implement pretty-printer

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: pretty-print of 'Exp_apply'

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: implement draft of qcheck

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: fix linter comments and clean up code

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: rework ast generation

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: zanuda's warnings and 'keyword'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: parsing sequence and construct

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: zanuda comment

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: implement draft of shrink

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: shrink of value_binding and case

Signed-off-by: Vladimir Zaikin <[email protected]>

* test: small refactor

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: simplify some checks and concatenation

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: add 'parse_exp_fun' and a test for it

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: implement pretty-printer

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: pretty-print of 'Exp_apply'

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: implement draft of qcheck

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: fix linter comments and clean up code

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: rework ast generation

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: zanuda's warnings and 'keyword'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: parsing sequence and construct

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: zanuda comment

Signed-off-by: Maxim Rodionov <[email protected]>

* chore: formatting

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: library qcheck -> qcheck-core

Signed-off-by: Vladimir Zaikin <[email protected]>

* test: pretty printer

Signed-off-by: Vladimir Zaikin <[email protected]>

* test: 'QCheck_base_runner' and pretty printer's tests

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: add brackets to pretty printer to make the meaning of expressions clear

Signed-off-by: Maxim Rodionov <[email protected]>

* test: update expected result from tests

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: string shrinking

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: parsing, pretty-printing, test for 'option'

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'List.con' -> '::' and rename some vars

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: replace 'run_qchecker.ml'

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: replace 'String.concat' with 'pp_print_list'

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: placement of parentheses in arithmetic expressions in pretty printer

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: rework pretty print of 'Exp_apply', add operators to qcheck

Signed-off-by: Maxim Rodionov <[email protected]>

* test: add pprinter to parser tests

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: tuple signature

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: explicit type assignment

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: match signature

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'Struct_value' and 'Exp_let' signatures

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'Exp_apply' signature

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: shrinker

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: auto generator

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: move shrinker to a separate file

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'Type_tuple' signature

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: construct keyword parsing

Signed-off-by: Maxim Rodionov <[email protected]>

* revert: construct keyword parsing

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: auto generator -> ast

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: 'expression' -> 't'

Signed-off-by: Vladimir Zaikin <[email protected]>

* docs: update 'README.md'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: zanuda's warnings

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: typos and defect in the content of 'ident'

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: 'core_type'

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: add 'bin_op' in auto generator

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: parsing and generating 'ident'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: generating constructs

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: 'core_type' and some construct in manual generator

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: manual generator

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: gen 'Exp_fun' and some limits

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: formatting

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: pretty output

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: 'Exp_fun' signature

* refactor: pretty print of 'Type_arrow' and 'Type_tuple'

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: 'verbose' option in generator

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: zanuda's warnings

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: 'ppx_deriving_qcheck' in depends

Signed-off-by: Vladimir Zaikin <[email protected]>

* docs: typos in 'README.md'

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: 'run_qchecker': executable -> module of library 'tests'

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: reduce the code, make it more reusable

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: draft version of type inference

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: 'ty' -> 'core_type' and expand 'core_type'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: 'Type_unit' and 'Type_name'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: type inference of 'Exp_tuple', 'Pat_tuple' and tests

* feat: draft version of type inference

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: 'ty' -> 'core_type' and expand 'core_type'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: 'Type_unit' and 'Type_name'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: type inference of 'Exp_tuple', 'Pat_tuple' and tests

* feat: inference of 'Exp_fun', 'Exp_match', 'Exp_sequence', 'Exp_constraint', 'Pat_constraint'

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: parsing and generating 'Type_name'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: work with core_type, add 'Type_unit'

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: impl prec printer and rebuild 'Exp_apply'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: pretty printer and shrinker

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: rename module R to State, remove unnecessary functions helper

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: inference of 'Exp_construct', 'Pat_construct'

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: prec printer

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: inference of 'Exp_apply', 'Exp_ifthenelse' without else branch

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: almost full inference of 'Exp_let', 'Struct_value'

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: parse and inference of cons operator

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: 'parse_expression'

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: inference of lists, recursive 'Struct_value'

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: 'Type_option'

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'let' and 'let rec' inference

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: inferencer to REPL

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: Exp_function

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: parse_expression and generating 'Exp_let'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: inference of 'Exp_function', 'Exp_match'

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: pprinter and qcheck

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: clean 'inferencer.mli', improve variable names

Signed-off-by: Maxim Rodionov <[email protected]>

* feat: support for negative numbers

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: names of type variables

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: 'run_tests' -> 'run_tests_main' in qcheck

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: generator type

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: inference of recursive definition

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: explicit assignment of types

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: parsing value_binding and construct 'Some'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: generating value_binding

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: indent in pretty printer

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: 'manytests' for type check

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: remove requirement of parentheses after 'Some'

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: remove hanging tests

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: formatting 'manytests'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: symbolic link for 'manytests'

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: react to linter report

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: 'Impossible_error'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: clean qcheck

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: clean pretty printer

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: pretty printer 'core_type'

Signed-off-by: Vladimir Zaikin <[email protected]>

* docs: complement in AST

Signed-off-by: Vladimir Zaikin <[email protected]>

* refactor: rename variables and functions

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: 'parse_expression', expand search for 'Bound_several_times' error

Signed-off-by: Maxim Rodionov <[email protected]>

* docs: type 'error'

Signed-off-by: Maxim Rodionov <[email protected]>

* chore: remove unnecessary variable

Signed-off-by: Maxim Rodionov <[email protected]>

* refactor: 'parse_type_var', inference of 'Exp_apply'

Signed-off-by: Maxim Rodionov <[email protected]>

* fix: ' in 'Type_var' and 'parse_list_or_option_type'

Signed-off-by: Vladimir Zaikin <[email protected]>

* feat: shrinker 'core_type'

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: 'parse_expression' and clean parsing

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: 'parse_expression' and tests for it

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: react to linter report

Signed-off-by: Vladimir Zaikin <[email protected]>

* fix: printer infer result

Signed-off-by: Vladimir Zaikin <[email protected]>

* chore: react to linter report

Signed-off-by: Vladimir Zaikin <[email protected]>

* revert: remove 'Type_any'

Signed-off-by: Vladimir Zaikin <[email protected]>

---------

Signed-off-by: Maxim Rodionov <[email protected]>
Signed-off-by: Friend-zva <[email protected]>
Signed-off-by: Vladimir Zaikin <[email protected]>
Co-authored-by: Maxim Rodionov <[email protected]>

OCamlPrintf/README.md

@@ -30,7 +30,7 @@
   - [x] Manual
   - [x] Auto
 - [x] Shrinker
-- [ ] Type Checker
+- [x] Type Checker
 - [ ] Interpreter
 
 ## Build
@@ -43,7 +43,9 @@ dune build # Build the project.
 ## Run
 
 ```shell
-dune test # Run all tests.
+dune runtest # Run all tests.
+dune exec -- repl/REPL.exe -dparsetree -fromfile tests/factorial.txt # Run parser tests and see AST.
+dune exec -- tests/run_qchecker.exe -v # Run qchecker tests with verbose mode.
 ```
 
 ## Authors

OCamlPrintf/lib/ast.ml

@@ -4,11 +4,10 @@
 
 open QCheck.Gen
 
-let coef = 50 (* For the generator's speed. *)
+let coef = 10 (* For the generator's speed. *)
 let min_range = int_range 0 10 (* For the generator's speed. *)
 let gen_string gen = string_size min_range ~gen
 let gen_list gen = list_size min_range gen
-let gen_operand gen = list_size (int_range 1 1) gen
 
 type 'a list_ = ('a list[@gen gen_list gen_a])
 [@@deriving show { with_path = false }, qcheck]
@@ -18,6 +17,28 @@ let gen_char =
   oneof [ return '!'; char_range '#' '&'; char_range '(' '['; char_range ']' '~' ]
 ;;
 
+let un_op_list = [ "~-", 1 ]
+
+let bin_op_list =
+  [ "*", 1
+  ; "/", 1
+  ; "+", 2
+  ; "-", 2
+  ; ">=", 3
+  ; "<=", 3
+  ; "<>", 3
+  ; "=", 3
+  ; ">", 3
+  ; "<", 3
+  ; "&&", 4
+  ; "||", 5
+  ]
+;;
+
+let is_operator opr = List.exists (fun (str, _) -> str = opr) bin_op_list
+let is_negative_op opr = List.exists (fun (str, _) -> str = opr) un_op_list
+let get_priority opr = List.assoc opr bin_op_list
+
 let is_keyword = function
   | "and"
   | "else"
@@ -26,6 +47,7 @@ let is_keyword = function
   | "if"
   | "in"
   | "let"
+  | "function"
   | "match"
   | "rec"
   | "then"
@@ -37,10 +59,10 @@ let is_keyword = function
 ;;
 
 let gen_ident =
-  let gen_var =
+  let gen_id =
     map2
-      (fun start_ident rest_ident ->
-        match Base.Char.to_string start_ident ^ rest_ident with
+      (fun fst_char rest_str ->
+        match Base.Char.to_string fst_char ^ rest_str with
         | "_" -> "id"
         | id -> id)
       (oneof [ char_range 'a' 'z'; return '_' ])
@@ -53,7 +75,7 @@ let gen_ident =
             ; return '\''
             ]))
   in
-  gen_var >>= fun name -> if is_keyword name then gen_var else return name
+  gen_id >>= fun id -> if is_keyword id then gen_id else return id
 ;;
 
 type ident = (string[@gen gen_ident]) [@@deriving show { with_path = false }, qcheck]
@@ -69,12 +91,34 @@ type constant =
   | Const_string of (string[@gen gen_string gen_char])
 [@@deriving show { with_path = false }, qcheck]
 
+let gen_type_var =
+  let gen_type_var =
+    map3
+      (fun fst_char snd_char rest_str ->
+        Printf.sprintf "%c%c%s" fst_char snd_char rest_str)
+      (oneof [ char_range 'a' 'z' ])
+      (oneof [ char_range '0' '9'; char_range 'A' 'Z'; char_range 'a' 'z'; return '_' ])
+      (gen_string
+         (oneof
+            [ char_range '0' '9'
+            ; char_range 'A' 'Z'
+            ; char_range 'a' 'z'
+            ; return '_'
+            ; return '\''
+            ]))
+  in
+  gen_type_var
+  >>= fun type_var -> if is_keyword type_var then gen_type_var else return ("'" ^ type_var)
+;;
+
 type core_type =
-  | Type_any
+  | Type_unit
   | Type_char
   | Type_int
   | Type_string
   | Type_bool
+  | Type_option of (core_type[@gen gen_core_type_sized (n / coef)])
+  | Type_var of (ident[@gen gen_type_var])
   | Type_list of (core_type[@gen gen_core_type_sized (n / coef)])
   | Type_tuple of
       (core_type[@gen gen_core_type_sized (n / coef)])
@@ -85,6 +129,25 @@ type core_type =
       * (core_type[@gen gen_core_type_sized (n / coef)])
 [@@deriving show { with_path = false }, qcheck]
 
+let gen_construct gen n tuple construct =
+  oneof
+    [ return ("()", None)
+    ; return ("true", None)
+    ; return ("false", None)
+    ; return ("None", None)
+    ; map (fun i -> "Some", Some i) (gen (n / coef))
+    ; (let rec gen_list n =
+         if n = 0
+         then return ("[]", None)
+         else (
+           let element = gen 0 in
+           let tail = gen_list (n / coef) in
+           map2 (fun e t -> "::", Some (tuple (e, construct t, []))) element tail)
+       in
+       gen_list n)
+    ]
+;;
+
 type pattern =
   | Pat_any
   | Pat_var of ident
@@ -96,24 +159,11 @@ type pattern =
   | Pat_construct of
       ((ident * pattern option)
       [@gen
-        oneof
-          [ (let rec gen_list_pat n =
-               if n = 0
-               then return ("[]", None)
-               else (
-                 let element = gen_pattern_sized 0 in
-                 let tail = gen_list_pat (n / coef) in
-                 map2
-                   (fun e t -> "::", Some (Pat_tuple (e, Pat_construct t, [])))
-                   element
-                   tail)
-             in
-             gen_list_pat n)
-          ; return ("true", None)
-          ; return ("false", None)
-          ; map (fun i -> "Some", Some i) (gen_pattern_sized (n / coef))
-          ; return ("None", None)
-          ]])
+        gen_construct
+          gen_pattern_sized
+          n
+          (fun (fst_pat, snd_pat, pat_list) -> Pat_tuple (fst_pat, snd_pat, pat_list))
+          (fun (id, pat_opt) -> Pat_construct (id, pat_opt))])
   | Pat_constraint of (pattern[@gen gen_pattern_sized (n / coef)]) * core_type
 [@@deriving show { with_path = false }, qcheck]
 
@@ -130,96 +180,99 @@ type 'exp case =
 [@@deriving show { with_path = false }, qcheck]
 
 module Expression = struct
-  type value_binding_exp = t value_binding
-  and case_exp = t case
+  let gen_value_binding gen n fix_exp_fun =
+    oneof
+      [ map2 (fun var exp -> { pat = Pat_var var; exp }) gen_ident (gen (n / coef))
+      ; map3
+          (fun id type' exp -> { pat = Pat_constraint (Pat_var id, type'); exp })
+          gen_ident
+          gen_core_type
+          (gen (n / coef))
+      ; map2 (fun pat exp -> { pat; exp = fix_exp_fun exp }) gen_pattern (gen (n / coef))
+      ]
+  ;;
+
+  let gen_exp_apply gen n exp_ident exp_apply =
+    oneof
+      [ map2 (fun id arg -> exp_ident id, arg) gen_ident (gen (n / coef))
+      ; map2
+          (fun opr opn -> opr, opn)
+          (oneofl (List.map (fun (opr, _) -> exp_ident opr) un_op_list))
+          (gen (n / coef))
+      ; map3
+          (fun opr opn1 opn2 -> opr, exp_apply (opn1, opn2))
+          (oneofl (List.map (fun (opr, _) -> exp_ident opr) bin_op_list))
+          (gen (n / coef))
+          (gen (n / coef))
+      ]
+  ;;
+
+  type value_binding_exp =
+    (t value_binding
+    [@gen
+      gen_value_binding
+        gen_sized
+        n
+        (let rec fix_exp_fun = function
+           | Exp_fun (_, _, exp) -> fix_exp_fun exp
+           | Exp_function ({ left = _; right = exp }, _) -> fix_exp_fun exp
+           | Exp_constraint (exp, type') -> Exp_constraint (fix_exp_fun exp, type')
+           | exp -> exp
+         in
+         fix_exp_fun)])
+
+  and case_exp =
+    (t case
+    [@gen map2 (fun left right -> { left; right }) gen_pattern (gen_sized (n / coef))])
 
   and t =
     | Exp_ident of ident
     | Exp_constant of constant
     | Exp_let of
         rec_flag
-        * (value_binding_exp
-          [@gen map2 (fun pat exp -> { pat; exp }) gen_pattern (gen_sized (n / coef))])
-        * (value_binding_exp
-          [@gen map2 (fun pat exp -> { pat; exp }) gen_pattern (gen_sized (n / coef))])
-            list_
+        * value_binding_exp
+        * value_binding_exp list_
         * (t[@gen gen_sized (n / coef)])
     | Exp_fun of pattern * pattern list_ * (t[@gen gen_sized (n / coef)])
     | Exp_apply of
-        ((t * t * t list)
+        ((t * t)
         [@gen
-          oneof
-            [ map3
-                (fun exp first_exp exp_list -> exp, first_exp, exp_list)
-                (gen_sized 0)
-                (gen_sized (n / coef))
-                (gen_list (gen_sized (n / coef)))
-            ; map3
-                (fun op exp1 exp2 -> op, exp1, exp2)
-                (oneofl
-                   [ Exp_ident "*"
-                   ; Exp_ident "/"
-                   ; Exp_ident "+"
-                   ; Exp_ident "-"
-                   ; Exp_ident ">="
-                   ; Exp_ident "<="
-                   ; Exp_ident "<>"
-                   ; Exp_ident "="
-                   ; Exp_ident ">"
-                   ; Exp_ident "<"
-                   ; Exp_ident "&&"
-                   ; Exp_ident "||"
-                   ])
-                (gen_sized (n / coef))
-                (gen_operand (gen_sized (n / coef)))
-            ]])
-    | Exp_match of
+          gen_exp_apply
+            gen_sized
+            n
+            (fun id -> Exp_ident id)
+            (fun (opn1, opn2) -> Exp_apply (opn1, opn2))])
+    | Exp_function of case_exp * case_exp list_
+    | Exp_match of (t[@gen gen_sized (n / coef)]) * case_exp * case_exp list_
+    | Exp_ifthenelse of
         (t[@gen gen_sized (n / coef)])
-        * (case_exp
-          [@gen
-            map2 (fun left right -> { left; right }) gen_pattern (gen_sized (n / coef))])
-        * (case_exp
-          [@gen
-            map2 (fun left right -> { left; right }) gen_pattern (gen_sized (n / coef))])
-            list_
+        * (t[@gen gen_sized (n / coef)])
+        * (t[@gen gen_sized (n / coef)]) option
     | Exp_tuple of
         (t[@gen gen_sized (n / coef)])
         * (t[@gen gen_sized (n / coef)])
         * (t[@gen gen_sized (n / coef)]) list_
     | Exp_construct of
         ((ident * t option)
         [@gen
-          oneof
-            [ (let rec gen_list_exp n =
-                 if n = 0
-                 then return ("[]", None)
-                 else (
-                   let element = gen_sized 0 in
-                   let tail = gen_list_exp (n / coef) in
-                   map2
-                     (fun e t -> "::", Some (Exp_tuple (e, Exp_construct t, [])))
-                     element
-                     tail)
-               in
-               gen_list_exp n)
-            ; return ("true", None)
-            ; return ("false", None)
-            ; map (fun i -> "Some", Some i) (gen_sized (n / coef))
-            ; return ("None", None)
-            ]])
-    | Exp_ifthenelse of
-        (t[@gen gen_sized (n / coef)])
-        * (t[@gen gen_sized (n / coef)])
-        * (t[@gen gen_sized (n / coef)]) option
+          gen_construct
+            gen_sized
+            n
+            (fun (fst_exp, snd_exp, exp_list) -> Exp_tuple (fst_exp, snd_exp, exp_list))
+            (fun (id, exp_opt) -> Exp_construct (id, exp_opt))])
     | Exp_sequence of (t[@gen gen_sized (n / coef)]) * (t[@gen gen_sized (n / coef)])
     | Exp_constraint of (t[@gen gen_sized (n / coef)]) * core_type
   [@@deriving show { with_path = false }, qcheck]
 end
 
+let show_value_binding = Expression.show_value_binding_exp
+let show_case = Expression.show_case_exp
+let show_expression = Expression.show
+
 type structure_item =
   | Struct_eval of Expression.t
   | Struct_value of
-      rec_flag * Expression.t value_binding * Expression.t value_binding list_
+      rec_flag * Expression.value_binding_exp * Expression.value_binding_exp list_
 [@@deriving show { with_path = false }, qcheck]
 
 type structure = structure_item list_ [@@deriving show { with_path = false }, qcheck]