Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: 3981eea1 by Jonathan Graveline at 2018-08-22T23:29:34Z New character '@' introducing docstring
New primitive `Elab.debug-doc` mostly for testing docstring
Replaced `load_` by `load`
- - - - -
8 changed files:
- btl/builtins.typer - btl/pervasive.typer - btl/tuple.typer - src/elab.ml - src/eval.ml - src/lexer.ml - src/prelexer.ml - src/util.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -276,6 +276,8 @@ Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> Strin
Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int;
+Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String; + %%%% Unit test helper IO
%% Print message and/or fail (terminate)
===================================== btl/pervasive.typer ===================================== @@ -545,14 +545,14 @@ define-operator "<-" 80 96; %%%%
%% `List` is the type and `list` is the module (tuple) -list = load_ "btl/list.typer"; +list = load "btl/list.typer";
%% macro `do` for easier series of IO operation -do = let lib = load_ "btl/do.typer" in lib.do; +do = let lib = load "btl/do.typer" in lib.do;
%% various macro for tuple %% used by `case_` -tuple-lib = load_ "btl/tuple.typer"; +tuple-lib = load "btl/tuple.typer";
%% get nth element tuple-nth = tuple-lib.tuple-nth; @@ -566,7 +566,7 @@ _,_ = tuple-lib.make-tuple; Tuple = tuple-lib.tuple-type;
%% macro `case` for a little more complex pattern matching -case_ = let lib = load_ "btl/case.typer" in lib.case-macro; +case_ = let lib = load "btl/case.typer" in lib.case-macro;
%%%% plain-let %%%% Not recursive and not sequential @@ -574,10 +574,10 @@ case_ = let lib = load_ "btl/case.typer" in lib.case-macro; define-operator "plain-let" () 3; %% define-operator "in" 3 67;
-plain-let_in_ = let lib = load_ "btl/plain-let.typer" in lib.plain-let-macro; +plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro;
%%%% `case` at function level -_|_ = let lib = load_ "btl/polyfun.typer" in lib._|_; +_|_ = let lib = load "btl/polyfun.typer" in lib._|_;
%%%% Unit tests function for doing file
@@ -604,8 +604,8 @@ Test_file = macro (lambda args -> let in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) (lambda _ _ -> ret) (lambda _ -> ret) - %% `load_` is a special form and takes a Sexp rather than a real `String` - (lambda s -> quote (let lib = load_ (uquote (Sexp_string s)); in lib.exec-test)) + %% `load` is a special form and takes a Sexp rather than a real `String` + (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test)) (lambda _ -> ret) (lambda _ -> ret) (lambda _ -> ret))
===================================== btl/tuple.typer ===================================== @@ -174,6 +174,8 @@ make-tuple = macro (lambda args -> do { IO_return r; });
+%% + tuple-type = macro (lambda args -> let
mf : Sexp -> Sexp -> Sexp;
===================================== src/elab.ml ===================================== @@ -1069,8 +1069,14 @@ and lexp_decls_1 [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, ctx_define nctx var lexp ltp
- | [Symbol ((l, vname) as v); sexp] + | [Symbol (l, vname); sexp] -> if SMap.mem vname pending_decls then + let decl_loc = SMap.find vname pending_decls in + let v = ({file = l.file; + line = l.line; + column = l.column; + docstr = String.concat "\n" [decl_loc.docstr; l.docstr]}, + vname) in let pending_decls = SMap.remove vname pending_decls in let pending_defs = ((v, sexp) :: pending_defs) in if SMap.is_empty pending_decls then @@ -1621,7 +1627,7 @@ let register_special_forms () = ("case_", sform_case); ("let_in_", sform_letin); ("Type_", sform_type); - ("load_", sform_load); + ("load", sform_load); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute); ("new-attribute", sform_new_attribute);
===================================== src/eval.ml ===================================== @@ -746,6 +746,16 @@ let getenv loc depth args_val = match args_val with | [v] -> Vcommand (fun () -> Velabctx !_last_elab_context) | _ -> error loc "getenv takes a single Unit as argument"
+let debug_doc loc depth args_val = match args_val with + | [Vstring name; Velabctx ectx] + -> (try let idx = senv_lookup name ectx in + let elem = lctx_lookup (ectx_to_lctx ectx) + (((dummy_location, Some name), idx)) in + match elem with + | ((l,_),_,_) -> Vstring (l.docstr) + with _ -> Vstring "element not found") + | _ -> error loc "Elab.debug_doc takes a String and an Elab_Context as arguments" + let is_bound loc depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (try (ignore (senv_lookup name ectx); true) @@ -994,6 +1004,7 @@ let register_builtin_functions () = ("Ref.write" , ref_write, 2); ("gensym" , gensym, 1); ("Elab.getenv" , getenv, 1); + ("Elab.debug-doc", debug_doc, 2); ("Elab.isbound" , is_bound, 2); ("Elab.isconstructor", is_constructor, 2); ("Elab.is-nth-erasable", is_nth_erasable, 3);
===================================== src/lexer.ml ===================================== @@ -48,7 +48,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos | [] -> (internal_error "No next token!") | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0) | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0) - | (Pretoken ({file;line;column}, name) :: pts') + | (Pretoken ({file;line;column;docstr}, name) :: pts') -> let char = name.[bpos] in if digit_p char || (char = '-' (* FIXME: Handle '+' as well! *) @@ -57,10 +57,10 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos let rec lexnum bp cp (np : num_part) = if bp >= String.length name then ((if np == NPint then - Integer ({file;line;column=column+cpos}, + Integer ({file;line;column=column+cpos;docstr=docstr}, int_of_string (string_sub name bpos bp)) else - Float ({file;line;column=column+cpos}, + Float ({file;line;column=column+cpos;docstr=docstr}, float_of_string (string_sub name bpos bp))), pts', 0, 0) else @@ -74,28 +74,28 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos -> lexnum (bp+1) (cp+1) NPexp | _ -> ((if np == NPint then - Integer ({file;line;column=column+cpos}, + Integer ({file;line;column=column+cpos;docstr=docstr}, int_of_string (string_sub name bpos bp)) else - Float ({file;line;column=column+cpos}, + Float ({file;line;column=column+cpos;docstr=docstr}, float_of_string (string_sub name bpos bp))), pts, bp, cp) in lexnum (bpos+1) (cpos+1) NPint else if bpos + 1 >= String.length name then - (hSymbol ({file;line;column=column+cpos}, + (hSymbol ({file;line;column=column+cpos;docstr=docstr}, string_sub name bpos (String.length name)), pts', 0, 0) else if stt.(Char.code name.[bpos]) = CKseparate then - (hSymbol ({file;line;column=column+cpos}, + (hSymbol ({file;line;column=column+cpos;docstr=docstr}, string_sub name bpos (bpos + 1)), pts, bpos+1, cpos+1) else let rec lexsym bpos cpos = let mksym epos escaped - = if epos = bpos then epsilon {file;line;column=column+cpos} else + = if epos = bpos then epsilon {file;line;column=column+cpos;docstr=docstr} 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 + hSymbol ({file;line;column=column+cpos;docstr=docstr}, str) in let rec lexsym' prec lf bp cp escaped = if bp >= String.length name then (lf (mksym (String.length name) escaped), pts', 0, 0) @@ -122,7 +122,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos && CKseparate != (stt.(Char.code name.[bp']))) || not (lf dummy_epsilon = dummy_epsilon) -> let left = mksym bp escaped in - let op = hSymbol ({file;line;column=column+cp}, + let op = hSymbol ({file;line;column=column+cp;docstr=docstr}, "__" ^ String.sub name bp 1 ^ "__") in let bpos = bp' in let cpos = inc_cp cp char in
===================================== src/prelexer.ml ===================================== @@ -50,90 +50,92 @@ let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) if utf8_head_p c then cp+1 else cp
-let rec prelex (file : string) (getline : unit -> string) ln ctx acc +let rec prelex (file : string) (getline : unit -> string) ln ctx acc (doc : string) : pretoken list = try (* let fin = open_in file in *) let line = getline () in let limit = String.length line in let nextline = prelex file getline (ln + 1) in - let rec prelex' ctx (bpos:bytepos) (cpos:charpos) acc = + let rec prelex' ctx (bpos:bytepos) (cpos:charpos) acc doc = let nexttok = prelex' ctx in - if bpos >= limit then nextline ctx acc else + if bpos >= limit then nextline ctx acc doc else match line.[bpos] with - | c when c <= ' ' -> nexttok (bpos+1) (cpos+1) acc - | '%' -> nextline ctx acc (* A comment. *) + | c when c <= ' ' -> nexttok (bpos+1) (cpos+1) acc doc + | '%' -> nextline ctx acc doc (* A comment. *) + (* line's bounds seems ok: String.sub line 1 0 == "" *) + | '@' -> nextline ctx acc (String.concat "\n" [doc; (String.sub line 1 (limit - 1))]) | '"' (* A string. *) -> let rec prestring bp cp chars = if bp >= limit then - (prelexer_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} "Unterminated string"; nextline ctx - (Prestring ({file=file; line=ln; column=cpos}, "") - :: acc)) + (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, "") + :: acc) "") else match line.[bp] with | '"' -> nexttok (bp+1) (cp+1) - (Prestring ({file=file; line=ln; column=cpos}, + (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, string_implode (List.rev chars)) - :: acc) + :: acc) "" | '\' -> (if bpos + 1 >= limit then - (prelexer_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} "Unterminated string"; nextline ctx - (Prestring ({file=file; line=ln; column=cpos}, + (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, "") - :: acc)) + :: acc) "") else match line.[bp + 1] with | 't' -> prestring (bp+2) (cp+2) ('\t' :: chars) | 'n' -> prestring (bp+2) (cp+2) ('\n' :: chars) | 'r' -> prestring (bp+2) (cp+2) ('\r' :: chars) | ('u' | 'U') -> - prelexer_error {file=file; line=ln; column=cp} + prelexer_error {file=file; line=ln; column=cp; docstr=doc} "Unimplemented unicode escape"; prestring (bp+2) (cp+2) chars | char -> prestring (bp+2) (cp+2) (char :: chars)) | char -> prestring (bp+1) (inc_cp cp char) (char :: chars) in prestring (bpos+1) (cpos+1) [] - | '{' -> prelex' ((ln, cpos, bpos, acc) :: ctx) (bpos+1) (cpos+1) [] + | '{' -> prelex' ((ln, cpos, bpos, acc) :: ctx) (bpos+1) (cpos+1) [] doc | '}' -> (match ctx with | ((sln, scpos, sbpos, sacc) :: ctx) -> prelex' ctx (bpos+1) (cpos+1) - (Preblock ({file=file; line=sln; column=scpos}, + (Preblock ({file=file; line=sln; column=scpos; docstr=doc}, List.rev acc, - {file=file; line=ln; column=(cpos + 1)}) - :: sacc) - | _ -> (prelexer_error {file=file; line=ln; column=cpos} + {file=file; line=ln; column=(cpos + 1); docstr=doc}) + :: sacc) "" + | _ -> (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} "Unmatched closing brace"; - prelex' ctx (bpos+1) (cpos+1) acc)) + prelex' ctx (bpos+1) (cpos+1) acc doc)) | char (* A pretoken. *) -> let rec pretok bp cp = if bp >= limit then - nextline ctx (Pretoken ({file=file; line=ln; column=cpos}, + nextline ctx (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, string_sub line bpos bp) - :: acc) + :: acc) "" else match line.[bp] with | (' '|'\t'|'\n'|'\r'|'%'|'"'|'{'|'}' ) -> nexttok bp cp - (Pretoken ({file=file; line=ln; column=cpos}, + (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, string_sub line bpos bp) - :: acc) + :: acc) "" | '\' when bp+1 < limit -> let char = line.[bp + 1] in pretok (bp + 2) (1 + inc_cp cp char) | char -> pretok (bp+1) (inc_cp cp char) in pretok (bpos+1) (inc_cp cpos char) - in prelex' ctx 0 1 acc (* Traditionally, column numbers start at 1 :-( *) + in prelex' ctx 0 1 acc doc (* Traditionally, column numbers start at 1 :-( *) with End_of_file -> match ctx with | [] -> List.rev acc | ((ln, cpos, _, _) :: ctx) -> - (prelexer_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos; docstr=""} "Unmatched opening brace"; List.rev acc)
@@ -141,7 +143,7 @@ let prelex_file file = let fin = open_in file in prelex file (fun _ -> input_line fin) (* Traditionally, line numbers start at 1 :-( *) - 1 [] [] + 1 [] [] ""
let prelex_string str = let pos = ref 0 in @@ -155,7 +157,7 @@ let prelex_string str = let line = string_sub str start npos in (* print_string ("Read line: " ^ line); *) line - in prelex "<string>" getline 1 [] [] + in prelex "<string>" getline 1 [] [] ""
let pretoken_name pretok = match pretok with
===================================== src/util.ml ===================================== @@ -25,8 +25,8 @@ module IMap = Map.Make (struct type t = int let compare = compare end)
type charpos = int type bytepos = int -type location = { file : string; line : int; column : charpos } -let dummy_location = {file=""; line=0; column=0} +type location = { file : string; line : int; column : charpos; docstr : string; } +let dummy_location = {file=""; line=0; column=0; docstr=""}
(*************** DeBruijn indices for variables *********************)
View it on GitLab: https://gitlab.com/monnier/typer/commit/3981eea1c7632db58f0d21ddd7a637341691...
Afficher les réponses par date