Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer

Commits: f04cab52 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Delay parsing of declarations until elaboration for define-operator

* elab.ml (lexp_p_decls): Add a parameter for unparsed tokens, so that later declarations can be parsed in a context with newly declared operators

- - - - - 456370bc by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Remove the parsing error for tightly binding postfix operators

- - - - - 8beb9266 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Dump the evaluation context when the variable names don't match

- - - - - 2e00884b by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00 Assign the builtins Int.+, etc to suitable variables Int_+, etc.

_+_ can be Int.+ by default, but we should also keep that value in Int_+ in case _+_ gets reassigned (with a num typeclass, for instance).

- - - - -

6 changed files:

- btl/builtins.typer - src/REPL.ml - src/debug_util.ml - src/elab.ml - src/env.ml - src/sexp.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -103,10 +103,15 @@ true = datacons Bool true; false = datacons Bool false;

%% Basic operators -_+_ = Built-in "Int.+" : Int -> Int -> Int; -_-_ = Built-in "Int.-" : Int -> Int -> Int; -_*_ = Built-in "Int.*" : Int -> Int -> Int; -_/_ = Built-in "Int./" : Int -> Int -> Int; +Int_+ = Built-in "Int.+" : Int -> Int -> Int; +Int_- = Built-in "Int.-" : Int -> Int -> Int; +Int_* = Built-in "Int.*" : Int -> Int -> Int; +Int_/ = Built-in "Int./" : Int -> Int -> Int; + +_+_ = Int_+; +_-_ = Int_-; +_*_ = Int_*; +_/_ = Int_/;

%% modulo Int_mod = Built-in "Int.mod" : Int -> Int -> Int;

===================================== src/REPL.ml ===================================== @@ -135,7 +135,9 @@ let ierase_type (lexps: (ldecl list list * lexpr list)) =

let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in - let ldecls, lctx = Elab.lexp_p_decls pdecls lctx in + (* FIXME We take the parsed input here but we should take the + unparsed tokens directly instead *) + let ldecls, lctx = Elab.lexp_p_decls pdecls [] lctx in let lexprs = Elab.lexp_parse_all pexprs lctx in List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) lexprs; @@ -164,8 +166,7 @@ let ieval f str ectx rctx = let raw_eval f str ectx rctx = let pres = (f str) in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in - let lxps, ectx = Elab.lexp_p_decls nods ectx in + let lxps, ectx = Elab.lexp_p_decls [] sxps ectx in let elxps = List.map OL.clean_decls lxps in (* At this point, `elxps` is a `(vname * elexp) list list`, where: * - each `(vname * elexp)` is a definition

===================================== src/debug_util.ml ===================================== @@ -138,8 +138,6 @@ let arg_defs = [ Arg.Unit (add_p_option "pretok"), " Print pretok debug info"); ("-tok", Arg.Unit (add_p_option "tok"), " Print tok debug info"); - ("-sexp", - Arg.Unit (add_p_option "sexp"), " Print sexp debug info"); ("-pexp", Arg.Unit (add_p_option "pexp"), " Print pexp debug info"); ("-lexp", @@ -152,7 +150,6 @@ let arg_defs = [ Arg.Unit (fun () -> add_p_option "pretok" (); add_p_option "tok" (); - add_p_option "sexp" (); add_p_option "pexp" (); add_p_option "lexp" (); add_p_option "lctx" (); @@ -165,7 +162,6 @@ let parse_args () =

let make_default () = arg_print_options := SMap.empty; - add_p_option "sexp" (); add_p_option "pexp" (); add_p_option "lexp" ()

@@ -176,10 +172,8 @@ let format_source () = let filename = List.hd (!arg_files) in let pretoks = prelex_file filename in let toks = lex default_stt pretoks in - let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx) - toks (Some ";") in let ctx = Elab.default_ectx in - let lexps, _ = Elab.lexp_p_decls nodes ctx in + let lexps, _ = Elab.lexp_p_decls [] toks ctx in

print_string (make_sep '-'); print_string "\n";

@@ -235,26 +229,12 @@ let main () = print_string (make_title " Base Sexp"); debug_sexp_print_all toks; print_string "\n"));

- (* get node sexp *) - print_string yellow; - let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx) - toks (Some ";") in - print_string reset; - - (if (get_p_option "sexp") then( - print_string (make_title " Node Sexp "); - debug_sexp_print_all nodes; print_string "\n")); - - (* Parse All Declaration *) - print_string yellow; - print_string reset; - (* get lexp *) let octx = Elab.default_ectx in

