Stefan pushed to branch master at Stefan / Typer

Commits: c4c529a9 by Stefan Monnier at 2016-05-06T23:51:30-04:00 * src/typecheck.ml (check): Add missing cases (mostly, Case and Cons)

* src/lexp.ml: Move the subst helper functions and the unsusp here from typecheck.ml. (U): Use named import instead of `open` for Util. (Case): Change pattern args so they always have an arg_kind. (_lexp_to_str.arg_str): Change accordingly.

* src/lparse.ml: Remove all ";;": they are only meaningful to OCaml's interactive loop and don't belong in source files. (lexp_read_pattern, lexp_read_pattern_args): Adjust to new `Case` type.

* src/subst.ml (cons): New primitive.

* src/typecheck.ml: Move the subst helper functions and `unsusp` to lexp.ml. (lookup_value): New function. (check): Add missing cases (mostly, Case and Cons).

- - - - -

8 changed files:

- DESIGN - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/subst.ml - src/typecheck.ml - src/util.ml

Changes:

===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -955,12 +955,6 @@ This should allow HOAS-style encodings like | App exp exp | Lam (IO (exp -> exp))

-* Universe polymorphism -Agda seems to do: -- Add Level as a new special type (with 0 and S constructors and without elim). -- Define: "Set : Πl:Level.Set(S l)". -- Give Πl:Level.e a "non-Set" type to disallow "deep" polymorphism. - * Strong elimination of large types *** From "Recursive Families of Inductive Types" by Capretta Strong elimination is the elimination rule for inductive types in which the @@ -1387,6 +1381,12 @@ when they're only used in irrelevant args might relieve the tension. *** pruning: [Pientka, PhD, Sec. 3.1.2; Abel & Pientka, TLCA 2011]

* Universes +** Universe polymorphism +Agda seems to do: +- Add Level as a new special type (with 0 and S constructors and without elim). +- Define: "Set : Πl:Level.Set(S l)". +- Give Πl:Level.e a "non-Set" type to disallow "deep" polymorphism. + ** PTS versions

*** universes with baked in ~subsumption

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -56,8 +56,7 @@ type value_type = | Vcons of symbol * value_type list | Vbuiltin of builtin * string | Closure of lexp * (((string option * value_type) ref myers) * (int * int)) - (* Macro type *) - | Vsexp of sexp + | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -199,10 +199,10 @@ and eval_case ctx i loc target pat dflt = (* This is more robust *) let rec fold2 nctx pats args = match pats, args with - | (Some (_, (_, name)))::pats, arg::args -> + | (_, Some (_, name))::pats, arg::args -> let nctx = add_rte_variable (Some name) arg nctx in fold2 nctx pats args - | None::pats, arg::args -> fold2 nctx pats args + | (_, None)::pats, arg::args -> fold2 nctx pats args (* Errors *) | _::_, [] -> eval_warning loc "a) Eval::Case Pattern Error"; nctx | [], _::_ -> eval_warning loc "b) Eval::Case Pattern Error"; nctx

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -20,7 +20,9 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

-open Util +module U = Util +module L = List +module SMap = U.SMap open Fmt

