Browse Source

extract everything related to simply typed lambda calculus to a library, it can

be used with any set of primitive types
hell
zapashcanon 2 years ago
parent
commit
5cacef2e0a
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
  1. 1
      complice.opam
  2. 1
      complice_web.opam
  3. 21
      dune-project
  4. 2
      src/compile.ml
  5. 2
      src/dune
  6. 7
      src/error.ml
  7. 19
      src/pp.ml
  8. 21
      src/type_check.ml
  9. 36
      src/type_inference.ml
  10. 43
      src/types.ml
  11. 3
      src/typlib/dune
  12. 60
      src/typlib/types.ml
  13. 30
      typlib.opam

1
complice.opam

@ -12,7 +12,6 @@ depends: [
"ocaml" {>= "4.05"}
"dune" {>= "2.0"}
"bisect_ppx" {>= "1.4"}
"menhir" {>= "20200211"}
]
build: [
["dune" "subst"] {pinned}

1
complice_web.opam

@ -12,7 +12,6 @@ depends: [
"ocaml" {>= "4.05"}
"dune" {>= "2.0"}
"bisect_ppx" {>= "1.4"}
"menhir" {>= "20200211"}
]
build: [
["dune" "subst"] {pinned}

21
dune-project

@ -45,9 +45,7 @@
(dune
(>= 2.0))
(bisect_ppx
(>= 1.4))
(menhir
(>= 20200211))))
(>= 1.4))))
(package
(name complice_web)
@ -60,8 +58,19 @@
(dune
(>= 2.0))
(bisect_ppx
(>= 1.4))
(menhir
(>= 20200211))))
(>= 1.4))))
(package
(name typlib)
(synopsis "typlib")
(description
"typlib")
(depends
(ocaml
(>= 4.05))
(dune
(>= 2.0))
(bisect_ppx
(>= 1.4))))
(using menhir 2.1)

2
src/compile.ml

@ -8,7 +8,7 @@ module M = struct
type ast = Lang.t
type ast_t = Types.dddddml_type
type ast_t = Types.type_expression
let expected_ext = Some "dddddml"

2
src/dune

