December 2016 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][master] 3 commits: * src/lexp.ml: modified lexp_string so metavar's result is printed instead of
by Setepenre 26 Dec '16

26 Dec '16

Setepenre pushed to branch master at Stefan / Typer Commits: 05b1ad07 by Pierre Delaunay at 2016-12-18T23:18:58-05:00 * src/lexp.ml: modified lexp_string so metavar's result is printed instead of metavar. Helps when debug printing * 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, the example is almost working (inference issue I think) * samples/acc.typer: new list functions - - - - - 8cc696db by Pierre Delaunay at 2016-12-20T16:43:45-05:00 Merge - - - - - c7ec8cf2 by Pierre Delaunay at 2016-12-26T11:54:38-05:00 added a new example `samples/io.typer` - - - - - 3 changed files: - + samples/acc.typer - + samples/io.typer - src/lexp.ml Changes: ===================================== samples/acc.typer ===================================== --- /dev/null +++ b/samples/acc.typer @@ -0,0 +1,23 @@ +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; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); \ No newline at end of file ===================================== samples/io.typer ===================================== --- /dev/null +++ b/samples/io.typer @@ -0,0 +1,70 @@ +type Location + | location (line : col) (col : Int) (file : String); + +% Symbolic Expression +Sexp : Type; +type Sexp + | epsilon + | block (loc_start : Location) (tok : List Pretoken) (loc_end : Location) + | symbol (loc : Location) (name : String) + | string (loc : Location) (value : String) + | integer (loc : Location) (value : Int) + | float (loc : Location) (value : Float) + | node (op : Sexp) (args : List Sexp); + +sexp_loc : Sexp -> Location; +sexp_loc s = + case s + | block loc _ _ => loc + | symbol loc _ => loc + | string loc _ => loc + | integer loc _ => loc + | float loc _ => loc + | node loc _ => sexp_loc op + | _ => dummy_location; + +sexp_name : Sexp -> String; +sexp_name s = + case s + | epsilon => "Epsilon" + | block _ _ _ => "Block" + | symbol _ _ => "Symbol" + | string _ _ => "String" + | integer _ _ => "Integer" + | float _ _ => "Float" + | node _ _ => "Node"; + +sexp_string : Sexp -> String; +sexp_string s = + case s + | epsilon => "ε" + | symbol _ v => v + | string _ v => v + | integer _ v => to-string v + | float _ v => to-string v + | block _ v _ => "{" ++ (pretokens_string v) ++ "}" + | node op args => + let args = accumulate + (lambda str val -> str ++ " " ++ sexp_string val) "" args in + "(" ++ (sexp_string op) ++ args ++ ")"; + +% is there a simplier way ? +sexp_equal : Sexp -> Sexp -> Bool; +sexp_equal a b = + case a + | epsilon => case b | + epsilon => true | _ => false + | symbol _ v => case b | + symbol _ v' => v = v' | _ => false + | string _ v => case b | + string _ v' => v = v' | _ => false + | integer _ v => case b | + integer _ v' => v = v' | _ => false + | float _ v => case b | + float _ v' => v = v' | _ => false + | block _ lst _ => case b | + block _ lst' _ => (lst = lst) | _ => false + | node op args => case b | + node op' args' => (op = op') && (args = args') | _ => false; + + ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -545,7 +545,6 @@ 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 View it on GitLab: https://gitlab.com/monnier/typer/compare/bd953f6da7ec2d2df739603e363a86d60a…

1 0

[Git][monnier/typer][master] 4 commits: modified lexp_string so metavar's result is printed instead of (?a...).
by Setepenre 20 Dec '16

20 Dec '16

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/1fd2d61213509a24f81332d41f6edd0165…

1 0

[Git][monnier/typer][master] * src/opslexp.ml (check'): Check Metavar's type annotation.
by Stefan 19 Dec '16

19 Dec '16

Stefan pushed to branch master at Stefan / Typer Commits: 1fd2d612 by Stefan Monnier at 2016-12-19T13:34:24-05:00 * src/opslexp.ml (check'): Check Metavar's type annotation. * src/opslexp.ml (conv_p'): Add partial support for SortLevel's SLlub. * src/lparse.ml (newMetalevel, newMetatype): Fix thinko's. (lexp_decls_macro): Use pexp_p_decls. * src/unification.ml (_unify_metavar): Also unify the var's type. Furthermore, when unifying two metavars, try it both ways. - - - - - 3 changed files: - src/lparse.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -238,9 +238,9 @@ let newMetavar l name t = mkMetavar (meta, S.Identity, (l, name), t) let newMetalevel () = - newMetavar Util.dummy_location "l" (mkSort (dummy_location, StypeLevel)) + newMetavar Util.dummy_location "l" type_level -let newMetatype loc = newMetavar loc "t" (newMetalevel ()) +let newMetatype loc = newMetavar loc "t" (mkSort (loc, Stype (newMetalevel ()))) (* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) @@ -901,7 +901,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp") in (* read as pexp_declaraton *) - (try pexp_decls_all [decls], ctx + (try pexp_p_decls decls, ctx (* if an error occur print generated code to ease debugging *) with e -> error loc "An error occurred while expanding a macro"; ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -224,7 +224,17 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 - | (SortLevel sl1, SortLevel sl2) -> sl1 = sl2 + | (SortLevel sl1, SortLevel sl2) + -> (match (sl1, sl2) with + | (SLz, SLz) -> true + | (SLsucc sl1, SLsucc sl2) -> conv_p sl1 sl2 + | (SLlub (sl11, sl12), sl2) + (* FIXME: This should be "<=" rather than equality! *) + -> conv_p sl11 e2' && conv_p sl12 e2' + | (sl1, SLlub (sl21, sl22)) + (* FIXME: This should be "<=" rather than equality! *) + -> conv_p e1' sl21 && conv_p e1' sl22 + | _ -> false) | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 || (match (s1, s2) with @@ -342,8 +352,9 @@ let rec check' meta_ctx erased ctx e = if conv_p meta_ctx ctx t t' then () else (U.msg_error "TC" (lexp_location e) ("Type mismatch for " - ^ lexp_string e ^ " : " - ^ lexp_string t ^ " != " ^ lexp_string t'); + ^ lexp_string (L.clean meta_ctx e) ^ " : " + ^ lexp_string (L.clean meta_ctx t) ^ " != " + ^ lexp_string (L.clean meta_ctx t')); (* U.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in @@ -589,8 +600,11 @@ let rec check' meta_ctx erased ctx e = ^ lexp_string t); DB.type_int)) | Metavar (idx, s, _, t) - -> try check erased ctx (push_susp (L.VMap.find idx meta_ctx) s) - with Not_found -> t + -> (try let e = push_susp (L.VMap.find idx meta_ctx) s in + let t' = check erased ctx e in + assert_type ctx e t' t + with Not_found -> ()); + t let check meta_ctx = check' meta_ctx DB.set_empty ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -98,12 +98,12 @@ and unify' (e1: lexp) (e2: lexp) | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _) | (Inductive _, Inductive _)) -> if OL.conv_p subst ctx e1' e2' then Some (subst, []) else None - | (l, (Metavar _ as r)) -> _unify_metavar r l subst + | (l, (Metavar (idx, s, _, t) as r)) -> _unify_metavar subst ctx idx s t r l + | ((Metavar (idx, s, _, t) as l), r) -> _unify_metavar subst ctx idx s t l r | (l, (Call _ as r)) -> _unify_call r l ctx vs' subst (* | (l, (Case _ as r)) -> _unify_case r l subst *) | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' subst | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' subst - | (Metavar _ as l, r) -> _unify_metavar l r subst | (Call _ as l, r) -> _unify_call l r ctx vs' subst (* | (Case _ as l, r) -> _unify_case l r subst *) (* | (Inductive _ as l, r) -> _unify_induct l r subst *) @@ -169,22 +169,36 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return - metavar , metavar -> if Metavar = Metavar then OK else ERROR - metavar , lexp -> OK *) -and _unify_metavar (meta: lexp) (lxp: lexp) (subst: meta_subst) : return_type = - let find_or_unify metavar value lxp s = - match find_or_none metavar s with - | Some (lxp_) -> assert false - | None -> (match metavar with - | Metavar (_, subst_, _, _) -> (match Inverse_subst.inverse subst_ with - | Some s' -> Some (associate value (mkSusp lxp s') s, []) +and _unify_metavar (subst: meta_subst) ctx idx s t (lxp1: lexp) (lxp2: lexp) + : return_type = + let unif idx s t lxp = match Inverse_subst.inverse s with + | None -> None + | Some s' + -> let subst = associate idx (mkSusp lxp s') subst in + match unify t (OL.get_type subst ctx lxp) ctx subst with + | Some (subst, []) as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> print_string ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean subst t) ^ " != " + ^ lexp_string (Lexp.clean subst (OL.get_type subst ctx lxp)) ^ "\n" + ^ "for " ^ lexp_string lxp ^ "\n"); + Some (subst, []) in + match lxp2 with + | Metavar (idx2, s2, _, t2) + -> if idx = idx2 then + (* FIXME: handle the case where s1 != s2 !! *) + Some ((subst, [])) + else + (* If one of the two subst can't be inverted, try the other. + * FIXME: There's probably a more general solution. *) + (match unif idx s t lxp2 with + | Some s -> Some s + | None -> + match unif idx2 s2 t2 lxp1 with + | Some s -> Some s | None -> None) - | _ -> None) - in - match (meta, lxp) with - | (Metavar (val1, s1, _, _), Metavar (val2, s2, _, _)) when val1 = val2 - (* FIXME: handle the case where s1 != s2 !! *) - -> Some ((subst, [])) - | (Metavar (v, s1, _, _), _) -> find_or_unify meta v lxp subst - | (_, _) -> None + | _ -> unif idx s t lxp2 (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY @@ -267,6 +281,7 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : retu | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> Some (subst, []) | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs subst + (* FIXME: Handle SLsub! *) | _, _ -> None) | _, _ -> None View it on GitLab: https://gitlab.com/monnier/typer/commit/1fd2d61213509a24f81332d41f6edd01654…

1 0

[Git][monnier/typer][master] * src/lparse.ml (lexp_expand_macro): Use `eval-call`.
by Stefan 19 Dec '16

19 Dec '16

Stefan pushed to branch master at Stefan / Typer Commits: 66730d6d by Stefan Monnier at 2016-12-19T11:30:12-05:00 * src/lparse.ml (lexp_expand_macro): Use `eval-call`. The main purpose of this is to avoid converting the `sexp list` of args to a `lexp list` on its way to a `value_type list` since conversion from lexp to value_type doesn't always create a Vsexp. * src/builtin.ml (o2l_list): Remove. * src/lparse.ml (lexp_eval): New function, extracted from lexp_expand_macro. (lexp_expand_macro): Use it. Add `loc` argument. Use `eval_call`. - - - - - 2 changed files: - src/builtin.ml - src/lparse.ml Changes: ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -113,17 +113,7 @@ let type_eq = let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx -(* lexp Imm list *) -let o2l_list ctx lst = - let tcons = get_predef "cons" ctx in - let tnil = get_predef "nil" ctx in - - let rlst = List.rev lst in - List.fold_left (fun tail elem -> - mkCall(tcons, [(Aexplicit, (Imm (elem))); - (Aexplicit, tail)])) tnil rlst - -(* typer list as seen during runtime *) +(* Typer list as seen during runtime. *) let o2v_list lst = (* FIXME: We're not using predef here. This will break if we change * the definition of `List` in builtins.typer. *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -380,7 +380,7 @@ and get_implicit_arg ctx loc name t = * call a `default-arg-filler` function, implemented in Typer, * just like `expand_macro_` function. That one can then look * things up in a table and/or do anything else it wants. *) - let v = lexp_expand_macro attr [] ctx (Some t) in + let v = lexp_expand_macro loc attr [] ctx (Some t) in (* get the sexp returned by the macro *) let lsarg = match v with @@ -706,7 +706,8 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt) and handle_macro_call ctx func args t = - let sxp = match lexp_expand_macro func args ctx (Some t) with + let sxp = match lexp_expand_macro (lexp_location func) + func args ctx (Some t) with | Vsexp (sxp) -> sxp | v -> value_fatal (lexp_location func) v "Macros should return a Sexp" in @@ -851,32 +852,37 @@ and track_fv meta_ctx rctx lctx e = | _ -> name in String.concat " " (List.map tfv nc) -and lexp_expand_macro macro_funct sargs ctx ot: value_type = +and lexp_eval meta_ctx ectx e = + (* FIXME: Make erase_type take meta_ctx directly! *) + 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: " + ^ track_fv meta_ctx rctx (ectx_to_lctx ectx) e); + + try EV.eval ee rctx + with exc -> EV.print_eval_trace None; raise exc + +and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) + : value_type = (* Build the function to be called *) + let meta_ctx, _ = !global_substitution in let macro_expand = BI.get_predef "expand_macro_" ctx in + (* FIXME: Rather than remember the lexp of "expand_macro" in predef, + * we should remember its value so we don't have to re-eval it everytime. *) + let macro_expand = lexp_eval meta_ctx ctx macro_expand in (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) - let args = [(Aexplicit, macro_funct); - (Aexplicit, (BI.o2l_list ctx sargs))] in + let macro = lexp_eval meta_ctx ctx macro_funct in + let args = [macro; BI.o2v_list sargs] in (* FIXME: Don't `mkCall + eval` but use eval_call instead! *) - let macro = mkCall (macro_expand, args) in - let meta_ctx, _ = !global_substitution in - let macro = L.clean meta_ctx macro in - let emacro = OL.erase_type macro in - let rctx = EV.from_ectx meta_ctx ctx in - - if not (EV.closed_p rctx (OL.fv macro)) then - (lexp_error (lexp_location macro_funct) macro_funct - ("Macro function is not closed: " - ^ track_fv meta_ctx rctx (ectx_to_lctx ctx) macro)); - - (* eval macro *) - let vxp = try EV._eval emacro rctx ([], []) - with e -> EV.print_eval_trace None; raise e in - (* Return results *) - (* Vint/Vstring/Vfloat might need to be converted to sexp *) - vxp + (* FIXME: Make a proper `Var`. *) + EV.eval_call loc (EL.Var ((DB.dloc, "expand_macro"), 0)) ([], []) + macro_expand args (* Print each generated decls *) and sexp_decls_macro_print sxp_decls = @@ -889,7 +895,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = try let lxp, ltp = infer (Pvar (loc, mname)) ctx in (* FIXME: Check that (conv_p ltp Macro)! *) - let ret = lexp_expand_macro lxp sargs ctx None in + let ret = lexp_expand_macro loc lxp sargs ctx None in let decls = match ret with | Vsexp(sexp) -> sexp | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp") in View it on GitLab: https://gitlab.com/monnier/typer/commit/66730d6dbf198522f461f5f80201937b632…

