Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Février 2016
- 4 participants
- 10 discussions
[Git][monnier/typer][master] 15 commits: sexp_parse_to_list + debugs in one files
by Setepenre 01 Mar '16
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
> 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
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
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
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
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
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
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
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
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