Setepenre pushed to branch master at Stefan / Typer

Commits: d919cdd9 by Pierre Delaunay at 2016-12-19T15:42:41-05:00 modified lexp_string so metavar's result is printed instead of (?a...). Helps when debug printing

* src/lexp.ml: modified lexp_string * src/lparse.ml: moved `global_substitution` to `src/lexp.ml` so the context can be used when printing lexp * samples/dependent.typer: fixed some issues * samples/acc.typer: new list functions

- - - - - 3a41b28f by Pierre Delaunay at 2016-12-19T15:43:05-05:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - eaa9b404 by Pierre Delaunay at 2016-12-19T20:42:07-05:00 new printing context, easier to modify

* src/lexp.ml: new printing context

- - - - - bd953f6d by Pierre Delaunay at 2016-12-20T16:37:31-05:00 Moved `quote` `list` `type` to BTL as those will soon belong to the default context

* samples/dependent.typer: updated example (Eq_cast) * src/lexp.ml: fix printing bug that caused function's name to be printed as `__` - added the option to print or not erasable and implicit arguments * src/lparse.ml: tries to read multiple BTL files but it is buggy

- - - - -

11 changed files:

- btl/builtins.typer - + btl/list.typer - + btl/quote.typer - + btl/type.typer - samples/dependent.typer - src/debruijn.ml - src/debug_util.ml - src/lexp.ml - src/lparse.ml - src/sexp.ml - tests/lexp_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -100,10 +100,6 @@ Bool = typecons (Boolean) (true) (false); true = datacons Bool true; false = datacons Bool false;

-Option = typecons (Option (a : Type)) (none) (some a); -some = datacons Option some; -none = datacons Option none; - string_eq = Built-in "string_eq" (String -> String -> Bool); int_eq = Built-in "int_eq" (Int -> Int -> Bool); sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); @@ -118,33 +114,6 @@ List = typecons (List (a : Type)) (nil) (cons a (List a)); nil = datacons List nil; cons = datacons List cons;

-length : (a : Type) ≡> List a -> Int; -length = lambda a ≡> - lambda xs -> - case xs - | nil => 0 - | cons hd tl => (1 + (length tl)); - -% ML's typical `head` function is not total, so can't be defined -% as-is in Typer. There are several workarounds: -% - Provide a default value : (a : Type) ≡> List a -> a -> a; -% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; -% - Return an Option/Error. -head : (a : Type) ≡> List a -> Option a; -head = lambda a ≡> - lambda xs -> - case xs - | nil => none - | cons hd tl => some hd; - -tail : (a : Type) ≡> List a -> List a; -tail = lambda a ≡> - lambda xs -> - case xs - | nil => nil - | cons hd tl => tl; - - % ----------------------------------------------------- % Macro % ----------------------------------------------------- @@ -206,7 +175,6 @@ open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String);

- % ----------------------------------------------------- % Logic % ----------------------------------------------------- @@ -222,3 +190,38 @@ Not prop = prop -> False; % Like Bool, except that it additionally carries the meaning of its value. Decidable = typecons (Decidable (prop : Type)) (true (p ::: prop)) (false (p ::: Not prop)); + + +% ----------------------------------------------------- +% To be removed (used it tests) +% ----------------------------------------------------- + +Option = typecons (Option (a : Type)) (none) (some a); +some = datacons Option some; +none = datacons Option none; + +length : (a : Type) ≡> List a -> Int; +length = lambda a ≡> + lambda xs -> + case xs + | nil => 0 + | cons hd tl => (1 + (length tl)); + +% ML's typical `head` function is not total, so can't be defined +% as-is in Typer. There are several workarounds: +% - Provide a default value : (a : Type) ≡> List a -> a -> a; +% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; +% - Return an Option/Error. +head : (a : Type) ≡> List a -> Option a; +head = lambda a ≡> + lambda xs -> + case xs + | nil => none + | cons hd tl => some hd; + +tail : (a : Type) ≡> List a -> List a; +tail = lambda a ≡> + lambda xs -> + case xs + | nil => nil + | cons hd tl => tl;

===================================== btl/list.typer ===================================== --- /dev/null +++ b/btl/list.typer @@ -0,0 +1,47 @@ +Option = typecons (Option (a : Type)) (none) (some a); +some = datacons Option some; +none = datacons Option none; + +length : (a : Type) ≡> List a -> Int; +length = lambda a ≡> + lambda xs -> + case xs + | nil => 0 + | cons hd tl => (1 + (length tl)); + +% ML's typical `head` function is not total, so can't be defined +% as-is in Typer. There are several workarounds: +% - Provide a default value : (a : Type) ≡> List a -> a -> a; +% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; +% - Return an Option/Error. +head : (a : Type) ≡> List a -> Option a; +head = lambda a ≡> + lambda xs -> + case xs + | nil => none + | cons hd tl => some hd; + +tail : (a : Type) ≡> List a -> List a; +tail = lambda a ≡> + lambda xs -> + case xs + | nil => nil + | cons hd tl => tl; + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil;

