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

Commits: c422f432 by “falismai@iro.umontreal.ca” at 2022-05-26T18:51:50+00:00 [OK] Compilateur

- - - - -

21 changed files:

- + Int - debug_util.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/eval.ml - src/instargs.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/positivity.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/env_test.ml - tests/instargs_test.ml - tests/positivity_test.ml - tests/unify_test.ml

Changes:

===================================== Int ===================================== @@ -0,0 +1,28 @@ +btl/builtins.typer:Integer->Int = Built-in "Integer->Int" : Integer -> Int; +btl/builtins.typer:Integer->String = Built-in "Integer->String" : Integer -> String; +btl/pervasive.typer: | nil => (Integer->Int 0) +btl/pervasive.typer: (Int_+ (Integer->Int 1) (List_length tl)); +btl/pervasive.typer: => case Int_<= n (Integer->Int 0) +btl/pervasive.typer: | false => List_nth (Int_- n (Integer->Int 1)) xs d; +btl/pervasive.typer: | cons x xs => cons (f x i) (helper f (Int_+ i (Integer->Int 1)) xs); +btl/pervasive.typer:in helper f (Integer->Int 0) xs; +btl/pervasive.typer:List_empty xs = Int_eq (List_length xs) (Integer->Int 0); +btl/pervasive.typer: (cons (List_nth (Integer->Int 1) ss Sexp_error) nil))); +btl/pervasive.typer: head = List_nth (Integer->Int 0) head-pair Sexp_error; +btl/pervasive.typer: type-type = List_nth (Integer->Int 1) head-pair Sexp_error; +btl/pervasive.typer: | vnil (p ::: Eq n (Integer->Int 0)) +btl/pervasive.typer: | vcons a (LList a ?n1) (p ::: Eq n (Int_+ ?n1 (Integer->Int 1))); +btl/pervasive.typer: let e1 = List_nth (Integer->Int 0) args Sexp_error; +btl/pervasive.typer: e2 = List_nth (Integer->Int 1) args Sexp_error; +btl/pervasive.typer: e3 = List_nth (Integer->Int 2) args Sexp_error; +btl/pervasive.typer:in case (Int_eq r (Integer->Int -1)) +btl/poly-lits.typer:IntFromInteger = mkFromInteger Integer->Int; +btl/tuple.typer: elem-sym = Sexp_symbol (String_concat "%" (Integer->String n)); +samples/nats.typer:Integer->Nat : Integer -> Nat; +samples/nats.typer:Integer->Nat i = +samples/nats.typer: S (Integer->Nat (Integer_- i 1)) +samples/nats.typer:NatFromInteger = mkFromInteger Integer->Nat; +src/eval.ml: let name = "Integer->Int" in +src/eval.ml: | _ -> error loc "Integer->String expects one Integer argument" +src/eval.ml: ("Integer->String", integer_to_string, 1); +tests/eval_test.ml:intFromIntegerCoercion = mkCoercible (Integer->Int);

===================================== debug_util.ml ===================================== @@ -59,6 +59,7 @@ open Debruijn open Env

let dloc = dummy_location +let dsinfo = DB.dsinfo let dummy_decl = Imm(String(dloc, "Dummy"))

let discard _v = () @@ -306,7 +307,7 @@ let main () = let main = (senv_lookup "main" nctx) in

(* get main body *) - let body = (get_rte_variable (dloc, Some "main") main rctx) in + let body = (get_rte_variable (dsinfo, Some "main") main rctx) in

(* eval main *) print_eval_result 1 body

===================================== src/builtin.ml ===================================== @@ -98,9 +98,10 @@ let set_predef name lexp

(* Builtin types *) let dloc = DB.dloc +let dsinfo = DB.dsinfo

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

let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx

@@ -159,7 +160,7 @@ let register_builtin_csts () = add_builtin_cst "Eq.refl" DB.eq_refl

let type_arrow_0 = - mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) + mkArrow (dsinfo, Anormal, (dsinfo, None), DB.type0, DB.type0)

let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in

===================================== src/debruijn.ml ===================================== @@ -36,6 +36,7 @@ module Str = Str

open Util

+open Sexp

open Lexp

@@ -117,45 +118,47 @@ let set_ascending_seq ((o, m) : set) : int Seq.t = * ---------------------------------- *)