open Sexp @@ -37,7 +39,7 @@ module S = Subst (* 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 vdef = location * string +type vdef = U.location * string type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) type db_revindex = int (* DeBruijn index counting from the root. *) @@ -65,25 +67,25 @@ type ltype = lexp and lexp = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level - | Sort of location * sort + | Sort of U.location * sort | Builtin of builtin * string * ltype | Var of vref | Susp of lexp * lexp S.subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) - | Let of location * (vdef * lexp * ltype) list * lexp - | Arrow of arg_kind * vdef option * ltype * location * lexp + | Let of U.location * (vdef * lexp * ltype) list * lexp + | Arrow of arg_kind * vdef option * ltype * U.location * lexp | Lambda of arg_kind * vdef * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of location * label * ((arg_kind * vdef * ltype) list) + | Inductive of U.location * label * ((arg_kind * vdef * ltype) list) * ((arg_kind * vdef option * ltype) list) SMap.t | Cons of vref * symbol (* = Type info * ctor_name *) - | Case of location * lexp + | Case of U.location * lexp * ltype (* The base inductive type over which we switch. *) * ltype (* The type of the return value of all branches *) - * (location * (arg_kind * vdef) option list * lexp) SMap.t + * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * lexp option (* Default. *) (* (* For logical metavars, there's no substitution. *) - * | Metavar of (location * string) * metakind * metavar ref + * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = * (* An uninstantiated var, along with a venv (stipulating over which vars * * it should be closed), and its type. @@ -105,10 +107,22 @@ type ltype = lexp | SLsucc of lexp

-(* let mk_susp s e = if VMap.is_empty s then e else Susp (s, e) - * let mk_subst x v e = Susp (VMap.add x v VMap.empty, e) *) +(********* 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 + * and be done with it. *)

-let opt_map f x = match x with None -> None | Some x -> Some (f x) +let rec mkSusp e s = + if S.identity_p s then e else + match e with + | Susp (e, s') -> mkSusp e (scompose s' s) + | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *) + | _ -> Susp (e, s) +and scompose s1 s2 = S.compose mkSusp s1 s2 +and slookup s l v = S.lookup (fun l i -> Var (l, i)) + (fun e o -> mkSusp e (S.shift o)) + s l v +let ssink = S.sink (fun l i -> Var (l, i))

(**** The builtin elements ****) (* @@ -126,7 +140,7 @@ let builtins = ] @ List.map (fun bi -> match bi with | Builtin (_, name, t) -> (name, Some bi, t) - | _ -> internal_error "Registering a non-builtin") + | _ -> U.internal_error "Registering a non-builtin") [type_level; type_int; type_float; type_eq] (* let var_bottom = Var (dloc, -1) *)

@@ -213,14 +227,14 @@ let id x = x (* let lexp_subst_subst s s' = * let s' = VMap.map (fun e -> mk_susp s e) s' in * VMap.fold (fun v e s -> if VMap.mem v s - * then (internal_error "Overlapping substs") + * then (U.internal_error "Overlapping substs") * else VMap.add v e s) * s s' *)

let lexp_max_sort (k1, k2) = match k1,k2 with | Sort (_,l1), Sort (_, l2) -> max l1 l2 - | _ -> internal_error "finding the max of non-sorts!" + | _ -> U.internal_error "finding the max of non-sorts!"