@ -23,7 +23,7 @@
(modules compile duplication_detection error eval lang lexer parser pp
scope_analysis scope_reduction simplification_analysis type_check
type_inference types usage_analysis)
(libraries complice)
(libraries complice typlib)
(preprocess
(pps bisect_ppx -- --conditional --exclusions src/bisect.exclude))
(preprocessor_deps

7
src/error.ml

@ -10,7 +10,7 @@ exception Internal_error of string
exception Known_value of Lang.expr
exception Recursive_type of Types.dddddml_type
exception Recursive_type of Types.type_expression
exception Scope_too_large of Lang.var_id
@ -24,9 +24,10 @@ exception Useless_if_cond of Lang.expr
exception Useless_if_expr of Lang.expr
exception Wrong_application of Lang.expr * Types.dddddml_type
exception Wrong_application of Lang.expr * Types.type_expression
exception Wrong_type of Lang.expr * Types.dddddml_type * Types.dddddml_type
exception
Wrong_type of Lang.expr * Types.type_expression * Types.type_expression
let apply_anon_const () = raise Apply_anon_const

19
src/pp.ml

@ -60,18 +60,19 @@ and fprintf_expr fmt = function
Format.fprintf fmt "if %a then %a else %a end" fprintf_expr cond
fprintf_expr e1 fprintf_expr e2
let fprintf_primitive_type fmt = function
| Types.Unit ->
Format.fprintf fmt "unit"
| Types.Bool ->
Format.fprintf fmt "bool"
let fprintf_primitive_type fmt =
let open Types in
function
| Unit -> Format.fprintf fmt "unit" | Bool -> Format.fprintf fmt "bool"
let rec fprintf_type fmt = function
| Types.Variable x ->
let rec fprintf_type fmt =
let open Types in
function
| Variable x ->
Format.fprintf fmt "%s" x
| Types.Primitive t ->
| Primitive t ->
fprintf_primitive_type fmt t
| Types.Arrow (t1, t2) ->
| Arrow (t1, t2) ->
Format.fprintf fmt "(%a -> %a)" fprintf_type t1 fprintf_type t2
let fprintf_et fmt (e, t) =

21
src/type_check.ml

@ -1,7 +1,7 @@
open Lang
module Make (M : sig
val get_type : string -> Types.dddddml_type
val get_type : string -> Types.type_expression
end) =
struct
let literal = function Unit -> Types.Unit | Bool _ -> Types.Bool
@ -12,25 +12,8 @@ struct
| Var x ->
M.get_type x
let rec type_comp =
let open Types in
function
(* TODO: this is probably wrong but will do the trick for now... *)
| Primitive _, Variable _ | Variable _, Primitive _ ->
true
| Arrow (t1, t2), Arrow (t3, t4) ->
type_comp (t1, t3) && type_comp (t2, t4)
| Primitive x, Primitive y ->
x = y
| Variable x, Variable y ->
x = y
| Primitive _, Arrow _ | Arrow _, Primitive _ ->
false
| Arrow _, Variable _ | Variable _, Arrow _ ->
false
let check_type e t expected_t =
if not @@ type_comp (t, expected_t) then Error.wrong_type e t expected_t
if not @@ Types.comp (t, expected_t) then Error.wrong_type e t expected_t
let rec expr = function
| Const c ->

36
src/type_inference.ml

@ -58,34 +58,36 @@ module Make () = struct
| Var x -> (
try Hashtbl.find infered x with Not_found -> mk_fresh x )
let rec expr = function
let rec expr =
let open Types in
function
| Const c ->
const c
| Bind (p, e, e') ->
let t = expr e in
Hashtbl.add infered p t ; expr e'
| Abstract (_, p, e) ->
| Bind (id, e1, e2) ->
let t = expr e1 in
Hashtbl.add infered id t ; expr e2
| Abstract (_, id, e) ->
let t = expr e in
Types.Arrow (Hashtbl.find infered p, t)
| Apply (e, e') -> (
let t = expr e in
let t' = expr e' in
match t with
| Types.Arrow (_t_in, t_out) ->
unify (t', _t_in) ;
Arrow (Hashtbl.find infered id, t)
| Apply (e1, e2) -> (
let t1 = expr e1 in
let t2 = expr e2 in
match t1 with
| Arrow (t_in, t_out) ->
unify (t2, t_in) ;
t_out
| Types.Variable _ ->
| Variable _ ->
let t_out = mk_fresh_dummy () in
let t_new = Types.Arrow (t', t_out) in
unify (t_new, t) ;
let t_new = Arrow (t2, t_out) in
unify (t_new, t1) ;
t_out
| _ ->
Error.wrong_application e t )
Error.wrong_application e1 t1 )
| If_then_else (cond, e1, e2) ->
let t_cond = expr cond in
let t1 = expr e1 in
let t2 = expr e2 in
unify (t_cond, Types.Primitive Types.Bool) ;
unify (t_cond, Primitive Bool) ;
unify (t1, t2) ;
t1

43
src/types.ml

@ -1,42 +1,9 @@
type primitive_type = Unit | Bool
type type_variable = string
type dddddml_type =
| Variable of type_variable
| Primitive of primitive_type
| Arrow of dddddml_type * dddddml_type
(* true if t appears in t' *)
let rec contains t t' =
if t = t' then true
else
match t' with
| Arrow (t1, t2) ->
contains t t1 || contains t t2
| _ ->
false
(** substitute t by t' in e *)
let subst (t, t') e =
let rec aux e =
if e = t then t'
else
match e with
| Variable _ | Primitive _ ->
e
| Arrow (t1, t2) ->
Arrow (aux t1, aux t2)
in
aux e
let primitive_card = function Unit -> 1 | Bool -> 2
let rec card = function
| Variable x ->
failwith (Format.sprintf "unknown card for type variable `%s`" x)
| Primitive t ->
primitive_card t
| Arrow (t1, t2) ->
int_of_float
@@ Float.pow (float_of_int @@ card t2) (float_of_int @@ card t1)
include Typlib.Types.Make (struct
type nonrec primitive_type = primitive_type
let primitive_card = primitive_card
end)

3
src/typlib/dune

@ -0,0 +1,3 @@
(library
(public_name typlib)
(modules types))

60
src/typlib/types.ml

@ -0,0 +1,60 @@
module Make (M : sig
type primitive_type
val primitive_card : primitive_type -> int
end) =
struct
type type_variable = string
type type_expression =
| Variable of type_variable
| Primitive of M.primitive_type
| Arrow of type_expression * type_expression
(** true if t appears in t' *)
let contains t t' =
let rec aux = function
| x when x = t ->
true
| Arrow (t1, t2) ->
aux t1 || aux t2
| _ ->
false
in
aux t'
(** substitue t by t' in e *)
let subst (t, t') e =
let rec aux = function
| x when x = t ->
t'
| (Variable _ | Primitive _) as x ->
x
| Arrow (t1, t2) ->
Arrow (aux t1, aux t2)
in
aux e
let rec comp = function
| Primitive _, Variable _ | Variable _, Primitive _ ->
true
| Arrow (t1, t2), Arrow (t3, t4) ->
comp (t1, t3) && comp (t2, t4)
| Primitive x, Primitive y ->
x = y
| Variable x, Variable y ->
x = y
| Primitive _, Arrow _ | Arrow _, Primitive _ ->
false
| Arrow _, Variable _ | Variable _, Arrow _ ->
false
let rec card = function
| Variable x ->
failwith (Format.sprintf "unknown card for type variable `%s`" x)
| Primitive t ->
M.primitive_card t
| Arrow (t1, t2) ->
int_of_float
@@ Float.pow (float_of_int @@ card t2) (float_of_int @@ card t1)
end

30
typlib.opam

@ -0,0 +1,30 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
synopsis: "typlib"
description: "typlib"
maintainer: ["Léo Andrès <contact@ndrs.fr>"]
authors: ["Léo Andrès <contact@ndrs.fr>"]
license: "ISC"
homepage: "https://git.zapashcanon.fr/zapashcanon/dddddml"
doc: "https://doc.zapashcanon.fr/dddddml/"
bug-reports: "https://git.zapashcanon.fr/zapashcanon/dddddml/issues"
depends: [
"ocaml" {>= "4.05"}
"dune" {>= "2.0"}
"bisect_ppx" {>= "1.4"}
]
build: [
["dune" "subst"] {pinned}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
dev-repo: "git://git.zapashcanon.fr/zapashcanon/dddddml.git"
Loading…
Cancel
Save