1 0

[Git][monnier/typer][master] * src/lparse.ml: when an error occur during macro expansion
by Setepenre 17 Dec '16

17 Dec '16

Setepenre pushed to branch master at Stefan / Typer Commits: e9d8852d by Pierre Delaunay at 2016-12-17T13:08:12-05:00 * src/lparse.ml: when an error occur during macro expansion (after getting the sexp but before pexp_parse) the generated sexp is printed - - - - - 2 changed files: - samples/inductive.typer - src/lparse.ml Changes: ===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -103,11 +103,11 @@ type_ = Macro_ type-impl; type A | a Int; -%type Pair t1 t2 -% | pair t1 t2; +type Pair (t1 : Type) (t2 : Type) + | pair t1 t2; -%type Point t -% | point (x : t) (y : t); +type Point (t : Type) + | point (x : t) (y : t); %get-first : (a : Type) => (b : Type) => Pair a b -> a; %get-second : (a : Type) => (b : Type) => Pair a b -> b; ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -711,7 +711,12 @@ and handle_macro_call ctx func args t = | v -> value_fatal (lexp_location func) v "Macros should return a Sexp" in - let pxp = pexp_parse sxp in + let pxp = try pexp_parse sxp + with e -> + error dloc "An error occurred while expanding a macro"; + sexp_print sxp; + raise e in + check pxp t ctx (* Identify Call Type and return processed call. *) @@ -873,6 +878,13 @@ and lexp_expand_macro macro_funct sargs ctx ot: value_type = (* Vint/Vstring/Vfloat might need to be converted to sexp *) vxp +(* Print each generated decls *) +and sexp_decls_macro_print sxp_decls = + match sxp_decls with + | Node(Symbol (_, "_;_"), decls) -> + List.iter (fun sxp -> sexp_decls_macro_print sxp) decls + | e -> sexp_print e; print_string "\n" + and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = try let lxp, ltp = infer (Pvar (loc, mname)) ctx in @@ -883,7 +895,13 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp") in (* read as pexp_declaraton *) - pexp_decls_all [decls], ctx + (try pexp_decls_all [decls], ctx + (* if an error occur print generated code to ease debugging *) + with e -> + error loc "An error occurred while expanding a macro"; + sexp_decls_macro_print decls; + raise e) + with e -> fatal loc ("Macro `" ^ mname ^ "`not found") View it on GitLab: https://gitlab.com/monnier/typer/commit/e9d8852d83fa0d85e538636c6fe45342957…

1 0

[Git][monnier/typer][master] 5 commits: * src/eval.ml: fixed sexp_dispatch implementation (was evaluating with the wrong context)
by Setepenre 17 Dec '16

17 Dec '16