let dloc = dummy_location -let type_level_sort = mkSort (dloc, StypeLevel) -let sort_omega = mkSort (dloc, StypeOmega) +let dsinfo = dummy_sinfo + +let type_level_sort = mkSort (dsinfo, StypeLevel) +let sort_omega = mkSort (dsinfo, StypeOmega) let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) -let type0 = mkSort (dloc, Stype level0) -let type1 = mkSort (dloc, Stype level1) -let type2 = mkSort (dloc, Stype level2) +let type0 = mkSort (dsinfo, Stype level0) +let type1 = mkSort (dsinfo, Stype level1) +let type2 = mkSort (dsinfo, Stype level2) let type_int = mkBuiltin ((dloc, "Int"), type0) let type_integer = mkBuiltin ((dloc, "Integer"), type0) let type_float = mkBuiltin ((dloc, "Float"), type0) let type_string = mkBuiltin ((dloc, "String"), type0) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, - type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 1), dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + mkArrow (dsinfo, Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 0), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 1), + mkSort (dsinfo, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let eq_refl = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - let xv = (dloc, Some "x") in + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + let xv = (dsinfo, Some "x") in mkBuiltin ((dloc, "Eq.refl"), - mkArrow (Aerasable, lv, - type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Aerasable, xv, - mkVar (tv, 0), dloc, - mkCall (type_eq, + mkArrow (dsinfo, Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Aerasable, xv, + mkVar (tv, 0), + mkCall (dsinfo, type_eq, [Aerasable, mkVar (lv, 2); Aerasable, mkVar (tv, 1); Anormal, mkVar (xv, 0); @@ -465,7 +468,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = else fun () -> summarize_lctx ctx dbi in fatal - ~loc ~print_action + ~loc:(sexp_location loc) ~print_action ({|DeBruijn index %d refers to wrong name. |} ^^ {|Expected: "%s" got "%s"|}) dbi ename name @@ -475,7 +478,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = with | Not_found -> fatal - ~loc "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) + ~loc:(sexp_location loc) "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename)

let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in

===================================== src/debug.ml ===================================== @@ -121,7 +121,7 @@ let debug_lexp_decls decls = List.iter (fun e -> let ((loc, _name), lxp, _ltp) = e in

- printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string loc); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string (sexp_location loc));

let str = lexp_str_decls (!debug_ppctx) [e] in

@@ -137,7 +137,7 @@ let debug_lexp_decls decls =

let str = match str with | scd :: tl - -> printf " FILE: %-25s : %s\n" loc.file scd; + -> printf " FILE: %-25s : %s\n" (sexp_location loc).file scd; tl | _ -> [] in

===================================== src/elab.ml ===================================== @@ -65,6 +65,7 @@ open Printf

(* dummies *) let dloc = dummy_location +let dsinfo = DB.dsinfo

let parsing_internals = ref false let btl_folder = @@ -108,11 +109,11 @@ type sform_type = | Lazy (* Hasn't looked as the requested type, nor inferred a type. *)

type special_forms_map = - (elab_context -> location -> sexp list -> ltype option + (elab_context -> sinfo -> sexp list -> ltype option -> (lexp * sform_type)) SMap.t

type special_decl_forms_map = - (elab_context -> location -> sexp list -> elab_context) SMap.t + (elab_context -> sinfo -> sexp list -> elab_context) SMap.t

let special_forms : special_forms_map ref = ref SMap.empty let special_decl_forms : special_decl_forms_map ref = ref SMap.empty @@ -141,7 +142,7 @@ let sform_default_ectx = ref empty_elab_context * (i.e. errors signalled here correspond to internal errors rather than * to errors in the user's code). *)

-let elab_check_sort (ctx : elab_context) lsort var ltp = +let elab_check_sort (ctx : elab_context) lsort (var: vname) ltp = match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) @@ -152,9 +153,9 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = | _ -> let tystr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with - | (l, None) -> lexp_error l ltp {|"%s" is not a proper type|} tystr + | (l, None) -> lexp_error (sexp_location l) ltp {|"%s" is not a proper type|} tystr | (l, Some name) - -> lexp_error l ltp {|Type of "%s" is not a proper type: %s|} name tystr + -> lexp_error (sexp_location l) ltp {|Type of "%s" is not a proper type: %s|} name tystr

let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp @@ -175,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 = lexp_location lxp in + let loc = sinfo_location lxp in

let ltype' = try OL.check lctx lxp with e -> match e with @@ -187,7 +188,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = print_lexp_ctx (ectx_to_lctx ctx); print_newline () ) - ~loc + ~loc:(sexp_location loc) "Error while type-checking"; raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' @@ -195,7 +196,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = | e -> info ~print_action:(lexp_print_details lxp) - ~loc + ~loc:(sexp_location loc) "Exception while conversion-checking types: %s and %s" (lexp_string ltype) (lexp_string ltype'); @@ -211,7 +212,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = " because"; lexp_string ltype' ^ " != " ^ lexp_string ltype ]) - ~loc + ~loc:(sexp_location loc) "Type check error: ¡¡ctx_define error!!"

let ctx_extend (ctx: elab_context) (var : vname) def ltype = @@ -341,7 +342,7 @@ let sdform_define_operator (ctx : elab_context) loc sargs : elab_context = | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ - -> sexp_error loc "define-operator expects 3 argument"; ctx + -> sexp_error (sexp_location loc) "define-operator expects 3 argument"; ctx

let sform_dummy_ret ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in @@ -361,7 +362,7 @@ let elab_varref ctx (loc, name) if ((List.length xs) > 0) then ". Did you mean: " ^ (String.concat " or " xs) ^" ?" else "" in - sexp_error loc {|The variable "%s" was not declared%s|} name relateds; + sexp_error (sexp_location loc) {|The variable "%s" was not declared%s|} name relateds; sform_dummy_ret ctx loc)

(* Turn metavar into plain vars after generalization. @@ -490,12 +491,12 @@ let meta_to_var ids (e : lexp) = loop (o' + o) t) :: defs)) defs (len, []) in mkLet (l, ndefs, loop (len + o) e) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, loop o t1, loop (1 + o) t2) | Lambda (ak, v, t, e) -> mkLambda (ak, v, loop o t, loop (1 + o) e) - | Call (f, args) - -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) + | Call (l, f, args) + -> mkCall (l, loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) | Inductive (l, label, args, cases) -> let alen = List.length args in let (_, nargs) @@ -599,17 +600,17 @@ let wrapLambda ne vname t _l e = mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e)

let elab_p_id ((l,name) : symbol) : vname = - (l, match name with "_" -> None | _ -> Some name) + (Symbol (l, name), match name with "_" -> None | _ -> Some name)

(* Infer or check, as the case may be. *) let rec elaborate ctx se ot = let (e, res_t) = match se with (* Rewrite SYM to `typer-identifier SYM`. *) - | Symbol ((loc, name) as id) + | Symbol ((loc, name) as _id) -> if not (name = "typer-identifier") then elaborate ctx (Node (Symbol (loc, "typer-identifier"), [se])) ot (* Break the inf-recursion! *) - else elab_varref ctx id + else elab_varref ctx (se, name)

(* Rewrite IMM to `typer-immediate IMM`. *) | (Integer _ | Float _ | String _ | Block _) @@ -651,32 +652,32 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype = | (e, Inferred t) -> (e, t)

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

| _ - -> lexp_error loc f "Unknown special-form: %s" (lexp_string f); + -> lexp_error (sexp_location loc) f "Unknown special-form: %s" (lexp_string f); sform_dummy_ret ctx loc

and elab_special_decl_form ctx f args = - let loc = lexp_location f in + let loc = sinfo_location f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) (get_special_decl_form name) ctx loc args - | _ -> lexp_error loc f "Unknown special-decl-form: %s" (lexp_string f); ctx + | _ -> lexp_error (sexp_location loc) f "Unknown special-decl-form: %s" (lexp_string f); ctx

(* Build the list of implicit arguments to instantiate. *) 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 (lexp_location e, v) t1 in + | Arrow (_, ((Aerasable | Aimplicit) as ak), (_, v), t1, t2) + -> let arg = newInstanceMetavar ctx (sinfo_location e, v) t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args), t) + | _ -> (mkCall (sinfo_location e, e, List.rev args), t) in instantiate t []

and resolve_instances e = @@ -686,7 +687,7 @@ and resolve_instances_and_generalize ctx e = resolve_instances e; generalize ctx e

-and sdform_typeclass (ctx : elab_context) (_l : location) sargs +and sdform_typeclass (ctx : elab_context) (_l : sinfo) sargs : elab_context = let make_typeclass ctx sarg = let (t, _) = infer sarg ctx in @@ -694,7 +695,7 @@ and sdform_typeclass (ctx : elab_context) (_l : location) sargs in List.fold_left make_typeclass ctx sargs

-and sdform_instance (inst : bool) (ctx : elab_context) (_l : location) sargs +and sdform_instance (inst : bool) (ctx : elab_context) (_l : sinfo) sargs : elab_context = let make_instance ctx sarg = let (lxp, _) = infer sarg ctx in @@ -704,7 +705,7 @@ and sdform_instance (inst : bool) (ctx : elab_context) (_l : location) sargs "Only variables can be instances"; ctx) in List.fold_left make_instance ctx sargs

-and infer_type pexp ectx var = +and infer_type pexp ectx (var: vname) = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) @@ -717,7 +718,7 @@ and infer_type pexp ectx var = | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. * Maybe it's actually correct?! *) - let l = lexp_location s in + let l = sinfo_location s in match Unif.unify (mkSort (l, Stype (newMetalevel (ectx_to_lctx ectx) @@ -729,15 +730,15 @@ and infer_type pexp ectx var = -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with | (l, None) - -> lexp_error l t {|"%s" is not a proper type|} typestr + -> lexp_error (sexp_location l) t {|"%s" is not a proper type|} typestr | (l, Some name) -> lexp_error - l t {|Type of "%s" is not a proper type: %s|} name typestr) + (sexp_location l) t {|Type of "%s" is not a proper type: %s|} name typestr) | [] -> ()); t

and lexp_let_decls declss (body: lexp) _ctx = - List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) + List.fold_right (fun decls lxp -> mkLet (dsinfo, decls, lxp)) declss body

and unify_with_arrow ctx tloc lxp kind var aty @@ -747,11 +748,11 @@ and unify_with_arrow ctx tloc lxp kind var aty let nctx = ectx_extend ctx var Variable arg in let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in - let arrow = mkArrow (kind, var, arg, l, body) in + let arrow = mkArrow (l, kind, var, arg, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error - tloc lxp {|Types:\n %s\n and:\n %s\n do not match!|} + (sexp_location tloc) lxp {|Types:\n %s\n and:\n %s\n do not match!|} (lexp_string t1) (lexp_string t2); (mkDummy_type ctx l, mkDummy_type nctx l) | [] -> arg, body @@ -785,7 +786,7 @@ and unify_or_error lctx lxp ?lxp_name expect actual = and check_inferred ctx e inferred_t t = let (e, inferred_t) = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit), _, _, _, _) + | Arrow (_, (Aerasable | Aimplicit), _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in unify_or_error (ectx_to_lctx ctx) e t inferred_t; @@ -799,7 +800,7 @@ and check_case rtype (loc, target, ppatterns) ctx =

let uniqueness_warn pat = warning - ~loc:(pexp_pat_location pat) + ~loc:(sexp_location (pexp_pat_location pat)) "Pattern %s is a duplicate. It will override a previous pattern." (pat_string pat) in @@ -821,7 +822,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match Unif.unify actual expected (ectx_to_lctx ctx) with | (_::_) -> lexp_error - loc lctor {|Expected pattern of type "%s", but got "%s"|} + (sexp_location loc) lctor {|Expected pattern of type "%s", but got "%s"|} (lexp_string expected) (lexp_string actual) | [] -> () in match !it_cs_as with @@ -840,12 +841,12 @@ and check_case rtype (loc, target, ppatterns) ctx = (S.identity, []) fargs in let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); + ltarget := check_inferred ctx tlxp tltp (mkCall (loc, it', args)); it_cs_as := Some (it', cs, args); (cs, args) | _ -> let call_split e = match OL.lexp'_whnf e (ectx_to_lctx ctx) with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (e,[]) in let (it, targs) = call_split tltp in unify_ind it it'; @@ -875,7 +876,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let tlxp' = shift_to_extended_ctx nctx tlxp in let tltp' = shift_to_extended_ctx nctx tltp in let tlvl' = shift_to_extended_ctx nctx tlvl in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (loc, DB.type_eq, [(Aerasable, tlvl'); (* Typelevel *) (Aerasable, tltp'); (* Inductive type *) (Anormal, head_lexp); (* Lexp of the branch head *) @@ -956,7 +957,7 @@ and check_case rtype (loc, target, ppatterns) ctx = sexp_error l {|Duplicate explicit field "%s"|} fname; make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, fname, fty)::cargs - -> let var = (loc, None) in + -> let var = ((Symbol(loc, "")), None) in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in if ak = Anormal then sexp_error @@ -969,15 +970,15 @@ and check_case rtype (loc, target, ppatterns) ctx = let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in let head_lexp_ctor = shift_to_extended_ctx nctx - (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + (mkCall (dsinfo, lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in let head_lexp_args = List.mapi (fun i (ak, vname) -> (ak, mkVar (vname, List.length fargs - i - 1))) fargs in - let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + let head_lexp = mkCall (dsinfo, head_lexp_ctor, head_lexp_args) in let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in - SMap.add cons_name (loc, fargs, lexp) lbranches, + SMap.add cons_name (Symbol(loc, ""), fargs, lexp) lbranches, dflt (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it * and try again with the result. *) @@ -988,7 +989,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) -> if Eval.constructor_p name ctx then - add_branch (Symbol (l, name)) [] + add_branch (Symbol (sexp_location l, name)) [] else add_default var (* A named default branch. *)

| Ppatcons (pctor, pargs) -> add_branch pctor pargs in @@ -1005,7 +1006,7 @@ and elab_macro_call (ot : ltype option) : lexp * sform_type =

- let location = lexp_location func in + let location = sinfo_location func in let t = match ot with | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location @@ -1014,26 +1015,26 @@ and elab_macro_call

if !macro_tracing_enabled then - (trace_macro ~location {|expanding: %s|} (lexp_string func); + (trace_macro ~location:(sexp_location location) {|expanding: %s|} (lexp_string func); List.iteri (fun i arg -> - arg |> sexp_string |> trace_macro ~location {|input %d: %s|} i) + arg |> sexp_string |> trace_macro ~location:(sexp_location location) {|input %d: %s|} i) args);

let sxp = lexp_expand_macro location func args ctx (Some t) in if !macro_tracing_enabled - then trace_macro ~location {|output: %s|} (sexp_string sxp); + then trace_macro ~location:(sexp_location location) {|output: %s|} (sexp_string sxp);

elaborate ctx sxp ot

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

let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in match sargs, lexp_lexp' ltp' with - | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type) + | _, Arrow (_, ak, (_, Some aname), arg_type, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in let larg = check sarg arg_type ctx in @@ -1042,7 +1043,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (L.mkSusp ret_type (S.substitute larg))

| (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, - Arrow (ak, _, arg_type, _, ret_type) + Arrow (_, ak, _, arg_type, ret_type) when (aname = "_") (* Explicit-implicit argument. *) -> let larg = check sarg arg_type ctx in @@ -1062,11 +1063,11 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = handle_fun_args largs sargs pending ltp

(* Aerasable *) - | _, Arrow ((Aerasable | Aimplicit) as ak, (_l,v), arg_type, _, ret_type) + | _, Arrow (_, ((Aerasable | Aimplicit) as ak), (_l,v), arg_type, ret_type) (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) - -> let arg_loc = try sexp_location (List.hd sargs) with _ -> loc in + -> let arg_loc = try (List.hd sargs) with _ -> loc in let larg = newInstanceMetavar ctx (arg_loc, v) arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) @@ -1083,16 +1084,16 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =

| sarg :: sargs, _ -> let (arg_type, ret_type) = match lexp_lexp' ltp' with - | Arrow (ak, _, arg_type, _, ret_type) + | Arrow (_, ak, _, arg_type, ret_type) -> assert (ak = Anormal); (arg_type, ret_type) - | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Anormal (dloc, None) None in + | _ -> unify_with_arrow ctx (sarg) + ltp' Anormal (sarg, None) None in let larg = check sarg arg_type ctx in 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 - (mkCall (func, List.rev largs), Inferred ret_type) + (mkCall (loc, func, List.rev largs), Inferred ret_type)

(* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -1109,11 +1110,11 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> mkArrow (ak, n, t, dummy_location, aa)) + -> mkArrow (dsinfo, ak, n, t, aa)) acc impossible in let g = resolve_instances_and_generalize nctx altacc in - let altacc' = g (fun _ne vname t l e - -> mkArrow (Aerasable, vname, t, l, e)) + let altacc' = g (fun _ne vname t _l e + -> mkArrow (sinfo_location altacc, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1121,7 +1122,7 @@ and lexp_parse_inductive ctors ctx = (* Convert the Lexp back into a list of fields. *) let rec loop e = match lexp_lexp' e with - | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) + | Arrow (_, ak, n, t, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in loop altacc' | (kind, var, exp)::tl @@ -1189,15 +1190,15 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in

(* FIXME: Make a proper `Var`. *) - let value = EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) + let value = EV.eval_call (sexp_location loc) (EL.Var ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args in match value with | Vcommand cmd -> (match cmd () with | Vsexp sxp -> sxp - | v -> value_fatal loc v "Macro `%s` should return an IO sexp" + | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO sexp" (lexp_string macro_funct)) - | v -> value_fatal loc v "Macro `%s` should return an IO" + | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO" (lexp_string macro_funct)

@@ -1222,7 +1223,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (* Preserve the new operators added to nctx. *) let (declmap) = List.fold_right - (fun ((l, vname), sexp) (map) -> + (fun ((_l, vname), sexp) (map) -> let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with @@ -1236,7 +1237,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) * proper format, e.g. for `lctx_view`! *) let e = check sexp adjusted_t nctx in (* let d = (v', LetDef (i + 1, e), t) in *) - (IMap.add i ((l, Some vname), e, t) map) + (IMap.add i ((sexp, Some vname), e, t) map) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in @@ -1273,13 +1274,13 @@ and infer_and_generalize_type (ctx : elab_context) se name = *) let rec strip_rettype t = match lexp_lexp' t with - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, t1, l, strip_rettype t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, t1, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = resolve_instances_and_generalize nctx (strip_rettype t) in g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) + -> mkArrow (Symbol(l,""), Aerasable, name, t, e)) t

and infer_and_generalize_def (ctx : elab_context) se = @@ -1288,8 +1289,8 @@ and infer_and_generalize_def (ctx : elab_context) se = let g = resolve_instances_and_generalize nctx e in let e' = g wrapLambda e in let t' = g (fun ne name t _l e - -> mkArrow ((if ne then Aimplicit else Aerasable), - name, t, sexp_location se, e)) + -> mkArrow (se, (if ne then Aimplicit else Aerasable), + name, t, e)) t in (e', t')

@@ -1333,7 +1334,7 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in + -> let ltp = infer_and_generalize_type nctx stp (Symbol(loc, ""), Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1354,7 +1355,7 @@ and lexp_decls_1 pending_defs then (error ~loc {|Variable "%s" already defined!|} vname; recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + else recur [] (ectx_extend nctx (Symbol(loc, ""), Some vname) ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs | _ @@ -1366,13 +1367,13 @@ and lexp_decls_1 | Some (Node (Symbol (loc, "_=_") as head, args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol ((l, vname)); sexp] + | [Symbol ((_l, vname)); sexp] when SMap.is_empty pending_decls -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (l, Some vname) in + let var = (sexp, Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, @@ -1418,7 +1419,7 @@ and lexp_decls_1 else if (OL.conv_p lctx t (BI.get_predef "Macro" nctx)) then (* expand macro and get the generated declarations *) let lxp, _ltp = infer sxp nctx in - let sdecl' = lexp_expand_macro (sexp_location sxp) lxp sargs nctx None in + let sdecl' = lexp_expand_macro sxp lxp sargs nctx None in recur [sdecl'] nctx pending_decls pending_defs else ( error ~loc:(sexp_location sxp) "Invalid declaration syntax"; @@ -1465,9 +1466,9 @@ and sform_declexpr ctx loc sargs _ot = | [e] when is_var e -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; + | None -> error ~loc:(sexp_location loc) "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; + | _ -> error ~loc:(sexp_location loc) "declexpr expects one argument"; sform_dummy_ret ctx loc

@@ -1475,7 +1476,7 @@ let sform_decltype ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc "decltype expects one argument"; + | _ -> error ~loc:(sexp_location loc) "decltype expects one argument"; sform_dummy_ret ctx loc

@@ -1492,18 +1493,18 @@ let sform_built_in ctx loc sargs ot = * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp') in + let bi = mkBuiltin ((sexp_location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then - sexp_error loc {|Unknown built-in "%s"|} name; + sexp_error (sexp_location loc) {|Unknown built-in "%s"|} name; BI.add_builtin_cst name bi; (bi, Checked) - | None -> error ~loc "Built-in's type not provided by context!"; + | None -> error ~loc:(sexp_location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc)

- | true, _ -> error ~loc "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc:(sexp_location loc) "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc

- | false, _ -> error ~loc "Use of `Built-in` in user code"; + | false, _ -> error ~loc:(sexp_location loc) "Use of `Built-in` in user code"; sform_dummy_ret ctx loc

let sform_datacons ctx loc sargs _ot = @@ -1512,9 +1513,9 @@ let sform_datacons ctx loc sargs _ot = -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy)

- | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; + | [_;_] -> sexp_error (sexp_location loc) "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc - | _ -> sexp_error loc "##constr requires two arguments"; + | _ -> sexp_error (sexp_location loc) "##constr requires two arguments"; sform_dummy_ret ctx loc

let elab_colon_to_ak k = match k with @@ -1525,22 +1526,22 @@ let elab_colon_to_ak k = match k with 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) - | _ -> (Anormal, (sexp_location s, None), s) + | _ -> (Anormal, (s, None), s)

let elab_typecons_arg arg : (arg_kind * vname * sexp option) = match arg with - | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e]) + | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (_l,name); e]) -> (elab_colon_to_ak k, - (l, Some name), Some e) - | Symbol (l, name) -> (Anormal, (l, Some name), None) + (arg, Some name), Some e) + | Symbol (_l, name) -> (Anormal, (arg, Some name), None) | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) (sexp_location arg) "Unrecognized formal arg"; - (Anormal, (sexp_location arg, None), None) + (Anormal, (arg, None), None)

