Stefan pushed to branch master at Stefan / Typer
Commits: 0aa7e076 by Stefan Monnier at 2016-12-01T22:32:38-05:00 Simplify predef slightly
* src/builtin.ml (predef_table): Remove type. (default_predef_map): Remove variable. (predef_map): Change type. Pre-fill with `Macro`. (get_predef_raw, get_predef_option, dump_predef, is_lbuiltin): Remove functions. (get_predef): Catch errors. (set_predef): Rewrite.
* src/lexp.ml (lexp_unparse): Use Pbuiltins for Sorts. (_lexp_to_str): Improve handling of SLsucc and Stype.
* src/lparse.ml (infer_call): Use BI.get_predef. (default_lctx): Adjust to new set_predef.
* src/opslexp.ml (check'): Catch case of Cons of a wrong label.
- - - - -
5 changed files:
- src/builtin.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml
Changes:
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -67,8 +67,6 @@ open Env (* get_rte_variable *) let error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) let warning loc msg = msg_warning "BUILT-IN" loc msg
-type predef_table = (lexp option ref) SMap.t - let predef_name = [ "cons"; "nil"; @@ -81,39 +79,21 @@ let predef_name = [ "expand_dmacro_"; ]
-let default_predef_map : predef_table = - (* add predef name, expr will be populated when parsing *) - List.fold_left (fun m name -> - SMap.add name (ref None) m) SMap.empty predef_name - -let predef_map = ref default_predef_map - -let get_predef_raw (name: string) : lexp = - match !(SMap.find name (!predef_map)) with - | Some exp -> exp - | None -> error dloc ("""^ name ^ "" was not predefined") - -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 +(* FIXME: Actually, we should map the predefs to *values* since that's + * where they're really needed! *) +let predef_map : lexp SMap.t ref + (* Pre-fill "Macro" with a dummy value, to avoid errors while reading + * the builtins.typer file. *) + = ref (SMap.add "Macro" impossible SMap.empty)
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)) + try let r = (DB.get_size ctx) - !builtin_size - 0 in + let p = SMap.find name (!predef_map) in + mkSusp p (S.shift r) + with Not_found -> error dummy_location ("""^ name ^ "" was not predefined")
-let set_predef name lexp = - SMap.find name (!predef_map) := lexp - -let dump_predef () = - let _ = SMap.iter (fun key item -> - print_string key; print_string " "; - let _ = match !item with - | Some lxp -> lexp_print lxp - | None -> print_string "None"; in - print_string "\n") !predef_map in () +let set_predef name lexp + = predef_map := SMap.add name lexp (!predef_map)
(* Builtin types *) let dloc = DB.dloc @@ -161,17 +141,8 @@ let rec tlist2olist acc expr = value_print expr; error dloc "List conversion failure'"
-let is_lbuiltin idx ctx = - let bsize = 1 in - let csize = DB.get_size ctx in - - if idx >= csize - bsize then - true - else - false - (* Map of lexp builtin elements accessible via (## <name>). *) -let lmap = ref (SMap.empty : (L.lexp * L.ltype) SMap.t) +let lmap = ref (SMap.empty : (lexp * ltype) SMap.t)
let add_builtin_cst (name : string) (e : lexp) = let map = !lmap in
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -511,7 +511,7 @@ and print_typer_trace trace = print_typer_trace' b
and print_trace title trace default = - (* If no trace is provided take the most recent one *) + (* If no trace is provided take the most revent one *) let trace = match trace with | Some trace -> trace | None -> default in
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -269,7 +269,7 @@ and nosusp e = (* Return `e` with no outermost `Susp`. *) | _ -> e
-(* Get rid of `Susp`ensions and instantiated `Maetavar`s. *) +(* Get rid of `Susp`ensions and instantiated `Metavar`s. *) let clean meta_ctx e = let rec clean s e = match e with | Imm _ -> e @@ -419,13 +419,15 @@ let rec lexp_unparse lxp = -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]>"))
- | SortLevel (SLz) -> Pimm (Integer (U.dummy_location, 0)) - | SortLevel (SLsucc sl) -> Pcall (Pimm (Symbol (U.dummy_location, "<S>")), - [pexp_unparse (lexp_unparse sl)]) - | Sort (l, StypeOmega) -> Pimm (Symbol (l, "<TypeOmega>")) - | Sort (l, StypeLevel) -> Pimm (Symbol (l, "<TypeLevel>")) - | Sort (l, Stype sl) -> Pcall (Pimm (Symbol (l, "<Type>")), - [pexp_unparse (lexp_unparse sl)]) + | SortLevel (SLz) -> Pbuiltin (U.dummy_location, "TypeLevel.z") + | SortLevel (SLsucc l) + -> Pcall (Pbuiltin (lexp_location l, "TypeLevel.succ"), + [pexp_unparse (lexp_unparse l)]) + | Sort (l, StypeOmega) -> Pbuiltin (l, "Type_ω") + | Sort (l, StypeLevel) -> Pbuiltin (l, "Type_ℓ") + | Sort (l, Stype sl) + -> Pcall (Pbuiltin (lexp_location sl, "Type_"), + [pexp_unparse (lexp_unparse sl)])
(* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) @@ -657,12 +659,12 @@ and _lexp_to_str ctx exp =
| Sort (_, Stype (SortLevel SLz)) -> "##Type" | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" + | Sort (_, Stype l) -> "(##Type_ " ^ lexp_string l ^ ")" | Sort (_, StypeLevel) -> "##Type_ℓ" - | Sort (_, Stype _) -> "##Type_?" (* FIXME! *) | Sort (_, StypeOmega) -> "##Type_ω"
| SortLevel (SLz) -> "##TypeLevel.z" - | SortLevel (SLsucc e) -> "##TypeLevel.succ" + | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")"
and lexp_str_ctor ctx ctors = SMap.fold (fun key value str
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -804,16 +804,17 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = infer pxp ctx in
(* This is the builtin Macro type *) - let macro_type = match BI.get_predef_option "Macro" ctx with - | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx - (* When type.typer is being parsed and the predef is not yet available *) - | None -> impossible in + let macro_type = BI.get_predef "Macro" ctx in
(* determine function type *) if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ltp type_special_form) then match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with | Builtin ((_, name), _, _) -> (* Special form. *) + (* FIXME: Special forms like `##case_` and `##lambda_` + * want to know the context's expected type. + * Also, for `##_->_`, calling `check` would be algorithmically + * expensive: a complexity of O(N²) for t₁ → t₂ ... → tₙ. *) let e = (get_special_form loc name) ctx loc sargs in let meta_ctx, _ = !global_substitution in (* FIXME: We don't actually need to typecheck `e`, we just need @@ -866,6 +867,7 @@ and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type = let args = [(Aexplicit, macro_funct); (Aexplicit, (BI.olist2tlist_lexp sargs ctx))] in
+ (* FIXME: Don't `mkCall + eval` but use eval_call instead! *) let macro = mkCall (macro_expand, args) in let emacro = OL.erase_type macro in let rctx = EV.from_lctx ctx in @@ -1169,7 +1171,7 @@ let default_lctx = List.iter (fun name -> let idx = senv_lookup name lctx in let v = Var((dloc, name), idx) in - BI.set_predef name (Some v)) BI.predef_name; + BI.set_predef name v) BI.predef_name; (* -- DONE -- *) lctx with e ->
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -521,31 +521,38 @@ let rec check' meta_ctx erased ctx e = ^ string_of_int diff ^ " cases missing")) | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); ret - | Cons (t, (_, name)) + | Cons (t, (l, name)) -> (match lexp_whnf t ctx meta_ctx with | Inductive (l, _, fargs, constructors) - -> let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, Var (vd, start_index)) - :: indtype fargs (start_index - 1) in - let rec fieldargs ftypes = - match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) - | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in - let rec buildtype fargs = - match fargs with - | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, Some vd, atype, l, - buildtype fargs) in - buildtype fargs + -> (try + let fieldtypes = SMap.find name constructors in + let rec indtype fargs start_index = + match fargs with + | [] -> [] + | (ak, vd, _)::fargs -> (ak, Var (vd, start_index)) + :: indtype fargs (start_index - 1) in + let rec fieldargs ftypes = + match ftypes with + | [] -> let nargs = List.length fieldtypes + List.length fargs in + mkCall (mkSusp t (S.shift nargs), + indtype fargs (nargs - 1)) + | (ak, vd, ftype) :: ftypes + -> mkArrow (ak, vd, ftype, lexp_location ftype, + fieldargs ftypes) in + let rec buildtype fargs = + match fargs with + | [] -> fieldargs fieldtypes + | (ak, ((l,_) as vd), atype) :: fargs + -> mkArrow (P.Aerasable, Some vd, atype, l, + buildtype fargs) in + buildtype fargs + with Not_found + -> (U.msg_error "TC" l + ("Constructor "" ^ name ^ "" does not exist"); + DB.type_int)) | _ -> (U.msg_error "TC" (lexp_location e) - "Cons of a non-inductive type!"; + ("Cons of a non-inductive type: " + ^ lexp_string t); DB.type_int)) | Metavar (idx, s, _, t) -> try check erased ctx (push_susp (L.VMap.find idx meta_ctx) s)
View it on GitLab: https://gitlab.com/monnier/typer/commit/0aa7e076aeb825c4824dda2a66301d0059de...
Afficher les réponses par date