OCaml LET REC правило печатания для вывода типа - PullRequest
Новая
       11

OCaml LET REC правило печатания для вывода типа

0 голосов
/ 07 декабря 2018

В настоящее время я пытаюсь реализовать анализатор типов с использованием системы статических типов, реализованной с использованием языка OCaml.

Алгоритм, который я использую, заключается в том, чтобы сначала генерировать уравнения типов, а затем решать эти уравнения с помощьюалгоритм унификации.Я смог реализовать код достаточно хорошо, за исключением рекурсивного типа привязки * 1003. *.

Вот полный код : 

type program = exp
and exp = 
  | NUM of int
  | VAR of var
  | SUM of exp * exp
  | DIFF of exp * exp
  | MULT of exp * exp
  | DIV of exp * exp
  | ZERO of exp
  | IF of exp * exp * exp
  | LET of var * exp * exp
  | LETREC of var * var * exp * exp
  | FUNC of var * exp
  | CALL of exp * exp
and var = string
;;

type typ = TypeInt | TypeBool | TypeFun of typ * typ | TypeVar of tyvar
and tyvar = string
;;
type type_equation = (typ * typ) list;;

module TypeEnv = struct
  type t = var -> typ

  let empty
  = fun _ -> raise (Failure "Type Env is empty")

  let extend (x, t) tenv
  = fun y -> if x = y then t else (tenv y)

  let find tenv x = tenv x
end
;;

let typevar_num = ref 0;;

let new_typevar () = (typevar_num := !typevar_num + 1; (TypeVar ("t" ^ string_of_int !typevar_num)));;

let rec generate_eqns : TypeEnv.t -> exp -> typ -> type_equation 
= fun tenv e ty ->
  match e with
  | NUM n -> [(ty, TypeInt)]
  | VAR x -> [(ty, TypeEnv.find tenv x)]
  | SUM (e1, e2) -> let eq1 = [(ty, TypeInt)] in
                      let eq2 = generate_eqns tenv e1 TypeInt in
                        let eq3 = generate_eqns tenv e2 TypeInt in
                          eq1 @ eq2 @ eq3
  | DIFF (e1, e2) -> let eq1 = [(ty, TypeInt)] in
                      let eq2 = generate_eqns tenv e1 TypeInt in
                        let eq3 = generate_eqns tenv e2 TypeInt in
                          eq1 @ eq2 @ eq3
  | DIV (e1, e2) -> let eq1 = [(ty, TypeInt)] in
                      let eq2 = generate_eqns tenv e1 TypeInt in
                        let eq3 = generate_eqns tenv e2 TypeInt in
                          eq1 @ eq2 @ eq3
  | MULT (e1, e2) -> let eq1 = [(ty, TypeInt)] in
                      let eq2 = generate_eqns tenv e1 TypeInt in
                        let eq3 = generate_eqns tenv e2 TypeInt in
                          eq1 @ eq2 @ eq3
  | ISZERO e -> let eq1 = [(ty, TypeBool)] in
                  let eq2 = generate_eqns tenv e TypeInt in
                    eq1 @ eq2
  | IF (e1, e2, e3) -> let eq1 = generate_eqns tenv e1 TypeBool in
                         let eq2 = generate_eqns tenv e2 ty in
                           let eq3 = gen_equations tenv e3 ty in
                             eq1 @ eq2 @ eq3
  | LET (x, e1, e2) -> let t1 = new_typevar () in
                         let eq1 = generate_eqns tenv e1 t1 in
                           let eq2 = generate_eqns (TypeEnv.extend (x, t1) tenv) e2 ty in
                             eq1 @ eq2
  | LETREC (f, x, e1, e2) -> (* let t1 = new_typevar () in
                           let new_env = TypeEnv.extend (x, t1) tenv in
                             let eq1 = generate_eqns new_env f *)
  | FUNC (x, e) -> let t1 = new_typevar () in
                     let t2 = new_typevar () in
                       let eq1 = [(ty, TypeFun (t1, t2))] in
                         let eq2 = generate_eqns (TypeEnv.extend (x, t1) tenv) e t2 in
                           eq1 @ eq2
  | CALL (e1, e2) -> let t1 = new_typevar () in
                       let eq1 = generate_eqns tenv e1 (TypeFun (t1, ty)) in
                         let eq2 = generate_eqns tenv e2 t1 in
                           eq1 @ eq2
;;


Основной функцией, которая выполняет генерацию уравнения типа, является generate_eqns.Он принимает пустое окружение типа, выражение и начальный тип в качестве аргументов и вызывается так: generate_eqns TypeEnv.empty (NUM 3) (new_typevar ()).

У меня проблемы с реализацией рекурсивного вызова LETREC.Я пытался найти материалы в Интернете, но они, похоже, не слишком помогают моей проблеме.

В частности, я пытался проанализировать это правило набора текста из Основы программированияЯзыки (3e) - Фридман и Жезл :

enter image description here

Кто-нибудь будет достаточно любезен, чтобы дать мне несколько советов или советов?

Спасибо.

1 Ответ

0 голосов
/ 07 декабря 2018

Итак, я просмотрел ваш код, этот непроверенный и т. Д. Но на первый взгляд я полагаю, что это должно быть что-то вроде этого, 

  | LETREC (f, x, e1, e2) ->
     let tx  = new_typevar ()    in (** type of x   **)
     let tfx = new_typevar ()    in (** type of f x **)
     let tf  = TypeFun (tx, tfx) in (** type of f   **)
     let tenvf  = TypeEnv.extend (f, tf) tenv  in (** f in env **) 
     let tenvxf = TypeEnv.extend (x, tx) tenvf in (** x and f in env **) 
     let eq1 = generate_eqns tenvxf e1 tfx in (** type e1 = type (f x) **)
     let eq2 = generate_eqns tenvf  e2 ty  in (** type e2 = typ **)
         eq1 @ eq2
...