===================================== btl/quote.typer ===================================== --- /dev/null +++ b/btl/quote.typer @@ -0,0 +1,49 @@ +% +% f = (qquote (uquote x) * x) (node _*_ [(node_ unquote "x") "x"]) +% +% f = node_ "*" cons (x, cons (symbol_ "x") nil)) +% +% +% => x + +get-head : List Sexp -> Sexp; +get-head x = case x + | cons hd _ => hd + | nil => symbol_ "error"; + +symbol = lambda (y : String) -> (symbol_ y); +string = lambda (y : String) -> (string_ y); +integer = lambda (y : Int) -> (integer_ y); +float = lambda (y : Float) -> (float_ y); +block = lambda (y : List Sexp) -> (block_ y); + +quote' : List Sexp -> List Sexp; + +has-uquote : List Sexp -> Sexp; +has-uquote = lambda y -> + let expr = case y + | cons hd tl => hd + | nil => symbol_ "uquote expects one argument" in + expr; + +% traverse nodes +node : Sexp -> List Sexp -> Sexp; +node = lambda (op : Sexp) -> + lambda (y : List Sexp) -> + case (sexp_eq op (symbol_ "uquote")) + | true => has-uquote y + | false => node_ op (quote' y); + +% tree traversal +quote' = lambda (x : List Sexp) -> + case x + | cons hd tl => ( + let nhd = sexp_dispatch_ (a := Sexp) hd node symbol string integer float block in + let ntl = quote' tl in + cons nhd ntl) + + | nil => nil; + +% quote definition +qq = lambda (x : List Sexp) -> get-head (quote' x); +quote = Macro_ qq;

===================================== btl/type.typer ===================================== --- /dev/null +++ b/btl/type.typer @@ -0,0 +1,96 @@ +% build a declaration +% var-name = value-expr; +make-decl : Sexp -> Sexp -> Sexp; +make-decl var-name value-expr = + node_ (symbol_ "_=_") + (cons var-name + (cons value-expr nil)); + +chain-decl : Sexp -> Sexp -> Sexp; +chain-decl a b = + node_ (symbol_ "_;_") (cons a (cons b nil)); + +% build datacons +% ctor-name = datacons type-name ctor-name; +make-cons : Sexp -> Sexp -> Sexp; +make-cons ctor-name type-name = + make-decl ctor-name + (node_ (symbol_ "datacons") + (cons type-name + (cons ctor-name nil))); + +% buil type annotation +% var-name : type-expr; +make-ann : Sexp -> Sexp -> Sexp; +make-ann var-name type-expr = + node_ (symbol_ "_:_") + (cons var-name + (cons type-expr nil)); + +type-impl = lambda (x : List Sexp) -> + % x follow the mask -> (_|_ Nat zero (succ Nat)) + % Type name --^ ^------^ constructors + + % Return a list contained inside a node sexp + let get-list : Sexp -> List Sexp; + get-list node = sexp_dispatch_ (a := List Sexp) node + (lambda op lst -> lst) % Nodes + (lambda _ -> nil) % Symbol + (lambda _ -> nil) % String + (lambda _ -> nil) % Integer + (lambda _ -> nil) % Float + (lambda _ -> nil) in % List of Sexp + + % Get a name from a sexp + % - (name t) -> name + % - name -> name + let get-name : Sexp -> Sexp; + get-name sxp = + sexp_dispatch_ (a := Sexp) sxp + (lambda op lst -> get-name op) % Nodes + (lambda str -> symbol_ str) % Symbol + (lambda _ -> symbol_ "error") % String + (lambda _ -> symbol_ "error") % Integer + (lambda _ -> symbol_ "error") % Float + (lambda _ -> symbol_ "error") in % List of Sexp + + let get-head : List Sexp -> Sexp; + get-head x = case x + | cons hd _ => hd + | nil => symbol_ "error" in + + % Get expression + let expr = get-head x in + + % Expression is node_ (symbol_ "|") (list) + % we only care about the list bit + let lst = get-list expr in + + % head is (node_ type-name (arg list)) + let name = get-head lst; + ctor = tail lst in + + let type-name = get-name name in + + % Create the inductive type definition + let inductive = node_ (symbol_ "typecons") + (cons name ctor) in + + let decl = make-decl type-name inductive in + + % Add constructors + let ctors = + let for-each : List Sexp -> Sexp -> Sexp; + for-each ctr acc = case ctr + | cons hd tl => ( + let acc2 = chain-decl (make-cons (get-name hd) type-name) acc in + for-each tl acc2) + | nil => acc + in for-each ctor (node_ (symbol_ "_;_") nil) in + + % return decls + (chain-decl decl % inductive type declaration + ctors); % constructor declarations + + +type_ = Macro_ type-impl;

===================================== samples/dependent.typer ===================================== --- a/samples/dependent.typer +++ b/samples/dependent.typer @@ -1,8 +1,8 @@

Reify = typecons (Reify (a : Type)) - (RInt (Eq (t := Type) Int a)) - (RFloat (Eq (t := Type) Float a)) - (RString (Eq (t := Type) String a)); + (RInt (Eq (t := Type) a Int)) + (RFloat (Eq (t := Type) a Float)) + (RString (Eq (t := Type) a String));

RInt = datacons Reify RInt; RFloat = datacons Reify RFloat; @@ -14,19 +14,23 @@ float-to-int x = 1; string-to-int : String -> Int; string-to-int x = 1;

-get-type : Reify -> Type; -get-type x = case x - | RInt => Int - | RFloat => Float - | RString => String; - % Here to-int : (a : Type) ≡> (r : (Reify a)) => (x : a) -> Int; -to-int = lambda a ≡> lambda r => lambda x -> case a - | RInt => x - | RFloat => float-to-int x - | RString => string-to-int x; - -%a = to-int (a := Float2) (2.0); -%b = to-int (a := String2) "2"; -%c = to-int (a := Int2) 2; +to-int = lambda a ≡> + lambda r => + lambda x -> + case r + | RInt p => Eq_cast (p := p) (f := (lambda x -> x)) x + | RFloat p => float-to-int (Eq_cast (p := p) (f := (lambda x -> x)) x) + | RString p => string-to-int (Eq_cast (p := p) (f := (lambda x -> x)) x); + +main = to-int 2.0; +main = to-int "2"; +main = to-int 2; + +a = cons 1 (cons 2 (cons 3 nil)); +main = (case head a + | some v => v + | none => 0); + +

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -131,11 +131,7 @@ let get_size ctx = let ((n, _), _) = ctx in n (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = let ((n, map), _) = ctx in - let raw_idx = n - (SMap.find name map) - 1 in (* - if raw_idx > (n - csize) then - raw_idx - rof (* Shift if the variable is not bound *) - else *) - raw_idx + n - (SMap.find name map) - 1

let lexp_ctx_cons (ctx : lexp_context) offset d v t = assert (offset >= 0 @@ -240,7 +236,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start = let _ = match exp with | None -> print_string "<var>" | Some exp -> ( - let str = _lexp_to_str (!debug_ppctx) exp in + let str = _lexp_str (!debug_ppctx) exp in let str = (match str_split str '\n' with | hd::tl -> print_string hd; tl | _ -> []) in

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -87,29 +87,29 @@ let get_p_option name = *)

let _format_mode = ref false -let _ppctx = ref (true , 0, true, false, true, 2, true) +let _ppctx = ref pretty_ppctx let _format_dest = ref "" let _write_file = ref false let _typecheck = ref false

let _set_print_pretty ctx v = - let (a, b, c, d, e, f, g) = !ctx in ctx := (v, b, c, d, e, f, g) + ctx := SMap.add "pretty" (Bool (v)) !ctx

let _set_print_type ctx v = - let (a, b, c, d, e, f, g) = !ctx in ctx := (a, b, v, d, e, f, g) + ctx := SMap.add "print_type" (Bool (v)) !ctx

let _set_print_index ctx v = - let (a, b, c, d, e, f, g) = !ctx in ctx := (a, b, c, v, e, f, g) + ctx := SMap.add "print_dbi" (Bool (v)) !ctx

let _set_print_indent_size ctx v = - let (a, b, c, d, e, f, g) = !ctx in ctx := (a, b, c, d, e, v, g) + ctx := SMap.add "indent_size" (Int (v)) !ctx

let _set_highlight ctx v = - let (a, b, c, d, e, f, g) = !ctx in ctx := (a, b, c, d, e, f, v) - + ctx := SMap.add "color" (Bool (v))!ctx

let mod_ctx f v = f _ppctx v; f debug_ppctx v + let set_print_type v () = mod_ctx _set_print_type v let set_print_index v () = mod_ctx _set_print_index v let set_print_indent_size v = mod_ctx _set_print_indent_size v @@ -432,6 +432,7 @@ let main () = (if (get_p_option "lctx") then( print_lexp_ctx (ectx_to_lctx nctx); print_string "\n"));

+ (* Type erasure *) let clean_lxp = List.map OL.clean_decls lexps in

(* Eval declaration *)

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -124,11 +124,23 @@ type varbind = module VMap = Map.Make (struct type t = int let compare = compare end) type meta_subst = lexp VMap.t type constraints = (lexp * lexp) list -let empty_meta_subst = VMap.empty + +(* What people do to statisfy Ocaml type inference ...*) +let empty_meta_subst = + let lxp = Var((U.dummy_location, "dummy"), -1) in + let v = VMap.empty in + let c = VMap.add 1 lxp v in VMap.remove 1 c + +let empty_constraint = + let lxp = Var((U.dummy_location, "dummy"), -1) in List.tl [(lxp, lxp)] + let impossible = Imm Sexp.Epsilon

let builtin_size = ref 0

+(* :-( *) +let global_substitution = ref (empty_meta_subst, empty_constraint) + (********************** Hash-consing **********************)

(* let hc_table : (lexp, lexp) Hashtbl.t = Hashtbl.create 1000 @@ -146,7 +158,7 @@ module WHC = Tweak.Make (struct type t = lexp end) let hc_table : WHC.t = WHC.create 1000 let hc : lexp -> lexp = WHC.merge hc_table - +

let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) @@ -464,80 +476,139 @@ and subst_string s = match s with | S.Shift (s, n) -> "(↑"^ string_of_int n ^ " " ^ subst_string s ^ ")" | S.Cons (l, s) -> lexp_string l ^ " · " ^ subst_string s

-(* - * Printing - * --------------------- *) -(* - pretty ? (print with new lines and indents) - indent level - print_type? (print inferred Type) - print_index (print dbi index) - separate decl (print extra newline between declarations) - indent size 2/4 - highlight (use console color to display hints) -*) - -type print_context = (bool * int * bool * bool * bool * bool* int) - -let pretty_ppctx = ref (true , 0, true, false, true, 2, true) -let compact_ppctx = ref (false, 0, true, false, true, 2, false) -let debug_ppctx = ref (false, 0, true, true , false, 2, true) - -let rec lexp_print e = _lexp_print (!debug_ppctx) e -and _lexp_print ctx e = print_string (_lexp_to_str ctx e) - -(* -type print_context2 = int SMap.t - -let default_print_context = - List.fold (fun map (key, v) -> SMap.add key v map) - [ - (* true options *) - ("pretty", 1); - ("print_type", 1); - ("print_dbi", 1); - ("indent_size", 2); - ("color", 1); - ("separate_decl", 1); - - (* State information *) - ("indent_level", 0); - ("previous node", 0) - ] - SMap.empty *) - -(* Print a lexp into its typer equivalent *) -(* Depending on the print_context the output can be correct typer code *) -(* This function will be very useful when debugging generated code *) - -(* If I remember correctly ocaml doc, concat string is actually terrible *) -(* It might be better to use a Buffer. *) -and lexp_pretty_string exp = _lexp_to_str (!debug_ppctx) exp - -and _lexp_to_str ctx exp = - (* create a string instead of printing *) - - let (pretty, indent, ptype, pindex, _, isize, color) = ctx in - let lexp_to_str = _lexp_to_str ctx in - - (* internal context, when parsing let *) - let inter_ctx = (pretty, indent + 1, ptype, pindex, false, isize, color) in - - let lexp_to_stri idt e = - _lexp_to_str (pretty, indent + idt, ptype, pindex, false, isize, color) e in +(* ------------------------------------------------------------------------- *) +(* Printing *) + +(* Printing Context + * ========================================== *) + +type print_context_value = + | Bool of bool + | Int of int + | Expr of lexp option + | Predtl of grammar (* precedence table *) + +type print_context = print_context_value SMap.t + +let pretty_ppctx = + List.fold_left (fun map (key, v) -> SMap.add key v map) + SMap.empty + [("pretty" , Bool (true) ); (* print with new lines and indents *) + ("print_type" , Bool (true) ); (* print inferred Type *) + ("print_dbi" , Bool (false)); (* print dbi index *) + ("indent_size" , Int (2) ); (* indent step *) + ("color" , Bool (true) ); (* use console color to display hints *) + ("separate_decl" , Bool (true) ); (* print newline between declarations *) + ("indent_level" , Int (0) ); (* current indent level *) + ("parent" , Expr (None) ); (* parent expression *) + ("metavar" , Expr (None) ); (* metavar being printed *) + ("col_max" , Int (80) ); (* col_size + col_ofsset <= col_max *) + ("col_size" , Int (0) ); (* current column size *) + ("col_ofsset" , Int (0) ); (* if col does not start at 0 *) + ("print_erasable", Bool (false)); + ("print_implicit", Bool (false)); + ("grammar" , Predtl (default_grammar))] + +(* debug_ppctx is a ref so we can modify it in the REPL *) +let debug_ppctx = ref ( + List.fold_left (fun map (key, v) -> SMap.add key v map) + pretty_ppctx + [("pretty" , Bool (false) ); + ("print_dbi" , Bool (true) ); + ("print_erasable", Bool (true)); + ("print_implicit", Bool (true)); + ("separate_decl" , Bool (false) );]) + +let pp_pretty ctx = match SMap.find "pretty" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let pp_type ctx = match SMap.find "print_type" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let pp_dbi ctx = match SMap.find "print_dbi" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let pp_size ctx = match SMap.find "indent_size" ctx with Int i -> i | _ -> U.typer_unreachable "" +let pp_color ctx = match SMap.find "color" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let pp_decl ctx = match SMap.find "separate_decl" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let pp_indent ctx = match SMap.find "indent_level" ctx with Int i -> i | _ -> U.typer_unreachable "" +let pp_parent ctx = match SMap.find "parent" ctx with Expr e -> e | _ -> U.typer_unreachable "" +let pp_meta ctx = match SMap.find "metavar" ctx with Expr e -> e | _ -> U.typer_unreachable "" +let pp_grammar ctx = match SMap.find "grammar" ctx with Predtl p -> p | _ -> U.typer_unreachable "" +let pp_colsize ctx = match SMap.find "col_size" ctx with Int i -> i | _ -> U.typer_unreachable "" +let pp_colmax ctx = match SMap.find "col_max" ctx with Int i -> i | _ -> U.typer_unreachable "" +let pp_erasable ctx = match SMap.find "print_erasable" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let pp_implicit ctx = match SMap.find "print_implicit" ctx with Bool b -> b | _ -> U.typer_unreachable "" + +let set_col_size p ctx = SMap.add "col_size" (Int p) ctx +let add_col_size p ctx = set_col_size ((pp_colsize ctx) + p) ctx +let reset_col_size ctx = set_col_size 0 ctx +let set_parent p ctx = SMap.add "parent" (Expr (Some p)) ctx +let set_meta p ctx = SMap.add "metavar" (Expr (Some p)) ctx +let add_indent ctx i = SMap.add "indent_level" (Int ((pp_indent ctx) + i)) ctx + +let pp_append_string buffer ctx str = + let n = (String.length str) in + Buffer.add_string buffer str; + add_col_size n ctx + +let pp_newline buffer ctx = + Buffer.add_char buffer '\n'; + reset_col_size ctx + +let is_binary_op str = + let c1 = String.get str 0 in + let cn = String.get str ((String.length str) - 1) in + if (c1 = '_') && (cn = '_') then true else false + +let get_binary_op_name name = + String.sub name 1 ((String.length name) - 2) + +let rec get_precedence expr ctx = + let lkp name = SMap.find name (pp_grammar ctx) in + match expr with + | Lambda _ -> lkp "lambda" + | Case _ -> lkp "case" + | Let _ -> lkp "let" + | Arrow (Aexplicit, _, _, _, _) -> lkp "->" + | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" + | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" + | Call (exp, _) -> get_precedence exp ctx + | Builtin ((_, name), _, _) when is_binary_op name -> + lkp (get_binary_op_name name) + | Var ((_, name), _) when is_binary_op name -> + lkp (get_binary_op_name name) + | _ -> None, None + +(* Printing Functions + * ========================================== *) + +let rec lexp_print e = print_string (lexp_string e) +and lexp_string e = lexp_cstring (!debug_ppctx) e + +(* Context Print *) +and lexp_cprint ctx e = print_string (lexp_cstring ctx e) +and lexp_cstring ctx e = _lexp_str ctx e + +(* Implementation *) +and _lexp_str ctx (exp : lexp) : string = + + let ctx = set_parent exp ctx in + let inter_ctx = add_indent ctx 1 in + let lexp_str = _lexp_str ctx in + let lexp_stri idt e = _lexp_str (add_indent ctx idt) e in + + let pretty = pp_pretty ctx in + let color = pp_color ctx in + let indent = pp_indent ctx in + let isize = pp_size ctx in

(* colors *) - let red = if color then red else "" in - let green = if color then green else "" in - let yellow = if color then yellow else "" in - let magenta = if color then magenta else "" in - let cyan = if color then cyan else "" in - let reset = if color then reset else "" in + let red = if color then red else "" in + let green = if color then green else "" in + let yellow = if color then yellow else "" in + let magenta = if color then magenta else "" in + let cyan = if color then cyan else "" in + let reset = if color then reset else "" in

- let _index idx = if pindex then ("[" ^ (string_of_int idx) ^ "]") else "" in + let make_indent idt = if pretty then + (make_line ' ' ((idt + indent) * isize)) else "" in

- let make_indent idt = if pretty then (make_line ' ' ((idt + indent) * isize)) else "" in - let newline = (if pretty then "\n" else " ") in + let newline = if pretty then "\n" else " " in let nl = newline in

let keyword str = magenta ^ str ^ reset in @@ -545,16 +616,23 @@ and _lexp_to_str ctx exp = let tval str = yellow ^ str ^ reset in let fun_call str = cyan ^ str ^ reset in

- let index idx = let str = _index idx in if idx < 0 then (error str) else + let index idx = + let _index idx = if pp_dbi ctx then ("[" ^ (string_of_int idx) ^ "]") else "" in + let str = _index idx in if idx < 0 then (error str) else (green ^ str ^ reset) in

- let kind_str k = - match k with - | Aexplicit -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in + let kind_str k = match k with + | Aexplicit -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in + + let kindp_str k = match k with + | Aexplicit -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in

- let kindp_str k = - match k with - | Aexplicit -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in + let get_name fname = match fname with + | Builtin ((_, name), _, _) -> name, 0 + | Var((_, name), idx) -> name, idx + | Lambda _ -> "__", 0 + | Cons _ -> "__", 0 + | _ -> "__", -1 in

match exp with | Imm(value) -> (match value with @@ -563,116 +641,104 @@ and _lexp_to_str ctx exp = | Float (_, s) -> tval (string_of_float s) | e -> sexp_string e)

- | Susp (e, s) -> _lexp_to_str ctx (push_susp e s) + | Susp (e, s) -> _lexp_str ctx (push_susp e s)

| Var ((loc, name), idx) -> name ^ (index idx) ;

- | Metavar (idx, subst, (loc, name), _) - -> "?" ^ name ^ (index idx) (*TODO : print subst*) + | Metavar (idx, subst, (loc, name), _) ->( + (* print metavar result if any *) + let print_meta exp = + let meta_ctx, _ = !global_substitution in + let ctx = set_meta exp ctx in + _lexp_str ctx (clean meta_ctx exp) in + + match pp_meta ctx with + | None -> print_meta exp + | Some e when e != exp -> print_meta exp + | _ -> + "?" ^ name ^ (subst_string subst) ^ (index idx))

| Let (_, decls, body) -> (* Print first decls without indent *) let h1, decls, idt_lvl = match _lexp_str_decls inter_ctx decls with | h1::decls -> h1, decls, 2 + | h1::[] -> h1, [], 1 | _ -> "", [], 1 in

- let decls = List.fold_left (fun str elem - -> str ^ (make_indent 1) ^ elem ^ nl) - (h1 ^ nl) decls in + let decls = List.fold_left (fun str elem -> + str ^ nl ^ (make_indent 1) ^ elem ^ " ") h1 decls in

let n = String.length decls - 2 in (* remove last newline *) let decls = (String.sub decls 0 n) in

(keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ - (make_indent idt_lvl) ^ (lexp_to_stri 1 body) + (make_indent idt_lvl) ^ (lexp_stri idt_lvl body)

| Arrow(k, Some (_, name), tp, loc, expr) -> - "(" ^ name ^ " : " ^ (lexp_to_str tp) ^ ") " ^ - (kind_str k) ^ " " ^ (lexp_to_str expr) + "(" ^ name ^ " : " ^ (lexp_str tp) ^ ") " ^ + (kind_str k) ^ " " ^ (lexp_str expr)

| Arrow(k, None, tp, loc, expr) -> - "(" ^ (lexp_to_str tp) ^ " " - ^ (kind_str k) ^ " " ^ (lexp_to_str expr) ^ ")" + "(" ^ (lexp_str tp) ^ " " + ^ (kind_str k) ^ " " ^ (lexp_str expr) ^ ")"

| Lambda(k, (loc, name), ltype, lbody) -> - let arg = "(" ^ name ^ " : " ^ (lexp_to_str ltype) ^ ")" in + let arg = "(" ^ name ^ " : " ^ (lexp_str ltype) ^ ")" in

(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ - (make_indent 1) ^ (lexp_to_stri 1 lbody) + (make_indent 1) ^ (lexp_stri 1 lbody)

| Cons(t, (_, ctor_name)) -> - (keyword "datacons ") ^ (lexp_to_str t) ^ " " ^ ctor_name - - | Call(fname, args) -> ( - (* get function name *) - let str, idx, inner_parens, outer_parens = match fname with - | Builtin ((_, name), _, _) -> name, 0, false, true - | Var((_, name), idx) -> name, idx, false, true - | Lambda _ -> "__", 0, true, false - | Cons _ -> "__", 0, false, false - | _ -> "__", -1, true, true in - - let binop_str op (_, lhs) (_, rhs) = - (lexp_to_str lhs) ^ op ^ (index idx) ^ " " ^ (lexp_to_str rhs) in - - let add_parens bl str = - if bl then "(" ^ str ^ ")" else str in - - match (str, args) with - (* Special Operators *) - (* FIXME: Get rid of these special cases: - * Either use the boring (_+_ e1 e2) notation, or check the - * grammar to decide when we can use the infix notation and - * when to add parenthese. *) - | ("_=_", [lhs; rhs]) -> binop_str " =" lhs rhs - | ("_+_", [lhs; rhs]) -> binop_str " +" lhs rhs - | ("_-_", [lhs; rhs]) -> binop_str " -" lhs rhs - | ("_/_", [lhs; rhs]) -> binop_str " /" lhs rhs - | ("_*_", [lhs; rhs]) -> binop_str " *" lhs rhs - (* not an operator *) - | _ -> - let args = List.fold_left - (fun str (_, lxp) - -> str ^ " " ^ (lexp_to_str lxp)) - "" args in - - let str = fun_call (lexp_to_str fname) in - let str = add_parens inner_parens str in - let str = str ^ args in - add_parens outer_parens str) + (keyword "datacons ") ^ (lexp_str t) ^ " " ^ ctor_name + + | Call(fname, args) -> + let name, idx = get_name fname in + let binop_str op (_, lhs) (_, rhs) = + "(" ^ (lexp_str lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str rhs) ^ ")" in + + let print_arg str (arg_type, lxp) = + match arg_type with + | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str lxp) + | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str lxp) + | Aexplicit -> str ^ " " ^ (lexp_str lxp) + | _ -> str in ( + + match args with + | [lhs; rhs] when is_binary_op name -> + binop_str (" " ^ (get_binary_op_name name)) lhs rhs + + | _ -> let args = List.fold_left print_arg "" args in + "(" ^ (lexp_str fname) ^ args ^ ")")

| Inductive (_, (_, name), [], ctors) -> - (keyword "typecons") ^ " (" ^ name ^") " ^ - (lexp_str_ctor ctx ctors) + (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ + (lexp_str_ctor ctx ctors)

| Inductive (_, (_, name), args, ctors) -> let args_str = List.fold_left (fun str (arg_kind, (_, name), ltype) -> str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_to_str ltype) ^ ")") + ^ (lexp_str ltype) ^ ")") "" args in

- (keyword "typecons") ^ " (" ^ name ^ args_str ^") " - ^ (lexp_str_ctor ctx ctors) + (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ + (lexp_str_ctor ctx ctors)

| Case (_, target, _ret, map, dflt) ->( - let str = (keyword "case ") ^ (lexp_to_str target) - (* FIXME: `tpe' is the *base* type of `target`. E.g. if `target` - * is a `List Int`, then `tpe` will be `List`. - ^ * " : " ^ (lexp_to_str tpe) *) in + let str = (keyword "case ") ^ (lexp_str target) in let arg_str arg = List.fold_left (fun str v -> match v with - | (_,None) -> str ^ " _" + | (_ ,None) -> str ^ " _" | (_, Some (_, n)) -> str ^ " " ^ n) "" arg in

let str = SMap.fold (fun k (_, arg, exp) str -> str ^ nl ^ (make_indent 1) ^ - "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_to_stri 1 exp)) + "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp)) map str in

match dflt with @@ -680,7 +746,7 @@ and _lexp_to_str ctx exp = | Some (v, df) -> str ^ nl ^ (make_indent 1) ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name) - ^ " => " ^ (lexp_to_stri 1 df)) + ^ " => " ^ (lexp_stri 1 df))

| Builtin ((_, name), _, _) -> "##" ^ name

@@ -696,31 +762,34 @@ and _lexp_to_str ctx exp = -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e1 ^ ")"

and lexp_str_ctor ctx ctors = + + let pretty = pp_pretty ctx in + let make_indent idt = if pretty then (make_line ' ' ((idt + (pp_indent ctx)) * (pp_size ctx))) else "" in + let newline = (if pretty then "\n" else " ") in + SMap.fold (fun key value str - -> let str = str ^ " (" ^ key in + -> let str = str ^ newline ^ (make_indent 1) ^ "(" ^ key in let str = List.fold_left (fun str (k, _, arg) - -> str ^ " " ^ (_lexp_to_str ctx arg)) + -> str ^ " " ^ (_lexp_str ctx arg)) str value in str ^ ")") ctors ""

and _lexp_str_decls ctx decls =

- let (pretty, indent, ptype, pindex, sepdecl, isize, _) = ctx in - let lexp_to_str = _lexp_to_str ctx in - - (* let make_indent idt = - if pretty then (make_line ' ' ((idt + indent) * isize)) else "" in *) - - let sepdecl = (if sepdecl then "\n" else "") in + let lexp_str = _lexp_str ctx in + let sepdecl = (if pp_decl ctx then "\n" else "") in + let septp = match pp_parent ctx with + | Some _ -> "" + | None -> "\n" in

- let type_str name lxp = (if ptype then ( - name ^ " : " ^ (lexp_to_str lxp) ^ ";") else "") in + let type_str name lxp = (if pp_type ctx then ( + name ^ " : " ^ (lexp_str lxp) ^ ";") else "") in

let ret = List.fold_left (fun str ((_, name), lxp, ltp) - -> let str = if ptype then (type_str name ltp)::str else str in - (name ^ " = " ^ (lexp_to_str lxp) ^ ";" ^ sepdecl)::str) + -> let str = if pp_type ctx then (type_str name ltp)::str else str in + (name ^ " = " ^ (lexp_str lxp) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -82,9 +82,6 @@ let pexp_fatal = debug_message fatal pexp_name pexp_string let pexp_error = debug_message error pexp_name pexp_string let value_fatal = debug_message fatal value_name value_string

-(* :-( *) -let global_substitution = ref (empty_meta_subst, []) - (** Builtin Macros i.e, special forms. *) type sform_type = | Inferred of ltype @@ -857,7 +854,7 @@ and lexp_eval meta_ctx ectx e = let e = L.clean meta_ctx e in let ee = OL.erase_type e in let rctx = EV.from_ectx meta_ctx ectx in - + if not (EV.closed_p rctx (OL.fv e)) then lexp_error (lexp_location e) e ("Expression `" ^ lexp_string e ^ "` is not closed: " @@ -1251,6 +1248,25 @@ let dynamic_bind r v body = (* Make lxp context with built-in types *) let default_ectx = let _ = register_special_forms () in + + (* Read BTL files *) + 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 default_grammar sxps (Some ";") in + let pxps = pexp_decls_all nods in + let _, lctx = dynamic_bind _parsing_internals true + (fun () -> lexp_p_decls pxps elctx) in lctx in + + (* Register predef *) + let register_pred elctx = + try List.iter (fun name -> + let idx = senv_lookup name elctx in + let v = Var((dloc, name), idx) in + BI.set_predef name v) BI.predef_name; + with e -> + warning dloc "Predef not found"; in + (* Empty context *) let lctx = make_elab_context in let lctx = SMap.fold (fun key (e, t) ctx @@ -1258,35 +1274,17 @@ let default_ectx else ctx_define ctx (dloc, key) e t) (!BI.lmap) lctx in

- (* Read BTL files *) - let pres = prelex_file (!btl_folder ^ "builtins.typer") in - let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in - let pxps = pexp_decls_all nods in - - let d, lctx = dynamic_bind _parsing_internals true - (fun () -> lexp_p_decls pxps lctx) in - - (* dump grouped decls * ) - List.iter (fun decls -> - print_string "["; - List.iter (fun ((_, s), _, _) -> - print_string (s ^ ", ")) decls; print_string "] \n") d; *) - - builtin_size := get_size lctx; - - (* Once default builtin are set we can populate the predef table *) - let lctx = try - List.iter (fun name -> - let idx = senv_lookup name lctx in - let v = Var((dloc, name), idx) in - BI.set_predef name v) BI.predef_name; - (* -- DONE -- *) - lctx - with e -> - warning dloc "Predef not found"; - lctx in - lctx + (* read base file *) + let lctx = read_file (!btl_folder ^ "builtins.typer") lctx in + let _ = register_pred lctx in + + (* Does not work, not sure why + let files = ["list.typer"; "quote.typer"; "type.typer"] in + let lctx = List.fold_left (fun lctx file_name -> + read_file (!btl_folder ^ file_name) lctx) lctx files in *) + + + builtin_size := get_size lctx; lctx

let default_rctx = let meta_ctx, _ = !global_substitution in

===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -259,3 +259,4 @@ and sexp_eq_list ss1 ss2 = match ss1, ss2 with | (s1 :: ss1), (s2 :: ss2) -> sexp_equal s1 s2 && sexp_eq_list ss1 ss2 | _ -> false +

===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -33,35 +33,51 @@ open Lparse (* add_def *)

open Builtin

-(* default environment * ) -let lctx = default_lctx - +(* default environment *) +let ectx = default_ectx +let rctx = default_rctx

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

let dcode = " - sqr = lambda (x : Int) -> x * x; - cube = lambda (x : Int) -> x * (sqr x); +sqr : (x : Int) -> Int; +sqr = lambda (x : Int) -> + (x * x); + +cube : (x : Int) -> Int; +cube = lambda (x : Int) -> + (x * (sqr x));

- mult = lambda (x : Int) -> lambda (y : Int) -> x * y; +mult : (x : Int) -> (y : Int) -> Int; +mult = lambda (x : Int) -> + lambda (y : Int) -> + (x * y);

- twice = (mult 2); +twice : (y : Int) -> Int; +twice = (mult 2);

- let_fun = lambda (x : Int) -> - let a = (twice x); b = (mult 2 x); in - a + b;" in +let_fun : (x : Int) -> Int; +let_fun = lambda (x : Int) -> + let a : Int; + a = (twice x); in + let b : Int; + b = (mult 2 x); in + (a + b);" in

- let ret1, _ = lexp_decl_str dcode lctx in + let ret1, _ = lexp_decl_str dcode ectx in

let to_str decls = - let str = _lexp_str_decls (!compact_ppctx) (List.flatten ret1) in - List.fold_left (fun str lxp -> str ^ lxp) "" str in + let str = _lexp_str_decls pretty_ppctx (List.flatten ret1) in + List.fold_left (fun str lxp -> str ^ "\n" ^ lxp) "" str in

(* Cast to string *) - let str1 = to_str ret1 in + let str1 = (to_str ret1) ^ "\n" in + + print_string str1;

(* read code again *) - let ret2, _ = lexp_decl_str str1 lctx in + let ret2, _ = lexp_decl_str str1 ectx in

(* Cast to string *) let str2 = to_str ret2 in

View it on GitLab: https://gitlab.com/monnier/typer/compare/1fd2d61213509a24f81332d41f6edd01654...