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@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@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@hec.ca + * Author: Stefan Monnier monnier@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@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@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@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@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/57a4f589c0c4dda04796fea8053dda038b6...