Setepenre pushed to branch master at Stefan / Typer Commits: e612a4c9 by Pierre Delaunay at 2016-10-06T15:38:31-04:00 Unified function name. (There were a lot of inconsistency) * To retrieve the string representation of a tree node use: pretoken_string/sexp_string/pexp_string/lexp_string/elexp_string/value_string * To retrieve the tree node name use: pretoken_name/sexp_name/pexp_name/lexp_name/elexp_name/value_name - - - - - 9 changed files: - src/debug.ml - src/elexp.ml - src/env.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml Changes: ===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -142,11 +142,11 @@ let debug_pexp_decls decls = let _ = match e with | Pexpr ((l, name), pxp) -> - lalign_print_string (pexp_to_string pxp) 15; + lalign_print_string (pexp_string pxp) 15; print_loc l; print_string " = "; pexp_print pxp | Ptype ((l, name), ptp) -> - lalign_print_string (pexp_to_string ptp) 15; + lalign_print_string (pexp_string ptp) 15; print_loc l; print_string " : "; pexp_print ptp | Pmcall((l, op), args) -> @@ -172,7 +172,7 @@ let debug_lexp_decls decls = let ((loc, name), lxp, ltp) = e in print_string " "; - lalign_print_string (lexp_to_string lxp) 15; + lalign_print_string (lexp_string lxp) 15; print_string "["; print_loc loc; print_string "]"; let str = _lexp_str_decls (!debug_ppctx) [e] in ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -78,28 +78,27 @@ let rec elexp_location e = let elexp_name e = match e with - | Imm _ -> "Imm" - | Builtin _ -> "Builtin" - | Var _ -> "Var" - | Let _ -> "Let" - | Lambda _ -> "Lambda" + | Imm _ -> "Imm" + | Var _ -> "Var" + | Let _ -> "Let" | Call _ -> "Call" | Cons _ -> "Cons" | Case _ -> "Case" - | Type -> "Type" + | Type -> "Type" + | Lambda _ -> "Lambda" + | Builtin _ -> "Builtin" | Inductive _ -> "Inductive" -let rec elexp_print lxp = print_string (elexp_str lxp) -and elexp_to_string lxp = elexp_str lxp -and elexp_str lxp = +let rec elexp_print lxp = print_string (elexp_string lxp) +and elexp_string lxp = let maybe_str lxp = match lxp with - | Some lxp -> " | _ => " ^ (elexp_str lxp) + | Some lxp -> " | _ => " ^ (elexp_string lxp) | None -> "" in let str_decls d = List.fold_left (fun str ((_, s), lxp) -> - str ^ " " ^ s ^ " = " ^ (elexp_str lxp)) "" d in + str ^ " " ^ s ^ " = " ^ (elexp_string lxp)) "" d in let str_pat lst = List.fold_left (fun str v -> @@ -109,29 +108,29 @@ and elexp_str lxp = let str_cases c = SMap.fold (fun key (_, lst, lxp) str -> - str ^ " | " ^ key ^ " " ^ (str_pat lst) ^ " => " ^ (elexp_str lxp)) + str ^ " | " ^ key ^ " " ^ (str_pat lst) ^ " => " ^ (elexp_string lxp)) c "" in let str_args lst = List.fold_left (fun str lxp -> - str ^ " " ^ (elexp_str lxp)) "" lst in + str ^ " " ^ (elexp_string lxp)) "" lst in match lxp with - | Imm(s) -> sexp_to_str s + | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), _) -> s | Cons((_, s)) -> s - | Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_str b) + | Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_string b) | Let(_, d, b) -> - "let" ^ (str_decls d) ^ " in " ^ (elexp_str b) + "let" ^ (str_decls d) ^ " in " ^ (elexp_string b) | Call(fct, args) -> - "(" ^ (elexp_str fct) ^ (str_args args) ^ ")" + "(" ^ (elexp_string fct) ^ (str_args args) ^ ")" | Case(_, t, cases, default) -> - "case " ^ (elexp_str t) ^ (str_cases cases) ^ (maybe_str default) + "case " ^ (elexp_string t) ^ (str_cases cases) ^ (maybe_str default) | Inductive(_, (_, s)) -> "inductive_ " ^ s @@ -140,7 +139,5 @@ and elexp_str lxp = (* Print Lexp name followed by the lexp in itself, finally throw an exception *) let elexp_debug_message loc lxp message = - print_string "\n"; - print_string (elexp_name lxp); print_string ": "; elexp_print lxp; print_string "\n"; - elexp_fatal loc message + elexp_fatal loc (message ^ "\n" ^ (elexp_name lxp) ^ ": " ^ (elexp_string lxp) ^ "\n"); ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -99,27 +99,6 @@ let rec value_eq_list a b = value_equal v1 v2 && value_eq_list vv1 vv2 | _ -> false -let rec value_print (vtp: value_type) = - match vtp with - | Closure (_, lxp, _) -> - print_string ("Closure(" ^ (elexp_str lxp) ^ ")") - | Vsexp sxp -> sexp_print sxp - | Vint(i) -> print_int i - | Vfloat(f) -> print_float f - | Vstring(s) -> print_string ("\"" ^ s ^ "\"") - | Vcons ((_, n), []) -> print_string n - | Vcons ((_, n), args) -> - print_string ("(" ^ n); - List.iter (fun arg -> print_string " "; value_print arg) args; - print_string ")"; - - | Vbuiltin(str) -> print_string str - | Vdummy -> print_string "value_print_dummy" - | Vin _ -> print_string "in_channel" - | Vout _ -> print_string "out_channel" - | Vcommand _ -> print_string "command" - (* | _ -> print_string "debug print" *) - let value_location (vtp: value_type) = match vtp with | Vcons ((loc, _), _) -> loc @@ -127,21 +106,39 @@ let value_location (vtp: value_type) = (* location info was lost or never existed *) | _ -> dloc - let value_name v = match v with - | Vint _ -> "Vint" - | Vstring _ -> "Vstring" - | Vcons _ -> "Vcons" - | Vbuiltin _ -> "Sbuiltin" + | Vin _ -> "Vin" + | Vout _ -> "Vout" + | Vint _ -> "Vint" + | Vsexp _ -> "Vsexp" + | Vcons _ -> "Vcons" | Vfloat _ -> "Vfloat" - | Closure _ -> "Closure" - | Vsexp _ -> "Vsexp" - | Vdummy -> "Vdummy" - | Vin _ -> "Vin" - | Vout _ -> "Vout" + | Vdummy -> "Vdummy" + | Vstring _ -> "Vstring" + | Closure _ -> "Closure" + | Vbuiltin _ -> "Vbuiltin" | Vcommand _ -> "Vcommand" +let rec value_string v = + match v with + | Vin _ -> "in_channel" + | Vout _ -> "out_channe;" + | Vdummy -> "dummy" + | Vcommand _ -> "command" + | Vstring s -> "\"" ^ s ^ "\"" + | Vbuiltin s -> s + | Vint i -> string_of_int i + | Vfloat f -> string_of_float f + | Vsexp s -> sexp_string s + | Closure (s, elexp, _) -> "(" ^ s ^ (elexp_string elexp) ^ ")" + | Vcons ((_, s), lst) -> + let args = List.fold_left (fun str v -> + (str ^ " " ^ (value_string v))) "" lst in + "(" ^ s ^ args ^ ")" + +let value_print (vtp: value_type) = print_string (value_string vtp) + let make_runtime_ctx = M.nil let get_rte_size (ctx: runtime_env): int = M.length ctx ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -339,18 +339,18 @@ and nosusp e = (* Return `e` without `Susp`. *) | Susp(e, s) -> push_susp e s | _ -> e -let lexp_to_string e = +let lexp_name e = match e with - | Imm _ -> "Imm" - | Var _ -> "Var" - | Let _ -> "let" - | Arrow _ -> "Arrow" + | Imm _ -> "Imm" + | Var _ -> "Var" + | Let _ -> "let" + | Arrow _ -> "Arrow" | Lambda _ -> "lambda" - | Call _ -> "Call" + | Call _ -> "Call" + | Cons _ -> "inductive-cons" + | Case _ -> "case" | Inductive _ -> "inductive_" - | Cons _ -> "inductive-cons" - | Case _ -> "case" - | Builtin _ -> "Builtin" + | Builtin _ -> "Builtin" | _ -> "lexp_to_string: not implemented" (* @@ -567,7 +567,7 @@ let rec lexp_unparse lxp = | _ as e -> Pimm (Symbol(lexp_location e, "Type")) - +let lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) (* * Printing * --------------------- *) @@ -616,7 +616,7 @@ let default_print_context = (* If I remember correctly ocaml doc, concat string is actually terrible *) (* It might be better to use a Buffer. *) -and lexp_to_str exp = _lexp_to_str (!debug_ppctx) exp +and lexp_pretty_string exp = _lexp_to_str (!debug_ppctx) exp and _lexp_to_str ctx exp = (* create a string instead of printing *) @@ -665,7 +665,7 @@ and _lexp_to_str ctx exp = | String (_, s) -> tval ("\"" ^ s ^ "\"") | Integer(_, s) -> tval (string_of_int s) | Float (_, s) -> tval (string_of_float s) - | e -> sexp_to_str e) + | e -> sexp_string e) | Susp (e, s) -> _lexp_to_str ctx (push_susp e s) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -72,7 +72,7 @@ let btl_folder = ref "./btl/" (* Print Lexp name followed by the lexp in itself, finally throw an exception *) let lexp_debug_message loc lxp message = print_string "\n"; - print_string (lexp_to_str lxp); print_string ": "; lexp_print lxp; print_string "\n"; + print_string (lexp_string lxp); print_string ": "; lexp_print lxp; print_string "\n"; lexp_fatal loc message @@ -86,12 +86,12 @@ let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) with | Sort (_, _) -> () (* All clear! *) | _ -> lexp_error l ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_to_str ltp) + ^ lexp_string ltp) let elab_check_proper_type (ctx : elab_context) ltp v = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp with e -> print_string ("Exception while checking type `" - ^ lexp_to_str ltp ^ "` of var `" ^ + ^ lexp_string ltp ^ "` of var `" ^ (let (_, name) = v in name) ^"`\n"); print_lexp_ctx (ectx_to_lctx ctx); raise e @@ -475,7 +475,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = handle_fun_args ((ak, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) | _ -> lexp_fatal (sexp_location sarg) - ("Explicit arg `" ^ aname ^ "` to non-function (type = " ^ lexp_to_str ltp ^ ")")) + ("Explicit arg `" ^ aname ^ "` to non-function (type = " ^ lexp_string ltp ^ ")")) | sarg :: sargs (* Process Argument *) -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) with @@ -492,8 +492,8 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = lexp_print t; print_string "\n"; print_lexp_ctx (ectx_to_lctx ctx); lexp_fatal (sexp_location sarg) - ("Explicit arg `" ^ sexp_to_str sarg - ^ "` to non-function (type = " ^ lexp_to_str ltp ^ ")")) in + ("Explicit arg `" ^ sexp_string sarg + ^ "` to non-function (type = " ^ lexp_string ltp ^ ")")) in let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK @@ -599,11 +599,11 @@ and lexp_read_pattern pattern exp target ctx: -> (try SMap.find cons_name map with Not_found -> lexp_warning loc - ("`" ^ lexp_to_str (it) + ("`" ^ lexp_string (it) ^ "` does not hold a `" ^ cons_name ^ "` constructor"); []) | it -> lexp_fatal loc - ("`" ^ lexp_to_str (it) + ("`" ^ lexp_string (it) ^ "` is not an inductive type!") in (* FIXME: Don't remove them, add them without names! *) @@ -622,7 +622,7 @@ and lexp_read_pattern pattern exp target ctx: (cons_name, loc, args), nctx | _ -> lexp_warning (pexp_location ctor) ("Invalid constructor `" - ^ (pexp_to_string ctor) ^ "`"); + ^ (pexp_string ctor) ^ "`"); ("_", pexp_location ctor, []), ctx (* Read patterns inside a constructor *) @@ -865,7 +865,7 @@ and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list = and print_lexp_trace () = - print_trace " LEXP TRACE " 50 pexp_to_string pexp_print !_global_lexp_trace + print_trace " LEXP TRACE " 50 pexp_string pexp_print !_global_lexp_trace (* Only print var info *) and lexp_print_var_info ctx = ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -194,8 +194,8 @@ let rec sort_level_max l1 l2 = match nosusp l1, nosusp l2 with | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *) -> U.msg_error "TC" (lexp_location l1) ("Can't compute the max of levels `" - ^ lexp_to_str l1 ^ "` and `" - ^ lexp_to_str l2 ^ "`"); + ^ lexp_string l1 ^ "` and `" + ^ lexp_string l2 ^ "`"); SortLevel SLz let sort_compose l s1 s2 = @@ -284,7 +284,7 @@ let rec check ctx e = mkSusp t2 (S.substitute arg) | _ -> (U.msg_error "TC" (lexp_location arg) ("Calling a non function (type = " - ^ lexp_to_str ft ^ ")!"); + ^ lexp_string ft ^ ")!"); ft)) ft args | Inductive (l, label, args, cases) @@ -305,9 +305,9 @@ let rec check ctx e = -> sort_level_max level level' | tt -> U.msg_error "TC" (lexp_location t) ("Field type " - ^ lexp_to_str t + ^ lexp_string t ^ " is not a Type! (" - ^ lexp_to_str tt ^")"); + ^ lexp_string tt ^")"); DB.print_lexp_ctx ctx; SortLevel SLz), DB.lctx_extend ctx v Variable t) @@ -459,4 +459,4 @@ and clean_map cases = SMap.mapi (fun key (l, args, expr) -> (l, (clean_arg_list args), (erase_type expr))) cases - + ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -404,16 +404,20 @@ let _pexp_decl_str (str: string) tenv grm limit = let pexp_decl_str str = _pexp_decl_str str default_stt default_grammar (Some ";") -let pexp_to_string e = + +let pexp_string e = sexp_string (pexp_unparse e) +let pexp_print e = print_string (pexp_string e) + +let pexp_name e = match e with - | Pimm _ -> "Pimm" - | Pvar (_,_) -> "Pvar" + | Pimm _ -> "Pimm" + | Pvar (_,_) -> "Pvar" | Phastype (_,_,_) -> "Phastype" - | Pmetavar (_, _) -> "Pmetavar" - | Plet (_, _, _) -> "Plet" - | Parrow (_, _, _, _, _) -> "Parrow" - | Plambda (_,(_,_), _, _) -> "Plambda" - | Pcall (_, _) -> "Pcall" + | Pmetavar (_, _) -> "Pmetavar" + | Plet (_, _, _) -> "Plet" + | Parrow (_, _, _, _, _) -> "Parrow" + | Plambda (_,(_,_), _, _) -> "Plambda" + | Pcall (_, _) -> "Pcall" | Pinductive ((_,_), _, _) -> "Pinductive" - | Pcons (_,_) -> "Pcons" + | Pcons (_,_) -> "Pcons" | Pcase (_, _, _) -> "Pcase" ===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -142,10 +142,6 @@ let prelex_file file = (* Traditionally, line numbers start at 1 :-( *) 1 [] [] -(* Since current implementation is not compatible with stream * - * we write a temporary file and use this file as input. * - * This is a terrible solution but for the things we do it does not * - * really matters. Plus it will make testing easier. *) let prelex_string str = let pos = ref 0 in let getline () = @@ -160,19 +156,25 @@ let prelex_string str = line in prelex "<string>" getline 1 [] [] -let rec _pretokens_to_str pretok = +let pretoken_name pretok = + match pretok with + | Pretoken _ -> "Pretoken" + | Prestring _ -> "Prestring" + | Preblock _ -> "Preblock" + +let rec pretoken_string pretok = match pretok with | Preblock(_,pts,_) -> "{" ^ ( - List.fold_left (fun str pts -> str ^ " " ^ (_pretokens_to_str pts)) + List.fold_left (fun str pts -> str ^ " " ^ (pretoken_string pts)) "" pts) ^ " }" | Pretoken(_, str) -> str | Prestring(_, str) -> "\"" ^ str ^ "\"" -let pretokens_to_str pretokens = - List.fold_left (fun str pt -> str ^ (_pretokens_to_str pt)) "" pretokens +let pretokens_string pretokens = + List.fold_left (fun str pt -> str ^ (pretoken_string pt)) "" pretokens -let pretokens_print p = print_string (pretokens_to_str p) +let pretokens_print p = print_string (pretokens_string p) (* Prelexer comparison, ignoring source-line-number info, used for tests. *) ===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -63,20 +63,20 @@ let emptyString = hString "" (*************** The Sexp Printer *********************) -let rec sexp_to_str sexp = +let rec sexp_string sexp = match sexp with | Epsilon -> "ε" (* "ε" *) - | Block(_,pts,_) -> "{" ^ (pretokens_to_str pts) ^ " }" + | Block(_,pts,_) -> "{" ^ (pretokens_string pts) ^ " }" | Symbol(_, name) -> name | String(_, str) -> "\"" ^ str ^ "\"" | Integer(_, n) -> string_of_int n | Float(_, x) -> string_of_float x | Node(f, args) -> - let str = "(" ^ (sexp_to_str f) in + let str = "(" ^ (sexp_string f) in (List.fold_left (fun str sxp -> - str ^ " " ^ (sexp_to_str sxp)) str args) ^ ")" + str ^ " " ^ (sexp_string sxp)) str args) ^ ")" -let sexp_print sexp = print_string (sexp_to_str sexp) +let sexp_print sexp = print_string (sexp_string sexp) let rec sexp_location s = match s with @@ -88,6 +88,16 @@ let rec sexp_location s = | 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" + | String _ -> "String" + | Integer _ -> "Integer" + | Float _ -> "Float" + | Node _ -> "Node" + | Epsilon -> "Epsilon" + (*************** The Sexp Parser *********************) View it on GitLab: https://gitlab.com/monnier/typer/commit/e612a4c982d28a99f3e7bc1d6377d011b9ca...