let sform_typecons ctx loc sargs _ot = match sargs with - | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) + | [] -> sexp_error (sexp_location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with | Node (label, formals) -> (label, formals) @@ -1589,7 +1590,7 @@ let sform_hastype ctx loc sargs _ot = | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) - | _ -> sexp_error loc "##_:_ takes two arguments"; + | _ -> sexp_error (sexp_location loc) "##_:_ takes two arguments"; sform_dummy_ret ctx loc

let sform_arrow kind ctx loc sargs _ot = @@ -1597,12 +1598,12 @@ let sform_arrow kind ctx loc sargs _ot = | [st1; st2] -> let (v, st1) = match st1 with | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) - | _ -> ((sexp_location st1, None), st1) in + | _ -> ((st1, None), st1) in let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in - let lt2 = infer_type st2 nctx (sexp_location st2, None) in - (mkArrow (kind, v, lt1, loc, lt2), Lazy) - | _ -> sexp_error loc "##_->_ takes two arguments"; + let lt2 = infer_type st2 nctx (st2, None) in + (mkArrow (loc, kind, v, lt1, lt2), Lazy) + | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc

let sform_immediate ctx loc sargs ot = @@ -1616,10 +1617,10 @@ let sform_immediate ctx loc sargs ot = let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot | [_se] - -> (sexp_error loc ("Non-immediate passed to ##typer-immediate"); + -> (sexp_error (sexp_location loc) ("Non-immediate passed to ##typer-immediate"); sform_dummy_ret ctx loc) | _ - -> (sexp_error loc ("Too many args to ##typer-immediate"); + -> (sexp_error (sexp_location loc) ("Too many args to ##typer-immediate"); sform_dummy_ret ctx loc)

@@ -1639,7 +1640,7 @@ let sform_identifier ctx loc sargs ot = (sexp_error l {|Invalid special identifier "%s"|} name; sform_dummy_ret ctx loc)

- | [Symbol (loc, name)] + | [Symbol (_loc, name)] when String.length name >= 1 && String.get name 0 = '?' -> let name = if name = "?" then "" else string_sub name 1 (String.length name) in @@ -1663,13 +1664,13 @@ let sform_identifier ctx loc sargs ot = (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for the metavar! *) - fatal ~loc ("Bug in the elaboration of a metavar" + fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" ^^ " repeated at a different scope level!") | MVal _ -> (* FIXME: We face the same problem as above, but here, the situation is worse, we don't even know the scope level! *) - fatal ~loc "Bug in the elaboration of a repeated metavar!" + fatal ~loc:(sexp_location loc) "Bug in the elaboration of a repeated metavar!" else let t = match ot with | None -> newMetatype octx sl loc @@ -1681,19 +1682,20 @@ let sform_identifier ctx loc sargs ot = let idx = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx - | _ -> fatal ~loc "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy)

(* Normal identifier. *) - | [Symbol id] -> elab_varref ctx id + | [Symbol (_n, name)] + -> elab_varref ctx (loc, name)

| [_se] - -> (sexp_error loc ("Non-symbol passed to ##typer-identifier"); + -> (sexp_error (sexp_location loc) ("Non-symbol passed to ##typer-identifier"); sform_dummy_ret ctx loc)

| _ - -> (sexp_error loc ("Too many args to ##typer-identifier"); + -> (sexp_error (sexp_location loc) ("Too many args to ##typer-identifier"); sform_dummy_ret ctx loc)

let rec sform_lambda kind ctx loc sargs ot = @@ -1704,7 +1706,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Symbol arg -> (elab_p_id arg, None) | _ -> sexp_error (sexp_location sarg) "Unrecognized lambda argument"; - ((dummy_location, None), None) in + ((dsinfo, None), None) in

let olt1 = match ost1 with | Some st -> Some (infer_type st ctx arg) @@ -1722,7 +1724,7 @@ let rec sform_lambda kind ctx loc sargs ot = let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2)) + | Inferred lt2 -> Inferred (mkArrow (loc, kind, arg, lt1, lt2)) | _ -> alt) in

(match ot with @@ -1735,7 +1737,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Some t -> let lp = OL.lexp_whnf t (ectx_to_lctx ctx) in match lexp_lexp' lp with - | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind + | Arrow (_, ak2, _, lt1, lt2) when ak2 = kind -> (match olt1 with | None -> () | Some lt1' @@ -1743,7 +1745,7 @@ let rec sform_lambda kind ctx loc sargs ot = ~lxp_name:"parameter" lt1 lt1'); mklam lt1 (Some lt2)

- | Arrow (ak2, v, lt1, _, lt2) when kind = Anormal + | 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. *) @@ -1756,7 +1758,7 @@ let rec sform_lambda kind ctx loc sargs ot = let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in (mkLambda (ak2, v, lt1, lam), match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) + | Inferred lt2' -> Inferred (mkArrow (loc, ak2, v, lt1, lt2')) | _ -> alt)