Setepenre pushed to branch master at Stefan / Typer Commits: d377f901 by Pierre Delaunay at 2016-12-08T10:01:37-05:00 * src/eval.ml: fixed sexp_dispatch implementation (was evaluating with the wrong context) * Merging - - - - - 461aff50 by Pierre Delaunay at 2016-12-08T10:03:19-05:00 Merge - - - - - 409f7728 by Pierre Delaunay at 2016-12-15T00:12:39-05:00 Merge branch 'master' of gitlab.com:monnier/typer - - - - - a2986fcc by Pierre Delaunay at 2016-12-17T12:34:53-05:00 * btl/builtins.typer: removed `DMacro_` as DMacro now retruns a single Sexp. * src/lparse.ml: removed `expand_dmacro` * tests/macro_test.ml: updated test * samples/inductive.typer: updated example * src/debruijn.ml: removed variable shadowing warning - - - - - ce0dfdc4 by Pierre Delaunay at 2016-12-17T12:42:50-05:00 Merging - - - - - 9 changed files: - btl/builtins.typer - samples/inductive.typer - samples/quote.typer - src/builtin.ml - src/debruijn.ml - src/eval.ml - src/lparse.ml - src/pexp.ml - tests/macro_test.ml Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -157,25 +157,14 @@ integer_ = Built-in "integer_" (Int -> Sexp); float_ = Built-in "float_" (Float -> Sexp); Macro = typecons (Macro) - (Macro_ (List Sexp -> Sexp)) - (DMacro_ (List Sexp -> List Sexp)); + (Macro_ (List Sexp -> Sexp)); Macro_ = datacons Macro Macro_ ; -DMacro_ = datacons Macro DMacro_ ; + expand_macro_ : Macro -> List Sexp -> Sexp; expand_macro_ m args = case m - | Macro_ f => (f args) - % return first sexp if a DMacro_ is used - | DMacro_ f => (case (f args) - | cons hd tl => hd - | nil => (symbol_ "error")); - -expand_dmacro_ : Macro -> List Sexp -> List Sexp; -expand_dmacro_ m args = case m - | DMacro_ f => (f args) - % Wrap a Macro in a list of Sexp if Macro_ is used - | Macro_ f => cons (f args) nil; + | Macro_ f => (f args); sexp_dispatch_ = Built-in "sexp_dispatch_" ( (a : Type) ≡> ===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -6,6 +6,10 @@ make-decl var-name value-expr = (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; @@ -23,7 +27,6 @@ make-ann var-name type-expr = (cons var-name (cons type-expr nil)); - type-impl = lambda (x : List Sexp) -> % x follow the mask -> (_|_ Nat zero (succ Nat)) % Type name --^ ^------^ constructors @@ -77,32 +80,34 @@ type-impl = lambda (x : List Sexp) -> % Add constructors let ctors = - let for-each : List Sexp -> List Sexp -> List Sexp; + let for-each : List Sexp -> Sexp -> Sexp; for-each ctr acc = case ctr | cons hd tl => ( - let acc2 = cons (make-cons (get-name hd) type-name) acc in + let acc2 = chain-decl (make-cons (get-name hd) type-name) acc in for-each tl acc2) | nil => acc - in for-each ctor nil in + in for-each ctor (node_ (symbol_ "_;_") nil) in % return decls - (cons decl % inductive type declaration - ctors); % constructor declarations + (chain-decl decl % inductive type declaration + ctors); % constructor declarations -type_ = DMacro_ type-impl; +type_ = Macro_ type-impl; % (type_ (_|_ (Either t1 t2) (either-first t1) (either-second t2))) %type Either t1 t2 % | either-first t1 % | either-second t2; +type A + | a Int; %type Pair t1 t2 % | pair t1 t2; -type Point t - | point (x : t) (y : t); +%type Point t +% | point (x : t) (y : t); %get-first : (a : Type) => (b : Type) => Pair a b -> a; %get-second : (a : Type) => (b : Type) => Pair a b -> b; ===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -55,34 +55,30 @@ my_sqr = lambda (x : List Sexp) -> | nil => symbol_ "x") : Sexp in (node_ (symbol_ "_*_") (cons hd (cons hd nil))); -my_add = lambda (x : List Sexp) -> - let hd = (case x - | cons hd tl => hd - | nil => symbol_ "x") : Sexp in - (node_ (symbol_ "_=_") (cons hd (cons hd nil))); +% Quote +qq_sqr' = lambda (args : List Sexp) -> + let hd : Sexp; + hd = case args + | cons hd tl => hd + | nil => symbol_ "sqr expects a single argument" in + + quote ((uquote hd) * (uquote hd)); sqr = Macro_ my_sqr; -add = Macro_ my_add; +qqsqr = Macro_ qq_sqr'; + +% fun = Macro_ my_fun; +% main = fun 2; my_fun = lambda (arg : List Sexp) -> let x = sqr 2 in integer_ 2; fun = Macro_ my_fun; -main = fun 2; +main = qqsqr 2; - -% Quote -%my_fun = lambda (args : List Sexp) -> -% let hd : Sexp; -% hd = case args -% | cons hd tl => hd -% | nil => symbol_ "sqr expects a single argument" in -% -% quote ((uquote hd) * (uquote hd)); - -x = 2; -sqr = Macro_ my_fun; +% x = 2; +% sqr = Macro_ my_fun; % main = sqr 2; % a = Macro_ (lambda x -> quote (2 + 2)); @@ -90,4 +86,4 @@ sqr = Macro_ my_fun; % main = a Unit; % main = let x = 2 in quote (x * x); % main = let x = 2 in quote ((uquote x) * (uquote x)); - +% add = Macro_ my_add; ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -74,7 +74,6 @@ let predef_name = [ "false"; "Macro"; "expand_macro_"; - "expand_dmacro_"; ] (* FIXME: Actually, we should map the predefs to *values* since that's ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -155,9 +155,6 @@ let lctx_extend (ctx : lexp_context) (def: vdef option) (v: varbind) (t: lexp) = let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env) = ctx in - (try let _ = senv_lookup name ctx in - warning loc ("Variable Shadowing " ^ name); - with Not_found -> ()); let nmap = SMap.add name n map in ((n + 1, nmap), lexp_ctx_cons env r (Some def) v t) ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -162,8 +162,8 @@ let make_node loc depth args_val = let s = List.map (fun g -> match g with | Vsexp(sxp) -> sxp (* eval transform sexp into those... *) - | Vint (i) -> Integer(dloc, i) - | Vstring (s) -> String(dloc, s) + | Vint (i) -> Integer(dloc, i) + | Vstring (s) -> String(dloc, s) | _ -> (* print_rte_ctx ctx; *) value_error loc g "node_ expects 'List Sexp' second as arguments") args in @@ -284,14 +284,9 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type (* Function call *) | Call (f, args) -> - (* we need to keep the trace from f and args evaluation - * else the trace will be truncated. - * we use _global_eval_trace to keep in memory previous steps *) - let ef = _eval f ctx trace in - let eargs = (List.map (fun e -> _eval e ctx (get_trace ())) args) in - eval_call (elexp_location f) f (get_trace ()) - ef - eargs + eval_call (elexp_location f) f trace + (_eval f ctx trace) + (List.map (fun e -> _eval e ctx trace) args) (* Case *) | Case (loc, target, pat, dflt) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -356,7 +356,7 @@ and parse_special_form ctx f args ot = | None -> (e, inferred_t) | Some t -> let e = check_inferred ctx e inferred_t t in (e, t)) - + | _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); let t = newMetatype loc in (newMetavar loc "<dummy>" t, t) @@ -380,7 +380,7 @@ and get_implicit_arg ctx loc name t = * call a `default-arg-filler` function, implemented in Typer, * just like `expand_macro_` function. That one can then look * things up in a table and/or do anything else it wants. *) - let v = lexp_expand_macro attr [] ctx t in + let v = lexp_expand_macro attr [] ctx (Some t) in (* get the sexp returned by the macro *) let lsarg = match v with @@ -706,7 +706,7 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt) and handle_macro_call ctx func args t = - let sxp = match lexp_expand_macro func args ctx t with + let sxp = match lexp_expand_macro func args ctx (Some t) with | Vsexp (sxp) -> sxp | v -> value_fatal (lexp_location func) v "Macros should return a Sexp" in @@ -820,14 +820,6 @@ and lexp_parse_inductive ctors ctx = SMap.add name (make_args args ctx) lctors) SMap.empty ctors -(* Macro declaration handling, return a list of declarations - * to be processed *) -and lexp_expand_macro macro_funct sargs ctx t - = lexp_expand_macro_ macro_funct sargs ctx (Some t) "expand_macro_" - -and lexp_expand_dmacro macro_funct sargs ctx - = lexp_expand_macro_ macro_funct sargs ctx None "expand_dmacro_" - and track_fv meta_ctx rctx lctx e = let (fvs, mvs) = OL.fv e in let nc = EV.not_closed rctx fvs in @@ -854,10 +846,10 @@ and track_fv meta_ctx rctx lctx e = | _ -> name in String.concat " " (List.map tfv nc) -and lexp_expand_macro_ macro_funct sargs ctx ot expand_fun : value_type = +and lexp_expand_macro macro_funct sargs ctx ot: value_type = (* Build the function to be called *) - let macro_expand = BI.get_predef expand_fun ctx in + let macro_expand = BI.get_predef "expand_macro_" ctx in (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) let args = [(Aexplicit, macro_funct); (Aexplicit, (BI.o2l_list ctx sargs))] in @@ -885,19 +877,13 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = try let lxp, ltp = infer (Pvar (loc, mname)) ctx in (* FIXME: Check that (conv_p ltp Macro)! *) - let ret = lexp_expand_dmacro lxp sargs ctx in - - (* convert typer list to ocaml *) - let decls = BI.v2o_list ret in - - (* extract sexp from result *) - let decls = List.map (fun g -> - match g with - | Vsexp(sxp) -> sxp - | _ -> value_fatal loc g "Macro expects sexp list") decls in + let ret = lexp_expand_macro lxp sargs ctx None in + let decls = match ret with + | Vsexp(sexp) -> sexp + | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp") in (* read as pexp_declaraton *) - pexp_decls_all decls, ctx + pexp_decls_all [decls], ctx with e -> fatal loc ("Macro `" ^ mname ^ "`not found") ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -78,6 +78,19 @@ let rec pexp_location e = | Pcall (f, _) -> pexp_location f | Pcase (l, _, _) -> l +let pexp_name e = + match e with + | Pimm _ -> "Pimm" + | Pbuiltin _ -> "Pbuiltin" + | Pvar (_,_) -> "Pvar" + | Phastype (_,_,_) -> "Phastype" + | Pmetavar (_, _) -> "Pmetavar" + | Plet (_, _, _) -> "Plet" + | Parrow (_, _, _, _, _) -> "Parrow" + | Plambda (_,(_,_), _, _) -> "Plambda" + | Pcall (_, _) -> "Pcall" + | Pcase (_, _, _) -> "Pcase" + let rec pexp_pat_location e = match e with | Ppatany l -> l | Ppatsym (l,_) -> l @@ -271,6 +284,7 @@ and pexp_p_decls e: pdecl list = * once expanded the Pmcall macro will produce a list of pdecl *) | Node (Symbol (l, op), args) -> [Pmcall((l, op), args)] | _ -> + print_string ((sexp_name e) ^ ": \""); sexp_print e; print_string "\"\n"; pexp_error (sexp_location e) ("Unknown declaration"); [] and pexp_unparse (e : pexp) : sexp = @@ -333,8 +347,8 @@ and pexp_u_decls (ds: pdecl list) = | _ -> Node (Symbol (dummy_location, "_;_"), List.map pexp_u_decl ds) -let pexp_print e = sexp_print (pexp_unparse e) - +and pexp_string e = sexp_string (pexp_unparse e) +and pexp_print e = print_string (pexp_string e) (* Parse All Pexp as a list *) let pexp_parse_all (nodes: sexp list) = @@ -371,19 +385,3 @@ 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_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" - | Pbuiltin _ -> "Pbuiltin" - | Pvar (_,_) -> "Pvar" - | Phastype (_,_,_) -> "Phastype" - | Pmetavar (_, _) -> "Pmetavar" - | Plet (_, _, _) -> "Plet" - | Parrow (_, _, _, _, _) -> "Parrow" - | Plambda (_,(_,_), _, _) -> "Plambda" - | Pcall (_, _) -> "Pcall" - | Pcase (_, _, _) -> "Pcase" ===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -71,12 +71,18 @@ let _ = (add_test "MACROS" "macros base" (fun () -> let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " decls-impl = lambda (x : List Sexp) -> - cons (node_ (symbol_ \"_=_\") - (cons (symbol_ \"a\") (cons (integer_ 1) nil))) - (cons (node_ (symbol_ \"_=_\") - (cons (symbol_ \"b\") (cons (integer_ 2) nil))) nil); + let chain-decl : Sexp -> Sexp -> Sexp; + chain-decl a b = node_ (symbol_ \"_;_\") (cons a (cons b nil)) in - my-decls = DMacro_ decls-impl; + let make-decl : String -> Int -> Sexp; + make-decl name val = + (node_ (symbol_ \"_=_\") (cons (symbol_ name) (cons (integer_ val) nil))) in + + let d1 = make-decl \"a\" 1 in + let d2 = make-decl \"b\" 2 in + chain-decl d1 d2; + + my-decls = Macro_ decls-impl; my-decls Nat;" in View it on GitLab: https://gitlab.com/monnier/typer/compare/f4630a769d53d108f6d6d0687ad9b3baca…

1 0

[Git][monnier/typer][master] Rename `inductive_` to `typecons` and make it a special-form
by Stefan 15 Dec '16

15 Dec '16

Stefan pushed to branch master at Stefan / Typer Commits: f4630a76 by Stefan Monnier at 2016-12-15T09:25:53-05:00 Rename `inductive_` to `typecons` and make it a special-form * src/lexp.ml (ptypecons): New var. (lexp_unparse): Don't use Pinductive. * src/lparse.ml (infer): Move Pinductive case to sform_typecons. (sform_typecons): New function. (register_special_forms): Add it. * src/pexp.ml (pexp): Remove Pinductive. (pexp_parse): Don't recognize `inductive_` any more. (pexp_unparse): Move Pinductive case to lexp_unparse. * src/tweak.ml (Make.create): Use new name Array.make. - - - - - 14 changed files: - btl/builtins.typer - samples/autodiff.typer - samples/dependent.typer - samples/error.typer - samples/inductive.typer - samples/nat.typer - samples/pervasive.typer - src/elexp.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/tweak.ml - tests/eval_test.ml - tests/unify_test.ml Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -36,11 +36,11 @@ % ----------------------------------------------------- % The trivial type which carries no information. -Unit = inductive_ Unit unit; +Unit = typecons Unit unit; unit = datacons Unit unit; % The empty type, with no constructors: nothing can have this type. -Void = inductive_ Void; +Void = typecons Void; % Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l % Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l @@ -96,11 +96,11 @@ _-_ = Built-in "Int.-" (Int -> Int -> Int); _*_ = Built-in "Int.*" (Int -> Int -> Int); _/_ = Built-in "Int./" (Int -> Int -> Int); -Bool = inductive_ (Boolean) (true) (false); +Bool = typecons (Boolean) (true) (false); true = datacons Bool true; false = datacons Bool false; -Option = inductive_ (Option (a : Type)) (none) (some a); +Option = typecons (Option (a : Type)) (none) (some a); some = datacons Option some; none = datacons Option none; @@ -113,7 +113,7 @@ sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); % ----------------------------------------------------- List : Type -> Type; -List = inductive_ (List (a : Type)) (nil) (cons a (List a)); +List = typecons (List (a : Type)) (nil) (cons a (List a)); nil = datacons List nil; cons = datacons List cons; @@ -156,7 +156,7 @@ node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp); integer_ = Built-in "integer_" (Int -> Sexp); float_ = Built-in "float_" (Float -> Sexp); -Macro = inductive_ (Macro) +Macro = typecons (Macro) (Macro_ (List Sexp -> Sexp)) (DMacro_ (List Sexp -> List Sexp)); @@ -231,5 +231,5 @@ Not : Type -> Type; Not prop = prop -> False; % Like Bool, except that it additionally carries the meaning of its value. -Decidable = inductive_ (Decidable (prop : Type)) - (true (p ::: prop)) (false (p ::: Not prop)); +Decidable = typecons (Decidable (prop : Type)) + (true (p ::: prop)) (false (p ::: Not prop)); ===================================== samples/autodiff.typer ===================================== --- a/samples/autodiff.typer +++ b/samples/autodiff.typer @@ -36,7 +36,7 @@ %* ---------------------------------------------------------------------------*) Sym : Type; -Sym = inductive_ (dSym) +Sym = typecons (dSym) % leafs (constant Int) (placeholder String) ===================================== samples/dependent.typer ===================================== --- a/samples/dependent.typer +++ b/samples/dependent.typer @@ -1,5 +1,5 @@ -Reify = inductive_ (Reify (a : Type)) +Reify = typecons (Reify (a : Type)) (RInt (Eq (t := Type) Int a)) (RFloat (Eq (t := Type) Float a)) (RString (Eq (t := Type) String a)); ===================================== samples/error.typer ===================================== --- a/samples/error.typer +++ b/samples/error.typer @@ -45,10 +45,10 @@ v = (a 2); m = lambda n -> n; % [!] Error [Ln 27, cl 28] LPARSE Constructor "cons3" does not exist -% > inductive_: (inductive_ e (cons1) (cons2 Int)) +% > typecons: (typecons e (cons1) (cons2 Int)) % > Root: -idt = inductive_ (idt) (cons1) (cons2 Int); +idt = typecons (idt) (cons1) (cons2 Int); cons1 = datacons idt cons1; cons2 = datacons idt cons2; cons3 = datacons idt cons3; @@ -94,7 +94,7 @@ fun2 n = case n % [!] Error [Ln 87, cl 1] LPARSE `fun4` defined but not declared! % [!] Error [Ln 86, cl 1] LPARSE Variable `fun4` declared but not defined! -% idtb = inductive_ (idtb) (cons1b) (cons2b Int); +% idtb = typecons (idtb) (cons1b) (cons2b Int); % cons1b = datacons idtb cons1b; % cons2b = datacons idtb cons2b; ===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -70,7 +70,7 @@ type-impl = lambda (x : List Sexp) -> let type-name = get-name name in % Create the inductive type definition - let inductive = node_ (symbol_ "inductive_") + let inductive = node_ (symbol_ "typecons") (cons name ctor) in let decl = make-decl type-name inductive in @@ -118,6 +118,6 @@ type Point t % transformed to: % Nat : Type; -% Nat = inductive_ (Nat) (succ Nat) (zero); +% Nat = typecons (Nat) (succ Nat) (zero); % zero = datacons Nat zero; % succ = datacons Nat succ; ===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -1,5 +1,5 @@ Nat : Type; -Nat = inductive_ (dNat) (zero) (succ Nat); +Nat = typecons (dNat) (zero) (succ Nat); zero = datacons Nat zero; succ = datacons Nat succ; ===================================== samples/pervasive.typer ===================================== --- a/samples/pervasive.typer +++ b/samples/pervasive.typer @@ -1,13 +1,13 @@ %% (_=_) = (l : TypeLevel) ≡> (t : Type@ l) ≡> t -> t -> Type; -Nat = inductive_ Type (zero : Nat) (succ : Nat -> Nat); +Nat = typecons Type (zero : Nat) (succ : Nat -> Nat); -Macro = inductive_ Type (MacroExp : Nat -> Macro); +Macro = typecons Type (MacroExp : Nat -> Macro); %% Use for `cast'. -Equiv = inductive_ (t -> t -> Type) (refl: Equiv a a); +Equiv = typecons (t -> t -> Type) (refl: Equiv a a); -or = inductive_ (t -> t -> Type) +or = typecons (t -> t -> Type) (left: t1 -> or t1 t2) (right: t2 -> or t1 t2); ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -133,6 +133,6 @@ and elexp_string lxp = "case " ^ (elexp_string t) ^ (str_cases cases) ^ (maybe_str default) | Inductive(_, (_, s)) -> - "inductive_ " ^ s + "typecons " ^ s | Type -> "Type " ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -349,7 +349,7 @@ let lexp_name e = | Call _ -> "Call" | Cons _ -> "datacons" | Case _ -> "case" - | Inductive _ -> "inductive_" + | Inductive _ -> "typecons" | Susp _ -> "Susp" | Builtin (_, _, None) -> "Builtin" | Builtin _ -> "AttributeTable" @@ -358,6 +358,7 @@ let lexp_name e = | SortLevel _ -> "SortLevel" let pdatacons = Pbuiltin (U.dummy_location, "datacons") +let ptypecons = Pbuiltin (U.dummy_location, "typecons") (* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = @@ -387,7 +388,7 @@ let rec lexp_unparse lxp = let sargs = List.map (fun elem -> pexp_unparse elem) pargs in Pcall(lexp_unparse lxp, sargs) - | Inductive(loc, label, lfargs, ctor) -> + | Inductive(loc, label, lfargs, ctors) -> (* (arg_kind * vdef * ltype) list *) (* (arg_kind * pvar * pexp option) list *) let pfargs = List.map (fun (kind, vdef, ltp) -> @@ -395,14 +396,19 @@ let rec lexp_unparse lxp = (* ((arg_kind * vdef option * ltype) list) SMap.t *) (* (symbol * (arg_kind * pvar option * pexp) list) list *) - let ctor = List.map (fun (str, largs) -> + let ctors = List.map (fun (str, largs) -> let pargs = List.map (fun (kind, var, ltp) -> match var with | Some (loc, name) -> (kind, Some (loc, name), lexp_unparse ltp) | None -> (kind, None, lexp_unparse ltp)) largs in ((loc, str), pargs) - ) (SMap.bindings ctor) - in Pinductive(label, pfargs, ctor) + ) (SMap.bindings ctors) in + Pcall (ptypecons, + Node (Symbol label, List.map pexp_u_formal_arg pfargs) + :: List.map (fun ((l,name) as s, types) + -> Node (Symbol s, + List.map pexp_u_ind_arg types)) + ctors) | Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in @@ -638,7 +644,7 @@ and _lexp_to_str ctx exp = add_parens outer_parens str) | Inductive (_, (_, name), [], ctors) -> - (keyword "inductive_") ^ " (" ^ name ^") " ^ + (keyword "typecons") ^ " (" ^ name ^") " ^ (lexp_str_ctor ctx ctors) | Inductive (_, (_, name), args, ctors) @@ -649,7 +655,7 @@ and _lexp_to_str ctx exp = ^ (lexp_to_str ltype) ^ ")") "" args in - (keyword "inductive_") ^ " (" ^ name ^ args_str ^") " + (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ (lexp_str_ctor ctx ctors) | Case (_, target, _ret, map, dflt) ->( ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -306,30 +306,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = let v = mkArrow(kind, ovar, ltp, tloc, lxp) in v, type0 - | Pinductive (label, formal_args, ctors) - -> let nctx = ref ctx in - (* (arg_kind * pvar * pexp option) list *) - let formal = List.map (fun (kind, var, opxp) - -> let ltp = match opxp with - | Some pxp -> let (l,_) = infer pxp !nctx in l - | None -> let (l,_) = var in newMetatype l in - - nctx := env_extend !nctx var Variable ltp; - (kind, var, ltp)) - formal_args in - - let nctx = !nctx in - let ltp = List.fold_left (fun tp (kind, v, ltp) - -> (mkArrow (kind, Some v, ltp, tloc, tp))) - (* FIXME: See OL.check for how to - * compute the real target sort - * (not always type0). *) - type0 (List.rev formal) in - - let map_ctor = lexp_parse_inductive ctors nctx in - let v = mkInductive(tloc, label, formal, map_ctor) in - v, ltp - (* This case can be inferred. *) | Plambda (kind, var, Some ptype, body) -> let ltp = infer_type ptype ctx (Some var) in @@ -1156,6 +1132,50 @@ let sform_datacons ctx loc sargs ot = | _ -> sexp_error loc "##constr requires two arguments"; sform_dummy_ret loc +let sform_typecons ctx loc sargs ot = + match sargs with + | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type loc, Lazy) + | formals :: constrs + -> let (label, formals) = match formals with + | Node (label, formals) -> (label, formals) + | _ -> (formals, []) in + let label = match label with + | Symbol label -> label + | _ -> let loc = sexp_location label in + sexp_error loc "Unrecognized inductive type name"; + (loc, "<error>") in + + let rec parse_formals sformals rformals ctx = match sformals with + | [] -> (List.rev rformals, ctx) + | sformal :: sformals + -> let (kind, var, opxp) = pexp_p_formal_arg sformal in + let ltp = match opxp with + | Some pxp -> let (l,_) = infer pxp ctx in l + | None -> let (l,_) = var in newMetatype l in + + parse_formals sformals ((kind, var, ltp) :: rformals) + (env_extend ctx var Variable ltp) in + + let (formals, nctx) = parse_formals formals [] ctx in + + let ctors + = List.fold_right + (fun case pcases + -> match case with + (* read Constructor name + args => Type ((Symbol * args) list) *) + | Node (Symbol s, cases) + -> (s, List.map pexp_p_ind_arg cases)::pcases + (* This is a constructor with no args *) + | Symbol s -> (s, [])::pcases + + | _ -> sexp_error (sexp_location case) + "Unrecognized constructor declaration"; + pcases) + constrs [] in + + let map_ctor = lexp_parse_inductive ctors nctx in + (mkInductive (loc, label, formals, map_ctor), Lazy) + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1195,6 +1215,7 @@ let register_special_forms () = [ ("Built-in", sform_built_in); ("datacons", sform_datacons); + ("typecons", sform_typecons); ("Type_", sform_type); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute); ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -49,8 +49,6 @@ type pexp = | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two * otherwise isomorphic types. *) - | Pinductive of symbol * (arg_kind * pvar * pexp option) list - * (symbol * (arg_kind * pvar option * pexp) list) list | Pcase of location * pexp * (ppat * pexp) list and ppat = @@ -78,7 +76,6 @@ let rec pexp_location e = | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l | Pcall (f, _) -> pexp_location f - | Pinductive ((l,_), _, _) -> l | Pcase (l, _, _) -> l let rec pexp_pat_location e = match e with @@ -146,29 +143,6 @@ let rec pexp_parse (s : sexp) : pexp = (pexp_parse body) | Node (Symbol (start, "lambda_"), _) -> pexp_error start "Unrecognized lambda expression"; Pmetavar (start, "_") - (* inductive type *) - | Node (Symbol (start, "inductive_"), t :: cases) - -> let (name, args) = match t with - | Node (Symbol s, args) -> (s, args) (* This a constructor *) - | Symbol s -> (s, []) (* This is a Label *) - | _ -> pexp_error start "Unrecognized inductive type name"; - ((dummy_location, ""), []) in - let pcases = - List.fold_right - (fun case pcases - -> match case with - (* read Constructor name + args => Type ((Symbol * args) list) *) - | Node (Symbol s, cases) - -> (s, List.map pexp_p_ind_arg cases)::pcases - (* This is a constructor with no args *) - | Symbol s -> (s, [])::pcases - - | _ -> pexp_error (sexp_location case) - "Unrecognized constructor declaration"; pcases) - cases [] in - Pinductive (name, List.map pexp_p_formal_arg args, pcases) - | Node (Symbol (start, "inductive_"), _) - -> pexp_error start "Unrecognized inductive type"; Pmetavar (start, "_") (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -331,14 +305,6 @@ and pexp_unparse (e : pexp) : sexp = [Symbol v; pexp_unparse t])); pexp_unparse body]) | Pcall (f, args) -> Node (pexp_unparse f, args) - (* Pinductive *) - | Pinductive (s, t, branches) -> - Node (Symbol (dummy_location, "inductive_"), - sexp_u_list (List.map pexp_u_formal_arg t) - :: List.map (fun ((l,name) as s, types) - -> Node (Symbol s, - List.map pexp_u_ind_arg types)) - branches) | Pcase (start, e, branches) -> Node (Symbol (start, "case_"), pexp_unparse e @@ -420,5 +386,4 @@ let pexp_name e = | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" | Pcall (_, _) -> "Pcall" - | Pinductive ((_,_), _, _) -> "Pinductive" | Pcase (_, _, _) -> "Pcase" ===================================== src/tweak.ml ===================================== --- a/src/tweak.ml +++ b/src/tweak.ml @@ -53,8 +53,8 @@ module Make (H : Hashtbl.HashedType) : (S with type data = H.t) = struct let sz = if sz < 7 then 7 else sz in let sz = if sz > Sys.max_array_length then Sys.max_array_length else sz in { - table = Array.create sz emptybucket; - hashes = Array.create sz [| |]; + table = Array.make sz emptybucket; + hashes = Array.make sz [| |]; limit = limit; oversize = 0; rover = 0; ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -87,7 +87,7 @@ let _ = test_eval_eqv_named "c = 3; e = 1; f = 2; d = 4;" - "let TrueProp = inductive_ TrueProp I; + "let TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3" @@ -99,7 +99,7 @@ let _ = test_eval_eqv_named "let TrueProp : Type; I : TrueProp; - TrueProp = inductive_ TrueProp I; + TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3" @@ -135,7 +135,7 @@ let _ = test_eval_eqv_named "i = 90; idt : Type; - idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); + idt = typecons (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); d = 10; ctr0 = datacons idt ctr0; e = 20; ctr1 = datacons idt ctr1; f = 30; @@ -159,7 +159,7 @@ let _ = test_eval_eqv_named (* Those wil be used multiple times *) let nat_decl = " Nat : Type; - Nat = inductive_ (dNat) (zero) (succ Nat); + Nat = typecons (dNat) (zero) (succ Nat); zero = datacons Nat zero; succ = datacons Nat succ; @@ -248,7 +248,7 @@ let _ = test_eval_eqv_named (cons 3 (cons 4 nil))); List' = let L : Type -> Type; - L = inductive_ (L (a : Type)) (nil) (cons a (L a)) + L = typecons (L (a : Type)) (nil) (cons a (L a)) in L; cons' = datacons List' cons; nil' = datacons List' nil; @@ -325,7 +325,7 @@ let _ = test_eval_eqv_named "Metavars" let _ = test_eval_eqv_named "Explicit field patterns" - "Triplet = inductive_ Triplet + "Triplet = typecons Triplet (triplet (a ::: Int) (b :: Float) (c : String) (d :: Int)); triplet = datacons Triplet triplet; t = triplet (b := 5.0) (a := 3) (d := 7) (c := \"hello\");" ===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -78,7 +78,7 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = ) str_lst (* Inputs for the test *) -let str_induct = "Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat)" +let str_induct = "Nat : Type; Nat = typecons (dNat) (zero) (succ Nat)" let str_int_3 = "i = 3" let str_int_4 = "i = 4" let str_case = "i = case true View it on GitLab: https://gitlab.com/monnier/typer/commit/f4630a769d53d108f6d6d0687ad9b3baca5…

1 0

[Git][monnier/typer][master] Add the Y operator in a safe(?) way
by Stefan 13 Dec '16

13 Dec '16

Stefan pushed to branch master at Stefan / Typer Commits: 9c9a1a0e by Stefan Monnier at 2016-12-13T13:09:11-05:00 Add the Y operator in a safe(?) way * btl/builtins.typer (Y): Give its type. * src/eval.ml (y_operator): New function. (register_built_functions): Add "Y" operator. * tests/eval_test.ml ("Y"): New test. - - - - - 4 changed files: - btl/builtins.typer - src/eval.ml - src/lparse.ml - tests/eval_test.ml Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -62,6 +62,34 @@ Eq_comm = lambda l t x y ≡> lambda p -> (p := p) Eq_refl; +%% General recursion!! +%% Whether this breaks onsistency or not is a good question. +%% The basic idea is the following: +%% +%% The `witness` argument presumably makes sure that "Y f" can only +%% create new recursive values for types which were already inhabited. +%% So there's no `f` such that `Y f : False`. +%% +%% But this is not sufficient, because you could use `Y` to create +%% new recursive *types* which then let you construct new arbitrary +%% recursive values of previously uninhabited types. +%% E.g. you could create Y <something> = ((... → t) -> t) -> t +%% and then give the term "λx. x x" inhabiting that type, and from that +%% get a proof of False. +%% +%% So we have a secondary restriction: This `Y` is a builtin primitive/axiom +%% with no reduction rule, so that Y <something> is never convertible +%% to something like ((... → t) -> t) -> t +%% +%% Of course, we do have a "natural" evaluation rule for it, so after type +%% checking we can run our recursive functions just fine, but those +%% recursive functions won't be unfolded during type checking. +%% +%% FIXME: Really, this Y should be used internally/transparently for any +%% function which has not been termination-checked successfully (or at all). +Y = Built-in "Y" ((a : Type) ≡> (b : Type) ≡> (witness : a -> b) ≡> + ((a -> b) -> (a -> b)) -> (a -> b)); + % Basic operators _+_ = Built-in "Int.+" (Int -> Int -> Int); _-_ = Built-in "Int.-" (Int -> Int -> Int); ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -559,6 +559,21 @@ and print_eval_trace trace = let (a, b) = !_global_eval_trace in print_trace " EVAL TRACE " trace a +let y_operator loc depth args = + match args with + | [f] -> let aname = "<anon>" in + let yf_ref = ref Vdummy in + let yf = Closure(aname, + Call (Var ((dloc, "f"), 1), + [Var ((dloc, "yf"), 2); + Var ((dloc, aname), 0)]), + Myers.cons (Some "f", ref f) + (Myers.cons (Some "yf", yf_ref) + Myers.nil)) in + yf_ref := yf; + yf + | _ -> error loc ("Y expects 1 (function) argument") + let arity0_fun loc _ _ = error loc "Called a 0-arity function!?" let nop_fun loc _ vs = match vs with | [v] -> v @@ -584,6 +599,7 @@ let register_built_functions () = ("write" , write_impl, 2); ("Eq.refl" , arity0_fun, 0); ("Eq.cast" , nop_fun, 1); + ("Y" , y_operator, 1); ] let _ = register_built_functions () ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -597,6 +597,9 @@ and check_case rtype (loc, target, ppatterns) ctx = | _ -> (e,[]) in let it, targs = call_split tltp in let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) meta_ctx with + (* FIXME: Check that it's `Inductive' only after performing Unif.unify + * with the various branches, so that we can infer the type + * of the target from the type of the patterns. *) | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -379,6 +379,20 @@ let _ = test_eval_eqv_named | (datacons ? false) (p := _) => 4;" "3;" +let _ = test_eval_eqv_named + "Y" + + "length_y = lambda t ≡> + Y (a := List t) (witness := (lambda l -> 0)) + (lambda length l + -> case l + | nil => 0 + | cons _ l => 1 + length l);" + + "length_y (cons 1 (cons 5 nil));" + + "2;" + (* run all tests *) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/commit/9c9a1a0ed83707b907ee1705eae806c8494…

