Février 2016 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][master] 15 commits: sexp_parse_to_list + debugs in one files
by Setepenre 01 Mar '16

01 Mar '16

Setepenre pushed to branch master at Stefan / Typer Commits: 59caf4c8 by Pierre Delaunay at 2016-02-18T17:04:36-05:00 sexp_parse_to_list + debugs in one files - - - - - 2c1f85fe by Pierre Delaunay at 2016-02-19T17:42:47-05:00 pexp debug_print - - - - - 1617fc49 by Pierre Delaunay at 2016-02-19T18:11:50-05:00 add pexp test file - - - - - f27e2fe6 by Pierre Delaunay at 2016-02-20T11:04:54-05:00 Pinductive fix - - - - - 15297a8c by Pierre Delaunay at 2016-02-22T16:52:39-05:00 debuijn data structure - - - - - d5019e4a by Pierre Delaunay at 2016-02-24T23:10:18-05:00 let/Arrow/Lambda lexp - - - - - 24668c78 by Pierre Delaunay at 2016-02-24T23:47:20-05:00 comment cleaning - - - - - fc20af3d by Pierre Delaunay at 2016-02-25T00:50:45-05:00 pexp_decls function node activated - - - - - 4115d3ff by Pierre Delaunay at 2016-02-25T01:29:52-05:00 add 'Section' (sexp, pexp, lexp, ...) in error message - - - - - a0c7ef21 by Pierre Delaunay at 2016-02-25T19:16:48-05:00 merging - - - - - 25508a29 by Pierre Delaunay at 2016-02-25T20:41:14-05:00 add Debruijn index - - - - - f9d3f518 by Pierre Delaunay at 2016-02-26T17:12:59-05:00 fix let declaration merging - - - - - 0119ea77 by Pierre Delaunay at 2016-02-26T17:38:56-05:00 lexp PCall handling - - - - - bb2cbbd5 by Pierre Delaunay at 2016-02-26T23:14:40-05:00 cleaning - - - - - 62596a77 by Pierre Delaunay at 2016-02-27T12:16:56-05:00 merging - - - - - 29 changed files: - .gitignore - GNUmakefile - + TODO.md - + _tags - + doc/Compiler Structure.md - + samples/debug_test.typer - samples/lexer_test.typer - + samples/lexp_test.typer - src/pervasive.typer → samples/pervasive.typer - − samples/pexp_test.typer - − samples/token_test.typer - + src/debruijn.ml - src/fmt.ml - tests/primary_debug.ml → src/grammar.ml - src/lexp.ml - + src/lparse.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - src/util.ml - + tests/debruijn_test.ml - tests/debug.ml - − tests/dummy1_test.ml - − tests/dummy2_test.ml - − tests/dummy_test.ml - + tests/full_debug.ml - − tests/lexer_debug.ml - − tests/prelexer_debug.ml - tests/utest_main.ml Changes: ===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -12,6 +12,7 @@ typer *.aux manual.?? *.info -_build/ +*_build/ *~ #*# +test__.ml ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -1,26 +1,28 @@ RM=rm -f TEST_FILES := $(wildcard ./tests/*_test.ml) +# This is for windows: Make windows version is old +ifeq ($(OS),Windows_NT) +SHELL=C:/Windows/System32/cmd.exe +endif all: typer debug tests typer: - ocamlbuild src/main.byte + ocamlbuild src/main.byte -cflag -rectypes mv _build/src/main.byte _build/typer # move and rename executable debug: - ocamlbuild tests/prelexer_debug.byte -I src # debug print - mv _build/tests/prelexer_debug.byte _build/prelexer_debug - ocamlbuild tests/lexer_debug.byte -I src # debug print - mv _build/tests/lexer_debug.byte _build/lexer_debug + ocamlbuild tests/full_debug.native -I src -cflag -rectypes + mv _build/tests/full_debug.native _build/full_debug tests: # Build tests - $(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.byte,$(test))) -I src;) + $(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.native,$(test))) -I src -cflag -rectypes;) # Run tests - ocamlbuild tests/utest_main.byte - ./_build/tests/utest_main.byte + ocamlbuild tests/utest_main.native + ./_build/tests/utest_main.native # Make language doc doc-tex: ===================================== TODO.md ===================================== --- /dev/null +++ b/TODO.md @@ -0,0 +1,31 @@ +TODO +==== + +PROJECT: + * pretty arg parsing utils + +FILE: full_debug.ml + * better arg parsing + * Allow users to choose what to print (Pretoks/Sexp/SexpNode/Pexp/Lexp/etc..) + * --all + * --pretoks + * --sexp + * --node + * --pexp + * --lexp + + Other Option + --repl + + +case (a,b) + | (Foo, Foo) => 3.14 + | (Bar, Bar) => 3.15 +;; + + + +# Issues + +* The duplicate ';' create Sexp::Epsilon() which makes pexp_parse fail +* pexp_parse fail to parse inductive ===================================== _tags ===================================== --- /dev/null +++ b/_tags ===================================== doc/Compiler Structure.md ===================================== --- /dev/null +++ b/doc/Compiler Structure.md @@ -0,0 +1,56 @@ +Stream.of_string + +Typer Compiler Structure +======================== + +Read tests/full_debug.ml for ocaml usage + + +* in_channel -> PreLexer: PreToken + + Skips Blocks and identifies Strings + + Blocks : {this is a block} + String : "this is a string" + PreToken: a pretoken is everything else + + Function: + prelex_file file + + TODO: + prelex_str "my code" + +* PreToken -> Lexer: Sexp + + Process PreToken. Cut them in smaller pieces according to [stt : token_env] + For example: + + Code: "a => 3;" + + Pretoken: ['a', '=>', '3;'] + + Lexer ['a', '=>', '3;'] => ['a', '=>', '3', ';'] + + Here ';' is in stt which makes the '3;' pretoken to explode in two. + + Function: + lex stt pretoken + +* Sexp -> sexp_parse: Sexp + + Group Sexp into Nodes according to the specified grammar. + Create the program tree. + + Code: "a => 3;" + + Pretoken: ['a', '=>', '3;'] + + Lexer ['a', '=>', '3;'] => ['a', '=>', '3', ';'] (Sexp) + + sexp_parse ['a', '=>', '3', ';'] + => Node('_=>_', ['a', '3']) + + Function: + sexp_parse sexp + +* Sexp -> Lexp \ No newline at end of file ===================================== samples/debug_test.typer ===================================== --- /dev/null +++ b/samples/debug_test.typer @@ -0,0 +1,41 @@ +% +% Pexp Debugging: Everything must work +% This is not meant to be correct Typer input +% + +{a => "This is a block"}; % Pimm: Block +"This is a String"; % Pimm: String +12; % Pimm: Integer +12.12; % Pimm: Float + +% Pvar +ab; + +% let_in +let a = b in + c = b +; + +% PCall +(function arg1 arg2 arg3); + +% Parrow +a -> 1; +a => 2; +a ≡> 1; + +% Lambda +a = lambda (x, y) -> x + y; +b = lambda (x, y) => x * y; +c = lambda (x, y) ≡> x / y; + +% case +case (a, b) + | (1, 2) => 1 + | (_, _) => 3 +; + +% inductive +% Nat : Type +Type = inductive_ (Type_Label) (zero) (succ Type); +inductive_ (Type_Label) (zero) (succ Type); \ No newline at end of file ===================================== samples/lexer_test.typer ===================================== --- a/samples/lexer_test.typer +++ b/samples/lexer_test.typer @@ -4,36 +4,30 @@ %% ---------------- %% String -a = "The answer is 42"; +a => "The answer is 42"; %% Integer -b = 11; +b => 11; %% Float -c = 3.14; +c => 3.14; %% Something -C = 3.14.14; - +C => 3.14.14; %% Case +%% ---------------- case (a,b) - | (Foo,Foo) => 3.14 - | (Bar,Bar) => 3.15 -;; + | (Foo, Foo) => 3.14 + | (Bar, Bar) => 3.15 +; %% Stuff %% ---------------- -%% Epsilon - %% Block - - -%% Node -%% -> Composed expression - -%% Symbol -%% --> Everything else +{ + a => "This is a Block"; +} \ No newline at end of file ===================================== samples/lexp_test.typer ===================================== --- /dev/null +++ b/samples/lexp_test.typer @@ -0,0 +1,62 @@ +ab; + +% Type is read as a Pvar ????? +add = lambda (a : Type) -> lambda (b : Type) -> (add a b); + +% How typer is supposed to read this +p:int -> int; + +% this is a call to _=_ +odd n = case n | 0 => false | S n' => even (n'); + +% +% Here we test that two declaration with different +% name are EXACLTY equivalent in the eyes +% of the compiler +% +% Declaration order STILL MATTERS +% + +% let +let a:Nat; d:Nat; c:Nat; b:Nat; + a = b; + d = a; + c = d; + b = c; + in a + b + c + d +; + +% let: Different naming +let e:Nat; f:Nat; g:Nat; h:Nat; + e = h; + f = e; + g = f; + h = g; + in e + h + g + f +; + +% let: Different Ordering +let b:Nat; c:Nat; d:Nat; a:Nat; + c = d; + d = a; + b = c; + a = b; + in a + b + c + d +; + +% +% Recursivity detection +% + +let odd: (int -> int); + even: (int -> int); + odd n = case n | 0 => false | S n' => even (n'); + even n = case n | 0 => true | S n' => odd (n'); + in a + b; + + +% Do I consider functions as variable ?? Yes + + + + ===================================== src/pervasive.typer → samples/pervasive.typer ===================================== --- a/src/pervasive.typer +++ b/samples/pervasive.typer ===================================== samples/pexp_test.typer deleted ===================================== --- a/samples/pexp_test.typer +++ /dev/null @@ -1,50 +0,0 @@ -%% -%% Proto lambda-expressions, half-way between Sexp and Lexp. -%% - -%% ppat -%% ----------------- - -%% Ppatany - -%% Ppatvar - -%% Ppatcons - - -%% pexp -%% ----------------- - -%% Pimm -%% - -%% Pvar -%% - -%% Phastype -%% - -%% Pmetavar -%% - -%% Plet -%% - -%% Parrow -%% - -%% Plambda -%% - -%% Pcall -%% - -%% Pinductive -%% - -%% Pcons -%% - -%% Pcase -%% - ===================================== samples/token_test.typer deleted ===================================== --- a/samples/token_test.typer +++ /dev/null @@ -1,28 +0,0 @@ -%% This file check if typer recognize correctly tokens - -%% builtin types -%% ---------------- - -%% String -a = "The answer is 42"; - -%% Integer -b = 11; - -%% Float -c = 3.14; - - -%% Stuff -%% ---------------- - -%% Epsilon - -%% Block - - -%% Node -%% -> Composed expression - -%% Symbol -%% --> Everything else ===================================== src/debruijn.ml ===================================== --- /dev/null +++ b/src/debruijn.ml @@ -0,0 +1,196 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * --------------------------------------------------------------------------- + * + * Description: + * Specifies recursive data structure for DeBruijn indexing + * methods starting with '_' are considered private and should not + * elsewhere in the project + * + * Methods: + * make_context : make an empty context + * add_scope ctx : add new scope to the current context + * find_var name ctx: return the index of the variable 'name' + * add_variable name loc ctx : add a variable to the current context + * + * TODO: + * ADD meyers list <index -> (type, name?)> + * + * ---------------------------------------------------------------------------*) + +open Util + +let debruijn_error = msg_error "DEBRUIJN" +let debruijn_warning = msg_warning "DEBRUIJN" + +(* Type definitions + * ---------------------------------- *) + +(* This exist because I don't want that file to depend on anything *) +module StringMap + = Map.Make (struct type t = string let compare = String.compare end) +;; + +(* Map matching variable name and its distance in the current scope *) +type scope = (int) StringMap.t (* Map<String, int>*) + +(* Offset is the number to take us out of the inner scope + * Scope is the Mapping between Variable's names and its current index loc + * Offset + Scope *) +type context_impl = int * scope + +(* The recursive type that does everything + * inner Scope * Outer Scope *) +type lexp_context = context_impl * lexp_context option + + +(* internal definitions: DO NOT USE + * ---------------------------------- *) + +let _make_scope = StringMap.empty;; +let _make_context_impl = (0, _make_scope);; + +let _get_inner_ctx (ctx: lexp_context) = + match ctx with + | (ct, _) -> ct +;; + +let _get_inner_scope (ctx: lexp_context): scope = + let ictx = _get_inner_ctx ctx in + match ictx with + | (_, scope) -> scope +;; + +(* get current offset *) +let _get_offset (ctx: lexp_context): int = + let inner = _get_inner_ctx ctx in + match inner with + | offset, _ -> offset +;; + +(* increase the offset *) +let _inc_offset (ctx: lexp_context): lexp_context = + (* Because using ref is hell, we make a copy *) + match ctx with + | ((offset, scope), None) -> ((offset + 1, scope), None) + | ((offset, scope), Some outter) -> ((offset + 1, scope), Some outter) +;; + +(* Increase the indexes of all inner variables *) +let _inc_index (ctx: lexp_context): lexp_context = + let ((offset, scope), otr) = ctx in + let scope = StringMap.map (fun value -> value + 1) scope in + ((offset, scope), otr) +;; + +(* Public methods: DO USE + * ---------------------------------- *) + +(* return its current DeBruijn index + * return -1 if the variable does not exist + * return closest variable *) +let rec find_var (name: string) (ctx: lexp_context) = + (* Search *) + let local_index = find_local name ctx in + if local_index >= 0 then + local_index + else + begin + let outter_index = _find_outer name ctx in + if outter_index >= 0 then + outter_index + (_get_offset ctx) + else + -1 + end + +and find_local (name: string) (ctx: lexp_context): int = + try + let inner = _get_inner_scope ctx in + StringMap.find name inner + with + Not_found -> -1 + +(* You should not use this function 'find_var' is the way + * the reason is _find_outer does not send back a correct index *) +and _find_outer (name: string) (ctx: lexp_context): int = + match ctx with + | (_, Some ct) -> (find_var name ct) + | _ -> -1 +;; + +(* Alias *) +let get_var_index name ctx = find_var name ctx;; + +let add_variable name loc ctx = + (* I think this should be illegal *) + let local_index = find_local name ctx in + if local_index >= 0 then (* This is the index not the number of element *) + debruijn_warning loc ("Variable Redefinition: " ^ name); + + let outer_index = _find_outer name ctx in + if outer_index >= 0 then + debruijn_warning loc ("Variable Shadowing: " ^ name); + + (* Increase distance *) + let scope = StringMap.map (fun value -> value + 1) (_get_inner_scope ctx) in + (* Add new Value *) + let new_scope = StringMap.add name 0 scope in + (* build new context *) + match ctx with + | ((offset, _), None) + -> ((offset + 1, new_scope), None) + | ((offset, _), Some outter) + -> ((offset + 1, new_scope), Some outter) +;; + +(* Make a Global context *) +let make_context = (_make_context_impl, None);; + +(* Make a new Scope inside the outer context 'ctx' *) +let add_scope ctx = (_make_context_impl, Some ctx);; + +(* Print Functions for testing *) +let print_scope (scp: scope) (offset: int): unit = + StringMap.iter + (fun key value + -> print_string (key ^ "\t"); + print_int (value + offset); + print_string "\n") + scp +;; + +let print_lexp_context (ctx: lexp_context): unit = + print_string " Context Print\n"; + + let rec impl (ctx2: lexp_context) (offset: int) = + let inner = _get_inner_scope ctx2 in + match ctx2 with + | (_, Some ct) + -> impl ct ((_get_offset ctx2) + offset); + (print_scope inner offset); + | _ -> (print_scope inner offset) in + (impl ctx 0) +;; \ No newline at end of file ===================================== src/fmt.ml ===================================== --- a/src/fmt.ml +++ b/src/fmt.ml @@ -1,20 +1,34 @@ (* - * Kiwi Compiler - * - * Pierre Delaunay + * Typer Compiler * - * --------------------------------------------------------------------------- + * --------------------------------------------------------------------------- * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. * - *) - - -(****************************************************************************** - * Print helper + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. * - * Declare new print function which align printed values. + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. * - *****************************************************************************) + * --------------------------------------------------------------------------- + * + * Description: + * Declare new print function which align printed values. + * + * ---------------------------------------------------------------------------*) (* Compute the number of character needed to print an integer*) let str_size_int value = @@ -47,3 +61,30 @@ let lalign_print_string str nb = print_string str; make_line " " (nb - String.length str); ;; + +(* print n char 'c' *) +let rec prerr_make_line c n = + prerr_string c; + if n >= 1 then (make_line c (n - 1)); +;; + +(* print an integer right-aligned *) +let ralign_prerr_int value nb = + prerr_make_line " " (nb - (str_size_int value)); + prerr_int value; +;; + +let lalign_prerr_int value nb = + prerr_int value; + prerr_make_line " " (nb - (str_size_int value)); +;; + +let ralign_prerr_string str nb = + prerr_make_line " " (nb - String.length str); + prerr_string str; +;; + +let lalign_prerr_string str nb = + prerr_string str; + prerr_make_line " " (nb - String.length str); +;; ===================================== tests/primary_debug.ml → src/grammar.ml ===================================== --- a/tests/primary_debug.ml +++ b/src/grammar.ml @@ -5,7 +5,7 @@ * * Copyright (C) 2011-2016 Free Software Foundation, Inc. * - * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Author: Stefan Monnier <monnier(a)iro.umontreal.ca> * Keywords: languages, lisp, dependent types. * * This file is part of Typer. @@ -26,108 +26,62 @@ * --------------------------------------------------------------------------- * * Description: - * print out read pexp (primary expression) + * Define the default Typer Grammar * * --------------------------------------------------------------------------- *) - -let rec debug_pexp_print pexp = - match pexp with - | Pimm(exp) - -> - | Pvar(p) - -> - | Phastype(l, exp2, exp1) - -> -;; +(* FIXME: it should be possible to make something like "." bind tighter than + function application. *) +(* FIXME: what about sections, as in "if_then e1 else_"? *) -let debug_pexp_print_all pexp = - List.iter (fun pt -> - print_string " "; - debug_pexp_print pt; - print_string "\n"; - ) - pexp -;; -(* Language config *) +module SMap + = Map.Make (struct type t = string let compare = String.compare end) + +type grammar = (int option * int option) SMap.t let default_stt = - let stt = Array.create 256 false + let stt = Array.make 256 false in stt.(Char.code ';') <- true; stt.(Char.code ',') <- true; stt.(Char.code '(') <- true; stt.(Char.code ')') <- true; stt -;; - -let default_grammar : grammar - = List.fold_left (fun g (n, ll, rl) -> SMap.add n (ll, rl) g) - SMap.empty - [("^", Some 171, Some 159); - ("/", Some 148, Some 160); - ("-", Some 92, Some 110); - ("+", Some 93, Some 111); - ("!=", Some 94, Some 75); - (">=", Some 95, Some 76); - ("<=", Some 96, Some 77); - (">", Some 97, Some 78); - ("<", Some 98, Some 79); - ("&&", Some 64, Some 81); - ("||", Some 39, Some 51); - (",", Some 26, Some 26); - ("then", Some 1, Some 0); - ("=", Some 99, Some 80); - ("type", None, Some 27); - (";", Some 15, Some 15); - ("*", Some 137, Some 137); - (":", Some 173, Some 115); - ("]", Some 3, None); - ("->", Some 126, Some 114); - ("=>", Some 126, Some 113); - ("≡>", Some 126, Some 112); - ("in", Some 2, Some 53); - ("else", Some 0, Some 52); - ("|", Some 40, Some 40); - (")", Some 4, None); - ("[", None, Some 3); - ("case", None, Some 28); - ("lambda", None, Some 126); - ("letrec", None, Some 2); - ("let", None, Some 2); - ("if", None, Some 1); - ("(", None, Some 4); - ] -;; - -let main filename () = - - (* Todo read file from prog args *) - (* get pretokens*) - let pretoks = prelex_file filename in - - (* get sexp/tokens *) - let toks = lex default_stt pretoks in - - (* get pexp *) - let pxp = sexp_parse_all grm toks limit in - - (* print pxp *) - debug_pexp_print_all pxp -;; - -(* Command Line *) -open Core.Std - -let command = - Command.basic - ~summary:"Print Compiler Debug Info" - ~readme:(fun () -> "More detailed information") - Command.Spec.(empty +> anon ("filename" %: string)) - main - -let () = - Command.run ~version:"1.0" ~build_info:"RWO" command - - - + +let default_grammar : grammar = + List.fold_left (fun g (n, ll, rl) -> SMap.add n (ll, rl) g) + SMap.empty + [("^", Some 171, Some 159); + ("/", Some 148, Some 160); + ("-", Some 92, Some 110); + ("+", Some 93, Some 111); + ("!=", Some 94, Some 75); + (">=", Some 95, Some 76); + ("<=", Some 96, Some 77); + (">", Some 97, Some 78); + ("<", Some 98, Some 79); + ("&&", Some 64, Some 81); + ("||", Some 39, Some 51); + (",", Some 26, Some 26); + ("then", Some 1, Some 0); + ("=", Some 99, Some 80); + ("type", None, Some 27); + (";", Some 15, Some 15); + ("*", Some 137, Some 137); + (":", Some 173, Some 115); + ("]", Some 3, None); + ("->", Some 126, Some 114); + ("=>", Some 126, Some 113); + ("=>", Some 126, Some 112); + ("in", Some 2, Some 53); + ("else", Some 0, Some 52); + ("|", Some 40, Some 40); + (")", Some 4, None); + ("[", None, Some 3); + ("case", None, Some 28); + ("lambda", None, Some 126); + ("letrec", None, Some 2); + ("let", None, Some 2); + ("if", None, Some 1); + ("(", None, Some 4); + ] \ No newline at end of file ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -25,6 +25,7 @@ open Lexer open Sexp open Pexp open Myers +open Grammar (* open Unify *) (*************** DeBruijn indices for variables *********************) @@ -52,6 +53,7 @@ type builtin = | EqType | LevelType + type ltype = lexp and lexp = | Imm of sexp (* Used for strings, ... *) @@ -75,6 +77,7 @@ type ltype = lexp * ltype (* The base inductive type over which we switch. *) * (location * (arg_kind * vdef) option list * lexp) SMap.t * lexp option (* Default. *) + | UnknownType of location (* This is easy to handle *) (* | Susp of subst * lexp * (\* For logical metavars, there's no substitution. *\) * | Metavar of (location * string) * metakind * metavar ref @@ -188,7 +191,8 @@ let builtins = * includes "younger" bindings. *) -type env_elem = (db_offset, vdef, lexp option, ltype) + +type env_elem = (db_offset * vdef * lexp option * ltype) type env_type = env_elem myers let env_lookup_type (env : env_type) (v : vref) = let ((_, rname), dbi) = v in @@ -510,6 +514,7 @@ let conv_erase = true (* If true, conv ignores erased terms. *) * decls1 decls2 * | (_, _) -> false *) +(* (* In non-recursion calls, `s' is always empty. *) let lexp_conv_p env = lexp_conv_p env VMap.empty @@ -576,11 +581,93 @@ and lexp_unparse e : pexp = (* (internal_error "Can't print a Susp") *) let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) - +<<<<<<< HEAD + +(* let rec lexp_type (env: (lexp option * lexp) VMap.t) e : lexp = + * let rec follow e = + * match e with + * | Var (_,v) -> vmap_getval v + * | Metavar (_,_,r) -> (match !r with MetaSet e -> follow e | _ -> e) + * | _ -> e + * and vmap_getval (v : var) = + * match VMap.find v env with (Some e, _) -> follow e + * | _ -> Var (dummy_location, v) in + * match e with + * | Sort (l, Stype e) -> Sort (l, Stype (SortLevel (SLsucc e))) + * | Sort (l, StypeOmega) + * -> msg_error l "TypeΩ doesn't have a type"; mk_meta_dummy env l + * | Sort (l, StypeLevel) + * -> msg_error l "TypeLevel doesn't have a type"; mk_meta_dummy env l + * | SortLevel _ -> Sort (lexp_location e, StypeLevel) + * | Imm (Integer _) -> type_int + * | Imm (Float _) -> type_float + * | Builtin (_,_,t) -> t + * (\* | Imm (String _) -> Var (dummy_location, var_string) *\) + * | Imm s -> let l = sexp_location s in + * msg_error l "Unrecognized sexp in lexp"; mk_meta_dummy env l + * | Var (_,name) -> snd (VMap.find name env) + * | Let (l, decls, body) -> + * lexp_type (List.fold_left (fun env ((_,v),e,t) -> + * VMap.add v (Some (Let (l, decls, e)), t) env) + * env decls) + * body + * | Arrow _ -> type0 (\* FIXME! *\) + * | Lambda (ak, ((l,v) as var),t,e) -> + * Arrow (ak, Some var, t, dummy_location, + * lexp_type (VMap.add v (None, t) env) e) + * | Call (f, args) -> + * let ft = lexp_type env f in + * let rec one_arg t (_,arg) = + * match lexp_whnf VMap.empty t with + * | Arrow (_, None, t1, _, t2) -> t2 + * | Arrow (_, Some (_,v), t1, _, t2) -> + * Susp (VMap.add v arg VMap.empty, t2) + * | _ -> msg_error (lexp_location arg) "Too many arguments"; t + * in List.fold_left one_arg ft args + * | Inductive (_,t,_) -> t + * | Cons (e,(l,name)) -> + * (match lexp_whnf VMap.empty e with + * | Inductive (_,_,branches) -> + * (try SMap.find name branches + * with Not_found -> msg_error l ("No such constructor name `"^name^"'"); + * mk_meta_dummy env l) + * | _ -> msg_error l "The constructor refers to a non-inductive type"; + * mk_meta_dummy env l) + * | Case (_,_,_,_,Some default) -> lexp_type env default + * (\* | Case (_,_,(_,i, args, branch) :: _,_) -> + * * let ct = lexp_type env (vmap_getval cv) in + * * let rec one_arg (t,env) argo = + * * match t with + * * | Arrow (_, None, t1, _, t2) -> + * * (t2, VMap.add (snd argo) (None, t1) env) + * * | Arrow (_, Some (l,v), t1, _, t2) -> + * * (Susp (VMap.add v (mk_meta_dummy l) VMap.empty, t2), + * * VMap.add (snd argo) (None, t1) env) + * * | Susp (s, Arrow (ak,v,t1,l,t2)) -> + * * one_arg (Arrow (ak, v, Susp (s, t1), l, Susp (s, t2)), env) argo + * * | _ -> msg_error (fst argo) "Too many arguments"; + * * (t, VMap.add (snd argo) + * * (None, mk_meta_dummy (fst argo)) + * * env) + * * in let (_,env') = List.fold_left one_arg (ct,env) args + * * in lexp_type env' branch *\) + * | Case (l,_,_,_,None) -> mk_meta_dummy env l (\* Dead code? *\) + * | Susp (s, e) -> lexp_type env (lexp_whnf s e) + * | Metavar ((l,_),_,r) + * -> match !r with MetaSet e -> lexp_type env e + * | MetaUnset (_, Some t, _) -> t + * | _ -> msg_error l "Uninstantiated metavar of unknown type"; + * mk_meta_dummy env l *) + +(* +let rec lexp_parse (p : pexp) (env : (vdef * lexp option * ltype) myers) = *) +*) + +(* FIXME type senv_type = (db_revindex SMap.t * db_index) let senv_lookup senv s : db_index = let (m, i) = senv in - i - SMap.find s senv + i - SMap.find s senv *) (* Parsing a Pexp into an Lexp is really "elaboration", i.e. it needs to * infer the types and perform macro-expansion. For won't really @@ -598,7 +685,10 @@ let senv_lookup senv s : db_index = * - use lexp_p_infer for destructors, and use lexp_p_check for constructors. * - use lexp_p_check whenever you can. *) -let rec lexp_p_infer (env : env_type) (p : pexp) : lexp * ltype = ? + +let rec lexp_p_infer (env : env_type) (p : pexp) : lexp * ltype = + (UnknownType(dummy_location), UnknownType(dummy_location)) + and lexp_p_check (env : env_type) (p : pexp) (t : ltype) : lexp = match p with | _ ===================================== src/lparse.ml ===================================== --- /dev/null +++ b/src/lparse.ml @@ -0,0 +1,297 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * --------------------------------------------------------------------------- + * + * Description: + * parse pexp expression into lexp + * + * --------------------------------------------------------------------------- *) + +open Util +open Sexp +open Pexp +open Lexp +open Grammar +open Debruijn +open Fmt + +(* Shortcut => Create a Var *) +let make_var name index loc = + Var(((loc, name), index)) +;; + +let not_implemented_error () = + internal_error "not implemented" +;; + +let lexp_error = msg_error "LEXP" +let lexp_warning = msg_warning "LEXP" + +(* Vdef is exactly similar to Pvar but need to modify our ctx *) +let pvar_to_vdef p = + p +;; +(* PEXP is not giving SEXP types this is why types are always unknown *) + +(* + * The main job of lexp (currently) is to determine variable name (index) + * and to regroup type specification with their variable + *) + +let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = + (* So I don't have to extract it *) + let tloc = pexp_location p in + match p with + (* Block/String/Integer/Float *) + | Pimm value -> Imm(value), ctx + + (* Symbol i.e identifier /!\ A lot of Pvar are not variables /!\ *) + | Pvar (loc, name) -> + let idx = get_var_index name ctx in + (* This should be an error but we accept it for debugging *) + if idx < 0 then + lexp_warning tloc ("Variable: '" ^ name ^ "' does not exist"); + (make_var name (idx + 1) loc), ctx; + + (* Let, Variable declaration + local scope *) + | Plet(loc, decls, body) -> (* /!\ HERE *) + let decl, nctx = lexp_parse_let decls (add_scope ctx) in + let bdy, nctx = lexp_parse body nctx in + (* print_lexp_context nctx; *) + (* Send back old context as we exit the inner scope *) + Let(tloc, decl, bdy), ctx + + (* ->/=> *) + | Parrow (kind, Some var, tp, loc, expr) -> + let nvar = pvar_to_vdef var in (* /!\ HERE *) + let ltyp, ctx = lexp_parse tp ctx in + let lxp, ctx = lexp_parse expr ctx in + Arrow(kind, Some nvar, ltyp, tloc, lxp), ctx + + | Parrow (kind, None, tp, loc, expr) -> + let ltyp, ctx = lexp_parse tp ctx in + let lxp, ctx = lexp_parse expr ctx in + Arrow(kind, None, ltyp, tloc, lxp), ctx + + (* *) + | Plambda (kind, var, Some ptype, body) -> + let nvar = pvar_to_vdef var in (* /!\ HERE *) + let ltyp, ctx = lexp_parse ptype ctx in + let lbody, ctx = lexp_parse body ctx in + Lambda(kind, nvar, ltyp, lbody), ctx + + | Plambda (kind, var, None, body) -> + let nvar = pvar_to_vdef var in (* /!\ HERE *)(* /!\ Missing Type *) + let lbody, ctx = lexp_parse body ctx in + Lambda(kind, nvar, UnknownType(tloc), lbody), ctx + + (* Function Call *) + | Pcall (fname, _args) -> + let fname, ctx = lexp_parse fname ctx in + let pargs = pexp_parse_all _args in + let largs, fctx = lexp_parse_all pargs ctx in + + (* Make everything explicit for now *) + let new_args = List.map (fun g -> (Aexplicit, g)) largs in + + Call(fname, new_args), ctx + + (* Pcons *) + (* Pcase *) + (* Pinductive *) (* Pinductive Pexp implementation is not ready *) + + | _ + -> UnknownType(tloc), ctx + + +and lexp_parse_let decls ctx = + + (* Merge Type info and declaration together *) + (* We use a list because order matters and Maps reorder elements *) + let rec is_equal target (p:(vdef * pexp option * pexp option)): bool = + let ((_, name), _, _) = p in + if name == target then true else false in + + let rec loop (decls: (pvar * pexp * bool) list) merged: + (vdef * pexp option * pexp option) list = + + (* we cant evaluate here because variable are not in the environment *) + match decls with + | [] -> List.rev merged + | hd::tl -> + match hd with + (* Type Info: Var:Type *) + | ((loc, name), type_info, true) -> begin + try + (* If found its means the instruction was declared + * before the type info. Should we allow this? *) + let (vd, inst, _) = List.find (is_equal name) merged in + let new_decl = (vd, inst, Some type_info) in + (loop tl (new_decl::merged)) + with Not_found -> + let new_decl = (loc, name), None, Some type_info in + (loop tl (new_decl::merged)) end + + (* Instruction: Var = expr *) + | ((loc, name), inst, false) -> begin + try + let (vd, _, ptyp) = List.find (is_equal name) merged in + let new_decl = (vd, Some inst, ptyp) in + (loop tl (new_decl::merged)) + with Not_found -> + let new_decl = ((loc, name), Some inst, None) in + (loop tl (new_decl::merged)) end in + + let decls = loop decls [] in + + (* Add Each Variable to the environment *) + let rec add_var_env decls ctx = + match decls with + | [] -> ctx + | hd::tl -> begin + match hd with + (* Unused variable: No Instruction *) + (* Warning will be printed later *) + | ((loc, name), None, _) -> add_var_env tl ctx + | ((loc, name), _, _) -> + let ctx = add_variable name loc ctx in + add_var_env tl ctx end in + + let nctx = add_var_env decls ctx in + + (* lexp_parse instruction and types *) + let rec parse_decls decls ctx acc = + match decls with + | [] -> (List.rev acc), ctx + | hd::tl -> begin + match hd with + | ((loc, name), Some pinst, Some ptype) -> + let linst, nctx = lexp_parse pinst ctx in + let ltyp, nctx = lexp_parse ptype nctx in + let nacc = ((loc, name), linst, ltyp)::acc in + (parse_decls tl nctx nacc) + | ((loc, name), Some pinst, None) -> + let linst, nctx = lexp_parse pinst ctx in + (* This is where UnknownType are introduced *) + (* need Inference HERE *) + let nacc = ((loc, name), linst, UnknownType(loc))::acc in + (parse_decls tl nctx nacc) + (* Skip the variable *) + | ((loc, name), None, _) -> + lexp_warning loc "Unused Variable"; + (parse_decls tl ctx acc) + end in + + parse_decls decls nctx [] + +and lexp_parse_all (p: pexp list) (ctx: lexp_context): + (lexp list * lexp_context) = + let rec loop (plst: pexp list) ctx (acc: lexp list) = + match plst with + | [] -> ((List.rev acc), ctx) + | _ -> let lxp, new_ctx = lexp_parse (List.hd plst) ctx in + (loop (List.tl plst) new_ctx (lxp::acc)) in + (loop p ctx []) +;; + +(* Print back in CET (Close Enough Typer) easier to read *) + (* pretty ? * indent level * print_type? *) +type print_context = (bool * int * bool) + +let rec lexp_print_adv opt exp = + let slexp_print = lexp_print_adv opt in (* short_lexp_print *) + let (pty, indent, prtp) = opt in + match exp with + | Imm(value) -> sexp_print value + | Var ((loc, name), idx) -> + print_string name; + if idx > 0 then begin + print_string "("; print_int idx; print_string ")"; end + + | Let (_, decls, body) -> + print_string "let"; lexp_print_decls (pty, indent + 1, prtp) decls; + if pty then make_line " " (indent * 4 + 4); + print_string " in "; lexp_print_adv (pty, indent + 2, prtp) body + + | Arrow(kind, Some (_, name), tp, loc, expr) -> + slexp_print tp; print_string ": "; print_string name; + print_string " -> "; slexp_print expr; + + | Arrow(kind, None, tp, loc, expr) -> + slexp_print tp; print_string " -> "; slexp_print expr; + + | Lambda(kind, (loc, name), ltype, lbody) -> + print_string "lambda ("; print_string (name ^ ": "); + slexp_print ltype; print_string ") -> "; slexp_print lbody; + + | Call(fname, args) -> begin (* /!\ Partial Print *) + (* get function name *) + let str = match fname with + | Var((_, name), _) -> name + | _ -> "unkwn" in + + let print_arg arg = match arg with | (kind, lxp) -> + lexp_print_adv (pty, 0, prtp) lxp in + + let print_binop op lhs rhs = + print_arg lhs; print_string op; print_arg rhs in + + match (str, args) with + (* Special Operator *) + | ("_=_", [lhs; rhs]) -> print_binop " = " lhs rhs + | ("_+_", [lhs; rhs]) -> print_binop " + " lhs rhs + | ("_-_", [lhs; rhs]) -> print_binop " - " lhs rhs + | ("_/_", [lhs; rhs]) -> print_binop " / " lhs rhs + | ("_*_", [lhs; rhs]) -> print_binop " * " lhs rhs + (* not an operator *) + | _ -> + print_string ("(" ^ str); + List.iter (fun arg -> print_string " "; print_arg arg) args; + print_string ")" end + + (* debug catch all *) + | UnknownType (loc) -> print_string "unkwn"; + | _ -> print_string "expr" + +and lexp_print_decls opt decls = + let (pty, indent, prtp) = opt in + let print_type nm tp = + print_string (" " ^ nm ^ ": "); lexp_print_adv opt tp; + print_string ";"; in + + List.iteri (fun idx g -> match g with + | ((loc, name), expr, ltyp) -> + if pty && idx > 0 then make_line " " (indent * 4); + if prtp then print_type name ltyp; print_string " "; + print_string (name ^ " = "); + lexp_print_adv opt expr; print_string ";"; + if pty then print_string "\n") + decls +;; + + +let lexp_print = lexp_print_adv (false, 0, true) + ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -23,9 +23,13 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util open Sexp +let pexp_error = msg_error "PEXP" + (*************** The Pexp Parser *********************) type arg_kind = Aexplicit | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) + +(* This is Dangerously misleading since pvar is NOT pexp but Pvar is *) type pvar = symbol (* type sort = Type | Ext *) (* type tag = string *) @@ -94,7 +98,7 @@ let rec pexp_parse (s : sexp) : pexp = | Node (Symbol (start, "let_in_"), [decls; body]) -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) - -> msg_error start "Unrecognized let expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized let expression"; Pmetavar (start, "_") (* arrow *) | Node (Symbol (start, (("_->_" | "_=>_" | "_≡>_") as arw)), [t1; t2]) -> let kind = (match arw with @@ -104,7 +108,7 @@ let rec pexp_parse (s : sexp) : pexp = -> Parrow (kind, Some v, pexp_parse t1, start, pexp_parse t2) | _ -> Parrow (kind, None, pexp_parse t1, start, pexp_parse t2)) | Node (Symbol (start, ("_->_" | "_=>_" | "_≡>_")), _) - -> msg_error start "Unrecognized arrow expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized arrow expression"; Pmetavar (start, "_") (* lambda *) | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), [arg; body]) @@ -117,37 +121,38 @@ let rec pexp_parse (s : sexp) : pexp = | Symbol v -> (v, None) | Node (Symbol (_, "_:_"), [Symbol v; t]) -> (v, Some (pexp_parse t)) - | _ -> msg_error start "Unrecognized lambda argument"; + | _ -> pexp_error start "Unrecognized lambda argument"; ((dummy_location, "unrecognized_arg"), None) in Plambda (kind, v, t, pbody)) (sexp_p_list arg ["_:_"]) (pexp_parse body) | Node (Symbol (start, "lambda_"), _) - -> msg_error start "Unrecognized lambda expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized lambda expression"; Pmetavar (start, "_") (* inductive type *) | Node (Symbol (start, "inductive_"), t :: cases) -> let (name, args) = match t with - | Node (Symbol s, args) -> (s, args) - | Symbol s -> (s, []) - | _ -> msg_error start "Unrecognized inductive type name"; + | Node (Symbol s, args) -> (s, args) (* This a constructor *) + | Symbol s -> (s, []) (* This is a Label *) + | _ -> pexp_error start "Unrecognized inductive type name"; ((dummy_location, ""), []) in let pcases = List.fold_right (fun case pcases -> match case with - | Node (Symbol s, cases) + (* read Constructor name + args => Type ((Symbol * args) list) *) + | Node (Symbol s, cases) -> (s, List.map pexp_p_ind_arg cases)::pcases - | _ -> msg_error (sexp_location case) + | _ -> pexp_error (sexp_location case) "Unrecognized constructor declaration"; pcases) cases [] in Pinductive (name, List.map pexp_p_formal_arg args, pcases) | Node (Symbol (start, "inductive_"), _) - -> msg_error start "Unrecognized inductive type"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized inductive type"; Pmetavar (start, "_") (* constructor *) | Node (Symbol (start, "inductive-cons"), [Symbol tname; Symbol tag]) -> Pcons (tname, tag) | Node (Symbol (start, "cons_"), _) - -> msg_error start "Unrecognized constructor call"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized constructor call"; Pmetavar (start, "_") (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -155,12 +160,12 @@ let rec pexp_parse (s : sexp) : pexp = | Node (Symbol (_, "_=>_"), [pat; code]) -> (pexp_p_pat pat, pexp_parse code) | _ -> let l = (sexp_location branch) in - msg_error l "Unrecognized simple case branch"; + pexp_error l "Unrecognized simple case branch"; (Ppatany l, Pmetavar (l, "_")) in Pcase (start, pexp_parse e, List.map parse_case cases) | Node (Symbol (start, "case_"), [e]) -> Pcase (start, pexp_parse e, []) | Node (Symbol (start, "case_"), _) - -> msg_error start "Unrecognized case expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized case expression"; Pmetavar (start, "_") (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f | Node (f, args) -> Pcall (pexp_parse f, args) @@ -184,9 +189,8 @@ and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = | Node (Symbol (_, ":"), [Symbol s; e]) -> (Aexplicit, s, Some (pexp_parse e)) | Symbol s -> (Aexplicit, s, None) - | _ -> (msg_error (sexp_location arg) - "Unrecognized formal arg"; - (Aexplicit, (sexp_location arg, "{arg}"), None)) + | _ -> (pexp_error (sexp_location arg) "Unrecognized formal arg"); + (Aexplicit, (sexp_location arg, "{arg}"), None) and pexp_u_formal_arg (arg : arg_kind * pvar * pexp option) = match arg with @@ -235,7 +239,7 @@ and pexp_p_pat_arg (s : sexp) = match s with | Node (Symbol (_, "_:≡_"), [Symbol f; Symbol s]) -> (Some (Aerasable, f), Ppatvar s) | _ -> let loc = sexp_location s in - msg_error loc "Unknown pattern arg"; + pexp_error loc "Unknown pattern arg"; (None, Ppatany loc) and pexp_u_pat_arg (arg : (arg_kind * symbol) option * ppat) : sexp = @@ -254,7 +258,7 @@ and pexp_p_pat (s : sexp) : ppat = match s with | Node (Symbol c, args) -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in - msg_error l "Unknown pattern"; Ppatany l + pexp_error l "Unknown pattern"; Ppatany l and pexp_u_pat (p : ppat) : sexp = match p with | Ppatany l -> Symbol (l, "_") @@ -268,16 +272,16 @@ and pexp_p_decls e = -> List.concat (List.map pexp_p_decls decls) | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [(s, pexp_parse t, true)] | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [(s, pexp_parse t, false)] - (* | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> - * let rec mkfun args = - * match args with - * | [] -> pexp_parse t - * | (Symbol s :: args) -> Plambda (s, None, mkfun args) - * | (arg :: args) -> msg_error (sexp_location arg) - * "Unknown argument format"; - * mkfun args - * in [(s, mkfun args, false)] *) - | _ -> msg_error (sexp_location e) ("Unknown declaration"); [] + | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> + let rec mkfun args = + match args with + | [] -> pexp_parse t (* Plambda of arg_kind * pvar * pexp option * pexp *) + | (Symbol s :: args) -> Plambda(Aexplicit, s, None, mkfun args) + | (arg :: args) -> pexp_error (sexp_location arg) + "Unknown argument format"; + mkfun args + in [(s, mkfun args, false)] + | _ -> pexp_error (sexp_location e) ("Unknown declaration"); [] and pexp_unparse (e : pexp) : sexp = match e with @@ -309,7 +313,8 @@ and pexp_unparse (e : pexp) : sexp = [Symbol v; pexp_unparse t])); pexp_unparse body]) | Pcall (f, args) -> Node (pexp_unparse f, args) - | Pinductive (_, t, branches) -> + (* Pinductive *) + | Pinductive (s, t, branches) -> Node (Symbol (dummy_location, "inductive_"), sexp_u_list (List.map pexp_u_formal_arg t) :: List.map (fun ((l,name) as s, types) @@ -340,4 +345,7 @@ and pexp_u_decls ds = let pexp_print e = sexp_print (pexp_unparse e) - +(* Parse All Pexp as a list *) +let pexp_parse_all (nodes: sexp list) = + List.map pexp_parse nodes +;; ===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -22,6 +22,8 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util +let prelexer_error = msg_error "PRELEXER" + type pretoken = | Pretoken of location * string | Prestring of location * string @@ -66,7 +68,7 @@ let rec prelex (file : string) (fin : in_channel) ln ctx acc | '"' -> (* A string. *) let rec prestring bp cp chars = if bp >= limit then - (msg_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos} "Unterminated string"; nextline ctx (Prestring ({file=file; line=ln; column=cpos}, "") @@ -80,7 +82,7 @@ let rec prelex (file : string) (fin : in_channel) ln ctx acc :: acc) | '\\' -> (if bpos + 1 >= limit then - (msg_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos} "Unterminated string"; nextline ctx (Prestring ({file=file; line=ln; column=cpos}, @@ -92,7 +94,7 @@ let rec prelex (file : string) (fin : in_channel) ln ctx acc | 'n' -> prestring (bp+2) (cp+2) ('\n' :: chars) | 'r' -> prestring (bp+2) (cp+2) ('\r' :: chars) | ('u' | 'U') -> - msg_error {file=file; line=ln; column=cp} + prelexer_error {file=file; line=ln; column=cp} "Unimplemented unicode escape"; prestring (bp+2) (cp+2) chars | char -> prestring (bp+2) (cp+2) (char :: chars)) @@ -107,7 +109,7 @@ let rec prelex (file : string) (fin : in_channel) ln ctx acc List.rev acc, {file=file; line=ln; column=(cpos + 1)}) :: sacc) - | _ -> (msg_error {file=file; line=ln; column=cpos} + | _ -> (prelexer_error {file=file; line=ln; column=cpos} "Unmatched closing brace"; prelex' ctx (bpos+1) (cpos+1) acc)) | char -> (* A pretoken. *) @@ -130,13 +132,16 @@ let rec prelex (file : string) (fin : in_channel) ln ctx acc match ctx with | [] -> List.rev acc | ((ln, cpos, _, _) :: ctx) -> - (msg_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos} "Unmatched opening brace"; List.rev acc) let prelex_file file = let fin = open_in file in prelex file fin 1 [] [] (* Traditionally, line numbers start at 1 :-( *) + +let prelex_string str = + prelex "string" str 1 [] [] let rec pretokens_print pretokens = List.iter (fun pt -> ===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -31,6 +31,9 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util open Prelexer +open Grammar + +let sexp_error = msg_error "SEXP" type integer = (* Num.num *) int type symbol = location * string @@ -86,13 +89,6 @@ let rec sexp_location s = (*************** The Sexp Parser *********************) -(* FIXME: it should be possible to make something like "." bind tighter than - function application. *) -(* FIXME: what about sections, as in "if_then e1 else_"? *) - -module SMap - = Map.Make (struct type t = string let compare = String.compare end) -type grammar = (int option * int option) SMap.t (* If true, infix symbols like "_;_" will be turned into ";_" or "_;" * if they had no right or left argument. @@ -160,7 +156,7 @@ let rec sexp_parse (g : grammar) (rest : sexp list) * It might simply be a postfix symbol that binds very tightly. * We currently signal an error because it's more common for * it to be a closer with missing opener. *) - -> msg_error l ("Lonely postfix/closer \""^name^"\""); + -> sexp_error l ("Lonely postfix/closer \""^name^"\""); sexp_parse rest' level op largs [mk_node [(l,name);(l,"")] [] rargs true] | (Some ll, Some rl) when ll > level @@ -223,4 +219,15 @@ let sexp_u_list (ss : sexp list) : sexp = | [] -> Epsilon | [s] -> s | (s :: ss) -> Node (s, ss) - + +(* Parse all the Sexp *) +let sexp_parse_all_to_list grm tokens limit = + let rec sexp_parse_impl grm tokens limit acc = + match tokens with + (* We are done parsing *) + | [] -> List.rev acc (* What does list rev do ? *) + (* Keep going *) + | _ -> let (sxp, rest) = sexp_parse_all grm tokens limit in + sexp_parse_impl grm rest limit (sxp :: acc) in + sexp_parse_impl grm tokens limit [] +;; ===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -27,20 +27,41 @@ let dummy_location = {file=""; line=0; column=0} type bottom = | B_o_t_t_o_m_ of bottom -let msg_message kind location msg = - prerr_string location.file; - prerr_char ':'; - prerr_int location.line; - prerr_char ':'; - prerr_int location.column; - prerr_string (":"^kind^": "); - prerr_string msg; - prerr_newline () - -let msg_error = msg_message "Error" -let msg_info = msg_message "Info" +(* print debug info *) +let print_loc (loc: location) = + (*print_string loc.file; *) (* Printing the file is too much*) + print_string "ln "; + Fmt.ralign_print_int loc.line 3; + print_string ", cl "; + Fmt.ralign_print_int loc.column 3; +;; + +(* print debug info *) +let prerr_loc (loc: location) = + (*print_string loc.file; *) (* Printing the file is too much*) + prerr_string "ln "; + Fmt.ralign_prerr_int loc.line 3; + prerr_string ", cl "; + Fmt.ralign_prerr_int loc.column 3; +;; + +(* File is not printed because currently we parse only one file... *) +(* Section is the name of the compilation step [for debugging] *) +(* 'prerr' output is ugly *) +let msg_message kind section (loc: location) msg = + print_string (" " ^ kind); + print_string " ["; print_loc loc; print_string "] "; + print_string (section ^ " "); + print_string msg; + print_newline () + +let msg_error = msg_message "[!] Error " +let msg_info = msg_message "[?] Info " +let msg_warning = msg_message "/!\\ Warning " let string_implode chars = String.concat "" (List.map (String.make 1) chars) exception Internal_error of string let internal_error s = raise (Internal_error s) + + ===================================== tests/debruijn_test.ml ===================================== --- /dev/null +++ b/tests/debruijn_test.ml @@ -0,0 +1,32 @@ +(* TODO make some real test *) +open Debruijn +open Util + +let main () = + (* Tests *) + (* Create a new scope: global scope *) + let loc = dummy_location in + let g0 = make_context in + let g1 = add_variable "a" loc g0 in + let g2 = add_variable "a" loc g1 in + let g3 = add_variable "b" loc g2 in + let g4 = add_variable "c" loc g3 in + let g5 = add_variable "d" loc g4 in + + (* we enter a let or whatever *) + let l0 = add_scope g5 in + let l1 = add_variable "a" loc l0 in + let l2 = add_variable "e" loc l1 in + + (* Testing is done *) + print_string "Inner Context\n"; + print_lexp_context l2; + + (* We exit the scope *) + print_string "Outer Context\n"; + print_lexp_context g5 +;; + + +main () +;; \ No newline at end of file ===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -27,113 +27,149 @@ * * Description: * Provide helper functions to print out - * extracted token - * extracted expression + * extracted Pretoken + * extracted Sexp * * --------------------------------------------------------------------------- *) (* removes some warnings *) open Util - -(* print debug info *) -let print_loc (loc : Util.location) = - print_string loc.file; - print_string ": ln "; - Fmt.ralign_print_int loc.line 3; - print_string ", cl "; - Fmt.ralign_print_int loc.column 3; -;; - +open Prelexer +open Lexer +open Sexp +open Pexp +open Lexp +open Lparse -(*open Token -open Token - -(* Print token with debug info *) -let print_token tok = - (* Shortcut *) - let lalign str = Fmt.lalign_print_string str 20 in - - (* When we need to print only the name *) - let quick_print name loc = - lalign name; - print_string "["; print_loc loc; print_string "] "; - print_string "\n" in - - let long_print name loc elem = - lalign name; - print_string "["; print_loc loc; print_string "] "; - print_string "'"; - print_string elem; - print_string "'\n" in +(* Print aPretokens *) +let rec debug_pretokens_print pretoken = + print_string " "; + let print_info msg loc = + print_string msg; + print_string "["; print_loc loc; print_string "]\t" in - let print_kwd name loc ch = - lalign name; - print_string "["; print_loc loc; print_string "] "; - print_char ch; - print_string "\n" in - - let print_float name loc ch = - lalign name; - print_string "["; print_loc loc; print_string "] "; - print_float ch; - print_string "\n" in - - let print_integer name loc ch = - lalign name; - print_string "["; print_loc loc; print_string "] "; - print_int ch; - print_string "\n" in - - (* Print tokens *) - match tok with - | Token.Arw(loc, str) -> long_print "Arw" loc str; - | Token.Assign(loc, str) -> long_print "Assign" loc str; - | Token.Colon(loc, str) -> long_print "Colon" loc str; - | Token.Lambda(loc) -> quick_print "Lambda" loc; - | Token.Case(loc) -> quick_print "Case" loc; - | Token.Inductive(loc) -> quick_print "Inductive" loc; - | Token.Let(loc) -> quick_print "Let" loc; - | Token.In(loc) -> quick_print "In" loc; - | Token.Ident(loc, str) -> long_print "Identifier" loc str; - | Token.Kwd(loc, ch) -> print_kwd "Kwd" loc ch; - | Token.Float(loc, value) -> print_float "Float" loc value; - | Token.Integer(loc, value) -> print_integer "Integer" loc value; - | Token.String(loc, str) -> long_print "String" loc str; + match pretoken with + | Preblock(loc, pts,_) + -> print_info "Preblock: " loc; + print_string "{"; pretokens_print pts; print_string " }" + + | Pretoken(loc, str) + -> print_info "Pretoken: " loc; + print_string ("'" ^ str ^ "'"); + + | Prestring(loc, str) + -> print_info "Prestring: " loc; + print_string ("\"" ^ str ^ "\""); ;; - -(* Lexer print - *--------------------------------------------------*) - -(* Print the list of token *) -let debug_lex file_name = - let file_stream = open_in file_name in - - (* Create a stream of tokens *) - let lex_stream = Lexer.lex file_name (Stream.of_channel file_stream) in - - (* Print each tokens *) - Stream.iter (fun tok -> print_token tok) lex_stream; +(* Print a List of Pretokens *) +let rec debug_pretokens_print_all pretokens = + List.iter (fun pt -> debug_pretokens_print pt; print_string "\n") pretokens +;; + +(* Sexp Print *) +let rec debug_sexp_print sexp = + let print_info msg loc = + print_string msg; + print_string "["; print_loc loc; print_string "]\t" in + match sexp with + | Epsilon + -> print_string "Epsilon " (* "ε" *) + + | Block(loc, pts, _) + -> print_info "Block: " loc; + print_string "{"; pretokens_print pts; print_string " }" + + | Symbol(loc, name) + -> print_info "Symbol: " loc; print_string name + + | String(loc, str) + -> print_info "String: " loc; + print_string "\""; print_string str; print_string "\"" + + | Integer(loc, n) + -> print_info "Integer: " loc; print_int n + + | Float(loc, x) + -> print_info "Float: " loc; print_float x + + | Node(f, args) + -> print_info "Node: " (sexp_location f); + sexp_print f; print_string " \t "; + List.iter (fun sexp -> sexp_print sexp; print_string " @ ") + args; + print_string " " +;; + +(* Print a list of sexp *) +let debug_sexp_print_all tokens = + List.iter (fun pt -> + print_string " "; + debug_sexp_print pt; + print_string "\n";) + tokens ;; -(* Parser print - *--------------------------------------------------(**) -let debug_parser file_name = - let file_stream = open_in file_name in +(* Print a Pexp with debug info *) +let debug_pexp_print pexp = + print_string " "; + let l = pexp_location pexp in + let print_info msg loc pex = + print_string msg; print_string "["; + print_loc loc; + print_string "]\t"; + pexp_print pexp in + match pexp with + | Pimm _ -> print_info "Pimm " l pexp + | Pvar (_,_) -> print_info "Pvar " l pexp + | Phastype (_,_,_) -> print_info "Phastype " l pexp + | Pmetavar (_, _) -> print_info "Pmetavar " l pexp + | Plet (_, _, _) -> print_info "Plet " l pexp + | Parrow (_, _, _, _, _) -> print_info "Parrow " l pexp + | Plambda (_,_, _, _) -> print_info "Plambda " l pexp + | Pcall (_, _) -> print_info "Pcall " l pexp + | Pinductive (_, _, _) -> print_info "Pinductive " l pexp + | Pcons (_,_) -> print_info "Pcons " l pexp + | Pcase (_, _, _) -> print_info "Pcase " l pexp + | _ -> print_info "Not Impl " l pexp +;; - (* Create a stream of tokens *) - let lex_stream = Lexer.lex file_name (Stream.of_channel file_stream) in - - (* Parse token's stream *) - Toplevel.main_loop lex_stream -;; **) +(* Print a list of pexp *) +let debug_pexp_print_all pexps = + List.iter + (fun px -> + debug_pexp_print px; + print_string "\n") + pexps +;; +(* Print lexp with debug info *) +let debug_lexp_print lxp = + print_string " "; + let print_info msg loc expr= + print_string msg; print_string "["; + print_loc loc; + print_string "]\t"; + lexp_print lxp in + match lxp with + | Var((loc, _), _) -> print_info "Var " loc lxp + | Imm(s) -> print_info "Imm " dummy_location lxp + | Let(loc, _, _) -> print_info "Let " loc lxp + | Arrow(_, _, _, loc, _) -> print_info "Arrow " loc lxp + | Lambda(_, (loc, _), _, _) -> print_info "Lambda " loc lxp + | Call(_, _) -> print_info "Call " dummy_location lxp + | UnknownType(loc) -> print_info "UnknownType " loc lxp + | _ -> print_string "Nothing"; +;; -let main () = - debug_lex "./typer_test/lexer_test.typer"; (**) - - (*debug_parser "kiwi_code/lexer_test.kwi";**) +(* Print a list of lexp *) +let debug_lexp_print_all lexps = + List.iter + (fun px -> + debug_lexp_print px; + print_string "\n") + lexps ;; -main ();*) + ===================================== tests/dummy1_test.ml deleted ===================================== --- a/tests/dummy1_test.ml +++ /dev/null @@ -1,13 +0,0 @@ - -open Util -open Prelexer -open Debug - -let main () = - - let file_name = (Sys.argv.(1) ^ "/samples/lexer_test.typer") in - prelex_file file_name -;; - -main () -;; \ No newline at end of file ===================================== tests/dummy2_test.ml deleted ===================================== --- a/tests/dummy2_test.ml +++ /dev/null @@ -1,13 +0,0 @@ - -open Util -open Prelexer -open Debug - -let main () = - - let file_name = (Sys.argv.(1) ^ "/samples/lexer_test.typer") in - prelex_file file_name -;; - -main () -;; \ No newline at end of file ===================================== tests/dummy_test.ml deleted ===================================== --- a/tests/dummy_test.ml +++ /dev/null @@ -1,16 +0,0 @@ - -open Util -open Prelexer -open Debug - -let main () = - - print_endline Sys.argv.(0); - print_endline Sys.argv.(1); - - let file_name = (Sys.argv.(1) ^ "/samples/lexer_test.typer") in - prelex_file file_name -;; - -main () -;; \ No newline at end of file ===================================== tests/full_debug.ml ===================================== --- /dev/null +++ b/tests/full_debug.ml @@ -0,0 +1,97 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * --------------------------------------------------------------------------- + * + * Description: + * print out each compilation' steps + * + * --------------------------------------------------------------------------- *) + +open Debug +open Prelexer +open Lexer +open Sexp +open Grammar +open Pexp +open Debruijn +open Lparse + + +let main () = + + let arg_n = Array.length Sys.argv in + let usage = + " Usage: \n " ^ Sys.argv.(0) ^ " <file_name> [options] \n\n" in + + let print_title msg = + print_string "\n\t====\n"; + print_string ("\t " ^ msg ^ "\n"); + print_string "\t=======================\n" in + + (* Print Usage *) + if arg_n == 1 then + begin + print_string usage; + print_string " Options:\n"; + end + else + begin + let filename = Sys.argv.(1) in + + (* Read additional Args if any *) + + (* get pretokens*) + let pretoks = prelex_file filename in + + (* get sexp/tokens *) + let toks = lex default_stt pretoks in + + (* get node sexp *) + let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in + + (* get pexp *) + let pexps = pexp_parse_all nodes in + + (* get lexp *) + let ctx = make_context in + let lexps, new_ctx = lexp_parse_all pexps ctx in + + (* Printing *)(* + print_title "PreTokens"; debug_pretokens_print_all pretoks; + print_title "Base Sexp"; debug_sexp_print_all toks; *) + print_title "Node Sexp"; debug_sexp_print_all nodes; + print_title "Pexp"; debug_pexp_print_all pexps; + print_title "Lexp"; debug_lexp_print_all lexps; + + (* Eval Each Expression *) + + + end +;; + +main () +;; + ===================================== tests/lexer_debug.ml deleted ===================================== --- a/tests/lexer_debug.ml +++ /dev/null @@ -1,131 +0,0 @@ -(* - * Typer Compiler - * - * --------------------------------------------------------------------------- - * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. - * - * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> - * Keywords: languages, lisp, dependent types. - * - * This file is part of Typer. - * - * Typer is free software; you can redistribute it and/or modify it under the - * terms of the GNU General Public License as published by the Free Software - * Foundation, either version 3 of the License, or (at your option) any - * later version. - * - * Typer is distributed in the hope that it will be useful, but WITHOUT ANY - * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS - * FOR A PARTICULAR PURPOSE. See the GNU General Public License for - * more details. - * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see <http://www.gnu.org/licenses/>. - * - * --------------------------------------------------------------------------- - * - * Description: - * print out read Sexp (Syntactic expression) - * i.e lexer's tokens - * - * --------------------------------------------------------------------------- *) - -open Util -open Prelexer -open Sexp -open Lexer - -let default_stt = - let stt = Array.create 256 false - in stt.(Char.code ';') <- true; - stt.(Char.code ',') <- true; - stt.(Char.code '(') <- true; - stt.(Char.code ')') <- true; - stt - - -let rec debug_sexp_print sexp = - let print_loc = Debug.print_loc in - match sexp with - | Epsilon - -> print_string "Epsilon()\n" (* "ε" *) - - | Block(loc, pts, _) - -> print_string "Block: \t{"; - print_string "["; print_loc loc; print_string "]\t"; - pretokens_print pts; - print_string " }" - - | Symbol(loc, name) - -> print_string "Symbol: \t"; - print_string "["; print_loc loc; print_string "]\t"; - print_string name - - | String(loc, str) - -> print_string "String: \t"; - print_string "["; print_loc loc; print_string "]\t"; - print_string "\""; print_string str; print_string "\"" - - | Integer(loc, n) - -> print_string "Integer: \t"; - print_string "["; print_loc loc; print_string "]\t"; - print_int n - - | Float(loc, x) - -> print_string "Float: \t"; - print_string "["; print_loc loc; print_string "]\t"; - print_float x - - | Node(f, args) - -> print_string "Node: \t"; - print_string "(";sexp_print f; - List.iter (fun sexp -> print_string " "; sexp_print sexp) - args; - print_string ")" -;; - -let debug_sexp_print_all tokens = - List.iter (fun pt -> - print_string " "; - debug_sexp_print pt; - print_string "\n"; - ) - tokens -;; - -let main () = - (* - * print tokens/sexp of the file given as first arg - * - ********************************************************) - - let file = Sys.argv.(1) in - print_string file; - print_string "\n"; - - (* Todo read file from prog args *) - (* get pretokens*) - let pretoks = prelex_file file in - - (* get tokens *) - let toks = lex default_stt pretoks in - - (* print tokens *) - debug_sexp_print_all toks -;; - -main ();; - -(* Command Line * ) -let command = - Command.basic - ~summary:"Print Compiler Debug Info" - ~readme:(fun () -> "More detailed information") - Command.Spec.(empty +> anon ("filename" %: string)) - main - -let () = - Command.run ~version:"1.0" ~build_info:"RWO" command * *) - -(*(main Sys.argv.(1));;*) ===================================== tests/prelexer_debug.ml deleted ===================================== --- a/tests/prelexer_debug.ml +++ /dev/null @@ -1,73 +0,0 @@ -(* - * Typer Compiler - * - * --------------------------------------------------------------------------- - * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. - * - * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> - * Keywords: languages, lisp, dependent types. - * - * This file is part of Typer. - * - * Typer is free software; you can redistribute it and/or modify it under the - * terms of the GNU General Public License as published by the Free Software - * Foundation, either version 3 of the License, or (at your option) any - * later version. - * - * Typer is distributed in the hope that it will be useful, but WITHOUT ANY - * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS - * FOR A PARTICULAR PURPOSE. See the GNU General Public License for - * more details. - * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see <http://www.gnu.org/licenses/>. - * - * --------------------------------------------------------------------------- - * - * Description: - * print out read pretoken - * - * --------------------------------------------------------------------------- *) - -open Util -open Prelexer -open Debug - -(* TODO: add a Prestring and a Preblock example into the test.typer file *) -let rec debug_pretokens_print pretokens = - List.iter (fun pt -> - print_string " "; - match pt with - | Preblock(loc, pts,_) - -> print_string "Preblock:\t"; - print_string "["; print_loc loc; print_string "]\t"; - print_string "{"; - pretokens_print pts; - print_string " }" - - | Pretoken(loc, str) - -> print_string "Pretoken:\t"; - print_string "["; print_loc loc; print_string "]\t"; - print_string str; - print_string "\n" - - | Prestring(loc, str) - -> print_string "Prestring:\t"; - print_string "["; print_loc loc; print_string "]\t"; - print_string "\""; - print_string str; - print_string "\"\n"; - ) - pretokens - -let main () = - let file = Sys.argv.(1) in - print_string file; - print_string "\n"; - - let arr = prelex_file file in - debug_pretokens_print arr -;; - -main (); ===================================== tests/utest_main.ml ===================================== --- a/tests/utest_main.ml +++ b/tests/utest_main.ml @@ -32,7 +32,7 @@ let cut_name str = - String.sub str 0 (String.length str - 10) + String.sub str 0 (String.length str - 12) ;; (* search *_test.byte executable en run them @@ -60,7 +60,9 @@ let main () = for i = 0 to files_n - 1 do (* Check if file is a test => if it is run it *) - (if Filename.check_suffix files.(i) "_test.byte" then begin + (if (Filename.check_suffix files.(i) "_test.byte") || + (Filename.check_suffix files.(i) "_test.native") then + begin tests_n := !tests_n + 1; View it on GitLab: https://gitlab.com/monnier/typer/compare/57a4f589c0c4dda04796fea8053dda038b…