| _lt @@ -1765,7 +1767,7 @@ let rec sform_lambda kind ctx loc sargs ot =

| _ -> sexp_error - loc "##lambda_%s_ takes two arguments" + (sexp_location loc) "##lambda_%s_ takes two arguments" (match kind with | Anormal -> "->" | Aimplicit -> "=>" @@ -1779,7 +1781,7 @@ let rec sform_case ctx loc sargs ot = match sargs with -> (pexp_p_pat pat, code) | _ -> let l = (sexp_location branch) in sexp_error l "Unrecognized simple case branch"; - (Ppatsym (l, None), Symbol (l, "?")) in + (Ppatsym (se, None), Symbol (l, "?")) in let pcases = List.map parse_case scases in let t = match ot with | Some t -> t @@ -1788,8 +1790,8 @@ let rec sform_case ctx loc sargs ot = match sargs with (le, match ot with Some _ -> Checked | None -> Inferred t)

(* In case there are no branches, pretend there was a | anyway. *) - | [_e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot - | _ -> sexp_error loc "Unrecognized case expression"; + | [_e] -> sform_case ctx loc [Node (Symbol (sexp_location loc, "_|_"), sargs)] ot + | _ -> sexp_error (sexp_location loc) "Unrecognized case expression"; sform_dummy_ret ctx loc

let sform_letin ctx loc sargs ot = match sargs with @@ -1805,7 +1807,7 @@ let sform_letin ctx loc sargs ot = match sargs with | Inferred t -> Inferred (mkSusp t s) | _ -> ot in (lexp_let_decls declss bdy nctx, ot) - | _ -> sexp_error loc "Unrecognized let_in_ expression"; + | _ -> sexp_error (sexp_location loc) "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc

let sform_proj ctx loc sargs _ = @@ -1815,9 +1817,9 @@ let sform_proj ctx loc sargs _ = let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) | [_;_] - -> sexp_error loc "Second argument is not a Symbol!"; + -> sexp_error (sexp_location loc) "Second argument is not a Symbol!"; sform_dummy_ret ctx loc - | _ -> sexp_error loc "Wrong arg number!"; + | _ -> sexp_error (sexp_location loc) "Wrong arg number!"; sform_dummy_ret ctx loc

let rec infer_level ctx se : lexp = @@ -1830,7 +1832,7 @@ let rec infer_level ctx se : lexp = -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> let l = (sexp_location se) in (sexp_error l "Unrecognized TypeLevel: %s" (sexp_string se); - newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) l) + newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) se)

(* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) @@ -1843,7 +1845,7 @@ let sform_type ctx loc sargs _ot = | [se] -> let l = infer_level ctx se in (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) - | _ -> (sexp_error loc "##Type_ expects one argument"; + | _ -> (sexp_error (sexp_location loc) "##Type_ expects one argument"; sform_dummy_ret ctx loc)

let sform_debruijn ctx loc sargs _ot = @@ -1854,7 +1856,7 @@ let sform_debruijn ctx loc sargs _ot = sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy) - | _ -> (sexp_error loc "##DeBruijn expects one integer argument"; + | _ -> (sexp_error (sexp_location loc) "##DeBruijn expects one integer argument"; sform_dummy_ret ctx loc)

(* Only print var info *) @@ -1890,7 +1892,7 @@ let sform_load usr_elctx loc sargs _ot = let pres = try prelex source with | Sys_error _ - -> error ~loc {|Could not load "%s": file not found.|} file_name; [] + -> error ~loc:(sexp_location loc) {|Could not load "%s": file not found.|} file_name; [] in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx @@ -1902,7 +1904,7 @@ let sform_load usr_elctx loc sargs _ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error ~loc "argument to load should be one file name (String)"; + | _ -> (error ~loc:(sexp_location loc) "argument to load should be one file name (String)"; !sform_default_ectx) in

(* get lexp_context *) @@ -1993,7 +1995,7 @@ let default_ectx let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in - let v = mkVar ((dloc, Some name), idx) in + let v = mkVar ((dsinfo, Some name), idx) in BI.set_predef name v) BI.predef_names; with Senv_Lookup_Fail _ -> warning "Predef not found"; in @@ -2002,7 +2004,7 @@ let default_ectx let lctx = empty_elab_context in let lctx = SMap.fold (fun key (e, t) ctx -> if String.get key 0 = '-' then ctx - else ctx_define ctx (dloc, Some key) e t) + else ctx_define ctx (dsinfo, Some key) e t) (!BI.lmap) lctx in

Heap.register_builtins ();

===================================== src/elexp.ml ===================================== @@ -36,8 +36,8 @@ open Sexp (* Sexp type *) module U = Util module L = Lexp

-type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type label = symbol

module SMap = U.SMap @@ -84,11 +84,11 @@ type elexp = let rec elexp_location e = match e with | Imm s -> sexp_location s - | Var ((l,_), _) -> l + | Var ((l,_), _) -> sexp_location l | Proj (l,_,_) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l - | Lambda ((l,_),_) -> l + | Lambda ((l,_),_) -> sexp_location l | Call (f,_) -> elexp_location f | Cons (_, (l, _)) -> l | Case (l,_,_,_) -> l

===================================== src/eval.ml ===================================== @@ -495,7 +495,7 @@ and eval_var ctx lxp v = with | _e -> Log.log_fatal - ~loc + ~loc:(sexp_location loc) "Variable: %s%d was not found\n%s" (L.maybename name) idx (trace_elexp lxp)

@@ -558,7 +558,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, [(Anormal, mkVar (vdummy, -1))])) + -> Vtype (L.mkCall (dsinfo, e, [(Anormal, mkVar (vdummy, -1))])) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f)

and eval_case ctx i loc target pat dflt = @@ -629,7 +629,7 @@ and eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let trace_dum = (Var ((loc, None), -1)) in + let trace_dum = (Var ((Symbol(loc, ""), None), -1)) in let eval_call a b = eval_call loc trace_dum depth a b in let sxp, nd, sym, str, it, flt, blk = match args with | [sxp; nd; sym; str; it; flt; blk] -> @@ -717,7 +717,7 @@ and print_eval_trace trace = print_trace " EVAL TRACE " trace a

let io_bind loc depth args_val = - let trace_dum = (Var ((loc, None), -1)) in + let trace_dum = (Var ((Symbol(loc, ""), None), -1)) in

