Alice de Berny pushed to branch alice at Stefan / Typer
Commits: ed3cbc75 by irradiee at 2020-06-02T12:47:36-04:00 correction sform
- - - - -
1 changed file:
- src/elab.ml
Changes:
===================================== src/elab.ml ===================================== @@ -1366,11 +1366,13 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), Lazy)
-and get_attribute ctx loc largs = - let ctx_n = get_size ctx in - let table, var = match largs with - | [table; (Var((_, Some name), _), idx)] -> table, (ctx_n - idx, name) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in + + and get_attribute ctx loc largs = + let ctx_n = get_size ctx in + let table, var = match largs with + | [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 @@ -1388,9 +1390,10 @@ 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((_, Some 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 = let lp = OL.lexp_whnf table (ectx_to_lctx ctx) in match lexp_lexp' lp with @@ -1400,23 +1403,25 @@ and sform_has_attribute ctx loc (sargs : sexp list) ot =
(BI.o2l_bool ctx (AttributeMap.mem var map), Lazy)
-and sform_declexpr ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [(Var((_, vn), _), vi)] - -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with - | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; - sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; - sform_dummy_ret ctx loc + and sform_declexpr ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [(Var((_, vn), vi), _)] + -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with + | Some lxp -> (lxp, Lazy) + | None -> error ~loc "no expr available"; + sform_dummy_ret ctx loc) + | _ -> error ~loc "declexpr expects one argument"; + sform_dummy_ret ctx loc + + + let sform_decltype ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [(Var((_, vn), vi), _)] + -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) + | _ -> error ~loc "decltype expects one argument"; + sform_dummy_ret ctx loc
-let sform_decltype ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [(Var((_, vn), _), vi)] - -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) - | _ -> error ~loc "decltype expects one argument"; - sform_dummy_ret ctx loc
let builtin_value_types : ltype option SMap.t ref = ref SMap.empty
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ed3cbc752545ab8d132c5623fceb2cef83...