Stefan pushed to branch master at Stefan / Typer

Commits: 2f9ed1b0 by Stefan Monnier at 2018-09-21T02:30:43Z Rename Aexplicit to Anormal

- - - - -

8 changed files:

- src/builtin.ml - src/elab.ml - src/elexp.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - tests/unify_test.ml

Changes:

===================================== src/builtin.ml ===================================== @@ -95,8 +95,8 @@ let set_predef name lexp (* Builtin types *) let dloc = DB.dloc

-let op_binary t = mkArrow (Aexplicit, (dloc, None), t, dloc, - mkArrow (Aexplicit, (dloc, None), t, dloc, t)) +let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, + mkArrow (Anormal, (dloc, None), t, dloc, t))

let type_eq = let lv = (dloc, Some "l") in @@ -105,9 +105,9 @@ let type_eq = DB.type_level, dloc, mkArrow (Aerasable, tv, mkSort (dloc, Stype (Var (lv, 0))), dloc, - mkArrow (Aexplicit, (dloc, None), + mkArrow (Anormal, (dloc, None), Var (tv, 0), dloc, - mkArrow (Aexplicit, (dloc, None), + mkArrow (Anormal, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (Var (lv, 3)))))))

@@ -164,13 +164,13 @@ let register_builtin_csts () = let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in let _ = new_builtin_type - "IO" (mkArrow (Aexplicit, (dloc, None), + "IO" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type - "Ref" (mkArrow (Aexplicit, (dloc, None), + "Ref" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type - "Array" (mkArrow (Aexplicit, (dloc, None), + "Array" (mkArrow (Anormal, (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/elab.ml ===================================== @@ -700,7 +700,7 @@ and check_case rtype (loc, target, ppatterns) ctx = ((ak, var)::acc) | ((ef, var)::pargs, (ak, _, fty)::cargs) when (match (ef, ak) with - | (Some (_, "_"), _) | (None, Aexplicit) -> true + | (Some (_, "_"), _) | (None, Anormal) -> true | _ -> false) -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in make_nctx nctx (ssink var s) pargs cargs pe @@ -712,7 +712,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | pargs, (ak, fname, fty)::cargs -> let var = (loc, None) in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in - if ak = Aexplicit then + if ak = Anormal then sexp_error loc ("Missing pattern for normal field" ^ (match fname with (_, Some n) -> " `" ^ n ^ "`" @@ -825,11 +825,11 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | sarg :: sargs, _ -> let (arg_type, ret_type) = match ltp' with | Arrow (ak, _, arg_type, _, ret_type) - -> assert (ak = Aexplicit); (arg_type, ret_type) + -> assert (ak = Anormal); (arg_type, ret_type) | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Aexplicit (dloc, None) None in + ltp' Anormal (dloc, None) None in let larg = check sarg arg_type ctx in - handle_fun_args ((Aexplicit, larg) :: largs) sargs pending + handle_fun_args ((Anormal, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) in

let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in @@ -1260,22 +1260,22 @@ let sform_datacons ctx loc sargs ot = let elab_colon_to_ak k = match k with | "_:::_" -> Aerasable | "_::_" -> Aimplicit - | _ -> Aexplicit + | _ -> Anormal

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) + | _ -> (Anormal, (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) + | Symbol (l, name) -> (Anormal, (l, Some name), None) | _ -> sexp_print arg; (sexp_error (sexp_location arg) "Unrecognized formal arg"); - (Aexplicit, (sexp_location arg, None), None) + (Anormal, (sexp_location arg, None), None)

let sform_typecons ctx loc sargs ot = match sargs with @@ -1459,8 +1459,8 @@ let rec sform_lambda kind ctx loc sargs ot = ^ lexp_string lt1 ^ "`")); mklam lt1 (Some lt2)

- | Arrow (ak2, v, lt1, _, lt2) when kind = Aexplicit - (* `t` is an implicit arrow and `kind` is Aexplicit, + | Arrow (ak2, v, lt1, _, lt2) when kind = Anormal + (* `t` is an implicit arrow and `kind` is Anormal, * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) -> (* FIXME: Here we end up adding a local variable `v` whose @@ -1479,7 +1479,7 @@ let rec sform_lambda kind ctx loc sargs ot = -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 in mklam lt1 (Some lt2))

- | _ -> sexp_error loc ("##lambda_"^(match kind with Aexplicit -> "->" + | _ -> sexp_error loc ("##lambda_"^(match kind with Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>") ^"_ takes two arguments"); @@ -1620,10 +1620,10 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); - ("lambda_->_", sform_lambda Aexplicit); + ("lambda_->_", sform_lambda Anormal); ("lambda_=>_", sform_lambda Aimplicit); ("lambda_≡>_", sform_lambda Aerasable); - ("_->_", sform_arrow Aexplicit); + ("_->_", sform_arrow Anormal); ("_=>_", sform_arrow Aimplicit); ("_≡>_", sform_arrow Aerasable); ("case_", sform_case);

===================================== src/elexp.ml ===================================== @@ -32,7 +32,7 @@

open Sexp (* Sexp type *) -open Pexp (* Aexplicit *) +open Pexp (* Anormal *)

module U = Util module L = Lexp

===================================== src/eval.ml ===================================== @@ -491,7 +491,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 (vdummy, -1))])) + -> Vtype (L.mkCall (e, [(Anormal, Var (vdummy, -1))])) | _ -> value_fatal loc f "Trying to call a non-function!"

and eval_case ctx i loc target pat dflt =

===================================== src/lexp.ml ===================================== @@ -429,14 +429,14 @@ let rec lexp_unparse lxp = -> let l = lexp_location lxp in let st = lexp_unparse ltp in Node (Symbol (l, match kind with - | Aexplicit -> "lambda_->_" + | Anormal -> "lambda_->_" | Aimplicit -> "lambda_=>_" | Aerasable -> "lambda_≡>_"), [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body]) | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) -> let ut1 = lexp_unparse ltp1 in - Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" + Node (Symbol (loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), [(match oname with None -> ut1 @@ -476,11 +476,11 @@ let rec lexp_unparse lxp = List.map (fun arg -> match arg with - | (Aexplicit, (_,None), t) -> lexp_unparse t + | (Anormal, (_,None), t) -> lexp_unparse t | (ak, s, t) -> let (l,_) as id = sname s in Node (Symbol (l, match ak with - | Aexplicit -> "_:_" + | Anormal -> "_:_" | Aimplicit -> "_::_" | Aerasable -> "_:::_"), [Symbol id; lexp_unparse t])) @@ -652,7 +652,7 @@ let rec get_precedence expr ctx = | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" - | Arrow (Aexplicit, _, _, _, _) -> lkp "->" + | Arrow (Anormal, _, _, _, _) -> lkp "->" | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" | Call (exp, _) -> get_precedence exp ctx @@ -712,10 +712,10 @@ and lexp_str ctx (exp : lexp) : string = else green ^ str ^ reset in

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

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

let get_name fname = match fname with | Builtin ((_, name), _, _) -> name, 0 @@ -792,7 +792,7 @@ and lexp_str ctx (exp : lexp) : string = match arg_type with | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) - | Aexplicit -> str ^ " " ^ (lexp_str' lxp) + | Anormal -> str ^ " " ^ (lexp_str' lxp) | _ -> str in (

match args with

===================================== src/opslexp.ml ===================================== @@ -391,7 +391,7 @@ let nerased_let defs erased = if not (List.mem true es) then nerased else List.fold_left (fun erased e - -> dbset_push (if e then P.Aerasable else P.Aexplicit) erased) + -> dbset_push (if e then P.Aerasable else P.Anormal) erased) erased es

(* "check ctx e" should return τ when "Δ ⊢ e : τ" *)

===================================== src/pexp.ml ===================================== @@ -29,7 +29,7 @@ let pexp_error = msg_error "PEXP"

(*************** The Pexp Parser *********************)

-type arg_kind = Aexplicit | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) +type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *)

(* This is Dangerously misleading since pvar is NOT pexp but Pvar is *) type pvar = symbol @@ -46,11 +46,11 @@ let pexp_pat_location e = match e with

let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with - | (Aexplicit, s, None) -> Symbol s + | (Anormal, s, None) -> Symbol s | (ak, ((l,_) as s), t) -> Node (Symbol (l, match ak with Aerasable -> ":::" | Aimplicit -> "::" - | Aexplicit -> ":"), + | Anormal -> ":"), [Symbol s; match t with Some e -> e | None -> Symbol (l, "_")])

===================================== tests/unify_test.ml ===================================== @@ -125,11 +125,11 @@ let input_type_t = generate_ltype_from_str str_type2

let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

- ( Lambda ((Aexplicit), + ( Lambda ((Anormal), (Util.dummy_location, Some "L1"), Var((Util.dummy_location, Some "z"), 3), Imm (Integer (Util.dummy_location, 3))), - Lambda ((Aexplicit), + Lambda ((Anormal), (Util.dummy_location, Some "L2"), Var((Util.dummy_location, Some "z"), 4), Imm (Integer (Util.dummy_location, 3))), Nothing )

View it on GitLab: https://gitlab.com/monnier/typer/commit/2f9ed1b09add160cbf9ea70bda4a4c30ee5a...