Hi guys,
Wondering if you might have an idea:
In Typer, the basic datastructure is the "algebraic datatype" (which
combines a sum, product, and recursion), and the basic eliminator is the
"pattern matching case".
It works OK, but is unsatisfactory:
1- both of those are fairly large/complex.
2- it means that extracting a record field is a "case" operation that
discards all but the required field, so it's an O(n) operation (where
n is the size of the record), if not in the final code, at least in
intermediate code.
3- it means the choice of representation of datatype tags is hardcoded
in the blackbox compiler.
While point n°2 might seem irrelevant, it is a pain with large records,
such as those you might get when records are used to represent modules:
the encoding of the simple "String.concat" reference ends up taking
space proportional to the number of primitives exported from the
"String" module, which can be rather large.
I'd like to find another option and was thinking of something along the
following lines:
- provide a separate product primitive.
- provide a "union" type, i.e. an *untagged* sum.
- provide primitive discrimination operations, such as "dispatch on an Int".
then the Either type could look like
Either a b = union (Singleton(1), a)
(Singleton(2), b)
and
case e
| Left x => ...
| Right y => ...
would turn into
switch (e.0 <withmagicproof>)
| 1 => let e' = cast (Singleton(1), a) e;
x = e'.1
in ...
| 2 => let e' = cast (Singleton(2), b) e;
y = e'.1
in ...
Obviously, we'd still want to have "case", but written as a macro.
The `magicproof` is needed to convince Typer that all union members have
a field 0. And of course, each `cast` would also need to provide
a proof (constructed from a proof provided by `switch`) that indeed we
know that `e` is this specific member of the union.
The way I presented it is fairly general, but pretty heavyweight to
define and to use: every "case" will be compiled to that big
switch-with-proofs and the definition of a "record selection out of
a union" (such as the "e.0 <withmagicproof>") seems fairly complex
as well.
Does anyone here have another approach to suggest?
Stefan
5
7
[Git][monnier/typer][graveline] 4 commits: macro do in pervasive; test for macro do; some change on macro case
by Jonathan Graveline 21 Jul '18
by Jonathan Graveline 21 Jul '18
21 Jul '18
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
abda0e39 by Jonathan Graveline at 2018-06-21T16:28:58Z
macro do in pervasive; test for macro do; some change on macro case
- - - - -
eb8acb50 by Jonathan Graveline at 2018-06-21T16:30:52Z
Merge branch 'graveline' of https://gitlab.com/monnier/typer into graveline
- - - - -
cec64f4a by Jonathan Graveline at 2018-06-21T16:57:44Z
After last merge symbol "_" in macro do need to be declared
- - - - -
a8a77d78 by Jonathan Graveline at 2018-06-22T20:45:23Z
New type Elab_Context and functions Elab_getenv, Elab_isbound, Elab_isconstructor
- - - - -
11 changed files:
- btl/builtins.typer
- btl/pervasive.typer
- samples/case.typer
- samples/do.typer
- src/builtin.ml
- src/debruijn.ml
- src/elab.ml
- src/env.ml
- src/eval.ml
- + tests/elabctx_test.ml
- + tests/macro_do_test.ml
Changes:
=====================================
btl/builtins.typer
=====================================
@@ -242,4 +242,13 @@ Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit;
gensym = Built-in "gensym" : Unit -> IO Sexp;
+%% Function on Elab_Context
+
+Elab_getenv = Built-in "Elab.getenv" : Unit -> IO Elab_Context;
+
+Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> IO Int;
+
+Elab_isconstructor = Built-in "Elab.isconstructor"
+ : String -> Elab_Context -> IO Int;
+
%%% builtins.typer ends here.
=====================================
btl/pervasive.typer
=====================================
@@ -413,4 +413,94 @@ test4 : Option Int;
test4 = test1 : Option ?;
test3 = test4;
+%%%%
+%%%% Macro : do
+%%%%
+
+assign = Sexp_symbol "<-";
+
+get-sym : Sexp -> Sexp;
+get-sym sexp = let
+
+ dflt-sym = (lambda _ -> Sexp_symbol "(_ : IO Unit)");
+
+ in Sexp_dispatch sexp
+
+ ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign)
+ (s)
+ (dflt-sym ())
+ )
+
+ dflt-sym dflt-sym dflt-sym
+ dflt-sym dflt-sym; % there must be a command
+
+get-op : Sexp -> Sexp;
+get-op sexp = let
+
+ as-is = lambda _ -> sexp;
+
+ helper = (lambda sexp -> Sexp_dispatch sexp
+
+ ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign)
+ (Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss)))
+ (Sexp_node s ss)
+ )
+
+ as-is as-is as-is as-is as-is
+ );
+
+ op = (helper sexp);
+
+in if_then_else_ (Sexp_eq op (Sexp_symbol "")) Sexp_error op;
+
+get-decl : List Sexp -> List Sexp;
+get-decl args = let
+
+ err = lambda _ -> cons Sexp_error nil;
+
+ % Expecting a Block of command separated by ";"
+
+ node = Sexp_dispatch (List_nth 0 args Sexp_error)
+
+ (lambda _ _ -> cons Sexp_error nil) err err err err
+
+ (lambda l -> Parser_default l);
+
+in node;
+
+%%
+%% The idea of the macro is :
+%%
+%% IO_bind a-op (lambda a-sym -> [next command or return a-sym])
+%% IO_bind a-op (lambda a-sym -> (IO_bind b-op (lambda b-sym -> [next command or return b-sym])))
+%%
+%% this way a-sym is defined within b-op and so on
+%% a-sym is now just `a` and not `IO a`
+%%
+
+set-fun : List Sexp -> Sexp;
+set-fun args = let
+
+ helper : Sexp -> List Sexp -> Sexp;
+ helper lsym args = case args
+ | cons s ss => (let
+
+ sym = get-sym s;
+
+ op = get-op s;
+
+ in Sexp_node (Sexp_symbol "IO_bind") (cons (op)
+ (cons (Sexp_node (Sexp_symbol "lambda_->_") (cons sym (cons (helper sym ss) nil))) nil))
+ )
+
+ | nil => Sexp_node (Sexp_symbol "IO_return") (cons lsym nil);
+
+in helper (Sexp_symbol "") args; % return Unit if no command given
+
+%% Serie of command
+
+do = macro (lambda args ->
+ (IO_return (set-fun (get-decl args)))
+);
+
%%% pervasive.typer ends here.
=====================================
samples/case.typer
=====================================
@@ -3,17 +3,28 @@
%%%
%%% (pattern matching)
%%%
+%%% This file may not be up to date with version
+%%% in pervasive.typer
+%%%
%%
-%% Match every variable in each pattern.
+%% Match every variable in each pattern with a list of VarTest.
+%%
+%% VarTest :
+%%
+%% var_test is (var_test [ctor to match])
%%
-%% var_test is (var_test ctor)
+%% Push current var n_times for sub test
+%% push_var is (push_var n_times)
%%
-%% Push current var n_times for sub test
-%% push_var is (push_var n_times)
+%% sub_test introduce a variable for testing sub pattern
+%% sub_test is (sub_test [sup. var name] [ctor to match])
%%
-%% sub_test introduce a variable for testing sub pattern
-%% sub_test is (sub_test sup_var ctor)
+%% Pattern :
+%%
+%% branch is (branch [list of var test] [user fun on match])
+%%
+%% dflt_branch is (dflt_branch [user fun]) and always match
%%
type VarTest
@@ -26,24 +37,27 @@ type Pattern
| dflt_branch Sexp;
%%
-%% Get matched variable (e.g. case (var1,var2,...) | ...)
+%% Get matched expression (e.g. case (var1,var2,...) | ...)
+%%
+%% Expression are separated by "," so it is useful for
+%% case (expr1,expr2,...) ...
+%% but also for
+%% case ... | (expr3,expr4,...) => ...
%%
-get_vars : Sexp -> List Sexp;
-get_vars sexp = let
+get_exprs : Sexp -> List Sexp;
+get_exprs sexp = let
err = (lambda _ -> cons Sexp_error nil);
- get_vars_helper : List Sexp -> List Sexp;
- get_vars_helper sexps = case sexps
- | (cons s ss) => (case (Sexp_eq (Sexp_symbol "_,_") s)
- | true => (ss) % tuple
- % constructor or function called (only 1 pattern)
- | false => (cons (Sexp_node s ss) nil))
- | nil => (cons (Sexp_symbol "_") nil);
+ get_exprs_helper : Sexp -> List Sexp -> List Sexp;
+ get_exprs_helper s ss = case (Sexp_eq (Sexp_symbol "_,_") s)
+ | true => (ss) % tuple
+ % constructor or function called (only 1 pattern)
+ | false => (cons (Sexp_node s ss) nil);
in Sexp_dispatch sexp
- (lambda s ss -> (get_vars_helper (cons s ss)))
+ get_exprs_helper
(lambda s -> (cons (Sexp_symbol s) nil))
err err err
(lambda ss -> cons ss nil); % do nothing to Block
@@ -79,7 +93,7 @@ get_cases sexps = let
(lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s)
% expecting a Sexp_node as second argument to _=>_
| true => (branch
- (List_map (lambda ctor -> var_test ctor) (get_vars (List_nth 0 ss Sexp_error)))
+ (List_map (lambda ctor -> var_test ctor) (get_exprs (List_nth 0 ss Sexp_error)))
(List_nth 1 ss Sexp_error))
| false => (dflt_branch (Sexp_node s ss)))
@@ -108,14 +122,15 @@ rename_nth n ctor sym = let
| cons x xs => if_then_else_ (b x)
(cons (f x i) (mapiif f b (i + 1) xs))
(cons x (mapiif f b i xs));
-
- % cons (f x i) (mapiif f b (if_then_else_ (b x) i (i + 1)) xs);
err = (lambda _ -> Sexp_symbol "<not a ctor (0)>");
%%
%% Is argument a variable or a ctor
%%
+ %% (use keyword "ctor" if the ctor has no argument to
+ %% to differentiate with a variable)
+ %%
is_ctor : Sexp -> Bool;
is_ctor v = Sexp_dispatch v
@@ -143,6 +158,7 @@ in IO_return (Sexp_dispatch ctor
%%
%% Expand sub pattern into sub_test
+%% and optionaly push_var when there's
%%
expand_cases : List Pattern -> IO (List Pattern);
@@ -191,6 +207,9 @@ expand_cases pats = let
expand : VarTest -> IO (List VarTest);
expand test = let
+ % I don't expect to use multiple not_unique_sym at the same time
+ % so the name may be reused
+
not_unique_sym : Sexp;
not_unique_sym = Sexp_symbol " %not gensym% ";
@@ -233,7 +252,7 @@ expand_cases pats = let
(IO_bind sub_case (lambda l -> IO_bind all
(lambda all -> IO_return (List_concat all l))))
- in expand test); % (List_concat all (cons test nil));
+ in expand test);
expand_all : Pattern -> IO Pattern;
expand_all p = case p
@@ -273,25 +292,25 @@ pattern_to_sexp vars pats = let
| (cons v _) => push (n - 1) (cons v vars)
| nil => nil);
- chain_ctors_fail : List Sexp -> List VarTest -> Sexp -> Sexp -> Sexp;
- chain_ctors_fail vars tests succ fail = case vars
+ chain_ctors : List Sexp -> List VarTest -> Sexp -> Sexp -> Sexp;
+ chain_ctors vars tests succ fail = case vars
| (cons v vv) => (case tests
| (cons t tt) => (case t
| (var_test t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_"))
- (to_case v t (chain_ctors_fail vv tt succ fail) none)
- (to_case v t (chain_ctors_fail vv tt succ fail) (some fail))
+ (to_case v t (chain_ctors vv tt succ fail) none)
+ (to_case v t (chain_ctors vv tt succ fail) (some fail))
| (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_"))
- (to_case v t (chain_ctors_fail vars tt succ fail) none)
- (to_case v t (chain_ctors_fail vars tt succ fail) (some fail))
- | (push_var n) => (chain_ctors_fail (push n vars) tt succ fail))
+ (to_case v t (chain_ctors vars tt succ fail) none)
+ (to_case v t (chain_ctors vars tt succ fail) (some fail))
+ | (push_var n) => (chain_ctors (push n vars) tt succ fail))
| nil => Sexp_error)
| nil => (case tests
| (cons t tt) => (case t
| (var_test _) => Sexp_error
| (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_"))
- (to_case v t (chain_ctors_fail vars tt succ fail) none)
- (to_case v t (chain_ctors_fail vars tt succ fail) (some fail))
- | (push_var n) => (chain_ctors_fail (push n vars) tt succ fail))
+ (to_case v t (chain_ctors vars tt succ fail) none)
+ (to_case v t (chain_ctors vars tt succ fail) (some fail))
+ | (push_var n) => (chain_ctors (push n vars) tt succ fail))
| nil => succ);
chain_ctors_nofail : List Sexp -> List VarTest -> Sexp -> Sexp;
@@ -315,7 +334,7 @@ pattern_to_sexp vars pats = let
one_to_sexp : List Sexp -> Pattern -> Sexp -> Sexp;
one_to_sexp vars pat fail = case pat
| (dflt_branch f) => f
- | (branch tests f) => (chain_ctors_fail vars tests f fail);
+ | (branch tests f) => (chain_ctors vars tests f fail);
last_to_sexp : List Sexp -> Pattern -> Sexp;
last_to_sexp vars pat = case pat
@@ -330,6 +349,9 @@ pattern_to_sexp vars pats = let
last_test_fun vars pat = (quote (lambda (_ : Unit) ->
(uquote (last_to_sexp vars pat))));
+ % Same thing as not_unique_sym, I can reuse the name because
+ % only the last defined is important
+
fail_sym : Sexp;
fail_sym = Sexp_symbol " %fail sym% ";
@@ -341,8 +363,6 @@ pattern_to_sexp vars pats = let
(cons (Sexp_node (Sexp_symbol "_=_") (cons fail_sym
(cons (helper vars pats) nil))) nil))
(cons (test_fun vars p fail_sym) nil))
- %(quote (let_in_ (_;_ (_=_ (uquote fail_sym) (uquote (helper vars pats))))
- %(uquote (test_fun vars p fail_sym))))
| nil => (last_test_fun vars p))
| nil => Sexp_error;
@@ -359,12 +379,12 @@ case_ = macro (lambda args -> let
| nil => o
| cons x xs => foldi f (i + 1) (f x i o) xs;
- case0_ : List Sexp -> IO Sexp;
- case0_ args = let
+ case0 : List Sexp -> IO Sexp;
+ case0 args = let
vars : List Sexp;
vars = case args
- | (cons s ss) => get_vars s
+ | (cons s ss) => get_exprs s
| nil => nil;
pats : List Pattern;
@@ -385,15 +405,23 @@ case_ = macro (lambda args -> let
rvars = List_reverse vars nil;
nfun : Sexp;
- nfun = (Sexp_node (foldi
- (lambda v i fun -> (quote (lambda_->_
- ((uquote (List_nth i nvars Sexp_error)) : (decltype (uquote v)))
- (uquote fun))))
- 0 fun fvars) (List_reverse fvars nil));
+ nfun = fun;
+
+ %
+ % I was using lambda_->_, then ##case_ needed a type so I added decltype,
+ % then decltype needed variable (rather than composed expression)
+ % so we end up with a let_in_ (thanks to gensym).
+ %
+ % nfun = (Sexp_node (foldi
+ % (lambda v i fun -> (quote (lambda_->_
+ % ((uquote (List_nth i nvars Sexp_error)) : (decltype (uquote v)))
+ % (uquote fun))))
+ % 0 fun fvars) (List_reverse fvars nil));
+ %
in IO_return ( (foldi
(lambda v i fun -> (quote (
- let (uquote (List_nth i fvars Sexp_error)) = (uquote v); in (uquote fun))))
+ let (uquote (List_nth i nvars Sexp_error)) = (uquote v); in (uquote fun))))
0 nfun vars));
% in IO_return nfun;
@@ -405,18 +433,15 @@ case_ = macro (lambda args -> let
% Only the Sexp after "_|_" are interesting
- case1_ : List Sexp -> IO Sexp;
- case1_ args = case args
- | (cons s ss) => if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s)
- (case0_ ss)
- (IO_return Sexp_error)
- | nil => IO_return Sexp_error;
+ case1 : Sexp -> List Sexp -> IO Sexp;
+ case1 s ss = if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s)
+ (case0 ss)
+ (IO_return Sexp_error);
err = (lambda _ -> IO_return Sexp_error);
% Expecting only one Sexp_node containing a case with arguments
in (Sexp_dispatch (List_nth 0 args Sexp_error)
- (lambda s ss -> (case1_ (cons s ss)))
- err err err err err)
+ case1 err err err err err)
);
=====================================
samples/do.typer
=====================================
@@ -1,11 +1,14 @@
%%%
-%%% Macro : action
+%%% Macro : do
+%%%
+%%% This file may not be up to date with version
+%%% in pervasive.typer
%%%
%%
%% Here's an example :
%%
-%% fun = action {
+%% fun = do {
%% str <- return "\n\tHello world!\n\n";
%% print str;
%% };
@@ -14,7 +17,7 @@
%%
%% fun is a command,
%%
-%% action may contain action because it returns a command.
+%% do may contain do because it returns a command.
%%
assign = Sexp_symbol "<-";
@@ -22,7 +25,7 @@ assign = Sexp_symbol "<-";
get-sym : Sexp -> Sexp;
get-sym sexp = let
- dflt-sym = (lambda _ -> Sexp_symbol "_");
+ dflt-sym = (lambda _ -> Sexp_symbol "(_ : IO Unit)");
in Sexp_dispatch sexp
@@ -99,7 +102,7 @@ in helper (Sexp_symbol "") args; % return Unit if no command given
%% Serie of command
-action = macro (lambda args ->
+do = macro (lambda args ->
(IO_return (set-fun (get-decl args)))
);
@@ -116,13 +119,13 @@ tab = print "\t";
float2string v = IO_return (Float->String v);
%%
-%% example0 = action {
+%% example0 = do {
%% str <- return "\n\tHello world!";
%% print str;
%% return 0.0;
%% };
%%
-%% example1 = action {
+%% example1 = do {
%% flt <- example0;
%% str <- float2string flt;
%% newline;
=====================================
src/builtin.ml
=====================================
@@ -158,7 +158,8 @@ let register_builtin_csts () =
add_builtin_cst "Int" DB.type_int;
add_builtin_cst "Integer" DB.type_integer;
add_builtin_cst "Float" DB.type_float;
- add_builtin_cst "String" DB.type_string
+ add_builtin_cst "String" DB.type_string;
+ add_builtin_cst "Elab_Context" DB.type_elabctx
let register_builtin_types () =
let _ = new_builtin_type "Sexp" DB.type0 in
=====================================
src/debruijn.ml
=====================================
@@ -92,6 +92,7 @@ let type_int = mkBuiltin ((dloc, "Int"), type0, None)
let type_integer = mkBuiltin ((dloc, "Integer"), type0, None)
let type_float = mkBuiltin ((dloc, "Float"), type0, None)
let type_string = mkBuiltin ((dloc, "String"), type0, None)
+let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None)
(* easier to debug with type annotations *)
type env_elem = (vname * varbind * ltype)
@@ -311,13 +312,31 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =
^ string_of_int dbi ^ " of `" ^ maybename oename
^ "` out of bounds!")
-
+let lctx_olookup (ctx : lexp_context) (var : string) : (int * env_elem) option =
+ let rec _lctx_olookup ctx var idx =
+ try (let elem = M.car ctx in match elem with
+ | ((_,Some name),_,_) as elem -> (if (name = var)
+ then (Some (idx,elem))
+ else _lctx_olookup (M.cdr ctx) var (idx + 1))
+ | _ -> error dloc ("error in lctx_olookup"))
+ with Not_found -> None
+ in (_lctx_olookup ctx var 0)
let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp =
let (_, i) = vref in
let (_, _, t) = lctx_lookup ctx vref in
mkSusp t (S.shift (i + 1))
+let lctx_olookup_type (ctx : lexp_context) (var : string) : lexp option =
+ let oelem = lctx_olookup ctx var in match oelem with
+ | Some (i,(_, _, t)) -> Some (mkSusp t (S.shift (i + 1)))
+ | None -> None
+
+let lctx_olookup_value (ctx : lexp_context) (var : string) : lexp option =
+ let oelem = lctx_olookup ctx var in match oelem with
+ | Some (i,(_, LetDef (o, v), _)) -> Some (push_susp v (S.shift (i + 1)))
+ | None -> None
+
let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option =
let (_, i) = vref in
match lctx_lookup ctx vref with
@@ -353,7 +372,6 @@ let rec lctx_view lctx =
| Myers.Mcons ((loname, odef, t), lctx, _, _)
-> CVlet (loname, odef, t, lctx)
-
(** Sets of DeBruijn indices **)
type set = db_offset * unit IMap.t
=====================================
src/elab.ml
=====================================
@@ -999,6 +999,7 @@ and lexp_decls_1
(pending_defs : (symbol * sexp) list) (* Pending definitions. *)
: (vname * lexp * ltype) list * sexp list * elab_context =
+ let rec _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs =
match sdecls with
| [] -> (if not (SMap.is_empty pending_decls) then
let (s, l) = SMap.choose pending_decls in
@@ -1008,10 +1009,10 @@ and lexp_decls_1
[], [], nctx
| Symbol (_, "") :: sdecls
- -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
+ -> _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
| Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls
- -> lexp_decls_1 (List.append sdecls' sdecls)
+ -> _lexp_decls_1 (List.append sdecls' sdecls)
ectx nctx pending_decls pending_defs
| Node (Symbol (l, "_:_"), args) :: sdecls
@@ -1034,17 +1035,17 @@ and lexp_decls_1
^ lexp_string ltp ^ "` incompatible with previous `"
^ lexp_string pt ^ "`")
| Some [] -> () in
- lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
+ _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
else if List.exists (fun ((_, vname'), _) -> vname = vname')
pending_defs then
(error l ("Variable `" ^ vname ^ "` already defined!");
- lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
- else lexp_decls_1 sdecls ectx
+ _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
+ else _lexp_decls_1 sdecls ectx
(ectx_extend nctx (l, Some vname) ForwardRef ltp)
(SMap.add vname l pending_decls)
pending_defs
| _ -> error l "Invalid type declaration syntax";
- lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
+ _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
| Node (Symbol (l, "_=_") as head, args) :: sdecls
(* FIXME: Move this to a "special form"! *)
@@ -1070,15 +1071,15 @@ and lexp_decls_1
let decls, nctx = lexp_check_decls ectx nctx pending_defs in
decls, sdecls, nctx
else
- lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
+ _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
else
(error l ("`" ^ vname ^ "` defined but not declared!");
- lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
+ _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
| [Node (Symbol s, args) as d; body]
-> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *)
- lexp_decls_1 ((Node (head,
+ _lexp_decls_1 ((Node (head,
[Symbol s;
Node (Symbol (sexp_location d, "lambda_->_"),
[sexp_u_list args; body])]))
@@ -1086,22 +1087,25 @@ and lexp_decls_1
ectx nctx pending_decls pending_defs
| _ -> error l "Invalid definition syntax";
- lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
+ _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
| Node (Symbol (l, "define-operator"), args) :: sdecls
(* FIXME: Move this to a "special form"! *)
- -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None)
+ -> _lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None)
pending_decls pending_defs
| Node (Symbol ((l, _) as v), sargs) :: sdecls
-> (* expand macro and get the generated declarations *)
let sdecl' = lexp_decls_macro v sargs nctx in
- lexp_decls_1 (sdecl' :: sdecls) ectx nctx
+ _lexp_decls_1 (sdecl' :: sdecls) ectx nctx
pending_decls pending_defs
| sexp :: sdecls
-> error (sexp_location sexp) "Invalid declaration syntax";
- lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
+ _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
+
+ in (EV.set_getenv nctx;
+ _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
and lexp_p_decls (sdecls : sexp list) (ctx : elab_context)
: ((vname * lexp * ltype) list list * elab_context) =
=====================================
src/env.ml
=====================================
@@ -39,6 +39,7 @@ open Elexp
module M = Myers
module L = Lexp
module BI = Big_int
+module DB = Debruijn
let dloc = dummy_location
@@ -63,6 +64,7 @@ type value_type =
| Vout of out_channel
| Vcommand of (unit -> value_type)
| Vref of (value_type ref)
+ | Velabctx of DB.elab_context
(* Runtime Environ *)
and runtime_env = (vname * (value_type ref)) M.myers
@@ -93,6 +95,8 @@ let rec value_equal a b =
| Vref (v1), Vref (v2) -> value_equal (!v1) (!v2)
+ | Velabctx (e1), Velabctx (e2) -> (e1 = e2)
+
| _ -> false
let rec value_eq_list a b =
@@ -124,6 +128,7 @@ let rec value_name v =
| Vbuiltin _ -> "Vbuiltin"
| Vcommand _ -> "Vcommand"
| Vref v -> ("Vref of "^(value_name (!v)))
+ | Velabctx _ -> ("Velabctx")
let rec value_string v =
match v with
@@ -145,6 +150,7 @@ let rec value_string v =
"" lst in
"(" ^ s ^ args ^ ")"
| Vref (v) -> ("Ref of "^(value_string (!v)))
+ | Velabctx _ -> ("Velabctx")
let value_print (vtp: value_type) = print_string (value_string vtp)
=====================================
src/eval.ml
=====================================
@@ -723,6 +723,33 @@ let gensym = let count = ref 0 in
Vsexp (Symbol (dloc,(" %gensym% no "^(string_of_int (!count))^" ")))))
| _ -> error loc "gensym takes a Unit as argument")
+(* I'm using a ref because I think register_builtin_functions
+ get called after the default_ctx is created in elab.
+ Another solution could be to define a function in elaboration step
+ and then undefine it. The thing is elab_context may not exist at runtime
+ so I must save it somewhere if the Elab.* function persist. *)
+let _last_elab_context = ref empty_elab_context
+
+let getenv loc depth args_val = match args_val with
+ | [v] -> Vcommand (fun () -> Velabctx !_last_elab_context)
+ | _ -> error loc "getenv takes a single Unit as argument"
+
+let set_getenv (ectx : elab_context) = _last_elab_context := ectx
+
+let is_bound loc depth args_val = match args_val with
+ | [Vstring name; Velabctx ectx] -> Vcommand (fun () ->
+ let t = lctx_olookup (ectx_to_lctx ectx) name in match t with
+ | Some _ -> (Vint 1)
+ | _ -> (Vint 0) )
+ | _ -> error loc "Elab.isbound takes an Elab_Context and a String as arguments"
+
+let is_constructor loc depth args_val = match args_val with
+ | [Vstring name; Velabctx ectx] -> Vcommand (fun () ->
+ let t = lctx_olookup_value (ectx_to_lctx ectx) name in match t with
+ | Some (Cons _) -> (Vint 1)
+ | _ -> (Vint 0) )
+ | _ -> error loc "Elab.isconstructor takes an Elab_Context and a String as arguments"
+
let register_builtin_functions () =
List.iter (fun (name, f, arity) -> add_builtin_function name f arity)
[
@@ -755,6 +782,9 @@ let register_builtin_functions () =
("Ref.read" , ref_read, 1);
("Ref.write" , ref_write, 2);
("gensym" , gensym, 1);
+ ("Elab.getenv" , getenv, 1);
+ ("Elab.isbound" , is_bound, 2);
+ ("Elab.isconstructor", is_constructor, 2);
]
let _ = register_builtin_functions ()
=====================================
tests/elabctx_test.ml
=====================================
@@ -0,0 +1,216 @@
+
+open Util
+open Utest_lib
+
+open Sexp
+open Lexp
+
+open Eval (* reset_eval_trace *)
+
+open Builtin
+open Env
+
+(* default environment *)
+let ectx = Elab.default_ectx
+let rctx = Elab.default_rctx
+
+
+let _ = (add_test "ELABCTX" "Elab_getenv" (fun () ->
+ let dcode = "
+ return = IO_return;
+
+ nop = (lambda _ -> return ());
+
+ action = do
+ {
+ env <- (Elab_getenv ());
+
+ return env;
+ };" in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "action;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vcommand cmd] -> ( match (cmd ()) with
+ | (Velabctx _) -> success ()
+ | _ -> failure () )
+ | _ -> failure ())
+)
+
+let _ = (add_test "ELABCTX" "Elab_isbound" (fun () ->
+ let dcode = "
+ return = IO_return;
+
+ nop = (lambda _ -> return ());
+
+ a = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isbound \"Int\" env);
+
+ return b;
+ };
+
+ b = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isbound \"List\" env);
+
+ return b;
+ };
+
+ c = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isbound \"Elab_isbound\" env);
+
+ return b;
+ };
+
+ d = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isbound \"do\" env);
+
+ return b;
+ };
+
+ e = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isbound \"randomunusednameabc123\" env);
+
+ return b;
+ };" in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "a; b; c; d; e;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vcommand a; Vcommand b; Vcommand c;
+ Vcommand d; Vcommand e] ->
+ ( match (a (), b (), c (), d (), e ()) with
+ | (Vint 1, Vint 1, Vint 1, Vint 1, Vint 0) -> success ()
+ | _ -> failure () )
+ | _ -> failure ())
+)
+
+let _ = (add_test "ELABCTX" "Elab_isconstructor" (fun () ->
+ let dcode = "
+ return = IO_return;
+
+ nop = (lambda _ -> return ());
+
+ af = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"Int\" env);
+
+ return b;
+ };
+
+ bf = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"List\" env);
+
+ return b;
+ };
+
+ cf = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"Elab_isbound\" env);
+
+ return b;
+ };
+
+ df = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"do\" env);
+
+ return b;
+ };
+
+ ef = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"randomunusednameabc123\" env);
+
+ return b;
+ };
+
+ at = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"cons\" env);
+
+ return b;
+ };
+
+ bt = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"nil\" env);
+
+ return b;
+ };
+
+ ct = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"true\" env);
+
+ return b;
+ };
+
+ dt = do
+ {
+ env <- (Elab_getenv ());
+
+ b <- (Elab_isconstructor \"false\" env);
+
+ return b;
+ };" in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "af; bf; cf; df; ef; at; bt; ct; dt;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vcommand af; Vcommand bf; Vcommand cf; Vcommand df; Vcommand ef;
+ Vcommand at; Vcommand bt; Vcommand ct; Vcommand dt] ->
+ ( match (af (), bf (), cf (), df (), ef (),
+ at (), bt (), ct (), dt ()) with
+ | (Vint 0, Vint 0, Vint 0, Vint 0, Vint 0,
+ Vint 1, Vint 1, Vint 1, Vint 1) -> success ()
+ | _ -> failure () )
+ | _ -> failure ())
+)
+
+
+(* run all tests *)
+let _ = run_all ()
=====================================
tests/macro_do_test.ml
=====================================
@@ -0,0 +1,118 @@
+
+open Util
+open Utest_lib
+
+open Sexp
+open Lexp
+
+open Eval (* reset_eval_trace *)
+
+open Builtin
+open Env
+
+(* default environment *)
+let ectx = Elab.default_ectx
+let rctx = Elab.default_rctx
+
+(* all tests use binded variable *)
+(* I'm saying it in case everythings break *)
+
+(* there's a problem with string inside string when I use new line ("\n") *)
+
+(* mostly to check if no exception are thrown *)
+let _ = (add_test "DO MACROS" "Hello, world!" (fun () ->
+ let dcode = "
+ return = IO_return;
+
+ nop = (lambda _ -> return ());
+
+ action = do
+ {
+ str <- return \"Hello, world!\";
+
+ nop str;
+ };" in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "action;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vcommand _] -> success ()
+ | _ -> failure ())
+)
+
+(* check return value from do macro *)
+let _ = (add_test "DO MACROS" "return value" (fun () ->
+ let dcode = "
+ return = IO_return;
+
+ nop = (lambda _ -> return ());
+
+ action = do
+ {
+ nop \"Doing random stuff before returning...\";
+
+ n <- return 123456789;
+
+ return n;
+ };" in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "action;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vcommand cmd] -> ( match (cmd ()) with
+ | Vint v ->
+ if (123456789 = v) then success () else failure ()
+ | _ -> failure() )
+
+ | _ -> failure ())
+)
+
+(* check if any problem when using do as command inside another do *)
+let _ = (add_test "DO MACROS" "do inside do" (fun () ->
+ let dcode = "
+ return = IO_return;
+
+ nop = (lambda _ -> return ());
+
+ action0 = do { return 123; };
+
+ action1 = do
+ {
+ x <- do { return (Float_+ 16.0 0.125); };
+
+ nop \"Doing random stuff...\";
+
+ str <- return (Float->String x);
+
+ val123 <- action0;
+
+ do { nop str; };
+
+ do { do { nop str; }; };
+
+ return str;
+ };" in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "action1;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vcommand cmd] -> ( match (cmd ()) with
+ | Vstring str -> if ("16.125" = str) then success () else failure ()
+ | _ -> failure () )
+ | _ -> failure ())
+)
+
+(* run all tests *)
+let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/compare/203222b1a7159cb62e213b5625323f286a…
--
View it on GitLab: https://gitlab.com/monnier/typer/compare/203222b1a7159cb62e213b5625323f286a…
You're receiving this email because of your account on gitlab.com.
3
2
[Git][monnier/typer][graveline] samples/list_n.typer, there must be some mistakes
by Jonathan Graveline 03 Jul '18
by Jonathan Graveline 03 Jul '18
03 Jul '18
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
46381fd8 by Jonathan Graveline at 2018-06-25T18:11:36Z
samples/list_n.typer, there must be some mistakes
- - - - -
1 changed file:
- + samples/list_n.typer
Changes:
=====================================
samples/list_n.typer
=====================================
@@ -0,0 +1,37 @@
+%%%
+%%% Size proved list : n_list
+%%%
+
+Nat : Type;
+
+type Nat
+ | zero
+ | succ Nat;
+
+Nat_add : Nat -> Nat -> Nat;
+
+Nat_add n k = case n
+ | (succ n) => Nat_add n (succ k)
+ | zero => k;
+
+Nat_eq : Nat -> Nat -> Type;
+Nat_eq n k = case (n,k)
+ | (succ n,succ k) => Nat_eq n k
+ | (zero,zero) => True
+ | False;
+
+one = succ zero;
+
+List_n : Nat -> Type -> Type;
+
+type List_n (n : Nat) (a : Type)
+ | cons a (List_n sn a) (p ::: (Nat_eq n (succ sn)))
+ | nil (p ::: (Nat_eq n zero));
+
+len : (n : Nat) ≡> (a : Type) ≡> List_n n a -> Nat;
+len xs = case (xs)
+ | cons x xs => succ (len xs)
+ | nil => zero;
+
+%prep : (n : Nat) ≡> a -> List_n n a -> List_n (succ n) a;
+%prep x xs = cons (n := (succ n)) x xs (Nat_eq (succ n) (succ n));
View it on GitLab: https://gitlab.com/monnier/typer/commit/46381fd83e2e2651d52d0aa645712b57a0c…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/46381fd83e2e2651d52d0aa645712b57a0c…
You're receiving this email because of your account on gitlab.com.
2
1
[Git][monnier/typer][graveline] Correction of Array functions and simplification
by Jonathan Graveline 29 Jui '18
by Jonathan Graveline 29 Jui '18
29 Jui '18
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
af4ba9f6 by Jonathan Graveline at 2018-06-29T20:41:33Z
Correction of Array functions and simplification
- - - - -
3 changed files:
- btl/builtins.typer
- src/eval.ml
- tests/array_test.ml
Changes:
=====================================
btl/builtins.typer
=====================================
--- a/btl/builtins.typer
+++ b/btl/builtins.typer
@@ -206,7 +206,7 @@ Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a
Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a;
Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int;
Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a;
-Array_get = Built-in "Array.get" : (a : Type) ≡> Int -> Array a -> a;
+Array_get = Built-in "Array.get" : (a : Type) ≡> a -> Int -> Array a -> a;
% let Typer deduce the value of (a : Type)
Array_empty = Built-in "Array.empty" : (a : Type) ≡> Unit -> Array a;
=====================================
src/eval.ml
=====================================
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -751,11 +751,8 @@ let is_constructor loc depth args_val = match args_val with
| _ -> error loc "Elab.isconstructor takes an Elab_Context and a String as arguments"
let array_append loc depth args_val = match args_val with
- | [v; Varray a] -> if (a = (Array.make 0 Vundefined)) then
- let a = (Array.make 0 v) in
- Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v))
- else
- Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v))
+ | [v; Varray a] ->
+ Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v))
| _ -> error loc "Array.append takes a value followed by an Array as arguments"
let array_create loc depth args_val = match args_val with
@@ -763,34 +760,31 @@ let array_create loc depth args_val = match args_val with
| _ -> error loc "Array.make takes an Int and a value and as arguemnts"
let array_length loc depth args_val = match args_val with
- | [Varray a] -> if (a = (Array.make 0 Vundefined))
- then
- (Vint 0)
- else
- Vint (Array.length a)
+ | [Varray a] -> Vint (Array.length a)
| _ -> error loc "Array.length takes an Array as argument"
let array_set loc depth args_val = match args_val with
- | [Vint idx; v; Varray a] -> if (a = (Array.make 0 Vundefined))
+ | [Vint idx; v; Varray a] -> if (idx > (Array.length a) || idx < 0)
then
- let a = (Array.make 0 v) in
- let copy = (Array.map (fun v -> v) a) in
- (Array.set copy idx v; Varray copy)
+ (warning loc "Array.set index out of bounds (array unchanged)";
+ (Varray a))
else
let copy = (Array.map (fun v -> v) a) in
(Array.set copy idx v; Varray copy)
| _ -> error loc "Array.set takes an Int, a value and an Array as arguments"
let array_get loc depth args_val = match args_val with
- | [Vint idx; Varray a] -> if (a = (Array.make 0 Vundefined))
- || (idx > (Array.length a))
- || (idx < 0)
+ | [dflt; Vint idx; Varray a] -> if (idx > (Array.length a)) || (idx < 0)
then
- error loc "Array.get index out of bounds"
+ dflt
else
Array.get a idx
- | _ -> error loc "Array.get takes an Int followed by an Array as arguments"
+ | _ -> error loc "Array.get takes a default value, an Int and an Array as arguments"
+
+(* Vundefined is used in array_empty because we have no default value
+ ("array_create 0 0" has a default value v (Vint 0)).
+*)
let array_empty loc depth args_val = match args_val with
| [_] -> Varray (Array.make 0 Vundefined)
| _ -> error loc "Array.empty takes a Unit as single argument"
@@ -834,7 +828,7 @@ let register_builtin_functions () =
("Array.create" , array_create,2);
("Array.length" , array_length,1);
("Array.set" , array_set,3);
- ("Array.get" , array_get,2);
+ ("Array.get" , array_get,3);
("Array.empty" , array_empty,1);
]
let _ = register_builtin_functions ()
=====================================
tests/array_test.ml
=====================================
--- a/tests/array_test.ml
+++ b/tests/array_test.ml
@@ -100,18 +100,21 @@ let _ = (add_test "ARRAY" "Array.set" (fun () ->
a = Array_create 101 0;
b = Array_set 57 1 a;
+
+ % should throw a warning (out of bounds)
+ c = Array_set 102 1 a;
" in
let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
- let ecode = "a; b;" in
+ let ecode = "a; b; c;" in
let ret = Elab.eval_expr_str ecode ectx rctx in
match ret with
- | [Varray a; Varray b] -> let
+ | [Varray a; Varray b; Varray c] -> let
aa = Array.make 101 (Vint 0)
- in if (a = aa) && (Array.set aa 57 (Vint 1); b = aa)
+ in if (a = aa) && (Array.set aa 57 (Vint 1); b = aa) && (a = c)
then success ()
else failure ()
| _ -> failure ())
@@ -121,18 +124,24 @@ let _ = (add_test "ARRAY" "Array.get" (fun () ->
let dcode = "
a = Array_create 101 0;
- b = Array_set 57 1 a;
+ aa = Array_set 57 1 a;
+
+ b = Array_get (-1) 57 aa;
+
+ c = Array_get (-1) 102 aa;
+
+ d = Array_get (-1) 0 aa;
" in
let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
- let ecode = "b;" in
+ let ecode = "b; c; d;" in
let ret = Elab.eval_expr_str ecode ectx rctx in
match ret with
- | [Varray b] ->
- if ((Array.get b 57) = (Vint 1)) && ((Array.get b 58) = (Vint 0))
+ | [Vint b; Vint c; Vint d] ->
+ if (b = 1 && c = (-1) && d = 0)
then success ()
else failure ()
| _ -> failure ())
View it on GitLab: https://gitlab.com/monnier/typer/commit/af4ba9f65f311ad34cd34faa513231abe25…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/af4ba9f65f311ad34cd34faa513231abe25…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][graveline] New type and value for Array with some functions
by Jonathan Graveline 29 Jui '18
by Jonathan Graveline 29 Jui '18
29 Jui '18
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
4c682c42 by Jonathan Graveline at 2018-06-28T21:57:57Z
New type and value for Array with some functions
- - - - -
6 changed files:
- btl/builtins.typer
- btl/pervasive.typer
- src/builtin.ml
- src/env.ml
- src/eval.ml
- + tests/array_test.ml
Changes:
=====================================
btl/builtins.typer
=====================================
--- a/btl/builtins.typer
+++ b/btl/builtins.typer
@@ -200,6 +200,17 @@ Sexp_dispatch = Built-in "Sexp.dispatch"
Parser_default = Built-in "Parser.default" : Sexp -> List Sexp;
+%%%% Array (without IO, but they could be added easily)
+
+Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a;
+Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a;
+Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int;
+Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a;
+Array_get = Built-in "Array.get" : (a : Type) ≡> Int -> Array a -> a;
+
+% let Typer deduce the value of (a : Type)
+Array_empty = Built-in "Array.empty" : (a : Type) ≡> Unit -> Array a;
+
%%%% Monads
%% Builtin bind
=====================================
btl/pervasive.typer
=====================================
--- a/btl/pervasive.typer
+++ b/btl/pervasive.typer
@@ -416,9 +416,6 @@ test3 = test4;
%%%%
%%%% Macro : do
%%%%
-%%%% This file may not be up to date with version
-%%%% in pervasive.typer
-%%%%
%%
%% Here's an example :
@@ -521,4 +518,18 @@ do = macro (lambda args ->
(IO_return (set-fun (get-decl args)))
);
+%%%%
+%%%% Array from List
+%%%%
+
+List->Array : (a : Type) ≡> List a -> Array a;
+List->Array xs = let
+
+ helper : List a -> Array a -> Array a;
+ helper xs a = case xs
+ | cons x xs => helper xs (Array_append x a)
+ | nil => a;
+
+in (helper xs (Array_empty ()));
+
%%% pervasive.typer ends here.
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -169,6 +169,9 @@ let register_builtin_types () =
let _ = new_builtin_type
"Ref" (mkArrow (Aexplicit, (dloc, None),
DB.type0, dloc, DB.type0)) in
+ let _ = new_builtin_type
+ "Array" (mkArrow (Aexplicit, (dloc, None),
+ DB.type0, dloc, DB.type0)) in
let _ = new_builtin_type "FileHandle" DB.type0 in
let _ = new_builtin_type "Eq" type_eq in
()
=====================================
src/env.ml
=====================================
--- a/src/env.ml
+++ b/src/env.ml
@@ -65,6 +65,7 @@ type value_type =
| Vcommand of (unit -> value_type)
| Vref of (value_type ref)
| Velabctx of DB.elab_context
+ | Varray of (value_type array)
(* Runtime Environ *)
and runtime_env = (vname * (value_type ref)) M.myers
@@ -97,6 +98,8 @@ let rec value_equal a b =
| Velabctx (e1), Velabctx (e2) -> (e1 = e2)
+ | Varray (a1), Varray (a2) -> (a1 = a2)
+
| _ -> false
let rec value_eq_list a b =
@@ -129,6 +132,7 @@ let rec value_name v =
| Vcommand _ -> "Vcommand"
| Vref v -> ("Vref of "^(value_name (!v)))
| Velabctx _ -> ("Velabctx")
+ | Varray _ -> ("Varray")
let rec value_string v =
match v with
@@ -151,6 +155,12 @@ let rec value_string v =
"(" ^ s ^ args ^ ")"
| Vref (v) -> ("Ref of "^(value_string (!v)))
| Velabctx _ -> ("Velabctx")
+ | Varray a -> if ( (Array.length a) = 0 )
+ then "[]"
+ else ( let
+ str = (Array.fold_left
+ (fun str v -> (str^(value_string v)^";")) "" a)
+ in ("["^(String.sub str 0 ((String.length str) - 1))^"]") )
let value_print (vtp: value_type) = print_string (value_string vtp)
=====================================
src/eval.ml
=====================================
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -750,6 +750,51 @@ let is_constructor loc depth args_val = match args_val with
| _ -> (Vint 0) )
| _ -> error loc "Elab.isconstructor takes an Elab_Context and a String as arguments"
+let array_append loc depth args_val = match args_val with
+ | [v; Varray a] -> if (a = (Array.make 0 Vundefined)) then
+ let a = (Array.make 0 v) in
+ Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v))
+ else
+ Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v))
+ | _ -> error loc "Array.append takes a value followed by an Array as arguments"
+
+let array_create loc depth args_val = match args_val with
+ | [Vint len; v] -> Varray (Array.make len v)
+ | _ -> error loc "Array.make takes an Int and a value and as arguemnts"
+
+let array_length loc depth args_val = match args_val with
+ | [Varray a] -> if (a = (Array.make 0 Vundefined))
+ then
+ (Vint 0)
+ else
+ Vint (Array.length a)
+ | _ -> error loc "Array.length takes an Array as argument"
+
+let array_set loc depth args_val = match args_val with
+ | [Vint idx; v; Varray a] -> if (a = (Array.make 0 Vundefined))
+ then
+ let a = (Array.make 0 v) in
+ let copy = (Array.map (fun v -> v) a) in
+ (Array.set copy idx v; Varray copy)
+ else
+ let copy = (Array.map (fun v -> v) a) in
+ (Array.set copy idx v; Varray copy)
+ | _ -> error loc "Array.set takes an Int, a value and an Array as arguments"
+
+let array_get loc depth args_val = match args_val with
+ | [Vint idx; Varray a] -> if (a = (Array.make 0 Vundefined))
+ || (idx > (Array.length a))
+ || (idx < 0)
+ then
+ error loc "Array.get index out of bounds"
+ else
+ Array.get a idx
+ | _ -> error loc "Array.get takes an Int followed by an Array as arguments"
+
+let array_empty loc depth args_val = match args_val with
+ | [_] -> Varray (Array.make 0 Vundefined)
+ | _ -> error loc "Array.empty takes a Unit as single argument"
+
let register_builtin_functions () =
List.iter (fun (name, f, arity) -> add_builtin_function name f arity)
[
@@ -783,8 +828,14 @@ let register_builtin_functions () =
("Ref.write" , ref_write, 2);
("gensym" , gensym, 1);
("Elab.getenv" , getenv, 1);
- ("Elab.isbound" , is_bound, 2);
+ ("Elab.isbound" , is_bound, 2);
("Elab.isconstructor", is_constructor, 2);
+ ("Array.append" , array_append,2);
+ ("Array.create" , array_create,2);
+ ("Array.length" , array_length,1);
+ ("Array.set" , array_set,3);
+ ("Array.get" , array_get,2);
+ ("Array.empty" , array_empty,1);
]
let _ = register_builtin_functions ()
=====================================
tests/array_test.ml
=====================================
--- /dev/null
+++ b/tests/array_test.ml
@@ -0,0 +1,176 @@
+
+open Util
+open Utest_lib
+
+open Sexp
+open Lexp
+
+open Eval (* reset_eval_trace *)
+
+open Builtin
+open Env
+
+(* default environment *)
+let ectx = Elab.default_ectx
+let rctx = Elab.default_rctx
+
+
+let _ = (add_test "ARRAY" "Array.create" (fun () ->
+ let dcode = "
+ % value_string should also be tested (it is used in interpreter)
+
+ empty = Array_create 0 0;
+
+ a = Array_create 1 1;
+
+ b = Array_create 10 1;
+ " in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "empty; a; b;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ (* should I use value_equal here? *)
+ match ret with
+ | [Varray empty; Varray a; Varray b] ->
+ if (empty = (Array.make 0 (Vint 0)))
+ && (a = (Array.make 1 (Vint 1)))
+ && (b = (Array.make 10 (Vint 1)))
+ then success ()
+ else failure ()
+ | _ -> failure ())
+)
+
+let _ = (add_test "ARRAY" "Array.append" (fun () ->
+ let dcode = "
+ empty = Array_create 0 0;
+
+ a = Array_append 1 empty;
+
+ b = Array_create 1 1;
+
+ c = Array_append 2 b;
+ " in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "a; c;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Varray a; Varray c] ->
+ if (a = (Array.make 1 (Vint 1)))
+ && (c =
+ (Array.append (Array.make 1 (Vint 1)) (Array.make 1 (Vint 2))))
+ then success ()
+ else failure ()
+ | _ -> failure ())
+)
+
+let _ = (add_test "ARRAY" "Array.length" (fun () ->
+ let dcode = "
+ empty = Array_create 0 0;
+
+ a = Array_create 101 0;
+
+ lempty = Array_length empty;
+
+ la = Array_length a;
+ " in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "lempty; la;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vint empty; Vint a] ->
+ if (empty = 0) && (a = 101)
+ then success ()
+ else failure ()
+ | _ -> failure ())
+)
+
+let _ = (add_test "ARRAY" "Array.set" (fun () ->
+ let dcode = "
+ a = Array_create 101 0;
+
+ b = Array_set 57 1 a;
+ " in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "a; b;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Varray a; Varray b] -> let
+ aa = Array.make 101 (Vint 0)
+ in if (a = aa) && (Array.set aa 57 (Vint 1); b = aa)
+ then success ()
+ else failure ()
+ | _ -> failure ())
+)
+
+let _ = (add_test "ARRAY" "Array.get" (fun () ->
+ let dcode = "
+ a = Array_create 101 0;
+
+ b = Array_set 57 1 a;
+ " in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "b;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Varray b] ->
+ if ((Array.get b 57) = (Vint 1)) && ((Array.get b 58) = (Vint 0))
+ then success ()
+ else failure ()
+ | _ -> failure ())
+)
+
+let _ = (add_test "ARRAY" "Array.empty, List->Array" (fun () ->
+ let dcode = "
+ empty1 = Array_empty ();
+
+ empty2 = List->Array nil;
+
+ a = List->Array (cons \"a\" (cons \"b\" (cons \"c\" nil)));
+
+ b = List->Array (cons 1 (cons 2 (cons 3 nil)));
+ " in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "empty1; empty2; a; b;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Varray empty1; Varray empty2; Varray a; Varray b] ->
+ if empty1 = empty2
+ && (Array.length empty1) = 0
+ && (Array.length empty2) = 0
+ && (Array.get a 0) = (Vstring "a")
+ && (Array.get a 1) = (Vstring "b")
+ && (Array.get a 2) = (Vstring "c")
+ && (Array.get b 0) = (Vint 1)
+ && (Array.get b 1) = (Vint 2)
+ && (Array.get b 2) = (Vint 3)
+ then success ()
+ else failure ()
+ | _ -> failure ())
+)
+
+
+(* run all tests *)
+let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/commit/4c682c4255948c4b00c5e81e2fc77296839…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/4c682c4255948c4b00c5e81e2fc77296839…
You're receiving this email because of your account on gitlab.com.
2
1
[Git][monnier/typer][graveline] Correction of macro "do", dflt-sym need a symbol and not just "_"
by Jonathan Graveline 27 Jui '18
by Jonathan Graveline 27 Jui '18
27 Jui '18
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
9e9a8e89 by Jonathan Graveline at 2018-06-27T17:57:09Z
Correction of macro "do", dflt-sym need a symbol and not just "_"
- - - - -
3 changed files:
- btl/pervasive.typer
- samples/do.typer
- tests/macro_do_test.ml
Changes:
=====================================
btl/pervasive.typer
=====================================
--- a/btl/pervasive.typer
+++ b/btl/pervasive.typer
@@ -416,13 +416,31 @@ test3 = test4;
%%%%
%%%% Macro : do
%%%%
+%%%% This file may not be up to date with version
+%%%% in pervasive.typer
+%%%%
+
+%%
+%% Here's an example :
+%%
+%% fun = do {
+%% str <- return "\n\tHello world!\n\n";
+%% print str;
+%% };
+%%
+%% str is bind by macro,
+%%
+%% fun is a command,
+%%
+%% do may contain do because it returns a command.
+%%
assign = Sexp_symbol "<-";
get-sym : Sexp -> Sexp;
get-sym sexp = let
- dflt-sym = (lambda _ -> Sexp_symbol "(_ : IO Unit)");
+ dflt-sym = (lambda _ -> (Sexp_symbol " %not used% "));
in Sexp_dispatch sexp
=====================================
samples/do.typer
=====================================
--- a/samples/do.typer
+++ b/samples/do.typer
@@ -25,7 +25,7 @@ assign = Sexp_symbol "<-";
get-sym : Sexp -> Sexp;
get-sym sexp = let
- dflt-sym = (lambda _ -> Sexp_symbol "(_ : IO Unit)");
+ dflt-sym = (lambda _ -> (Sexp_symbol " %not used% "));
in Sexp_dispatch sexp
=====================================
tests/macro_do_test.ml
=====================================
--- a/tests/macro_do_test.ml
+++ b/tests/macro_do_test.ml
@@ -114,5 +114,36 @@ let _ = (add_test "DO MACROS" "do inside do" (fun () ->
| _ -> failure ())
)
+(* declaring the type before assignement *)
+(* this is an unexpected functionality that may be usefull *)
+let _ = (add_test "DO MACROS" "assignement with type declaration" (fun () ->
+ let dcode = "
+ return = IO_return;
+
+ nop = (lambda _ -> return ());
+
+ action = do
+ {
+ (t : Bool) <- return true;
+
+ (f : Bool) <- return false;
+
+ return (if_then_else_ f 333
+ (if_then_else_ t 777 333));
+ };" in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "action;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vcommand cmd] -> ( match (cmd ()) with
+ | Vint 777 -> success ()
+ | _ -> failure () )
+ | _ -> failure ())
+)
+
(* run all tests *)
let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/commit/9e9a8e89166c6270e77be19d6947b50c73b…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/9e9a8e89166c6270e77be19d6947b50c73b…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][graveline] macro "case" now use "do" and "Elab_isconstructor"; added tests/case_test.ml
by Jonathan Graveline 25 Jui '18
by Jonathan Graveline 25 Jui '18
25 Jui '18
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
246ba428 by Jonathan Graveline at 2018-06-25T21:22:00Z
macro "case" now use "do" and "Elab_isconstructor"; added tests/case_test.ml
- - - - -
2 changed files:
- samples/case.typer
- + tests/case_test.ml
Changes:
=====================================
samples/case.typer
=====================================
@@ -3,9 +3,6 @@
%%%
%%% (pattern matching)
%%%
-%%% This file may not be up to date with version
-%%% in pervasive.typer
-%%%
%%
%% Match every variable in each pattern with a list of VarTest.
@@ -68,12 +65,21 @@ mapi f i xs = case xs
| cons x xs => cons (f x i) (mapi f (i + 1) xs);
io_list : List (IO ?a) -> IO (List ?a);
-io_list l = IO_bind (List_foldl
- (lambda o v -> IO_bind o
- (lambda o -> IO_bind v
- (lambda v -> IO_return (cons v o))))
- (IO_return nil) l)
- (lambda l -> IO_return (List_reverse l nil));
+io_list l = let
+
+ fold_fun : IO (List ?a) -> IO ?a -> IO (List ?a);
+ fold_fun o v = do
+ {
+ o <- o;
+ v <- v;
+ IO_return (cons v o);
+ };
+
+in do
+{
+ l <- (List_foldl fold_fun (IO_return nil) l);
+ IO_return (List_reverse l nil);
+};
get_num_vars : List Sexp -> IO (List Sexp);
get_num_vars vars = io_list (List_map
@@ -109,6 +115,21 @@ get_cases sexps = let
in helper sexps;
+%%
+%% return true if v is a ctor
+%%
+is_ctor : Sexp -> IO Bool;
+is_ctor v = Sexp_dispatch v
+ (lambda _ _ -> IO_return true)
+ (lambda s -> do
+ {
+ env <- Elab_getenv ();
+ b <- Elab_isconstructor s env;
+ IO_return (Int_eq b 1);
+ })
+ (lambda _ -> IO_return false) (lambda _ -> IO_return false)
+ (lambda _ -> IO_return false) (lambda _ -> IO_return false);
+
%%
%% Rename nth constructor inside ctor to sym
%%
@@ -116,27 +137,45 @@ in helper sexps;
rename_nth : Int -> Sexp -> Sexp -> IO Sexp;
rename_nth n ctor sym = let
- mapiif : (Sexp -> Int -> Sexp) -> (Sexp -> Bool) -> Int -> List Sexp -> List Sexp;
- mapiif f b i xs = case xs
- | nil => nil
- | cons x xs => if_then_else_ (b x)
- (cons (f x i) (mapiif f b (i + 1) xs))
- (cons x (mapiif f b i xs));
+ mapiif : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool)
+ -> Int -> IO (List Sexp) -> IO (List Sexp);
+ mapiif f b i xs = let
- err = (lambda _ -> Sexp_symbol "<not a ctor (0)>");
+ helper : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int
+ -> List Sexp -> IO (List Sexp);
+ helper f b i xs = case xs
+ | nil => IO_return nil
+ | cons x xs => (let
+
+ apply : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int
+ -> List Sexp -> IO (List Sexp);
+ apply f b i xs = do
+ {
+ xs <- (helper f b (i + 1) xs);
+ IO_return (cons (f x i) xs);
+ };
+
+ continue : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int
+ -> List Sexp -> IO (List Sexp);
+ continue f b i xs = do
+ {
+ xs <- (helper f b i xs);
+ IO_return (cons x xs);
+ };
+
+ in do
+ {
+ bv <- b x;
+ (if_then_else_ bv (apply f b i xs) (continue f b i xs));
+ });
- %%
- %% Is argument a variable or a ctor
- %%
- %% (use keyword "ctor" if the ctor has no argument to
- %% to differentiate with a variable)
- %%
+ in do
+ {
+ xs <- xs;
+ helper f b i xs;
+ };
- is_ctor : Sexp -> Bool;
- is_ctor v = Sexp_dispatch v
- (lambda _ _ -> true) (lambda _ -> false)
- (lambda _ -> false) (lambda _ -> false)
- (lambda _ -> false) (lambda _ -> false);
+ err = (lambda _ -> Sexp_symbol "<not a ctor (0)>");
%%
%% Check for ctor within englobing ctor and rename variable
@@ -147,14 +186,21 @@ rename_nth n ctor sym = let
(lambda s ss -> if_then_else_ (Int_eq i n)
(sym)
(Sexp_symbol "_"))
- (lambda s -> Sexp_symbol s)
+ (lambda s -> if_then_else_ (Int_eq i n)
+ (sym)
+ (Sexp_symbol "_"))
err err err err ;
+
+ io_err = (lambda _ -> IO_return (Sexp_symbol "<not a ctor (1)>"));
-in IO_return (Sexp_dispatch ctor
- (lambda s ss -> Sexp_node s
- (mapiif sub_ctor is_ctor 0 ss))
- (lambda s -> Sexp_symbol s)
- err err err err);
+in (Sexp_dispatch ctor
+ (lambda s ss -> do
+ {
+ ss <- (mapiif sub_ctor is_ctor 0 (IO_return ss));
+ IO_return (Sexp_node s ss);
+ })
+ (lambda s -> IO_return (Sexp_symbol s))
+ io_err io_err io_err io_err);
%%
%% Expand sub pattern into sub_test
@@ -170,28 +216,29 @@ expand_cases pats = let
| nil => o
| cons x xs => foldi f (i + 1) (f x i o) xs;
- get_sub_pattern : Sexp -> List Sexp;
+ get_sub_pattern : Sexp -> IO (List Sexp);
get_sub_pattern ctor = let
err = (lambda _ -> Sexp_error);
-
- check_keyword : Sexp -> Sexp;
- check_keyword ctor = Sexp_dispatch ctor
- (lambda s ss -> if_then_else_ (Sexp_eq s (Sexp_symbol "ctor"))
- (Sexp_node (List_nth 0 ss Sexp_error) (List_tail ss))
- (Sexp_node s ss))
- (lambda s -> Sexp_symbol s)
- err err err err;
- no_pattern : List Sexp -> ? -> List Sexp;
- no_pattern pats = (lambda _ -> pats);
+ no_pattern : List Sexp -> ? -> IO (List Sexp);
+ no_pattern pats = (lambda _ -> IO_return pats);
- helper : List Sexp -> List Sexp;
- helper vars = List_foldl (lambda pats var ->
+ helper : List Sexp -> IO (List Sexp);
+ helper vars = List_foldl (lambda pats var -> do
+ {
+ pats <- pats;
Sexp_dispatch var
- (lambda s ss -> cons (check_keyword (Sexp_node s ss)) pats)
- (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats)
- ) nil vars;
+ (lambda s ss -> IO_return (cons (Sexp_node s ss) pats))
+ (lambda s -> do
+ {
+ b <- is_ctor (Sexp_symbol s);
+ if_then_else_ b
+ (IO_return (cons (Sexp_symbol s) pats))
+ (no_pattern pats ());
+ })
+ (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats)
+ }) (IO_return nil) vars;
in Sexp_dispatch ctor
(lambda s ss -> helper ss)
@@ -227,11 +274,12 @@ expand_cases pats = let
(lambda t -> IO_return (sub_test v t))
| _ => IO_return (var_test Sexp_error);
- sub_pattern : List Sexp;
- sub_pattern = List_reverse (get_sub_pattern t) nil;
-
- nb_pattern : Int;
- nb_pattern = List_length sub_pattern;
+ sub_pattern : IO (List Sexp);
+ sub_pattern = do
+ {
+ l <- get_sub_pattern t;
+ IO_return (List_reverse l nil);
+ };
sub_case : IO (List VarTest);
sub_case = let
@@ -240,17 +288,42 @@ expand_cases pats = let
helper c r o = IO_return (List_concat o
(cons r (cons (sub_test not_unique_sym c) nil)));
- in IO_bind (foldi
- (lambda c i o -> IO_bind o (lambda o -> (IO_bind (renamed i)
- (lambda r -> (helper c r o)))))
- 0 (IO_return nil) sub_pattern)
- (lambda l -> IO_return (cons (push_var nb_pattern) l));
+ l : IO (List VarTest);
+ l = do
+ {
+ sub_pattern <- sub_pattern;
+ (foldi
+ (lambda c i o -> do
+ {
+ o <- o;
+ r <- (renamed i);
+ helper c r o;
+ }) 0 (IO_return nil) sub_pattern)
+ };
- in if_then_else_ (Int_eq nb_pattern 0)
- (IO_bind all (lambda all ->
- IO_return (List_concat all (cons test nil))))
- (IO_bind sub_case (lambda l -> IO_bind all
- (lambda all -> IO_return (List_concat all l))))
+ in do
+ {
+ l <- l;
+ sub_pattern <- sub_pattern;
+ IO_return (cons (push_var (List_length sub_pattern)) l);
+ };
+
+ in do
+ {
+ sub_pattern <- sub_pattern;
+ if_then_else_ (Int_eq (List_length sub_pattern) 0)
+ (do
+ {
+ all <- all;
+ IO_return (List_concat all (cons test nil));
+ })
+ (do
+ {
+ sub_case <- sub_case;
+ all <- all;
+ IO_return (List_concat all sub_case);
+ })
+ };
in expand test);
@@ -261,11 +334,18 @@ expand_cases pats = let
ctors : IO (List VarTest);
ctors = (List_foldl expand_one (IO_return nil) cs);
-
- in IO_bind ctors (lambda ctors ->
- if_then_else_ (Int_eq (List_length cs) (List_length ctors))
+
+ stop_on_id : List VarTest -> IO Pattern;
+ stop_on_id ctors = if_then_else_
+ (Int_eq (List_length cs) (List_length ctors))
(IO_return (branch ctors f))
- (expand_all (branch ctors f))));
+ (expand_all (branch ctors f));
+
+ in do
+ {
+ ctors <- ctors;
+ stop_on_id ctors;
+ });
in io_list (List_map expand_all pats);
@@ -406,30 +486,20 @@ case_ = macro (lambda args -> let
nfun : Sexp;
nfun = fun;
-
- %
- % I was using lambda_->_, then ##case_ needed a type so I added decltype,
- % then decltype needed variable (rather than composed expression)
- % so we end up with a let_in_ (thanks to gensym).
- %
- % nfun = (Sexp_node (foldi
- % (lambda v i fun -> (quote (lambda_->_
- % ((uquote (List_nth i nvars Sexp_error)) : (decltype (uquote v)))
- % (uquote fun))))
- % 0 fun fvars) (List_reverse fvars nil));
- %
in IO_return ( (foldi
(lambda v i fun -> (quote (
let (uquote (List_nth i nvars Sexp_error)) = (uquote v); in (uquote fun))))
0 nfun vars));
- % in IO_return nfun;
- in IO_bind (expand_cases pats) (lambda pats ->
- (IO_bind num_vars (lambda num_vars ->
- IO_bind free_vars (lambda free_vars ->
- IO_bind (pattern_to_sexp num_vars pats) (lambda f ->
- vars_wrap free_vars num_vars f)))));
+ in do
+ {
+ pats <- expand_cases pats;
+ num_vars <- num_vars;
+ free_vars <- free_vars;
+ f <- pattern_to_sexp num_vars pats;
+ vars_wrap free_vars num_vars f;
+ };
% Only the Sexp after "_|_" are interesting
=====================================
tests/case_test.ml
=====================================
@@ -0,0 +1,212 @@
+
+open Util
+open Utest_lib
+
+open Sexp
+open Lexp
+
+open Eval (* reset_eval_trace *)
+
+open Builtin
+open Env
+
+(* default environment *)
+let ectx = Elab.default_ectx
+let rctx = Elab.default_rctx
+
+(*
+ Macro case break some test so I read definition here.
+ It's temporary. I will need to modify other test to use ##case_ (which is what
+ they need to test) or modify the macro to work with everything (there's strange
+ case in eval_test.ml which I did not expect).
+*)
+let case_decl = let read_file filename =
+ let lines = ref [] in
+ let chan = open_in filename in
+ try
+ while true; do
+ lines := input_line chan :: !lines
+ done; !lines
+ with End_of_file ->
+ close_in chan;
+ List.rev !lines
+
+in String.concat "\n" (read_file "samples/case.typer")
+
+let _ = (add_test "CASE MACROS" "case on single variable" (fun () ->
+ let dcode = (case_decl^"
+ f : Bool -> Int;
+ f a = case a
+ | true => 1
+ | 0;
+
+ g : List Int -> Int;
+ g xs = case xs
+ | cons x nil => x
+ | cons x xs => g xs
+ | 0;
+
+ va = f true;
+ vb = f false;
+ vc = g nil;
+ vd = g (cons 1 nil);
+ ve = g (cons 1 (cons 2 nil));") in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "va; vb; vc; vd; ve;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vint a; Vint b; Vint c; Vint d; Vint e;] -> (
+ match (a,b,c,d,e) with
+ | (1,0,0,1,2) -> success ()
+ | (_,_,_,_,_) -> failure () )
+ | _ -> failure ())
+)
+
+let _ = (add_test "CASE MACROS" "case on Bool" (fun () ->
+ let dcode = (case_decl^"
+ f : Bool -> Bool -> Bool -> Int;
+ f a b c = case (a,b,c)
+ | (true,false,_) => 1
+ | (false,_,true) => 2
+ | (_,true,false) => 3
+ | (true,true,true) => 4
+ | (_,_,_) => 0;
+
+ va = f true true true;
+ vb = f false true true;
+ vc = f true false true;
+ vd = f false false true;
+ ve = f true true false;
+ vf = f false true false;
+ vg = f true false false;
+ vh = f false false false;
+ ") in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "va; vb; vc; vd; ve; vf; vg; vh;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vint a; Vint b; Vint c; Vint d;
+ Vint e; Vint f; Vint g; Vint h] -> (
+ match (a,b,c,d,e,f,g,h) with
+ | (4,2,1,2,3,3,1,0) -> success ()
+ | (_,_,_,_,_,_,_,_) -> failure () )
+ | _ -> failure ())
+)
+
+let _ = (add_test "CASE MACROS" "case on list" (fun () ->
+ let dcode = (case_decl^"
+ f : List Int -> List Int -> Int;
+ f xs ys = case (xs,ys)
+ | (cons x xs,cons y ys) => (x + y) + (f xs ys)
+ | (_,_) => 0;
+
+ g : List Int -> List Int;
+ g xs = case xs
+ | cons x ( nil) => (nil : List Int)
+ | cons x xs => cons x (g xs)
+ | _ => (nil : List Int);
+
+ va = f (g (cons 100 (cons 101 (cons 102 nil))))
+ (g (cons 1000 (cons 1001 nil)));
+
+ vb = f (g nil) (g (cons 100 (cons 101 nil)));
+ ") in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "va; vb;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vint a; Vint b] -> (
+ match (a,b) with
+ | (1100,0) -> success ()
+ | (_,_) -> failure () )
+ | _ -> failure ())
+)
+
+let _ = (add_test "CASE MACROS" "3 constant" (fun () ->
+ let dcode = (case_decl^"
+ type ColorComponent
+ | red
+ | green
+ | blue;
+
+ f : ColorComponent -> ColorComponent -> Int;
+ f c1 c2 = case (c1,c2)
+ | (red,red) => 1
+ | (green,green) => 3
+ | (blue,blue) => 2
+ | (red,green) => 1
+ | (red,blue) => 1
+ | (green,red) => 3
+ | (green,blue) => 3
+ | (blue,red) => 2
+ | 2; % (blue,green)
+
+ va = f red red; vb = f red green; vc = f red blue;
+ vd = f blue blue; ve = f blue red; vf = f blue green;
+ vg = f green green; vh = f green red; vi = f green blue;
+ ") in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "va; vb; vc; vd; ve; vf; vg; vh; vi;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vint a; Vint b; Vint c;
+ Vint d; Vint e; Vint f;
+ Vint g; Vint h; Vint i] -> (
+ match (a,b,c,d,e,f,g,h,i) with
+ | (1,1,1,2,2,2,3,3,3) -> success ()
+ | (_,_,_,_,_,_,_,_,_) -> failure () )
+ | _ -> failure ())
+)
+
+let _ = (add_test "CASE MACROS" "sub pattern" (fun () ->
+ let dcode = (case_decl^"
+ f : List (Option Bool) -> List (Option Bool) -> Int;
+ f xs ys = case (xs,ys)
+ | (cons (some true) xs, cons (some true) ys) => f xs ys
+ | (nil,nil) => 1
+ | 0;
+
+ va = f (cons (some true) nil) (cons (some true) nil);
+ vb = f (cons (some true) (cons (some true) nil))
+ (cons (some true) (cons (some true) nil));
+ vc = f nil nil;
+ vd = f (cons (some true) (cons none nil)) (cons (some true) (cons none nil));
+ ve = f (cons (some false) nil) (cons (some false) nil);
+ vf = f (cons none nil) (cons (some true) nil);
+ vg = f (cons (some true) nil) (cons none nil);
+ ") in
+
+ let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in
+
+ let ecode = "va; vb; vc; vd; ve; vf; vg;" in
+
+ let ret = Elab.eval_expr_str ecode ectx rctx in
+
+ match ret with
+ | [Vint a; Vint b; Vint c;
+ Vint d; Vint e; Vint f; Vint g] -> (
+ match (a,b,c,d,e,f,g) with
+ | (1,1,1,0,0,0,0) -> success ()
+ | (_,_,_,_,_,_,_) -> failure () )
+ | _ -> failure ())
+)
+
+
+(* run all tests *)
+let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/commit/246ba4287daff4c4107d43fd8db4fc9727c…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/246ba4287daff4c4107d43fd8db4fc9727c…
You're receiving this email because of your account on gitlab.com.
1
0
21 Jui '18
Stefan pushed to branch graveline at Stefan / Typer
Commits:
7896e300 by Stefan Monnier at 2018-06-21T01:28:09Z
Make all variable "names" optional
* src/util.ml (vname): Make the string optional.
Change all `vname option` to `vname`.
- - - - -
203222b1 by Stefan Monnier at 2018-06-21T15:06:32Z
Merge branch 'trunk' into graveline
- - - - -
15 changed files:
- src/builtin.ml
- src/debruijn.ml
- src/debug_util.ml
- src/elab.ml
- src/elexp.ml
- src/env.ml
- src/eval.ml
- src/inverse_subst.ml
- src/lexp.ml
- src/opslexp.ml
- src/pexp.ml
- src/unification.ml
- src/util.ml
- tests/env_test.ml
- tests/unify_test.ml
Changes:
=====================================
src/builtin.ml
=====================================
@@ -1,6 +1,6 @@
(* builtin.ml --- Infrastructure to define built-in primitives
*
- * Copyright (C) 2016-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2016-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -95,19 +95,19 @@ let set_predef name lexp
(* Builtin types *)
let dloc = DB.dloc
-let op_binary t = mkArrow (Aexplicit, None, t, dloc,
- mkArrow (Aexplicit, None, t, dloc, t))
+let op_binary t = mkArrow (Aexplicit, (dloc, None), t, dloc,
+ mkArrow (Aexplicit, (dloc, None), t, dloc, t))
let type_eq =
- let lv = (dloc, "l") in
- let tv = (dloc, "t") in
- mkArrow (Aerasable, Some lv,
+ let lv = (dloc, Some "l") in
+ let tv = (dloc, Some "t") in
+ mkArrow (Aerasable, lv,
DB.type_level, dloc,
- mkArrow (Aerasable, Some tv,
+ mkArrow (Aerasable, tv,
mkSort (dloc, Stype (Var (lv, 0))), dloc,
- mkArrow (Aexplicit, None,
+ mkArrow (Aexplicit, (dloc, None),
Var (tv, 0), dloc,
- mkArrow (Aexplicit, None,
+ mkArrow (Aexplicit, (dloc, None),
mkVar (tv, 1), dloc,
mkSort (dloc, Stype (Var (lv, 3)))))))
@@ -163,9 +163,11 @@ let register_builtin_csts () =
let register_builtin_types () =
let _ = new_builtin_type "Sexp" DB.type0 in
let _ = new_builtin_type
- "IO" (mkArrow (Aexplicit, None, DB.type0, dloc, DB.type0)) in
+ "IO" (mkArrow (Aexplicit, (dloc, None),
+ DB.type0, dloc, DB.type0)) in
let _ = new_builtin_type
- "Ref" (mkArrow (Aexplicit, None, DB.type0, dloc, DB.type0)) in
+ "Ref" (mkArrow (Aexplicit, (dloc, None),
+ DB.type0, dloc, DB.type0)) in
let _ = new_builtin_type "FileHandle" DB.type0 in
let _ = new_builtin_type "Eq" type_eq in
()
=====================================
src/debruijn.ml
=====================================
@@ -94,7 +94,7 @@ let type_float = mkBuiltin ((dloc, "Float"), type0, None)
let type_string = mkBuiltin ((dloc, "String"), type0, None)
(* easier to debug with type annotations *)
-type env_elem = (vname option * varbind * ltype)
+type env_elem = (vname * varbind * ltype)
type lexp_context = env_elem M.myers
type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *)
@@ -166,31 +166,24 @@ let lexp_ctx_cons (ctx : lexp_context) d v t =
| _ -> true));
M.cons (d, v, t) ctx
-let lctx_extend (ctx : lexp_context) (def: vname option) (v: varbind) (t: lexp) =
+let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) =
lexp_ctx_cons ctx def v t
let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) =
- let (loc, name) = def in
+ let (loc, oname) = def in
let (grm, (n, map), env, sl) = ctx in
- let nmap = SMap.add name n map in
+ let nmap = match oname with None -> map | Some name -> SMap.add name n map in
(grm, (n + 1, nmap),
- lexp_ctx_cons env (Some def) v t,
+ lexp_ctx_cons env def v t,
sl)
-let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t
-
-let ectx_extend (ectx: elab_context) (def: vname option) (v: varbind) (t: lexp)
- : elab_context =
- match def with
- | None -> let (grm, (n, map), lctx, sl) = ectx in
- (grm, (n + 1, map), lexp_ctx_cons lctx None v t, sl)
- | Some def -> env_extend ectx def v t
+let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t
let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) =
let (ctx, _) =
List.fold_left
(fun (ctx, recursion_offset) (def, e, t) ->
- lexp_ctx_cons ctx (Some def) (LetDef (recursion_offset, e)) t,
+ lexp_ctx_cons ctx def (LetDef (recursion_offset, e)) t,
recursion_offset - 1)
(ctx, List.length defs) defs in
ctx
@@ -198,8 +191,10 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) =
let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) =
let (grm, (n, senv), lctx, sl) = ctx in
let senv', _ = List.fold_left
- (fun (senv, i) ((_, vname), _, _) ->
- SMap.add vname i senv, i + 1)
+ (fun (senv, i) ((_, oname), _, _) ->
+ (match oname with None -> senv
+ | Some name -> SMap.add name i senv),
+ i + 1)
(senv, n) defs in
(grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl)
@@ -236,7 +231,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start =
let names = ref [] in
for i = start to n do
let name = match (M.nth (n - i) lst) with
- | (Some (_, name), _, _) -> name
+ | ((_, Some name), _, _) -> name
| _ -> "" in
names := name::!names
done; !names in
@@ -255,14 +250,13 @@ let print_lexp_ctx_n (ctx : lexp_context) start =
try let r, name, exp, tp =
match env_lookup_by_index (n - idx - 1) ctx with
- | (Some (_, name), LetDef (r, exp), tp) -> r, name, Some exp, tp
- | (Some (_, name), _, tp) -> 0, name, None, tp
- | (_, _, tp) -> 0, "", None, tp in
+ | ((_, name), LetDef (r, exp), tp) -> r, name, Some exp, tp
+ | ((_, name), _, tp) -> 0, name, None, tp in
(* Print env Info *)
lalign_print_int r 4;
print_string " | ";
- lalign_print_string name 10; (* name must match *)
+ lalign_print_string (maybename name) 10; (* name must match *)
print_string " | ";
let _ = match exp with
@@ -296,11 +290,11 @@ let dump_lexp_ctx (ctx : lexp_context) =
(* generic lookup *)
let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =
- let ((loc, ename), dbi) = v in
+ let ((loc, oename), dbi) = v in
try(let ret = (Myers.nth dbi ctx) in
- let _ = match ret with
- | (Some (_, name), _, _) ->
+ let _ = match (ret, oename) with
+ | (((_, Some name), _, _), Some ename) ->
(* Check if names match *)
if not (ename = name) then
(print_lexp_ctx ctx;
@@ -314,7 +308,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =
ret)
with
Not_found -> error loc ("DeBruijn index "
- ^ string_of_int dbi ^ " of `" ^ ename
+ ^ string_of_int dbi ^ " of `" ^ maybename oename
^ "` out of bounds!")
@@ -340,8 +334,8 @@ let env_lookup_expr ctx (v : vref): lexp option =
type lct_view =
| CVempty
- | CVlet of vname option * varbind * ltype * lexp_context
- | CVfix of (vname option * lexp * ltype) list * lexp_context
+ | CVlet of vname * varbind * ltype * lexp_context
+ | CVfix of (vname * lexp * ltype) list * lexp_context
let rec lctx_view lctx =
match lctx with
=====================================
src/debug_util.ml
=====================================
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -281,10 +281,10 @@ let main () =
(if (get_p_option "lexp-merge-debug") then(
List.iter (fun ((l, s), lxp, ltp) ->
- lalign_print_string s 20;
+ lalign_print_string (maybename s) 20;
lexp_print ltp; print_string "\n";
- lalign_print_string s 20;
+ lalign_print_string (maybename s) 20;
lexp_print lxp; print_string "\n";
) flexps));
@@ -334,7 +334,7 @@ let main () =
let main = (senv_lookup "main" nctx) in
(* get main body *)
- let body = (get_rte_variable (Some "main") main rctx) in
+ let body = (get_rte_variable (dloc, Some "main") main rctx) in
(* eval main *)
print_eval_result 1 body
=====================================
src/elab.ml
=====================================
@@ -61,10 +61,6 @@ module Unif = Unification
module OL = Opslexp
module EL = Elexp
-(* Shortcut => Create a Var *)
-let make_var name index loc =
- mkVar (((loc, name), index))
-
(* dummies *)
let dloc = dummy_location
@@ -135,9 +131,9 @@ let elab_check_sort (ctx : elab_context) lsort var ltp =
| _ -> let lexp_string e = lexp_string (L.clean e) in
let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in
match var with
- | None -> lexp_error (lexp_location ltp) ltp
- ("`" ^ typestr ^ "` is not a proper type")
- | Some (l, name)
+ | (l, None) -> lexp_error l ltp
+ ("`" ^ typestr ^ "` is not a proper type")
+ | (l, Some name)
-> lexp_error l ltp
("Type of `" ^ name ^ "` is not a proper type: "
^ typestr)
@@ -147,8 +143,8 @@ let elab_check_proper_type (ctx : elab_context) ltp var =
with e -> print_string "Exception while checking type `";
lexp_print ltp;
(match var with
- | None -> ()
- | Some (_, name)
+ | (_, None) -> ()
+ | (_, Some name)
-> print_string ("` of var `" ^ name ^"`\n"));
print_lexp_ctx (ectx_to_lctx ctx);
raise e
@@ -175,26 +171,26 @@ let elab_check_def (ctx : elab_context) var lxp ltype =
^ lexp_string ltype ^ " and " ^ lexp_string ltype');
raise e)
then
- elab_check_proper_type ctx ltype (Some var)
+ elab_check_proper_type ctx ltype var
else
(EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [
lexp_string lxp ^ " !: " ^ lexp_string ltype;
" because";
lexp_string ltype' ^ " != " ^ lexp_string ltype])
-let ctx_extend (ctx: elab_context) (var : vname option) def ltype =
+let ctx_extend (ctx: elab_context) (var : vname) def ltype =
elab_check_proper_type ctx ltype var;
ectx_extend ctx var def ltype
let ctx_define (ctx: elab_context) var lxp ltype =
elab_check_def ctx var lxp ltype;
- env_extend ctx var (LetDef (0, lxp)) ltype
+ ectx_extend ctx var (LetDef (0, lxp)) ltype
let ctx_define_rec (ctx: elab_context) decls =
let nctx = ectx_extend_rec ctx decls in
let _ = List.fold_left (fun n (var, lxp, ltp)
-> elab_check_proper_type
- nctx (push_susp ltp (S.shift n)) (Some var);
+ nctx (push_susp ltp (S.shift n)) var;
n - 1)
(List.length decls)
decls in
@@ -243,21 +239,22 @@ let ctx_define_rec (ctx: elab_context) decls =
* definitions.
*)
-let newMetavar (ctx : lexp_context) sl l name t=
+let newMetavar (ctx : lexp_context) sl name t =
let meta = Unif.create_metavar ctx sl t in
- mkMetavar (meta, S.Identity, (l, name))
+ mkMetavar (meta, S.Identity, name)
let newMetalevel (ctx : lexp_context) sl loc =
- newMetavar ctx sl Util.dummy_location "ℓ" type_level
+ newMetavar ctx sl (loc, Some "ℓ") type_level
let newMetatype (ctx : lexp_context) sl loc
- = newMetavar ctx sl loc "τ" (mkSort (loc, Stype (newMetalevel ctx sl loc)))
+ = newMetavar ctx sl (loc, Some "τ")
+ (mkSort (loc, Stype (newMetalevel ctx sl loc)))
(* Functions used when we need to return some lexp/ltype but
* an error makes it impossible to return "the right one". *)
let mkDummy_type ctx loc = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc
let mkDummy_check ctx loc t = newMetavar (ectx_to_lctx ctx) dummy_scope_level
- loc "dummy" t
+ (loc, None) t
let mkDummy_infer ctx loc =
let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in
(mkDummy_check ctx loc t, t)
@@ -276,9 +273,10 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context =
| _
-> sexp_error loc "define-operator expects 3 argument"; ctx
-let elab_varref ctx ((loc, name) as id)
+let elab_varref ctx (loc, name)
= let idx = senv_lookup name ctx in
- let lxp = make_var name idx loc in
+ let id = (loc, Some name) in
+ let lxp = mkVar (id, idx) in
let ltp = env_lookup_type ctx (id, idx) in
(lxp, Inferred ltp)
@@ -401,6 +399,9 @@ let generalize (nctx : elab_context) e =
wrap (IMap.mem id nes) vname mt'' l e' in
loop (IMap.empty) len mfvs
+and elab_p_id ((l,name) : symbol) : vname =
+ (l, match name with "_" -> None | _ -> Some name)
+
(* Infer or check, as the case may be. *)
let rec elaborate ctx se ot =
match se with
@@ -451,7 +452,7 @@ and elab_special_form ctx f args ot =
sform_dummy_ret ctx loc
(* Make up an argument of type `t` when none is provided. *)
-and get_implicit_arg ctx loc name t =
+and get_implicit_arg ctx loc oname t =
(* lookup default attribute of t. *)
(* FIXME: Don't lookup defaults/tactics here. Instead, just always
* generate a metavar at this point. The use of defaults/tactics should be
@@ -459,7 +460,7 @@ and get_implicit_arg ctx loc name t =
match
try (* FIXME: We shouldn't hard code as popular a name as `default`. *)
let pidx, pname = (senv_lookup "default" ctx), "default" in
- let default = Var ((dloc, pname), pidx) in
+ let default = Var ((dloc, Some pname), pidx) in
get_attribute ctx loc [default; t]
with Not_found -> None with
| Some attr
@@ -481,17 +482,15 @@ and get_implicit_arg ctx loc name t =
(* Elaborate the argument *)
check lsarg t ctx
- | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc name t
+ | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx)
+ (loc, oname) t
(* Build the list of implicit arguments to instantiate. *)
and instantiate_implicit e t ctx =
let rec instantiate t args =
match OL.lexp_whnf t (ectx_to_lctx ctx) with
- | Arrow ((Aerasable | Aimplicit) as ak, v, t1, _, t2)
- -> let arg = get_implicit_arg
- ctx (lexp_location e)
- (Eval.varname v)
- t1 in
+ | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2)
+ -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in
instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args)
| _ -> (mkCall (e, List.rev args), t)
in instantiate t []
@@ -521,9 +520,9 @@ and infer_type pexp ectx var =
-> (let lexp_string e = lexp_string (L.clean e) in
let typestr = lexp_string t ^ " : " ^ lexp_string s in
match var with
- | None -> lexp_error (lexp_location t) t
- ("`" ^ typestr ^ "` is not a proper type")
- | Some (l, name)
+ | (l, None) -> lexp_error l t
+ ("`" ^ typestr ^ "` is not a proper type")
+ | (l, Some name)
-> lexp_error l t
("Type of `" ^ name ^ "` is not a proper type: "
^ typestr))
@@ -538,10 +537,10 @@ and unify_with_arrow ctx tloc lxp kind var aty
= let arg = match aty with
| None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) tloc
| Some laty -> laty in
- let nctx = ectx_extend ctx (Some var) Variable arg in
+ let nctx = ectx_extend ctx var Variable arg in
let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in
let (l, _) = var in
- let arrow = mkArrow (kind, Some var, arg, l, body) in
+ let arrow = mkArrow (kind, var, arg, l, body) in
match Unif.unify arrow lxp (ectx_to_lctx ctx) with
| None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp
^ " and "
@@ -677,39 +676,34 @@ and check_case rtype (loc, target, ppatterns) ctx =
-> lexp_error loc lctor
"Too many pattern args to the constructor";
make_nctx ctx s [] [] pe acc
- | (_, Ppatcons (p, _))::pargs, cargs
- -> lexp_error (sexp_location p) lctor
- "Nested patterns not supported!";
- make_nctx ctx s pargs cargs pe acc
- | (_, (ak, Some (_, fname), fty)::cargs)
+ | (_, (ak, (_, Some fname), fty)::cargs)
when SMap.mem fname pe
-> let var = SMap.find fname pe in
let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
- make_nctx nctx (ssink (maybev var) s) pargs cargs
+ make_nctx nctx (ssink var s) pargs cargs
(SMap.remove fname pe)
((ak, var)::acc)
- | ((ef, fpat)::pargs, (ak, _, fty)::cargs)
+ | ((ef, var)::pargs, (ak, _, fty)::cargs)
when (match (ef, ak) with
| (Some (_, "_"), _) | (None, Aexplicit) -> true
| _ -> false)
- -> let var = match fpat with Ppatsym v -> Some v | _ -> None in
- let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
- make_nctx nctx (ssink (maybev var) s) pargs cargs pe
+ -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
+ make_nctx nctx (ssink var s) pargs cargs pe
((ak, var)::acc)
- | ((Some (l, fname), fpat)::pargs, cargs)
- -> let var = match fpat with Ppatsym v -> Some v | _ -> None in
- if SMap.mem fname pe then
+ | ((Some (l, fname), var)::pargs, cargs)
+ -> if SMap.mem fname pe then
sexp_error l ("Duplicate explicit field `" ^ fname ^ "`");
make_nctx ctx s pargs cargs (SMap.add fname var pe) acc
| pargs, (ak, fname, fty)::cargs
- -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in
+ -> let var = (loc, None) in
+ let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
if ak = Aexplicit then
sexp_error loc
("Missing pattern for normal field"
- ^ (match fname with Some (_,n) -> " `" ^ n ^ "`"
+ ^ (match fname with (_, Some n) -> " `" ^ n ^ "`"
| _ -> ""));
- make_nctx nctx (ssink vdummy s) pargs cargs pe
- ((ak, None)::acc) in
+ make_nctx nctx (ssink var s) pargs cargs pe
+ ((ak, var)::acc) in
let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in
let rtype' = mkSusp rtype
(S.shift (M.length (ectx_to_lctx nctx)
@@ -723,15 +717,15 @@ and check_case rtype (loc, target, ppatterns) ctx =
in
match pat with
- | Ppatany _ -> add_default None
- | Ppatsym ((_, name) as var)
+ | Ppatsym ((_, None) as var) -> add_default var
+ | Ppatsym ((l, Some name) as var)
-> (try let idx = senv_lookup name ctx in
match OL.lexp_whnf (mkVar (var, idx))
(ectx_to_lctx ctx) with
| Cons _ (* It's indeed a constructor! *)
- -> add_branch (Symbol var) []
- | _ -> add_default (Some var) (* A named default branch. *)
- with Not_found -> add_default (Some var))
+ -> add_branch (Symbol (l, name)) []
+ | _ -> add_default var (* A named default branch. *)
+ with Not_found -> add_default var)
| Ppatcons (pctor, pargs) -> add_branch pctor pargs in
@@ -763,7 +757,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
let rec handle_fun_args largs sargs pending ltp =
let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in
match sargs, ltp' with
- | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type)
+ | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type)
when SMap.mem aname pending
-> let sarg = SMap.find aname pending in
let larg = check sarg arg_type ctx in
@@ -792,7 +786,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
handle_fun_args largs sargs pending ltp
(* Aerasable *)
- | _, Arrow ((Aerasable | Aimplicit) as ak, v, arg_type, _, ret_type)
+ | _, Arrow ((Aerasable | Aimplicit) as ak, (l,v), arg_type, _, ret_type)
(* Don't instantiate after the last explicit arg: the rest is done,
* when needed in infer_and_check (via instantiate_implicit). *)
when not (sargs = [] && SMap.is_empty pending)
@@ -800,8 +794,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
ctx (match sargs with
| [] -> loc
| sarg::_ -> sexp_location sarg)
- (match v with Some (_, name) -> name | _ -> "v")
- arg_type in
+ v arg_type in
handle_fun_args ((ak, larg) :: largs) sargs pending
(L.mkSusp ret_type (S.substitute larg))
| [], _
@@ -822,7 +815,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
| Arrow (ak, _, arg_type, _, ret_type)
-> assert (ak = Aexplicit); (arg_type, ret_type)
| _ -> unify_with_arrow ctx (sexp_location sarg)
- ltp' Aexplicit (dloc, "<anon>") None in
+ ltp' Aexplicit (dloc, None) None in
let larg = check sarg arg_type ctx in
handle_fun_args ((Aexplicit, larg) :: largs) sargs pending
(L.mkSusp ret_type (S.substitute larg)) in
@@ -833,8 +826,8 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
(* Parse inductive type definition. *)
and lexp_parse_inductive ctors ctx =
- let make_args (args:(arg_kind * pvar option * sexp) list) ctx
- : (arg_kind * vname option * ltype) list =
+ let make_args (args:(arg_kind * vname * sexp) list) ctx
+ : (arg_kind * vname * ltype) list =
let nctx = ectx_new_scope ctx in
let rec loop args acc ctx =
match args with
@@ -849,7 +842,7 @@ and lexp_parse_inductive ctors ctx =
acc impossible in
let g = generalize nctx altacc in
let altacc' = g (fun _ne vname t l e
- -> Arrow (Aerasable, Some vname, t, l, e))
+ -> Arrow (Aerasable, vname, t, l, e))
altacc in
if altacc' == altacc
then acc (* No generalization! *)
@@ -859,13 +852,10 @@ and lexp_parse_inductive ctors ctx =
| Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e)
| _ -> assert (e = impossible); [] in
loop altacc'
- | hd::tl -> begin
- match hd with
- | (kind, var, exp) ->
- let lxp = infer_type exp ctx var in
- let nctx = ectx_extend ctx var Variable lxp in
- loop tl ((kind, var, lxp)::acc) nctx
- end in
+ | (kind, var, exp)::tl
+ -> let lxp = infer_type exp ctx var in
+ let nctx = ectx_extend ctx var Variable lxp in
+ loop tl ((kind, var, lxp)::acc) nctx in
loop args [] nctx in
List.fold_left
@@ -882,7 +872,7 @@ and track_fv rctx lctx e =
"a bug"
else let tfv i =
let name = match Myers.nth i rctx with
- | (Some n,_) -> n
+ | ((_, Some n),_) -> n
| _ -> "<anon>" in
match Myers.nth i lctx with
| (_, LetDef (o, e), _)
@@ -924,7 +914,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option)
let args = [macro; BI.o2v_list sargs] in
(* FIXME: Make a proper `Var`. *)
- EV.eval_call loc (EL.Var ((DB.dloc, "expand_macro"), 0)) ([], [])
+ EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) ([], [])
macro_expand args
(* Print each generated decls *)
@@ -950,7 +940,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp =
and lexp_check_decls (ectx : elab_context) (* External context. *)
(nctx : elab_context) (* Context with type declarations. *)
- (defs : (vname * sexp) list)
+ (defs : (symbol * sexp) list)
: (vname * lexp * ltype) list * elab_context =
(* Preserve the new operators added to nctx. *)
let ectx = let (_, a, b, c) = ectx in
@@ -958,7 +948,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *)
(grm, a, b, c) in
let (declmap, nctx)
= List.fold_right
- (fun ((_, vname) as v, pexp) (map, nctx) ->
+ (fun ((l, vname), pexp) (map, nctx) ->
let i = senv_lookup vname nctx in
assert (i < List.length defs);
match Myers.nth i (ectx_to_lctx nctx) with
@@ -967,24 +957,24 @@ and lexp_check_decls (ectx : elab_context) (* External context. *)
let e = check pexp adjusted_t nctx in
let (grm, ec, lc, sl) = nctx in
let d = (v', LetDef (i + 1, e), t) in
- (IMap.add i (v, e, t) map,
+ (IMap.add i ((l, Some vname), e, t) map,
(grm, ec, Myers.set_nth i d lc, sl))
| _ -> U.internal_error "Defining same slot!")
defs (IMap.empty, nctx) in
let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in
decls, ctx_define_rec ectx decls
-and infer_and_generalize_type (ctx : elab_context) se oname =
+and infer_and_generalize_type (ctx : elab_context) se name =
let nctx = ectx_new_scope ctx in
- let t = infer_type se nctx oname in
+ let t = infer_type se nctx name in
match OL.lexp_whnf t (ectx_to_lctx ctx) with
(* There's no point generalizing a single metavar, and it's useful
* to keep it ungeneralized so we can use `x : ?` to declare that
* `x` will be defined later without specifying its type yet. *)
| Metavar _ -> t
| _ -> let g = generalize nctx t in
- g (fun _ne vname t l e
- -> mkArrow (Aerasable, Some vname, t, l, e))
+ g (fun _ne name t l e
+ -> mkArrow (Aerasable, name, t, l, e))
t
and infer_and_generalize_def (ctx : elab_context) se =
@@ -995,9 +985,9 @@ and infer_and_generalize_def (ctx : elab_context) se =
-> mkLambda ((if ne then Aimplicit else Aerasable),
vname, t, e))
e in
- let t' = g (fun ne vname t l e
+ let t' = g (fun ne name t l e
-> mkArrow ((if ne then Aimplicit else Aerasable),
- Some vname, t, sexp_location se, e))
+ name, t, sexp_location se, e))
t in
(e', t')
@@ -1006,7 +996,7 @@ and lexp_decls_1
(ectx : elab_context) (* External ctx. *)
(nctx : elab_context) (* New context. *)
(pending_decls : location SMap.t) (* Pending type decls. *)
- (pending_defs : (vname * sexp) list) (* Pending definitions. *)
+ (pending_defs : (symbol * sexp) list) (* Pending definitions. *)
: (vname * lexp * ltype) list * sexp list * elab_context =
match sdecls with
@@ -1027,8 +1017,8 @@ and lexp_decls_1
| Node (Symbol (l, "_:_"), args) :: sdecls
(* FIXME: Move this to a "special form"! *)
-> (match args with
- | [Symbol ((l, vname) as v); stp]
- -> let ltp = infer_and_generalize_type nctx stp (Some v) in
+ | [Symbol (l, vname); stp]
+ -> let ltp = infer_and_generalize_type nctx stp (l, Some vname) in
if SMap.mem vname pending_decls then
(* Don't burp: take'em all and unify! *)
let pt_idx = senv_lookup vname nctx in
@@ -1050,7 +1040,7 @@ and lexp_decls_1
(error l ("Variable `" ^ vname ^ "` already defined!");
lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
else lexp_decls_1 sdecls ectx
- (env_extend nctx v ForwardRef ltp)
+ (ectx_extend nctx (l, Some vname) ForwardRef ltp)
(SMap.add vname l pending_decls)
pending_defs
| _ -> error l "Invalid type declaration syntax";
@@ -1059,16 +1049,17 @@ and lexp_decls_1
| Node (Symbol (l, "_=_") as head, args) :: sdecls
(* FIXME: Move this to a "special form"! *)
-> (match args with
- | [Symbol ((l, vname) as v); sexp]
+ | [Symbol ((l, vname)); sexp]
when SMap.is_empty pending_decls
-> assert (pending_defs == []);
(* Used to be true before we added define-operator. *)
(* assert (ectx == nctx); *)
let (lexp, ltp) = infer_and_generalize_def nctx sexp in
+ let var = (l, Some vname) in
(* Lexp decls are always recursive, so we have to shift by 1 to
* account for the extra var (ourselves). *)
- [(v, mkSusp lexp (S.shift 1), ltp)], sdecls,
- ctx_define nctx v lexp ltp
+ [(var, mkSusp lexp (S.shift 1), ltp)], sdecls,
+ ctx_define nctx var lexp ltp
| [Symbol ((l, vname) as v); sexp]
-> if SMap.mem vname pending_decls then
@@ -1132,7 +1123,7 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp =
and sform_new_attribute ctx loc sargs ot =
match sargs with
- | [t] -> let ltp = infer_type t ctx None in
+ | [t] -> let ltp = infer_type t ctx (loc, None) in
(* FIXME: This creates new values for type `ltp` (very wrong if `ltp`
* is False, for example): Should be a type like `AttributeMap t`
* instead. *)
@@ -1145,7 +1136,7 @@ and sform_new_attribute ctx loc sargs ot =
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
+ | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr
| _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in
let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with
@@ -1161,7 +1152,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot =
and get_attribute ctx loc largs =
let ctx_n = get_size ctx in
let table, var = match largs with
- | [table; Var((_, name), idx)] -> table, (ctx_n - idx, name)
+ | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name)
| _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in
let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with
@@ -1173,7 +1164,8 @@ and get_attribute ctx loc largs =
and sform_dummy_ret ctx loc =
let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in
- (newMetavar (ectx_to_lctx ctx) dummy_scope_level loc "special-form-error" t,
+ (newMetavar (ectx_to_lctx ctx) dummy_scope_level
+ (loc, Some "special-form-error") t,
Inferred t)
and sform_get_attribute ctx loc (sargs : sexp list) ot =
@@ -1184,7 +1176,7 @@ and sform_get_attribute ctx loc (sargs : sexp list) ot =
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)
+ | [table; Var((_, Some name), idx)] -> table, (n - idx, name)
| _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in
let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with
@@ -1245,6 +1237,26 @@ let sform_datacons ctx loc sargs ot =
| _ -> sexp_error loc "##constr requires two arguments";
sform_dummy_ret ctx loc
+let elab_colon_to_ak k = match k with
+ | "_:::_" -> Aerasable
+ | "_::_" -> Aimplicit
+ | _ -> Aexplicit
+
+let elab_datacons_arg s = match s with
+ | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol s; t])
+ -> (elab_colon_to_ak k, elab_p_id s, t)
+ | _ -> (Aexplicit, (sexp_location s, None), s)
+
+let elab_typecons_arg arg : (arg_kind * vname * sexp option) =
+ match arg with
+ | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e])
+ -> (elab_colon_to_ak k,
+ (l, Some name), Some e)
+ | Symbol (l, name) -> (Aexplicit, (l, Some name), None)
+ | _ -> sexp_print arg;
+ (sexp_error (sexp_location arg) "Unrecognized formal arg");
+ (Aexplicit, (sexp_location arg, None), None)
+
let sform_typecons ctx loc sargs ot =
match sargs with
| [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy)
@@ -1261,7 +1273,7 @@ let sform_typecons ctx loc sargs ot =
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 (kind, var, opxp) = elab_typecons_arg sformal in
let ltp = match opxp with
| Some pxp -> let (l,_) = infer pxp ctx in l
| None -> let (l,_) = var in
@@ -1269,7 +1281,7 @@ let sform_typecons ctx loc sargs ot =
(ectx_to_scope_level ctx) l in
parse_formals sformals ((kind, var, ltp) :: rformals)
- (env_extend ctx var Variable ltp) in
+ (ectx_extend ctx var Variable ltp) in
let (formals, nctx) = parse_formals formals [] ctx in
@@ -1279,7 +1291,7 @@ let sform_typecons ctx loc sargs ot =
-> match case with
(* read Constructor name + args => Type ((Symbol * args) list) *)
| Node (Symbol s, cases)
- -> (s, List.map pexp_p_ind_arg cases)::pcases
+ -> (s, List.map elab_datacons_arg cases)::pcases
(* This is a constructor with no args *)
| Symbol s -> (s, [])::pcases
@@ -1293,7 +1305,7 @@ let sform_typecons ctx loc sargs ot =
let sform_hastype ctx loc sargs ot =
match sargs with
- | [se; st] -> let lt = infer_type st ctx None in
+ | [se; st] -> let lt = infer_type st ctx (loc, None) in
let le = check se lt ctx in
(le, Inferred lt)
| _ -> sexp_error loc "##_:_ takes two arguments";
@@ -1303,11 +1315,11 @@ let sform_arrow kind ctx loc sargs ot =
match sargs with
| [st1; st2]
-> let (v, st1) = match st1 with
- | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (Some v, st1)
- | _ -> (None, st1) in
+ | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1)
+ | _ -> ((sexp_location st1, None), st1) in
let lt1 = infer_type st1 ctx v in
let nctx = ectx_extend ctx v Variable lt1 in
- let lt2 = infer_type st2 nctx None in
+ let lt2 = infer_type st2 nctx (sexp_location st2, None) in
(mkArrow (kind, v, lt1, loc, lt2), Lazy)
| _ -> sexp_error loc "##_->_ takes two arguments";
sform_dummy_ret ctx loc
@@ -1359,14 +1371,14 @@ let sform_identifier ctx loc sargs ot =
let subst = S.shift ctx_shift in
let (_, _, rmmap) = ectx_get_scope ctx in
if not (name = "") && SMap.mem name (!rmmap) then
- (mkMetavar (SMap.find name (!rmmap), subst, (loc, name)), Lazy)
+ (mkMetavar (SMap.find name (!rmmap), subst, (loc, Some name)), Lazy)
else
let t = match ot with
| None -> newMetatype octx sl loc
| Some t
(* `t` is defined in ctx instead of octx. *)
-> Inverse_subst.apply_inv_subst t subst in
- let mv = newMetavar octx sl loc name t in
+ let mv = newMetavar octx sl (loc, Some name) t in
(if not (name = "") then
let idx = match mv with
| Metavar (idx, _, _) -> idx
@@ -1395,22 +1407,22 @@ let rec sform_lambda kind ctx loc sargs ot =
match sargs with
| [sarg; sbody]
-> let (arg, ost1) = match sarg with
- | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (arg, Some st)
- | Symbol arg -> (arg, None)
+ | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st)
+ | Symbol arg -> (elab_p_id arg, None)
| _ -> sexp_error (sexp_location sarg)
"Unrecognized lambda argument";
- ((dummy_location, "_"), None) in
+ ((dummy_location, None), None) in
let olt1 = match ost1 with
- | Some st -> Some (infer_type st ctx (Some arg))
+ | Some st -> Some (infer_type st ctx arg)
| _ -> None in
let mklam lt1 olt2 =
- let nctx = env_extend ctx arg Variable lt1 in
+ let nctx = ectx_extend ctx arg Variable lt1 in
let (lbody, alt) = elaborate nctx sbody olt2 in
(mkLambda (kind, arg, lt1, lbody),
match alt with
- | Inferred lt2 -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2))
+ | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2))
| _ -> alt) in
(match ot with
@@ -1432,21 +1444,20 @@ let rec sform_lambda kind ctx loc sargs ot =
^ lexp_string lt1 ^ "`"));
mklam lt1 (Some lt2)
- | Arrow (ak2, ov, lt1, _, lt2) when kind = Aexplicit
+ | Arrow (ak2, v, lt1, _, lt2) when kind = Aexplicit
(* `t` is an implicit arrow and `kind` is Aexplicit,
* so auto-add a corresponding Lambda wrapper!
* FIXME: This should be moved to a macro. *)
- -> let v = var_of_ovar loc ov in
- (* FIXME: Here we end up adding a local variable `v` whose
+ -> (* FIXME: Here we end up adding a local variable `v` whose
* name is lot lexically present, so there's a risk of
* name capture. We should make those vars anonymous? *)
- let nctx = env_extend ctx v Variable lt1 in
+ let nctx = ectx_extend ctx v Variable lt1 in
(* FIXME: Don't go back to sform_lambda, but use an internal
* loop to avoid re-computing olt1 each time. *)
let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in
(mkLambda (ak2, v, lt1, lam),
match alt with
- | Inferred lt2' -> Inferred (mkArrow (ak2, ov, lt1, loc, lt2'))
+ | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2'))
| _ -> alt)
| lt
@@ -1466,7 +1477,7 @@ let rec sform_case ctx loc sargs ot = match sargs with
-> (pexp_p_pat pat, code)
| _ -> let l = (sexp_location branch) in
sexp_error l "Unrecognized simple case branch";
- (Ppatany l, Symbol (l, "?")) in
+ (Ppatsym (l, None), Symbol (l, "?")) in
let pcases = List.map parse_case scases in
let t = match ot with
| Some t -> t
@@ -1616,7 +1627,7 @@ let default_ectx
let register_predefs elctx =
try List.iter (fun name ->
let idx = senv_lookup name elctx in
- let v = Var((dloc, name), idx) in
+ let v = mkVar ((dloc, Some name), idx) in
BI.set_predef name v) BI.predef_names;
with e ->
warning dloc "Predef not found"; in
@@ -1625,7 +1636,7 @@ let default_ectx
let lctx = empty_elab_context in
let lctx = SMap.fold (fun key (e, t) ctx
-> if String.get key 0 = '-' then ctx
- else ctx_define ctx (dloc, key) e t)
+ else ctx_define ctx (dloc, Some key) e t)
(!BI.lmap) lctx in
(* read base file *)
@@ -1656,7 +1667,7 @@ let default_rctx =
(* Lexp helper *)
let _lexp_expr_str (str: string) (tenv: token_env)
(grm: grammar) (limit: string option) (ctx: elab_context) =
- let pxps = _pexp_expr_str str tenv grm limit in
+ let pxps = _sexp_parse_str str tenv grm limit in
let lexps = lexp_parse_all pxps ctx in
List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp))
lexps;
=====================================
src/elexp.ml
=====================================
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -48,7 +48,7 @@ type elexp =
| Imm of sexp
(* A builtin constant, typically a function implemented in Ocaml. *)
- | Builtin of vname
+ | Builtin of symbol
(* A variable reference, using deBruijn indexing. *)
| Var of vref
@@ -72,8 +72,8 @@ type elexp =
* tests the value of `e`, and either selects the corresponding branch
* in `branches` or branches to the `default`. *)
| Case of U.location * elexp
- * (U.location * (vname option) list * elexp) SMap.t
- * (vname option * elexp) option
+ * (U.location * vname list * elexp) SMap.t
+ * (vname * elexp) option
(* A Type expression. There's no useful operation we can apply to it,
* but they can appear in the code. *)
@@ -109,19 +109,19 @@ and elexp_string lxp =
let maybe_str lxp =
match lxp with
| Some (v, lxp)
- -> " | " ^ (match v with None -> "_" | Some (_,name) -> name)
+ -> " | " ^ (match v with (_, None) -> "_" | (_, Some name) -> name)
^ " => " ^ elexp_string lxp
| None -> "" in
let str_decls d =
List.fold_left (fun str ((_, s), lxp) ->
- str ^ " " ^ s ^ " = " ^ (elexp_string lxp)) "" d in
+ str ^ " " ^ L.maybename s ^ " = " ^ (elexp_string lxp)) "" d in
let str_pat lst =
List.fold_left (fun str v ->
str ^ " " ^ (match v with
- | None -> "_"
- | Some (_, s) -> s)) "" lst in
+ | (_, None) -> "_"
+ | (_, Some s) -> s)) "" lst in
let str_cases c =
SMap.fold (fun key (_, lst, lxp) str ->
@@ -135,10 +135,10 @@ and elexp_string lxp =
match lxp with
| Imm(s) -> sexp_string s
| Builtin((_, s)) -> s
- | Var((_, s), i) -> s ^ "[" ^ string_of_int i ^ "]"
+ | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]"
| Cons((_, s)) -> "datacons(" ^ s ^")"
- | Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_string b)
+ | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b)
| Let(_, d, b) ->
"let" ^ (str_decls d) ^ " in " ^ (elexp_string b)
=====================================
src/env.ml
=====================================
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -54,7 +54,7 @@ type value_type =
| Vcons of symbol * value_type list
| Vbuiltin of string
| Vfloat of float
- | Closure of string * elexp * runtime_env
+ | Closure of vname * elexp * runtime_env
| Vsexp of sexp (* Values passed to macros. *)
(* Unable to eval during macro expansion, only throw if the value is used *)
| Vundefined
@@ -65,7 +65,7 @@ type value_type =
| Vref of (value_type ref)
(* Runtime Environ *)
- and runtime_env = (string option * (value_type ref)) M.myers
+ and runtime_env = (vname * (value_type ref)) M.myers
let rec value_equal a b =
match a, b with
@@ -138,7 +138,7 @@ let rec value_string v =
| Vfloat f -> string_of_float f
| Vsexp s -> sexp_string s
| Vtype e -> L.lexp_string e
- | Closure (s, elexp, _) -> "(lambda " ^ s ^ " -> " ^ (elexp_string elexp) ^ ")"
+ | Closure ((_, s), elexp, _) -> "(lambda " ^ L.maybename s ^ " -> " ^ (elexp_string elexp) ^ ")"
| Vcons ((_, s), lst)
-> let args = List.fold_left
(fun str v -> str ^ " " ^ value_string v)
@@ -152,13 +152,13 @@ let make_runtime_ctx = M.nil
let get_rte_size (ctx: runtime_env): int = M.length ctx
-let get_rte_variable (name: string option) (idx: int)
+let get_rte_variable (name: vname) (idx: int)
(ctx: runtime_env): value_type =
try (
let (defname, ref_cell) = (M.nth idx ctx) in
let x = !ref_cell in
match (defname, name) with
- | (Some n1, Some n2) -> (
+ | ((_, Some n1), (_, Some n2)) -> (
if n1 = n2 then
x
else (
@@ -168,11 +168,11 @@ let get_rte_variable (name: string option) (idx: int)
| _ -> x)
with Not_found ->
- let n = match name with Some n -> n | None -> "" in
+ let n = match name with (_, Some n) -> n | _ -> "" in
error dloc ("Variable lookup failure. Var: \"" ^
n ^ "\" idx: " ^ (str_idx idx))
-let add_rte_variable name (x: value_type) (ctx: runtime_env)
+let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env)
: runtime_env =
let valcell = ref x in
M.cons (name, valcell) ctx
@@ -181,7 +181,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) =
let (n, ref_cell) = (M.nth idx ctx) in
(match (n, name) with
- | Some n1, Some n2
+ | ((_, Some n1), (_, Some n2))
-> if (n1 != n2) then
error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2)
| _ -> ());
@@ -192,7 +192,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) =
let nfirst_rte_var n ctx =
let rec loop i acc =
if i < n then
- loop (i + 1) ((get_rte_variable None i ctx)::acc)
+ loop (i + 1) ((get_rte_variable L.vdummy i ctx)::acc)
else
List.rev acc in
loop 0 []
@@ -219,8 +219,8 @@ let print_rte_ctx_n (ctx: runtime_env) start =
let g = !vref in
let _ =
match n with
- | Some m -> lalign_print_string m 12; print_string " | "
- | None -> print_string (make_line ' ' 12); print_string " | " in
+ | (_, Some m) -> lalign_print_string m 12; print_string " | "
+ | _ -> print_string (make_line ' ' 12); print_string " | " in
value_print g; print_string "\n") start
=====================================
src/eval.ml
=====================================
@@ -370,7 +370,7 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type
| Imm(Float (_, n)) -> Vfloat n
| Imm(sxp) -> Vsexp sxp
| Cons (label) -> Vcons (label, [])
- | Lambda ((_, n), lxp) -> Closure (n, lxp, ctx)
+ | Lambda (n, lxp) -> Closure (n, lxp, ctx)
| Builtin ((_, str)) -> Vbuiltin str
(* Return a value stored in env *)
@@ -407,11 +407,11 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type
and eval_var ctx lxp v =
- let ((loc, name), idx) = v in
- try get_rte_variable (Some name) (idx) ctx
+ let (name, idx) = v in
+ try get_rte_variable name idx ctx
with e ->
- elexp_fatal loc lxp
- ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")
+ elexp_fatal (fst name) lxp
+ ("Variable: " ^ L.maybename (snd name) ^ (str_idx idx) ^ " was not found ")
(* unef: unevaluated function (to make the trace readable) *)
and eval_call loc unef i f args =
@@ -424,14 +424,14 @@ and eval_call loc unef i f args =
| Closure (x, e, ctx), v::vs
-> let rec bindargs e vs ctx = match (vs, e) with
- | (v::vs, Lambda ((_, x), e))
+ | (v::vs, Lambda (x, e))
(* "Uncurry" on the fly. *)
- -> bindargs e vs (add_rte_variable (Some x) v ctx)
+ -> bindargs e vs (add_rte_variable x v ctx)
| ([], _) ->
let trace = append_typer_trace i unef in
_eval e ctx trace
| _ -> eval_call loc unef i (_eval e ctx i) vs in
- bindargs e vs (add_rte_variable (Some x) v ctx)
+ bindargs e vs (add_rte_variable x v ctx)
| Vbuiltin (name), args
-> (try let (builtin, arity) = SMap.find name !builtin_functions in
@@ -448,16 +448,16 @@ and eval_call loc unef i f args =
else
let rec buildctx args ctx = match args with
| [] -> ctx
- | arg::args -> buildctx args (add_rte_variable None arg ctx) in
+ | arg::args -> buildctx args (add_rte_variable vdummy arg ctx) in
let rec buildargs n =
if n >= 0
- then (Var ((loc, "<dummy>"), n))::buildargs (n - 1)
+ then (Var (vdummy, n))::buildargs (n - 1)
else [] in
let rec buildbody n =
if n > 0 then
- Lambda ((loc, "<dummy>"), buildbody (n - 1))
+ Lambda (vdummy, buildbody (n - 1))
else Call (Builtin (dloc, name), buildargs (arity - 1)) in
- Closure ("<dummy>",
+ Closure (vdummy,
buildbody (arity - nargs - 1),
buildctx args Myers.nil)
@@ -469,7 +469,7 @@ and eval_call loc unef i f args =
(* We may call a Vlexp e.g. for "x = Map Int String".
* FIXME: The arg will sometimes be a Vlexp but not always, so this is
* really just broken! *)
- -> Vtype (L.mkCall (e, [(Aexplicit, Var ((dummy_location, "?"), -1))]))
+ -> Vtype (L.mkCall (e, [(Aexplicit, Var (vdummy, -1))]))
| _ -> value_fatal loc f "Trying to call a non-function!"
and eval_case ctx i loc target pat dflt =
@@ -489,9 +489,7 @@ and eval_case ctx i loc target pat dflt =
let rec fold2 nctx pats args =
match pats, args with
| pat::pats, arg::args
- -> let nctx = add_rte_variable (match pat with
- | Some (_, name) -> Some name
- | _ -> None) arg nctx in
+ -> let nctx = add_rte_variable pat arg nctx in
fold2 nctx pats args
(* Errors: those should not happen but they might *)
(* List.fold2 would complain. we print more info *)
@@ -506,8 +504,7 @@ and eval_case ctx i loc target pat dflt =
(* Run default *)
with Not_found -> (match dflt with
| Some (var, lxp)
- -> let var' = match var with None -> None | Some (_, n) -> Some n in
- _eval lxp (add_rte_variable var' v ctx) i
+ -> _eval lxp (add_rte_variable var v ctx) i
| _ -> error loc "Match Failure")
and build_arg_list args ctx i =
@@ -515,7 +512,7 @@ and build_arg_list args ctx i =
let arg_val = List.map (fun (k, e) -> _eval e ctx i) args in
(* Add args inside context *)
- List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val
+ List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val
and _eval_decls (decls: (vname * elexp) list)
(ctx: runtime_env) i: runtime_env =
@@ -523,13 +520,13 @@ and _eval_decls (decls: (vname * elexp) list)
let n = (List.length decls) - 1 in
(* Read declarations once and push them *)
- let nctx = List.fold_left (fun ctx ((_, name), _) ->
- add_rte_variable (Some name) Vundefined ctx) ctx decls in
+ let nctx = List.fold_left (fun ctx (name, _) ->
+ add_rte_variable name Vundefined ctx) ctx decls in
- List.iteri (fun idx ((_, name), lxp) ->
+ List.iteri (fun idx (name, lxp) ->
let v = _eval lxp nctx i in
let offset = n - idx in
- ignore (set_rte_variable offset (Some name) v nctx)) decls;
+ ignore (set_rte_variable offset name v nctx)) decls;
nctx
@@ -547,7 +544,8 @@ and sexp_dispatch loc depth args =
it, ctx_it,
flt, ctx_flt,
blk, ctx_blk = match args with
-
+ (* FIXME: Don't match against `Closure` to later use `eval`, instead
+ * pass the value to "funcall". *)
| [sxp; Closure(_, nd, ctx_nd); Closure(_, sym, ctx_sym);
Closure(_, str, ctx_str); Closure(_, it, ctx_it);
Closure(_, flt, ctx_flt); Closure(_, blk, ctx_blk)] ->
@@ -562,32 +560,32 @@ and sexp_dispatch loc depth args =
match sxp with
| Node (op, s) ->(
let rctx = ctx_nd in
- let rctx = add_rte_variable None (Vsexp(op)) rctx in
- let rctx = add_rte_variable None (o2v_list s) rctx in
+ let rctx = add_rte_variable vdummy (Vsexp(op)) rctx in
+ let rctx = add_rte_variable vdummy (o2v_list s) rctx in
match eval nd rctx with
| Closure(_, nd, _) -> eval nd rctx
| _ -> error loc "Node has 2 arguments")
| Symbol (_ , s) ->
let rctx = ctx_sym in
- eval sym (add_rte_variable None (Vstring s) rctx)
+ eval sym (add_rte_variable vdummy (Vstring s) rctx)
| String (_ , s) ->
let rctx = ctx_str in
- eval str (add_rte_variable None (Vstring s) rctx)
+ eval str (add_rte_variable vdummy (Vstring s) rctx)
| Integer (_ , i) ->
let rctx = ctx_it in
- eval it (add_rte_variable None (Vinteger (BI.big_int_of_int i))
+ eval it (add_rte_variable vdummy (Vinteger (BI.big_int_of_int i))
rctx)
| Float (_ , f) ->
let rctx = ctx_flt in
- eval flt (add_rte_variable None (Vfloat f) rctx)
+ eval flt (add_rte_variable vdummy (Vfloat f) rctx)
| Block (_ , _, _) as b ->
(* I think this code breaks what Blocks are. *)
(* We delay parsing but parse with default_stt and default_grammar... *)
(*let toks = Lexer.lex default_stt s in
let s = sexp_parse_all_to_list default_grammar toks (Some ";") in*)
let rctx = ctx_blk in
- eval blk (add_rte_variable None (Vsexp b) rctx)
+ eval blk (add_rte_variable vdummy (Vsexp b) rctx)
| _ ->
print_string "match error\n"; flush stdout;
error loc "sexp_dispatch error"
@@ -653,7 +651,7 @@ and print_eval_trace trace =
print_trace " EVAL TRACE " trace a
let io_bind loc depth args_val =
- let trace_dum = (Var ((loc, "<dummy>"), -1)) in
+ let trace_dum = (Var ((loc, None), -1)) in
match args_val with
| [Vcommand cmd; callback]
@@ -686,14 +684,15 @@ let sys_exit loc depth args_val = match args_val with
let y_operator loc depth args =
match args with
- | [f] -> let aname = "<anon>" in
- let yf_ref = ref Vundefined 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)
+ | [f] -> let yf_ref = ref Vundefined in
+ let fname = (dloc, Some "f") in
+ let yfname = (dloc, Some "yf") in
+ let yf = Closure(vdummy,
+ Call (Var (fname, 1),
+ [Var (yfname, 2);
+ Var (vdummy, 0)]),
+ Myers.cons (fname, ref f)
+ (Myers.cons (yfname, yf_ref)
Myers.nil)) in
yf_ref := yf;
yf
@@ -797,12 +796,6 @@ let eval_all lxps rctx silent =
List.map (fun g -> evalfun g rctx) lxps
-let varname s = match s with Some (_, v) -> v | _ -> "<anon>"
-
-let roname loname = (match (loname : symbol option) with
- | Some (_, name) -> Some name
- | _ -> None)
-
module CMap
(* Memoization table. FIXME: Ideally the keys should be "weak", but
* I haven't found any such functionality in OCaml's libs. *)
@@ -828,7 +821,7 @@ let from_lctx (lctx: lexp_context): runtime_env =
| CVempty -> Myers.nil
| CVlet (loname, def, _, lctx)
-> let rctx = from_lctx lctx in
- Myers.cons (roname loname,
+ Myers.cons (loname,
ref (match def with
| LetDef (_, e)
-> let e = L.clean e in
@@ -847,7 +840,7 @@ let from_lctx (lctx: lexp_context): runtime_env =
let (nrctx, evs, alldefs)
= List.fold_left (fun (rctx, evs, alldefs) (loname, e, _)
-> let rc = ref Vundefined in
- let nrctx = Myers.cons (roname loname, rc) rctx in
+ let nrctx = Myers.cons (loname, rc) rctx in
(nrctx, (e, rc)::evs, alldefs))
(rctx, [], true) defs in
let _ =
=====================================
src/inverse_subst.ml
=====================================
@@ -1,6 +1,6 @@
(* inverse_subst.ml --- Computing the inverse of a substitution
-Copyright (C) 2016-2017 Free Software Foundation, Inc.
+Copyright (C) 2016-2018 Free Software Foundation, Inc.
Author: Vincent Bonnevalle <tiv.crb(a)gmail.com>
@@ -92,7 +92,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s
let counter = ref 0
let mkVar (idx: int) : lexp =
counter := !counter + 1;
- Lexp.mkVar ((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx)
+ Lexp.mkVar ((U.dummy_location, None), idx)
(** Fill the gap between e_i in the list of couple (e_i, i) by adding
dummy variables.
@@ -270,7 +270,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with
mkLet (l, ndefs, apply_inv_subst e s')
| Arrow (ak, v, t1, l, t2)
-> mkArrow (ak, v, apply_inv_subst t1 s, l,
- apply_inv_subst t2 (ssink (maybev v) s))
+ apply_inv_subst t2 (ssink v s))
| Lambda (ak, v, t, e)
-> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s))
| Call (f, args)
@@ -285,7 +285,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink (maybev v) s,
+ -> (ssink v s,
(ak, v, apply_inv_subst t s)
:: nargs))
(s, []) args in
@@ -297,13 +297,13 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with
-> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink (maybev ov) s)
+ (fun s (_,ov) -> ssink ov s)
s cargs in
(l, cargs, apply_inv_subst e s'))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, apply_inv_subst e (ssink (maybev v) s)))
+ | Some (v,e) -> Some (v, apply_inv_subst e (ssink v s)))
| Metavar (id, s', name)
-> match metavar_lookup id with
| MVal e -> apply_inv_subst (push_susp e s') s
=====================================
src/lexp.ml
=====================================
@@ -64,22 +64,22 @@ type ltype = lexp
| Imm of sexp (* Used for strings, ... *)
| SortLevel of sort_level
| Sort of U.location * sort
- | Builtin of vname * ltype * lexp AttributeMap.t option
+ | Builtin of symbol * ltype * lexp AttributeMap.t option
| Var of vref
| Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *)
(* This "Let" allows recursion. *)
| Let of U.location * (vname * lexp * ltype) list * lexp
- | Arrow of arg_kind * vname option * ltype * U.location * lexp
+ | Arrow of arg_kind * vname * ltype * U.location * lexp
| Lambda of arg_kind * vname * ltype * lexp
| Call of lexp * (arg_kind * lexp) list (* Curried call. *)
| Inductive of U.location * label
* ((arg_kind * vname * ltype) list) (* formal Args *)
- * ((arg_kind * vname option * ltype) list) SMap.t
+ * ((arg_kind * vname * ltype) list) SMap.t
| Cons of lexp * symbol (* = Type info * ctor_name *)
| Case of U.location * lexp
* ltype (* The type of the return value of all branches *)
- * (U.location * (arg_kind * vname option) list * lexp) SMap.t
- * (vname option * lexp) option (* Default. *)
+ * (U.location * (arg_kind * vname) list * lexp) SMap.t
+ * (vname * lexp) option (* Default. *)
(* The `subst` only applies to the lexp associated
* with the metavar's "value", not to the ltype. *)
| Metavar of meta_id * subst * vname
@@ -205,10 +205,6 @@ let mkCall (f, es)
| _, [] -> f
| _ -> hc (Call (f, es))
-let var_of_ovar l ov = match ov with
- | None -> (l, "<anon>")
- | Some v -> v
-
(********* Helper functions to use the Subst operations *********)
(* This basically "ties the knot" between Subst and Lexp.
* Maybe it would be cleaner to just move subst.ml into lexp.ml
@@ -257,8 +253,9 @@ let rec lexp_location e =
(********* Normalizing a term *********)
-let vdummy = (U.dummy_location, "<anon>")
-let maybev mv = match mv with None -> vdummy | Some v -> v
+let vdummy = (U.dummy_location, None)
+let maybename n = match n with None -> "<anon>" | Some v -> v
+let sname (l,n) = (l, maybename n)
let rec push_susp e s = (* Push a suspension one level down. *)
match e with
@@ -278,7 +275,7 @@ let rec push_susp e s = (* Push a suspension one level down. *)
-> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in
mkLet (l, loop s defs, mkSusp e s')
| Arrow (ak, v, t1, l, t2)
- -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s))
+ -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink v s))
| Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s))
| Call (f, args) -> mkCall (mkSusp f s,
L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args)
@@ -290,7 +287,7 @@ let rec push_susp e s = (* Push a suspension one level down. *)
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink (maybev v) s,
+ -> (ssink v s,
(ak, v, mkSusp t s)
:: nargs))
(s, []) args in
@@ -302,13 +299,13 @@ let rec push_susp e s = (* Push a suspension one level down. *)
-> mkCase (l, mkSusp e s, mkSusp ret s,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink (maybev ov) s)
+ (fun s (_,ov) -> ssink ov s)
s cargs in
(l, cargs, mkSusp e s'))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, mkSusp e (ssink (maybev v) s)))
+ | Some (v,e) -> Some (v, mkSusp e (ssink v s)))
(* Susp should never appear around Var/Susp/Metavar because mkSusp
* pushes the subst into them eagerly. IOW if there's a Susp(Var..)
* or Susp(Metavar..) it's because some chunk of code should use mkSusp
@@ -342,7 +339,7 @@ let clean e =
(s, []) defs in
mkLet (l, ndefs, clean s' e)
| Arrow (ak, v, t1, l, t2)
- -> mkArrow (ak, v, clean s t1, l, clean (ssink (maybev v) s) t2)
+ -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2)
| Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e)
| Call (f, args) -> mkCall (clean s f,
L.map (fun (ak, arg) -> (ak, clean s arg)) args)
@@ -354,7 +351,7 @@ let clean e =
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink (maybev v) s,
+ -> (ssink v s,
(ak, v, clean s t)
:: nargs))
(s, []) args in
@@ -366,13 +363,13 @@ let clean e =
-> mkCase (l, clean s e, clean s ret,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink (maybev ov) s)
+ (fun s (_,ov) -> ssink ov s)
s cargs in
(l, cargs, clean s' e))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, clean (ssink (maybev v) s) e))
+ | Some (v,e) -> Some (v, clean (ssink v s) e))
| Susp (e, s') -> clean (scompose s' s) e
| Var _ -> if S.identity_p s then e
else clean S.identity (mkSusp e s)
@@ -392,7 +389,8 @@ let rec lexp_unparse lxp =
| Susp _ as e -> lexp_unparse (nosusp e)
| Imm (sexp) -> sexp
| Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name)
- | Var ((loc, name), _) -> Symbol (loc, name)
+ (* FIXME: Add a Sexp syntax for debindex references. *)
+ | Var ((loc, name), _) -> Symbol (loc, maybename name)
| Cons (t, (l, name))
-> Node (sdatacons,
[lexp_unparse t; Symbol (l, name)])
@@ -403,16 +401,16 @@ let rec lexp_unparse lxp =
| Aexplicit -> "lambda_->_"
| Aimplicit -> "lambda_=>_"
| Aerasable -> "lambda_≡>_"),
- [Node (Symbol (l, "_:_"), [Symbol vdef; st]);
+ [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]);
lexp_unparse body])
- | Arrow (arg_kind, vdef, ltp1, loc, ltp2)
+ | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2)
-> let ut1 = lexp_unparse ltp1 in
Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_"
| Aimplicit -> "_=>_"
| Aerasable -> "_≡>_"),
- [(match vdef with None -> ut1
- | Some v -> Node (Symbol (loc, "_:_"),
- [Symbol v; ut1]));
+ [(match oname with None -> ut1
+ | Some v -> Node (Symbol (l, "_:_"),
+ [Symbol (l,v); ut1]));
lexp_unparse ltp2])
| Let (loc, ldecls, body)
@@ -420,9 +418,9 @@ let rec lexp_unparse lxp =
let sdecls = List.fold_left
(fun acc (vdef, lxp, ltp)
-> Node (Symbol (U.dummy_location, "_=_"),
- [Symbol vdef; lexp_unparse ltp])
+ [Symbol (sname vdef); lexp_unparse ltp])
:: Node (Symbol (U.dummy_location, "_=_"),
- [Symbol vdef; lexp_unparse lxp])
+ [Symbol (sname vdef); lexp_unparse lxp])
:: acc)
[] ldecls in
Node (Symbol (loc, "let_in_"),
@@ -437,7 +435,7 @@ let rec lexp_unparse lxp =
(* (arg_kind * vdef * ltype) list *)
(* (arg_kind * pvar * pexp option) list *)
let pfargs = List.map (fun (kind, vdef, ltp) ->
- (kind, vdef, Some (lexp_unparse ltp))) lfargs in
+ (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in
Node (stypecons,
Node (Symbol label, List.map pexp_u_formal_arg pfargs)
@@ -447,9 +445,9 @@ let rec lexp_unparse lxp =
List.map
(fun arg ->
match arg with
- | (Aexplicit, None, t) -> lexp_unparse t
+ | (Aexplicit, (_,None), t) -> lexp_unparse t
| (ak, s, t)
- -> let (l,_) as id = pexp_u_id s in
+ -> let (l,_) as id = sname s in
Node (Symbol (l, match ak with
| Aexplicit -> "_:_"
| Aimplicit -> "_::_"
@@ -462,13 +460,13 @@ let rec lexp_unparse lxp =
let bt = lexp_unparse bltp in
let pbranch = List.map (fun (str, (loc, args, bch)) ->
match args with
- | [] -> Ppatsym (loc, str), lexp_unparse bch
+ | [] -> Ppatsym (loc, Some str), lexp_unparse bch
| _ ->
let pat_args
- = List.map (fun (kind, vdef)
- -> match vdef with
- | Some vdef -> Some vdef, Ppatsym vdef
- | None -> None, Ppatany loc)
+ = List.map (fun (kind, ((l,oname) as name))
+ -> match oname with
+ | Some vdef -> (Some (l,vdef), name)
+ | None -> (None, name))
args
(* FIXME: Rather than a Pcons we'd like to refer to an existing
* binding with that value! *)
@@ -479,9 +477,7 @@ let rec lexp_unparse lxp =
) (SMap.bindings branches) in
let pbranch = match default with
- | Some (v,dft) -> ((match v with
- | None -> Ppatany loc
- | Some vdef -> Ppatsym vdef),
+ | Some (v,dft) -> (Ppatsym v,
lexp_unparse dft)::pbranch
| None -> pbranch
in let e = lexp_unparse target in
@@ -494,7 +490,7 @@ let rec lexp_unparse lxp =
(* FIXME: The cases below are all broken! *)
| Metavar (idx, subst, (loc, name))
- -> Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx
+ -> Symbol (loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx
^ "[" ^ subst_string subst ^ "]")
| SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z")
@@ -630,7 +626,7 @@ let rec get_precedence expr ctx =
| 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 ->
+ | Var ((_, Some name), _) when is_binary_op name ->
lkp (get_binary_op_name name)
| _ -> None, None
@@ -689,7 +685,7 @@ and _lexp_str ctx (exp : lexp) : string =
let get_name fname = match fname with
| Builtin ((_, name), _, _) -> name, 0
- | Var((_, name), idx) -> name, idx
+ | Var((_, Some name), idx) -> name, idx
| Lambda _ -> "__", 0
| Cons _ -> "__", 0
| _ -> "__", -1 in
@@ -703,7 +699,7 @@ and _lexp_str ctx (exp : lexp) : string =
| Susp (e, s) -> _lexp_str ctx (push_susp e s)
- | Var ((loc, name), idx) -> name ^ (index idx) ;
+ | Var ((loc, name), idx) -> maybename name ^ (index idx) ;
| Metavar (idx, subst, (loc, name))
(* print metavar result if any *)
@@ -715,7 +711,7 @@ and _lexp_str ctx (exp : lexp) : string =
| None -> print_meta exp
| Some e when e != exp -> print_meta exp
| _ ->
- "?" ^ name ^ (subst_string subst) ^ (index idx))
+ "?" ^ maybename name ^ (subst_string subst) ^ (index idx))
| Let (_, decls, body) ->
(* Print first decls without indent *)
@@ -736,16 +732,16 @@ and _lexp_str ctx (exp : lexp) : string =
(keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^
(make_indent idt_lvl) ^ (lexp_stri idt_lvl body)
- | Arrow(k, Some (_, name), tp, loc, expr) ->
+ | Arrow(k, (_, Some name), tp, loc, expr) ->
"(" ^ name ^ " : " ^ (lexp_str tp) ^ ") " ^
(kind_str k) ^ " " ^ (lexp_str expr)
- | Arrow(k, None, tp, loc, expr) ->
+ | Arrow(k, (_, None), tp, loc, expr) ->
"(" ^ (lexp_str tp) ^ " "
^ (kind_str k) ^ " " ^ (lexp_str expr) ^ ")"
| Lambda(k, (loc, name), ltype, lbody) ->
- let arg = "(" ^ name ^ " : " ^ (lexp_str ltype) ^ ")" in
+ let arg = "(" ^ maybename name ^ " : " ^ (lexp_str ltype) ^ ")" in
(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^
(make_indent 1) ^ (lexp_stri 1 lbody)
@@ -780,7 +776,7 @@ and _lexp_str ctx (exp : lexp) : string =
-> let args_str
= List.fold_left
(fun str (arg_kind, (_, name), ltype)
- -> str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " "
+ -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " "
^ (lexp_str ltype) ^ ")")
"" args in
@@ -792,8 +788,8 @@ and _lexp_str ctx (exp : lexp) : string =
let arg_str arg
= List.fold_left (fun str v
-> match v with
- | (_ ,None) -> str ^ " _"
- | (_, Some (_, n)) -> str ^ " " ^ n)
+ | (_, (_, None)) -> str ^ " _"
+ | (_, (_, Some n)) -> str ^ " " ^ n)
"" arg in
let str = SMap.fold (fun k (_, arg, exp) str ->
@@ -805,7 +801,8 @@ and _lexp_str ctx (exp : lexp) : string =
| None -> str
| Some (v, df) ->
str ^ nl ^ (make_indent 1)
- ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name)
+ ^ "| " ^ (match v with (_, None) -> "_"
+ | (_, Some name) -> name)
^ " => " ^ (lexp_stri 1 df))
| Builtin ((_, name), _, _) -> "##" ^ name
@@ -845,7 +842,8 @@ and _lexp_str_decls ctx decls =
let ret = List.fold_left
(fun str ((_, name), lxp, ltp)
- -> let str = if pp_type ctx then (type_str name ltp)::str else str in
+ -> let name = maybename name in
+ 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/opslexp.ml
=====================================
@@ -79,19 +79,17 @@ let rec lctx_to_subst lctx =
| DB.CVlet (_, LetDef (_, e), _, lctx)
-> let s = lctx_to_subst lctx in
L.scompose (S.substitute e) s
- | DB.CVlet (ov, _, _, lctx)
+ | DB.CVlet (v, _, _, lctx)
-> let s = lctx_to_subst lctx in
(* Here we decide to keep those vars in the target domain.
* Another option would be to map them to `L.impossible`,
* hence making the target domain be empty (i.e. making the substitution
* generate closed results). *)
- L.ssink (maybev ov) s
+ L.ssink v s
| DB.CVfix (defs, lctx)
-> let s1 = lctx_to_subst lctx in
let s2 = lexp_defs_subst DB.dloc S.identity
- (List.map (fun (oname, e, t)
- -> (maybev oname, e, t))
- (List.rev defs)) in
+ (List.rev defs) in
L.scompose s2 s1
(* Take an expression `e` that is "closed" relatively to context lctx
@@ -246,7 +244,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
t12 t22
| (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2))
-> ak1 == ak2 && (conv_erase || conv_p t1 t2)
- && conv_p' (DB.lexp_ctx_cons ctx (Some l1) Variable t1)
+ && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1)
(set_shift vs')
e1 e2
| (Call (f1, args1), Call (f2, args2))
@@ -275,7 +273,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
SMap.equal (conv_fields ctx vs) cases1 cases2
| ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2)
-> ak1 == ak2 && conv_p' ctx vs t1 t2
- && conv_args (DB.lexp_ctx_cons ctx (Some l1) Variable t1)
+ && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1)
(set_shift vs)
args1 args2
| _,_ -> false in
@@ -422,10 +420,10 @@ let rec check' erased ctx e =
(* FIXME: Check the attributemap as well! *)
t
(* FIXME: Check recursive references. *)
- | Var (((_, name), idx) as v)
+ | Var (((l, name), idx) as v)
-> if DB.set_mem idx erased then
- U.msg_error "TC" (lexp_location e)
- ("Var `" ^ name ^ "`"
+ U.msg_error "TC" l
+ ("Var `" ^ maybename name ^ "`"
^ " can't be used here, because it's `erasable`");
lookup_type ctx v
| Susp (e, s) -> check erased ctx (push_susp e s)
@@ -433,7 +431,7 @@ let rec check' erased ctx e =
-> let _ =
List.fold_left (fun ctx (v, e, t)
-> (let _ = check_type DB.set_empty ctx t in
- DB.lctx_extend ctx (Some v) ForwardRef t))
+ DB.lctx_extend ctx v ForwardRef t))
ctx defs in
(* FIXME: Allow erasable let-bindings! *)
let nerased = DB.set_sink (List.length defs) erased in
@@ -466,9 +464,9 @@ let rec check' erased ctx e =
mkSort (l, StypeOmega)))
| Lambda (ak, ((l,_) as v), t, e)
-> (let _k = check_type DB.set_empty ctx t in
- mkArrow (ak, Some v, t, l,
+ mkArrow (ak, v, t, l,
check (dbset_push ak erased)
- (DB.lctx_extend ctx (Some v) Variable t)
+ (DB.lctx_extend ctx v Variable t)
e))
| Call (f, args)
-> let ft = check erased ctx f in
@@ -526,8 +524,8 @@ let rec check' erased ctx e =
mkSort (l, Stype level)
| (ak, v, t)::args
-> let _k = check_type DB.set_empty ctx t in
- mkArrow (ak, Some v, t, lexp_location t,
- arg_loop (DB.lctx_extend ctx (Some v) Variable t)
+ mkArrow (ak, v, t, lexp_location t,
+ arg_loop (DB.lctx_extend ctx v Variable t)
(dbset_push ak erased)
args) in
let tct = arg_loop ctx erased args in
@@ -562,9 +560,7 @@ let rec check' erased ctx e =
| (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes
-> mkctx (dbset_push ak erased)
(DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s))
- (S.cons (Var ((match vdef with Some vd -> vd
- | None -> (l, "_")),
- 0))
+ (S.cons (Var (vdef, 0))
(S.mkShift s 1))
vdefs fieldtypes
| _,_ -> (U.msg_error "TC" l
@@ -611,7 +607,7 @@ let rec check' erased ctx e =
match fargs with
| [] -> fieldargs fieldtypes
| (ak, ((l,_) as vd), atype) :: fargs
- -> mkArrow (P.Aerasable, Some vd, atype, l,
+ -> mkArrow (P.Aerasable, vd, atype, l,
buildtype fargs) in
buildtype fargs
with Not_found
@@ -773,8 +769,8 @@ let rec get_type ctx e =
| SortResult k -> k
| _ -> mkSort (l, StypeOmega))
| Lambda (ak, ((l,_) as v), t, e)
- -> (mkArrow (ak, Some v, t, l,
- get_type (DB.lctx_extend ctx (Some v) Variable t)
+ -> (mkArrow (ak, v, t, l,
+ get_type (DB.lctx_extend ctx v Variable t)
e))
| Call (f, args)
-> let ft = get_type ctx f in
@@ -814,8 +810,8 @@ let rec get_type ctx e =
cases (mkSortLevel SLz) in
mkSort (l, Stype level)
| (ak, v, t)::args
- -> mkArrow (ak, Some v, t, lexp_location t,
- arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in
+ -> mkArrow (ak, v, t, lexp_location t,
+ arg_loop args (DB.lctx_extend ctx v Variable t)) in
let tct = arg_loop args ctx in
tct
| Case (l, e, ret, branches, default) -> ret
@@ -841,7 +837,7 @@ let rec get_type ctx e =
match fargs with
| [] -> fieldargs fieldtypes
| (ak, ((l,_) as vd), atype) :: fargs
- -> mkArrow (P.Aerasable, Some vd, atype, l,
+ -> mkArrow (P.Aerasable, vd, atype, l,
buildtype fargs) in
buildtype fargs
with Not_found -> DB.type_int)
@@ -959,19 +955,20 @@ let ctx2tup ctx nctx =
SMap.empty),
cons_label),
List.mapi (fun i (oname, t)
- -> (P.Aimplicit, Var (maybev oname, offset - i - 1)))
+ -> (P.Aimplicit, Var (oname, offset - i - 1)))
types)
- | (DB.CVlet (oname, LetDef (_, e), t, _) :: blocs)
- -> Let (loc, [(maybev oname, mkSusp e (S.shift 1), t)],
- mk_lets_and_tup blocs ((oname, t) :: types))
+ | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs)
+ -> Let (loc, [(name, mkSusp e (S.shift 1), t)],
+ mk_lets_and_tup blocs ((name, t) :: types))
| (DB.CVfix (defs, _) :: blocs)
- -> Let (loc, List.map (fun (oname, e, t) -> (maybev oname, e, t)) defs,
+ -> Let (loc, defs,
mk_lets_and_tup blocs (List.append
(List.rev
(List.map (fun (oname, _, t)
-> (oname, t))
defs))
- types)) in
+ types))
+ | _ -> assert false in
mk_lets_and_tup (get_blocs nctx []) []
(* opslexp.ml ends here. *)
=====================================
src/pexp.ml
=====================================
@@ -1,6 +1,6 @@
(* pexp.ml --- Proto lambda-expressions, half-way between Sexp and Lexp.
-Copyright (C) 2011-2017 Free Software Foundation, Inc.
+Copyright (C) 2011-2018 Free Software Foundation, Inc.
Author: Stefan Monnier <monnier(a)iro.umontreal.ca>
Keywords: languages, lisp, dependent types.
@@ -37,31 +37,14 @@ type pvar = symbol
(* type tag = string *)
type ppat =
- (* This data type allows nested patterns, but in reality we don't
- * support them. I.e. we don't want Ppatcons within Ppatcons. *)
- | Ppatany of location
- | Ppatsym of pvar (* A named default pattern, or a 0-ary constructor. *)
- | Ppatcons of sexp * (symbol option * ppat) list
-
-let rec pexp_pat_location e = match e with
- | Ppatany l -> l
+ | Ppatsym of vname (* A named default pattern, or a 0-ary constructor. *)
+ | Ppatcons of sexp * (symbol option * vname) list
+
+let pexp_pat_location e = match e with
| Ppatsym (l,_) -> l
| Ppatcons (e, _) -> sexp_location e
-and pexp_p_formal_arg arg : (arg_kind * pvar * sexp option) =
- match arg with
- | Node (Symbol (_, "_:::_"), [Symbol s; e])
- -> (Aerasable, s, Some e)
- | Node (Symbol (_, "_::_"), [Symbol s; e])
- -> (Aimplicit, s, Some e)
- | Node (Symbol (_, "_:_"), [Symbol s; e])
- -> (Aexplicit, s, Some e)
- | Symbol s -> (Aexplicit, s, None)
- | _ -> sexp_print arg;
- (pexp_error (sexp_location arg) "Unrecognized formal arg");
- (Aexplicit, (sexp_location arg, "{arg}"), None)
-
-and pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) =
+let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) =
match arg with
| (Aexplicit, s, None) -> Symbol s
| (ak, ((l,_) as s), t)
@@ -71,62 +54,29 @@ and pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) =
[Symbol s; match t with Some e -> e
| None -> Symbol (l, "_")])
-and pexp_p_id (x : location * string) : (location * string) option =
- match x with
- | (_, "_") -> None
- | _ -> Some x
-
-and pexp_u_id (x : (location * string) option) : (location * string) =
- match x with
- | None -> (dummy_location, "_")
- | Some x -> x
-
-and pexp_p_ind_arg s = match s with
- | Node (Symbol (_,"_:_"), [Symbol s; t])
- -> (Aexplicit, pexp_p_id s, t)
- | Node (Symbol (_,"_::_"), [Symbol s; t])
- -> (Aimplicit, pexp_p_id s, t)
- | Node (Symbol (_,"_:::_"), [Symbol s; t])
- -> (Aerasable, pexp_p_id s, t)
- | _ -> (Aexplicit, None, s)
-
-and pexp_p_pat_arg (s : sexp) = match s with
- | Symbol _ -> (None, pexp_p_pat s)
- | Node (Symbol (_, "_:=_"), [Symbol f; Symbol s])
- -> (Some f, Ppatsym s)
+let pexp_p_pat_arg (s : sexp) = match s with
+ | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n))
+ | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)])
+ -> (Some f, (l, Some n))
| _ -> let loc = sexp_location s in
pexp_error loc "Unknown pattern arg";
- (None, Ppatany loc)
+ (None, (loc, None))
-and pexp_u_pat_arg (arg : symbol option * ppat) : sexp =
- match arg with
- | (None, p) -> pexp_u_pat p
- | (Some ((l,_) as n), p) ->
- Node (Symbol (l, "_:=_"),
- (* FIXME: the label is wrong! *)
- [Symbol (pexp_u_id (Some n)); pexp_u_pat p])
-
-and pexp_p_pat (s : sexp) : ppat = match s with
- | Symbol (l, "_") -> Ppatany l
- | Symbol s -> Ppatsym s
+let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp =
+ let pname = Symbol (l, match oname with None -> "_" | Some n -> n) in
+ match okn with
+ | None -> pname
+ | Some ((l,_) as n) ->
+ Node (Symbol (l, "_:=_"), [Symbol n; pname])
+
+let pexp_p_pat (s : sexp) : ppat = match s with
+ | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n)
| Node (c, args)
-> Ppatcons (c, List.map pexp_p_pat_arg args)
| _ -> let l = sexp_location s in
- pexp_error l "Unknown pattern"; Ppatany l
+ pexp_error l "Unknown pattern"; Ppatsym (l, None)
-and pexp_u_pat (p : ppat) : sexp = match p with
- | Ppatany l -> Symbol (l, "_")
- | Ppatsym s -> Symbol s
+let pexp_u_pat (p : ppat) : sexp = match p with
+ | Ppatsym (l, None) -> Symbol (l, "_")
+ | Ppatsym (l, Some n) -> Symbol (l, n)
| Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args)
-
-(* String Parsing
- * --------------------------------------------------------- *)
-
-(* Lexp helper *)
-let _pexp_expr_str (str: string) (tenv: token_env)
- (grm: grammar) (limit: string option) =
- _sexp_parse_str str tenv grm limit
-
-(* specialized version *)
-let pexp_expr_str str =
- _pexp_expr_str str default_stt default_grammar (Some ";")
=====================================
src/unification.ml
=====================================
@@ -194,7 +194,7 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type =
-> if var_kind1 = var_kind2
then unify_and (unify' ltype1 ltype2 ctx vs)
(unify' lexp1 lexp2
- (DB.lexp_ctx_cons ctx (Some v1) Variable ltype1)
+ (DB.lexp_ctx_cons ctx v1 Variable ltype1)
(OL.set_shift vs))
else None
| ((Lambda _, Var _)
=====================================
src/util.ml
=====================================
@@ -1,6 +1,6 @@
(* util.ml --- Misc definitions for Typer. -*- coding: utf-8 -*-
-Copyright (C) 2011-2017 Free Software Foundation, Inc.
+Copyright (C) 2011-2018 Free Software Foundation, Inc.
Author: Stefan Monnier <monnier(a)iro.umontreal.ca>
Keywords: languages, lisp, dependent types.
@@ -33,7 +33,7 @@ let dummy_location = {file=""; line=0; column=0}
(* Occurrence of a variable's symbol: we use DeBruijn index, and for
* debugging purposes, we remember the name that was used in the source
* code. *)
-type vname = location * string
+type vname = location * string option
type db_index = int (* DeBruijn index. *)
type db_offset = int (* DeBruijn index offset. *)
type db_revindex = int (* DeBruijn index counting from the root. *)
=====================================
tests/env_test.ml
=====================================
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -45,18 +45,19 @@ let _ = (add_test "ENV" "Set Variables" (fun () ->
if 10 <= (!_global_verbose_lvl) then (
let var = [
- ((Some "a"), DB.type_int, (make_val "a"));
- ((Some "b"), DB.type_int, (make_val "b"));
- ((Some "c"), DB.type_int, (make_val "c"));
- ((Some "d"), DB.type_int, (make_val "d"));
- ((Some "e"), DB.type_int, (make_val "e"));
+ ((dloc, Some "a"), DB.type_int, (make_val "a"));
+ ((dloc, Some "b"), DB.type_int, (make_val "b"));
+ ((dloc, Some "c"), DB.type_int, (make_val "c"));
+ ((dloc, Some "d"), DB.type_int, (make_val "d"));
+ ((dloc, Some "e"), DB.type_int, (make_val "e"));
] in
let n = (List.length var) - 1 in
- let rctx = List.fold_left (fun ctx (n, t, _) ->
- add_rte_variable n Vundefined ctx)
- rctx var in
+ let rctx = List.fold_left
+ (fun ctx (n, t, _) ->
+ add_rte_variable n Vundefined ctx)
+ rctx var in
print_rte_ctx rctx;
=====================================
tests/unify_test.ml
=====================================
@@ -1,6 +1,6 @@
(* unify_test.ml --- Test the unification algorithm
*
- * Copyright (C) 2016-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2016-2018 Free Software Foundation, Inc.
*
* Author: Vincent Bonnevalle <tiv.crb(a)gmail.com>
*
@@ -126,12 +126,12 @@ let input_type_t = generate_ltype_from_str str_type2
let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
( Lambda ((Aexplicit),
- (Util.dummy_location, "L1"),
- Var((Util.dummy_location, "z"), 3),
+ (Util.dummy_location, Some "L1"),
+ Var((Util.dummy_location, Some "z"), 3),
Imm (Integer (Util.dummy_location, 3))),
Lambda ((Aexplicit),
- (Util.dummy_location, "L2"),
- Var((Util.dummy_location, "z"), 4),
+ (Util.dummy_location, Some "L2"),
+ Var((Util.dummy_location, Some "z"), 4),
Imm (Integer (Util.dummy_location, 3))), Nothing )
::(input_induct , input_induct , Equivalent) (* 2 *)
@@ -183,8 +183,8 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
::(input_type , input_type_t , Equivalent) (* 44 *)
- ::(Metavar (0, S.Identity, (Util.dummy_location, "M")),
- Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *)
+ ::(Metavar (0, S.Identity, (Util.dummy_location, Some "M")),
+ Var ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *)
::[]
View it on GitLab: https://gitlab.com/monnier/typer/compare/56e7649d252fa1205c848d22f48761f20f…
--
View it on GitLab: https://gitlab.com/monnier/typer/compare/56e7649d252fa1205c848d22f48761f20f…
You're receiving this email because of your account on gitlab.com.
1
0
Stefan pushed to branch master at Stefan / Typer
Commits:
7896e300 by Stefan Monnier at 2018-06-21T01:28:09Z
Make all variable "names" optional
* src/util.ml (vname): Make the string optional.
Change all `vname option` to `vname`.
- - - - -
15 changed files:
- src/builtin.ml
- src/debruijn.ml
- src/debug_util.ml
- src/elab.ml
- src/elexp.ml
- src/env.ml
- src/eval.ml
- src/inverse_subst.ml
- src/lexp.ml
- src/opslexp.ml
- src/pexp.ml
- src/unification.ml
- src/util.ml
- tests/env_test.ml
- tests/unify_test.ml
Changes:
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -1,6 +1,6 @@
(* builtin.ml --- Infrastructure to define built-in primitives
*
- * Copyright (C) 2016-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2016-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -95,19 +95,19 @@ let set_predef name lexp
(* Builtin types *)
let dloc = DB.dloc
-let op_binary t = mkArrow (Aexplicit, None, t, dloc,
- mkArrow (Aexplicit, None, t, dloc, t))
+let op_binary t = mkArrow (Aexplicit, (dloc, None), t, dloc,
+ mkArrow (Aexplicit, (dloc, None), t, dloc, t))
let type_eq =
- let lv = (dloc, "l") in
- let tv = (dloc, "t") in
- mkArrow (Aerasable, Some lv,
+ let lv = (dloc, Some "l") in
+ let tv = (dloc, Some "t") in
+ mkArrow (Aerasable, lv,
DB.type_level, dloc,
- mkArrow (Aerasable, Some tv,
+ mkArrow (Aerasable, tv,
mkSort (dloc, Stype (Var (lv, 0))), dloc,
- mkArrow (Aexplicit, None,
+ mkArrow (Aexplicit, (dloc, None),
Var (tv, 0), dloc,
- mkArrow (Aexplicit, None,
+ mkArrow (Aexplicit, (dloc, None),
mkVar (tv, 1), dloc,
mkSort (dloc, Stype (Var (lv, 3)))))))
@@ -163,7 +163,8 @@ let register_builtin_csts () =
let register_builtin_types () =
let _ = new_builtin_type "Sexp" DB.type0 in
let _ = new_builtin_type
- "IO" (mkArrow (Aexplicit, None, DB.type0, dloc, DB.type0)) in
+ "IO" (mkArrow (Aexplicit, (dloc, None),
+ DB.type0, dloc, DB.type0)) in
let _ = new_builtin_type "FileHandle" DB.type0 in
let _ = new_builtin_type "Eq" type_eq in
()
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -94,7 +94,7 @@ let type_float = mkBuiltin ((dloc, "Float"), type0, None)
let type_string = mkBuiltin ((dloc, "String"), type0, None)
(* easier to debug with type annotations *)
-type env_elem = (vname option * varbind * ltype)
+type env_elem = (vname * varbind * ltype)
type lexp_context = env_elem M.myers
type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *)
@@ -166,31 +166,24 @@ let lexp_ctx_cons (ctx : lexp_context) d v t =
| _ -> true));
M.cons (d, v, t) ctx
-let lctx_extend (ctx : lexp_context) (def: vname option) (v: varbind) (t: lexp) =
+let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) =
lexp_ctx_cons ctx def v t
let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) =
- let (loc, name) = def in
+ let (loc, oname) = def in
let (grm, (n, map), env, sl) = ctx in
- let nmap = SMap.add name n map in
+ let nmap = match oname with None -> map | Some name -> SMap.add name n map in
(grm, (n + 1, nmap),
- lexp_ctx_cons env (Some def) v t,
+ lexp_ctx_cons env def v t,
sl)
-let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t
-
-let ectx_extend (ectx: elab_context) (def: vname option) (v: varbind) (t: lexp)
- : elab_context =
- match def with
- | None -> let (grm, (n, map), lctx, sl) = ectx in
- (grm, (n + 1, map), lexp_ctx_cons lctx None v t, sl)
- | Some def -> env_extend ectx def v t
+let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t
let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) =
let (ctx, _) =
List.fold_left
(fun (ctx, recursion_offset) (def, e, t) ->
- lexp_ctx_cons ctx (Some def) (LetDef (recursion_offset, e)) t,
+ lexp_ctx_cons ctx def (LetDef (recursion_offset, e)) t,
recursion_offset - 1)
(ctx, List.length defs) defs in
ctx
@@ -198,8 +191,10 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) =
let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) =
let (grm, (n, senv), lctx, sl) = ctx in
let senv', _ = List.fold_left
- (fun (senv, i) ((_, vname), _, _) ->
- SMap.add vname i senv, i + 1)
+ (fun (senv, i) ((_, oname), _, _) ->
+ (match oname with None -> senv
+ | Some name -> SMap.add name i senv),
+ i + 1)
(senv, n) defs in
(grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl)
@@ -236,7 +231,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start =
let names = ref [] in
for i = start to n do
let name = match (M.nth (n - i) lst) with
- | (Some (_, name), _, _) -> name
+ | ((_, Some name), _, _) -> name
| _ -> "" in
names := name::!names
done; !names in
@@ -255,14 +250,13 @@ let print_lexp_ctx_n (ctx : lexp_context) start =
try let r, name, exp, tp =
match env_lookup_by_index (n - idx - 1) ctx with
- | (Some (_, name), LetDef (r, exp), tp) -> r, name, Some exp, tp
- | (Some (_, name), _, tp) -> 0, name, None, tp
- | (_, _, tp) -> 0, "", None, tp in
+ | ((_, name), LetDef (r, exp), tp) -> r, name, Some exp, tp
+ | ((_, name), _, tp) -> 0, name, None, tp in
(* Print env Info *)
lalign_print_int r 4;
print_string " | ";
- lalign_print_string name 10; (* name must match *)
+ lalign_print_string (maybename name) 10; (* name must match *)
print_string " | ";
let _ = match exp with
@@ -296,11 +290,11 @@ let dump_lexp_ctx (ctx : lexp_context) =
(* generic lookup *)
let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =
- let ((loc, ename), dbi) = v in
+ let ((loc, oename), dbi) = v in
try(let ret = (Myers.nth dbi ctx) in
- let _ = match ret with
- | (Some (_, name), _, _) ->
+ let _ = match (ret, oename) with
+ | (((_, Some name), _, _), Some ename) ->
(* Check if names match *)
if not (ename = name) then
(print_lexp_ctx ctx;
@@ -314,7 +308,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =
ret)
with
Not_found -> error loc ("DeBruijn index "
- ^ string_of_int dbi ^ " of `" ^ ename
+ ^ string_of_int dbi ^ " of `" ^ maybename oename
^ "` out of bounds!")
@@ -340,8 +334,8 @@ let env_lookup_expr ctx (v : vref): lexp option =
type lct_view =
| CVempty
- | CVlet of vname option * varbind * ltype * lexp_context
- | CVfix of (vname option * lexp * ltype) list * lexp_context
+ | CVlet of vname * varbind * ltype * lexp_context
+ | CVfix of (vname * lexp * ltype) list * lexp_context
let rec lctx_view lctx =
match lctx with
=====================================
src/debug_util.ml
=====================================
--- a/src/debug_util.ml
+++ b/src/debug_util.ml
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -281,10 +281,10 @@ let main () =
(if (get_p_option "lexp-merge-debug") then(
List.iter (fun ((l, s), lxp, ltp) ->
- lalign_print_string s 20;
+ lalign_print_string (maybename s) 20;
lexp_print ltp; print_string "\n";
- lalign_print_string s 20;
+ lalign_print_string (maybename s) 20;
lexp_print lxp; print_string "\n";
) flexps));
@@ -334,7 +334,7 @@ let main () =
let main = (senv_lookup "main" nctx) in
(* get main body *)
- let body = (get_rte_variable (Some "main") main rctx) in
+ let body = (get_rte_variable (dloc, Some "main") main rctx) in
(* eval main *)
print_eval_result 1 body
=====================================
src/elab.ml
=====================================
--- a/src/elab.ml
+++ b/src/elab.ml
@@ -60,10 +60,6 @@ module Unif = Unification
module OL = Opslexp
module EL = Elexp
-(* Shortcut => Create a Var *)
-let make_var name index loc =
- mkVar (((loc, name), index))
-
(* dummies *)
let dloc = dummy_location
@@ -124,9 +120,9 @@ let elab_check_sort (ctx : elab_context) lsort var ltp =
| _ -> let lexp_string e = lexp_string (L.clean e) in
let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in
match var with
- | None -> lexp_error (lexp_location ltp) ltp
- ("`" ^ typestr ^ "` is not a proper type")
- | Some (l, name)
+ | (l, None) -> lexp_error l ltp
+ ("`" ^ typestr ^ "` is not a proper type")
+ | (l, Some name)
-> lexp_error l ltp
("Type of `" ^ name ^ "` is not a proper type: "
^ typestr)
@@ -136,8 +132,8 @@ let elab_check_proper_type (ctx : elab_context) ltp var =
with e -> print_string "Exception while checking type `";
lexp_print ltp;
(match var with
- | None -> ()
- | Some (_, name)
+ | (_, None) -> ()
+ | (_, Some name)
-> print_string ("` of var `" ^ name ^"`\n"));
print_lexp_ctx (ectx_to_lctx ctx);
raise e
@@ -164,26 +160,26 @@ let elab_check_def (ctx : elab_context) var lxp ltype =
^ lexp_string ltype ^ " and " ^ lexp_string ltype');
raise e)
then
- elab_check_proper_type ctx ltype (Some var)
+ elab_check_proper_type ctx ltype var
else
(EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [
lexp_string lxp ^ " !: " ^ lexp_string ltype;
" because";
lexp_string ltype' ^ " != " ^ lexp_string ltype])
-let ctx_extend (ctx: elab_context) (var : vname option) def ltype =
+let ctx_extend (ctx: elab_context) (var : vname) def ltype =
elab_check_proper_type ctx ltype var;
ectx_extend ctx var def ltype
let ctx_define (ctx: elab_context) var lxp ltype =
elab_check_def ctx var lxp ltype;
- env_extend ctx var (LetDef (0, lxp)) ltype
+ ectx_extend ctx var (LetDef (0, lxp)) ltype
let ctx_define_rec (ctx: elab_context) decls =
let nctx = ectx_extend_rec ctx decls in
let _ = List.fold_left (fun n (var, lxp, ltp)
-> elab_check_proper_type
- nctx (push_susp ltp (S.shift n)) (Some var);
+ nctx (push_susp ltp (S.shift n)) var;
n - 1)
(List.length decls)
decls in
@@ -232,21 +228,22 @@ let ctx_define_rec (ctx: elab_context) decls =
* definitions.
*)
-let newMetavar (ctx : lexp_context) sl l name t=
+let newMetavar (ctx : lexp_context) sl name t =
let meta = Unif.create_metavar ctx sl t in
- mkMetavar (meta, S.Identity, (l, name))
+ mkMetavar (meta, S.Identity, name)
let newMetalevel (ctx : lexp_context) sl loc =
- newMetavar ctx sl Util.dummy_location "ℓ" type_level
+ newMetavar ctx sl (loc, Some "ℓ") type_level
let newMetatype (ctx : lexp_context) sl loc
- = newMetavar ctx sl loc "τ" (mkSort (loc, Stype (newMetalevel ctx sl loc)))
+ = newMetavar ctx sl (loc, Some "τ")
+ (mkSort (loc, Stype (newMetalevel ctx sl loc)))
(* Functions used when we need to return some lexp/ltype but
* an error makes it impossible to return "the right one". *)
let mkDummy_type ctx loc = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc
let mkDummy_check ctx loc t = newMetavar (ectx_to_lctx ctx) dummy_scope_level
- loc "dummy" t
+ (loc, None) t
let mkDummy_infer ctx loc =
let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in
(mkDummy_check ctx loc t, t)
@@ -265,9 +262,10 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context =
| _
-> sexp_error loc "define-operator expects 3 argument"; ctx
-let elab_varref ctx ((loc, name) as id)
+let elab_varref ctx (loc, name)
= let idx = senv_lookup name ctx in
- let lxp = make_var name idx loc in
+ let id = (loc, Some name) in
+ let lxp = mkVar (id, idx) in
let ltp = env_lookup_type ctx (id, idx) in
(lxp, Inferred ltp)
@@ -390,6 +388,9 @@ let generalize (nctx : elab_context) e =
wrap (IMap.mem id nes) vname mt'' l e' in
loop (IMap.empty) len mfvs
+and elab_p_id ((l,name) : symbol) : vname =
+ (l, match name with "_" -> None | _ -> Some name)
+
(* Infer or check, as the case may be. *)
let rec elaborate ctx se ot =
match se with
@@ -440,7 +441,7 @@ and elab_special_form ctx f args ot =
sform_dummy_ret ctx loc
(* Make up an argument of type `t` when none is provided. *)
-and get_implicit_arg ctx loc name t =
+and get_implicit_arg ctx loc oname t =
(* lookup default attribute of t. *)
(* FIXME: Don't lookup defaults/tactics here. Instead, just always
* generate a metavar at this point. The use of defaults/tactics should be
@@ -448,7 +449,7 @@ and get_implicit_arg ctx loc name t =
match
try (* FIXME: We shouldn't hard code as popular a name as `default`. *)
let pidx, pname = (senv_lookup "default" ctx), "default" in
- let default = Var ((dloc, pname), pidx) in
+ let default = Var ((dloc, Some pname), pidx) in
get_attribute ctx loc [default; t]
with Not_found -> None with
| Some attr
@@ -470,17 +471,15 @@ and get_implicit_arg ctx loc name t =
(* Elaborate the argument *)
check lsarg t ctx
- | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc name t
+ | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx)
+ (loc, oname) t
(* Build the list of implicit arguments to instantiate. *)
and instantiate_implicit e t ctx =
let rec instantiate t args =
match OL.lexp_whnf t (ectx_to_lctx ctx) with
- | Arrow ((Aerasable | Aimplicit) as ak, v, t1, _, t2)
- -> let arg = get_implicit_arg
- ctx (lexp_location e)
- (Eval.varname v)
- t1 in
+ | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2)
+ -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in
instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args)
| _ -> (mkCall (e, List.rev args), t)
in instantiate t []
@@ -510,9 +509,9 @@ and infer_type pexp ectx var =
-> (let lexp_string e = lexp_string (L.clean e) in
let typestr = lexp_string t ^ " : " ^ lexp_string s in
match var with
- | None -> lexp_error (lexp_location t) t
- ("`" ^ typestr ^ "` is not a proper type")
- | Some (l, name)
+ | (l, None) -> lexp_error l t
+ ("`" ^ typestr ^ "` is not a proper type")
+ | (l, Some name)
-> lexp_error l t
("Type of `" ^ name ^ "` is not a proper type: "
^ typestr))
@@ -527,10 +526,10 @@ and unify_with_arrow ctx tloc lxp kind var aty
= let arg = match aty with
| None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) tloc
| Some laty -> laty in
- let nctx = ectx_extend ctx (Some var) Variable arg in
+ let nctx = ectx_extend ctx var Variable arg in
let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in
let (l, _) = var in
- let arrow = mkArrow (kind, Some var, arg, l, body) in
+ let arrow = mkArrow (kind, var, arg, l, body) in
match Unif.unify arrow lxp (ectx_to_lctx ctx) with
| None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp
^ " and "
@@ -666,39 +665,34 @@ and check_case rtype (loc, target, ppatterns) ctx =
-> lexp_error loc lctor
"Too many pattern args to the constructor";
make_nctx ctx s [] [] pe acc
- | (_, Ppatcons (p, _))::pargs, cargs
- -> lexp_error (sexp_location p) lctor
- "Nested patterns not supported!";
- make_nctx ctx s pargs cargs pe acc
- | (_, (ak, Some (_, fname), fty)::cargs)
+ | (_, (ak, (_, Some fname), fty)::cargs)
when SMap.mem fname pe
-> let var = SMap.find fname pe in
let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
- make_nctx nctx (ssink (maybev var) s) pargs cargs
+ make_nctx nctx (ssink var s) pargs cargs
(SMap.remove fname pe)
((ak, var)::acc)
- | ((ef, fpat)::pargs, (ak, _, fty)::cargs)
+ | ((ef, var)::pargs, (ak, _, fty)::cargs)
when (match (ef, ak) with
| (Some (_, "_"), _) | (None, Aexplicit) -> true
| _ -> false)
- -> let var = match fpat with Ppatsym v -> Some v | _ -> None in
- let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
- make_nctx nctx (ssink (maybev var) s) pargs cargs pe
+ -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
+ make_nctx nctx (ssink var s) pargs cargs pe
((ak, var)::acc)
- | ((Some (l, fname), fpat)::pargs, cargs)
- -> let var = match fpat with Ppatsym v -> Some v | _ -> None in
- if SMap.mem fname pe then
+ | ((Some (l, fname), var)::pargs, cargs)
+ -> if SMap.mem fname pe then
sexp_error l ("Duplicate explicit field `" ^ fname ^ "`");
make_nctx ctx s pargs cargs (SMap.add fname var pe) acc
| pargs, (ak, fname, fty)::cargs
- -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in
+ -> let var = (loc, None) in
+ let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
if ak = Aexplicit then
sexp_error loc
("Missing pattern for normal field"
- ^ (match fname with Some (_,n) -> " `" ^ n ^ "`"
+ ^ (match fname with (_, Some n) -> " `" ^ n ^ "`"
| _ -> ""));
- make_nctx nctx (ssink vdummy s) pargs cargs pe
- ((ak, None)::acc) in
+ make_nctx nctx (ssink var s) pargs cargs pe
+ ((ak, var)::acc) in
let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in
let rtype' = mkSusp rtype
(S.shift (M.length (ectx_to_lctx nctx)
@@ -712,15 +706,15 @@ and check_case rtype (loc, target, ppatterns) ctx =
in
match pat with
- | Ppatany _ -> add_default None
- | Ppatsym ((_, name) as var)
+ | Ppatsym ((_, None) as var) -> add_default var
+ | Ppatsym ((l, Some name) as var)
-> (try let idx = senv_lookup name ctx in
match OL.lexp_whnf (mkVar (var, idx))
(ectx_to_lctx ctx) with
| Cons _ (* It's indeed a constructor! *)
- -> add_branch (Symbol var) []
- | _ -> add_default (Some var) (* A named default branch. *)
- with Not_found -> add_default (Some var))
+ -> add_branch (Symbol (l, name)) []
+ | _ -> add_default var (* A named default branch. *)
+ with Not_found -> add_default var)
| Ppatcons (pctor, pargs) -> add_branch pctor pargs in
@@ -749,7 +743,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
let rec handle_fun_args largs sargs pending ltp =
let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in
match sargs, ltp' with
- | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type)
+ | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type)
when SMap.mem aname pending
-> let sarg = SMap.find aname pending in
let larg = check sarg arg_type ctx in
@@ -778,7 +772,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
handle_fun_args largs sargs pending ltp
(* Aerasable *)
- | _, Arrow ((Aerasable | Aimplicit) as ak, v, arg_type, _, ret_type)
+ | _, Arrow ((Aerasable | Aimplicit) as ak, (l,v), arg_type, _, ret_type)
(* Don't instantiate after the last explicit arg: the rest is done,
* when needed in infer_and_check (via instantiate_implicit). *)
when not (sargs = [] && SMap.is_empty pending)
@@ -786,8 +780,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
ctx (match sargs with
| [] -> loc
| sarg::_ -> sexp_location sarg)
- (match v with Some (_, name) -> name | _ -> "v")
- arg_type in
+ v arg_type in
handle_fun_args ((ak, larg) :: largs) sargs pending
(L.mkSusp ret_type (S.substitute larg))
| [], _
@@ -808,7 +801,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
| Arrow (ak, _, arg_type, _, ret_type)
-> assert (ak = Aexplicit); (arg_type, ret_type)
| _ -> unify_with_arrow ctx (sexp_location sarg)
- ltp' Aexplicit (dloc, "<anon>") None in
+ ltp' Aexplicit (dloc, None) None in
let larg = check sarg arg_type ctx in
handle_fun_args ((Aexplicit, larg) :: largs) sargs pending
(L.mkSusp ret_type (S.substitute larg)) in
@@ -819,8 +812,8 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
(* Parse inductive type definition. *)
and lexp_parse_inductive ctors ctx =
- let make_args (args:(arg_kind * pvar option * sexp) list) ctx
- : (arg_kind * vname option * ltype) list =
+ let make_args (args:(arg_kind * vname * sexp) list) ctx
+ : (arg_kind * vname * ltype) list =
let nctx = ectx_new_scope ctx in
let rec loop args acc ctx =
match args with
@@ -835,7 +828,7 @@ and lexp_parse_inductive ctors ctx =
acc impossible in
let g = generalize nctx altacc in
let altacc' = g (fun _ne vname t l e
- -> Arrow (Aerasable, Some vname, t, l, e))
+ -> Arrow (Aerasable, vname, t, l, e))
altacc in
if altacc' == altacc
then acc (* No generalization! *)
@@ -845,13 +838,10 @@ and lexp_parse_inductive ctors ctx =
| Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e)
| _ -> assert (e = impossible); [] in
loop altacc'
- | hd::tl -> begin
- match hd with
- | (kind, var, exp) ->
- let lxp = infer_type exp ctx var in
- let nctx = ectx_extend ctx var Variable lxp in
- loop tl ((kind, var, lxp)::acc) nctx
- end in
+ | (kind, var, exp)::tl
+ -> let lxp = infer_type exp ctx var in
+ let nctx = ectx_extend ctx var Variable lxp in
+ loop tl ((kind, var, lxp)::acc) nctx in
loop args [] nctx in
List.fold_left
@@ -868,7 +858,7 @@ and track_fv rctx lctx e =
"a bug"
else let tfv i =
let name = match Myers.nth i rctx with
- | (Some n,_) -> n
+ | ((_, Some n),_) -> n
| _ -> "<anon>" in
match Myers.nth i lctx with
| (_, LetDef (o, e), _)
@@ -910,7 +900,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option)
let args = [macro; BI.o2v_list sargs] in
(* FIXME: Make a proper `Var`. *)
- EV.eval_call loc (EL.Var ((DB.dloc, "expand_macro"), 0)) ([], [])
+ EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) ([], [])
macro_expand args
(* Print each generated decls *)
@@ -934,7 +924,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp =
and lexp_check_decls (ectx : elab_context) (* External context. *)
(nctx : elab_context) (* Context with type declarations. *)
- (defs : (vname * sexp) list)
+ (defs : (symbol * sexp) list)
: (vname * lexp * ltype) list * elab_context =
(* Preserve the new operators added to nctx. *)
let ectx = let (_, a, b, c) = ectx in
@@ -942,7 +932,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *)
(grm, a, b, c) in
let (declmap, nctx)
= List.fold_right
- (fun ((_, vname) as v, pexp) (map, nctx) ->
+ (fun ((l, vname), pexp) (map, nctx) ->
let i = senv_lookup vname nctx in
assert (i < List.length defs);
match Myers.nth i (ectx_to_lctx nctx) with
@@ -951,24 +941,24 @@ and lexp_check_decls (ectx : elab_context) (* External context. *)
let e = check pexp adjusted_t nctx in
let (grm, ec, lc, sl) = nctx in
let d = (v', LetDef (i + 1, e), t) in
- (IMap.add i (v, e, t) map,
+ (IMap.add i ((l, Some vname), e, t) map,
(grm, ec, Myers.set_nth i d lc, sl))
| _ -> U.internal_error "Defining same slot!")
defs (IMap.empty, nctx) in
let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in
decls, ctx_define_rec ectx decls
-and infer_and_generalize_type (ctx : elab_context) se oname =
+and infer_and_generalize_type (ctx : elab_context) se name =
let nctx = ectx_new_scope ctx in
- let t = infer_type se nctx oname in
+ let t = infer_type se nctx name in
match OL.lexp_whnf t (ectx_to_lctx ctx) with
(* There's no point generalizing a single metavar, and it's useful
* to keep it ungeneralized so we can use `x : ?` to declare that
* `x` will be defined later without specifying its type yet. *)
| Metavar _ -> t
| _ -> let g = generalize nctx t in
- g (fun _ne vname t l e
- -> mkArrow (Aerasable, Some vname, t, l, e))
+ g (fun _ne name t l e
+ -> mkArrow (Aerasable, name, t, l, e))
t
and infer_and_generalize_def (ctx : elab_context) se =
@@ -979,9 +969,9 @@ and infer_and_generalize_def (ctx : elab_context) se =
-> mkLambda ((if ne then Aimplicit else Aerasable),
vname, t, e))
e in
- let t' = g (fun ne vname t l e
+ let t' = g (fun ne name t l e
-> mkArrow ((if ne then Aimplicit else Aerasable),
- Some vname, t, sexp_location se, e))
+ name, t, sexp_location se, e))
t in
(e', t')
@@ -990,7 +980,7 @@ and lexp_decls_1
(ectx : elab_context) (* External ctx. *)
(nctx : elab_context) (* New context. *)
(pending_decls : location SMap.t) (* Pending type decls. *)
- (pending_defs : (vname * sexp) list) (* Pending definitions. *)
+ (pending_defs : (symbol * sexp) list) (* Pending definitions. *)
: (vname * lexp * ltype) list * sexp list * elab_context =
match sdecls with
@@ -1011,8 +1001,8 @@ and lexp_decls_1
| Node (Symbol (l, "_:_"), args) :: sdecls
(* FIXME: Move this to a "special form"! *)
-> (match args with
- | [Symbol ((l, vname) as v); stp]
- -> let ltp = infer_and_generalize_type nctx stp (Some v) in
+ | [Symbol (l, vname); stp]
+ -> let ltp = infer_and_generalize_type nctx stp (l, Some vname) in
if SMap.mem vname pending_decls then
(* Don't burp: take'em all and unify! *)
let pt_idx = senv_lookup vname nctx in
@@ -1034,7 +1024,7 @@ and lexp_decls_1
(error l ("Variable `" ^ vname ^ "` already defined!");
lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
else lexp_decls_1 sdecls ectx
- (env_extend nctx v ForwardRef ltp)
+ (ectx_extend nctx (l, Some vname) ForwardRef ltp)
(SMap.add vname l pending_decls)
pending_defs
| _ -> error l "Invalid type declaration syntax";
@@ -1043,16 +1033,17 @@ and lexp_decls_1
| Node (Symbol (l, "_=_") as head, args) :: sdecls
(* FIXME: Move this to a "special form"! *)
-> (match args with
- | [Symbol ((l, vname) as v); sexp]
+ | [Symbol ((l, vname)); sexp]
when SMap.is_empty pending_decls
-> assert (pending_defs == []);
(* Used to be true before we added define-operator. *)
(* assert (ectx == nctx); *)
let (lexp, ltp) = infer_and_generalize_def nctx sexp in
+ let var = (l, Some vname) in
(* Lexp decls are always recursive, so we have to shift by 1 to
* account for the extra var (ourselves). *)
- [(v, mkSusp lexp (S.shift 1), ltp)], sdecls,
- ctx_define nctx v lexp ltp
+ [(var, mkSusp lexp (S.shift 1), ltp)], sdecls,
+ ctx_define nctx var lexp ltp
| [Symbol ((l, vname) as v); sexp]
-> if SMap.mem vname pending_decls then
@@ -1116,7 +1107,7 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp =
and sform_new_attribute ctx loc sargs ot =
match sargs with
- | [t] -> let ltp = infer_type t ctx None in
+ | [t] -> let ltp = infer_type t ctx (loc, None) in
(* FIXME: This creates new values for type `ltp` (very wrong if `ltp`
* is False, for example): Should be a type like `AttributeMap t`
* instead. *)
@@ -1129,7 +1120,7 @@ and sform_new_attribute ctx loc sargs ot =
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
+ | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr
| _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in
let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with
@@ -1145,7 +1136,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot =
and get_attribute ctx loc largs =
let ctx_n = get_size ctx in
let table, var = match largs with
- | [table; Var((_, name), idx)] -> table, (ctx_n - idx, name)
+ | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name)
| _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in
let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with
@@ -1157,7 +1148,8 @@ and get_attribute ctx loc largs =
and sform_dummy_ret ctx loc =
let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in
- (newMetavar (ectx_to_lctx ctx) dummy_scope_level loc "special-form-error" t,
+ (newMetavar (ectx_to_lctx ctx) dummy_scope_level
+ (loc, Some "special-form-error") t,
Inferred t)
and sform_get_attribute ctx loc (sargs : sexp list) ot =
@@ -1168,7 +1160,7 @@ and sform_get_attribute ctx loc (sargs : sexp list) ot =
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)
+ | [table; Var((_, Some name), idx)] -> table, (n - idx, name)
| _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in
let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with
@@ -1229,6 +1221,26 @@ let sform_datacons ctx loc sargs ot =
| _ -> sexp_error loc "##constr requires two arguments";
sform_dummy_ret ctx loc
+let elab_colon_to_ak k = match k with
+ | "_:::_" -> Aerasable
+ | "_::_" -> Aimplicit
+ | _ -> Aexplicit
+
+let elab_datacons_arg s = match s with
+ | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol s; t])
+ -> (elab_colon_to_ak k, elab_p_id s, t)
+ | _ -> (Aexplicit, (sexp_location s, None), s)
+
+let elab_typecons_arg arg : (arg_kind * vname * sexp option) =
+ match arg with
+ | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e])
+ -> (elab_colon_to_ak k,
+ (l, Some name), Some e)
+ | Symbol (l, name) -> (Aexplicit, (l, Some name), None)
+ | _ -> sexp_print arg;
+ (sexp_error (sexp_location arg) "Unrecognized formal arg");
+ (Aexplicit, (sexp_location arg, None), None)
+
let sform_typecons ctx loc sargs ot =
match sargs with
| [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy)
@@ -1245,7 +1257,7 @@ let sform_typecons ctx loc sargs ot =
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 (kind, var, opxp) = elab_typecons_arg sformal in
let ltp = match opxp with
| Some pxp -> let (l,_) = infer pxp ctx in l
| None -> let (l,_) = var in
@@ -1253,7 +1265,7 @@ let sform_typecons ctx loc sargs ot =
(ectx_to_scope_level ctx) l in
parse_formals sformals ((kind, var, ltp) :: rformals)
- (env_extend ctx var Variable ltp) in
+ (ectx_extend ctx var Variable ltp) in
let (formals, nctx) = parse_formals formals [] ctx in
@@ -1263,7 +1275,7 @@ let sform_typecons ctx loc sargs ot =
-> match case with
(* read Constructor name + args => Type ((Symbol * args) list) *)
| Node (Symbol s, cases)
- -> (s, List.map pexp_p_ind_arg cases)::pcases
+ -> (s, List.map elab_datacons_arg cases)::pcases
(* This is a constructor with no args *)
| Symbol s -> (s, [])::pcases
@@ -1277,7 +1289,7 @@ let sform_typecons ctx loc sargs ot =
let sform_hastype ctx loc sargs ot =
match sargs with
- | [se; st] -> let lt = infer_type st ctx None in
+ | [se; st] -> let lt = infer_type st ctx (loc, None) in
let le = check se lt ctx in
(le, Inferred lt)
| _ -> sexp_error loc "##_:_ takes two arguments";
@@ -1287,11 +1299,11 @@ let sform_arrow kind ctx loc sargs ot =
match sargs with
| [st1; st2]
-> let (v, st1) = match st1 with
- | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (Some v, st1)
- | _ -> (None, st1) in
+ | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1)
+ | _ -> ((sexp_location st1, None), st1) in
let lt1 = infer_type st1 ctx v in
let nctx = ectx_extend ctx v Variable lt1 in
- let lt2 = infer_type st2 nctx None in
+ let lt2 = infer_type st2 nctx (sexp_location st2, None) in
(mkArrow (kind, v, lt1, loc, lt2), Lazy)
| _ -> sexp_error loc "##_->_ takes two arguments";
sform_dummy_ret ctx loc
@@ -1343,14 +1355,14 @@ let sform_identifier ctx loc sargs ot =
let subst = S.shift ctx_shift in
let (_, _, rmmap) = ectx_get_scope ctx in
if not (name = "") && SMap.mem name (!rmmap) then
- (mkMetavar (SMap.find name (!rmmap), subst, (loc, name)), Lazy)
+ (mkMetavar (SMap.find name (!rmmap), subst, (loc, Some name)), Lazy)
else
let t = match ot with
| None -> newMetatype octx sl loc
| Some t
(* `t` is defined in ctx instead of octx. *)
-> Inverse_subst.apply_inv_subst t subst in
- let mv = newMetavar octx sl loc name t in
+ let mv = newMetavar octx sl (loc, Some name) t in
(if not (name = "") then
let idx = match mv with
| Metavar (idx, _, _) -> idx
@@ -1379,22 +1391,22 @@ let rec sform_lambda kind ctx loc sargs ot =
match sargs with
| [sarg; sbody]
-> let (arg, ost1) = match sarg with
- | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (arg, Some st)
- | Symbol arg -> (arg, None)
+ | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st)
+ | Symbol arg -> (elab_p_id arg, None)
| _ -> sexp_error (sexp_location sarg)
"Unrecognized lambda argument";
- ((dummy_location, "_"), None) in
+ ((dummy_location, None), None) in
let olt1 = match ost1 with
- | Some st -> Some (infer_type st ctx (Some arg))
+ | Some st -> Some (infer_type st ctx arg)
| _ -> None in
let mklam lt1 olt2 =
- let nctx = env_extend ctx arg Variable lt1 in
+ let nctx = ectx_extend ctx arg Variable lt1 in
let (lbody, alt) = elaborate nctx sbody olt2 in
(mkLambda (kind, arg, lt1, lbody),
match alt with
- | Inferred lt2 -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2))
+ | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2))
| _ -> alt) in
(match ot with
@@ -1416,21 +1428,20 @@ let rec sform_lambda kind ctx loc sargs ot =
^ lexp_string lt1 ^ "`"));
mklam lt1 (Some lt2)
- | Arrow (ak2, ov, lt1, _, lt2) when kind = Aexplicit
+ | Arrow (ak2, v, lt1, _, lt2) when kind = Aexplicit
(* `t` is an implicit arrow and `kind` is Aexplicit,
* so auto-add a corresponding Lambda wrapper!
* FIXME: This should be moved to a macro. *)
- -> let v = var_of_ovar loc ov in
- (* FIXME: Here we end up adding a local variable `v` whose
+ -> (* FIXME: Here we end up adding a local variable `v` whose
* name is lot lexically present, so there's a risk of
* name capture. We should make those vars anonymous? *)
- let nctx = env_extend ctx v Variable lt1 in
+ let nctx = ectx_extend ctx v Variable lt1 in
(* FIXME: Don't go back to sform_lambda, but use an internal
* loop to avoid re-computing olt1 each time. *)
let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in
(mkLambda (ak2, v, lt1, lam),
match alt with
- | Inferred lt2' -> Inferred (mkArrow (ak2, ov, lt1, loc, lt2'))
+ | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2'))
| _ -> alt)
| lt
@@ -1450,7 +1461,7 @@ let rec sform_case ctx loc sargs ot = match sargs with
-> (pexp_p_pat pat, code)
| _ -> let l = (sexp_location branch) in
sexp_error l "Unrecognized simple case branch";
- (Ppatany l, Symbol (l, "?")) in
+ (Ppatsym (l, None), Symbol (l, "?")) in
let pcases = List.map parse_case scases in
let t = match ot with
| Some t -> t
@@ -1563,7 +1574,7 @@ let default_ectx
let register_predefs elctx =
try List.iter (fun name ->
let idx = senv_lookup name elctx in
- let v = Var((dloc, name), idx) in
+ let v = mkVar ((dloc, Some name), idx) in
BI.set_predef name v) BI.predef_names;
with e ->
warning dloc "Predef not found"; in
@@ -1572,7 +1583,7 @@ let default_ectx
let lctx = empty_elab_context in
let lctx = SMap.fold (fun key (e, t) ctx
-> if String.get key 0 = '-' then ctx
- else ctx_define ctx (dloc, key) e t)
+ else ctx_define ctx (dloc, Some key) e t)
(!BI.lmap) lctx in
(* read base file *)
@@ -1600,7 +1611,7 @@ let default_rctx = EV.from_ectx default_ectx
(* Lexp helper *)
let _lexp_expr_str (str: string) (tenv: token_env)
(grm: grammar) (limit: string option) (ctx: elab_context) =
- let pxps = _pexp_expr_str str tenv grm limit in
+ let pxps = _sexp_parse_str str tenv grm limit in
let lexps = lexp_parse_all pxps ctx in
List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp))
lexps;
=====================================
src/elexp.ml
=====================================
--- a/src/elexp.ml
+++ b/src/elexp.ml
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -48,7 +48,7 @@ type elexp =
| Imm of sexp
(* A builtin constant, typically a function implemented in Ocaml. *)
- | Builtin of vname
+ | Builtin of symbol
(* A variable reference, using deBruijn indexing. *)
| Var of vref
@@ -72,8 +72,8 @@ type elexp =
* tests the value of `e`, and either selects the corresponding branch
* in `branches` or branches to the `default`. *)
| Case of U.location * elexp
- * (U.location * (vname option) list * elexp) SMap.t
- * (vname option * elexp) option
+ * (U.location * vname list * elexp) SMap.t
+ * (vname * elexp) option
(* A Type expression. There's no useful operation we can apply to it,
* but they can appear in the code. *)
@@ -109,19 +109,19 @@ and elexp_string lxp =
let maybe_str lxp =
match lxp with
| Some (v, lxp)
- -> " | " ^ (match v with None -> "_" | Some (_,name) -> name)
+ -> " | " ^ (match v with (_, None) -> "_" | (_, Some name) -> name)
^ " => " ^ elexp_string lxp
| None -> "" in
let str_decls d =
List.fold_left (fun str ((_, s), lxp) ->
- str ^ " " ^ s ^ " = " ^ (elexp_string lxp)) "" d in
+ str ^ " " ^ L.maybename s ^ " = " ^ (elexp_string lxp)) "" d in
let str_pat lst =
List.fold_left (fun str v ->
str ^ " " ^ (match v with
- | None -> "_"
- | Some (_, s) -> s)) "" lst in
+ | (_, None) -> "_"
+ | (_, Some s) -> s)) "" lst in
let str_cases c =
SMap.fold (fun key (_, lst, lxp) str ->
@@ -135,10 +135,10 @@ and elexp_string lxp =
match lxp with
| Imm(s) -> sexp_string s
| Builtin((_, s)) -> s
- | Var((_, s), i) -> s ^ "[" ^ string_of_int i ^ "]"
+ | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]"
| Cons((_, s)) -> "datacons(" ^ s ^")"
- | Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_string b)
+ | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b)
| Let(_, d, b) ->
"let" ^ (str_decls d) ^ " in " ^ (elexp_string b)
=====================================
src/env.ml
=====================================
--- a/src/env.ml
+++ b/src/env.ml
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -54,7 +54,7 @@ type value_type =
| Vcons of symbol * value_type list
| Vbuiltin of string
| Vfloat of float
- | Closure of string * elexp * runtime_env
+ | Closure of vname * elexp * runtime_env
| Vsexp of sexp (* Values passed to macros. *)
(* Unable to eval during macro expansion, only throw if the value is used *)
| Vundefined
@@ -64,7 +64,7 @@ type value_type =
| Vcommand of (unit -> value_type)
(* Runtime Environ *)
- and runtime_env = (string option * (value_type ref)) M.myers
+ and runtime_env = (vname * (value_type ref)) M.myers
let rec value_equal a b =
match a, b with
@@ -134,7 +134,7 @@ let rec value_string v =
| Vfloat f -> string_of_float f
| Vsexp s -> sexp_string s
| Vtype e -> L.lexp_string e
- | Closure (s, elexp, _) -> "(lambda " ^ s ^ " -> " ^ (elexp_string elexp) ^ ")"
+ | Closure ((_, s), elexp, _) -> "(lambda " ^ L.maybename s ^ " -> " ^ (elexp_string elexp) ^ ")"
| Vcons ((_, s), lst)
-> let args = List.fold_left
(fun str v -> str ^ " " ^ value_string v)
@@ -147,13 +147,13 @@ let make_runtime_ctx = M.nil
let get_rte_size (ctx: runtime_env): int = M.length ctx
-let get_rte_variable (name: string option) (idx: int)
+let get_rte_variable (name: vname) (idx: int)
(ctx: runtime_env): value_type =
try (
let (defname, ref_cell) = (M.nth idx ctx) in
let x = !ref_cell in
match (defname, name) with
- | (Some n1, Some n2) -> (
+ | ((_, Some n1), (_, Some n2)) -> (
if n1 = n2 then
x
else (
@@ -163,11 +163,11 @@ let get_rte_variable (name: string option) (idx: int)
| _ -> x)
with Not_found ->
- let n = match name with Some n -> n | None -> "" in
+ let n = match name with (_, Some n) -> n | _ -> "" in
error dloc ("Variable lookup failure. Var: \"" ^
n ^ "\" idx: " ^ (str_idx idx))
-let add_rte_variable name (x: value_type) (ctx: runtime_env)
+let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env)
: runtime_env =
let valcell = ref x in
M.cons (name, valcell) ctx
@@ -176,7 +176,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) =
let (n, ref_cell) = (M.nth idx ctx) in
(match (n, name) with
- | Some n1, Some n2
+ | ((_, Some n1), (_, Some n2))
-> if (n1 != n2) then
error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2)
| _ -> ());
@@ -187,7 +187,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) =
let nfirst_rte_var n ctx =
let rec loop i acc =
if i < n then
- loop (i + 1) ((get_rte_variable None i ctx)::acc)
+ loop (i + 1) ((get_rte_variable L.vdummy i ctx)::acc)
else
List.rev acc in
loop 0 []
@@ -214,8 +214,8 @@ let print_rte_ctx_n (ctx: runtime_env) start =
let g = !vref in
let _ =
match n with
- | Some m -> lalign_print_string m 12; print_string " | "
- | None -> print_string (make_line ' ' 12); print_string " | " in
+ | (_, Some m) -> lalign_print_string m 12; print_string " | "
+ | _ -> print_string (make_line ' ' 12); print_string " | " in
value_print g; print_string "\n") start
=====================================
src/eval.ml
=====================================
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -301,7 +301,7 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type
| Imm(Float (_, n)) -> Vfloat n
| Imm(sxp) -> Vsexp sxp
| Cons (label) -> Vcons (label, [])
- | Lambda ((_, n), lxp) -> Closure (n, lxp, ctx)
+ | Lambda (n, lxp) -> Closure (n, lxp, ctx)
| Builtin ((_, str)) -> Vbuiltin str
(* Return a value stored in env *)
@@ -338,11 +338,11 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type
and eval_var ctx lxp v =
- let ((loc, name), idx) = v in
- try get_rte_variable (Some name) (idx) ctx
+ let (name, idx) = v in
+ try get_rte_variable name idx ctx
with e ->
- elexp_fatal loc lxp
- ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")
+ elexp_fatal (fst name) lxp
+ ("Variable: " ^ L.maybename (snd name) ^ (str_idx idx) ^ " was not found ")
(* unef: unevaluated function (to make the trace readable) *)
and eval_call loc unef i f args =
@@ -355,14 +355,14 @@ and eval_call loc unef i f args =
| Closure (x, e, ctx), v::vs
-> let rec bindargs e vs ctx = match (vs, e) with
- | (v::vs, Lambda ((_, x), e))
+ | (v::vs, Lambda (x, e))
(* "Uncurry" on the fly. *)
- -> bindargs e vs (add_rte_variable (Some x) v ctx)
+ -> bindargs e vs (add_rte_variable x v ctx)
| ([], _) ->
let trace = append_typer_trace i unef in
_eval e ctx trace
| _ -> eval_call loc unef i (_eval e ctx i) vs in
- bindargs e vs (add_rte_variable (Some x) v ctx)
+ bindargs e vs (add_rte_variable x v ctx)
| Vbuiltin (name), args
-> (try let (builtin, arity) = SMap.find name !builtin_functions in
@@ -379,16 +379,16 @@ and eval_call loc unef i f args =
else
let rec buildctx args ctx = match args with
| [] -> ctx
- | arg::args -> buildctx args (add_rte_variable None arg ctx) in
+ | arg::args -> buildctx args (add_rte_variable vdummy arg ctx) in
let rec buildargs n =
if n >= 0
- then (Var ((loc, "<dummy>"), n))::buildargs (n - 1)
+ then (Var (vdummy, n))::buildargs (n - 1)
else [] in
let rec buildbody n =
if n > 0 then
- Lambda ((loc, "<dummy>"), buildbody (n - 1))
+ Lambda (vdummy, buildbody (n - 1))
else Call (Builtin (dloc, name), buildargs (arity - 1)) in
- Closure ("<dummy>",
+ Closure (vdummy,
buildbody (arity - nargs - 1),
buildctx args Myers.nil)
@@ -400,7 +400,7 @@ and eval_call loc unef i f args =
(* We may call a Vlexp e.g. for "x = Map Int String".
* FIXME: The arg will sometimes be a Vlexp but not always, so this is
* really just broken! *)
- -> Vtype (L.mkCall (e, [(Aexplicit, Var ((dummy_location, "?"), -1))]))
+ -> Vtype (L.mkCall (e, [(Aexplicit, Var (vdummy, -1))]))
| _ -> value_fatal loc f "Trying to call a non-function!"
and eval_case ctx i loc target pat dflt =
@@ -420,9 +420,7 @@ and eval_case ctx i loc target pat dflt =
let rec fold2 nctx pats args =
match pats, args with
| pat::pats, arg::args
- -> let nctx = add_rte_variable (match pat with
- | Some (_, name) -> Some name
- | _ -> None) arg nctx in
+ -> let nctx = add_rte_variable pat arg nctx in
fold2 nctx pats args
(* Errors: those should not happen but they might *)
(* List.fold2 would complain. we print more info *)
@@ -437,8 +435,7 @@ and eval_case ctx i loc target pat dflt =
(* Run default *)
with Not_found -> (match dflt with
| Some (var, lxp)
- -> let var' = match var with None -> None | Some (_, n) -> Some n in
- _eval lxp (add_rte_variable var' v ctx) i
+ -> _eval lxp (add_rte_variable var v ctx) i
| _ -> error loc "Match Failure")
and build_arg_list args ctx i =
@@ -446,7 +443,7 @@ and build_arg_list args ctx i =
let arg_val = List.map (fun (k, e) -> _eval e ctx i) args in
(* Add args inside context *)
- List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val
+ List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val
and _eval_decls (decls: (vname * elexp) list)
(ctx: runtime_env) i: runtime_env =
@@ -454,13 +451,13 @@ and _eval_decls (decls: (vname * elexp) list)
let n = (List.length decls) - 1 in
(* Read declarations once and push them *)
- let nctx = List.fold_left (fun ctx ((_, name), _) ->
- add_rte_variable (Some name) Vundefined ctx) ctx decls in
+ let nctx = List.fold_left (fun ctx (name, _) ->
+ add_rte_variable name Vundefined ctx) ctx decls in
- List.iteri (fun idx ((_, name), lxp) ->
+ List.iteri (fun idx (name, lxp) ->
let v = _eval lxp nctx i in
let offset = n - idx in
- ignore (set_rte_variable offset (Some name) v nctx)) decls;
+ ignore (set_rte_variable offset name v nctx)) decls;
nctx
@@ -478,7 +475,8 @@ and sexp_dispatch loc depth args =
it, ctx_it,
flt, ctx_flt,
blk, ctx_blk = match args with
-
+ (* FIXME: Don't match against `Closure` to later use `eval`, instead
+ * pass the value to "funcall". *)
| [sxp; Closure(_, nd, ctx_nd); Closure(_, sym, ctx_sym);
Closure(_, str, ctx_str); Closure(_, it, ctx_it);
Closure(_, flt, ctx_flt); Closure(_, blk, ctx_blk)] ->
@@ -493,25 +491,25 @@ and sexp_dispatch loc depth args =
match sxp with
| Node (op, s) ->(
let rctx = ctx_nd in
- let rctx = add_rte_variable None (Vsexp(op)) rctx in
- let rctx = add_rte_variable None (o2v_list s) rctx in
+ let rctx = add_rte_variable vdummy (Vsexp(op)) rctx in
+ let rctx = add_rte_variable vdummy (o2v_list s) rctx in
match eval nd rctx with
| Closure(_, nd, _) -> eval nd rctx
| _ -> error loc "Node has 2 arguments")
| Symbol (_ , s) ->
let rctx = ctx_sym in
- eval sym (add_rte_variable None (Vstring s) rctx)
+ eval sym (add_rte_variable vdummy (Vstring s) rctx)
| String (_ , s) ->
let rctx = ctx_str in
- eval str (add_rte_variable None (Vstring s) rctx)
+ eval str (add_rte_variable vdummy (Vstring s) rctx)
| Integer (_ , i) ->
let rctx = ctx_it in
- eval it (add_rte_variable None (Vinteger (BI.big_int_of_int i))
+ eval it (add_rte_variable vdummy (Vinteger (BI.big_int_of_int i))
rctx)
| Float (_ , f) ->
let rctx = ctx_flt in
- eval flt (add_rte_variable None (Vfloat f) rctx) (*
+ eval flt (add_rte_variable vdummy (Vfloat f) rctx) (*
| Block (_ , s, _) ->
eval blk (add_rte_variable None (o2v_list s)) *)
| _ ->
@@ -579,7 +577,7 @@ and print_eval_trace trace =
print_trace " EVAL TRACE " trace a
let io_bind loc depth args_val =
- let trace_dum = (Var ((loc, "<dummy>"), -1)) in
+ let trace_dum = (Var ((loc, None), -1)) in
match args_val with
| [Vcommand cmd; callback]
@@ -608,14 +606,15 @@ let sys_exit loc depth args_val = match args_val with
let y_operator loc depth args =
match args with
- | [f] -> let aname = "<anon>" in
- let yf_ref = ref Vundefined 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)
+ | [f] -> let yf_ref = ref Vundefined in
+ let fname = (dloc, Some "f") in
+ let yfname = (dloc, Some "yf") in
+ let yf = Closure(vdummy,
+ Call (Var (fname, 1),
+ [Var (yfname, 2);
+ Var (vdummy, 0)]),
+ Myers.cons (fname, ref f)
+ (Myers.cons (yfname, yf_ref)
Myers.nil)) in
yf_ref := yf;
yf
@@ -690,12 +689,6 @@ let eval_all lxps rctx silent =
List.map (fun g -> evalfun g rctx) lxps
-let varname s = match s with Some (_, v) -> v | _ -> "<anon>"
-
-let roname loname = (match (loname : symbol option) with
- | Some (_, name) -> Some name
- | _ -> None)
-
module CMap
(* Memoization table. FIXME: Ideally the keys should be "weak", but
* I haven't found any such functionality in OCaml's libs. *)
@@ -721,7 +714,7 @@ let from_lctx (lctx: lexp_context): runtime_env =
| CVempty -> Myers.nil
| CVlet (loname, def, _, lctx)
-> let rctx = from_lctx lctx in
- Myers.cons (roname loname,
+ Myers.cons (loname,
ref (match def with
| LetDef (_, e)
-> let e = L.clean e in
@@ -740,7 +733,7 @@ let from_lctx (lctx: lexp_context): runtime_env =
let (nrctx, evs, alldefs)
= List.fold_left (fun (rctx, evs, alldefs) (loname, e, _)
-> let rc = ref Vundefined in
- let nrctx = Myers.cons (roname loname, rc) rctx in
+ let nrctx = Myers.cons (loname, rc) rctx in
(nrctx, (e, rc)::evs, alldefs))
(rctx, [], true) defs in
let _ =
=====================================
src/inverse_subst.ml
=====================================
--- a/src/inverse_subst.ml
+++ b/src/inverse_subst.ml
@@ -1,6 +1,6 @@
(* inverse_subst.ml --- Computing the inverse of a substitution
-Copyright (C) 2016-2017 Free Software Foundation, Inc.
+Copyright (C) 2016-2018 Free Software Foundation, Inc.
Author: Vincent Bonnevalle <tiv.crb(a)gmail.com>
@@ -92,7 +92,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s
let counter = ref 0
let mkVar (idx: int) : lexp =
counter := !counter + 1;
- Lexp.mkVar ((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx)
+ Lexp.mkVar ((U.dummy_location, None), idx)
(** Fill the gap between e_i in the list of couple (e_i, i) by adding
dummy variables.
@@ -270,7 +270,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with
mkLet (l, ndefs, apply_inv_subst e s')
| Arrow (ak, v, t1, l, t2)
-> mkArrow (ak, v, apply_inv_subst t1 s, l,
- apply_inv_subst t2 (ssink (maybev v) s))
+ apply_inv_subst t2 (ssink v s))
| Lambda (ak, v, t, e)
-> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s))
| Call (f, args)
@@ -285,7 +285,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink (maybev v) s,
+ -> (ssink v s,
(ak, v, apply_inv_subst t s)
:: nargs))
(s, []) args in
@@ -297,13 +297,13 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with
-> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink (maybev ov) s)
+ (fun s (_,ov) -> ssink ov s)
s cargs in
(l, cargs, apply_inv_subst e s'))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, apply_inv_subst e (ssink (maybev v) s)))
+ | Some (v,e) -> Some (v, apply_inv_subst e (ssink v s)))
| Metavar (id, s', name)
-> match metavar_lookup id with
| MVal e -> apply_inv_subst (push_susp e s') s
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -64,22 +64,22 @@ type ltype = lexp
| Imm of sexp (* Used for strings, ... *)
| SortLevel of sort_level
| Sort of U.location * sort
- | Builtin of vname * ltype * lexp AttributeMap.t option
+ | Builtin of symbol * ltype * lexp AttributeMap.t option
| Var of vref
| Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *)
(* This "Let" allows recursion. *)
| Let of U.location * (vname * lexp * ltype) list * lexp
- | Arrow of arg_kind * vname option * ltype * U.location * lexp
+ | Arrow of arg_kind * vname * ltype * U.location * lexp
| Lambda of arg_kind * vname * ltype * lexp
| Call of lexp * (arg_kind * lexp) list (* Curried call. *)
| Inductive of U.location * label
* ((arg_kind * vname * ltype) list) (* formal Args *)
- * ((arg_kind * vname option * ltype) list) SMap.t
+ * ((arg_kind * vname * ltype) list) SMap.t
| Cons of lexp * symbol (* = Type info * ctor_name *)
| Case of U.location * lexp
* ltype (* The type of the return value of all branches *)
- * (U.location * (arg_kind * vname option) list * lexp) SMap.t
- * (vname option * lexp) option (* Default. *)
+ * (U.location * (arg_kind * vname) list * lexp) SMap.t
+ * (vname * lexp) option (* Default. *)
(* The `subst` only applies to the lexp associated
* with the metavar's "value", not to the ltype. *)
| Metavar of meta_id * subst * vname
@@ -205,10 +205,6 @@ let mkCall (f, es)
| _, [] -> f
| _ -> hc (Call (f, es))
-let var_of_ovar l ov = match ov with
- | None -> (l, "<anon>")
- | Some v -> v
-
(********* Helper functions to use the Subst operations *********)
(* This basically "ties the knot" between Subst and Lexp.
* Maybe it would be cleaner to just move subst.ml into lexp.ml
@@ -257,8 +253,9 @@ let rec lexp_location e =
(********* Normalizing a term *********)
-let vdummy = (U.dummy_location, "<anon>")
-let maybev mv = match mv with None -> vdummy | Some v -> v
+let vdummy = (U.dummy_location, None)
+let maybename n = match n with None -> "<anon>" | Some v -> v
+let sname (l,n) = (l, maybename n)
let rec push_susp e s = (* Push a suspension one level down. *)
match e with
@@ -278,7 +275,7 @@ let rec push_susp e s = (* Push a suspension one level down. *)
-> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in
mkLet (l, loop s defs, mkSusp e s')
| Arrow (ak, v, t1, l, t2)
- -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s))
+ -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink v s))
| Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s))
| Call (f, args) -> mkCall (mkSusp f s,
L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args)
@@ -290,7 +287,7 @@ let rec push_susp e s = (* Push a suspension one level down. *)
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink (maybev v) s,
+ -> (ssink v s,
(ak, v, mkSusp t s)
:: nargs))
(s, []) args in
@@ -302,13 +299,13 @@ let rec push_susp e s = (* Push a suspension one level down. *)
-> mkCase (l, mkSusp e s, mkSusp ret s,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink (maybev ov) s)
+ (fun s (_,ov) -> ssink ov s)
s cargs in
(l, cargs, mkSusp e s'))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, mkSusp e (ssink (maybev v) s)))
+ | Some (v,e) -> Some (v, mkSusp e (ssink v s)))
(* Susp should never appear around Var/Susp/Metavar because mkSusp
* pushes the subst into them eagerly. IOW if there's a Susp(Var..)
* or Susp(Metavar..) it's because some chunk of code should use mkSusp
@@ -342,7 +339,7 @@ let clean e =
(s, []) defs in
mkLet (l, ndefs, clean s' e)
| Arrow (ak, v, t1, l, t2)
- -> mkArrow (ak, v, clean s t1, l, clean (ssink (maybev v) s) t2)
+ -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2)
| Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e)
| Call (f, args) -> mkCall (clean s f,
L.map (fun (ak, arg) -> (ak, clean s arg)) args)
@@ -354,7 +351,7 @@ let clean e =
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink (maybev v) s,
+ -> (ssink v s,
(ak, v, clean s t)
:: nargs))
(s, []) args in
@@ -366,13 +363,13 @@ let clean e =
-> mkCase (l, clean s e, clean s ret,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink (maybev ov) s)
+ (fun s (_,ov) -> ssink ov s)
s cargs in
(l, cargs, clean s' e))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, clean (ssink (maybev v) s) e))
+ | Some (v,e) -> Some (v, clean (ssink v s) e))
| Susp (e, s') -> clean (scompose s' s) e
| Var _ -> if S.identity_p s then e
else clean S.identity (mkSusp e s)
@@ -392,7 +389,8 @@ let rec lexp_unparse lxp =
| Susp _ as e -> lexp_unparse (nosusp e)
| Imm (sexp) -> sexp
| Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name)
- | Var ((loc, name), _) -> Symbol (loc, name)
+ (* FIXME: Add a Sexp syntax for debindex references. *)
+ | Var ((loc, name), _) -> Symbol (loc, maybename name)
| Cons (t, (l, name))
-> Node (sdatacons,
[lexp_unparse t; Symbol (l, name)])
@@ -403,16 +401,16 @@ let rec lexp_unparse lxp =
| Aexplicit -> "lambda_->_"
| Aimplicit -> "lambda_=>_"
| Aerasable -> "lambda_≡>_"),
- [Node (Symbol (l, "_:_"), [Symbol vdef; st]);
+ [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]);
lexp_unparse body])
- | Arrow (arg_kind, vdef, ltp1, loc, ltp2)
+ | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2)
-> let ut1 = lexp_unparse ltp1 in
Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_"
| Aimplicit -> "_=>_"
| Aerasable -> "_≡>_"),
- [(match vdef with None -> ut1
- | Some v -> Node (Symbol (loc, "_:_"),
- [Symbol v; ut1]));
+ [(match oname with None -> ut1
+ | Some v -> Node (Symbol (l, "_:_"),
+ [Symbol (l,v); ut1]));
lexp_unparse ltp2])
| Let (loc, ldecls, body)
@@ -420,9 +418,9 @@ let rec lexp_unparse lxp =
let sdecls = List.fold_left
(fun acc (vdef, lxp, ltp)
-> Node (Symbol (U.dummy_location, "_=_"),
- [Symbol vdef; lexp_unparse ltp])
+ [Symbol (sname vdef); lexp_unparse ltp])
:: Node (Symbol (U.dummy_location, "_=_"),
- [Symbol vdef; lexp_unparse lxp])
+ [Symbol (sname vdef); lexp_unparse lxp])
:: acc)
[] ldecls in
Node (Symbol (loc, "let_in_"),
@@ -437,7 +435,7 @@ let rec lexp_unparse lxp =
(* (arg_kind * vdef * ltype) list *)
(* (arg_kind * pvar * pexp option) list *)
let pfargs = List.map (fun (kind, vdef, ltp) ->
- (kind, vdef, Some (lexp_unparse ltp))) lfargs in
+ (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in
Node (stypecons,
Node (Symbol label, List.map pexp_u_formal_arg pfargs)
@@ -447,9 +445,9 @@ let rec lexp_unparse lxp =
List.map
(fun arg ->
match arg with
- | (Aexplicit, None, t) -> lexp_unparse t
+ | (Aexplicit, (_,None), t) -> lexp_unparse t
| (ak, s, t)
- -> let (l,_) as id = pexp_u_id s in
+ -> let (l,_) as id = sname s in
Node (Symbol (l, match ak with
| Aexplicit -> "_:_"
| Aimplicit -> "_::_"
@@ -462,13 +460,13 @@ let rec lexp_unparse lxp =
let bt = lexp_unparse bltp in
let pbranch = List.map (fun (str, (loc, args, bch)) ->
match args with
- | [] -> Ppatsym (loc, str), lexp_unparse bch
+ | [] -> Ppatsym (loc, Some str), lexp_unparse bch
| _ ->
let pat_args
- = List.map (fun (kind, vdef)
- -> match vdef with
- | Some vdef -> Some vdef, Ppatsym vdef
- | None -> None, Ppatany loc)
+ = List.map (fun (kind, ((l,oname) as name))
+ -> match oname with
+ | Some vdef -> (Some (l,vdef), name)
+ | None -> (None, name))
args
(* FIXME: Rather than a Pcons we'd like to refer to an existing
* binding with that value! *)
@@ -479,9 +477,7 @@ let rec lexp_unparse lxp =
) (SMap.bindings branches) in
let pbranch = match default with
- | Some (v,dft) -> ((match v with
- | None -> Ppatany loc
- | Some vdef -> Ppatsym vdef),
+ | Some (v,dft) -> (Ppatsym v,
lexp_unparse dft)::pbranch
| None -> pbranch
in let e = lexp_unparse target in
@@ -494,7 +490,7 @@ let rec lexp_unparse lxp =
(* FIXME: The cases below are all broken! *)
| Metavar (idx, subst, (loc, name))
- -> Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx
+ -> Symbol (loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx
^ "[" ^ subst_string subst ^ "]")
| SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z")
@@ -630,7 +626,7 @@ let rec get_precedence expr ctx =
| 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 ->
+ | Var ((_, Some name), _) when is_binary_op name ->
lkp (get_binary_op_name name)
| _ -> None, None
@@ -689,7 +685,7 @@ and _lexp_str ctx (exp : lexp) : string =
let get_name fname = match fname with
| Builtin ((_, name), _, _) -> name, 0
- | Var((_, name), idx) -> name, idx
+ | Var((_, Some name), idx) -> name, idx
| Lambda _ -> "__", 0
| Cons _ -> "__", 0
| _ -> "__", -1 in
@@ -703,7 +699,7 @@ and _lexp_str ctx (exp : lexp) : string =
| Susp (e, s) -> _lexp_str ctx (push_susp e s)
- | Var ((loc, name), idx) -> name ^ (index idx) ;
+ | Var ((loc, name), idx) -> maybename name ^ (index idx) ;
| Metavar (idx, subst, (loc, name))
(* print metavar result if any *)
@@ -715,7 +711,7 @@ and _lexp_str ctx (exp : lexp) : string =
| None -> print_meta exp
| Some e when e != exp -> print_meta exp
| _ ->
- "?" ^ name ^ (subst_string subst) ^ (index idx))
+ "?" ^ maybename name ^ (subst_string subst) ^ (index idx))
| Let (_, decls, body) ->
(* Print first decls without indent *)
@@ -736,16 +732,16 @@ and _lexp_str ctx (exp : lexp) : string =
(keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^
(make_indent idt_lvl) ^ (lexp_stri idt_lvl body)
- | Arrow(k, Some (_, name), tp, loc, expr) ->
+ | Arrow(k, (_, Some name), tp, loc, expr) ->
"(" ^ name ^ " : " ^ (lexp_str tp) ^ ") " ^
(kind_str k) ^ " " ^ (lexp_str expr)
- | Arrow(k, None, tp, loc, expr) ->
+ | Arrow(k, (_, None), tp, loc, expr) ->
"(" ^ (lexp_str tp) ^ " "
^ (kind_str k) ^ " " ^ (lexp_str expr) ^ ")"
| Lambda(k, (loc, name), ltype, lbody) ->
- let arg = "(" ^ name ^ " : " ^ (lexp_str ltype) ^ ")" in
+ let arg = "(" ^ maybename name ^ " : " ^ (lexp_str ltype) ^ ")" in
(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^
(make_indent 1) ^ (lexp_stri 1 lbody)
@@ -780,7 +776,7 @@ and _lexp_str ctx (exp : lexp) : string =
-> let args_str
= List.fold_left
(fun str (arg_kind, (_, name), ltype)
- -> str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " "
+ -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " "
^ (lexp_str ltype) ^ ")")
"" args in
@@ -792,8 +788,8 @@ and _lexp_str ctx (exp : lexp) : string =
let arg_str arg
= List.fold_left (fun str v
-> match v with
- | (_ ,None) -> str ^ " _"
- | (_, Some (_, n)) -> str ^ " " ^ n)
+ | (_, (_, None)) -> str ^ " _"
+ | (_, (_, Some n)) -> str ^ " " ^ n)
"" arg in
let str = SMap.fold (fun k (_, arg, exp) str ->
@@ -805,7 +801,8 @@ and _lexp_str ctx (exp : lexp) : string =
| None -> str
| Some (v, df) ->
str ^ nl ^ (make_indent 1)
- ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name)
+ ^ "| " ^ (match v with (_, None) -> "_"
+ | (_, Some name) -> name)
^ " => " ^ (lexp_stri 1 df))
| Builtin ((_, name), _, _) -> "##" ^ name
@@ -845,7 +842,8 @@ and _lexp_str_decls ctx decls =
let ret = List.fold_left
(fun str ((_, name), lxp, ltp)
- -> let str = if pp_type ctx then (type_str name ltp)::str else str in
+ -> let name = maybename name in
+ 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/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -79,19 +79,17 @@ let rec lctx_to_subst lctx =
| DB.CVlet (_, LetDef (_, e), _, lctx)
-> let s = lctx_to_subst lctx in
L.scompose (S.substitute e) s
- | DB.CVlet (ov, _, _, lctx)
+ | DB.CVlet (v, _, _, lctx)
-> let s = lctx_to_subst lctx in
(* Here we decide to keep those vars in the target domain.
* Another option would be to map them to `L.impossible`,
* hence making the target domain be empty (i.e. making the substitution
* generate closed results). *)
- L.ssink (maybev ov) s
+ L.ssink v s
| DB.CVfix (defs, lctx)
-> let s1 = lctx_to_subst lctx in
let s2 = lexp_defs_subst DB.dloc S.identity
- (List.map (fun (oname, e, t)
- -> (maybev oname, e, t))
- (List.rev defs)) in
+ (List.rev defs) in
L.scompose s2 s1
(* Take an expression `e` that is "closed" relatively to context lctx
@@ -246,7 +244,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
t12 t22
| (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2))
-> ak1 == ak2 && (conv_erase || conv_p t1 t2)
- && conv_p' (DB.lexp_ctx_cons ctx (Some l1) Variable t1)
+ && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1)
(set_shift vs')
e1 e2
| (Call (f1, args1), Call (f2, args2))
@@ -275,7 +273,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
SMap.equal (conv_fields ctx vs) cases1 cases2
| ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2)
-> ak1 == ak2 && conv_p' ctx vs t1 t2
- && conv_args (DB.lexp_ctx_cons ctx (Some l1) Variable t1)
+ && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1)
(set_shift vs)
args1 args2
| _,_ -> false in
@@ -422,10 +420,10 @@ let rec check' erased ctx e =
(* FIXME: Check the attributemap as well! *)
t
(* FIXME: Check recursive references. *)
- | Var (((_, name), idx) as v)
+ | Var (((l, name), idx) as v)
-> if DB.set_mem idx erased then
- U.msg_error "TC" (lexp_location e)
- ("Var `" ^ name ^ "`"
+ U.msg_error "TC" l
+ ("Var `" ^ maybename name ^ "`"
^ " can't be used here, because it's `erasable`");
lookup_type ctx v
| Susp (e, s) -> check erased ctx (push_susp e s)
@@ -433,7 +431,7 @@ let rec check' erased ctx e =
-> let _ =
List.fold_left (fun ctx (v, e, t)
-> (let _ = check_type DB.set_empty ctx t in
- DB.lctx_extend ctx (Some v) ForwardRef t))
+ DB.lctx_extend ctx v ForwardRef t))
ctx defs in
(* FIXME: Allow erasable let-bindings! *)
let nerased = DB.set_sink (List.length defs) erased in
@@ -466,9 +464,9 @@ let rec check' erased ctx e =
mkSort (l, StypeOmega)))
| Lambda (ak, ((l,_) as v), t, e)
-> (let _k = check_type DB.set_empty ctx t in
- mkArrow (ak, Some v, t, l,
+ mkArrow (ak, v, t, l,
check (dbset_push ak erased)
- (DB.lctx_extend ctx (Some v) Variable t)
+ (DB.lctx_extend ctx v Variable t)
e))
| Call (f, args)
-> let ft = check erased ctx f in
@@ -526,8 +524,8 @@ let rec check' erased ctx e =
mkSort (l, Stype level)
| (ak, v, t)::args
-> let _k = check_type DB.set_empty ctx t in
- mkArrow (ak, Some v, t, lexp_location t,
- arg_loop (DB.lctx_extend ctx (Some v) Variable t)
+ mkArrow (ak, v, t, lexp_location t,
+ arg_loop (DB.lctx_extend ctx v Variable t)
(dbset_push ak erased)
args) in
let tct = arg_loop ctx erased args in
@@ -562,9 +560,7 @@ let rec check' erased ctx e =
| (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes
-> mkctx (dbset_push ak erased)
(DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s))
- (S.cons (Var ((match vdef with Some vd -> vd
- | None -> (l, "_")),
- 0))
+ (S.cons (Var (vdef, 0))
(S.mkShift s 1))
vdefs fieldtypes
| _,_ -> (U.msg_error "TC" l
@@ -611,7 +607,7 @@ let rec check' erased ctx e =
match fargs with
| [] -> fieldargs fieldtypes
| (ak, ((l,_) as vd), atype) :: fargs
- -> mkArrow (P.Aerasable, Some vd, atype, l,
+ -> mkArrow (P.Aerasable, vd, atype, l,
buildtype fargs) in
buildtype fargs
with Not_found
@@ -773,8 +769,8 @@ let rec get_type ctx e =
| SortResult k -> k
| _ -> mkSort (l, StypeOmega))
| Lambda (ak, ((l,_) as v), t, e)
- -> (mkArrow (ak, Some v, t, l,
- get_type (DB.lctx_extend ctx (Some v) Variable t)
+ -> (mkArrow (ak, v, t, l,
+ get_type (DB.lctx_extend ctx v Variable t)
e))
| Call (f, args)
-> let ft = get_type ctx f in
@@ -814,8 +810,8 @@ let rec get_type ctx e =
cases (mkSortLevel SLz) in
mkSort (l, Stype level)
| (ak, v, t)::args
- -> mkArrow (ak, Some v, t, lexp_location t,
- arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in
+ -> mkArrow (ak, v, t, lexp_location t,
+ arg_loop args (DB.lctx_extend ctx v Variable t)) in
let tct = arg_loop args ctx in
tct
| Case (l, e, ret, branches, default) -> ret
@@ -841,7 +837,7 @@ let rec get_type ctx e =
match fargs with
| [] -> fieldargs fieldtypes
| (ak, ((l,_) as vd), atype) :: fargs
- -> mkArrow (P.Aerasable, Some vd, atype, l,
+ -> mkArrow (P.Aerasable, vd, atype, l,
buildtype fargs) in
buildtype fargs
with Not_found -> DB.type_int)
@@ -958,20 +954,21 @@ let ctx2tup ctx nctx =
types)
SMap.empty),
cons_label),
- List.map (fun (oname, t)
- -> (P.Aimplicit, Var (maybev oname, offset)))
+ List.map (fun (name, t)
+ -> (P.Aimplicit, Var (name, offset)))
types)
- | (DB.CVlet (oname, LetDef (_, e), t, _) :: blocs)
- -> Let (loc, [(maybev oname, mkSusp e (S.shift 1), t)],
- mk_lets_and_tup blocs ((oname, t) :: types))
+ | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs)
+ -> Let (loc, [(name, mkSusp e (S.shift 1), t)],
+ mk_lets_and_tup blocs ((name, t) :: types))
| (DB.CVfix (defs, _) :: blocs)
- -> Let (loc, List.map (fun (oname, e, t) -> (maybev oname, e, t)) defs,
+ -> Let (loc, defs,
mk_lets_and_tup blocs (List.append
(List.rev
(List.map (fun (oname, _, t)
-> (oname, t))
defs))
- types)) in
+ types))
+ | _ -> assert false in
mk_lets_and_tup (get_blocs nctx []) []
(* opslexp.ml ends here. *)
=====================================
src/pexp.ml
=====================================
--- a/src/pexp.ml
+++ b/src/pexp.ml
@@ -1,6 +1,6 @@
(* pexp.ml --- Proto lambda-expressions, half-way between Sexp and Lexp.
-Copyright (C) 2011-2017 Free Software Foundation, Inc.
+Copyright (C) 2011-2018 Free Software Foundation, Inc.
Author: Stefan Monnier <monnier(a)iro.umontreal.ca>
Keywords: languages, lisp, dependent types.
@@ -37,31 +37,14 @@ type pvar = symbol
(* type tag = string *)
type ppat =
- (* This data type allows nested patterns, but in reality we don't
- * support them. I.e. we don't want Ppatcons within Ppatcons. *)
- | Ppatany of location
- | Ppatsym of pvar (* A named default pattern, or a 0-ary constructor. *)
- | Ppatcons of sexp * (symbol option * ppat) list
-
-let rec pexp_pat_location e = match e with
- | Ppatany l -> l
+ | Ppatsym of vname (* A named default pattern, or a 0-ary constructor. *)
+ | Ppatcons of sexp * (symbol option * vname) list
+
+let pexp_pat_location e = match e with
| Ppatsym (l,_) -> l
| Ppatcons (e, _) -> sexp_location e
-and pexp_p_formal_arg arg : (arg_kind * pvar * sexp option) =
- match arg with
- | Node (Symbol (_, "_:::_"), [Symbol s; e])
- -> (Aerasable, s, Some e)
- | Node (Symbol (_, "_::_"), [Symbol s; e])
- -> (Aimplicit, s, Some e)
- | Node (Symbol (_, "_:_"), [Symbol s; e])
- -> (Aexplicit, s, Some e)
- | Symbol s -> (Aexplicit, s, None)
- | _ -> sexp_print arg;
- (pexp_error (sexp_location arg) "Unrecognized formal arg");
- (Aexplicit, (sexp_location arg, "{arg}"), None)
-
-and pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) =
+let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) =
match arg with
| (Aexplicit, s, None) -> Symbol s
| (ak, ((l,_) as s), t)
@@ -71,62 +54,29 @@ and pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) =
[Symbol s; match t with Some e -> e
| None -> Symbol (l, "_")])
-and pexp_p_id (x : location * string) : (location * string) option =
- match x with
- | (_, "_") -> None
- | _ -> Some x
-
-and pexp_u_id (x : (location * string) option) : (location * string) =
- match x with
- | None -> (dummy_location, "_")
- | Some x -> x
-
-and pexp_p_ind_arg s = match s with
- | Node (Symbol (_,"_:_"), [Symbol s; t])
- -> (Aexplicit, pexp_p_id s, t)
- | Node (Symbol (_,"_::_"), [Symbol s; t])
- -> (Aimplicit, pexp_p_id s, t)
- | Node (Symbol (_,"_:::_"), [Symbol s; t])
- -> (Aerasable, pexp_p_id s, t)
- | _ -> (Aexplicit, None, s)
-
-and pexp_p_pat_arg (s : sexp) = match s with
- | Symbol _ -> (None, pexp_p_pat s)
- | Node (Symbol (_, "_:=_"), [Symbol f; Symbol s])
- -> (Some f, Ppatsym s)
+let pexp_p_pat_arg (s : sexp) = match s with
+ | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n))
+ | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)])
+ -> (Some f, (l, Some n))
| _ -> let loc = sexp_location s in
pexp_error loc "Unknown pattern arg";
- (None, Ppatany loc)
+ (None, (loc, None))
-and pexp_u_pat_arg (arg : symbol option * ppat) : sexp =
- match arg with
- | (None, p) -> pexp_u_pat p
- | (Some ((l,_) as n), p) ->
- Node (Symbol (l, "_:=_"),
- (* FIXME: the label is wrong! *)
- [Symbol (pexp_u_id (Some n)); pexp_u_pat p])
-
-and pexp_p_pat (s : sexp) : ppat = match s with
- | Symbol (l, "_") -> Ppatany l
- | Symbol s -> Ppatsym s
+let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp =
+ let pname = Symbol (l, match oname with None -> "_" | Some n -> n) in
+ match okn with
+ | None -> pname
+ | Some ((l,_) as n) ->
+ Node (Symbol (l, "_:=_"), [Symbol n; pname])
+
+let pexp_p_pat (s : sexp) : ppat = match s with
+ | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n)
| Node (c, args)
-> Ppatcons (c, List.map pexp_p_pat_arg args)
| _ -> let l = sexp_location s in
- pexp_error l "Unknown pattern"; Ppatany l
+ pexp_error l "Unknown pattern"; Ppatsym (l, None)
-and pexp_u_pat (p : ppat) : sexp = match p with
- | Ppatany l -> Symbol (l, "_")
- | Ppatsym s -> Symbol s
+let pexp_u_pat (p : ppat) : sexp = match p with
+ | Ppatsym (l, None) -> Symbol (l, "_")
+ | Ppatsym (l, Some n) -> Symbol (l, n)
| Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args)
-
-(* String Parsing
- * --------------------------------------------------------- *)
-
-(* Lexp helper *)
-let _pexp_expr_str (str: string) (tenv: token_env)
- (grm: grammar) (limit: string option) =
- _sexp_parse_str str tenv grm limit
-
-(* specialized version *)
-let pexp_expr_str str =
- _pexp_expr_str str default_stt default_grammar (Some ";")
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -194,7 +194,7 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type =
-> if var_kind1 = var_kind2
then unify_and (unify' ltype1 ltype2 ctx vs)
(unify' lexp1 lexp2
- (DB.lexp_ctx_cons ctx (Some v1) Variable ltype1)
+ (DB.lexp_ctx_cons ctx v1 Variable ltype1)
(OL.set_shift vs))
else None
| ((Lambda _, Var _)
=====================================
src/util.ml
=====================================
--- a/src/util.ml
+++ b/src/util.ml
@@ -1,6 +1,6 @@
(* util.ml --- Misc definitions for Typer. -*- coding: utf-8 -*-
-Copyright (C) 2011-2017 Free Software Foundation, Inc.
+Copyright (C) 2011-2018 Free Software Foundation, Inc.
Author: Stefan Monnier <monnier(a)iro.umontreal.ca>
Keywords: languages, lisp, dependent types.
@@ -33,7 +33,7 @@ let dummy_location = {file=""; line=0; column=0}
(* Occurrence of a variable's symbol: we use DeBruijn index, and for
* debugging purposes, we remember the name that was used in the source
* code. *)
-type vname = location * string
+type vname = location * string option
type db_index = int (* DeBruijn index. *)
type db_offset = int (* DeBruijn index offset. *)
type db_revindex = int (* DeBruijn index counting from the root. *)
=====================================
tests/env_test.ml
=====================================
--- a/tests/env_test.ml
+++ b/tests/env_test.ml
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -45,18 +45,19 @@ let _ = (add_test "ENV" "Set Variables" (fun () ->
if 10 <= (!_global_verbose_lvl) then (
let var = [
- ((Some "a"), DB.type_int, (make_val "a"));
- ((Some "b"), DB.type_int, (make_val "b"));
- ((Some "c"), DB.type_int, (make_val "c"));
- ((Some "d"), DB.type_int, (make_val "d"));
- ((Some "e"), DB.type_int, (make_val "e"));
+ ((dloc, Some "a"), DB.type_int, (make_val "a"));
+ ((dloc, Some "b"), DB.type_int, (make_val "b"));
+ ((dloc, Some "c"), DB.type_int, (make_val "c"));
+ ((dloc, Some "d"), DB.type_int, (make_val "d"));
+ ((dloc, Some "e"), DB.type_int, (make_val "e"));
] in
let n = (List.length var) - 1 in
- let rctx = List.fold_left (fun ctx (n, t, _) ->
- add_rte_variable n Vundefined ctx)
- rctx var in
+ let rctx = List.fold_left
+ (fun ctx (n, t, _) ->
+ add_rte_variable n Vundefined ctx)
+ rctx var in
print_rte_ctx rctx;
=====================================
tests/unify_test.ml
=====================================
--- a/tests/unify_test.ml
+++ b/tests/unify_test.ml
@@ -1,6 +1,6 @@
(* unify_test.ml --- Test the unification algorithm
*
- * Copyright (C) 2016-2017 Free Software Foundation, Inc.
+ * Copyright (C) 2016-2018 Free Software Foundation, Inc.
*
* Author: Vincent Bonnevalle <tiv.crb(a)gmail.com>
*
@@ -126,12 +126,12 @@ let input_type_t = generate_ltype_from_str str_type2
let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
( Lambda ((Aexplicit),
- (Util.dummy_location, "L1"),
- Var((Util.dummy_location, "z"), 3),
+ (Util.dummy_location, Some "L1"),
+ Var((Util.dummy_location, Some "z"), 3),
Imm (Integer (Util.dummy_location, 3))),
Lambda ((Aexplicit),
- (Util.dummy_location, "L2"),
- Var((Util.dummy_location, "z"), 4),
+ (Util.dummy_location, Some "L2"),
+ Var((Util.dummy_location, Some "z"), 4),
Imm (Integer (Util.dummy_location, 3))), Nothing )
::(input_induct , input_induct , Equivalent) (* 2 *)
@@ -183,8 +183,8 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
::(input_type , input_type_t , Equivalent) (* 44 *)
- ::(Metavar (0, S.Identity, (Util.dummy_location, "M")),
- Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *)
+ ::(Metavar (0, S.Identity, (Util.dummy_location, Some "M")),
+ Var ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *)
::[]
View it on GitLab: https://gitlab.com/monnier/typer/commit/7896e300745bccf30ff3514672b43f9a369…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/7896e300745bccf30ff3514672b43f9a369…
You're receiving this email because of your account on gitlab.com.
1
0
Stefan pushed new branch feedback/graveline at Stefan / Typer
--
View it on GitLab: https://gitlab.com/monnier/typer/tree/feedback/graveline
You're receiving this email because of your account on gitlab.com.
1
0