Stefan pushed to branch master at Stefan / Typer
Commits: a93ade4b by Stefan Monnier at 2016-05-11T23:10:29-04:00 Rename ityper to typer
- - - - -
3 changed files:
- GNUmakefile - src/REPL.ml - − src/main.ml
Changes:
===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -7,7 +7,7 @@ TEST_FILES := $(wildcard ./tests/*_test.ml) OBFLAGS = -build-dir _build # COMPILE_MODE = native
-all: ityper typer debug tests-build +all: typer debug tests-build
ifeq ($(OS), Windows_NT) # Windows need '-r' and building to native can be problematic (linking error) @@ -20,13 +20,6 @@ COMPILE_MODE = byte
-typer: - # ============================ - # Build typer - # ============================ - ocamlbuild src/main.$(COMPILE_MODE) $(OBFLAGS) - @mv _build/src/main.$(COMPILE_MODE) _build/typer - # debug file eval debug: # ============================ @@ -36,12 +29,12 @@ debug: @mv _build/src/debug_util.$(COMPILE_MODE) _build/debug_util
# interactive typer -ityper: +typer: # ============================ - # Build ityper + # Build typer # ============================ ocamlbuild src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/src/REPL.$(COMPILE_MODE) _build/ityper + @mv _build/src/REPL.$(COMPILE_MODE) _build/typer
tests-build: # ============================ @@ -68,17 +61,17 @@ doc-ocaml: clean: -rm -rf _build
-.PHONY: ityper typer debug tests +.PHONY: typer debug tests
run/debug_util: @./_build/debug_util ./samples/test__.typer -fmt-type=off
-run/ityper: - @./_build/ityper +run/typer: + @./_build/typer
run/tests: @./_build/tests/utests --verbose= 1
-run/ityper-file: - @./_build/ityper ./samples/test__.typer +run/typer-file: + @./_build/typer ./samples/test__.typer
===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -26,7 +26,7 @@ this program. If not, see http://www.gnu.org/licenses/. *) * * Example: * - * $./_build/ityper [files] + * $./_build/typer [files] * In[ 1] >> sqr = lambda x -> x * x; * In[ 2] >> (sqr 4); * Out[ 2] >> 16 @@ -54,6 +54,7 @@ open Builtin
open Env open Debruijn +module TC = Typecheck
(* how to handle arrow keys ? *) let _history = ref [] @@ -132,6 +133,8 @@ let ieval lexps rctx = let _ieval f str lctx rctx = let pres = (f str) in let sxps = lex default_stt pres in + (* FIXME: This is too eager: it prevents one declaration from changing + * the grammar used in subsequent declarations. *) let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in
(* Different from usual typer *) @@ -156,7 +159,7 @@ let _help_msg = %who (%w) : print runtime environment %info (%i) : print elaboration environment %calltrace (%ct): print call trace of last call - %readfile : read a typer/ityper file + %readfile : read a Typer file %help (%h) : print help "
@@ -169,6 +172,8 @@ let readfiles files (i, lctx, rctx) prt = print_string " In["; ralign_print_int i 2; print_string "] >> "; print_string ("%readfile " ^ file); print_string "\n";));
+ (* FIXME: This should not use the "ieval" but the "eval" syntax, + * i.e. only accept a sequence of declarations at top-level. *) try let (ret, lctx, rctx) = ieval_file file lctx rctx in (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) with @@ -214,7 +219,7 @@ let rec repl i clxp rctx = let arg_files = ref []
-(* ./ityper [options] files *) +(* ./typer [options] files *) let arg_defs = [ (*"-I", Arg.String (fun f -> searchpath := f::!searchpath),
===================================== src/main.ml deleted ===================================== --- a/src/main.ml +++ /dev/null @@ -1,168 +0,0 @@ -(* main.ml --- Toplevel file for Typer. - -Copyright (C) 2011-2016 Free Software Foundation, Inc. - -Author: Stefan Monnier monnier@iro.umontreal.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/. *) - -(* open Printf *) -open Util -open Lexer -open Sexp -(* open Elaborate *) -(* open Javascript *) - -(* I think they shouldn't be here, but for now I use them. *) -(* open Lexp *) -open Prelexer -open Pexp -open Grammar -module TC = Typecheck - -(* Overview. - * - * The front-end is split into parsing and elaboration. - * Parsing (string -> pexp) is done in the following steps: - * - Prelexer (string -> pretokens): Get rid of comments, recognize - * strings, match braces, and split the rest into chunks separated by - * whitespace. This process is not influenced by the program - * being compiled. - * - Lexer (pretokens -> tokens): Split the pretokens into tokens. - * This recognizes floats, integers, and splits the few tokens that are - * "self-delimited" rather than being delimited by spaces - * (e.g. semi-colons, since ";;" is one pretoken but two tokens). - * This phase depends on the lexing rules that define which tokens are - * self-delimiting. Programs can change those rules. - * - Sexp (tokens -> sexp): Extract the structure using operator precedence - * parsing. The result is an S-expression. This phase depends on the - * operator precedences, which can be changed by the programs. - * - Pexp (sexp -> pexp): Assuming a Sexp represents a valid Typer - * expression, turn it into a specialized datatype for easier subsequent - * processing. This process is not influenced by the program - * being compiled. - * - * Elaboration (pexp -> lexp) is basically done in a single step, which is - * decomposed into a few different parts which are all run bit-by-bit in - * interleaved ways during elaboration: - * - Normalize: Perform β-reductions to normalize open terms. - * - Unify: Higher-order unification of `lexp' terms. May call the normalizer. - * - Eval: Call-by-value interpreter of closed lexp terms, with potential - * side-effects and all. - * - Elaborate: Expand macros and infer types. Will call the evaluator to - * perform macro expansion and the unification to infer the types. - * The result of the front-end is a term of type Lexp, a fairly normal - * explicitly typed lambda-calculus amenable to the usual - * compilation strategies. - * - * The middle-end is done in the following steps: - * - Type-erasure (lexp -> ulexp) erases all the type annotation and erasable - * arguments. - * - * The Javascript backend is done in the following steps: - * - Conversion (ulexp -> jsexp) turns a Ulexp into an abstract representation - * of a Javascript expression. - * - The output step then takes this Jsexp and turns it into a Javascript - * program. - *) - -(*************** The Top Level *********************) - -let process_typer_file sourcename choppable_suffix venv = - (* let targetbase = Filename.chop_suffix sourcename choppable_suffix in *) - let pretokens = prelex_file sourcename in - let tokens = lex default_stt pretokens in - (* sexp_print (Node (Symbol (dummy_location, "tokens"), tokens)); - * print_newline(); *) - - (* let js_file = open_out (sourcename ^ ".js") in - * - * output_string js_file (Javascript.intro ^ "\n\n"); *) - - let rec process_decl (grm, tokens, decls, pnames, delayed, senv, venv) = - let (sexp, rest) = sexp_parse_all grm tokens (Some ";") in - (* sexp_print e; print_newline(); *) - 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(); *) - (* print_string ": "; - * sexp_print (pexp_unparse (lexp_unparse t)); print_newline(); *) - (* print_newline(); *) - - - - (* let ule = Ulexp.optimisation_pass (Ulexp.from_lexp le) in - * Ulexp.pretty_print print_string ule; - * - * - * (let freevars = Ulexp.freevars ule in - * Ulexp.print_freevars freevars ; - * Ulexp.print_scc ule; - * ); - * - * - * print_string "\nJAVASCRIPT:\n "; - * - * print_jsstatement (output_string js_file) (translate_to_js (ule)); - * output_string js_file "\n\n"; - * - * output_jsexp (translate_to_js (ule)); - * - * - * (*jsexp_parse_to_console le;*) - * print_newline(); - * print_newline(); *) - - match rest with - | [] -> (decls, venv) - | _ -> process_decl (grm, rest, - pdecls @ decls, pnames, delayed, senv, venv) - in process_decl (default_grammar, tokens, - [], SMap.empty, None, [], venv) - (* ; close_out js_file *) - -let process_file filename venv = - if Filename.check_suffix filename ".typer" then - process_typer_file filename ".typer" venv - else - raise (Arg.Bad ("Unknown filetype: " ^ filename)) - -let (perv_decls, perv_venv) = process_file "pervasive.typer" None - -let _ = Arg.parse - [ - (* "-dpretty-term", Arg.Set print_pretty, - * "Pretty-print after preterm conversion"; *) - (* "-dno-pretty-term", Arg.Clear print_pretty, - * "Don't pretty-print after preterm conversion"; *) - (* "-dpretty-cons", Arg.Set print_constr, - * "Pretty-print after preterm conversion"; *) - (* "-dno-pretty-cons", Arg.Clear print_constr, - * "Don't pretty-print after preterm conversion"; *) - (* "-dverbose-pretty", Arg.Unit (fun () -> Print.set_pp_verbose true), - * "Use an extra-unambiguous pretty-printer syntax"; *) - (* "-use-typeof", Arg.Set do_verif_types, - * "Check types with typeof rather than infer them"; *) - ] - (fun s -> ignore (process_file s perv_venv)) - "Usage: typer [options] [files]\nOptions are:"
View it on GitLab: https://gitlab.com/monnier/typer/commit/a93ade4b22f00b07114f4865a3555181d4f1...
Afficher les réponses par date