(* Invert a substitution. I.e. return s' such that s'(s(e))=e. * It is allowed to presume that e is closed in `venv'. *) @@ -241,10 +255,10 @@ let rec lexp_location e = match e with | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e - | SortLevel (SLn _) -> dummy_location + | SortLevel (SLn _) -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l - | Builtin _ -> dummy_location + | Builtin _ -> U.dummy_location | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l | Lambda (_,(l,_),_,_) -> l @@ -257,6 +271,64 @@ let rec lexp_location e = * | Metavar ((l,_),_,_) -> l *)

+(********* Normalizing a term *********) + +let vdummy = (U.dummy_location, "dummy") +let maybev mv = match mv with None -> vdummy | Some v -> v + +let rec unsusp e s = (* Push a suspension one level down. *) + match e with + | Imm _ -> e + | SortLevel _ -> e + | Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s)) + | Sort (l, _) -> e + | Builtin _ -> e + | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v + | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; + mkSusp e (scompose s' s) + | Let (l, defs, e) + -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in + let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) + -> (ssink v s, + (v, mkSusp e s', mkSusp ty s) :: ndefs)) + (s, []) defs in + Let (l, ndefs, mkSusp e s') + | Arrow (ak, v, t1, l, t2) + -> Arrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s)) + | Lambda (ak, v, t, e) -> Lambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) + | Call (f, args) -> Call (mkSusp f s, + L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) + | Inductive (l, label, args, cases) + -> let (_, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) + (s, []) args in + let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink (maybev v) s, + (ak, v, mkSusp t s) + :: nargs)) + (s, []) args in + ncase) + cases in + Inductive (l, label, nargs, ncases) + | Cons _ -> e + | Case (l, e, it, ret, cases, default) + -> Case (l, mkSusp e s, mkSusp it s, mkSusp ret s, + SMap.map (fun (l, cargs, e) + -> let s' = L.fold_left (fun s carg + -> match carg with + | (_,None) -> s + | (_,Some v) -> ssink v s) + s cargs in + (l, cargs, mkSusp e s')) + cases, + match default with + | None -> default + | Some e -> Some (mkSusp e s)) + + + let lexp_to_string e = match e with | Imm _ -> "Imm" @@ -269,13 +341,12 @@ let lexp_to_string e = | Cons _ -> "inductive-cons" | Case _ -> "case" | _ -> "not implemented" -;;

-let builtin_reduce b args arg = - match b,args,arg with - | IAdd, [(_,Imm (Integer (_, i1)))], (Imm (Integer (_, i2))) - -> Some (Imm (Integer (dummy_location, i1 + i2))) - | _ -> None +(* let builtin_reduce b args arg = + * match b,args,arg with + * | IAdd, [(_,Imm (Integer (_, i1)))], (Imm (Integer (_, i2))) + * -> Some (Imm (Integer (U.dummy_location, i1 + i2))) + * | _ -> None *)

(* Apply substitution `s' and then reduce to weak head normal form. * WHNF implies: @@ -395,11 +466,11 @@ and lexp_unparse e : pexp = | Sort (l, StypeOmega) -> Pvar (l, "TypeΩ") | Sort (l, Stype e) -> Pcall (Pvar (l, "Type"), [pexp_unparse (lexp_unparse e)]) - | SortLevel (SLn n) -> Pimm (Integer (dummy_location, n)) + | SortLevel (SLn n) -> Pimm (Integer (U.dummy_location, n)) | SortLevel (SLsucc e) -> Pcall (Pvar (lexp_location e, "S"), [pexp_unparse (lexp_unparse e)]) | Imm s -> Pimm s - | Builtin (b,name,t) -> Pvar (dummy_location, name) + | Builtin (b,name,t) -> Pvar (U.dummy_location, name) | Var v -> Pvar (lexp_unparse_v v) | Let (l,decls,e) -> Plet (l, lexp_unparse_decls decls, @@ -423,7 +494,7 @@ and lexp_unparse e : pexp = | Cons (Var v, tag) -> Pcons (lexp_unparse_v v, tag) | Cons (_,_) - -> (internal_error "Can't print a non-Var-typed Constructor") + -> (U.internal_error "Can't print a non-Var-typed Constructor") | Case (l, e, t, branches, default) -> Pcase (l, lexp_unparse e, (* FIXME!! *) @@ -438,7 +509,7 @@ and lexp_unparse e : pexp = * | MetaSet e -> lexp_unparse e * | _ -> Pmetavar v) (* FIXME: losing the ref. *) * | Susp (s,e) -> lexp_unparse (lexp_whnf s e) *) - (* (internal_error "Can't print a Susp") *) + (* (U.internal_error "Can't print a Susp") *)

let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e))

@@ -450,7 +521,7 @@ let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) * | _ -> e * and vmap_getval (v : var) = * match VMap.find v env with (Some e, _) -> follow e - * | _ -> Var (dummy_location, v) in + * | _ -> Var (U.dummy_location, v) in * match e with * | Sort (l, Stype e) -> Sort (l, Stype (SortLevel (SLsucc e))) * | Sort (l, StypeOmega) @@ -461,7 +532,7 @@ let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) * | Imm (Integer _) -> type_int * | Imm (Float _) -> type_float * | Builtin (_,_,t) -> t - * (* | Imm (String _) -> Var (dummy_location, var_string) *) + * (* | Imm (String _) -> Var (U.dummy_location, var_string) *) * | Imm s -> let l = sexp_location s in * msg_error l "Unrecognized sexp in lexp"; mk_meta_dummy env l * | Var (_,name) -> snd (VMap.find name env) @@ -472,7 +543,7 @@ let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) * body * | Arrow _ -> type0 (* FIXME! *) * | Lambda (ak, ((l,v) as var),t,e) -> - * Arrow (ak, Some var, t, dummy_location, + * Arrow (ak, Some var, t, U.dummy_location, * lexp_type (VMap.add v (None, t) env) e) * | Call (f, args) -> * let ft = lexp_type env f in @@ -685,8 +756,8 @@ and _lexp_to_str ctx exp = let arg_str arg = List.fold_left (fun str v -> match v with - | None -> str ^ " _" - | Some (_, (_, n)) -> str ^ " " ^ n) "" arg in + | (_,None) -> str ^ " _" + | (_, Some (_, n)) -> str ^ " " ^ n) "" arg in