1 0

Finding names for error messages
by Stefan Monnier 11 Dec '16

11 Dec '16

Hello, Here's another one of my design rants... Here's another problem we have in Typer: currently error messages will often print types as some horrendous unintelligible expression. This was made worse by my change to make builtins "closed", since now `List` is not shown as `List` any more but as let List : Type -> Type; List = inductive_ (List t) nil (cons t (List t)) in List or some less pretty rendition thereof. I have some idea for how to improve this, e.g. when printing a `lexp`, we should look up some hash-table which will give some candidate var-name, then confirm in the lexp_context that this var's name indeed is equivalent to the lexp we're trying to print. [ Of course, a hash-table indexed by a `lexp` is a problem in itself, since a given `lexp` can/will be different depending on the context in which it appears (because of debruijn indices being adjusted). But that's a problem we will need to solve somehow anyway. ] But that's just the beginning of our problems. E.g. Let's say we have a `Tree` module, whose type would be `Set.t`. In reality, `Tree.t` is actually a macro call (i.e. it's equivalent to `__\.__ Tree t` which would presumably expand to something like `case Tree | cons (t := x) => x`) which will select the first `t` from the value `Tree`. So now, how do I go back from the `lexp` that represents this tree type (which will probably look like some `let Tree = ... in Tree` or something even more cumbersome) to `Tree.t`? It seems this calls for an even more general "reverse lparse" hash-table, which maps all lexps we have elaborated back to their corresponding source code (probably as an sexp since pexp is on the way of the dodo), so that when we try to print a lexp, we look this up in the table to see if this lexp actually existed in the source code and use that source's format. Hmm... maybe, instead of a hash-table, we should "simply" replace the `location` info (currently file+line+column) with a reference to the corresponding source sexp. Admittedly, this is not as simple as it sounds: some of the manipulations we do on `lexp` will result in an `lexp` that's not equivalent to any of the `sexps` we got, so either we dynamically try to create a corresponding `sexp`, or this "original sexp" data should be optional. And it won't solve our `Tree.t` problem, since the tree type returned by (say) `Tree.insert` was not elaborated from `Tree.t` but from the representation used before creating the `Tree` module/object. A different avenue might be to provide some primitive that the __\.__ macro could use to "register" the `Tree.t` sexp in some hash-table, so that if we later see the same type we can know that it can *also* be referred to as `Tree.t` even when this occurrence of the type wasn't originally elaborated from a source code of the form `Tree.t`. Stefan

