commit 6c49dbe4642edde8743597bd94b19f03988a4d8a Author: zapashcanon Date: Fri Mar 6 17:45:57 2020 +0100 first commit diff --git a/.build.yml b/.build.yml new file mode 100644 index 0000000..1579965 --- /dev/null +++ b/.build.yml @@ -0,0 +1,80 @@ +image: debian/unstable +packages: + - opam + - ocaml + - curl +environment: + deploy: fs@zapashcanon.fr + sshopts: "-o StrictHostKeyChecking=no -q" +secrets: + - ec1f49cd-38dc-41d9-89f4-c3b6ecd7bcad # ssh deploy key + - b5b0e36c-fe52-43c4-9103-0aa918ad175c # github token + - c9e55d80-7b6a-4ad4-81bd-921d2c3247b8 # dune release profile + - ff8575b8-7192-4e0c-9905-6d04142a4ec1 # git config +tasks: + - setup: | + opam init -y + opam update -y + opam install -y dune bisect_ppx odoc ocamlformat + - lint-format: | + cd $GIT_REPO_NAME + eval "$(opam env)" + ocamlformat -p ocamlformat --enable-outside-detected-project --check $(find . -name '*.ml') + - build: | + cd $GIT_REPO_NAME + eval "$(opam env)" + dune build @all + - test: | + cd $GIT_REPO_NAME + eval "$(opam env)" + dune runtest + - deploy-doc: | + cd $GIT_REPO_NAME + eval "$(opam env)" + dune build @doc + doc_dst="/var/www/doc.zapashcanon.fr/$GIT_REPO_NAME/" + ssh $sshopts $deploy "mkdir -p $doc_dst" + scp $sshopts -r _build/default/_doc/_html/* $deploy:$doc_dst + - deploy-coverage: | + cd $GIT_REPO_NAME + eval "$(opam env)" + dune clean + BISECT_ENABLE=YES dune runtest --no-buffer --force > /dev/null + bisect-ppx-report -html _coverage/ "$(find . -name 'bisect*.out')" + cov_dst="/var/www/coverage.zapashcanon.fr/$GIT_REPO_NAME/" + ssh $sshopts $deploy "mkdir -p $cov_dst" + scp $sshopts -r _coverage/* $deploy:$cov_dst + - archive: | + cd $GIT_REPO_NAME + eval "$(opam env)" + dune clean + archive=${GIT_REPO_NAME}-dev.tar.xz + git archive -o $archive HEAD + arc_dst="/var/www/fs.zapashcanon.fr/archive/$GIT_REPO_NAME/" + ssh $sshopts $deploy "mkdir -p $arc_dst" + scp $sshopts $archive $deploy:$arc_dst + rm $archive + - release: | + cd $GIT_REPO_NAME + eval "$(opam env)" + [ -n "$GIT_TAG" ] || exit 0 + opam install -y dune-release + dune-release distrib || true + archive=${GIT_REPO_NAME}-${GIT_TAG}.tbz + ls _build/${archive} + arc_dst="/var/www/fs.zapashcanon.fr/archive/$GIT_REPO_NAME/" + scp $sshopts _build/${archive} $deploy:$arc_dst + url="https://fs.zapashcanon.fr/archive/$GIT_REPO_NAME/$archive" + echo $url > _build/${GIT_REPO_NAME}-${GIT_TAG}.url + dune-release opam pkg + opam_file=_build/${GIT_REPO_NAME}.${GIT_TAG}/opam + line_num="$(grep -n -e 'src:' $opam_file | cut -d: -f1)" + sed -i -e "${line_num}s|^.*| src: \"${url}\"|" $opam_file + line_num=$(($line_num + 1)) + sed -i -e "${line_num}d" $opam_file + sed -i -e "${line_num}d" $opam_file + cd .. + echo -e "Host github.com\n\tStrictHostKeyChecking no\n" >> ~/.ssh/config + git clone https://github.com/Cameleo/opam-repository.git + cd $GIT_REPO_NAME + dune-release opam submit --no-auto-open -y diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..4c9c859 --- /dev/null +++ b/.gitignore @@ -0,0 +1,4 @@ +_build/ +_coverage/ +*.merlin +*.install diff --git a/CHANGES.md b/CHANGES.md new file mode 100644 index 0000000..e69de29 diff --git a/LICENSE.md b/LICENSE.md new file mode 100644 index 0000000..cba946b --- /dev/null +++ b/LICENSE.md @@ -0,0 +1,8 @@ +The ISC License (ISC) +===================== + +Copyright © 2020, Léo Andrès + +Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appear in all copies. + +THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..75d01d1 --- /dev/null +++ b/README.md @@ -0,0 +1,11 @@ +# dddddml [![builds.sr.ht status](https://builds.sr.ht/~zapashcanon/dddddml.svg)](https://builds.sr.ht/~zapashcanon/dddddml?) + +dddddml. + +- [LICENSE] +- [CHANGELOG] +- [documentation] + +[CHANGELOG]: ./CHANGES.md +[documentation]: https://doc.zapashcanon.fr/dddddml/ +[LICENSE]: ./LICENSE.md diff --git a/complice.opam b/complice.opam new file mode 100644 index 0000000..b6a2c04 --- /dev/null +++ b/complice.opam @@ -0,0 +1,30 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "complice" +description: "complice" +maintainer: ["Léo Andrès "] +authors: ["Léo Andrès "] +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" diff --git a/dddddml.opam b/dddddml.opam new file mode 100644 index 0000000..79209d4 --- /dev/null +++ b/dddddml.opam @@ -0,0 +1,30 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "dddddml" +description: "ddddd à la ML" +maintainer: ["Léo Andrès "] +authors: ["Léo Andrès "] +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" diff --git a/doc/dune b/doc/dune new file mode 100644 index 0000000..e2f3285 --- /dev/null +++ b/doc/dune @@ -0,0 +1,3 @@ +(documentation + (package dddddml) + (mld_files usage index)) diff --git a/doc/index.mld b/doc/index.mld new file mode 100644 index 0000000..79575ed --- /dev/null +++ b/doc/index.mld @@ -0,0 +1,7 @@ +{0 dddddml} + +todo + +todo + +See {{:usage.html} usage} for a short explanation on how to use the library and {{:Memo/index.html} Memo} for a more detailled explanation. diff --git a/doc/usage.mld b/doc/usage.mld new file mode 100644 index 0000000..ad32fef --- /dev/null +++ b/doc/usage.mld @@ -0,0 +1,3 @@ +{0 Usage} + +todo diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..27be3aa --- /dev/null +++ b/dune-project @@ -0,0 +1,48 @@ +(lang dune 2.0) + +(name dddddml) + +(license ISC) + +(authors "Léo Andrès ") + +(maintainers "Léo Andrès ") + +(source + (uri git://git.zapashcanon.fr/zapashcanon/dddddml.git)) + +(bug_reports https://git.zapashcanon.fr/zapashcanon/dddddml/issues) + +(homepage https://git.zapashcanon.fr/zapashcanon/dddddml) + +(documentation https://doc.zapashcanon.fr/dddddml/) + +(generate_opam_files true) + +(package + (name dddddml) + (synopsis "dddddml") + (description + "ddddd à la ML") + (depends + (ocaml + (>= 4.05)) + (dune + (>= 2.0)) + (bisect_ppx + (>= 1.4)))) + +(package + (name complice) + (synopsis "complice") + (description + "complice") + (depends + (ocaml + (>= 4.05)) + (dune + (>= 2.0)) + (bisect_ppx + (>= 1.4)))) + +(using menhir 2.1) diff --git a/src/complice/cli.ml b/src/complice/cli.ml new file mode 100644 index 0000000..efae5e7 --- /dev/null +++ b/src/complice/cli.ml @@ -0,0 +1,22 @@ +module Make (M : S.S) = struct + let fail = Utils.failwith + + let check_usage () = + if Array.length Sys.argv <> 2 then + fail (Format.sprintf "usage: %s " Sys.argv.(0)) + + let check_file_name f = + if not (Sys.file_exists f) then + fail (Format.sprintf "file %s doesn't exist" f) ; + if Sys.is_directory f then fail (Format.sprintf "file %s is a directory" f) ; + match M.expected_ext with + | None -> + () + | Some ext -> + if not (Filename.check_suffix f ext) then + fail + (Format.sprintf "file %s doesn't have the expected extension: %s" f + ext) ; + let name = Filename.chop_suffix (Filename.basename f) ext in + if String.length name = 0 then fail "file name shouldn't be empty" +end diff --git a/src/complice/comp.ml b/src/complice/comp.ml new file mode 100644 index 0000000..f4f5feb --- /dev/null +++ b/src/complice/comp.ml @@ -0,0 +1,9 @@ +module Make (L : S.S) = struct + module Cli = Cli.Make (L) + module Parse = Parse.Make (L) + + let compile () = + Cli.check_usage () ; + let file = Sys.argv.(1) in + Cli.check_file_name file ; Parse.from_file file +end diff --git a/src/complice/dune b/src/complice/dune new file mode 100644 index 0000000..4fa715d --- /dev/null +++ b/src/complice/dune @@ -0,0 +1,3 @@ +(library + (public_name complice) + (modules cli comp lexer parse s utils)) diff --git a/src/complice/lexer.ml b/src/complice/lexer.ml new file mode 100644 index 0000000..fcbcf69 --- /dev/null +++ b/src/complice/lexer.ml @@ -0,0 +1,43 @@ +module type S = sig + val get_mem_new_line : unit -> int list + + val unexpected_char : char -> unit + + val incr_offset_string : string -> unit + + val new_line_met : unit -> unit + + val incr_offset : int -> unit +end + +module Make () : S = struct + let curr_line = ref 1 + + let curr_offset = ref 1 + + let total_offset = ref 1 + + let mem_new_line = ref [] + + let get_mem_new_line () = List.rev !mem_new_line + + let new_line_met () = + incr total_offset ; + mem_new_line := !total_offset :: !mem_new_line ; + incr curr_line ; + curr_offset := 0 + + let incr_offset x = + total_offset := !total_offset + x ; + curr_offset := !curr_offset + x + + let incr_offset_string x = incr_offset (String.length x) + + let fail msg = + Utils.failwith + (Format.sprintf "lexer: line %d, at offset %d: %s" !curr_line !curr_offset + msg) + + let unexpected_char c = + fail (Format.sprintf "unexpected character: '%s'" (Char.escaped c)) +end diff --git a/src/complice/parse.ml b/src/complice/parse.ml new file mode 100644 index 0000000..5262a14 --- /dev/null +++ b/src/complice/parse.ml @@ -0,0 +1,28 @@ +module Make (M : S.S) = struct + let fail s = Utils.failwith (Format.sprintf "parser: %s" s) + + let from_lexing buf = + let exception Stop in + try M.Parser.file M.Lexer.token buf + with M.Parser.Error -> + let err_pos = Lexing.lexeme_start buf in + let err_line, line_offset = (ref 1, ref 0) in + ( try + List.iter + (fun x -> + if x > err_pos then raise Stop ; + incr err_line ; + line_offset := x) + (M.Lexer.Helper.get_mem_new_line ()) + with Stop -> () ) ; + let offset = err_pos - !line_offset in + fail + (Format.sprintf "on line %d at offset %d, syntax error" !err_line + offset) + + let from_file f = + let chan = open_in f in + let buf = Lexing.from_channel chan in + let res = from_lexing buf in + close_in chan ; res +end diff --git a/src/complice/s.ml b/src/complice/s.ml new file mode 100644 index 0000000..a6a6842 --- /dev/null +++ b/src/complice/s.ml @@ -0,0 +1,19 @@ +module type S = sig + type ast + + module Parser : sig + type token + + exception Error + + val file : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> ast + end + + module Lexer : sig + val token : Lexing.lexbuf -> Parser.token + + module Helper : Lexer.S + end + + val expected_ext : string option +end diff --git a/src/complice/utils.ml b/src/complice/utils.ml new file mode 100644 index 0000000..ca7ba9e --- /dev/null +++ b/src/complice/utils.ml @@ -0,0 +1 @@ +let failwith s = Format.eprintf "%s@." s ; exit 1 diff --git a/src/dddddmlc.ml b/src/dddddmlc.ml new file mode 100644 index 0000000..deaf529 --- /dev/null +++ b/src/dddddmlc.ml @@ -0,0 +1,29 @@ +module Compiler = Complice.Comp.Make (struct + include Dddddml + + type ast = Dddddml.Lang.t + + let expected_ext = Some "dddddml" +end) + +let _ = + let print s = Format.printf "%s@." s in + let open Dddddml in + print "lexing and parsing..." ; + let ast = Compiler.compile () in + (* let print_ast = Pp.fprintf_file Format.std_formatter in *) + (* print_ast ast; *) + print "analysing scope..." ; + let renamed_ast, _old_names = Scope_analysis.file ast in + (* Hashtbl.iter (fun k v -> Format.printf "variable %s was %s@." k v) _old_names; *) + (* print_ast renamed_ast; *) + print "infering types..." ; + let infered, t = Type_inference.file renamed_ast in + (* Hashtbl.iter (fun k v -> + Format.printf "%s has type %a@." k Pp.fprintf_type v + ) infered; *) + print "type checking..." ; + Type_check.file renamed_ast infered ; + print "OK !" ; + Format.printf "%a : %a@." Pp.fprintf_expr ast Pp.fprintf_type t ; + () diff --git a/src/dune b/src/dune new file mode 100644 index 0000000..bde9e13 --- /dev/null +++ b/src/dune @@ -0,0 +1,20 @@ +(executable + (package dddddml) + (public_name dddddmlc) + (libraries complice dddddml) + (modules dddddmlc) + (preprocess + (pps bisect_ppx -conditional))) + +(library + (public_name dddddml) + (modules lang lexer parser pp scope_analysis type_check type_inference types) + (libraries complice) + (preprocess + (pps bisect_ppx -conditional))) + +(ocamllex + (modules lexer)) + +(menhir + (modules parser)) diff --git a/src/lang.ml b/src/lang.ml new file mode 100644 index 0000000..1cfa890 --- /dev/null +++ b/src/lang.ml @@ -0,0 +1,19 @@ +(* ast *) + +type pattern = string + +type var_id = string + +type literal = Unit | Bool of bool + +type const = Literal of literal | Var of var_id + +type expr = + | Const of const + | Bind of pattern * expr * expr + | Abstract of pattern * expr + | Apply of expr * expr + +type file = expr + +type t = file diff --git a/src/lexer.mll b/src/lexer.mll new file mode 100644 index 0000000..bdc7182 --- /dev/null +++ b/src/lexer.mll @@ -0,0 +1,25 @@ +{ open Parser + + module Helper = Complice.Lexer.Make () + module M = Helper + +} + +let newline = ['\n' '\r'] +let whitespace = [' ' '\t'] +let var_id = ['a'-'z' 'A'-'Z']+ + +rule token = parse + | newline { M.new_line_met (); token lexbuf } + | whitespace { M.incr_offset 1; token lexbuf } + | "false" { M.incr_offset 5; BOOL false } + | "true" { M.incr_offset 4; BOOL true } + | "unit" { M.incr_offset 4; UNIT } + | "let" { M.incr_offset 3; LET } + | "fun" { M.incr_offset 3; FUN } + | "in" { M.incr_offset 2; IN } + | "->" { M.incr_offset 2; RARROW } + | "=" { M.incr_offset 1; EQ } + | var_id as id { M.incr_offset_string id; VARID id } + | eof { EOF } + | _ as c { M.incr_offset 1; M.unexpected_char c; EOF } diff --git a/src/parser.mly b/src/parser.mly new file mode 100644 index 0000000..f912084 --- /dev/null +++ b/src/parser.mly @@ -0,0 +1,39 @@ +%{ + open Lang +%} + +%token LET FUN IN RARROW EQ +%token UNIT +%token BOOL +%token VARID +%token EOF + +%right LET +%right IN +%left FUN RARROW BOOL VARID UNIT + +%start file + +%% +%inline literal: +| UNIT { Unit } +| b = BOOL { Bool b } + +%inline var_id: +| id = VARID { id } + +%inline const: +| l = literal { Literal l } +| v = var_id { Var v } + +%inline pattern: +| p = var_id { p } + +expr: +| FUN p = pattern RARROW e = expr { Abstract (p, e) } +| LET p = pattern EQ e = expr IN e2 = expr { Bind (p, e, e2) } +| e = expr e2 = expr { Apply (e, e2) } +| c = const { Const c } + +file: +| e = expr EOF { e } diff --git a/src/pp.ml b/src/pp.ml new file mode 100644 index 0000000..76ff663 --- /dev/null +++ b/src/pp.ml @@ -0,0 +1,42 @@ +open Lang + +let fprintf_literal fmt = function + | Unit -> + Format.fprintf fmt "unit" + | Bool b -> + Format.fprintf fmt "%B" b + +let fprintf_const fmt = function + | Literal l -> + Format.fprintf fmt "%a" fprintf_literal l + | Var v -> + Format.fprintf fmt "%s" v + +let fprintf_pattern fmt p = Format.fprintf fmt "%s" p + +let rec fprintf_expr fmt = function + | Const c -> + fprintf_const fmt c + | Bind (p, e, e') -> + Format.fprintf fmt "let %a = %a in %a" fprintf_pattern p fprintf_expr e + fprintf_expr e' + | Abstract (p, e) -> + Format.fprintf fmt "(fun %a -> %a)" fprintf_pattern p fprintf_expr e + | Apply (e, e') -> + Format.fprintf fmt "%a %a" fprintf_expr e fprintf_expr e' + +let fprintf_file fmt f = Format.fprintf fmt "%a@." fprintf_expr f + +let fprintf_primitive_type fmt = function + | Types.Unit -> + Format.fprintf fmt "unit" + | Types.Bool -> + Format.fprintf fmt "bool" + +let rec fprintf_type fmt = function + | Types.Variable x -> + Format.fprintf fmt "%s" x + | Types.Primitive t -> + fprintf_primitive_type fmt t + | Types.Arrow (t1, t2) -> + Format.fprintf fmt "(%a -> %a)" fprintf_type t1 fprintf_type t2 diff --git a/src/scope_analysis.ml b/src/scope_analysis.ml new file mode 100644 index 0000000..4952b13 --- /dev/null +++ b/src/scope_analysis.ml @@ -0,0 +1,67 @@ +open Lang + +let fail s = Complice.Utils.failwith (Format.sprintf "scope analysis: %s" s) + +module Scope () = struct + let mk_fresh = + let seen = Hashtbl.create 512 in + fun x -> + match Hashtbl.find_opt seen x with + | None -> + Hashtbl.add seen x 0 ; x + | Some n -> + Hashtbl.replace seen x (n + 1) ; + Format.sprintf "_%s%d" x n + + module Env = Map.Make (String) + + let old_names = Hashtbl.create 512 + + let unused = Hashtbl.create 512 + + let add key value scope = + Hashtbl.add old_names value key ; + Hashtbl.add unused value () ; + Env.add key value scope + + let const scope = function + | Literal b -> + Literal b + | Var id -> ( + try + let new_name = Env.find id scope in + Hashtbl.remove unused new_name ; + Var new_name + with Not_found -> fail (Format.sprintf "unbound variable %s" id) ) + + let rec expr scope = function + | Const c -> + Const (const scope c) + | Bind (p, e, e') -> + let fresh_p = mk_fresh p in + let fresh_e = expr scope e in + let fresh_e' = expr (add p fresh_p scope) e' in + Bind (fresh_p, fresh_e, fresh_e') + | Abstract (p, e) -> + let fresh_p = mk_fresh p in + let fresh_e = expr (add p fresh_p scope) e in + Abstract (fresh_p, fresh_e) + | Apply (e, e') -> + Apply (expr scope e, expr scope e') + + let check_unused () = + Hashtbl.iter + (fun k _ -> + fail (Format.sprintf "unused variable %s" (Hashtbl.find old_names k))) + unused + + let file f = + let res = expr Env.empty f in + check_unused () ; res +end + +let file f = + let module M = Scope () in + let renamed = M.file f in + let old_names = M.old_names in + (renamed, old_names) diff --git a/src/type_check.ml b/src/type_check.ml new file mode 100644 index 0000000..0a6432f --- /dev/null +++ b/src/type_check.ml @@ -0,0 +1,51 @@ +open Lang + +let fail s = Complice.Utils.failwith (Format.sprintf "type check: %s" s) + +module type S = sig + val get_type : string -> Types.dddddml_type +end + +module Check (M : S) = struct + let literal = function Unit -> Types.Unit | Bool _ -> Types.Bool + + let const = function + | Literal l -> + Types.Primitive (literal l) + | Var x -> + M.get_type x + + let check_type e t expected_t = + if t <> expected_t then + fail + (Format.asprintf + "expression %a has type %a but an expression of type %a was expected" + Pp.fprintf_expr e Pp.fprintf_type t Pp.fprintf_type expected_t) + + let rec expr = function + | Const c -> + const c + | Bind (x, e, e') -> + let t = expr e in + let expected_t = M.get_type x in + check_type e t expected_t ; expr e' + | Abstract (p, e) -> + Types.Arrow (M.get_type p, expr e) + | Apply (e, e') -> ( + let t = expr e in + let t' = expr e' in + match t with + | Types.Arrow (_, t_out) -> + check_type e t (Types.Arrow (t', t_out)) ; + t_out + | _ -> + fail + "function expected (should have been reported during type \ + inference)" ) +end + +let file f tbl = + let module M = Check (struct + let get_type x = Hashtbl.find tbl x + end) in + ignore (M.expr f) diff --git a/src/type_inference.ml b/src/type_inference.ml new file mode 100644 index 0000000..d34b51e --- /dev/null +++ b/src/type_inference.ml @@ -0,0 +1,105 @@ +open Lang + +let fail s = Complice.Utils.failwith (Format.sprintf "type inference: %s" s) + +module Inference () = struct + let subst = Hashtbl.create 512 + + let add_subst t t' = Hashtbl.add subst t t' + + let rec unify = + let open Types in + function + | Primitive t, Primitive t' when t = t' -> + () + | Primitive t, Variable v | Variable v, Primitive t -> + add_subst (Variable v) (Primitive t) + | Arrow (t1, t1'), Arrow (t2, t2') -> + unify (t1, t2) ; + unify (t1', t2') + | Variable v, Variable v' -> + add_subst (Variable v) (Variable v') + | _ -> + fail "can't unify (unsatisfiable constraint)" + + let infered = Hashtbl.create 512 + + let mk_fresh = + let count = ref (-1) in + fun x -> + incr count ; + let res = Types.Variable (Format.sprintf "_t%d" !count) in + Hashtbl.add infered x res ; res + + let literal = function Unit -> Types.Unit | Bool _ -> Types.Bool + + let const = function + | Literal l -> + Types.Primitive (literal l) + | Var x -> ( + try Hashtbl.find infered x with Not_found -> mk_fresh x ) + + let rec expr = function + | Const c -> + const c + | Bind (p, e, e') -> + let t = expr e in + Hashtbl.add infered p t ; expr e' + | Abstract (p, 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_in, t') ; + t_out + | _ -> + fail + (Format.asprintf + "%a has type %a, it is not a function, it can't be applied" + Pp.fprintf_expr e Pp.fprintf_type t) ) + + let file f = + let res = expr f in + res +end + +let file f = + let module M = Inference () in + let res = ref (M.file f) in + let keep_on = ref true in + let check_cycle orig x = + let rec aux x = + match Hashtbl.find_opt M.subst x with + | None -> + () + | Some y -> + (* TODO: print the list of ids in which orig appears... *) + if y = orig then + fail + (Format.asprintf + "type %a is recursive, stop doing this please... ( \ + https://youtu.be/mqA2evDu4Mw )" + Pp.fprintf_type orig) ; + aux y + in + aux x + in + Hashtbl.iter (fun k _ -> check_cycle k k) M.subst ; + while !keep_on do + keep_on := false ; + Hashtbl.iter + (fun old_type new_type -> + res := Types.subst old_type new_type !res ; + Hashtbl.iter + (fun var var_type -> + let new_var_type = Types.subst old_type new_type var_type in + if var_type <> new_var_type then ( + Hashtbl.replace M.infered var new_var_type ; + keep_on := true )) + M.infered) + M.subst + done ; + (M.infered, !res) diff --git a/src/types.ml b/src/types.ml new file mode 100644 index 0000000..f205cae --- /dev/null +++ b/src/types.ml @@ -0,0 +1,17 @@ +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 + +let rec subst t t' e = + if e = t then t' + else + match e with + | Variable _ | Primitive _ -> + e + | Arrow (t1, t2) -> + Arrow (subst t t' t1, subst t t' t2) diff --git a/test/cc.dddddml b/test/cc.dddddml new file mode 100644 index 0000000..675a136 --- /dev/null +++ b/test/cc.dddddml @@ -0,0 +1 @@ +let x = true in true diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..dcda481 --- /dev/null +++ b/test/dune @@ -0,0 +1,3 @@ +(test + (name test) + (libraries dddddml)) diff --git a/test/id.dddddml b/test/id.dddddml new file mode 100644 index 0000000..e887e12 --- /dev/null +++ b/test/id.dddddml @@ -0,0 +1 @@ +let id = fun x -> x in id diff --git a/test/renaming.dddddml b/test/renaming.dddddml new file mode 100644 index 0000000..4e0a54f --- /dev/null +++ b/test/renaming.dddddml @@ -0,0 +1,4 @@ +let f = fun x -> + let g = fun x -> x in + g x +in f true diff --git a/test/test.ml b/test/test.ml new file mode 100644 index 0000000..8271edc --- /dev/null +++ b/test/test.ml @@ -0,0 +1 @@ +let _ = Format.printf "Tests are OK !@." diff --git a/test/unbound.dddddml b/test/unbound.dddddml new file mode 100644 index 0000000..f09f505 --- /dev/null +++ b/test/unbound.dddddml @@ -0,0 +1 @@ +let bla = true in blo diff --git a/test/unused.dddddml b/test/unused.dddddml new file mode 100644 index 0000000..023fa00 --- /dev/null +++ b/test/unused.dddddml @@ -0,0 +1,4 @@ +let f = true in +let g = fun x -> x in +let f = false in +g f diff --git a/test/wrongapp.dddddml b/test/wrongapp.dddddml new file mode 100644 index 0000000..b81faca --- /dev/null +++ b/test/wrongapp.dddddml @@ -0,0 +1 @@ +true true diff --git a/test/wrongtype.dddddml b/test/wrongtype.dddddml new file mode 100644 index 0000000..bd2df1b --- /dev/null +++ b/test/wrongtype.dddddml @@ -0,0 +1,4 @@ +let f = fun x -> + let g = fun x -> x in + g x +in f f diff --git a/test/wrongtype2.dddddml b/test/wrongtype2.dddddml new file mode 100644 index 0000000..02b58de --- /dev/null +++ b/test/wrongtype2.dddddml @@ -0,0 +1,4 @@ +let f = fun x -> + let g = fun x -> x in + g x +in f f true