(* debug lexp parsing once merged *) print_string yellow; - let lexps, nctx = try Elab.lexp_p_decls nodes octx + let lexps, nctx = try Elab.lexp_p_decls [] toks octx with e -> print_string reset; raise e in

===================================== src/elab.ml ===================================== @@ -1181,136 +1181,152 @@ and infer_and_generalize_def (ctx : elab_context) se = (e', t')

and lexp_decls_1 - (sdecls : sexp list) + (sdecls : sexp list) (* What's already parsed *) + (tokens : token list) (* Rest of input *) (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) (pending_decls : location SMap.t) (* Pending type decls. *) (pending_defs : (symbol * sexp) list) (* Pending definitions. *) - : (vname * lexp * ltype) list * sexp list * elab_context = - - let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = - match sdecls with - | [] -> (if not (SMap.is_empty pending_decls) then - let (s, loc) = SMap.choose pending_decls in - error ~loc ("Variable `" ^ s ^ "` declared but not defined!") - else - assert (pending_defs == [])); - [], [], nctx - - | Symbol (_, "") :: sdecls - -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - - | Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls - -> lexp_decls_1 (List.append sdecls' sdecls) - ectx nctx pending_decls pending_defs - - | Node (Symbol (loc, "_:_"), args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in - if SMap.mem vname pending_decls then - (* Don't burp: take'em all and unify! *) - let pt_idx = senv_lookup vname nctx in - (* Take the previous type annotation. *) - let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with - | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) - | _ -> Log.internal_error "Var not found at its index!" in - (* Unify it with the new one. *) - let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with - | (_::_) - -> lexp_error loc ltp - ("New type annotation `" - ^ lexp_string ltp ^ "` incompatible with previous `" - ^ lexp_string pt ^ "`") - | [] -> () in - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - else if List.exists (fun ((_, vname'), _) -> vname = vname') - pending_defs then - (error ~loc ("Variable `" ^ vname ^ "` already defined!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - else lexp_decls_1 sdecls ectx - (ectx_extend nctx (loc, Some vname) ForwardRef ltp) - (SMap.add vname loc pending_decls) - pending_defs - | _ -> error ~loc "Invalid type declaration syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | Node (Symbol (l, "_=_") as head, args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol ((l, vname)); sexp] - when SMap.is_empty pending_decls - -> assert (pending_defs == []); - (* Used to be true before we added define-operator. *) - (* assert (ectx == nctx); *) - let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (l, Some vname) in - (* Lexp decls are always recursive, so we have to shift by 1 to - * account for the extra var (ourselves). *) - [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, - ctx_define nctx var lexp ltp - - | [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 - let nctx = ectx_new_scope nctx in - let decls, nctx = lexp_check_decls ectx nctx pending_defs in - decls, sdecls, nctx - else - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - - else - (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | [Node (Symbol s, args) as d; body] - -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - lexp_decls_1 ((Node (head, - [Symbol s; - Node (Symbol (sexp_location d, "lambda_->_"), - [sexp_u_list args; body])])) - :: sdecls) - ectx nctx pending_decls pending_defs - - | _ -> error ~loc:l "Invalid definition syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | Node (Symbol (l, "define-operator"), args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) - pending_decls pending_defs - - | Node (Symbol ((l, _) as v), sargs) :: sdecls - -> (* expand macro and get the generated declarations *) - let sdecl' = lexp_decls_macro v sargs nctx in - lexp_decls_1 (sdecl' :: sdecls) ectx nctx - pending_decls pending_defs - - | sexp :: sdecls - -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + : (vname * lexp * ltype) list * sexp list * token list * elab_context = + + let rec lexp_decls_1 sdecls tokens nctx pending_decls pending_defs = + let sdecl, sdecls, toks = + match (sdecls, tokens) with + | (s :: sdecls, _) -> Some s, sdecls, tokens + | ([], []) -> None, [], [] + | ([], _) -> + let (s, toks) = sexp_parse_all (ectx_get_grammar nctx) + tokens (Some ";") in + Some s, [], toks in + let recur prepend_sdecls nctx pending_decls pending_defs = + lexp_decls_1 (List.append prepend_sdecls sdecls) + toks nctx pending_decls pending_defs in + match sdecl with + | None -> (if not (SMap.is_empty pending_decls) then + let (s, loc) = SMap.choose pending_decls in + error ~loc ("Variable `" ^ s ^ "` declared but not defined!") + else + assert (pending_defs == [])); + [], [], [], nctx + + | Some (Symbol (_, "")) + -> recur [] nctx pending_decls pending_defs + + | Some (Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls')) + -> recur sdecls' nctx pending_decls pending_defs + + | Some (Node (Symbol (loc, "_:_"), args) as thesexp) + (* FIXME: Move this to a "special form"! *) + -> (match args with + | [Symbol (loc, vname); stp] + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in + if SMap.mem vname pending_decls then + (* Don't burp: take'em all and unify! *) + let pt_idx = senv_lookup vname nctx in + (* Take the previous type annotation. *) + let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with + | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) + | _ -> Log.internal_error "Var not found at its index!" in + (* Unify it with the new one. *) + let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with + | (_::_) + -> lexp_error loc ltp + ("New type annotation `" + ^ lexp_string ltp ^ "` incompatible with previous `" + ^ lexp_string pt ^ "`") + | [] -> () in + recur [] nctx pending_decls pending_defs + else if List.exists (fun ((_, vname'), _) -> vname = vname') + pending_defs then + (error ~loc ("Variable `" ^ vname ^ "` already defined!"); + recur [] nctx pending_decls pending_defs) + else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + (SMap.add vname loc pending_decls) + pending_defs + | _ -> error ~loc ("Invalid type declaration syntax : `" ^ + (sexp_string thesexp) ^ "`"); + recur [] nctx pending_decls pending_defs) + + | Some (Node (Symbol (l, "_=_") as head, args) as thesexp) + (* FIXME: Move this to a "special form"! *) + -> (match args with + | [Symbol ((l, vname)); sexp] + when SMap.is_empty pending_decls + -> assert (pending_defs == []); + (* Used to be true before we added define-operator. *) + (* assert (ectx == nctx); *) + let (lexp, ltp) = infer_and_generalize_def nctx sexp in + let var = (l, Some vname) in + (* Lexp decls are always recursive, so we have to shift by 1 to + * account for the extra var (ourselves). *) + [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, + ctx_define nctx var lexp ltp + + | [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 + let nctx = ectx_new_scope nctx in + let decls, nctx = lexp_check_decls ectx nctx pending_defs in + decls, sdecls, toks, nctx + else + recur [] nctx pending_decls pending_defs + + else + (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); + recur [] nctx pending_decls pending_defs) + + | [Node (Symbol s, args) as d; body] + -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) + recur [Node (head, + [Symbol s; + Node (Symbol (sexp_location d, "lambda_->_"), + [sexp_u_list args; body])])] + nctx pending_decls pending_defs + + | _ -> error ~loc:l ("Invalid definition syntax : `" ^ + (sexp_string thesexp) ^ "`"); + recur [] nctx pending_decls pending_defs) + + | Some (Node (Symbol (l, "define-operator"), args)) + (* FIXME: Move this to a "special form"! *) + -> recur [] (sdform_define_operator nctx l args None) + pending_decls pending_defs + + | Some (Node (Symbol ((l, _) as v), sargs)) + -> (* expand macro and get the generated declarations *) + let sdecl' = lexp_decls_macro v sargs nctx in + recur [sdecl'] nctx pending_decls pending_defs + + | Some sexp + -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; + recur [] nctx pending_decls pending_defs

in (EV.set_getenv nctx; - let res = lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in + let res = lexp_decls_1 sdecls tokens nctx + pending_decls pending_defs in (Log.stop_on_error (); res))

-and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) +and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = - let impl sdecls ctx = match sdecls with - | [] -> [], ectx_new_scope ctx - | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in - let declss, nnctx = lexp_p_decls sdecls nctx in - decls :: declss, nnctx in - let res = impl sdecls ctx in (Log.stop_on_error (); res) + let rec impl sdecls tokens ctx = + match (sdecls, tokens) with + | ([], []) -> [], ectx_new_scope ctx + | _ -> + let decls, sdecls, tokens, nctx = + lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in + Log.stop_on_error (); + let declss, nnctx = impl sdecls tokens nctx in + decls :: declss, nnctx in + impl sdecls tokens ctx

and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in @@ -1695,7 +1711,7 @@ let rec sform_case ctx loc sargs ot = match sargs with

let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] - -> let declss, nctx = lexp_p_decls [sdecls] ctx in + -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in (* FIXME: Use `elaborate`. *) let bdy, ltp = infer sbody (ectx_new_scope nctx) in let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in @@ -1772,9 +1788,7 @@ let sform_load usr_elctx loc sargs ot = let read_file file_name elctx = let pres = prelex_file file_name in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) - sxps (Some ";") in - let _, elctx = lexp_p_decls nods elctx + let _, elctx = lexp_p_decls [] sxps elctx in elctx in

(* read file as elab_context *) @@ -1860,9 +1874,7 @@ let default_ectx let read_file file_name elctx = let pres = prelex_file file_name in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) - sxps (Some ";") in - let _, lctx = lexp_p_decls nods elctx + let _, lctx = lexp_p_decls [] sxps elctx in lctx in

(* Register predef *) @@ -1922,10 +1934,8 @@ let lexp_expr_str str ctx =

let lexp_decl_str str ctx = try let tenv = default_stt in - let grm = ectx_get_grammar ctx in - let limit = Some ";" in - let sdecls = sexp_parse_str str tenv grm limit in - lexp_p_decls sdecls ctx + let tokens = lex_str str tenv in + lexp_p_decls [] tokens ctx with Log.Stop_Compilation s -> ([],ctx)

===================================== src/env.ml ===================================== @@ -167,6 +167,41 @@ let make_runtime_ctx = M.nil

let get_rte_size (ctx: runtime_env): int = M.length ctx

+let print_myers_list l print_fun start = + let n = (M.length l) - 1 in + print_string (make_title " ENVIRONMENT "); + make_rheader [(None, "INDEX"); + (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; + print_string (make_sep '-'); + + for i = start to n do + print_string " | "; + ralign_print_int (n - i) 5; + print_string " | "; + print_fun (M.nth (n - i) l); + done; + print_string (make_sep '=') + +let print_rte_ctx_n (ctx: runtime_env) start = + print_myers_list + ctx + (fun (n, vref) -> + let g = !vref in + let _ = + match n with + | (_, Some m) -> lalign_print_string m 12; print_string " | " + | _ -> print_string (make_line ' ' 12); print_string " | " in + + value_print g; print_string "\n") start + +(* Only print user defined variables *) +let print_rte_ctx ctx = + print_rte_ctx_n ctx (!L.builtin_size) + +(* Dump the whole context *) +let dump_rte_ctx ctx = + print_rte_ctx_n ctx 0 + let get_rte_variable (name: vname) (idx: int) (ctx: runtime_env): value_type = try ( @@ -177,7 +212,7 @@ let get_rte_variable (name: vname) (idx: int) if n1 = n2 then x else ( - fatal + fatal ~print_action:(fun () -> dump_rte_ctx ctx) ("Variable lookup failure. Expected: "" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """)))

@@ -212,37 +247,3 @@ let nfirst_rte_var n ctx = List.rev acc in loop 0 []

-let print_myers_list l print_fun start = - let n = (M.length l) - 1 in - print_string (make_title " ENVIRONMENT "); - make_rheader [(None, "INDEX"); - (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; - print_string (make_sep '-'); - - for i = start to n do - print_string " | "; - ralign_print_int (n - i) 5; - print_string " | "; - print_fun (M.nth (n - i) l); - done; - print_string (make_sep '=') - -let print_rte_ctx_n (ctx: runtime_env) start = - print_myers_list - ctx - (fun (n, vref) -> - let g = !vref in - let _ = - match n with - | (_, Some m) -> lalign_print_string m 12; print_string " | " - | _ -> print_string (make_line ' ' 12); print_string " | " in - - value_print g; print_string "\n") start - -(* Only print user defined variables *) -let print_rte_ctx ctx = - print_rte_ctx_n ctx (!L.builtin_size) - -(* Dump the whole context *) -let dump_rte_ctx ctx = - print_rte_ctx_n ctx 0

===================================== src/sexp.ml ===================================== @@ -160,13 +160,18 @@ let rec sexp_parse (g : grammar) (rest : sexp list) mk_node ((l,"")::op) largs rargs true), rest) | (Some ll, None) when ll > level - (* A closer without matching opener. - * 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. *) - -> sexp_error l ("Lonely postfix/closer ""^name^"""); - sexp_parse rest' level op largs - [mk_node [(l,name);(l,"")] [] rargs true] + (* A closer without matching opener or a postfix symbol + that binds very tightly. Previously, we signaled an + error (assuming the former), but it prevented the use + tightly binding postfix operators. + + For example, it signaled spurious errors when parsing + expressions with a tightly binding postfix # operator + that implemented record construction by taking an + inductive as argument and returning the inductive's only + constructor. *) + -> sexp_parse rest' level op largs + [mk_node [(l,name);(l,"")] [] rargs true] | (Some ll, Some rl) when ll > level (* A new infix which binds more tightly, i.e. does not close * the current `op' but takes its `rargs' instead. *)

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/2bd6aa15e783ef5ce69df7339a9dcfe2f...