Ismaila FALL pushed to branch location-sinfo at Stefan / Typer

Commits: b638446c by “falismai@iro.umontreal.ca” at 2022-05-31T22:03:08+00:00 Suppression du dossier idea

- - - - -

4 changed files:

- src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== src/elab.ml ===================================== @@ -176,7 +176,7 @@ let elab_check_proper_type (ctx : elab_context) ltp var =

let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in - let loc = sinfo_location lxp in + let loc = lexp_sinfo lxp in

let ltype' = try OL.check lctx lxp with e -> match e with @@ -652,7 +652,7 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype = | (e, Inferred t) -> (e, t)

and elab_special_form ctx f args ot = - let loc = sinfo_location f in + let loc = lexp_sinfo f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) @@ -663,7 +663,7 @@ and elab_special_form ctx f args ot = sform_dummy_ret ctx loc

and elab_special_decl_form ctx f args = - let loc = sinfo_location f in + let loc = lexp_sinfo f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) @@ -675,9 +675,9 @@ and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow (_, ((Aerasable | Aimplicit) as ak), (_, v), t1, t2) - -> let arg = newInstanceMetavar ctx (sinfo_location e, v) t1 in + -> let arg = newInstanceMetavar ctx (lexp_sinfo e, v) t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) - | _ -> (mkCall (sinfo_location e, e, List.rev args), t) + | _ -> (mkCall (lexp_sinfo e, e, List.rev args), t) in instantiate t []

and resolve_instances e = @@ -718,7 +718,7 @@ and infer_type pexp ectx (var: vname) = | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. * Maybe it's actually correct?! *) - let l = sinfo_location s in + let l = lexp_sinfo s in match Unif.unify (mkSort (l, Stype (newMetalevel (ectx_to_lctx ectx) @@ -1006,7 +1006,7 @@ and elab_macro_call (ot : ltype option) : lexp * sform_type =

- let location = sinfo_location func in + let location = lexp_sinfo func in let t = match ot with | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location @@ -1029,7 +1029,7 @@ and elab_macro_call

(* Identify Call Type and return processed call. *) and elab_call ctx (func, ltp) (sargs: sexp list) = - let loc = sinfo_location func in + let loc = lexp_sinfo func in

let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in @@ -1114,7 +1114,7 @@ and lexp_parse_inductive ctors ctx = acc impossible in let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t _l e - -> mkArrow (sinfo_location altacc, Aerasable, vname, t, e)) + -> mkArrow (lexp_sinfo altacc, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *)

===================================== src/lexp.ml ===================================== @@ -516,30 +516,30 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) * S.sink (fun l i -> mkVar (l, i)) l s *)

-let rec sinfo_location s = +let rec lexp_sinfo s = match lexp_lexp' s with | Sort (l,_) -> l - | SortLevel (SLsucc s) -> sinfo_location s - | SortLevel (SLlub (s, _)) -> sinfo_location s + | SortLevel (SLsucc s) -> lexp_sinfo s + | SortLevel (SLlub (s, _)) -> lexp_sinfo s | SortLevel SLz -> dummy_sinfo | Imm s -> s | Var ((l,_),_) -> l - | Builtin ((l, _), _) -> Symbol (l, "") + | Builtin ((l, _), _) -> epsilon l | Let (l,_,_) -> l | Arrow (l,_,_,_,_) -> l | Lambda (_,(l,_),_,_) -> l - | Call (_,f,_) -> sinfo_location f + | Call (_,f,_) -> lexp_sinfo f | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> Symbol (l, "") + | Cons (_,(l,_)) -> epsilon l | Case (l,_,_,_,_) -> l - | Susp (s, _) -> sinfo_location s + | Susp (s, _) -> lexp_sinfo s (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l | Proj (l,_,_) -> l

let lexp_location e = - sexp_location (sinfo_location e) + sexp_location (lexp_sinfo e)

(********* Normalizing a term *********)

===================================== src/opslexp.ml ===================================== @@ -781,7 +781,7 @@ and check'' erased ctx e = mkSort (l, Stype level) | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in - mkArrow (sinfo_location t, ak, v, t, + mkArrow (lexp_sinfo t, ak, v, t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) args) in @@ -937,7 +937,7 @@ and check'' erased ctx e = mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (sinfo_location ftype, ak, vd, ftype, + -> mkArrow (lexp_sinfo ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with @@ -1207,7 +1207,7 @@ and get_type ctx e = cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> mkArrow (sinfo_location t, ak, v, t, + -> mkArrow (lexp_sinfo t, ak, v, t, arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct @@ -1228,7 +1228,7 @@ and get_type ctx e = mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (sinfo_location ftype, ak, vd, ftype, + -> mkArrow (lexp_sinfo ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with

===================================== src/unification.ml ===================================== @@ -146,7 +146,7 @@ let common_subset ctx s1 s2 = && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2)) then match loop s1' s2' o1 o2 1 with | S.Identity 1 -> S.Identity o (* Optimization! *) - | s' -> S.Cons (mkVar ((sinfo_location le1, None), 0), + | s' -> S.Cons (mkVar ((lexp_sinfo le1, None), 0), s', o) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that

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