3 4

Re: [Typer] none
by Stefan Monnier 01 Mar '16

01 Mar '16

> Je me souviens plus pourquoi que l'on voulait utiliser une liste de Meyers ? Pour que l'accès aux variables dans l'environnement soit O(log N) au lieu de O(N). > Il me semblait que l'on avait dit que > let a = b, c = d in > devient > let a = b in > let c = d in > Nous n'avons donc pas besoin que Lexp.Let(location * (vdef * lexp * ltype) > list * lexp) > et nous pouvons utiliser location Lexp.Let(location * (vdef * lexp * ltype) > * lexp) à la place. Non, parce qu'il y a aussi le cas let odd : int -> int; even : int -> int; odd n = case n | 0 => false | S n' => even (n'); even n = case n | 0 => true | S n' => odd (n'); in <exp> qui ne peut pas se décomposer. > Je vais créer un type temporaire Lexp.UnknownType(loc) pour remplacer les > types qui ne sont pas encore inféré OK. Sinon tu peux aussi simplement utiliser type_int. > Est-ce bien un exemple correcte d'un let dans typer ? > let a::Nat, a = b in Presque. L'annotation de type utilise ":" plutôt que "::" et le séparateur entre déclarations est ";" plutôt que ",". Stefan

4 4

[Git][monnier/typer][master] * src/pexp.ml: Adjust to recent changes to Pinductive
by Stefan 26 Fév '16

