Stefan pushed to branch master at Stefan / Typer

Commits: 0bd0dac5 by Stefan Monnier at 2017-02-13T15:40:25-05:00 * src/sexp.ml (sexp): Remove Epsilon. Use empty Symbol instead

(epsilon, dummy_epsilon): New definitions. (sexp_string, sexp_location, sexp_name, sexp_parse.mk_node) (sexp_p_list, sexp_u_list, sexp_equal): * src/pexp.ml (pexp_parse, pexp_p_decls): * src/opslexp.ml (check', get_type): * src/lexp.ml (impossible): * src/lexer.ml (nexttoken.lexsym.mksym, nexttoken.lexsym.lexsym'): * src/debug.ml (debug_sexp_print): Adjust users accordingly.

- - - - -

7 changed files:

- src/debug.ml - src/lexer.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/sexp.ml - tests/lexp_test.ml

Changes:

===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -75,7 +75,7 @@ let rec debug_sexp_print sexp = print_string msg; print_string "["; loc_print loc; print_string "]\t" in match sexp with - | Epsilon + | Symbol(_, "") -> print_string "Epsilon " (* "ε" *)

| Block(loc, pts, _)

===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -1,6 +1,6 @@ (* lexer.ml --- Second half of lexical analysis of Typer.

-Copyright (C) 2011-2012, 2016 Free Software Foundation, Inc. +Copyright (C) 2011-2017 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -92,7 +92,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos else let rec lexsym bpos cpos = let mksym epos escaped - = if epos = bpos then Epsilon else + = if epos = bpos then epsilon {file;line;column=column+cpos} else let rawstr = string_sub name bpos epos in let str = if escaped then unescape rawstr else rawstr in hSymbol ({file;line;column=column+cpos}, str) in @@ -120,7 +120,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos when bpos != bp || (not is_last && CKseparate != (stt.(Char.code name.[bp']))) - || lf Epsilon != Epsilon + || not (lf dummy_epsilon = dummy_epsilon) -> let left = mksym bp escaped in let op = hSymbol ({file;line;column=column+cp}, "__" ^ String.sub name bp 1 ^ "__") in

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -129,7 +129,7 @@ let empty_meta_subst : meta_subst = VMap.empty

let empty_constraint : constraints = []

-let impossible = Imm Sexp.Epsilon +let impossible = Imm Sexp.dummy_epsilon

let builtin_size = ref 0

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -367,7 +367,7 @@ let rec check' meta_ctx erased ctx e = | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string - | Imm (Epsilon | Block (_, _, _) | Symbol _ | Node (_, _)) + | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level @@ -710,7 +710,7 @@ let rec get_type meta_ctx ctx e = | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string - | Imm (Epsilon | Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int + | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t, _) -> t | SortLevel _ -> DB.type_level | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (SLsucc e)))

===================================== 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, 2016 Free Software Foundation, Inc. +Copyright (C) 2011-2017 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -102,7 +102,6 @@ let rec pexp_parse (s : sexp) : pexp = match s with (* This is an internal error because Epsilon does not have any location * information so it needs to be caught elsewhere. *) - | Epsilon -> (internal_error "Epsilon in pexp_parse") | (Block _ | Integer _ | Float _ | String _) -> Pimm s (* | Symbol (l, "Type") -> Psort (l, Type) *) | Symbol (l, name) when String.length name > 0 && String.get name 0 == '?' @@ -265,7 +264,7 @@ and pexp_u_pat (p : ppat) : sexp = match p with

and pexp_p_decls e: pdecl list = match e with - | Epsilon -> [] + | Symbol (_, "") -> [] | Node (Symbol (_, ("_;_" | "_;" | ";_")), decls) -> List.concat (List.map pexp_p_decls decls) | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, pexp_parse t)] @@ -342,7 +341,7 @@ and pexp_u_decl decl =

and pexp_u_decls (ds: pdecl list) = match ds with - | [] -> Epsilon + | [] -> dummy_epsilon | [d] -> pexp_u_decl d | _ -> Node (Symbol (dummy_location, "_;_"), List.map pexp_u_decl ds)

===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -1,6 +1,6 @@ (* sexp.ml --- The Lisp-style Sexp abstract syntax tree.

-Copyright (C) 2011-2016 Free Software Foundation, Inc. +Copyright (C) 2011-2017 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -39,7 +39,6 @@ type integer = (* Num.num *) int type symbol = location * string

type sexp = (* Syntactic expression, kind of like Lisp. *) - | Epsilon | Block of location * pretoken list * location | Symbol of symbol | String of location * string @@ -47,6 +46,9 @@ type sexp = (* Syntactic expression, kind of like Lisp. *) | Float of location * float | Node of sexp * sexp list

+let epsilon l = Symbol (l, "") +let dummy_epsilon = epsilon dummy_location + (**************** Hash-consing symbols *********************)

module SHash = Hashtbl.Make (struct type t = string @@ -65,8 +67,8 @@ let emptyString = hString ""

let rec sexp_string sexp = match sexp with - | Epsilon -> "ε" (* "ε" *) | Block(_,pts,_) -> "{" ^ (pretokens_string pts) ^ " }" + | Symbol(_, "") -> "()" (* Epsilon *) | Symbol(_, name) -> name | String(_, str) -> """ ^ str ^ """ | Integer(_, n) -> string_of_int n @@ -86,17 +88,16 @@ let rec sexp_location s = | Integer (l, _) -> l | Float (l, _) -> l | Node (s, _) -> sexp_location s - | Epsilon -> (internal_error "Looking for the location of Epsilon")

let rec sexp_name s = match s with | Block _ -> "Block" + | Symbol (_, "") -> "ε" | Symbol _ -> "Symbol" | String _ -> "String" | Integer _ -> "Integer" | Float _ -> "Float" | Node _ -> "Node" - | Epsilon -> "Epsilon"

(*************** The Sexp Parser *********************)

@@ -128,24 +129,24 @@ let rec sexp_parse (g : grammar) (rest : sexp list) (List.rev ss))) in

let push_largs largs rargs closer = match List.rev rargs with - | [] -> if closer then Epsilon :: largs else largs + | [] -> if closer then dummy_epsilon :: largs else largs | e::es -> (match es with [] -> e | _ -> Node (e, es)) :: largs in

let mk_node op largs rargs closer = let args = List.rev (push_largs largs rargs closer) in match op with - | [] -> (match args with [] -> Epsilon - | [e] -> e - | e::es -> Node (e, es)) - | ss -> let headname = compose_symbol ss in - match (headname, args) with - (* FIXME: While it's uaulyl good to strip away parens, - * this makes assumptions about the grammar (i.e. there's - * a rule « exp ::= '(' exp ')' » ), and this is sometimes - * not desired (e.g. to distinguish "a b ⊢ c d" from - * "(a b) ⊢ (c d)"). *) - | ((_,"(_)"), [arg]) -> arg (* Strip away parens. *) - | _ -> Node (hSymbol (headname), args) in + | [] -> (match args with [] -> dummy_epsilon + | [e] -> e + | e::es -> Node (e, es)) + | ss -> let headname = compose_symbol ss in + match (headname, args) with + (* FIXME: While it's uaulyl good to strip away parens, + * this makes assumptions about the grammar (i.e. there's + * a rule « exp ::= '(' exp ')' » ), and this is sometimes + * not desired (e.g. to distinguish "a b ⊢ c d" from + * "(a b) ⊢ (c d)"). *) + | ((_,"(_)"), [arg]) -> arg (* Strip away parens. *) + | _ -> Node (hSymbol (headname), args) in

match rest with | (((Symbol ((l,name) as s)) as e)::rest') -> @@ -220,14 +221,14 @@ let sexp_parse_all grm tokens limit =

let sexp_p_list (s : sexp) (exceptions : string list) : sexp list = match s with - | Epsilon -> [] + | Symbol (_, "") -> [] | Node (Symbol (_, head), tail) when List.mem head exceptions -> [s] | Node (head, tail) -> head :: tail | _ -> [s]

let sexp_u_list (ss : sexp list) : sexp = match ss with - | [] -> Epsilon + | [] -> dummy_epsilon | [s] -> s | (s :: ss) -> Node (s, ss)

@@ -244,7 +245,6 @@ let sexp_parse_all_to_list grm tokens limit =

(* Sexp comparison, ignoring source-line-number info, used for tests. *) let rec sexp_equal s1 s2 = match s1, s2 with - | Epsilon, Epsilon -> true | Block (_, ps1, _), Block (_, ps2, _) -> pretokens_eq_list ps1 ps2 | Symbol (_, s1), Symbol (_, s2) -> s1 = s2 | String (_, s1), String (_, s2) -> s1 = s2

===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -37,7 +37,7 @@ open Builtin let ectx = default_ectx let rctx = default_rctx

-(*) +(* let _ = (add_test "LEXP" "lexp_print" (fun () ->

let dcode = "

View it on GitLab: https://gitlab.com/monnier/typer/commit/0bd0dac5c3e9a74fb52a8a4667118eca511b...