Setepenre pushed to branch master at Stefan / Typer
Commits: a20dd18a by Pierre Delaunay at 2016-11-15T19:46:00-05:00 Modified how properties are handled
* src/lexp.ml - Added a new lexp `AttributeTable` - Modified multiple functions to handle the new lexp * src/lparse.ml - moved special forms implementation from builtin.ml to lparse.ml (circular reference issue) - probably that builtin.ml will be removed soon - finished the implicit arguments lookup * btl/types.typer - called our attribute table simply `Attribute` * src/opslexp.ml: - replace `AttributeTable` by a dummy during type erasure * src/debruijn.ml - removed old property_environment and related functions
- - - - - 766a7745 by Pierre Delaunay at 2016-11-16T14:06:35-05:00 Merging, adapt implicit arg lookup to the new argument reordering algorithm
- - - - - 2fadd29b by Pierre Delaunay at 2016-11-16T14:08:39-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - -
11 changed files:
- btl/types.typer - + samples/bugs.typer - + samples/dependent.typer - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - tests/eval_test.ml
Changes:
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -118,11 +118,17 @@ DMacro_ = inductive-cons Macro DMacro_ ;
expand_macro_ : Macro -> List Sexp -> Sexp; expand_macro_ m args = case m - | Macro_ f => (f args); + | Macro_ f => (f args) + % return first sexp if a DMacro_ is used + | DMacro_ f => (case (f args) + | cons hd tl => hd + | nil => (symbol_ "error"));
expand_dmacro_ : Macro -> List Sexp -> List Sexp; expand_dmacro_ m args = case m - | DMacro_ f => (f args); + | DMacro_ f => (f args) + % Wrap a Macro in a list of Sexp if Macro_ is used + | Macro_ f => cons (a := Sexp) (f args) (nil (a := Sexp));
sexp_dispatch_ = Built-in "sexp_dispatch_" ( (a : Type) ≡> @@ -172,13 +178,15 @@ read = Built-in "read" (FileHandle -> Int -> IO String); % Attributes % -----------------------------------------------------
+% Despite being typed as macro those actually returns lexp. +% not that it matters for the end user Attribute = Built-in "Attribute"; new-attribute = Built-in "new-attribute" Macro; get-attribute = Built-in "get-attribute" Macro; has-attribute = Built-in "has-attribute" Macro; +add-attribute = Built-in "add-attribute" Macro;
-add-attribute = Built-in "add-attribute" (List Sexp -> Sexp); -attribute = Macro_ add-attribute; +% attribute = Macro_ add-attribute;
% ----------------------------------------------------- % Context Accessors
===================================== samples/bugs.typer ===================================== --- /dev/null +++ b/samples/bugs.typer @@ -0,0 +1,8 @@ +x = 2.0; +y = 2; +% This produce the same error +% While I think the first one should say "x" has the wrong type +% and the second should say "Integer::mult expects Integers as arguments" +% i.e `hastype` should force type checking +main = (x : Int) * y; +main = x * y; \ No newline at end of file
===================================== samples/dependent.typer ===================================== --- /dev/null +++ b/samples/dependent.typer @@ -0,0 +1,28 @@ + +Reify = inductive_ (Reify (a : Type)) (RInt (a = Int)) (RFloat (a = Float)) (RString (a = String)); +RInt = inductive-cons Reify RInt; +RFloat = inductive-cons Reify RFloat; +RString = inductive-cons Reify RString; + +float-to-int : Float -> Int; +float-to-int x = 1; + +string-to-int : String -> Int; +string-to-int x = 1; + +get-type : Reify -> Type; +get-type x = case x + | RInt => Int + | RFloat => Float + | RString => String; + +% Here +to-int : (a : Type) ≡> (r : (Reify a)) => (x : a) -> Int; +to-int = lambda a ≡> lambda r = lambda x -> case a + | RInt => x + | RFloat => float-to-int x + | RString => string-to-int x; + +a = to-int (a := Float2) (2.0); +b = to-int (a := String2) "2"; +c = to-int (a := Int2) 2; \ No newline at end of file
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -68,13 +68,13 @@ let get_predef_raw (name: string) : lexp = | Some exp -> exp | None -> error dloc ("""^ name ^ "" was not predefined")
-let get_predef_option (name: string) ctx = +let get_predef_option (name: string) (ctx: DB.elab_context) = let r = (DB.get_size ctx) - !builtin_size - 0 in match !(SMap.find name (!predef_map)) with | Some exp -> Some (mkSusp exp (S.shift r)) | None -> None
-let get_predef (name: string) ctx = +let get_predef (name: string) (ctx: DB.elab_context) = let r = (DB.get_size ctx) - !builtin_size - 0 in let p = get_predef_raw name in (mkSusp p (S.shift r)) @@ -155,43 +155,14 @@ let is_lbuiltin idx ctx = else false
-(* -------------------------------------------------------------------------- - * Built-in Macro - * -------------------------------------------------------------------------- *)
-(* Those are function that are evaluated during lexp_parse *) +let has_attribute_impl loc largs ctx ftype = (*) + let table, attr_name = get_table "has-attribute" largs ctx in + let b = SMap.exists attr_name table in + let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in *) + (get_predef "False" ctx), (get_predef "Bool" ctx)
-let get_attribute_impl loc largs ctx ftype =
- let (vi, vn), (ai, an) = match largs with - | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an) - | _ -> error loc "get-attribute expects two arguments" in - - let lxp = DB.get_property ctx (vi, vn) (ai, an) in - let ltype = match DB.env_lookup_expr ctx ((loc, an), ai) with - | Some ltp -> ltp - | None -> error loc "not expression available" in - - lxp, ltype - -let new_attribute_impl loc largs ctx ftype = - - let eltp = match largs with - | [eltp] -> eltp - | _ -> warning loc "new-attribute expects one argument"; type0 in - - eltp, ftype - -let has_attribute_impl loc largs ctx ftype = - - let (vi, vn), (ai, an) = match largs with - | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an) - | _ -> error loc "has-attribute expects two arguments" in - - let b = DB.has_property ctx (vi, vn) (ai, an) in - - let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in - rvar, (get_predef "Bool" ctx)
let declexpr_impl loc largs ctx ftype =
@@ -217,31 +188,9 @@ let decltype_impl loc largs ctx ftype = (* mkSusp prop (S.shift (var_i + 1)) *) ltype, type0
-let builtin_macro = [ - (* FIXME: These should be functions! *) - ("decltype", decltype_impl); - ("declexpr", declexpr_impl); - (* FIXME: These are not macros but `special-forms`. - * We should add here `let_in_`, `case_`, etc... *) - ("get-attribute", get_attribute_impl); - ("new-attribute", new_attribute_impl); - ("has-attribute", has_attribute_impl); -] - -type macromap = - (location -> lexp list -> DB.elab_context -> lexp -> (lexp * lexp)) SMap.t
-let macro_impl_map : macromap = - List.fold_left (fun map (name, funct) -> - SMap.add name funct map) SMap.empty builtin_macro
-let get_macro_impl loc name = - try SMap.find name macro_impl_map - with Not_found -> error loc ("Builtin macro" ^ name ^ " not found")
-let is_builtin_macro name = - try let _ = SMap.find name macro_impl_map in true - with Not_found -> false
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -83,14 +83,6 @@ let level0 = mkSortLevel SLz let type0 = mkSort (dloc, Stype level0) let dltype = type0
-type property_key = (int * string) (* rev_dbi * Var name *) -module PropertyMap - = Map.Make (struct type t = property_key let compare = compare end) - -(* (* rev_dbi * Var name *) => (name * lexp) *) -type property_elem = lexp PropertyMap.t -type property_env = property_elem PropertyMap.t - (* easier to debug with type annotations *) type env_elem = (db_offset * vdef option * varbind * ltype) type lexp_context = env_elem M.myers @@ -105,11 +97,11 @@ type senv_type = senv_length * scope
(* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) -type elab_context = senv_type * lexp_context * property_env +type elab_context = senv_type * lexp_context
(* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = - let (_, lctx, _) = ectx in lctx + let (_, lctx) = ectx in lctx
(* internal definitions * ---------------------------------- *) @@ -121,15 +113,15 @@ let _make_myers = M.nil (* Public methods: DO USE * ---------------------------------- *)
-let make_elab_context = (_make_senv_type, _make_myers, PropertyMap.empty) +let make_elab_context = (_make_senv_type, _make_myers)
let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof
-let get_size ctx = let ((n, _), _, _) = ctx in n +let get_size ctx = let ((n, _), _) = ctx in n
(* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = - let ((n, map), _, _) = ctx in + let ((n, map), _) = ctx in let raw_idx = n - (SMap.find name map) - 1 in (* if raw_idx > (n - csize) then raw_idx - rof (* Shift if the variable is not bound *) @@ -153,22 +145,21 @@ let lctx_extend (ctx : lexp_context) (def: vdef option) (v: varbind) (t: lexp) =
let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in - let ((n, map), env, f) = ctx in + let ((n, map), env) = ctx in (try let _ = senv_lookup name ctx in warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); let nmap = SMap.add name n map in ((n + 1, nmap), - lexp_ctx_cons env r (Some def) v t, - f) + lexp_ctx_cons env r (Some def) v t)
let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t
let ectx_extend (ectx: elab_context) (def: vdef option) (v: varbind) (t: lexp) : elab_context = match def with - | None -> let ((n, map), lctx, f) = ectx in - ((n + 1, map), lexp_ctx_cons lctx 0 None v t, f) + | None -> let ((n, map), lctx) = ectx in + ((n + 1, map), lexp_ctx_cons lctx 0 None v t) | Some def -> env_extend ectx def v t
let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = @@ -181,12 +172,12 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = ctx
let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = - let ((n, senv), lctx, f) = ctx in + let ((n, senv), lctx) = ctx in let senv', _ = List.fold_left (fun (senv, i) ((_, vname), _, _) -> SMap.add vname i senv, i + 1) (senv, n) defs in - ((n + List.length defs, senv'), lctx_extend_rec lctx defs, f) + ((n + List.length defs, senv'), lctx_extend_rec lctx defs)
let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx @@ -312,83 +303,3 @@ let env_lookup_type ctx (v : vref): lexp = let env_lookup_expr ctx (v : vref): lexp option = lctx_lookup_value (ectx_to_lctx ctx) v
-(* -------------------------------------------------------------------------- *) -(* PropertyMap *) -(* -------------------------------------------------------------------------- *) - - -let add_property ctx (var_i, var_n) (att_i, att_n) (prop: lexp) - : elab_context = - - let (a, b, property_map) = ctx in - let n = get_size ctx in - - (* get_var properties *) - let vmap = try PropertyMap.find (var_i, var_n) property_map - with Not_found -> PropertyMap.empty in - - (* add property *) - let nvmap = PropertyMap.add (n - att_i, att_n) prop vmap in - - (* update properties *) - let property_map = PropertyMap.add (n - var_i, var_n) nvmap property_map in - - (a, b, property_map) - -let get_property ctx (var_i, var_n) (att_i, att_n): lexp = - let (a, b, property_map) = ctx in - let n = get_size ctx in - - (* /!\ input index are reversed or not ? I think not so I shift them *) - let pmap = try PropertyMap.find (n - var_i, var_n) property_map - with Not_found -> - error dummy_location ("Variable "" ^ var_n ^ "" does not have any properties") in - - let prop = try PropertyMap.find (n - att_i, att_n) pmap - with Not_found -> - error dummy_location ("Property "" ^ att_n ^ "" not found") in - mkSusp prop (S.shift (var_i + 1)) - -let has_property ctx (var_i, var_n) (att_i, att_n): bool = - let (a, b, property_map) = ctx in - let n = get_size ctx in - - try - let pmap = PropertyMap.find (n - var_i, var_n) property_map in - let _ = PropertyMap.find (n - att_i, att_n) pmap in - true - with Not_found -> false - - -let dump_properties ctx = - let (a, b, property_map) = ctx in - print_string (make_title " Properties "); - - make_rheader [ - (Some ('l', 10), "V-NAME"); - (Some ('l', 4), "RIDX"); - (Some ('l', 10), "P-NAME"); - (Some ('l', 4), "RIDX"); - (Some ('l', 32), "LEXP")]; - - print_string (make_sep '-'); - - PropertyMap.iter (fun (var_i, var_n) pmap -> - print_string " | "; - lalign_print_string var_n 10; print_string " | "; - ralign_print_int var_i 4; print_string " | "; - let first = ref true in - - PropertyMap.iter (fun (att_i, att_n) lxp -> - (if (!first = false) then - print_string (make_line ' ' 20) - else - first := false); - - lalign_print_string att_n 10; print_string " | "; - ralign_print_int att_i 4; print_string " : "; - lexp_print lxp; print_string "\n") pmap) property_map; - - print_string (make_sep '-'); - -
===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -409,13 +409,9 @@ let main () =
) flexps));
- (if (get_p_option "dump-prop") then( - dump_properties ctx; - print_string "\n")); - (* get typecheck context *) let lctx_to_cctx (lctx: elab_context) = - let (_, env, _) = ctx in env in + let (_, env) = ctx in env in
(if (get_p_option "typecheck") then( print_string (make_title " TYPECHECK ");
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -606,7 +606,7 @@ let varname s = match s with Some (_, v) -> v | _ -> "<anon>"
(* build a rctx from a lctx. *) let from_lctx (ctx: elab_context): runtime_env = - let (_, lctx, _) = ctx in + let (_, lctx) = ctx in let rctx : runtime_env = M.map (fun (_, oname, _, _) -> (match (oname : symbol option) with
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -39,6 +39,9 @@ type vref = U.vref
type label = symbol
+type attribute_key = (int * string) (* rev_dbi * Var name *) +module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) + (*************** Elaboration to Lexp *********************)
(* The scoping of `Let` is tricky: @@ -76,6 +79,8 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * (vdef option * lexp) option (* Default. *) + (* Special property table *) + | AttributeTable of lexp AttributeMap.t * ltype (* The `subst` only applies to the lexp associated * with the metavar's index (i.e. its "value"), not to the ltype. *) | Metavar of int * subst * vdef * ltype @@ -254,6 +259,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s) + | AttributeTable _ -> e
and nosusp e = (* Return `e` with no outermost `Susp`. *) match e with @@ -332,6 +338,7 @@ let lexp_name e = | Inductive _ -> "inductive_" | Builtin _ -> "Builtin" | Susp _ -> "Susp" + | AttributeTable _ -> "AttributeTable" | _ -> "lexp_to_string: not implemented"
(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) @@ -517,6 +524,7 @@ and _lexp_to_str ctx exp = | Aexplicit -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in
match exp with + | AttributeTable _ -> "AttributeTable" | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) | Integer(_, s) -> tval (string_of_int s)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -106,6 +106,10 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr)
+(* Builtin Macro i.e, special forms *) +type macromap = + (location -> lexp list -> elab_context -> lexp -> (lexp * lexp)) SMap.t + let elab_check_proper_type (ctx : elab_context) ltp var = let meta_ctx, _ = !global_substitution in try elab_check_sort ctx (OL.check meta_ctx (ectx_to_lctx ctx) ltp) var ltp @@ -702,12 +706,34 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = let larg = check parg arg_type ctx in handle_fun_args ((Aexplicit, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) - | sarg :: sargs, Arrow (kind, v, arg_type, _, ret_type) + (* Aimplicit, FIXME: use a meta var if a default macro is not provided *) + | sarg :: sargs, Arrow (Aimplicit, v, arg_type, _, ret_type) + -> ((* get default attribute *) + let pidx, pname = (senv_lookup "default" ctx), "default" in + let default = Var((dloc, pname), pidx) in + + (* lookup default attribute of ltp *) + let attr, attr_type = get_attribute_impl loc [default; arg_type] ctx arg_type in + let v = lexp_expand_macro attr [] ctx in + + (* get the sexp returned by the macro *) + let lsarg = match v with + | Vsexp (sexp) -> sexp + | _ -> value_fatal loc v "default attribute should return a sexp" in + + (* lparse the argument *) + let parg = pexp_parse lsarg in + let larg = check parg arg_type ctx in + + handle_fun_args ((Aimplicit, larg) :: largs) (sarg::sargs) pending + (L.mkSusp ret_type (S.substitute larg))) + (* Aerasable *) + | sarg :: sargs, Arrow (Aerasable, v, arg_type, _, ret_type) -> let larg = newMetavar (sexp_location sarg) - (match v with Some (_, name) -> name | _ -> "v") - arg_type in - handle_fun_args ((kind, larg) :: largs) (sarg::sargs) pending - (L.mkSusp ret_type (S.substitute larg)) + (match v with Some (_, name) -> name | _ -> "v") + arg_type in + handle_fun_args ((Aerasable, larg) :: largs) (sarg::sargs) pending + (L.mkSusp ret_type (S.substitute larg))
| sarg :: sargs, t -> print_lexp_ctx (ectx_to_lctx ctx); @@ -740,7 +766,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = | e -> (* Process Arguments. *) let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in - mkCall (body, List.rev largs), ret_type in + mkCall (body, List.rev largs), ret_type in
let handle_macro_call () = let sxp = match lexp_expand_macro body sargs ctx with @@ -808,7 +834,7 @@ and lexp_expand_macro macro_funct sargs ctx and lexp_expand_dmacro macro_funct sargs ctx = lexp_expand_macro_ macro_funct sargs ctx "expand_dmacro_"
-and lexp_expand_macro_ macro_funct sargs ctx expand_fun = +and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type =
(* Build the function to be called *) let macro_expand = get_predef expand_fun ctx in @@ -842,37 +868,19 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = | None -> fatal loc "expression does not exist" in
(* Special Form *) - match mfun with - | Var((_, "add-attribute"), _) ->( - (* Builtin macro *) - let pargs = List.map pexp_parse sargs in - let largs = lexp_parse_all pargs ctx in - - (* extract info *) - let var, att, fn = match largs with - | [Var((_, vn), vi); Var((_, an), ai); fn] -> (vi, vn), (ai, an), fn - | _ -> fatal loc "add-attribute expects 3 args" in - - let ctx = add_property ctx var att fn in - - (* FIXME: We need to have something in lexp to represent this - * add-attribute operation! *) - [], ctx) - - | _ ->( let ret = lexp_expand_dmacro body sargs ctx in
- (* convert typer list to ocaml *) - let decls = tlist2olist [] ret in + (* convert typer list to ocaml *) + let decls = tlist2olist [] ret in
- (* extract sexp from result *) - let decls = List.map (fun g -> - match g with - | Vsexp(sxp) -> sxp - | _ -> value_fatal loc g "Macro expects sexp list") decls in + (* extract sexp from result *) + let decls = List.map (fun g -> + match g with + | Vsexp(sxp) -> sxp + | _ -> value_fatal loc g "Macro expects sexp list") decls in
- (* read as pexp_declaraton *) - pexp_decls_all decls, ctx) + (* read as pexp_declaraton *) + pexp_decls_all decls, ctx with e -> fatal loc ("Macro `" ^ mname ^ "`not found")
@@ -980,6 +988,92 @@ and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list =
(loop p ctx [])
+(* -------------------------------------------------------------------------- + * Built-in Macro: i.e special forms + * -------------------------------------------------------------------------- *) +and builtin_macro = [ + (* FIXME: These should be functions! *) + ("decltype", decltype_impl); + ("declexpr", declexpr_impl); + (* FIXME: These are not macros but `special-forms`. + * We should add here `let_in_`, `case_`, etc... *) + ("get-attribute", get_attribute_impl); + ("new-attribute", new_attribute_impl); + ("has-attribute", has_attribute_impl); + ("add-attribute", add_attribute_impl); +] + +and make_macro_map unit = + List.fold_left (fun map (name, funct) -> + SMap.add name funct map) SMap.empty builtin_macro + +and get_macro_impl loc name = + try SMap.find name (make_macro_map ()) + with Not_found -> fatal loc ("Builtin macro" ^ name ^ " not found") + +and is_builtin_macro name = + try let _ = SMap.find name (make_macro_map ()) in true + with Not_found -> false + +(* -------------------------------------------------------------------------- + * Special form implementation + * -------------------------------------------------------------------------- *) +and new_attribute_impl loc largs ctx ftype = + let ltp = match largs with + | [ltp] -> ltp + | _ -> fatal loc "new-attribute expects a single Type argument" in + + let attr_table_type = type0 in + AttributeTable (AttributeMap.empty, ltp), attr_table_type + +and add_attribute_impl loc largs ctx ftype = + let meta_ctx, _ = !global_substitution in + let n = get_size ctx in + let table, var, attr = match largs with + | [table; Var((_, 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) meta_ctx with + | AttributeTable (map, attr_type) -> map, attr_type + | _ -> fatal loc "add-attribute expects a table as first argument" in + + (* FIXME: Type check (attr: type == attr_type) *) + let attr_table_type = type0 in + AttributeTable (AttributeMap.add var attr map, attr_type), attr_table_type + +and get_attribute_impl loc largs ctx ftype = + let meta_ctx, _ = !global_substitution in + let ctx_n = get_size ctx in + let table, var = match largs with + | [table; Var((_, name), idx)] -> table, (ctx_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) meta_ctx with + | AttributeTable (map, attr_type) -> map, attr_type + | _ -> fatal loc "get-attribute expects a table as first argument" in + + let lxp = AttributeMap.find var map in + let (reverse_idx, _) = var in + (* we need to subst this expression as it was added in an older context *) + (* FIXME: What should be the correct shift *) + let s = 2 in + mkSusp lxp (S.shift s), mkSusp attr_type (S.shift s) + +and has_attribute_impl loc largs ctx ftype = + let meta_ctx, _ = !global_substitution in + let n = get_size ctx in + let table, var = match largs with + | [table; Var((_, 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) meta_ctx with + | AttributeTable (map, attr_type) -> map, attr_type + | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in + + try let _ = AttributeMap.find var map in + (get_predef "True" ctx), (get_predef "Bool" ctx) + with Not_found -> + (get_predef "False" ctx), (get_predef "Bool" ctx)
(* Only print var info *) and lexp_print_var_info ctx =
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -471,11 +471,11 @@ let rec check meta_ctx ctx e = let rec erase_type (lxp: L.lexp): E.elexp =
match lxp with - | L.Imm(s) -> E.Imm(s) - | L.Builtin(v, _) -> E.Builtin(v) - | L.Var(v) -> E.Var(v) - | L.Cons(_, s) -> E.Cons(s) - + | L.Imm(s) -> E.Imm(s) + | L.Builtin(v, _) -> E.Builtin(v) + | L.Var(v) -> E.Var(v) + | L.Cons(_, s) -> E.Cons(s) + | L.AttributeTable _ -> E.Type | L.Lambda (P.Aerasable, _, _, body) -> (* The var shouldn't appear in body, basically, but we need * to adjust the debruijn indices of other vars, hence the subst. *)
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -262,12 +262,13 @@ let _ = test_eval_eqv "w = 2" "declexpr w" "2"
let attr_decl = " w = 2; - greater-than = new-attribute (Int -> Bool); - attribute w greater-than (lambda (y : Int) -> True);" + greater-than = new-attribute (Int -> Int); + greater-than = add-attribute greater-than w (lambda (x : Int) -> x);"
let _ = test_eval_eqv attr_decl - "has-attribute w greater-than" - "True" + "has-attribute greater-than w; + (get-attribute greater-than w) 3;" + "True; 3"
(* This makes sure contexts are reinitialized between calls * i.e the context should not grow *) @@ -356,17 +357,17 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Implicit Arguments"
- "default = new-attribute (Int -> Bool); - attribute Int default (lambda (lst : List Sexp) -> integer_ 1); + "default = new-attribute Macro; + default = add-attribute default Int (Macro_ (lambda (lst : List Sexp) -> integer_ 1));
fun = lambda (x : Int) => lambda (y : Int) -> lambda (z : Int) -> x * y + z;"
"fun 2 1; - fun (z := 1) (y := 2)" + %fun (z := 1) (y := 2)"
- "3; 3" + "3%; 3"
(* run all tests *)
View it on GitLab: https://gitlab.com/monnier/typer/compare/df369e1854b6273b12bb22e2e3418c4a021...
Afficher les réponses par date
- src/lexp.ml
- Added a new lexp `AttributeTable`
- Modified multiple functions to handle the new lexp
- src/lparse.ml
(circular reference issue)
- moved special forms implementation from builtin.ml to lparse.ml
- probably that builtin.ml will be removed soon
- finished the implicit arguments lookup
- btl/types.typer
- called our attribute table simply `Attribute`
- src/opslexp.ml:
- replace `AttributeTable` by a dummy during type erasure
- src/debruijn.ml
- removed old property_environment and related functions
Please write your commit messages in the present tense, i.e. describe what the change *does*. E.g. "Add a new lexp `AttributeTable`".
expand_dmacro_ : Macro -> List Sexp -> List Sexp; expand_dmacro_ m args = case m
- | DMacro_ f => (f args);
- | DMacro_ f => (f args)
- % Wrap a Macro in a list of Sexp if Macro_ is used
- | Macro_ f => cons (a := Sexp) (f args) (nil (a := Sexp));
The (a := Sexp) args shouldn't be needed any more nowadays.
===================================== samples/bugs.typer ===================================== --- /dev/null +++ b/samples/bugs.typer @@ -0,0 +1,8 @@ +x = 2.0; +y = 2; +% This produce the same error +% While I think the first one should say "x" has the wrong type +% and the second should say "Integer::mult expects Integers as arguments" +% i.e `hastype` should force type checking +main = (x : Int) * y; +main = x * y;
I don't know what you mean by "`hastype` should force type checking". But I think the error message will be the same in both cases for the foreseeable future (the type of `*` already tells us the arg is of type `Int` so the hastype makes no difference), and I definitely don't consider this as a bug.
Currently we get
[!] Error LPARSE Type mismatch! Context expected `Int` but expression has type `Float`
with a line+column pointing at the `x` variable. We could improve it by giving the start *and* end of the expression (in this case, the expression is a single char, so it wouldn't help much, but in general it's helpful), and we could improve it by making the "context" a bit more precise (i.e. pass to `Lparse.check` not just the expected type, but some "context description" which in this case could be something like "1st arg of `*`").
\ No newline at end of file
[ Try and terminate your files with newline, as god intended. ]
- | AttributeTable of lexp AttributeMap.t * ltype
You haven't added the corresponding code to all the functions that do `match` on a lexp (e.g. OL.check, OL.whnf, ...), so I'm not sure exactly what is the corresponding intended meaning. Please try and avoid `this pattern-matching is not exhaustive` warnings.
| AttributeTable _ -> e
in push_susp, this looks wrong.
The more I look at it, the more I think AttributeTable should not be a new `lexp` element, but should be a new builtin type, with corresponding built-in functions. This way, we don't need to change whnf, check, and whatnot.
Stefan