1 0

[Git][monnier/typer][master] Handle special forms and macros in `check` as well
by Stefan 07 Dec '16

07 Dec '16

Stefan pushed to branch master at Stefan / Typer Commits: f19ead0d by Stefan Monnier at 2016-12-07T15:33:18-05:00 Handle special forms and macros in `check` as well * src/lparse.ml (dlxp, dltype): Remove. (sform_type): New datatype. (special_forms_map): Make the functions return it and optionally take the expected type as well. (get_special_form): Don't catch errors. (newMetatype): Take a `loc` argument as well. (mkDummy_type, mkDummy_check, mkDummy_infer): New functions. (infer) <Pcall>: Check the type a dispatch for special-forms or macros. (parse_special_form): New function, extracted from infer_call. (get_implicit_arg): Pass expected type to lexp_expand_macro. (check) <Pcall>: Handle it as well. (check_inferred): New function extracted from infer_and_check. (infer_and_check): Use it. (handle_macro_call): Extract from infer_call. (infer_call): Remove the macro and special-form handling. (lexp_parse_inductive.make_args.loop): Pass actual type to ectx_extend. (lexp_expand_macro): Add expected-type argument. (track_fv): New function. (lexp_expand_macro_): Use it to give more complete error message. (sform_*): Adjust to new calling convention. (default_rctx): Pass the actual meta_ctx! * src/debruijn.ml (dltype): Remove. - - - - - 3 changed files: - src/debruijn.ml - src/eval.ml - src/lparse.ml Changes: ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -92,9 +92,6 @@ let type_int = mkBuiltin ((dloc, "Int"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) -(* FIXME: Make it a metavar. *) -let dltype = type0 - (* easier to debug with type annotations *) type env_elem = (db_offset * vdef option * varbind * ltype) type lexp_context = env_elem M.myers ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -624,8 +624,9 @@ module CMap let ctx_memo = CMap.create 1000 let not_closed rctx ((o, vm) : DB.set) = - VMap.fold (fun i () nc -> let (_, rc) = Myers.nth (i + o) rctx in - match !rc with Vundefined -> (i+o)::nc | _ -> nc) + VMap.fold (fun i () nc -> let i = i + o in + let (_, rc) = Myers.nth i rctx in + match !rc with Vundefined -> i::nc | _ -> nc) vm [] let closed_p rctx (fvs, mvs) = ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -58,8 +58,6 @@ let make_var name index loc = mkVar (((loc, name), index)) (* dummies *) -let dlxp = type0 -let dltype = type0 let dloc = dummy_location let _global_lexp_ctx = ref make_elab_context @@ -88,8 +86,14 @@ 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 + | Checked + | Lazy + type special_forms_map = - (elab_context -> location -> sexp list -> lexp) SMap.t + (elab_context -> location -> sexp list -> ltype option + -> (lexp * sform_type)) SMap.t let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0 @@ -98,9 +102,8 @@ let add_special_form (name, func) = BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form, None)); special_forms := SMap.add name func (!special_forms) -let get_special_form loc name = - try SMap.find name (!special_forms) - with Not_found -> fatal loc ("Special form `" ^ name ^ "` not found!") +let get_special_form name = + SMap.find name (!special_forms) (* The prefix `elab_check_` is used for functions which do internal checking @@ -237,7 +240,14 @@ let newMetavar l name t = let newMetalevel () = newMetavar Util.dummy_location "l" (mkSort (dummy_location, StypeLevel)) -let newMetatype () = newMetavar Util.dummy_location "t" (newMetalevel ()) +let newMetatype loc = newMetavar loc "t" (newMetalevel ()) + +(* Functions used when we need to return some lexp/ltype but + * an error makes it impossible to return "the right one". *) +let mkDummy_type loc = newMetatype loc +let mkDummy_check loc t = newMetavar loc "dummy" t +let mkDummy_infer loc = + let t = newMetatype loc in (mkDummy_check loc t, t) let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = @@ -256,13 +266,13 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = | Float _ -> DB.type_float | String _ -> DB.type_string; | _ -> pexp_error tloc p "Could not find type"; - dltype) + mkDummy_type tloc) | Pbuiltin (l,name) -> (try SMap.find name (! BI.lmap) with Not_found -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); - dlxp, dltype) + mkDummy_infer l) (* Symbol i.e identifier. *) | Pvar (loc, name) @@ -276,8 +286,7 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = with Not_found -> (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); - (* Error recovery. The -1 index will raise an error later on *) - (make_var name (-1) loc), dltype)) + mkDummy_infer loc)) (* Let, Variable declaration + local scope. *) | Plet (loc, decls, body) @@ -301,9 +310,9 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = -> let nctx = ref ctx in (* (arg_kind * pvar * pexp option) list *) let formal = List.map (fun (kind, var, opxp) - -> let ltp, _ = match opxp with - | Some pxp -> infer pxp !nctx - | None -> dltype, dltype in + -> let ltp = match opxp with + | Some pxp -> let (l,_) = infer pxp !nctx in l + | None -> let (l,_) = var in newMetatype l in nctx := env_extend !nctx var Variable ltp; (kind, var, ltp)) @@ -331,16 +340,50 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = let lambda_type = mkArrow (kind, Some var, ltp, tloc, lbtp) in mkLambda(kind, var, ltp, lbody), lambda_type - | Pcall (fname, args) -> infer_call fname args ctx + | Pcall (func, args) + -> let (f, t) as ft = infer func ctx in + let meta_ctx, _ = !global_substitution in + if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t type_special_form) then + parse_special_form ctx f args None + else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t + (BI.get_predef "Macro" ctx)) then + let t = newMetatype (pexp_location func) in + let lxp = handle_macro_call ctx f args t in + (lxp, t) + else + infer_call ctx ft args | Phastype (_, pxp, ptp) -> let ltp = infer_type ptp ctx None in (check pxp ltp ctx, ltp) | (Plambda _ | Pcase _ | Pmetavar _) - -> let t = newMetatype () in - let lxp = check p t ctx in - (lxp, t) + -> let t = newMetatype (pexp_location p) in + let lxp = check p t ctx in + (lxp, t) + +and parse_special_form ctx f args ot = + let loc = lexp_location f in + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf f (ectx_to_lctx ctx) meta_ctx with + | Builtin ((_, name), _, _) -> + (* Special form. *) + let (e, ot') = (get_special_form name) ctx loc args None in + (* `ot` is None if we're inferring and `Some t` if we're checking. *) + (match (ot, ot') with + | (Some t, Checked) -> (e, t) + | _ -> let inferred_t = match ot' with + | Inferred t -> t + | _ -> let meta_ctx, _ = !global_substitution in + OL.get_type meta_ctx (ectx_to_lctx ctx) e in + match ot with + | None -> (e, inferred_t) + | Some t -> let e = check_inferred ctx e inferred_t t in + (e, t)) + + | _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); + let t = newMetatype loc in + (newMetavar loc "<dummy>" t, t) (* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc name t = @@ -361,7 +404,7 @@ and get_implicit_arg ctx loc name t = * call a `default-arg-filler` function, implemented in Typer, * just like `expand_macro_` function. That one can then look * things up in a table and/or do anything else it wants. *) - let v = lexp_expand_macro attr [] ctx in + let v = lexp_expand_macro attr [] ctx t in (* get the sexp returned by the macro *) let lsarg = match v with @@ -425,9 +468,9 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = _global_lexp_ctx := ctx; let unify_with_arrow lxp kind var aty subst = - let body = newMetatype () in + let body = newMetatype tloc in let arg = match aty with - | None -> newMetatype () + | None -> newMetatype tloc | Some laty -> laty in let l, _ = var in let arrow = mkArrow (kind, Some var, arg, l, body) in @@ -436,13 +479,13 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = ^ " and " ^ lexp_string arrow ^ " does not match"); - dltype, dltype + (mkDummy_type l, mkDummy_type l) | Some (_, (t1,t2)::_) -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 ^ " and " ^ lexp_string t2 ^ " do not match"); - dltype, dltype + (mkDummy_type l, mkDummy_type l) | Some subst -> global_substitution := subst; arg, body in @@ -481,8 +524,17 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = | Pcase (loc, target, branches) -> check_case t (loc, target, branches) ctx - (* FIXME: Handle *macro* pcalls here! *) - (* | Pcall (fname, _args) -> *) + | Pcall (func, args) + -> let (f, ft) = infer func ctx in + let meta_ctx, _ = !global_substitution in + if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft type_special_form) then + let (e, _) = parse_special_form ctx f args (Some t) in e + else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft + (BI.get_predef "Macro" ctx)) then + handle_macro_call ctx f args t + else + let (e, inferred_t) = infer_call ctx (f, ft) args in + check_inferred ctx e inferred_t t | Pmetavar (l,"") -> newMetavar l "v" t | Pmetavar (l, name) @@ -493,6 +545,13 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = and infer_and_check pexp ctx t = let (e, inferred_t) = infer pexp ctx in + check_inferred ctx e inferred_t t + +(* This is a crucial function: take an expression `e` of type `inferred_t + * and convert it into something of type `t`. Currently the only conversion + * we use is to instantiate implicit arguments when needed, but we could/should + * do lots of other things. *) +and check_inferred ctx e inferred_t t = let subst, _ = !global_substitution in let (e, inferred_t) = match OL.lexp_whnf t (ectx_to_lctx ctx) subst with | Arrow ((Aerasable | Aimplicit), _, _, _, _) @@ -500,12 +559,12 @@ and infer_and_check pexp ctx t = | _ -> instantiate_implicit e inferred_t ctx in (match Unif.unify inferred_t t (ectx_to_lctx ctx) subst with | None - -> lexp_error (pexp_location pexp) e + -> lexp_error (lexp_location e) e ("Type mismatch! Context expected `" ^ lexp_string t ^ "` but expression has type `" ^ lexp_string inferred_t ^ "`") | Some (_, (t1,t2)::_) - -> lexp_error (pexp_location pexp) e + -> lexp_error (lexp_location e) e ("Type mismatch! Context expected `" ^ lexp_string t2 ^ "` but expression has type `" ^ lexp_string t1 ^ "`") @@ -667,20 +726,26 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt) +and handle_macro_call ctx func args t = + let sxp = match lexp_expand_macro func args ctx t with + | Vsexp (sxp) -> sxp + | v -> value_fatal (lexp_location func) v + "Macros should return a Sexp" in + + let pxp = pexp_parse sxp in + check pxp t ctx + (* Identify Call Type and return processed call. *) -and infer_call (func: pexp) (sargs: sexp list) ctx = - let loc = pexp_location func in - let meta_ctx, _ = !global_substitution in +and infer_call ctx (func, ltp) (sargs: sexp list) = + let loc = lexp_location func in (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned * Macro : sqr is returned * Constructor : a constructor is returned * Anonymous : lambda *) - (* retrieve function's body (sqr 3) sqr is a Pvar() *) - let body, ltp = infer func ctx in - let rec handle_fun_args largs sargs pending ltp = + let meta_ctx, _ = !global_substitution in let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx in match sargs, ltp' with | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) @@ -720,7 +785,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = when not (sargs = [] && SMap.is_empty pending) -> let larg = get_implicit_arg ctx (match sargs with - | [] -> pexp_location func + | [] -> loc | sarg::_ -> sexp_location sarg) (match v with Some (_, name) -> name | _ -> "v") arg_type in @@ -732,7 +797,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = let loc = match pending with | (_, sarg)::_ -> sexp_location sarg | _ -> assert false in - pexp_error loc func + lexp_error loc func ("Explicit actual args `" ^ String.concat ", " (List.map (fun (l, _) -> l) pending) @@ -751,47 +816,8 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = ("Explicit arg `" ^ sexp_string sarg ^ "` to non-function (type = " ^ lexp_string ltp ^ ")") in - let handle_funcall () = - let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in - mkCall (body, List.rev largs), ret_type in - - let handle_macro_call () = - let sxp = match lexp_expand_macro body sargs ctx with - | Vsexp(sxp) -> sxp - (* Those are sexp converted by the eval function *) - | Vint(i) -> Integer(dloc, i) - | Vstring(s) -> String(dloc, s) - | Vfloat(f) -> Float(dloc, f) - | v -> - value_fatal loc v "Macro_ expects `(List Sexp) -> Sexp`" in - - let pxp = pexp_parse sxp in - infer pxp ctx in - - (* This is the builtin Macro type *) - let macro_type = BI.get_predef "Macro" ctx in - - (* determine function type *) - if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ltp type_special_form) then - match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with - | Builtin ((_, name), _, _) -> - (* Special form. *) - (* FIXME: Special forms like `##case_` and `##lambda_` - * want to know the context's expected type. - * Also, for `##_->_`, calling `check` would be algorithmically - * expensive: a complexity of O(N²) for t₁ → t₂ ... → tₙ. *) - let e = (get_special_form loc name) ctx loc sargs in - let meta_ctx, _ = !global_substitution in - (e, OL.get_type meta_ctx (ectx_to_lctx ctx) e) - - | _ -> lexp_error loc body ("Unknown special-form: " - ^ lexp_string body); - let t = newMetatype () in - (newMetavar loc "<dummy>" t, t) - else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ltp macro_type) then - handle_macro_call () - else - handle_funcall () + let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in + mkCall (func, List.rev largs), ret_type (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -805,7 +831,7 @@ and lexp_parse_inductive ctors ctx = match hd with | (kind, var, exp) -> let lxp = infer_type exp ctx var in - let nctx = ectx_extend ctx var Variable dltype in + let nctx = ectx_extend ctx var Variable lxp in loop tl ((kind, var, lxp)::acc) nctx end in loop args [] ctx in @@ -817,16 +843,43 @@ and lexp_parse_inductive ctors ctx = (* Macro declaration handling, return a list of declarations * to be processed *) -and lexp_expand_macro macro_funct sargs ctx - = lexp_expand_macro_ macro_funct sargs ctx "expand_macro_" +and lexp_expand_macro macro_funct sargs ctx t + = lexp_expand_macro_ macro_funct sargs ctx (Some t) "expand_macro_" and lexp_expand_dmacro macro_funct sargs ctx - = lexp_expand_macro_ macro_funct sargs ctx "expand_dmacro_" - -and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type = + = lexp_expand_macro_ macro_funct sargs ctx None "expand_dmacro_" + +and track_fv meta_ctx rctx lctx e = + let (fvs, mvs) = OL.fv e in + let nc = EV.not_closed rctx fvs in + if nc = [] && not (VMap.is_empty mvs) then + "metavars" + else if nc = [] then + "a bug" + else let rec tfv i = + let name = match Myers.nth i rctx with + | (Some n,_) -> n + | _ -> "<anon>" in + match Myers.nth i lctx with + | (o, _, LetDef e, _) + -> let drop = i + 1 - o in + if drop <= 0 then + "somevars[" ^ string_of_int i ^ "-" ^ string_of_int o ^ "]" + else + name ^ " (" + ^ track_fv meta_ctx + (Myers.nthcdr drop rctx) + (Myers.nthcdr drop lctx) + (L.clean meta_ctx e) + ^ ")" + | _ -> name + in String.concat " " (List.map tfv nc) + +and lexp_expand_macro_ macro_funct sargs ctx ot expand_fun : value_type = (* Build the function to be called *) let macro_expand = BI.get_predef expand_fun ctx in + (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) let args = [(Aexplicit, macro_funct); (Aexplicit, (BI.o2l_list ctx sargs))] in @@ -838,15 +891,9 @@ and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type = let rctx = EV.from_ectx meta_ctx ctx in if not (EV.closed_p rctx (OL.fv macro)) then - (let (fvs, _) = OL.fv macro in - let nc = EV.not_closed rctx fvs in - lexp_error (lexp_location macro_funct) macro_funct + (lexp_error (lexp_location macro_funct) macro_funct ("Macro function is not closed: " - ^ String.concat - " " (List.map (fun i -> match Myers.nth i rctx with - | (Some n,_) -> n - | _ -> "<anon>") - nc))); + ^ track_fv meta_ctx rctx (ectx_to_lctx ctx) macro)); (* eval macro *) let vxp = try EV._eval emacro rctx ([], []) @@ -987,7 +1034,7 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = * Special forms implementation * -------------------------------------------------------------------------- *) -and sform_new_attribute ctx loc sargs = +and sform_new_attribute ctx loc sargs ot = match sargs with | [t] -> let ptp = pexp_parse t in let ltp = infer_type ptp ctx None in @@ -995,12 +1042,13 @@ and sform_new_attribute ctx loc sargs = (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` * is False, for example): Should be a type like `AttributeMap t` * instead. *) - mkBuiltin ((loc, "new-attribute"), - OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp, - Some AttributeMap.empty) + (mkBuiltin ((loc, "new-attribute"), + OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp, + Some AttributeMap.empty), + Lazy) | _ -> fatal loc "new-attribute expects a single Type argument" -and sform_add_attribute ctx loc (sargs : sexp list) = +and sform_add_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, name), idx); attr] -> table, (n - idx, name), attr @@ -1014,7 +1062,8 @@ and sform_add_attribute ctx loc (sargs : sexp list) = (* FIXME: Type check (attr: type == attr_type) *) let attr' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) attr in let table = AttributeMap.add var attr' map in - mkBuiltin ((loc, "add-attribute"), attr_type, Some table) + (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), + Lazy) and get_attribute ctx loc largs = let ctx_n = get_size ctx in @@ -1030,12 +1079,16 @@ and get_attribute ctx loc largs = try Some (AttributeMap.find var map) with Not_found -> None -and sform_get_attribute ctx loc (sargs : sexp list) = +and sform_dummy_ret loc = + let t = newMetatype loc in + (newMetavar loc "special-form-error" t, Inferred t) + +and sform_get_attribute ctx loc (sargs : sexp list) ot = match get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) with - | Some e -> e - | None -> sexp_error loc "No attribute found"; dlxp + | Some e -> (e, Lazy) + | None -> sexp_error loc "No attribute found"; sform_dummy_ret loc -and sform_has_attribute ctx loc (sargs : sexp list) = +and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, name), idx)] -> table, (n - idx, name) @@ -1047,27 +1100,29 @@ and sform_has_attribute ctx loc (sargs : sexp list) = | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in - BI.o2l_bool ctx (AttributeMap.mem var map) + (BI.o2l_bool ctx (AttributeMap.mem var map), Lazy) -and sform_declexpr ctx loc sargs = +and sform_declexpr ctx loc sargs ot = match List.map (lexp_parse_sexp ctx) sargs with | [Var((_, vn), vi)] -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with - | Some lxp -> lxp + | Some lxp -> (lxp, Lazy) | None -> error loc "no expr available"; - dlxp) + sform_dummy_ret loc) | _ -> error loc "declexpr expects one argument"; - dlxp + sform_dummy_ret loc -let sform_decltype ctx loc sargs = +let sform_decltype ctx loc sargs ot = match List.map (lexp_parse_sexp ctx) sargs with | [Var((_, vn), vi)] - -> DB.env_lookup_type ctx ((loc, vn), vi) + -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) | _ -> error loc "decltype expects one argument"; - dlxp + sform_dummy_ret loc -let sform_built_in ctx loc sargs = +let builtin_value_types : ltype option SMap.t ref = ref SMap.empty + +let sform_built_in ctx loc sargs ot = match !_parsing_internals, sargs with | true, [String (_, name); stp] -> let ptp = pexp_parse stp in @@ -1078,25 +1133,25 @@ let sform_built_in ctx loc sargs = if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; - bi + (bi, Inferred ltp') | true, _ -> error loc "Wrong Usage of `Built-in`"; - dlxp + sform_dummy_ret loc | false, _ -> error loc "Use of `Built-in` in user code"; - dlxp + sform_dummy_ret loc -let sform_datacons ctx loc sargs = +let sform_datacons ctx loc sargs ot = match sargs with | [t; Symbol ((sloc, cname) as sym)] -> let pt = pexp_parse t in let idt, _ = infer pt ctx in - mkCons(idt, sym) + (mkCons (idt, sym), Lazy) | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; - dlxp + sform_dummy_ret loc | _ -> sexp_error loc "##constr requires two arguments"; - dlxp + sform_dummy_ret loc (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) @@ -1104,12 +1159,14 @@ let sform_datacons ctx loc sargs = * so it really can only be used applied to something, so it always generates * β-redexes. Furthermore, I'm not sure if my PTS definition is correct to * allow such a lambda. *) -let sform_type ctx loc sargs = +let sform_type ctx loc sargs ot = match sargs with | [l] -> let l = pexp_parse l in let l, _ = infer l ctx in - mkSort (loc, Stype l) - | _ -> sexp_error loc "##Type_ expects one argument"; dlxp + (mkSort (loc, Stype l), + Inferred (mkSort (loc, Stype (SortLevel (SLsucc l))))) + | _ -> sexp_error loc "##Type_ expects one argument"; + sform_dummy_ret loc (* Only print var info *) and lexp_print_var_info ctx = @@ -1197,7 +1254,9 @@ let default_ectx lctx in lctx -let default_rctx = EV.from_ectx VMap.empty default_ectx +let default_rctx = + let meta_ctx, _ = !global_substitution in + EV.from_ectx meta_ctx default_ectx (* String Parsing * --------------------------------------------------------- *) View it on GitLab: https://gitlab.com/monnier/typer/commit/f19ead0d4948a486c60d472393da52895d3…

1 0