open Asttypes
open Ast_helper
open Types
open Typedtree
open Parsetree

(* some helper functions *)

(* extract_typ : Typedtree.structure -> type_expr *)
let extract_typ str = match str.str_items with
    [{str_desc = Tstr_eval ({ exp_type = typ }, _)}] -> typ
  | _ -> failwith "cannot happen"

(* split_arrow : type_expr -> type_expr * type_expr *)
let rec split_arrow typ = match typ.desc with
    Tarrow (_, t1, t2, _) -> (t1, t2)
  | Tlink (typ') -> split_arrow typ'
  | _ -> failwith "cannot happen"

(* various expressions *)

(* 1 *)
let one : expression = Exp.constant (Const.integer "1")

(* false *)
let ff : expression = Exp.construct (mknoloc (Longident.Lident "false")) None

(* variable pattern *)
let var x : pattern = Pat.var (mknoloc x)

(* fun x -> 1 *)
let fun_x_one : expression = Exp.fun_ Nolabel None (var "x") one

(* let a = 1 in fun x -> 1 *)
let exp1 : expression =
  Exp.let_ Nonrecursive [Vb.mk (var "a") one] fun_x_one

let env : Env.t = Env.initial_safe_string

(* infer type of exp1 *)
let (str1', _, _) =
  Typemod.type_structure env [Str.eval exp1] Location.none

(* type of x *)
let (typx1, _) = split_arrow (extract_typ str1')

let b1 = Ctype.moregeneral env false typx1 (Btype.newgenvar ())

;; print_endline (if b1 then "true" else "false")

(* assert false *)
let assert_false : expression = Exp.assert_ ff

(* let a = assert false in fun x -> 1 *)
let exp2 : expression =
  Exp.let_ Nonrecursive [Vb.mk (var "a") assert_false] fun_x_one

(* infer type of exp2 *)
let (str2', _, _) =
  Typemod.type_structure env [Str.eval exp2] Location.none

(* type of x *)
let (typx2, _) = split_arrow (extract_typ str2')

let b2 = Ctype.moregeneral env false typx2 (Btype.newgenvar ())

;; print_endline (if b2 then "true" else "false")