let str = SMap.fold (fun k (_, arg, exp) str ->

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -48,7 +48,6 @@ open Builtin (* Shortcut => Create a Var *) let make_var name index loc = Var(((loc, name), index)) -;;

let dlxp = type0 let dltype = type0 @@ -58,7 +57,7 @@ let lexp_warning = msg_warning "LPARSE" let lexp_error = msg_error "LPARSE" let lexp_fatal = msg_fatal "LPARSE"

-let _global_lexp_ctx = ref make_lexp_context;; +let _global_lexp_ctx = ref make_lexp_context let _global_lexp_trace = ref []

(* The main job of lexp (currently) is to determine variable name (index) @@ -459,7 +458,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* Read a pattern and create the equivalent representation *) and lexp_read_pattern pattern exp target ctx: - ((string * location * (arg_kind * vdef) option list) * lexp_context) = + ((string * location * (arg_kind * vdef option) list) * lexp_context) =

match pattern with | Ppatany (loc) -> (* Catch all expression nothing to do *) @@ -494,7 +493,7 @@ and lexp_read_pattern pattern exp target ctx:

(* Read patterns inside a constructor *) and lexp_read_pattern_args args ctx: - (((arg_kind * vdef) option list) * lexp_context)= + (((arg_kind * vdef option) list) * lexp_context)=

let rec loop args acc ctx = match args with @@ -503,14 +502,14 @@ and lexp_read_pattern_args args ctx: let (_, pat) = hd in match pat with (* Nothing to do *) - | Ppatany (loc) -> loop tl (None::acc) ctx + | Ppatany (loc) -> loop tl ((Aexplicit, None)::acc) ctx | Ppatvar ((loc, name) as var) -> (* Add var *) let nctx = env_extend ctx var None dltype in - let nacc = (Some (Aexplicit, var))::acc in + let nacc = (Aexplicit, Some var)::acc in loop tl nacc nctx | _ -> lexp_error dloc "Constructor inside a Constructor"; - loop tl (None::acc) ctx) + loop tl ((Aexplicit, None)::acc) ctx)

in loop args [] ctx

@@ -713,11 +712,10 @@ and lexp_print_var_info ctx = print_string ": "; lexp_print tp; print_string "\n") - done; -;; + done

-let lexp_parse_all p ctx = _lexp_parse_all p ctx 1;; +let lexp_parse_all p ctx = _lexp_parse_all p ctx 1

(* add dummy definition helper *) @@ -725,7 +723,6 @@ let add_def name ctx = let var = (dloc, name) in let ctx = senv_add_var var ctx in env_add_var_info (0, var, None, dlxp) ctx -;;