match args_val with | [Vcommand cmd; callback] @@ -755,8 +755,8 @@ let sys_exit loc _depth args_val = match args_val with let y_operator loc _depth args = match args with | [f] -> let yf_ref = ref Vundefined in - let fname = (dloc, Some "f") in - let yfname = (dloc, Some "yf") in + let fname = (dsinfo, Some "f") in + let yfname = (dsinfo, Some "yf") in let yf = Closure(vdummy, Call (Var (fname, 1), [Var (yfname, 2); @@ -808,7 +808,7 @@ let constructor_p name ectx = (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons _ -> true (* It's indeed a constructor! *) | _ -> false with Senv_Lookup_Fail _ -> false @@ -822,7 +822,7 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -843,7 +843,7 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some t), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -861,7 +861,7 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -882,7 +882,7 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i

===================================== src/instargs.ml ===================================== @@ -25,6 +25,7 @@ module U = Util module Unif = Unification

open Printf +open Sexp

(** If true, log all the matching instances when resolving. *) let debug_list_all_candidates = ref false @@ -40,10 +41,10 @@ let recursion_limit = ref (Some 100) let log_skipped_uncertain_matches = ref (Some Log.Warning)

let metavar_resolution_contexts = - ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t) + ref (U.IMap.empty : (DB.elab_context * sinfo) U.IMap.t)

let lookup_metavar_resolution_ctxt (id : L.meta_id) - : (DB.elab_context * U.location) option + : (DB.elab_context * sinfo) option = U.IMap.find_opt id (!metavar_resolution_contexts)

let save_metavar_resolution_ctxt (id : L.meta_id) ctx loc : unit @@ -79,7 +80,7 @@ let in_typeclass_set (ectx : DB.elab_context) (t : L.ltype) : bool = let get_head (lctx : DB.lexp_context) (t : L.ltype) : L.ltype = let whnft = OL.lexp_whnf t lctx in match L.lexp_lexp' whnft with - | L.Call (head, _) -> head + | L.Call (_, head, _) -> head | _ -> whnft

(** A type is a type class if its head is in the set of type class @@ -112,8 +113,8 @@ let try_match t1 t2 lctx sl = | _ -> Possible

let search_instance (instantiate_implicit) (ctx : DB.elab_context) - (loc : U.location) (t : L.ltype) : L.lexp option = - Log.log_debug ~loc "Resolving type `%s`" (L.lexp_string t); + (loc : sinfo) (t : L.ltype) : L.lexp option = + Log.log_debug ~loc:(sexp_location loc) "Resolving type `%s`" (L.lexp_string t); let lctx = DB.ectx_to_lctx ctx in let (_, _, insts) = DB.ectx_to_tcctx ctx in

@@ -133,7 +134,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) let var = L.mkVar ((loc,namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in - Log.log_debug ~loc + Log.log_debug ~loc:(sexp_location loc) "Considering potential instance `%s : %s` while resolving for `%s`" (L.lexp_string var) (L.lexp_string t') (L.lexp_string t); (* All candidates should have a type that is a typeclass. *) @@ -149,7 +150,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | Possible -> (match !log_skipped_uncertain_matches with | Some level -> - Log.log_msg ignore level ~loc + Log.log_msg ignore level ~loc:(sexp_location loc) "Skipping potential instance `%s : %s` while resolving for `%s`" (L.lexp_string var) (L.lexp_string t') (L.lexp_string t) @@ -178,7 +179,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | None -> None | Some (i, (vname, _, t'), e) -> let t' = L.mkSusp t' (S.shift (i + 1)) in - Log.log_debug ~loc + Log.log_debug ~loc:(sexp_location loc) "Found instance for `%s` at index %i: `%s : %s`" (L.lexp_string t) i (L.lexp_string (L.mkVar (vname, i))) (L.lexp_string t'); @@ -199,12 +200,12 @@ let resolve_instances instantiate_implicit e = | MVar _ -> true | _ -> false in if uninstantiated && is_typeclass ctx t then - (match search_instance instantiate_implicit ctx loc t with + (match search_instance instantiate_implicit ctx (loc) t with | Some e -> Unif.associate i e; true | None -> (* The metavar will be generalized, unified, or will remain and cause an error. *) - Log.log_info ~loc "No instance found for type `%s`" + Log.log_info ~loc:(sexp_location loc) "No instance found for type `%s`" (L.lexp_string t); false ) else false

===================================== src/inverse_subst.ml ===================================== @@ -53,6 +53,8 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an

type substIR = ((int * int) list * int * int)

+let dsinfo = Sexp.dummy_sinfo + (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) @@ -94,7 +96,7 @@ let sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - mkVar ((U.dummy_location, None), idx) + mkVar ((dsinfo, None), idx)

(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -275,13 +277,13 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = :: ndefs)) (s, []) defs in mkLet (l, ndefs, apply_inv_subst e s') - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, apply_inv_subst t1 s, l, + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, apply_inv_subst t1 s, apply_inv_subst t2 (ssink v s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) - | Call (f, args) - -> mkCall (apply_inv_subst f s, + | Call (l, f, args) + -> mkCall (l, apply_inv_subst f s, L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) | Inductive (l, label, args, cases) -> let (s, nargs)

===================================== src/lexp.ml ===================================== @@ -33,9 +33,10 @@ open Grammar (* open Unify *) module S = Subst

-type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type meta_id = int (* Identifier of a meta variable. *) +type sinfo = sexp

type label = symbol

@@ -63,23 +64,23 @@ type ltype = lexp and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level - | Sort of U.location * sort + | Sort of sinfo * sort | Builtin of symbol * ltype | Var of vref - | Proj of U.location * lexp * label + | Proj of sinfo * lexp * label | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) - | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * ltype + | Let of sinfo * (vname * lexp * ltype) list * lexp + | Arrow of sinfo * arg_kind * vname * ltype * ltype | Lambda of arg_kind * vname * ltype * lexp - | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label + | Call of sinfo * lexp * (arg_kind * lexp) list (* Curried call. *) + | Inductive of sinfo * label * ((arg_kind * vname * ltype) list) (* formal Args *) * ((arg_kind * vname * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) - | Case of U.location * lexp + | Case of sinfo * lexp * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (sinfo * (arg_kind * vname) list * lexp) SMap.t * (vname * lexp) option (* Default. *) (* The `subst` will be applied to the the metavar's value when it * gets instantiated. *) @@ -164,6 +165,8 @@ let dummy_scope_level = 0

let builtin_size = ref 0

+let dummy_sinfo = Sexp.dummy_sinfo + let metavar_table = ref (U.IMap.empty : meta_subst) let metavar_lookup (id : meta_id) : metavar_info = try U.IMap.find id (!metavar_table) @@ -209,11 +212,11 @@ let lexp'_hash (lp : lexp') = (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) ds)) (lexp_hash e))) - | Arrow (k, v, t1, l, t2) + | Arrow (l, k, v, t1, t2) -> U.combine_hash 7 (U.combine_hash - (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (U.combine_hash (lexp_hash t1) - (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) + (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash k)) + (U.combine_hash (Hashtbl.hash v) + (U.combine_hash (lexp_hash t1) (lexp_hash t2)))) | Lambda (k, v, t, e) -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) @@ -239,7 +242,7 @@ let lexp'_hash (lp : lexp') = | Metavar (id, s, v) -> U.combine_hash 12 (U.combine_hash id (U.combine_hash (Hashtbl.hash s) (Hashtbl.hash v))) - | Call (e, args) + | Call (_, e, args) -> U.combine_hash 13 (U.combine_hash (lexp_hash e) (U.combine_hashes (List.map (fun e -> let (ak, lp) = e in (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) @@ -272,11 +275,11 @@ let hc_eq e1 e2 = | (Let (_, defs1, e1), Let (_, defs2, e2)) -> e1 == e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> t1 == t2 && e1 == e2) defs1 defs2 - | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + | (Arrow (_, ak1, _, t11, t21), Arrow (_, ak2, _, t12, t22)) -> ak1 = ak2 && t11 == t12 && t21 == t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) -> ak1 = ak2 && t1 == t2 && e1 == e2 - | (Call (e1, as1), Call (e2, as2)) + | (Call (_, e1, as1), Call (_, e2, as2)) -> e1 == e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) @@ -316,17 +319,17 @@ let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) let mkLet (l, ds, e) = hc (Let (l, ds, e)) -let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) +let mkArrow (l, k, v, t1, t2) = hc (Arrow (l, k, v, t1, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) -let mkCall (f, es) = +let mkCall (l, f, es) = match lexp_lexp' f, es with - | Call (f', es'), _ -> hc (Call (f', es' @ es)) + | Call (l, f', es'), _ -> hc (Call (l, f', es' @ es)) | _, [] -> f - | _ -> hc (Call (f, es)) + | _ -> hc (Call (l, f, es))

let impossible = mkImm Sexp.dummy_epsilon

@@ -513,33 +516,37 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) * S.sink (fun l i -> mkVar (l, i)) l s *)

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

+let lexp_location e = + sexp_location (sinfo_location e) + + (********* Normalizing a term *********)

-let vdummy = (U.dummy_location, None) +let vdummy = (dummy_sinfo, None) let maybename n = match n with None -> "<anon>" | Some v -> v -let sname (l,n) = (l, maybename n) +let sname (l,n) = (sexp_location l, maybename n)

let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with @@ -559,10 +566,10 @@ let rec push_susp e s = (* Push a suspension one level down. *) | (v, def, ty) :: defs -> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in mkLet (l, loop s defs, mkSusp e s') - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink v s)) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, mkSusp t1 s, mkSusp t2 (ssink v s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) - | Call (f, args) -> mkCall (mkSusp f s, + | Call (l, f, args) -> mkCall (l,mkSusp f s, L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -627,10 +634,10 @@ let clean e = (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in mkLet (l, ndefs, clean s' e) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, clean s t1, clean (ssink v s) t2) | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) - | Call (f, args) -> mkCall (clean s f, + | Call (l, f, args) -> mkCall (l, clean s f, L.map (fun (ak, arg) -> (ak, clean s arg)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -681,9 +688,9 @@ let rec lexp_unparse lxp = | Imm (sexp) -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) - | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) | Proj (l,lxp,(loc,str) ) - -> Node (Symbol (l, "__.__"), + -> Node (Symbol (sexp_location l, "__.__"), [(lexp_unparse lxp);(Symbol (loc,str))]) | Cons (t, (l, name)) -> Node (sdatacons, @@ -697,14 +704,14 @@ let rec lexp_unparse lxp = | Aerasable -> "lambda_≡>_"), [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body]) - | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) + | Arrow (loc, arg_kind, (l,oname), ltp1, ltp2) -> let ut1 = lexp_unparse ltp1 in - Node (Symbol (loc, match arg_kind with Anormal -> "_->_" + Node (Symbol (sexp_location loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), [(match oname with None -> ut1 - | Some v -> Node (Symbol (l, "_:_"), - [Symbol (l,v); ut1])); + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); lexp_unparse ltp2])

| Let (loc, ldecls, body) @@ -717,11 +724,11 @@ let rec lexp_unparse lxp = [Symbol (sname vdef); lexp_unparse lxp]) :: acc) [] ldecls in - Node (Symbol (loc, "let_in_"), + Node (Symbol (sexp_location loc, "let_in_"), [Node (Symbol (U.dummy_location, "_;_"), sdecls); lexp_unparse body])

- | Call(lxp, largs) -> (* (arg_kind * lexp) list *) + | Call(_, lxp, largs) -> (* (arg_kind * lexp) list *) let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem) largs in Node (lexp_unparse lxp, sargs)