26 Fév '16

Stefan pushed to branch master at Stefan / Typer Commits: 57a4f589 by Stefan Monnier at 2016-02-26T23:18:43-05:00 * src/pexp.ml: Adjust to recent changes to Pinductive * src/main.ml (process_typer_file.process_decl): Remove Lexp use since it's not ready yet. * src/pexp.ml (pexp_p_actual_arg, pexp_p_formal_arg) (pexp_u_formal_arg): New functions. (pexp_unparse, pexp_parse.pcases): Use them to handle the formal args of inductive types. (pexp_p_decls): Rename from pexp_decls. * .gitignore: Ignore *.byte files. - - - - - 3 changed files: - .gitignore - src/main.ml - src/pexp.ml Changes: ===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ ChangeLog typer +*.byte *.elc *.annot *.cmi ===================================== src/main.ml ===================================== --- a/src/main.ml +++ b/src/main.ml @@ -24,11 +24,11 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util open Lexer open Sexp -open Elaborate -open Javascript +(* open Elaborate *) +(* open Javascript *) (* I think they shouldn't be here, but for now I use them. *) -open Lexp +(* open Lexp *) open Prelexer open Pexp @@ -154,15 +154,15 @@ let process_typer_file sourcename choppable_suffix venv = sexp_print sexp; print_newline(); let pdecls = pexp_p_decls sexp in sexp_print (pexp_u_decls pdecls); print_newline(); - let (decls',pnames',delayed',senv',venv') - = List.fold_left (elaborate_decl (ScopeLevel 0) (default_stt, grm)) - ([], pnames, delayed, senv, venv) - pdecls in - let pdecls = lexp_unparse_decls decls' in - sexp_print (pexp_u_decls pdecls); print_newline(); + (* let (decls',pnames',delayed',senv',venv') + * = List.fold_left (elaborate_decl (ScopeLevel 0) (default_stt, grm)) + * ([], pnames, delayed, senv, venv) + * pdecls in + * let pdecls = lexp_unparse_decls decls' in + * sexp_print (pexp_u_decls pdecls); print_newline(); *) (* print_string ": "; * sexp_print (pexp_unparse (lexp_unparse t)); print_newline(); *) - print_newline(); + (* print_newline(); *) @@ -191,9 +191,9 @@ let process_typer_file sourcename choppable_suffix venv = match rest with | [] -> (decls, venv) | _ -> process_decl (grm, rest, - decls' @ decls, pnames', delayed', senv', venv') + pdecls @ decls, pnames, delayed, senv, venv) in process_decl (default_grammar, tokens, - [], SMap.empty, [], senv_builtin, venv) + [], SMap.empty, None, [], venv) (* ; close_out js_file *) let process_file filename venv = @@ -202,7 +202,7 @@ let process_file filename venv = else raise (Arg.Bad ("Unknown filetype: " ^ filename)) -let (perv_decls, perv_venv) = process_file "pervasive.typer" venv_builtin +let (perv_decls, perv_venv) = process_file "pervasive.typer" None let _ = Arg.parse [ ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -92,7 +92,7 @@ let rec pexp_parse (s : sexp) : pexp = -> Phastype (start, pexp_parse e, pexp_parse t) (* let *) | Node (Symbol (start, "let_in_"), [decls; body]) - -> Plet (start, pexp_decls decls, pexp_parse body) + -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) -> msg_error start "Unrecognized let expression"; Pmetavar (start, "_") (* arrow *) @@ -140,7 +140,7 @@ let rec pexp_parse (s : sexp) : pexp = | _ -> msg_error (sexp_location case) "Unrecognized constructor declaration"; pcases) cases [] in - Pinductive (name, List.map pexp_parse args, pcases) + Pinductive (name, List.map pexp_p_formal_arg args, pcases) | Node (Symbol (start, "inductive_"), _) -> msg_error start "Unrecognized inductive type"; Pmetavar (start, "_") (* constructor *) @@ -165,6 +165,39 @@ let rec pexp_parse (s : sexp) : pexp = | Node (f, []) -> pexp_parse f | Node (f, args) -> Pcall (pexp_parse f, args) +and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = + match arg with + | Node (Symbol (_, ":≡"), [Symbol s; e]) + -> (Aerasable, Some s, pexp_parse e) + | Node (Symbol (_, ":="), [Symbol s; e]) + -> (Aimplicit, Some s, pexp_parse e) + | Node (Symbol (_, ":-"), [Symbol s; e]) + -> (Aexplicit, Some s, pexp_parse e) + | e -> (Aexplicit, None, pexp_parse e) + +and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = + match arg with + | Node (Symbol (_, ":::"), [Symbol s; e]) + -> (Aerasable, s, Some (pexp_parse e)) + | Node (Symbol (_, "::"), [Symbol s; e]) + -> (Aimplicit, s, Some (pexp_parse e)) + | Node (Symbol (_, ":"), [Symbol s; e]) + -> (Aexplicit, s, Some (pexp_parse e)) + | Symbol s -> (Aexplicit, s, None) + | _ -> (msg_error (sexp_location arg) + "Unrecognized formal arg"; + (Aexplicit, (sexp_location arg, "{arg}"), None)) + +and pexp_u_formal_arg (arg : arg_kind * pvar * pexp option) = + match arg with + | (Aexplicit, s, None) -> Symbol s + | (ak, ((l,_) as s), t) + -> Node (Symbol (l, match ak with Aerasable -> ":::" + | Aimplicit -> "::" + | Aexplicit -> ":"), + [Symbol s; match t with Some e -> pexp_unparse e + | None -> Symbol (l, "_")]) + and pexp_p_id (x : location * string) : (location * string) option = match x with | (_, "_") -> None @@ -228,11 +261,11 @@ and pexp_u_pat (p : ppat) : sexp = match p with | Ppatvar s -> Symbol s | Ppatcons (c, args) -> Node (Symbol c, List.map pexp_u_pat_arg args) -and pexp_decls e = +and pexp_p_decls e = match e with | Epsilon -> [] | Node (Symbol (_, ("_;_" | "_;" | ";_")), decls) - -> List.concat (List.map pexp_decls decls) + -> List.concat (List.map pexp_p_decls decls) | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [(s, pexp_parse t, true)] | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [(s, pexp_parse t, false)] (* | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> @@ -278,7 +311,7 @@ and pexp_unparse (e : pexp) : sexp = | Pcall (f, args) -> Node (pexp_unparse f, args) | Pinductive (_, t, branches) -> Node (Symbol (dummy_location, "inductive_"), - sexp_u_list (List.map pexp_unparse t) + sexp_u_list (List.map pexp_u_formal_arg t) :: List.map (fun ((l,name) as s, types) -> Node (Symbol s, List.map pexp_u_ind_arg types)) View it on GitLab: https://gitlab.com/monnier/typer/commit/57a4f589c0c4dda04796fea8053dda038b6…

1 0

mailing list test - PInductive parsing bug
by Pierre Delaunay 22 Fév '16

22 Fév '16

File: pexp.ml Line: 130-152 Pinductive is expecting: (arg_kind * pvar * pexp option) list and (pexp list) is given. I modified the type declaration for this to work. But it is not what it should be. Old Type Pinductive of symbol * (arg_kind * pvar * pexp option) * (symbol * (arg_kind * pvar option * pexp) list) list Temporary Fix: Type Pinductive of symbol * pexp list * (symbol * (arg_kind * pvar option * pexp) list) list Does (arg_kind * pvar * pexp option) <=> (typer code) pvar : pexp ? pexp: is a type pvar: variable name

2 1

[Git][monnier/typer][master] * src/lexp.ml: Various tweaks to prepare for DeBruijn indices
by Stefan 20 Fév '16

20 Fév '16

Stefan pushed to branch master at Stefan / Typer Commits: 3560cc78 by Stefan Monnier at 2016-02-20T00:13:57-05:00 * src/lexp.ml: Various tweaks to prepare for DeBruijn indices (db_index, db_offset, db_revindex): New types. (vref): Use them. (lexp): Add Shift. (env_type): New type. (env_lookup_type): New function. (senv_type): New type. (senv_lookup): New function. (lexp_p_infer, lexp_p_check): New functions. - - - - - 1 changed file: - src/lexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -33,7 +33,10 @@ open Myers * debugging purposes, we remember the name that was used in the source * code. *) type vdef = location * string -type vref = vdef * int +type db_index = int (* DeBruijn index. *) +type db_offset = int (* DeBruijn index offset. *) +type db_revindex = int (* DeBruijn index counting from the root. *) +type vref = vdef * db_index type label = symbol @@ -56,6 +59,10 @@ type ltype = lexp | Sort of location * sort | Builtin of builtin * string * ltype | Var of vref + (* This just means that all non-local Var bindings in the lexp should + * have their debuijn index incremented by i. IOW it guarantees that + * the lexp does not refer to the topmost i elements of the context. *) + | Shift of db_offset * lexp (* This "Let" allows recursion. *) | Let of location * (vdef * lexp * ltype) list * lexp | Arrow of arg_kind * vdef option * ltype * location * lexp @@ -150,6 +157,48 @@ let builtins = * (SMap.empty, VMap.empty) * builtins *) +(* Handling scoping/bindings is always tricky. So it's always important + * to keep in mind for *every* expression which is its context. + * + * In particular, this holds true as well for those expressions that appear + * in the context. Traditionally for dependently typed languages we expect + * the context's rules to say something like: + * + * ⊢ Γ Γ ⊢ τ:Type + * ————————————————— + * ⊢ Γ,x:τ + * + * Which means that we expect (τ) expressions in the context to be typed + * within the *rest* of that context. + * + * This also means that when we look up a binding in the context, we need to + * adjust the result, since we need to use it in the context where we looked + * it up, which is different from the context where it was defined. + * + * More concretely, this means that lookup(Γ, i) should return an expression + * where debruijn indices have been shifted by "i". + * + * This is nice for "normal bindings", but there's a complication in the + * case of recursive definitions. Typically, this is handled by using + * something like a μx.e construct, which works OK for the theory but tends + * to become rather inconvenient in practice for mutually recursive + * definitions. So instead, we annotate the recursive binding with + * a "recursion_offset" to say that rather than being defined in "the rest + * of the context", they're defined in a slightly larger context that + * includes "younger" bindings. + *) + +type env_elem = (db_offset, vdef, lexp option, ltype) +type env_type = env_elem myers +let env_lookup_type (env : env_type) (v : vref) = + let ((_, rname), dbi) = v in + try let (recursion_offset, (_, dname), _, t) = Myers.nth dbi env in + if dname = rname then + Shift (dbi - recursion_offset, t) + else + internal_error "DeBruijn index refers to wrong name!" + with Not_found -> internal_error "DeBruijn index out of bounds!" + (***** SMap fold2 helper *****) let smap_fold2 c f m1 m2 init @@ -527,82 +576,32 @@ and lexp_unparse e : pexp = (* (internal_error "Can't print a Susp") *) let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) - -(* let rec lexp_type (env: (lexp option * lexp) VMap.t) e : lexp = - * let rec follow e = - * match e with - * | Var (_,v) -> vmap_getval v - * | Metavar (_,_,r) -> (match !r with MetaSet e -> follow e | _ -> e) - * | _ -> e - * and vmap_getval (v : var) = - * match VMap.find v env with (Some e, _) -> follow e - * | _ -> Var (dummy_location, v) in - * match e with - * | Sort (l, Stype e) -> Sort (l, Stype (SortLevel (SLsucc e))) - * | Sort (l, StypeOmega) - * -> msg_error l "TypeΩ doesn't have a type"; mk_meta_dummy env l - * | Sort (l, StypeLevel) - * -> msg_error l "TypeLevel doesn't have a type"; mk_meta_dummy env l - * | SortLevel _ -> Sort (lexp_location e, StypeLevel) - * | Imm (Integer _) -> type_int - * | Imm (Float _) -> type_float - * | Builtin (_,_,t) -> t - * (\* | Imm (String _) -> Var (dummy_location, var_string) *\) - * | Imm s -> let l = sexp_location s in - * msg_error l "Unrecognized sexp in lexp"; mk_meta_dummy env l - * | Var (_,name) -> snd (VMap.find name env) - * | Let (l, decls, body) -> - * lexp_type (List.fold_left (fun env ((_,v),e,t) -> - * VMap.add v (Some (Let (l, decls, e)), t) env) - * env decls) - * body - * | Arrow _ -> type0 (\* FIXME! *\) - * | Lambda (ak, ((l,v) as var),t,e) -> - * Arrow (ak, Some var, t, dummy_location, - * lexp_type (VMap.add v (None, t) env) e) - * | Call (f, args) -> - * let ft = lexp_type env f in - * let rec one_arg t (_,arg) = - * match lexp_whnf VMap.empty t with - * | Arrow (_, None, t1, _, t2) -> t2 - * | Arrow (_, Some (_,v), t1, _, t2) -> - * Susp (VMap.add v arg VMap.empty, t2) - * | _ -> msg_error (lexp_location arg) "Too many arguments"; t - * in List.fold_left one_arg ft args - * | Inductive (_,t,_) -> t - * | Cons (e,(l,name)) -> - * (match lexp_whnf VMap.empty e with - * | Inductive (_,_,branches) -> - * (try SMap.find name branches - * with Not_found -> msg_error l ("No such constructor name `"^name^"'"); - * mk_meta_dummy env l) - * | _ -> msg_error l "The constructor refers to a non-inductive type"; - * mk_meta_dummy env l) - * | Case (_,_,_,_,Some default) -> lexp_type env default - * (\* | Case (_,_,(_,i, args, branch) :: _,_) -> - * * let ct = lexp_type env (vmap_getval cv) in - * * let rec one_arg (t,env) argo = - * * match t with - * * | Arrow (_, None, t1, _, t2) -> - * * (t2, VMap.add (snd argo) (None, t1) env) - * * | Arrow (_, Some (l,v), t1, _, t2) -> - * * (Susp (VMap.add v (mk_meta_dummy l) VMap.empty, t2), - * * VMap.add (snd argo) (None, t1) env) - * * | Susp (s, Arrow (ak,v,t1,l,t2)) -> - * * one_arg (Arrow (ak, v, Susp (s, t1), l, Susp (s, t2)), env) argo - * * | _ -> msg_error (fst argo) "Too many arguments"; - * * (t, VMap.add (snd argo) - * * (None, mk_meta_dummy (fst argo)) - * * env) - * * in let (_,env') = List.fold_left one_arg (ct,env) args - * * in lexp_type env' branch *\) - * | Case (l,_,_,_,None) -> mk_meta_dummy env l (\* Dead code? *\) - * | Susp (s, e) -> lexp_type env (lexp_whnf s e) - * | Metavar ((l,_),_,r) - * -> match !r with MetaSet e -> lexp_type env e - * | MetaUnset (_, Some t, _) -> t - * | _ -> msg_error l "Uninstantiated metavar of unknown type"; - * mk_meta_dummy env l *) - -let rec lexp_parse (p : pexp) (env : (vdef * lexp option * ltype) myers) = - + +type senv_type = (db_revindex SMap.t * db_index) +let senv_lookup senv s : db_index = + let (m, i) = senv in + i - SMap.find s senv + +(* Parsing a Pexp into an Lexp is really "elaboration", i.e. it needs to + * infer the types and perform macro-expansion. For won't really + * do any of that, but we can already start structuring it accordingly. + * + * More specifically, we do it with 2 mutually recursive functions: + * one takes a Pexp along with its expected type and return an Lexp + * of that type (hopefully), whereas the other takes a Pexp and + * infers its type (which it returns along with the Lexp). + * This is the idea of "bidirectional type checking", which minimizes + * the amount of "guessing" and/or annotations. Basically guessing/annotations + * is only needed at those few places where the code is not fully-normalized, + * which in normal programs is only in "let" definitions. + * So the rule of thumbs are: + * - use lexp_p_infer for destructors, and use lexp_p_check for constructors. + * - use lexp_p_check whenever you can. + *) +let rec lexp_p_infer (env : env_type) (p : pexp) : lexp * ltype = ? +and lexp_p_check (env : env_type) (p : pexp) (t : ltype) : lexp = + match p with + | _ + -> let (e, inferred_t) = lexp_p_infer env p in + (* FIXME: check that inferred_t = t! *) + e View it on GitLab: https://gitlab.com/monnier/typer/commit/3560cc78e2749a05bfaa746d8ecc1305e20…

1 0

[Git][monnier/typer][master] Fix various minor issues we saw while reading lexp.ml
by Stefan 16 Fév '16

16 Fév '16

Stefan pushed to branch master at Stefan / Typer Commits: cb8b9b2f by Stefan Monnier at 2016-02-16T15:29:26-05:00 Fix various minor issues we saw while reading lexp.ml * src/pexp.ml (pexp): Fix Pinductive definition. (pexp_parse): Fix "inductive-cons" name. * src/lexp.ml: Comment out most of the code. - - - - - 2 changed files: - src/lexp.ml - src/pexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -63,10 +63,10 @@ type ltype = lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of location * label * ((arg_kind * vdef * ltype) list) * ((arg_kind * ltype) list) SMap.t - | Cons of ltype * symbol + | Cons of vref * symbol | Case of location * lexp * ltype (* The base inductive type over which we switch. *) - * (location * (arg_kind * vdef) list * lexp) SMap.t + * (location * (arg_kind * vdef) option list * lexp) SMap.t * lexp option (* Default. *) (* | Susp of subst * lexp * (\* For logical metavars, there's no substitution. *\) @@ -253,213 +253,213 @@ let builtin_reduce b args arg = * - Not a Case (Cons _). * - Not a Call (MetaSet, ..). *) -let rec lexp_whnf (s : lexp VMap.t) e = - match e with - | (Imm _ | Builtin _) -> e - | Sort (_, (StypeLevel | StypeOmega | Stype (SortLevel (SLn _)))) -> e - | Sort (l, Stype e) -> Sort (l, Stype (mk_susp s e)) - | SortLevel (SLn _) -> e - | SortLevel (SLsucc e) -> - (match lexp_whnf s e with - | SortLevel (SLn n) -> SortLevel (SLn (n + 1)) - | e' -> SortLevel (SLsucc e')) - | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, mk_susp s t1, l, mk_susp s t2) - | Lambda (ak, v, t, e) -> Lambda (ak, v, mk_susp s t, mk_susp s e) - | Call (f, args) -> - List.fold_left (fun e (ak,arg) -> - match e with - | Builtin (b,_,_) -> - (match builtin_reduce b [] arg with - | Some e -> e - | _ -> Call (e, [(ak, mk_susp s arg)])) - | Call (Builtin (b,_,_), args) -> - (match builtin_reduce b args arg with - | Some e -> e - | _ -> Call (e, [(ak, mk_susp s arg)])) - | Lambda (_, (_,v), _, body) - -> lexp_whnf (VMap.add v (mk_susp s arg) VMap.empty) body - | Call (f, args) -> Call (f, (ak, mk_susp s arg) :: args) - | _ -> Call (e, [(ak, mk_susp s arg)])) - (lexp_whnf s f) args - | Inductive (id, t, branches) - -> Inductive (id, mk_susp s t, SMap.map (mk_susp s) branches) - | Cons (t, tag) -> Cons (mk_susp s t, tag) - | Case (l, e, t, branches, default) - -> let select name actuals - = try let (l,formals,body) = SMap.find name branches in - lexp_whnf (List.fold_left2 (fun s (_,a) (_,(_,f)) -> - VMap.add f a s) - s actuals formals) - body - with Not_found -> - match default with - | None -> msg_error l "Unmatched constructor"; - mk_meta_dummy VMap.empty l - | Some body -> lexp_whnf s body - in - (match lexp_whnf s e with - | Cons (_, (_,name)) -> select name [] - | Call (Cons (_, (_, name)), actuals) -> select name actuals - | e -> Case (l, e, t, - SMap.map (fun (l,args,body) - -> (l, args, mk_susp s body)) - branches, - match default with Some e -> Some (mk_susp s e) - | None -> None)) - | Susp (s', e) -> lexp_whnf (lexp_subst_subst s s') e - | Metavar (_,MetaFoF,r) -> - (match !r with | MetaSet e -> lexp_whnf s e | _ -> e) - | Metavar (l, MetaGraft s', r) -> - let s' = (lexp_subst_subst s s') in - (match !r with MetaSet e -> lexp_whnf s' e - (* FIXME: filter s' w.r.t `venv'. *) - | MetaUnset (venv,_,_) -> Metavar (l, MetaGraft s', r)) - (* BEWARE: we need a recursive environment, which is kinda painful - * to create (tho we could use ref'cells), so we use a hack instead. *) - | Let (l,decls,body) - -> let decls' = List.map (fun (v, e, t) -> (v, mk_susp s e, mk_susp s t)) - decls in - let s' = List.fold_left (fun s ((l',v),e,t) -> - VMap.add v (Let (l, decls', Var (l', v))) s) - s decls - in lexp_whnf s' body - | Var (l,v) - -> (try match VMap.find v s with - (* Hack attack! A recursive binding, let's unroll it here. *) - | Let (_,decls,Var (_, v')) when v = v' - -> let e = List.fold_left (fun e ((_,v'), e', _) -> - if v = v' then e' else e) - (* This metavar is just a placeholder - * which should be dropped. *) - (mk_meta_dummy VMap.empty l) decls - (* Here we stay in `s' to keep the recursive bindings. *) - in lexp_whnf s (lexp_copy e) - | e -> lexp_whnf VMap.empty (lexp_copy e) - with Not_found -> e) +(* let rec lexp_whnf (s : lexp VMap.t) e = + * match e with + * | (Imm _ | Builtin _) -> e + * | Sort (_, (StypeLevel | StypeOmega | Stype (SortLevel (SLn _)))) -> e + * | Sort (l, Stype e) -> Sort (l, Stype (mk_susp s e)) + * | SortLevel (SLn _) -> e + * | SortLevel (SLsucc e) -> + * (match lexp_whnf s e with + * | SortLevel (SLn n) -> SortLevel (SLn (n + 1)) + * | e' -> SortLevel (SLsucc e')) + * | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, mk_susp s t1, l, mk_susp s t2) + * | Lambda (ak, v, t, e) -> Lambda (ak, v, mk_susp s t, mk_susp s e) + * | Call (f, args) -> + * List.fold_left (fun e (ak,arg) -> + * match e with + * | Builtin (b,_,_) -> + * (match builtin_reduce b [] arg with + * | Some e -> e + * | _ -> Call (e, [(ak, mk_susp s arg)])) + * | Call (Builtin (b,_,_), args) -> + * (match builtin_reduce b args arg with + * | Some e -> e + * | _ -> Call (e, [(ak, mk_susp s arg)])) + * | Lambda (_, (_,v), _, body) + * -> lexp_whnf (VMap.add v (mk_susp s arg) VMap.empty) body + * | Call (f, args) -> Call (f, (ak, mk_susp s arg) :: args) + * | _ -> Call (e, [(ak, mk_susp s arg)])) + * (lexp_whnf s f) args + * | Inductive (id, t, branches) + * -> Inductive (id, mk_susp s t, SMap.map (mk_susp s) branches) + * | Cons (t, tag) -> Cons (mk_susp s t, tag) + * | Case (l, e, t, branches, default) + * -> let select name actuals + * = try let (l,formals,body) = SMap.find name branches in + * lexp_whnf (List.fold_left2 (fun s (_,a) (_,(_,f)) -> + * VMap.add f a s) + * s actuals formals) + * body + * with Not_found -> + * match default with + * | None -> msg_error l "Unmatched constructor"; + * mk_meta_dummy VMap.empty l + * | Some body -> lexp_whnf s body + * in + * (match lexp_whnf s e with + * | Cons (_, (_,name)) -> select name [] + * | Call (Cons (_, (_, name)), actuals) -> select name actuals + * | e -> Case (l, e, t, + * SMap.map (fun (l,args,body) + * -> (l, args, mk_susp s body)) + * branches, + * match default with Some e -> Some (mk_susp s e) + * | None -> None)) + * | Susp (s', e) -> lexp_whnf (lexp_subst_subst s s') e + * | Metavar (_,MetaFoF,r) -> + * (match !r with | MetaSet e -> lexp_whnf s e | _ -> e) + * | Metavar (l, MetaGraft s', r) -> + * let s' = (lexp_subst_subst s s') in + * (match !r with MetaSet e -> lexp_whnf s' e + * (\* FIXME: filter s' w.r.t `venv'. *\) + * | MetaUnset (venv,_,_) -> Metavar (l, MetaGraft s', r)) + * (\* BEWARE: we need a recursive environment, which is kinda painful + * * to create (tho we could use ref'cells), so we use a hack instead. *\) + * | Let (l,decls,body) + * -> let decls' = List.map (fun (v, e, t) -> (v, mk_susp s e, mk_susp s t)) + * decls in + * let s' = List.fold_left (fun s ((l',v),e,t) -> + * VMap.add v (Let (l, decls', Var (l', v))) s) + * s decls + * in lexp_whnf s' body + * | Var (l,v) + * -> (try match VMap.find v s with + * (\* Hack attack! A recursive binding, let's unroll it here. *\) + * | Let (_,decls,Var (_, v')) when v = v' + * -> let e = List.fold_left (fun e ((_,v'), e', _) -> + * if v = v' then e' else e) + * (\* This metavar is just a placeholder + * * which should be dropped. *\) + * (mk_meta_dummy VMap.empty l) decls + * (\* Here we stay in `s' to keep the recursive bindings. *\) + * in lexp_whnf s (lexp_copy e) + * | e -> lexp_whnf VMap.empty (lexp_copy e) + * with Not_found -> e) *) let conv_erase = true (* If true, conv ignores erased terms. *) (* Return true iff e₁ and e₂ are convertible in `env'. * `s' maps vars bound in e₁ to their α-equivalent in e₂. *) -let rec lexp_conv_p env s e1 e2 = - let lexp_conv_p = lexp_conv_p env in - (* We compare e1 and e2 directly because vars in `s' should never appear - * in e2 anyway, so if e1 and e2 are equal, then e1 doesn't refer to vars - * in `s' either. *) - e1 == e2 - || match (e1, e2) with - | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 - | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 - | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 - | (Var (_, v1), Var (_, v2)) -> - v1 = v2 - || (match try fst (VMap.find v1 env) with _ -> None with - | Some e1 -> lexp_conv_p s e1 e2 - | None -> match try fst (VMap.find v2 env) with _ -> None with - | Some e2 -> lexp_conv_p s e1 e2 - | None -> v2 = VMap.find v1 s) - | (Var (_, v1), _) - -> (match try fst (VMap.find v1 env) with _ -> None with - | Some e1 -> lexp_conv_p s e1 e2 - | None -> false) - | (_, Var (_, v2)) - -> (match try fst (VMap.find v2 env) with _ -> None with - | Some e2 -> lexp_conv_p s e1 e2 - | None -> false) - | (Metavar (_, mk, r1), _) - when (match !r1 with MetaSet _ -> true | _ -> false) - -> (match !r1,mk with - | MetaSet e1, MetaGraft s1 -> lexp_conv_p s (mk_susp s1 e1) e2 - | MetaSet e1, MetaFoF -> lexp_conv_p s e1 e2 - | _ -> false) (* Impossible. *) - | (_, Metavar (_, mk, r2)) - when (match !r2 with MetaSet _ -> true | _ -> false) - -> (match !r2,mk with - | MetaSet e2, MetaGraft s2 -> lexp_conv_p s e1 (mk_susp s2 e2) - | MetaSet e2, MetaFoF -> lexp_conv_p s e1 e2 - | _ -> false) (* Impossible. *) - | (Metavar ((l,_), MetaGraft s1, r1), Metavar (_, MetaGraft s2, r2)) - when r1 = r2 - -> (match !r1 with - | MetaSet _ -> false (* Impossible! *) - | MetaUnset (venv,_,_) - -> let diffs - (* FIXME: If we filter s1&s2 when constructing MetaGraft, we can - * use VMap.equal. *) - = VMap.merge - (fun v e1 e2 - -> try let _ = VMap.find v venv in - match e1,e2 with - | Some e1, Some e2 when lexp_conv_p s e1 e2 - -> None - | _ -> Some () - (* If `v' is not in `venv' that means `v' cannot - * appear in the var's instantiation, so we only need - * to decide if s(e)=e which we presume to be true for - * the same reason that we started this function by - * comparing e1≡e2 rather than s(e1)=e2. *) - with _ -> None) - s1 s2 - in VMap.is_empty diffs) - | (Metavar (_, MetaFoF, r1), Metavar (_, MetaFoF, r2)) -> r1 = r2 - | (Susp (s1, e1), _) -> lexp_conv_p s (lexp_whnf s1 e1) e2 - | (_, Susp (s2, e2)) -> lexp_conv_p s e1 (lexp_whnf s2 e2) - | (Cons (t1, (_, tag1)), Cons (t2, (_, tag2))) - -> tag1 = tag2 && lexp_conv_p s t1 t2 - | (Case (_,e1,t1,branches1,default1), Case (_,e2,t2,branches2,default2)) - -> lexp_conv_p s e1 e2 - && (match (default1, default2) with - | (None, None) -> true - | (Some e1, Some e2) -> lexp_conv_p s e1 e2 - | _ -> false) - && (conv_erase || lexp_conv_p s t1 t2) - && SMap.equal - (fun (_, args1, e1) (_, args2, e2) - -> lexp_conv_p (List.fold_left2 - (fun s (ak1,(_,arg1)) (ak2,(_,arg2)) - -> if conv_erase && ak1 = Aerasable then s - else VMap.add arg1 arg2 s) - s args1 args2) - e1 e2) - branches1 branches2 - | (Inductive ((_,id1), t1, cases1), Inductive ((_,id2), t2, cases2)) - -> id1 = id2 - && lexp_conv_p s t1 t2 - && SMap.equal (lexp_conv_p s) cases1 cases2 - | (Lambda (Aerasable,_,_,e1), Lambda (Aerasable,_,_,e2)) when conv_erase - -> lexp_conv_p s e1 e2 - | (Lambda (ak1,(_,v1),t1,e1), Lambda (ak2,(_,v2),t2,e2)) - -> ak1 = ak2 - && (conv_erase || lexp_conv_p s t1 t2) - && lexp_conv_p (VMap.add v1 v2 s) e1 e2 - | (Call (f1, args1), Call (f2, args2)) - -> lexp_conv_p s f1 f2 - && List.length args1 = List.length args2 - && List.fold_left2 (fun eqp (ak1,a1) (ak2,a2) -> - eqp && ak1 = ak2 - && ((conv_erase && ak1 = Aerasable) - || lexp_conv_p s a1 a2)) - true args1 args2 - | (Arrow (ak1,v1,t11,_,t21), Arrow (ak2,v2,t12,_,t22)) - -> ak1 = ak2 - && lexp_conv_p s t11 t12 - && lexp_conv_p (match (v1,v2) with - | (Some (_,v1), Some (_,v2)) -> VMap.add v1 v2 s - | _ -> s) - t21 t22 - | (Let (_,decls1,body1), Let (_,decls2,body2)) - -> List.length decls1 = List.length decls2 - && let s' = List.fold_left2 (fun s ((_,v1),_,_) ((_,v2),_,_) - -> VMap.add v1 v2 s) - s decls1 decls2 - in List.fold_left2 (fun eqp (_,e1,t1) (_,e2,t2) -> - eqp - && lexp_conv_p s' e1 e2 - && lexp_conv_p s t1 t2) - (lexp_conv_p s' body1 body2) - decls1 decls2 - | (_, _) -> false +(* let rec lexp_conv_p env s e1 e2 = + * let lexp_conv_p = lexp_conv_p env in + * (\* We compare e1 and e2 directly because vars in `s' should never appear + * * in e2 anyway, so if e1 and e2 are equal, then e1 doesn't refer to vars + * * in `s' either. *\) + * e1 == e2 + * || match (e1, e2) with + * | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 + * | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 + * | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 + * | (Var (_, v1), Var (_, v2)) -> + * v1 = v2 + * || (match try fst (VMap.find v1 env) with _ -> None with + * | Some e1 -> lexp_conv_p s e1 e2 + * | None -> match try fst (VMap.find v2 env) with _ -> None with + * | Some e2 -> lexp_conv_p s e1 e2 + * | None -> v2 = VMap.find v1 s) + * | (Var (_, v1), _) + * -> (match try fst (VMap.find v1 env) with _ -> None with + * | Some e1 -> lexp_conv_p s e1 e2 + * | None -> false) + * | (_, Var (_, v2)) + * -> (match try fst (VMap.find v2 env) with _ -> None with + * | Some e2 -> lexp_conv_p s e1 e2 + * | None -> false) + * | (Metavar (_, mk, r1), _) + * when (match !r1 with MetaSet _ -> true | _ -> false) + * -> (match !r1,mk with + * | MetaSet e1, MetaGraft s1 -> lexp_conv_p s (mk_susp s1 e1) e2 + * | MetaSet e1, MetaFoF -> lexp_conv_p s e1 e2 + * | _ -> false) (\* Impossible. *\) + * | (_, Metavar (_, mk, r2)) + * when (match !r2 with MetaSet _ -> true | _ -> false) + * -> (match !r2,mk with + * | MetaSet e2, MetaGraft s2 -> lexp_conv_p s e1 (mk_susp s2 e2) + * | MetaSet e2, MetaFoF -> lexp_conv_p s e1 e2 + * | _ -> false) (\* Impossible. *\) + * | (Metavar ((l,_), MetaGraft s1, r1), Metavar (_, MetaGraft s2, r2)) + * when r1 = r2 + * -> (match !r1 with + * | MetaSet _ -> false (\* Impossible! *\) + * | MetaUnset (venv,_,_) + * -> let diffs + * (\* FIXME: If we filter s1&s2 when constructing MetaGraft, we can + * * use VMap.equal. *\) + * = VMap.merge + * (fun v e1 e2 + * -> try let _ = VMap.find v venv in + * match e1,e2 with + * | Some e1, Some e2 when lexp_conv_p s e1 e2 + * -> None + * | _ -> Some () + * (\* If `v' is not in `venv' that means `v' cannot + * * appear in the var's instantiation, so we only need + * * to decide if s(e)=e which we presume to be true for + * * the same reason that we started this function by + * * comparing e1≡e2 rather than s(e1)=e2. *\) + * with _ -> None) + * s1 s2 + * in VMap.is_empty diffs) + * | (Metavar (_, MetaFoF, r1), Metavar (_, MetaFoF, r2)) -> r1 = r2 + * | (Susp (s1, e1), _) -> lexp_conv_p s (lexp_whnf s1 e1) e2 + * | (_, Susp (s2, e2)) -> lexp_conv_p s e1 (lexp_whnf s2 e2) + * | (Cons (t1, (_, tag1)), Cons (t2, (_, tag2))) + * -> tag1 = tag2 && lexp_conv_p s t1 t2 + * | (Case (_,e1,t1,branches1,default1), Case (_,e2,t2,branches2,default2)) + * -> lexp_conv_p s e1 e2 + * && (match (default1, default2) with + * | (None, None) -> true + * | (Some e1, Some e2) -> lexp_conv_p s e1 e2 + * | _ -> false) + * && (conv_erase || lexp_conv_p s t1 t2) + * && SMap.equal + * (fun (_, args1, e1) (_, args2, e2) + * -> lexp_conv_p (List.fold_left2 + * (fun s (ak1,(_,arg1)) (ak2,(_,arg2)) + * -> if conv_erase && ak1 = Aerasable then s + * else VMap.add arg1 arg2 s) + * s args1 args2) + * e1 e2) + * branches1 branches2 + * | (Inductive ((_,id1), t1, cases1), Inductive ((_,id2), t2, cases2)) + * -> id1 = id2 + * && lexp_conv_p s t1 t2 + * && SMap.equal (lexp_conv_p s) cases1 cases2 + * | (Lambda (Aerasable,_,_,e1), Lambda (Aerasable,_,_,e2)) when conv_erase + * -> lexp_conv_p s e1 e2 + * | (Lambda (ak1,(_,v1),t1,e1), Lambda (ak2,(_,v2),t2,e2)) + * -> ak1 = ak2 + * && (conv_erase || lexp_conv_p s t1 t2) + * && lexp_conv_p (VMap.add v1 v2 s) e1 e2 + * | (Call (f1, args1), Call (f2, args2)) + * -> lexp_conv_p s f1 f2 + * && List.length args1 = List.length args2 + * && List.fold_left2 (fun eqp (ak1,a1) (ak2,a2) -> + * eqp && ak1 = ak2 + * && ((conv_erase && ak1 = Aerasable) + * || lexp_conv_p s a1 a2)) + * true args1 args2 + * | (Arrow (ak1,v1,t11,_,t21), Arrow (ak2,v2,t12,_,t22)) + * -> ak1 = ak2 + * && lexp_conv_p s t11 t12 + * && lexp_conv_p (match (v1,v2) with + * | (Some (_,v1), Some (_,v2)) -> VMap.add v1 v2 s + * | _ -> s) + * t21 t22 + * | (Let (_,decls1,body1), Let (_,decls2,body2)) + * -> List.length decls1 = List.length decls2 + * && let s' = List.fold_left2 (fun s ((_,v1),_,_) ((_,v2),_,_) + * -> VMap.add v1 v2 s) + * s decls1 decls2 + * in List.fold_left2 (fun eqp (_,e1,t1) (_,e2,t2) -> + * eqp + * && lexp_conv_p s' e1 e2 + * && lexp_conv_p s t1 t2) + * (lexp_conv_p s' body1 body2) + * decls1 decls2 + * | (_, _) -> false *) (* In non-recursion calls, `s' is always empty. *) let lexp_conv_p env = lexp_conv_p env VMap.empty @@ -519,88 +519,90 @@ and lexp_unparse e : pexp = lexp_unparse e) :: cases) branches [], opt_map lexp_unparse default) - | Metavar (v,_,r) -> - (match !r with - | MetaSet e -> lexp_unparse e - | _ -> Pmetavar v) (* FIXME: losing the ref. *) - | Susp (s,e) -> lexp_unparse (lexp_whnf s e) + (* | Metavar (v,_,r) -> + * (match !r with + * | MetaSet e -> lexp_unparse e + * | _ -> Pmetavar v) (\* FIXME: losing the ref. *\) + * | Susp (s,e) -> lexp_unparse (lexp_whnf s e) *) (* (internal_error "Can't print a Susp") *) let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) -let rec lexp_type (env: (lexp option * lexp) VMap.t) e : lexp = - let rec follow e = - match e with - | Var (_,v) -> vmap_getval v - | Metavar (_,_,r) -> (match !r with MetaSet e -> follow e | _ -> e) - | _ -> e - and vmap_getval (v : var) = - match VMap.find v env with (Some e, _) -> follow e - | _ -> Var (dummy_location, v) in - match e with - | Sort (l, Stype e) -> Sort (l, Stype (SortLevel (SLsucc e))) - | Sort (l, StypeOmega) - -> msg_error l "TypeΩ doesn't have a type"; mk_meta_dummy env l - | Sort (l, StypeLevel) - -> msg_error l "TypeLevel doesn't have a type"; mk_meta_dummy env l - | SortLevel _ -> Sort (lexp_location e, StypeLevel) - | Imm (Integer _) -> type_int - | Imm (Float _) -> type_float - | Builtin (_,_,t) -> t - (* | Imm (String _) -> Var (dummy_location, var_string) *) - | Imm s -> let l = sexp_location s in - msg_error l "Unrecognized sexp in lexp"; mk_meta_dummy env l - | Var (_,name) -> snd (VMap.find name env) - | Let (l, decls, body) -> - lexp_type (List.fold_left (fun env ((_,v),e,t) -> - VMap.add v (Some (Let (l, decls, e)), t) env) - env decls) - body - | Arrow _ -> type0 (* FIXME! *) - | Lambda (ak, ((l,v) as var),t,e) -> - Arrow (ak, Some var, t, dummy_location, - lexp_type (VMap.add v (None, t) env) e) - | Call (f, args) -> - let ft = lexp_type env f in - let rec one_arg t (_,arg) = - match lexp_whnf VMap.empty t with - | Arrow (_, None, t1, _, t2) -> t2 - | Arrow (_, Some (_,v), t1, _, t2) -> - Susp (VMap.add v arg VMap.empty, t2) - | _ -> msg_error (lexp_location arg) "Too many arguments"; t - in List.fold_left one_arg ft args - | Inductive (_,t,_) -> t - | Cons (e,(l,name)) -> - (match lexp_whnf VMap.empty e with - | Inductive (_,_,branches) -> - (try SMap.find name branches - with Not_found -> msg_error l ("No such constructor name `"^name^"'"); - mk_meta_dummy env l) - | _ -> msg_error l "The constructor refers to a non-inductive type"; - mk_meta_dummy env l) - | Case (_,_,_,_,Some default) -> lexp_type env default - (* | Case (_,_,(_,i, args, branch) :: _,_) -> - * let ct = lexp_type env (vmap_getval cv) in - * let rec one_arg (t,env) argo = - * match t with - * | Arrow (_, None, t1, _, t2) -> - * (t2, VMap.add (snd argo) (None, t1) env) - * | Arrow (_, Some (l,v), t1, _, t2) -> - * (Susp (VMap.add v (mk_meta_dummy l) VMap.empty, t2), - * VMap.add (snd argo) (None, t1) env) - * | Susp (s, Arrow (ak,v,t1,l,t2)) -> - * one_arg (Arrow (ak, v, Susp (s, t1), l, Susp (s, t2)), env) argo - * | _ -> msg_error (fst argo) "Too many arguments"; - * (t, VMap.add (snd argo) - * (None, mk_meta_dummy (fst argo)) - * env) - * in let (_,env') = List.fold_left one_arg (ct,env) args - * in lexp_type env' branch *) - | Case (l,_,_,_,None) -> mk_meta_dummy env l (* Dead code? *) - | Susp (s, e) -> lexp_type env (lexp_whnf s e) - | Metavar ((l,_),_,r) - -> match !r with MetaSet e -> lexp_type env e - | MetaUnset (_, Some t, _) -> t - | _ -> msg_error l "Uninstantiated metavar of unknown type"; - mk_meta_dummy env l +(* let rec lexp_type (env: (lexp option * lexp) VMap.t) e : lexp = + * let rec follow e = + * match e with + * | Var (_,v) -> vmap_getval v + * | Metavar (_,_,r) -> (match !r with MetaSet e -> follow e | _ -> e) + * | _ -> e + * and vmap_getval (v : var) = + * match VMap.find v env with (Some e, _) -> follow e + * | _ -> Var (dummy_location, v) in + * match e with + * | Sort (l, Stype e) -> Sort (l, Stype (SortLevel (SLsucc e))) + * | Sort (l, StypeOmega) + * -> msg_error l "TypeΩ doesn't have a type"; mk_meta_dummy env l + * | Sort (l, StypeLevel) + * -> msg_error l "TypeLevel doesn't have a type"; mk_meta_dummy env l + * | SortLevel _ -> Sort (lexp_location e, StypeLevel) + * | Imm (Integer _) -> type_int + * | Imm (Float _) -> type_float + * | Builtin (_,_,t) -> t + * (\* | Imm (String _) -> Var (dummy_location, var_string) *\) + * | Imm s -> let l = sexp_location s in + * msg_error l "Unrecognized sexp in lexp"; mk_meta_dummy env l + * | Var (_,name) -> snd (VMap.find name env) + * | Let (l, decls, body) -> + * lexp_type (List.fold_left (fun env ((_,v),e,t) -> + * VMap.add v (Some (Let (l, decls, e)), t) env) + * env decls) + * body + * | Arrow _ -> type0 (\* FIXME! *\) + * | Lambda (ak, ((l,v) as var),t,e) -> + * Arrow (ak, Some var, t, dummy_location, + * lexp_type (VMap.add v (None, t) env) e) + * | Call (f, args) -> + * let ft = lexp_type env f in + * let rec one_arg t (_,arg) = + * match lexp_whnf VMap.empty t with + * | Arrow (_, None, t1, _, t2) -> t2 + * | Arrow (_, Some (_,v), t1, _, t2) -> + * Susp (VMap.add v arg VMap.empty, t2) + * | _ -> msg_error (lexp_location arg) "Too many arguments"; t + * in List.fold_left one_arg ft args + * | Inductive (_,t,_) -> t + * | Cons (e,(l,name)) -> + * (match lexp_whnf VMap.empty e with + * | Inductive (_,_,branches) -> + * (try SMap.find name branches + * with Not_found -> msg_error l ("No such constructor name `"^name^"'"); + * mk_meta_dummy env l) + * | _ -> msg_error l "The constructor refers to a non-inductive type"; + * mk_meta_dummy env l) + * | Case (_,_,_,_,Some default) -> lexp_type env default + * (\* | Case (_,_,(_,i, args, branch) :: _,_) -> + * * let ct = lexp_type env (vmap_getval cv) in + * * let rec one_arg (t,env) argo = + * * match t with + * * | Arrow (_, None, t1, _, t2) -> + * * (t2, VMap.add (snd argo) (None, t1) env) + * * | Arrow (_, Some (l,v), t1, _, t2) -> + * * (Susp (VMap.add v (mk_meta_dummy l) VMap.empty, t2), + * * VMap.add (snd argo) (None, t1) env) + * * | Susp (s, Arrow (ak,v,t1,l,t2)) -> + * * one_arg (Arrow (ak, v, Susp (s, t1), l, Susp (s, t2)), env) argo + * * | _ -> msg_error (fst argo) "Too many arguments"; + * * (t, VMap.add (snd argo) + * * (None, mk_meta_dummy (fst argo)) + * * env) + * * in let (_,env') = List.fold_left one_arg (ct,env) args + * * in lexp_type env' branch *\) + * | Case (l,_,_,_,None) -> mk_meta_dummy env l (\* Dead code? *\) + * | Susp (s, e) -> lexp_type env (lexp_whnf s e) + * | Metavar ((l,_),_,r) + * -> match !r with MetaSet e -> lexp_type env e + * | MetaUnset (_, Some t, _) -> t + * | _ -> msg_error l "Uninstantiated metavar of unknown type"; + * mk_meta_dummy env l *) + +let rec lexp_parse (p : pexp) (env : (vdef * lexp option * ltype) myers) = ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -1,6 +1,6 @@ (* pexp.ml --- Proto lambda-expressions, half-way between Sexp and Lexp. -Copyright (C) 2011-2012, 2015 Free Software Foundation, Inc. +Copyright (C) 2011-2012, 2015, 2016 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -51,7 +51,7 @@ type pexp = | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two * otherwise isomorphic types. *) - | Pinductive of symbol * pexp list + | Pinductive of symbol * (arg_kind * pvar * pexp option) list * (symbol * (arg_kind * pvar option * pexp) list) list | Pcons of pvar * symbol | Pcase of location * pexp * (ppat * pexp) list @@ -144,7 +144,7 @@ let rec pexp_parse (s : sexp) : pexp = | Node (Symbol (start, "inductive_"), _) -> msg_error start "Unrecognized inductive type"; Pmetavar (start, "_") (* constructor *) - | Node (Symbol (start, "cons_"), [Symbol tname; Symbol tag]) + | Node (Symbol (start, "inductive-cons"), [Symbol tname; Symbol tag]) -> Pcons (tname, tag) | Node (Symbol (start, "cons_"), _) -> msg_error start "Unrecognized constructor call"; Pmetavar (start, "_") View it on GitLab: https://gitlab.com/monnier/typer/commit/cb8b9b2f26868607579c04701a5a9eb389a…

1 0

[Git][monnier/typer][master] Start changes to use deb-indices and drop type inference
by Stefan 15 Fév '16

15 Fév '16

Stefan pushed to branch master at Stefan / Typer Commits: f15cc0c5 by Stefan Monnier at 2016-02-15T10:19:55-05:00 Start changes to use deb-indices and drop type inference * src/lexp.ml: Start changes to use deb-indices and simplify things. (vref): New type. (lexp): Var now uses debruijn-indices. Comment out metavars since we're not going to do inference for now. (type_eq, builtins, lexp_location): Adjust accordingly. (lexp_alpha): Remove since deb-indices don't need it. * typer-mode.el (typer-smie-grammar): Add an explicit level for "=". - - - - - 3 changed files: - src/test.typer → samples/test.typer - src/lexp.ml - typer-mode.el Changes: ===================================== src/test.typer → samples/test.typer ===================================== --- a/src/test.typer +++ b/samples/test.typer @@ -1,5 +1,3 @@ -%% FIXME: adjust to the new top-level made of decls instead of exps. - %% Issues: %% - syntax of "telescopes", especially the implicit and erasable args. %% ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -27,17 +27,18 @@ open Pexp open Myers (* open Unify *) -(*************** Unique small integers for variables *********************) +(*************** DeBruijn indices for variables *********************) -type var = int -module VMap - = Map.Make (struct type t = var let compare = compare end) -type varo = location * var (* Occurrence of a variable's symbol. *) +(* Occurrence of a variable's symbol: we use DeBruijn index, and for + * debugging purposes, we remember the name that was used in the source + * code. *) +type vdef = location * string +type vref = vdef * int -(*************** Elaboration to Lexp *********************) -type scope_level = | ScopeLevel of int -let next_scope (ScopeLevel sl) = ScopeLevel (1+sl) +type label = symbol + +(*************** Elaboration to Lexp *********************) type builtin = | IntType @@ -54,33 +55,34 @@ type ltype = lexp | SortLevel of sort_level | Sort of location * sort | Builtin of builtin * string * ltype - | Var of varo - | Let of location * (varo * lexp * ltype) list * lexp - | Arrow of arg_kind * varo option * ltype * location * lexp - | Lambda of arg_kind * varo * ltype * lexp + | Var of vref + (* This "Let" allows recursion. *) + | Let of location * (vdef * lexp * ltype) list * lexp + | Arrow of arg_kind * vdef option * ltype * location * lexp + | Lambda of arg_kind * vdef * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of varo * ltype * lexp SMap.t + | Inductive of location * label * ((arg_kind * vdef * ltype) list) + * ((arg_kind * ltype) list) SMap.t | Cons of ltype * symbol - (* FIXME: how 'bout return type, type refinement, ...? *) | Case of location * lexp * ltype (* The base inductive type over which we switch. *) - * (location * (arg_kind * varo) list * lexp) SMap.t + * (location * (arg_kind * vdef) list * lexp) SMap.t * lexp option (* Default. *) - | Susp of subst * lexp - (* For logical metavars, there's no substitution. *) - | Metavar of (location * string) * metakind * metavar ref - and metavar = - (* An uninstantiated var, along with a venv (stipulating over which vars - * it should be closed), and its type. - * If its type is not given, it implies its type should be a sort. *) - | MetaUnset of (lexp option * lexp) VMap.t * ltype option * scope_level - | MetaSet of lexp - and metakind = - | MetaGraft of subst - (* Forward reference or Free var: Not known yet, but not instantiable by - * unification. *) - | MetaFoF - and subst = lexp VMap.t + (* | Susp of subst * lexp + * (\* For logical metavars, there's no substitution. *\) + * | Metavar of (location * string) * metakind * metavar ref + * and metavar = + * (\* An uninstantiated var, along with a venv (stipulating over which vars + * * it should be closed), and its type. + * * If its type is not given, it implies its type should be a sort. *\) + * | MetaUnset of (lexp option * lexp) VMap.t * ltype option * scope_level + * | MetaSet of lexp + * and metakind = + * | MetaGraft of subst + * (\* Forward reference or Free var: Not known yet, but not instantiable by + * * unification. *\) + * | MetaFoF + * and subst = lexp VMap.t *) and sort = | Stype of lexp | StypeOmega @@ -90,22 +92,9 @@ type ltype = lexp | SLsucc of lexp -let mk_susp s e = if VMap.is_empty s then e else Susp (s, e) -let mk_subst x v e = Susp (VMap.add x v VMap.empty, e) +(* let mk_susp s e = if VMap.is_empty s then e else Susp (s, e) + * let mk_subst x v e = Susp (VMap.add x v VMap.empty, e) *) -(**** Make fresh new small ints, and keep track of their name ****) - -let varcounter = ref 0 -let varname_table = ref VMap.empty -let varname var = VMap.find var !varname_table -let mkvar name = - let v = !varcounter in - varcounter := 1 + !varcounter; - varname_table := VMap.add v name !varname_table; - v -let copy_var v = mkvar (varname v) -let print_var v = print_string (varname v); print_int v - let opt_map f x = match x with None -> None | Some x -> Some (f x) (**** The builtin elements ****) @@ -123,12 +112,14 @@ let type_level = Builtin (LevelType, "TypeLevel", type_level) let type_eq = Builtin (EqType, "_₌_", - let lv = (dloc, mkvar "ℓ") in - let tv = (dloc, mkvar "t") in + let lv = (dloc, "ℓ") in + let tv = (dloc, "t") in Arrow (Aerasable, Some lv, type_level, dloc, - Arrow (Aerasable, Some tv, Sort (dloc, Stype (Var lv)), dloc, - Arrow (Aexplicit, None, Var tv, dloc, - Arrow (Aexplicit, None, Var tv, dloc, type0))))) + Arrow (Aerasable, Some tv, + Sort (dloc, Stype (Var (lv, 0))), dloc, + Arrow (Aexplicit, None, Var (tv, 0), dloc, + Arrow (Aexplicit, None, Var (tv, 1), dloc, + type0))))) let iop_binary = Arrow (Aexplicit, None, type_int, dummy_location, Arrow (Aexplicit, None, type_int, dummy_location, type_int)) @@ -137,27 +128,27 @@ let builtins = (* let l = dloc in *) [ (* (0,"%type1%", Some (type1), Lsort (l, 2)) *) ("Type", Some (type0), type1) - ; ("Type@", Some (let lv = (dloc, mkvar "ℓ") in + ; ("Type@", Some (let lv = (dloc, "ℓ") in Lambda (Aexplicit, lv, type_level, - Sort (dloc, Stype (Var lv)))), - let lv = (dloc, mkvar "ℓ") in + Sort (dloc, Stype (Var (lv, 0))))), + let lv = (dloc, "ℓ") in Arrow (Aexplicit, Some lv, type_level, dloc, - Sort (dloc, Stype (SortLevel (SLsucc (Var lv)))))) - (* ;(var_macro, "%Macro%", None, type0) *) + Sort (dloc, Stype (SortLevel (SLsucc (Var (lv,0))))))) + (* ;(var_macro, "%Macro%", None, type0) *) ] @ List.map (fun bi -> match bi with | Builtin (_, name, t) -> (name, Some bi, t) | _ -> internal_error "Registering a non-builtin") [type_level; type_int; type_float; type_eq] -let var_bottom = Var (dloc, -1) +(* let var_bottom = Var (dloc, -1) *) -let (senv_builtin,venv_builtin) - = List.fold_left (fun (senv,venv) (name,e,t) -> - let v = mkvar name in - (SMap.add name v senv, - VMap.add v (e, t) venv)) - (SMap.empty, VMap.empty) - builtins +(* let (senv_builtin,venv_builtin) + * = List.fold_left (fun (senv,venv) (name,e,t) -> + * let v = name in + * (SMap.add name v senv, + * VMap.add v (e, t) venv)) + * (SMap.empty, VMap.empty) + * builtins *) (***** SMap fold2 helper *****) @@ -167,43 +158,44 @@ let smap_fold2 c f m1 m2 init (** Elaboration. **) -let mk_meta2 sl venv l - = let mk = MetaGraft VMap.empty in - let t = Metavar ((l, "_"), mk, ref (MetaUnset (venv, None, sl))) - in (Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))), t) -let mk_meta sl venv l - = let mk = MetaGraft VMap.empty in - let t = Metavar ((l, "_"), mk, ref (MetaUnset (venv, None, sl))) - in Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))) -let mk_meta_dummy = mk_meta (ScopeLevel(-1)) -let mk_metat sl venv l t - = let mk = MetaGraft VMap.empty in - Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))) +(* let mk_meta2 sl venv l + * = let mk = MetaGraft VMap.empty in + * let t = Metavar ((l, "_"), mk, ref (MetaUnset (venv, None, sl))) + * in (Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))), t) + * let mk_meta sl venv l + * = let mk = MetaGraft VMap.empty in + * let t = Metavar ((l, "_"), mk, ref (MetaUnset (venv, None, sl))) + * in Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))) + * let mk_meta_dummy = mk_meta (ScopeLevel(-1)) + * let mk_metat sl venv l t + * = let mk = MetaGraft VMap.empty in + * Metavar ((l, "_"), mk, ref (MetaUnset (venv, Some t, sl))) *) type value = lexp -type fvars = lexp SMap.t (* Free vars (with type) we need to generalize. *) +(* Free vars (with type) we need to generalize. *) +(* type fvars = lexp SMap.t *) (* Each element of a unification constraint is a pair of expresions that * need to be unified together with a boolean indicating whether this might be * algorithmically unifiable. I.e. if the boolean is false, then there's no * point calling lexp_unify on it because we know it will just re-add the same * constraint. *) -type unify_cond = - | UnifyNever (* Can't be resolved by unification. *) - | UnifyWhenInst of metavar ref (* Needs ref to be instantiated. *) - | UnifyMaybe (* Not clear when. *) -type unify_csts = (lexp * lexp * unify_cond) list -type constraints = unify_csts - -type pending = constraints +(* type unify_cond = + * | UnifyNever (\* Can't be resolved by unification. *\) + * | UnifyWhenInst of metavar ref (\* Needs ref to be instantiated. *\) + * | UnifyMaybe (\* Not clear when. *\) + * type unify_csts = (lexp * lexp * unify_cond) list + * type constraints = unify_csts + * + * type pending = constraints *) let id x = x (* Combine two substitutions. I.e. e = s(s'(e))). *) -let lexp_subst_subst s s' = - let s' = VMap.map (fun e -> mk_susp s e) s' in - VMap.fold (fun v e s -> if VMap.mem v s - then (internal_error "Overlapping substs") - else VMap.add v e s) - s s' +(* let lexp_subst_subst s s' = + * let s' = VMap.map (fun e -> mk_susp s e) s' in + * VMap.fold (fun v e s -> if VMap.mem v s + * then (internal_error "Overlapping substs") + * else VMap.add v e s) + * s s' *) let lexp_max_sort (k1, k2) = match k1,k2 with @@ -212,18 +204,18 @@ let lexp_max_sort (k1, k2) = (* Invert a substitution. I.e. return s' such that s'(s(e))=e. * It is allowed to presume that e is closed in `venv'. *) -exception Lexp_subst_inv -let lexp_subst_inv venv s = - VMap.fold (fun v e s -> - try let _ = VMap.find v venv in - match e with - (* | Var _ when e = var_bottom -> s *) - | Var (l,v') -> if VMap.mem v' s then raise Lexp_subst_inv - else VMap.add v' (Var (l,v)) s - | _ -> raise Lexp_subst_inv - (* `v' is not in `venv' so it won't appear in `e'. *) - with Not_found -> s) - s VMap.empty +(* exception Lexp_subst_inv + * let lexp_subst_inv venv s = + * VMap.fold (fun v e s -> + * try let _ = VMap.find v venv in + * match e with + * (\* | Var _ when e = var_bottom -> s *\) + * | Var (l,v') -> if VMap.mem v' s then raise Lexp_subst_inv + * else VMap.add v' (Var (l,v)) s + * | _ -> raise Lexp_subst_inv + * (\* `v' is not in `venv' so it won't appear in `e'. *\) + * with Not_found -> s) + * s VMap.empty *) let rec lexp_location e = match e with @@ -231,80 +223,17 @@ let rec lexp_location e = | SortLevel (SLsucc e) -> lexp_location e | SortLevel (SLn _) -> dummy_location | Imm s -> sexp_location s - | Var (l,_) -> l + | Var ((l,_),_) -> l | Builtin _ -> dummy_location | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l | Lambda (_,(l,_),_,_) -> l | Call (f,_) -> lexp_location f - | Inductive ((l,_),_,_) -> l + | Inductive (l,_,_,_) -> l | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l - | Susp (_, e) -> lexp_location e - | Metavar ((l,_),_,_) -> l - -(* Apply alpha-renaming to all variables in `e'. *) -let rec lexp_alpha s e = - match e with - | (Sort (_, (StypeLevel | StypeOmega | Stype (SortLevel (SLn _)))) - | Imm _ | Builtin _ | SortLevel (SLn _)) -> e - | Sort (l, Stype e) -> Sort (l, Stype (lexp_alpha s e)) - | SortLevel (SLsucc e) -> SortLevel (SLsucc (lexp_alpha s e)) - | Var (l,v) -> (try Var (l, VMap.find v s) with Not_found -> e) - | Let (l,decls,body) - -> let (decls',s') = List.fold_left (fun (d,s) ((l,v), e, t) -> - let v' = copy_var v in - (((l,v'), e, t) :: d, VMap.add v v' s)) - ([], s) - decls in - Let (l, List.map (fun (v, e, t) -> (v, lexp_alpha s' e, lexp_alpha s' t)) - decls, lexp_alpha s' body) - | Arrow (ak, None, t1, l, t2) - -> Arrow (ak, None, lexp_alpha s t1, l, lexp_alpha s t2) - | Arrow (ak, Some (l',v), t1, l, t2) - -> let v' = copy_var v in - Arrow (ak, Some (l',v'), lexp_alpha s t1, l, - lexp_alpha (VMap.add v v' s) t2) - | Lambda (ak, (l,v), t, e) - -> let v' = copy_var v in - Lambda (ak, (l,v'), lexp_alpha s t, - lexp_alpha (VMap.add v v' s) e) - | Call (f,args) - -> Call (lexp_alpha s f, List.map (fun (ak,e) -> (ak, lexp_alpha s e)) args) - | Inductive (id, t, branches) - -> Inductive (id, lexp_alpha s t, - SMap.map (lexp_alpha s) branches) - | Cons (e,tag) -> Cons (lexp_alpha s e, tag) - | Case (l,e,t,branches,default) - -> Case (l, lexp_alpha s e, lexp_alpha s t, - SMap.map (fun (l, args, branch) -> - let args' = List.map (fun (ak,(l,a)) - -> (ak, (l, copy_var a))) - args in - (l, args', - lexp_alpha (List.fold_left2 (fun s (_,(_,v)) (_,(_,v')) - -> VMap.add v v' s) - s args args') - branch)) - branches, - match default with Some e -> Some (lexp_alpha s e) | None -> None) - | Susp (env, e) -> - VMap.iter (fun v _ -> - if VMap.mem v s - then (internal_error "overlapping alpha and subst!!") - else ()) - env; - Susp (VMap.map (lexp_alpha s) env, lexp_alpha s e) - | Metavar (_, MetaFoF, _) -> e - | Metavar ((l,_), MetaGraft subst, r) - -> match !r with - | MetaSet e -> lexp_alpha s (mk_susp subst e) - (* FIXME: filter out vars not in `venv'. *) - (* FIXME: Signal a warning if not all the vars are filtered out, - * because I really wonder when that might happen. *) - | _ -> mk_susp (VMap.map (fun v -> Var (dummy_location, v)) s) e - -let lexp_copy e = lexp_alpha VMap.empty e + (* | Susp (_, e) -> lexp_location e + * | Metavar ((l,_),_,_) -> l *) let builtin_reduce b args arg = match b,args,arg with ===================================== typer-mode.el ===================================== --- a/typer-mode.el +++ b/typer-mode.el @@ -134,6 +134,7 @@ ;; - "f x = e : t" (smie-precs->prec2 '((assoc ";") + (nonassoc "=") (assoc ",") (left "||") (left "&&") View it on GitLab: https://gitlab.com/monnier/typer/commit/f15cc0c5b0feb2a3b584404cbc3f703c402…

1 0

[Git][monnier/typer] Deleted branch work
by Stefan 14 Fév '16

14 Fév '16

Stefan deleted branch work at Stefan / Typer

1 0

[Git][monnier/typer][master] * GNUmakefile: Rename since it uses GNU extensions
by Stefan 14 Fév '16

14 Fév '16

Stefan pushed to branch master at Stefan / Typer Commits: 7b2de3d5 by Stefan Monnier at 2016-02-14T16:03:18-05:00 * GNUmakefile: Rename since it uses GNU extensions - - - - - 1 changed file: - Makefile → GNUmakefile Changes: ===================================== Makefile → GNUmakefile ===================================== --- a/Makefile +++ b/GNUmakefile @@ -1,3 +1,4 @@ +RM=rm -f TEST_FILES := $(wildcard ./tests/*_test.ml) View it on GitLab: https://gitlab.com/monnier/typer/commit/7b2de3d5ecccf718f0d5ba374a33be440b8…

1 0

[Git][monnier/typer][master] 7 commits: new make file
by Stefan 14 Fév '16

14 Fév '16

Stefan pushed to branch master at Stefan / Typer Commits: a90614fc by Pierre Delaunay at 2016-01-18T11:54:44-05:00 new make file - - - - - 908e455e by Pierre Delaunay at 2016-01-21T09:58:20-05:00 new make file - - - - - f509e8a2 by Pierre Delaunay at 2016-01-22T10:42:40-05:00 Merge remote-tracking branch 'origin/master' into work - - - - - 6cb6f695 by Pierre Delaunay at 2016-01-22T13:34:33-05:00 utest_main + Makefile update - - - - - 482a5aab by Pierre Delaunay at 2016-01-22T14:04:28-05:00 utest_main + Makefile update - - - - - ad00ffbd by Pierre Delaunay at 2016-01-22T14:08:57-05:00 Merge branch 'work' of gitlab.com:monnier/typer into work Conflicts: Makefile tests/utest_main.ml - - - - - 4e901ec3 by Stefan Monnier at 2016-02-14T15:57:51-05:00 * .gitignore: Add ChangeLog. - - - - - 32 changed files: - .gitignore - − GNUmakefile - + Makefile - + README.md - manual.texi → doc/manual.texi - + samples/lexer_test.typer - + samples/pexp_test.typer - + samples/pretoken_test.typer - + samples/token_test.typer - elaborate.ml → src/elaborate.ml - + src/fmt.ml - javascript.ml → src/javascript.ml - lexer.ml → src/lexer.ml - lexp.ml → src/lexp.ml - main.ml → src/main.ml - myers.ml → src/myers.ml - pervasive.typer → src/pervasive.typer - pexp.ml → src/pexp.ml - prelexer.ml → src/prelexer.ml - sexp.ml → src/sexp.ml - test.typer → src/test.typer - ulexp.ml → src/ulexp.ml - unify.ml → src/unify.ml - util.ml → src/util.ml - + tests/debug.ml - + tests/dummy1_test.ml - + tests/dummy2_test.ml - + tests/dummy_test.ml - + tests/lexer_debug.ml - + tests/prelexer_debug.ml - + tests/primary_debug.ml - + tests/utest_main.ml Changes: ===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +ChangeLog typer *.elc *.annot @@ -10,3 +11,6 @@ typer *.aux manual.?? *.info +_build/ +*~ +#*# ===================================== GNUmakefile deleted ===================================== --- a/GNUmakefile +++ /dev/null @@ -1,37 +0,0 @@ -OCAMLC = ocamlc -OCAMLDEP = ocamldep -OCAMLC_FLAGS = -annot -g -OCAMLLD = ocamlc -OCAMLLD_FLAGS = -g -RM = rm -f - -FILES = $(wildcard *.ml) - -# OCAMLC wants its object files in the right order so the modules get -# initialized correctly. Ideally `make' should do this job (it already has -# the dependency info and knows all too weel how to do a topological sort), -# but I don't know how to get `make' to do what I want, so I used some `sed' -# magic to massage the .depend in a form that `tsort' can take. -ORDERED_OBJECTS = $(shell sed -e '/$[^ :]*\.cmo$ *:/{ : start; s/^$[^ :]*$ *: *$[^ :\\][^ :\\]*$/\2 \1\n\1:/; t loop2; /\\$$/{; N; s/\\.//; b start}; d; : loop2; P; D}; d' .depend | tsort) - -all: typer - -%.cmi %.cmo: %.ml - $(OCAMLC) $(OCAMLC_FLAGS) -c $< - -clean: - $(RM) *.cmo *.cmi *.cmx *.annot - -typer: $(ORDERED_OBJECTS) #$(FILES:.ml=.cmo) - $(OCAMLLD) $(OCAMLLD_FLAGS) -o $@ $(ORDERED_OBJECTS) - -.PHONY: test -# The "OCAMLRUNPARAM=-b" is so as to cause ocamlrun to print a backtrace -# when an exception is not caught. -test: typer - OCAMLRUNPARAM=-b ./typer test.typer - -depend: - $(OCAMLDEP) $(FILES) > .depend - --include .depend ===================================== Makefile ===================================== --- /dev/null +++ b/Makefile @@ -0,0 +1,34 @@ + +TEST_FILES := $(wildcard ./tests/*_test.ml) + +all: typer debug tests + +typer: + ocamlbuild src/main.byte + mv _build/src/main.byte _build/typer # move and rename executable + +debug: + ocamlbuild tests/prelexer_debug.byte -I src # debug print + mv _build/tests/prelexer_debug.byte _build/prelexer_debug + ocamlbuild tests/lexer_debug.byte -I src # debug print + mv _build/tests/lexer_debug.byte _build/lexer_debug + +tests: + # Build tests + $(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.byte,$(test))) -I src;) + + # Run tests + ocamlbuild tests/utest_main.byte + ./_build/tests/utest_main.byte + +# Make language doc +doc-tex: + texi2pdf ./doc/manual.texi --pdf --build=clean + +# Make implementation doc +doc-ocaml: + ocamldoc + +.PHONY: typer +.PHONY: debug +.PHONY: tests ===================================== README.md ===================================== --- /dev/null +++ b/README.md @@ -0,0 +1,30 @@ + +Typer +===== + +# How to build Typer + +## Requirement + +* Ocaml 4.01 + +## Build + +By default ocamlbuild creates a '_build' folder which holds all the compiled files. + +* make typer: build typer interpreter 'typer' +* make debug: build typer with debug info 'debug' +* make tests: run interpreter's tests '/.tests/utest_main.byte' + +# Directory layout + +* src/ interpreter's source +* doc/ interpreter's doc files +* sample/ typer code sample for testing purposes +* tests/ ocaml test files + +# Emacs files + + /typer-mode.el + + \ No newline at end of file ===================================== manual.texi → doc/manual.texi ===================================== --- a/manual.texi +++ b/doc/manual.texi ===================================== samples/lexer_test.typer ===================================== --- /dev/null +++ b/samples/lexer_test.typer @@ -0,0 +1,39 @@ +%% This file check if typer recognize correctly tokens + +%% builtin types +%% ---------------- + +%% String +a = "The answer is 42"; + +%% Integer +b = 11; + +%% Float +c = 3.14; + +%% Something +C = 3.14.14; + + +%% Case + +case (a,b) + | (Foo,Foo) => 3.14 + | (Bar,Bar) => 3.15 +;; + + +%% Stuff +%% ---------------- + +%% Epsilon + +%% Block + + +%% Node +%% -> Composed expression + +%% Symbol +%% --> Everything else ===================================== samples/pexp_test.typer ===================================== --- /dev/null +++ b/samples/pexp_test.typer @@ -0,0 +1,50 @@ +%% +%% Proto lambda-expressions, half-way between Sexp and Lexp. +%% + +%% ppat +%% ----------------- + +%% Ppatany + +%% Ppatvar + +%% Ppatcons + + +%% pexp +%% ----------------- + +%% Pimm +%% + +%% Pvar +%% + +%% Phastype +%% + +%% Pmetavar +%% + +%% Plet +%% + +%% Parrow +%% + +%% Plambda +%% + +%% Pcall +%% + +%% Pinductive +%% + +%% Pcons +%% + +%% Pcase +%% + ===================================== samples/pretoken_test.typer ===================================== --- /dev/null +++ b/samples/pretoken_test.typer @@ -0,0 +1,15 @@ +%% This file check if typer recognize correctly pretokens + +%% Preblock +%% --> hum, hum + + +%% Prestring +%% --> String variable +b = "The answer is 42"; + + +%% Pretoken +%% --> Everything else + +a = 3; \ No newline at end of file ===================================== samples/token_test.typer ===================================== --- /dev/null +++ b/samples/token_test.typer @@ -0,0 +1,28 @@ +%% This file check if typer recognize correctly tokens + +%% builtin types +%% ---------------- + +%% String +a = "The answer is 42"; + +%% Integer +b = 11; + +%% Float +c = 3.14; + + +%% Stuff +%% ---------------- + +%% Epsilon + +%% Block + + +%% Node +%% -> Composed expression + +%% Symbol +%% --> Everything else ===================================== elaborate.ml → src/elaborate.ml ===================================== --- a/elaborate.ml +++ b/src/elaborate.ml ===================================== src/fmt.ml ===================================== --- /dev/null +++ b/src/fmt.ml @@ -0,0 +1,49 @@ +(* + * Kiwi Compiler + * + * Pierre Delaunay + * + * --------------------------------------------------------------------------- + * + * + *) + + +(****************************************************************************** + * Print helper + * + * Declare new print function which align printed values. + * + *****************************************************************************) + +(* Compute the number of character needed to print an integer*) +let str_size_int value = + (int_of_float (log10 (float value))) + 1 +;; + +(* print n char 'c' *) +let rec make_line c n = + print_string c; + if n >= 1 then (make_line c (n - 1)); +;; + +(* print an integer right-aligned *) +let ralign_print_int value nb = + make_line " " (nb - (str_size_int value)); + print_int value; +;; + +let lalign_print_int value nb = + print_int value; + make_line " " (nb - (str_size_int value)); +;; + +let ralign_print_string str nb = + make_line " " (nb - String.length str); + print_string str; +;; + +let lalign_print_string str nb = + print_string str; + make_line " " (nb - String.length str); +;; ===================================== javascript.ml → src/javascript.ml ===================================== --- a/javascript.ml +++ b/src/javascript.ml ===================================== lexer.ml → src/lexer.ml ===================================== --- a/lexer.ml +++ b/src/lexer.ml ===================================== lexp.ml → src/lexp.ml ===================================== --- a/lexp.ml +++ b/src/lexp.ml ===================================== main.ml → src/main.ml ===================================== --- a/main.ml +++ b/src/main.ml ===================================== myers.ml → src/myers.ml ===================================== --- a/myers.ml +++ b/src/myers.ml ===================================== pervasive.typer → src/pervasive.typer ===================================== --- a/pervasive.typer +++ b/src/pervasive.typer ===================================== pexp.ml → src/pexp.ml ===================================== --- a/pexp.ml +++ b/src/pexp.ml ===================================== prelexer.ml → src/prelexer.ml ===================================== --- a/prelexer.ml +++ b/src/prelexer.ml ===================================== sexp.ml → src/sexp.ml ===================================== --- a/sexp.ml +++ b/src/sexp.ml ===================================== test.typer → src/test.typer ===================================== --- a/test.typer +++ b/src/test.typer ===================================== ulexp.ml → src/ulexp.ml ===================================== --- a/ulexp.ml +++ b/src/ulexp.ml ===================================== unify.ml → src/unify.ml ===================================== --- a/unify.ml +++ b/src/unify.ml ===================================== util.ml → src/util.ml ===================================== --- a/util.ml +++ b/src/util.ml ===================================== tests/debug.ml ===================================== --- /dev/null +++ b/tests/debug.ml @@ -0,0 +1,139 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * --------------------------------------------------------------------------- + * + * Description: + * Provide helper functions to print out + * extracted token + * extracted expression + * + * --------------------------------------------------------------------------- *) + +(* removes some warnings *) +open Util + +(* print debug info *) +let print_loc (loc : Util.location) = + print_string loc.file; + print_string ": ln "; + Fmt.ralign_print_int loc.line 3; + print_string ", cl "; + Fmt.ralign_print_int loc.column 3; +;; + + +(*open Token +open Token + +(* Print token with debug info *) +let print_token tok = + (* Shortcut *) + let lalign str = Fmt.lalign_print_string str 20 in + + (* When we need to print only the name *) + let quick_print name loc = + lalign name; + print_string "["; print_loc loc; print_string "] "; + print_string "\n" in + + let long_print name loc elem = + lalign name; + print_string "["; print_loc loc; print_string "] "; + print_string "'"; + print_string elem; + print_string "'\n" in + + let print_kwd name loc ch = + lalign name; + print_string "["; print_loc loc; print_string "] "; + print_char ch; + print_string "\n" in + + let print_float name loc ch = + lalign name; + print_string "["; print_loc loc; print_string "] "; + print_float ch; + print_string "\n" in + + let print_integer name loc ch = + lalign name; + print_string "["; print_loc loc; print_string "] "; + print_int ch; + print_string "\n" in + + (* Print tokens *) + match tok with + | Token.Arw(loc, str) -> long_print "Arw" loc str; + | Token.Assign(loc, str) -> long_print "Assign" loc str; + | Token.Colon(loc, str) -> long_print "Colon" loc str; + | Token.Lambda(loc) -> quick_print "Lambda" loc; + | Token.Case(loc) -> quick_print "Case" loc; + | Token.Inductive(loc) -> quick_print "Inductive" loc; + | Token.Let(loc) -> quick_print "Let" loc; + | Token.In(loc) -> quick_print "In" loc; + | Token.Ident(loc, str) -> long_print "Identifier" loc str; + | Token.Kwd(loc, ch) -> print_kwd "Kwd" loc ch; + | Token.Float(loc, value) -> print_float "Float" loc value; + | Token.Integer(loc, value) -> print_integer "Integer" loc value; + | Token.String(loc, str) -> long_print "String" loc str; +;; + +(* Lexer print + *--------------------------------------------------*) + +(* Print the list of token *) +let debug_lex file_name = + + let file_stream = open_in file_name in + + (* Create a stream of tokens *) + let lex_stream = Lexer.lex file_name (Stream.of_channel file_stream) in + + (* Print each tokens *) + Stream.iter (fun tok -> print_token tok) lex_stream; +;; + +(* Parser print + *--------------------------------------------------(**) +let debug_parser file_name = + + let file_stream = open_in file_name in + + (* Create a stream of tokens *) + let lex_stream = Lexer.lex file_name (Stream.of_channel file_stream) in + + (* Parse token's stream *) + Toplevel.main_loop lex_stream +;; **) + + +let main () = + debug_lex "./typer_test/lexer_test.typer"; (**) + + (*debug_parser "kiwi_code/lexer_test.kwi";**) +;; + +main ();*) ===================================== tests/dummy1_test.ml ===================================== --- /dev/null +++ b/tests/dummy1_test.ml @@ -0,0 +1,13 @@ + +open Util +open Prelexer +open Debug + +let main () = + + let file_name = (Sys.argv.(1) ^ "/samples/lexer_test.typer") in + prelex_file file_name +;; + +main () +;; \ No newline at end of file ===================================== tests/dummy2_test.ml ===================================== --- /dev/null +++ b/tests/dummy2_test.ml @@ -0,0 +1,13 @@ + +open Util +open Prelexer +open Debug + +let main () = + + let file_name = (Sys.argv.(1) ^ "/samples/lexer_test.typer") in + prelex_file file_name +;; + +main () +;; \ No newline at end of file ===================================== tests/dummy_test.ml ===================================== --- /dev/null +++ b/tests/dummy_test.ml @@ -0,0 +1,16 @@ + +open Util +open Prelexer +open Debug + +let main () = + + print_endline Sys.argv.(0); + print_endline Sys.argv.(1); + + let file_name = (Sys.argv.(1) ^ "/samples/lexer_test.typer") in + prelex_file file_name +;; + +main () +;; \ No newline at end of file ===================================== tests/lexer_debug.ml ===================================== --- /dev/null +++ b/tests/lexer_debug.ml @@ -0,0 +1,131 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * --------------------------------------------------------------------------- + * + * Description: + * print out read Sexp (Syntactic expression) + * i.e lexer's tokens + * + * --------------------------------------------------------------------------- *) + +open Util +open Prelexer +open Sexp +open Lexer + +let default_stt = + let stt = Array.create 256 false + in stt.(Char.code ';') <- true; + stt.(Char.code ',') <- true; + stt.(Char.code '(') <- true; + stt.(Char.code ')') <- true; + stt + + +let rec debug_sexp_print sexp = + let print_loc = Debug.print_loc in + match sexp with + | Epsilon + -> print_string "Epsilon()\n" (* "ε" *) + + | Block(loc, pts, _) + -> print_string "Block: \t{"; + print_string "["; print_loc loc; print_string "]\t"; + pretokens_print pts; + print_string " }" + + | Symbol(loc, name) + -> print_string "Symbol: \t"; + print_string "["; print_loc loc; print_string "]\t"; + print_string name + + | String(loc, str) + -> print_string "String: \t"; + print_string "["; print_loc loc; print_string "]\t"; + print_string "\""; print_string str; print_string "\"" + + | Integer(loc, n) + -> print_string "Integer: \t"; + print_string "["; print_loc loc; print_string "]\t"; + print_int n + + | Float(loc, x) + -> print_string "Float: \t"; + print_string "["; print_loc loc; print_string "]\t"; + print_float x + + | Node(f, args) + -> print_string "Node: \t"; + print_string "(";sexp_print f; + List.iter (fun sexp -> print_string " "; sexp_print sexp) + args; + print_string ")" +;; + +let debug_sexp_print_all tokens = + List.iter (fun pt -> + print_string " "; + debug_sexp_print pt; + print_string "\n"; + ) + tokens +;; + +let main () = + (* + * print tokens/sexp of the file given as first arg + * + ********************************************************) + + let file = Sys.argv.(1) in + print_string file; + print_string "\n"; + + (* Todo read file from prog args *) + (* get pretokens*) + let pretoks = prelex_file file in + + (* get tokens *) + let toks = lex default_stt pretoks in + + (* print tokens *) + debug_sexp_print_all toks +;; + +main ();; + +(* Command Line * ) +let command = + Command.basic + ~summary:"Print Compiler Debug Info" + ~readme:(fun () -> "More detailed information") + Command.Spec.(empty +> anon ("filename" %: string)) + main + +let () = + Command.run ~version:"1.0" ~build_info:"RWO" command * *) + +(*(main Sys.argv.(1));;*) ===================================== tests/prelexer_debug.ml ===================================== --- /dev/null +++ b/tests/prelexer_debug.ml @@ -0,0 +1,73 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * --------------------------------------------------------------------------- + * + * Description: + * print out read pretoken + * + * --------------------------------------------------------------------------- *) + +open Util +open Prelexer +open Debug + +(* TODO: add a Prestring and a Preblock example into the test.typer file *) +let rec debug_pretokens_print pretokens = + List.iter (fun pt -> + print_string " "; + match pt with + | Preblock(loc, pts,_) + -> print_string "Preblock:\t"; + print_string "["; print_loc loc; print_string "]\t"; + print_string "{"; + pretokens_print pts; + print_string " }" + + | Pretoken(loc, str) + -> print_string "Pretoken:\t"; + print_string "["; print_loc loc; print_string "]\t"; + print_string str; + print_string "\n" + + | Prestring(loc, str) + -> print_string "Prestring:\t"; + print_string "["; print_loc loc; print_string "]\t"; + print_string "\""; + print_string str; + print_string "\"\n"; + ) + pretokens + +let main () = + let file = Sys.argv.(1) in + print_string file; + print_string "\n"; + + let arr = prelex_file file in + debug_pretokens_print arr +;; + +main (); ===================================== tests/primary_debug.ml ===================================== --- /dev/null +++ b/tests/primary_debug.ml @@ -0,0 +1,133 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * --------------------------------------------------------------------------- + * + * Description: + * print out read pexp (primary expression) + * + * --------------------------------------------------------------------------- *) + + +let rec debug_pexp_print pexp = + match pexp with + | Pimm(exp) + -> + | Pvar(p) + -> + | Phastype(l, exp2, exp1) + -> +;; + +let debug_pexp_print_all pexp = + List.iter (fun pt -> + print_string " "; + debug_pexp_print pt; + print_string "\n"; + ) + pexp +;; + +(* Language config *) + +let default_stt = + let stt = Array.create 256 false + in stt.(Char.code ';') <- true; + stt.(Char.code ',') <- true; + stt.(Char.code '(') <- true; + stt.(Char.code ')') <- true; + stt +;; + +let default_grammar : grammar + = List.fold_left (fun g (n, ll, rl) -> SMap.add n (ll, rl) g) + SMap.empty + [("^", Some 171, Some 159); + ("/", Some 148, Some 160); + ("-", Some 92, Some 110); + ("+", Some 93, Some 111); + ("!=", Some 94, Some 75); + (">=", Some 95, Some 76); + ("<=", Some 96, Some 77); + (">", Some 97, Some 78); + ("<", Some 98, Some 79); + ("&&", Some 64, Some 81); + ("||", Some 39, Some 51); + (",", Some 26, Some 26); + ("then", Some 1, Some 0); + ("=", Some 99, Some 80); + ("type", None, Some 27); + (";", Some 15, Some 15); + ("*", Some 137, Some 137); + (":", Some 173, Some 115); + ("]", Some 3, None); + ("->", Some 126, Some 114); + ("=>", Some 126, Some 113); + ("≡>", Some 126, Some 112); + ("in", Some 2, Some 53); + ("else", Some 0, Some 52); + ("|", Some 40, Some 40); + (")", Some 4, None); + ("[", None, Some 3); + ("case", None, Some 28); + ("lambda", None, Some 126); + ("letrec", None, Some 2); + ("let", None, Some 2); + ("if", None, Some 1); + ("(", None, Some 4); + ] +;; + +let main filename () = + + (* Todo read file from prog args *) + (* get pretokens*) + let pretoks = prelex_file filename in + + (* get sexp/tokens *) + let toks = lex default_stt pretoks in + + (* get pexp *) + let pxp = sexp_parse_all grm toks limit in + + (* print pxp *) + debug_pexp_print_all pxp +;; + +(* Command Line *) +open Core.Std + +let command = + Command.basic + ~summary:"Print Compiler Debug Info" + ~readme:(fun () -> "More detailed information") + Command.Spec.(empty +> anon ("filename" %: string)) + main + +let () = + Command.run ~version:"1.0" ~build_info:"RWO" command + + + ===================================== tests/utest_main.ml ===================================== --- /dev/null +++ b/tests/utest_main.ml @@ -0,0 +1,92 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * --------------------------------------------------------------------------- + * + * Description: + * Basic utest program run all tests + * + * --------------------------------------------------------------------------- *) + + +let cut_name str = + String.sub str 0 (String.length str - 10) +;; + +(* search *_test.byte executable en run them + Usage: + ./utest_main tests_folder root_folder *) +let main () = + let arg_n = Array.length Sys.argv in + + (* read where tests files are*) + let folder = (if arg_n > 1 then Sys.argv.(1) else "./_build/tests/") in + + print_string " \n"; + print_string " Running Unit Tests \n"; + print_string " \n"; + (*print_string ("[ ] Test folder: " ^ folder ^ "\n"); *) + + (* get tests files *) + let files = Sys.readdir folder in + let files_n = Array.length files in + + let exit_code = ref 0 in + let failed_test = ref 0 in + let tests_n = ref 0 in + let root_folder = (if arg_n > 2 then Sys.argv.(2) else "./") in (* /_build/tests/ *) + + for i = 0 to files_n - 1 do + (* Check if file is a test => if it is run it *) + (if Filename.check_suffix files.(i) "_test.byte" then begin + + tests_n := !tests_n + 1; + + print_string " " ; + print_int !tests_n; + print_endline (") " ^ (cut_name files.(i))); + print_endline "[RUN ]"; + + exit_code := Sys.command (folder ^ files.(i) ^ " " ^ root_folder); + + if !exit_code <> 0 then begin + print_string "[ FAIL]\n" ; + print_endline " =========== TEST FAILURE ==========="; + failed_test := !failed_test + 1; + end + else + print_string "[ OK]\n" ; + end) + done; + + print_string "\n\n\n"; + print_endline " =========== Test Summary ===========\n"; + print_string " Test Ran : "; print_int !tests_n; + print_string "\n Test Failed : "; print_int !failed_test; + print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); + print_endline "\n =========== Test Summary ===========\n"; +;; + +main (); View it on GitLab: https://gitlab.com/monnier/typer/compare/a547bdb886d2cdaf6ed20561726b85ba7b…

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Février 2016