(* String Parsing @@ -736,22 +733,18 @@ let _lexp_expr_str (str: string) (tenv: bool array) (grm: grammar) (limit: string option) (ctx: lexp_context) = let pxps = _pexp_expr_str str tenv grm limit in lexp_parse_all pxps ctx -;;

(* specialized version *) let lexp_expr_str str lctx = _lexp_expr_str str default_stt default_grammar (Some ";") lctx -;;

let _lexp_decl_str (str: string) tenv grm limit ctx = let pxps = _pexp_decl_str str tenv grm limit in lexp_p_decls pxps ctx -;;

(* specialized version *) let lexp_decl_str str lctx = _lexp_decl_str str default_stt default_grammar (Some ";") lctx -;;

(* Eval String @@ -761,11 +754,9 @@ let lexp_decl_str str lctx = let _eval_expr_str str lctx rctx silent = let lxps = lexp_expr_str str lctx in (eval_all lxps rctx silent) -;;

let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false

let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in (eval_decls lxps rctx), lctx -;;

===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -258,5 +258,9 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:'a subst) = Cons (mkVar l 0, mkShift s 1)

+(* Return a substitution which replaces #0 with `e` and the applies `s` + * to the rest. *) +let cons e s = Cons (e, s) + (* Return a substitution which replaces #0 with `e`. *) let substitute e = Cons (e, Identity)

===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -24,7 +24,7 @@ module U = Util module SMap = U.SMap (* open Lexer *) open Sexp -(* open Pexp *) +module P = Pexp (* open Myers *) (* open Grammar *) open Lexp @@ -36,24 +36,6 @@ module B = Builtin

let conv_erase = true (* If true, conv ignores erased terms. *)

-(********* 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 - * and be done with it. *) - -let rec mkSusp e s = - if S.identity_p s then e else - match e with - | Susp (e, s') -> mkSusp e (scompose s' s) - | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *) - | _ -> Susp (e, s) -and scompose s1 s2 = S.compose mkSusp s1 s2 -and slookup s l v = S.lookup (fun l i -> Var (l, i)) - (fun e o -> mkSusp e (S.shift o)) - s l v -let ssink = S.sink (fun l i -> Var (l, i)) - - (********* Testing if two types are "convertible" aka "equivalent" *********)

let rec conv_arglist_p s1 s2 args1 args2 : bool = @@ -117,62 +99,6 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2

-(********* Normalizing a term *********) - -let vdummy = (U.dummy_location, "dummy") -let maybev mv = match mv with None -> vdummy | Some v -> v - -let rec unsusp e s = (* Push a suspension one level down. *) - match e with - | Imm _ -> e - | SortLevel _ -> e - | Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s)) - | Sort (l, _) -> e - | Builtin _ -> e - | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v - | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; - mkSusp e (scompose s' s) - | Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in - let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) - -> (ssink v s, - (v, mkSusp e s', mkSusp ty s) :: ndefs)) - (s, []) defs in - Let (l, ndefs, mkSusp e s') - | Arrow (ak, v, t1, l, t2) - -> Arrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s)) - | Lambda (ak, v, t, e) -> Lambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) - | Call (f, args) -> Call (mkSusp f s, - L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) - | Inductive (l, label, args, cases) - -> let (_, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) - (s, []) args in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink (maybev v) s, - (ak, v, mkSusp t s) - :: nargs)) - (s, []) args in - ncase) - cases in - Inductive (l, label, nargs, ncases) - | Cons _ -> e - | Case (l, e, it, ret, cases, default) - -> Case (l, mkSusp e s, mkSusp it s, mkSusp ret s, - SMap.map (fun (l, cargs, e) - -> let s' = L.fold_left (fun s carg - -> match carg with - | None -> s - | Some (ak, v) -> ssink v s) - s cargs in - (l, cargs, mkSusp e s')) - cases, - match default with - | None -> default - | Some e -> Some (mkSusp e s)) - (********* Testing if a lexp is properly typed *********)

type varbind = @@ -183,7 +109,13 @@ type varbind = let lookup_type ctx vref = let (_, i) = vref in let (_, _, _, t) = Myers.nth i ctx in - Susp (t, S.shift (i + 1)) + mkSusp t (S.shift (i + 1)) + +let lookup_value ctx vref = + let (_, i) = vref in + match Myers.nth i ctx with + | (o, _, LetDef v, _) -> Some (unsusp v (S.shift (i + 1 - o))) + | _ -> None

let assert_type e t t' = if conv_p t t' then () @@ -208,9 +140,18 @@ let rec check ctx e = match e with | Imm (Float (_, _)) -> B.type_float | Imm (Integer (_, _)) -> B.type_int + | Imm (Epsilon|Block (_, _, _)|Symbol _|String (_, _)|Node (_, _)) + -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; + B.type_int) | SortLevel (_) -> B.type_level | Sort (l, Stype (SortLevel (SLn n))) -> Sort (l, Stype (SortLevel (SLn (1 + n)))) + | Sort (_, (StypeOmega|StypeLevel)) + -> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sorts!"; + B.type_omega) + | Sort (_, (Stype _)) + -> (U.msg_error "TC" (lexp_location e) "Non-level arg to Type!"; + B.type_omega) | Builtin (_, _, t) -> t (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v @@ -242,9 +183,9 @@ let rec check ctx e = | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) "Not a proper type"; Sort (l, StypeOmega)) - | (_, Sort (_, _)) -> (U.msg_error "TC" (lexp_location t1) - "Not a proper type"; - Sort (l, StypeOmega))) + | (_, _) -> (U.msg_error "TC" (lexp_location t1) + "Not a proper type"; + Sort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) -> ((match check ctx t with | Sort _ -> () @@ -274,19 +215,84 @@ let rec check ctx e = match args with | [] -> Sort (l, s) | (ak, v, t)::args - -> match check ctx t with - | Sort (_, s') - -> Arrow (ak, Some v, t, lexp_location t, - (* FIXME: `sort_compose` doesn't do what we want! *) - arg_loop args (sort_compose l s s') - (Myers.cons (0, Some v, Variable, t) ctx)) in + -> let s' = match check ctx t with + | Sort (_, s') -> s' + | _ -> (U.msg_error "TC" (lexp_location t) + "Field type is not a Type!"; + Stype (SortLevel (SLn 0))) in + Arrow (ak, Some v, t, lexp_location t, + (* FIXME: `sort_compose` doesn't do what we want! *) + arg_loop args (sort_compose l s s') + (Myers.cons (0, Some v, Variable, t) ctx)) in let tct = arg_loop args (Stype (SortLevel (SLn 0))) ctx in (* FIXME: Check cases! *) tct - (*| Case (l, e, it, branches, default) - -> let et = check ctx e in - (* FIXME: Check that `et` is derived from `it`. - * E.g. if `et` is `List Int` then `it` should be `List`. *) - SMap.iter (fun name (l, vdefs, branch) - -> - *) + | Case (l, e, it, ret, branches, default) + -> let rec call_split e = + match e with + | Call (f, args) -> let (f',args') = call_split f in (f', args' @ args) + | _ -> (e,[]) in + (match call_split (check ctx e) with + | Inductive (_, _, fargs, constructors), aargs -> + let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + (* We don't check aarg's type, because we assume that `check` + * returns a valid type. *) + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (U.msg_error "TC" l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + SMap.iter + (fun name (l, vdefs, branch) + -> let fieldtypes = SMap.find name constructors in + let rec mkctx ctx s vdefs fieldtypes = + match vdefs, fieldtypes with + | [], [] -> ctx + (* FIXME: If ak is Aerasable, make sure the var only + * appears in type annotations. *) + | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes + -> mkctx (Myers.cons (0, vdef, Variable, mkSusp ftype s) ctx) + (S.cons (Var ((match vdef with Some vd -> vd + | None -> (l, "_")), + 0)) s) + vdefs fieldtypes + | _,_ -> (U.msg_error "TC" l + "Wrong number of args to constructor!"; + ctx) in + let nctx = mkctx ctx s vdefs fieldtypes in + assert_type branch ret (check nctx branch)) + branches; + (match default with + | Some d -> assert_type d ret (check ctx d) + | _ -> ()) + | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); + ret + | Cons (vr, (_, name)) + -> (match lookup_value ctx vr with + | Some (Inductive (l, _, fargs, constructors) as it) + -> 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 fieldtypes = + match fieldtypes with + | [] -> Call (it, indtype fargs (L.length fieldtypes + + L.length fargs - 1)) + | (ak, vd, ftype) :: fieldtypes + -> Arrow (ak, vd, ftype, lexp_location ftype, + fieldargs fieldtypes) in + let rec buildtype fargs = + match fargs with + | [] -> fieldargs fieldtypes + | (ak, ((l,_) as vd), atype) :: fargs + -> Arrow (P.Aerasable, Some vd, atype, l, + buildtype fargs) in + buildtype fargs + | _ -> (U.msg_error "TC" (lexp_location e) + "Cons of a non-inductive type!"; + B.type_int)) +

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -37,8 +37,7 @@ let print_loc (loc: location) = print_string "ln "; Fmt.ralign_print_int loc.line 3; print_string ", cl "; - Fmt.ralign_print_int loc.column 3; -;; + Fmt.ralign_print_int loc.column 3

(* * -1 - Nothing (* During testing we may want to produce errors *) @@ -90,6 +89,7 @@ let print_trace name max elem_to_string print_elem trace = print_string (elem_to_string g); print_string ": "; print_elem g; print_string "\n");

- print_string (Fmt.make_sep '='); + print_string (Fmt.make_sep '=')

+let opt_map f x = match x with None -> None | Some x -> Some (f x)

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