@@ -735,7 +742,7 @@ let rec lexp_unparse lxp = Node (Symbol label, List.map pexp_u_formal_arg pfargs) :: List.map (fun (name, types) - -> Node (Symbol (loc, name), + -> Node (Symbol (sexp_location loc, name), List.map (fun arg -> match arg with @@ -759,13 +766,13 @@ let rec lexp_unparse lxp = let pat_args = List.map (fun (_kind, ((l,oname) as name)) -> match oname with - | Some vdef -> (Some (l,vdef), name) + | Some vdef -> (Some (sexp_location l,vdef), name) | None -> (None, name)) args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) in (Ppatcons (Node (sdatacons, - [bt; Symbol (loc, str)]), + [bt; Symbol (sexp_location loc, str)]), pat_args), lexp_unparse bch) ) (SMap.bindings branches) in @@ -775,16 +782,16 @@ let rec lexp_unparse lxp = lexp_unparse dft)::pbranch | None -> pbranch in let e = lexp_unparse target in - Node (Symbol (loc, "case_"), + Node (Symbol (sexp_location loc, "case_"), e :: List.map (fun (pat, branch) -> - Node (Symbol (pexp_pat_location pat, "_=>_"), + Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), [pexp_u_pat pat; branch])) pbranch)

(* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name)) - -> Symbol (loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx + -> Symbol (sexp_location loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]")

| SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") @@ -794,8 +801,8 @@ let rec lexp_unparse lxp = | SortLevel (SLlub (l1, l2)) -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), [lexp_unparse l1; lexp_unparse l2]) - | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") - | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") + | Sort (l, StypeOmega) -> Symbol (sexp_location l, "##Type_ω") + | Sort (l, StypeLevel) -> Symbol (sexp_location l, "##TypeLevel.Sort") | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [lexp_unparse sl]) @@ -904,10 +911,10 @@ let rec get_precedence expr ctx = | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" - | Arrow (Anormal, _, _, _, _) -> lkp "->" - | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" - | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" - | Call (exp, _) -> get_precedence exp ctx + | Arrow (_, Anormal, _, _, _) -> lkp "->" + | Arrow (_, Aimplicit, _, _, _) -> lkp "=>" + | Arrow (_, Aerasable, _, _, _) -> lkp "≡>" + | Call (_, exp, _) -> get_precedence exp ctx | Builtin ((_, name), _) when is_binary_op name -> lkp (get_binary_op_name name) | Var ((_, Some name), _) when is_binary_op name -> @@ -1015,11 +1022,11 @@ and lexp_str ctx (exp : lexp) : string = (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body)

- | Arrow(k, (_, Some name), tp, _loc, expr) -> + | Arrow(_loc, k, (_, Some name), tp, expr) -> "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ (kind_str k) ^ " " ^ (lexp_str' expr)

- | Arrow(k, (_, None), tp, _loc, expr) -> + | Arrow(_loc, k, (_, None), tp, expr) -> "(" ^ (lexp_str' tp) ^ " " ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")"

@@ -1032,7 +1039,7 @@ and lexp_str ctx (exp : lexp) : string = | Cons(t, (_, ctor_name)) -> (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name

- | Call(fname, args) -> + | Call(_, fname, args) -> let name, idx = get_name fname in let binop_str op (_, lhs) (_, rhs) = "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in @@ -1156,11 +1163,11 @@ let rec eq e1 e2 = | (Let (_, defs1, e1), Let (_, defs2, e2)) -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> eq t1 t2 && eq e1 e2) defs1 defs2 - | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + | (Arrow (_, ak1, _, t11, t21), Arrow (_, ak2, _, t12, t22)) -> ak1 = ak2 && eq t11 t12 && eq t21 t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) -> ak1 = ak2 && eq t1 t2 && eq e1 e2 - | (Call (e1, as1), Call (e2, as2)) + | (Call (_, e1, as1), Call (_, e2, as2)) -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2))

===================================== src/opslexp.ml ===================================== @@ -51,6 +51,9 @@ type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t let error ~location fmt = Log.log_fatal ~section:"OPSLEXP" ~loc:location fmt

+let dloc = DB.dloc +let dsinfo = DB.dsinfo + module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but * I haven't found any such functionality in OCaml's libs. *) @@ -127,7 +130,7 @@ let rec lctx_to_subst lctx = L.ssink v s | DB.CVfix (defs, lctx) -> let s1 = lctx_to_subst lctx in - let s2 = lexp_defs_subst DB.dloc S.identity + let s2 = lexp_defs_subst dsinfo S.identity (List.rev defs) in L.scompose s2 s1

@@ -177,17 +180,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = * things like full normalization (e.g. lexp_conv_p). *) | Some e' -> lexp_whnf e' ctx) | Susp (e, s) -> lexp_whnf (push_susp e s) ctx - | Call (e, []) -> lexp_whnf e ctx - | Call (f, (((_, arg)::args) as xs)) -> + | Call (_, e, []) -> lexp_whnf e ctx + | Call (l, f, (((_, arg)::args) as xs)) -> (match lexp'_whnf f ctx with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (mkCall (push_susp body (S.substitute (lexp_whnf arg ctx)), + lexp_whnf (mkCall (l, push_susp body (S.substitute (lexp_whnf arg ctx)), args)) ctx - | Call (f', xs1) -> mkCall (f', List.append xs1 xs) + | Call (l, f', xs1) -> mkCall (l, f', List.append xs1 xs) | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> Option.value ~default:e (f ctx args) @@ -200,7 +203,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, + mkCall (l, DB.eq_refl, [L.Aerasable, elevel; L.Aerasable, etype; L.Aerasable, e]) in @@ -230,12 +233,12 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = -> let subst = S.cons (get_refl e') (S.substitute e') in lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error - ~section:"WHNF" ~loc:l + ~section:"WHNF" ~loc:(sexp_location l) {|Unhandled constructor "%s" in case expression|} name; mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] - | Call (f, aargs) -> + | Call (_, f, aargs) -> (match lexp'_whnf f ctx with | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default)) @@ -243,7 +246,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp =

