Stefan pushed to branch master at Stefan / Typer

Commits: aaa414b2 by Stefan Monnier at 2017-07-27T10:29:18-04:00 Don't pass meta_ctx as arg any more

Instead, assign to global_substitution directly from unification.ml.

- - - - -

2 changed files:

- src/lexp.ml - src/opslexp.ml

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -80,7 +80,7 @@ type ltype = lexp * (U.location * (arg_kind * vname option) list * lexp) SMap.t * (vname option * lexp) option (* Default. *) (* The `subst` only applies to the lexp associated - * with the metavar's index (i.e. its "value"), not to the ltype. *) + * with the metavar's "value", not to the ltype. *) | Metavar of int * subst * vname * ltype (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref @@ -289,7 +289,7 @@ and nosusp e = (* Return `e` with no outermost `Susp`. *)

(* Get rid of `Susp`ensions and instantiated `Metavar`s. *) -let clean meta_ctx e = +let clean e = let rec clean s e = match e with | Imm _ -> e | SortLevel (SLz) -> e @@ -342,6 +342,7 @@ let clean meta_ctx e = else clean S.identity (mkSusp e s) | Metavar (idx, s', l, t) -> let s = (scompose s' s) in + let meta_ctx, _ = !global_substitution in try clean s (VMap.find idx meta_ctx) with Not_found -> mkMetavar (idx, s, l, t) in clean S.identity e @@ -667,9 +668,8 @@ and _lexp_str ctx (exp : lexp) : string = | Metavar (idx, subst, (loc, name), _) ->( (* print metavar result if any *) let print_meta exp = - let meta_ctx, _ = !global_substitution in let ctx = set_meta exp ctx in - _lexp_str ctx (clean meta_ctx exp) in + _lexp_str ctx (clean exp) in

match pp_meta ctx with | None -> print_meta exp @@ -810,9 +810,8 @@ and _lexp_str_decls ctx decls =

(** Syntactic equality (i.e. without β). *******)

-let rec eq meta_ctx e1 e2 = +let rec eq e1 e2 = e1 == e2 || - let eq = eq meta_ctx in match (e1, e2) with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 @@ -859,23 +858,23 @@ let rec eq meta_ctx e1 e2 = | (Some (_, e1), Some (_, e2)) -> eq e1 e2 | _ -> def1 = def2) | (Metavar (i1, s1, _, t1), Metavar (i2, s2, _, t2)) - -> i1 = i2 && eq t1 t2 && subst_eq meta_ctx s1 s2 + -> i1 = i2 && eq t1 t2 && subst_eq s1 s2 | _ -> false

-and subst_eq meta_ctx s1 s2 = +and subst_eq s1 s2 = s1 == s2 || match (s1, s2) with | (S.Identity, S.Identity) -> true | (S.Cons (e1, s1), S.Cons (e2, s2)) - -> eq meta_ctx e1 e2 && subst_eq meta_ctx s1 s2 + -> eq e1 e2 && subst_eq s1 s2 | (S.Shift (s1, o1), S.Shift (s2, o2)) -> let o = min o1 o2 in - subst_eq meta_ctx (S.mkShift s1 (o1 - o)) (S.mkShift s2 (o2 - o)) + subst_eq (S.mkShift s1 (o1 - o)) (S.mkShift s2 (o2 - o)) | (S.Shift (S.Cons (e1, s1), o1), S.Cons (e2, s2)) - -> eq meta_ctx (mkSusp e1 (S.shift o1)) e2 - && subst_eq meta_ctx (S.mkShift s1 o1) s2 + -> eq (mkSusp e1 (S.shift o1)) e2 + && subst_eq (S.mkShift s1 o1) s2 | (S.Cons (e1, s1), S.Shift (S.Cons (e2, s2), o2)) - -> eq meta_ctx e1 (mkSusp e2 (S.shift o2)) - && subst_eq meta_ctx s1 (S.mkShift s2 o2) + -> eq e1 (mkSusp e2 (S.shift o2)) + && subst_eq s1 (S.mkShift s2 o2) | _ -> false

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -99,14 +99,14 @@ let rec lctx_to_subst lctx = * and return an equivalent expression valid in the empty context. * By "closed" I mean that it only refers to elements of the context which * are LetDef. *) -let lexp_close meta_ctx lctx e = +let lexp_close lctx e = (* There are many different ways to skin this cat. * This is definitely not the best one: * - it inlines all the definitions everywhere they're used * - It turns the lctx (of O(log N) access time) into a subst * (of O(N) access time) * Oh well! *) - L.clean meta_ctx (mkSusp e (lctx_to_subst lctx)) + L.clean (mkSusp e (lctx_to_subst lctx))

(** Reduce to weak head normal form. @@ -125,7 +125,7 @@ let lexp_close meta_ctx lctx e = * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = +let lexp_whnf e (ctx : DB.lexp_context) : lexp = let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = match e with | Var v -> (match lookup_value ctx v with @@ -173,7 +173,8 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _, _) - -> (try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx + -> (let meta_ctx, _ = !global_substitution in + try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx with Not_found -> e)

(* FIXME: I'd really prefer to use "native" recursive substitutions, using @@ -189,16 +190,16 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = (** A very naive implementation of sets of pairs of lexps. *) type set_plexp = (lexp * lexp) list let set_empty : set_plexp = [] -let set_member_p meta_ctx (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool +let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool = assert (e1 == Lexp.hc e1); assert (e2 == Lexp.hc e2); try let _ = List.find (fun (e1', e2') - -> L.eq meta_ctx e1 e1' && L.eq meta_ctx e2 e2') + -> L.eq e1 e1' && L.eq e2 e2') s in true with Not_found -> false let set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp - = (* assert (not (set_member_p meta_ctx s e1 e2)); *) + = (* assert (not (set_member_p s e1 e2)); *) ((e1, e2) :: s) let set_shift_n (s : set_plexp) (n : U.db_offset) = List.map (let s = S.shift n in @@ -209,13 +210,12 @@ let set_shift s : set_plexp = set_shift_n s 1 (********* Testing if two types are "convertible" aka "equivalent" *********)

(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = - let conv_p' = conv_p' meta_ctx in - let e1' = lexp_whnf e1 ctx meta_ctx in - let e2' = lexp_whnf e2 ctx meta_ctx in +let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = + let e1' = lexp_whnf e1 ctx in + let e2' = lexp_whnf e2 ctx in e1' == e2' || let changed = not (e1 == e1' && e2 == e2') in - if changed && set_member_p meta_ctx vs e1' e2' then true else + if changed && set_member_p vs e1' e2' then true else let vs' = if changed then set_add vs e1' e2' else vs in let conv_p = conv_p' ctx vs' in match (e1', e2') with @@ -285,14 +285,15 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (* FIXME: Various missing cases, such as Case. *) | (_, _) -> false

-let conv_p meta_ctx (ctx : DB.lexp_context) e1 e2 +let conv_p (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true - else conv_p' meta_ctx ctx set_empty e1 e2 + else conv_p' ctx set_empty e1 e2

(********* Testing if a lexp is properly typed *********)

-(* Turn e into its canonical representation, which is basically the set - * of vars it references along with the number of `succ` applied to them. +(* Turn e (presumably of type TypeLevel) into its canonical representation, + * which is basically the set of vars it references along with the number of + * `succ` applied to them. * `c` is the maximum "constant" level that occurs in `e` * and `m` maps variable indices to the maxmimum depth at which they were * found. *) @@ -304,8 +305,11 @@ let level_canon e = | Var (_, i) -> let o = try VMap.find i m with Not_found -> -1 in if o < d then (c, VMap.add i d m) else acc | Metavar (i, _, _, _) - -> let o = try VMap.find (- i) m with Not_found -> -1 in - if o < d then (c, VMap.add (- i) d m) else acc + -> (let meta_ctx, _ = !global_substitution in + try canon (VMap.find i meta_ctx) d acc + with Not_found + -> let o = try VMap.find (- i) m with Not_found -> -1 in + if o < d then (c, VMap.add (- i) d m) else acc) | _ -> (max_int, m) in canon e 0 (0,VMap.empty)

@@ -315,22 +319,22 @@ let level_leq (c1, m1) (c2, m2) = && VMap.for_all (fun i d -> try d <= VMap.find i m2 with Not_found -> false) m1

-let rec mkSLlub meta_ctx ctx e1 e2 = - match (lexp_whnf e1 ctx meta_ctx, lexp_whnf e2 ctx meta_ctx) with +let rec mkSLlub ctx e1 e2 = + match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with | (SortLevel SLz, e2) -> e2 | (e1, SortLevel SLz) -> e1 | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) - -> mkSortLevel (SLsucc (mkSLlub meta_ctx ctx e1 e2)) + -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') - -> let ce1 = level_canon (L.clean meta_ctx e1') in - let ce2 = level_canon (L.clean meta_ctx e2') in + -> let ce1 = level_canon (L.clean e1') in + let ce2 = level_canon (L.clean e2') in if level_leq ce1 ce2 then e1 else if level_leq ce2 ce1 then e2 else mkSortLevel (SLlub (e1, e2))

-let sort_compose meta_ctx ctx l s1 s2 = +let sort_compose ctx l s1 s2 = match s1, s2 with - | (Stype l1, Stype l2) -> Stype (mkSLlub meta_ctx ctx l1 l2) + | (Stype l1, Stype l2) -> Stype (mkSLlub ctx l1 l2) | ( (StypeLevel, Stype _) | (StypeLevel, StypeOmega) (* This is probably safe, but I don't think it adds much power nor @@ -347,19 +351,19 @@ let dbset_push ak erased = if ak = P.Aerasable then DB.set_set 0 nerased else nerased

(* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check' meta_ctx erased ctx e = - let check = check' meta_ctx in +let rec check' erased ctx e = + let check = check' in let assert_type ctx e t t' = - if conv_p meta_ctx ctx t t' then () + if conv_p ctx t t' then () else (U.msg_error "TC" (lexp_location e) ("Type mismatch for " - ^ lexp_string (L.clean meta_ctx e) ^ " : " - ^ lexp_string (L.clean meta_ctx t) ^ " != " - ^ lexp_string (L.clean meta_ctx t')); + ^ lexp_string (L.clean e) ^ " : " + ^ lexp_string (L.clean t) ^ " != " + ^ lexp_string (L.clean t')); (* U.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in - (match lexp_whnf s ctx meta_ctx with + (match lexp_whnf s ctx with | Sort _ -> () | _ -> U.msg_error "TC" (lexp_location t) ("Not a proper type: " ^ lexp_string t)); @@ -432,12 +436,12 @@ let rec check' meta_ctx erased ctx e = * should ignore `k2` and return TypeOmega anyway. *) let k2 = check_type (DB.set_sink 1 erased) nctx t2 in let k2 = mkSusp k2 (S.substitute impossible) in - match lexp_whnf k1 ctx meta_ctx, lexp_whnf k2 ctx meta_ctx with + match lexp_whnf k1 ctx, lexp_whnf k2 ctx with | (Sort (_, s1), Sort (_, s2)) (* FIXME: fix scoping of `k2` and `s2`. *) -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel then k2 - else mkSort (l, sort_compose meta_ctx ctx l s1 s2) + else mkSort (l, sort_compose ctx l s1 s2) | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) "Not a proper type"; mkSort (l, StypeOmega)) @@ -445,7 +449,7 @@ let rec check' meta_ctx erased ctx e = "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) - -> ((match lexp_whnf (check_type DB.set_empty ctx t) ctx meta_ctx with + -> ((match lexp_whnf (check_type DB.set_empty ctx t) ctx with | Sort _ -> () | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); @@ -459,7 +463,7 @@ let rec check' meta_ctx erased ctx e = (fun ft (ak,arg) -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) ctx arg in - match lexp_whnf ft ctx meta_ctx with + match lexp_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (U.msg_error "TC" (lexp_location arg) @@ -484,13 +488,13 @@ let rec check' meta_ctx erased ctx e = (fun (level, ctx) (ak, v, t) -> (* FIXME: DB.set_empty seems wrong! *) (match lexp_whnf (check_type DB.set_empty ctx t) - ctx meta_ctx with + ctx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') (* FIXME: scoping of level vars! *) - -> mkSLlub meta_ctx ctx level level' + -> mkSLlub ctx level level' | tt -> U.msg_error "TC" (lexp_location t) ("Field type " ^ lexp_string t @@ -515,9 +519,9 @@ let rec check' meta_ctx erased ctx e = -> let call_split e = match e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = lexp_whnf (check erased ctx e) ctx meta_ctx in + let etype = lexp_whnf (check erased ctx e) ctx in let it, aargs = call_split etype in - (match lexp_whnf it ctx meta_ctx, aargs with + (match lexp_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -569,7 +573,7 @@ let rec check' meta_ctx erased ctx e = | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx meta_ctx with + -> (match lexp_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in @@ -602,13 +606,14 @@ let rec check' meta_ctx erased ctx e = ^ lexp_string t); DB.type_int)) | Metavar (idx, s, _, t) - -> (try let e = push_susp (L.VMap.find idx meta_ctx) s in + -> (try let meta_ctx, _ = !global_substitution in + let e = push_susp (L.VMap.find idx meta_ctx) s in let t' = check erased ctx e in assert_type ctx e t' t with Not_found -> ()); t

-let check meta_ctx = check' meta_ctx DB.set_empty +let check = check' DB.set_empty

(** Compute the set of free (meta)variables. **)

@@ -708,8 +713,7 @@ let rec fv (e : lexp) : (DB.set * mv_set) = (** Finding the type of a expression. **) (* This should never signal any warning/error. *)

-let rec get_type meta_ctx ctx e = - let get_type = get_type meta_ctx in +let rec get_type ctx e = match e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int @@ -734,11 +738,11 @@ let rec get_type meta_ctx ctx e = * should ignore `k2` and return TypeOmega anyway. *) let k2 = get_type nctx t2 in let k2 = mkSusp k2 (S.substitute impossible) in - match lexp_whnf k1 ctx meta_ctx, lexp_whnf k2 ctx meta_ctx with + match lexp_whnf k1 ctx, lexp_whnf k2 ctx with | (Sort (_, s1), Sort (_, s2)) -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel then k2 - else mkSort (l, sort_compose meta_ctx ctx l s1 s2) + else mkSort (l, sort_compose ctx l s1 s2) | _ -> DB.type0) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (ak, Some v, t, l, @@ -748,7 +752,7 @@ let rec get_type meta_ctx ctx e = -> let ft = get_type ctx f in List.fold_left (fun ft (ak,arg) - -> match lexp_whnf ft ctx meta_ctx with + -> match lexp_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) @@ -764,14 +768,13 @@ let rec get_type meta_ctx ctx e = let level, _ = List.fold_left (fun (level, ctx) (ak, v, t) -> - (match lexp_whnf (get_type ctx t) - ctx meta_ctx with + (match lexp_whnf (get_type ctx t) ctx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') (* FIXME: scoping of level vars! *) - -> mkSLlub meta_ctx ctx level level' + -> mkSLlub ctx level level' | tt -> level), DB.lctx_extend ctx v Variable t) (level, ctx) @@ -786,7 +789,7 @@ let rec get_type meta_ctx ctx e = tct | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx meta_ctx with + -> (match lexp_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in

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

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/aaa414b231a5f51452e45b4ea6e8a654601c... You're receiving this email because of your account on gitlab.com.