| Proj (loc, lxp, (_loc, label)) -> let c, args = match lexp'_whnf lxp ctx with - | Call (f, args) -> f, args + | Call (_loc, f, args) -> f, args | _ -> lxp, [] in (match lexp'_whnf c ctx with | Cons (it, _) -> @@ -256,17 +259,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = _ -> []) in let rec getfield label args fields = match args, fields with - | _ , [] -> Log.log_error ~loc + | _ , [] -> Log.log_error ~loc:(sexp_location loc) "Tuple does not have the field `%s`" label; e | (_, arg)::_, (_, (_, Some fn), _)::_ when fn = label -> (* Reduce to the argument corresponding to the field *) lexp_whnf arg ctx | _::args, _::fields -> getfield label args fields | [], _ -> (* This case should be impossible through typing *) - Log.log_fatal ~loc + Log.log_fatal ~loc:(sexp_location loc) "Projected tuple has fewer arguments than fields" in getfield label (drop (List.length targs) args) fields - | _ -> Log.log_error ~loc "Proj on a non-tuple in WHNF!"; e) + | _ -> Log.log_error ~loc:(sexp_location loc) "Proj on a non-tuple in WHNF!"; e) | _ -> e) (* Not a proj of a cons: don't reduce. *)

| Metavar (idx, s, _) @@ -288,7 +291,7 @@ and eq_cast_whnf ctx args = match args with | [_l; _t; _x; _y; (_, p); _f; (_, fx)] -> (match lexp'_whnf p ctx with - | Call (refl, _) when conv_p ctx refl DB.eq_refl + | Call (_, refl, _) when conv_p ctx refl DB.eq_refl -> Some (lexp_whnf fx ctx) | _ -> None) | _ -> None @@ -378,7 +381,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _ -> false) | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 | (Var (_, v1), Var (_, v2)) -> v1 = v2 - | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, _vd2, t21, _, t22)) + | (Arrow (_, ak1, vd1, t11, t12), Arrow (_, ak2, _vd2, t21, t22)) -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') @@ -388,7 +391,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) (set_shift vs') e1 e2 - | (Call (f1, args1), Call (f2, args2)) + | (Call (_, f1, args1), Call (_, f2, args2)) -> let conv_arglist_p args1 args2 : bool = List.fold_left2 (fun eqp (ak1,t1) (ak2,t2) @@ -441,7 +444,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = "Target lexp's kind is not a sort"; in (* 1. Get the inductive for the field types *) let it, aargs = match lexp_lexp' etype with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (etype, []) in (* 2. Build the substitution for the inductive arguments *) let fargs, ctors = @@ -456,12 +459,12 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tlxp = mkSusp target subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (dsinfo, DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) (L.Anormal, tlxp)]) in (* Target lexp *) - DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in + DB.lexp_ctx_cons ctx (dsinfo, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types from the inductive. Instead, we work with the lists of @@ -492,9 +495,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let subst = S.shift offset in let eaargs = List.map (fun (_, a) -> (P.Aerasable, a)) aargs in - let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)), + let ctor = mkSusp (mkCall (dsinfo, mkCons (it, (DB.dloc, l1)), eaargs)) subst in - let hlxp = mkCall (ctor, args) in + let hlxp = mkCall (dsinfo, ctor, args) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 ) (SMap.bindings cases1) (SMap.bindings cases2) @@ -505,7 +508,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Some (v1, e1), Some (_v2, e2)) -> let nctx = DB.lctx_extend ctx v1 Variable etype in let subst = S.shift 1 in - let hlxp = mkVar ((DB.dloc, None), 0) in + let hlxp = mkVar ((dsinfo, None), 0) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' 2) e1 e2 | None, None -> true @@ -661,7 +664,7 @@ and check'' erased ctx e = | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then log_tc_error - ~loc + ~loc:(sexp_location loc) {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v @@ -687,14 +690,14 @@ and check'' erased ctx e = (List.length defs) defs in mkSusp (check nerased nctx e) (lexp_defs_subst l S.identity defs) - | Arrow (ak, v, t1, loc, t2) + | Arrow (loc, ak, v, t1, t2) -> (let k1 = check_type erased ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in let k2 = check_type (DB.set_sink 1 erased) nctx t2 in match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; + -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; @@ -704,18 +707,18 @@ and check'' erased ctx e = mkSort (loc, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in - mkArrow (ak, v, t, l, + mkArrow (l, ak, v, t, check (dbset_push ak erased) (DB.lctx_extend ctx v Variable t) e)) - | Call (f, args) + | Call (_, f, args) -> let ft = check erased ctx f in List.fold_left (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 with - | Arrow (ak', _v, t1, _l, t2) + | Arrow (_l, ak', _v, t1, t2) -> if ak != ak' then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; assert_type ctx arg at t1; @@ -778,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 (ak, v, t, lexp_location t, + mkArrow (sinfo_location t, ak, v, t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) args) in @@ -787,7 +790,7 @@ and check'' erased ctx e = | Proj (l, e, (loc, label)) -> ( let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in let it, aargs = call_split etype in @@ -799,20 +802,20 @@ and check'' erased ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:l + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasable field: %s" + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -824,16 +827,16 @@ and check'' erased ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:l + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype)

| Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in (* FIXME save the type in the case lexp instead of recomputing @@ -854,14 +857,14 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:l "Wrong arg number to inductive type!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (l, DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) @@ -882,13 +885,13 @@ and check'' erased ctx e = -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) (ssink vdef s) - (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) + (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _ - -> log_tc_error ~loc:l "Wrong number of args to constructor!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (mkCons (it, (l, name)), + mkCall (l, mkCons (it, (sexp_location l, name)), List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in @@ -902,7 +905,7 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 - then log_tc_warning ~loc:l "Redundant default clause"; + then log_tc_warning ~loc:(sexp_location l) "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -915,8 +918,8 @@ and check'' erased ctx e = -> if diff > 0 then log_tc_error - ~loc:l "Non-exhaustive match: %d cases missing" diff) - | _,_ -> log_tc_error ~loc:l "Case on a non-inductive type!"); + ~loc:(sexp_location l) "Non-exhaustive match: %d cases missing" diff) + | _,_ -> log_tc_error ~loc:(sexp_location l) "Case on a non-inductive type!"); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -931,21 +934,21 @@ and check'' erased ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), + mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> mkArrow (sinfo_location ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, + -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs with | Not_found - -> log_tc_error ~loc:l {|Constructor "%s" does not exist|} name; + -> log_tc_error ~loc:(sexp_location l) {|Constructor "%s" does not exist|} name; DB.type_int) | _ -> log_tc_error ~loc:(lexp_location e) @@ -1020,9 +1023,9 @@ and fv (e : lexp) : (DB.set * mv_set) = o - 1)) (fv e, len) defs in fv_hoist len fvs - | Arrow (_, _, t1, _, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) + | Arrow (_, _, _, t1, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) | Lambda (_, _, t, e) -> fv_union (fv_erase (fv t)) (fv_hoist 1 (fv e)) - | Call (f, args) + | Call (_, f, args) -> List.fold_left (fun fvs (ak, arg) -> let afvs = fv arg in fv_union fvs @@ -1102,7 +1105,7 @@ and get_type ctx e =

let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (get_type ctx e) ctx in let it, aargs = call_split etype in @@ -1114,21 +1117,21 @@ and get_type ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:l + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -1140,16 +1143,16 @@ and get_type ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:l + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) - | Arrow (ak, v, t1, l, t2) + | Arrow (l, ak, v, t1, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in @@ -1158,15 +1161,15 @@ and get_type ctx e = | SortResult k -> k | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) - -> (mkArrow (ak, v, t, l, + -> (mkArrow (l, ak, v, t, get_type (DB.lctx_extend ctx v Variable t) e)) - | Call (f, args) + | Call (_l, f, args) -> let ft = get_type ctx f in List.fold_left (fun ft (_ak,arg) -> match lexp'_whnf ft ctx with - | Arrow (_ak', _v, _t1, _l, t2) + | Arrow (_l, _ak', _v, _t1, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args @@ -1204,14 +1207,14 @@ and get_type ctx e = cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> mkArrow (ak, v, t, lexp_location t, + -> mkArrow (sinfo_location t, ak, v, t, arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with - | Inductive (_l, _, fargs, constructors) + | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -1222,16 +1225,16 @@ and get_type ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), + mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> mkArrow (sinfo_location ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, + -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs with Not_found -> DB.type_int) @@ -1280,7 +1283,7 @@ let arity_of_cons let pos_of_label lctx label e : int = let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (e,[]) in

let it, aargs = call_split (lexp_whnf e lctx) in @@ -1322,7 +1325,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Var (v) -> E.Var (v) | L.Proj (l, exp, label) -> let t = get_type lctx exp in - E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) + E.Proj (sexp_location l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)

| L.Lambda (P.Aerasable, _, _, body) @@ -1334,15 +1337,15 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp =

| L.Let (l, decls, body) -> let lctx', edecls = clean_decls lctx decls in - E.Let (l, edecls, erase_type lctx' body) + E.Let (sexp_location l, edecls, erase_type lctx' body)

- | L.Call (fct, args) + | L.Call (_, fct, args) -> E.Call (erase_type lctx fct, List.filter_map (clean_arg lctx) args)

| L.Case (location, target, _, branches, default) -> let etarget = erase_type lctx target in let ebranches = clean_branch_map lctx branches in - E.Case (location, etarget, ebranches, clean_default lctx default) + E.Case (sexp_location location, etarget, ebranches, clean_default lctx default)

| L.Susp (l, s) -> erase_type lctx (L.push_susp l s)

@@ -1391,7 +1394,7 @@ and clean_branch_map lctx cases = in let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) - (l, eargs, erase_type lctx' (L.push_susp expr subst)) + (sexp_location l, eargs, erase_type lctx' (L.push_susp expr subst)) in SMap.map clean_branch cases

@@ -1404,7 +1407,7 @@ let erase_type lctx lxp = Log.log_fatal ~print_action:(fun () -> IMap.iter (fun i (_, t, _, (l, n)) -> - print_endline ("\t" ^ (Source.Location.to_string l) + print_endline ("\t" ^ (Source.Location.to_string (sexp_location l)) ^ " ?" ^ (Option.value ~default:"" n) ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) ) mvs) @@ -1434,17 +1437,17 @@ let ctx2tup ctx nctx = | DB.CVfix (_, nctx) as bloc -> get_blocs nctx (bloc :: blocs) | _ -> assert false in let rec mk_lets_and_tup blocs types = - let loc = U.dummy_location in + let loc = dsinfo in match blocs with | [] -> let cons_name = "cons" in - let cons_label = (loc, cons_name) in - let type_label = (loc, "record") in + let cons_label = (sexp_location loc, cons_name) in + let type_label = (sexp_location loc, "record") in let offset = List.length types in let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*)

- mkCall (mkCons (mkInductive (loc, type_label, [], + mkCall (dsinfo, mkCons (mkInductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname,

===================================== src/pexp.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 +(* +*open Util +*) open Sexp (* Symbol *)

let pexp_error loc = Log.log_error ~section:"PEXP" ~loc @@ -43,7 +45,7 @@ type ppat =

let pexp_pat_location e = match e with | Ppatsym (l,_) -> l - | Ppatcons (e, _) -> sexp_location e + | Ppatcons (e, _) -> e

let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with @@ -56,28 +58,28 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = | None -> Symbol (l, "_")])

let pexp_p_pat_arg (s : sexp) = match s with - | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n)) - | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)]) - -> (Some f, (l, Some n)) + | Symbol (_l , n) -> (None, (s, match n with "_" -> None | _ -> Some n)) + | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) + -> (Some f, (s, Some n)) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; - (None, (loc, None)) + (None, (s, None))

let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = - let pname = Symbol (l, match oname with None -> "_" | Some n -> n) in + let pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in match okn with | None -> pname | Some ((l,_) as n) -> Node (Symbol (l, "_:=_"), [Symbol n; pname])

let pexp_p_pat (s : sexp) : ppat = match s with - | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n) + | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) | Node (c, args) -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in - pexp_error l "Unknown pattern"; Ppatsym (l, None) + pexp_error l "Unknown pattern"; Ppatsym (s, None)

let pexp_u_pat (p : ppat) : sexp = match p with - | Ppatsym (l, None) -> Symbol (l, "_") - | Ppatsym (l, Some n) -> Symbol (l, n) + | Ppatsym (l, None) -> Symbol (sexp_location l, "_") + | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args)

===================================== src/positivity.ml ===================================== @@ -69,7 +69,7 @@ let rec positive (index : db_index) (lexp : lexp) : bool =

and positive' index lexp = match Lexp.lexp_lexp' lexp with - | Lexp.Arrow (_, _, tau, _, e) + | Lexp.Arrow (_, _, _, tau, e) (* * x ⊢ e pos x ∉ fv(τ) * ────────────────────── @@ -77,7 +77,7 @@ and positive' index lexp = *) -> absent index tau && positive' (index + 1) e

- | Lexp.Call (f, args) + | Lexp.Call (_, f, args) (* * x ∉ fv(e⃗) * ──────────────

===================================== src/sexp.ml ===================================== @@ -38,10 +38,15 @@ type sexp = (* Syntactic expression, kind of like Lisp. *) | Float of location * float | Node of sexp * sexp list type token = sexp +type sinfo = sexp

let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location

+let dummy_sinfo = epsilon dummy_location + +type vname = sinfo * string option +type vref = vname * db_index (********************** Sexp tests **********************)

let pred_symbol s pred =

===================================== src/unification.ml ===================================== @@ -40,6 +40,9 @@ let create_metavar_1 (sl : scope_level) (t : ltype) (clen : int) let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) = create_metavar_1 sl t (Myers.length ctx)

+let dloc = DB.dloc +let dsinfo = DB.dsinfo + (* For convenience *) type constraint_kind = | CKimpossible (* Unification is simply impossible. *) @@ -78,9 +81,9 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with (* ; oi (push_susp e s) *) | Let (_, defs, e) -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs - | Arrow (_, _, t1, _, t2) -> oi t1 || oi t2 + | Arrow (_, _, _, t1, t2) -> oi t1 || oi t2 | Lambda (_, _, t, e) -> oi t || oi e - | Call (f, args) + | Call (_, f, args) -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args | Inductive (_, _, args, cases) -> SMap.fold @@ -143,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 ((lexp_location le1, None), 0), + | s' -> S.Cons (mkVar ((sinfo_location le1, None), 0), s', o) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that @@ -151,11 +154,11 @@ let common_subset ctx s1 s2 = * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) *) | (S.Cons _, S.Identity o2') - -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0), + -> loop s1 (S.Cons (mkVar ((dsinfo, None), 0), S.Identity 1, o2')) o1 o2 o | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0), + -> loop (S.Cons (mkVar ((dsinfo, None), 0), S.Identity 1, o1')) s2 o1 o2 o | (S.Identity o1', S.Identity o2') @@ -282,8 +285,8 @@ and unify' (e1: lexp) (e2: lexp) and unify_arrow (matching : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' arrow, lexp_lexp' lxp) with - | (Arrow (var_kind1, v1, ltype1, _, lexp1), - Arrow (var_kind2, _, ltype2, _, lexp2)) + | (Arrow (_, var_kind1, v1, ltype1, lexp1), + Arrow (_, var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs matching) @(unify' lexp1 (srename v1 lexp2) @@ -445,7 +448,7 @@ and unify_var (var: lexp) (lxp: lexp) ctx and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' call, lexp_lexp' lxp) with - | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) + | (Call (_, lxp_left, lxp_list1), Call (_, lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right -> (try List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then @@ -457,10 +460,10 @@ and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs -> [(CKresidual, ctx, call, lxp)]) | (call', lxp') -> let head_left = match call' with - | Call (head_left, _) -> head_left + | Call (_, head_left, _) -> head_left | _ -> call in let head_right = match lxp' with - | Call (head_right, _) -> head_right + | Call (_, head_right, _) -> head_right | _ -> lxp in let for_sure_irreducible_call_head ctx head = match OL.lexp'_whnf head ctx with

===================================== src/util.ml ===================================== @@ -33,11 +33,9 @@ let dummy_location = Source.Location.dummy (* 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 vname = location * string option type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) type db_revindex = int (* DeBruijn index counting from the root. *) -type vref = vname * db_index

type bottom = | B_o_t_t_o_m_ of bottom

===================================== tests/env_test.ml ===================================== @@ -30,6 +30,7 @@ open Typerlib open Utest_lib open Env

+let dsinfo = DB.dsinfo

let rctx = Elab.default_rctx

@@ -41,11 +42,11 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> if 10 <= (!global_verbose_lvl) then (

let var = [ - ((dloc, Some "a"), DB.type_int, (make_val "a")); - ((dloc, Some "b"), DB.type_int, (make_val "b")); - ((dloc, Some "c"), DB.type_int, (make_val "c")); - ((dloc, Some "d"), DB.type_int, (make_val "d")); - ((dloc, Some "e"), DB.type_int, (make_val "e")); + ((dsinfo, Some "a"), DB.type_int, (make_val "a")); + ((dsinfo, Some "b"), DB.type_int, (make_val "b")); + ((dsinfo, Some "c"), DB.type_int, (make_val "c")); + ((dsinfo, Some "d"), DB.type_int, (make_val "d")); + ((dsinfo, Some "e"), DB.type_int, (make_val "e")); ] in

let n = (List.length var) - 1 in

===================================== tests/instargs_test.ml ===================================== @@ -34,10 +34,10 @@ let add_test = add_test "INSTARGS"

let default_ectx = E.default_ectx let default_rctx = E.default_rctx -let dummy_vname = Util.dummy_location, None +let dummy_vname = DB.dsinfo, None

let make_metavar t ctx = - E.newInstanceMetavar ctx (Util.dummy_location, Some "inst") t + E.newInstanceMetavar ctx (DB.dsinfo, Some "inst") t

let lexp_from_str str ctx = List.hd (E.lexp_expr_str str ctx) @@ -171,7 +171,7 @@ let to_nat n ctx = let s = lexp_from_str "S" ctx in let z = lexp_from_str "Z" ctx in let rec loop i nat = - if i = 0 then nat else loop (i - 1) (L.mkCall (s,[Pexp.Anormal, nat])) in + if i = 0 then nat else loop (i - 1) (L.mkCall (DB.dsinfo, s,[Pexp.Anormal, nat])) in loop n z

let to_snat n ctx = @@ -181,13 +181,13 @@ let to_snat n ctx = let rec loop i nat snat = if i = 0 then snat else loop (i - 1) - (L.mkCall (s,[Pexp.Anormal, nat])) - (L.mkCall (ss,[Pexp.Aimplicit, nat; Pexp.Aimplicit, snat])) in + (L.mkCall (DB.dsinfo, s,[Pexp.Anormal, nat])) + (L.mkCall (DB.dsinfo, ss,[Pexp.Aimplicit, nat; Pexp.Aimplicit, snat])) in loop n (to_nat 0 ctx) zs

let snat_n_t n ctx = let snat = lexp_from_str "SNat" ctx in - L.mkCall (snat, [Pexp.Anormal, to_nat n ctx]) + L.mkCall (DB.dsinfo, snat, [Pexp.Anormal, to_nat n ctx])

let snat_metavar i ctx = make_metavar (snat_n_t i ctx) ctx

===================================== tests/positivity_test.ml ===================================== @@ -23,7 +23,7 @@ open Utest_lib

open Lexp open Positivity -open Util +(*open Util*)

exception WrongPolarity of vname

===================================== tests/unify_test.ml ===================================== @@ -35,6 +35,8 @@ module U = Util let ectx = Elab.default_ectx let rctx = Elab.default_rctx

+let dsinfo = DB.dsinfo + type result = | Constraint | Unification @@ -94,19 +96,19 @@ let _ = | Z | S (Nat); |} ectx in - let dloc = U.dummy_location in - let nat = mkVar ((dloc, Some "Nat"), 2) in + let dsinfo = DB.dsinfo in + let nat = mkVar ((dsinfo, Some "Nat"), 2) in let shift l i = mkSusp l (S.shift i) in let ectx, _ = List.fold_left (fun (ectx, i) (name, lexp) -> - Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) + Elab.ctx_extend ectx (dsinfo, Some name) Variable (shift lexp i), i + 1) (ectx, 0) - [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, - mkArrow (Anormal, (dloc, Some "y"), shift nat 1, - dloc, shift nat 2)))); + [("f", (mkArrow (dsinfo, Anormal, (dsinfo, None), nat, shift nat 1))); + ("g", (mkArrow (dsinfo, Anormal, (dsinfo, None), nat, shift nat 1))); + ("h", (mkArrow (dsinfo, Anormal, (dsinfo, Some "x"), nat, + mkArrow (dsinfo, Anormal, (dsinfo, Some "y"), shift nat 1, + shift nat 2)))); ("a", nat); ("b", nat)] in

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