Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer

Commits: 62b305cd by “falismai@iro.umontreal.ca” at 2022-04-27T15:48:06+00:00 String.sub

- - - - -

17 changed files:

- − .idea/.gitignore - − .idea/misc.xml - − .idea/modules.xml - − .idea/typer.iml - − .idea/vcs.xml - − .vscode/settings.json - debug_util.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/positivity.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== .idea/.gitignore deleted ===================================== @@ -1,8 +0,0 @@ -# Default ignored files -/shelf/ -/workspace.xml -# Editor-based HTTP Client requests -/httpRequests/ -# Datasource local storage ignored files -/dataSources/ -/dataSources.local.xml

===================================== .idea/misc.xml deleted ===================================== @@ -1,8 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<project version="4"> - <component name="SwUserDefinedSpecifications"> - <option name="specTypeByUrl"> - <map /> - </option> - </component> -</project> \ No newline at end of file

===================================== .idea/modules.xml deleted ===================================== @@ -1,8 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<project version="4"> - <component name="ProjectModuleManager"> - <modules> - <module fileurl="file://$PROJECT_DIR$/.idea/typer.iml" filepath="$PROJECT_DIR$/.idea/typer.iml" /> - </modules> - </component> -</project> \ No newline at end of file

===================================== .idea/typer.iml deleted ===================================== @@ -1,9 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<module type="JAVA_MODULE" version="4"> - <component name="NewModuleRootManager" inherit-compiler-output="true"> - <exclude-output /> - <content url="file://$MODULE_DIR$" /> - <orderEntry type="inheritedJdk" /> - <orderEntry type="sourceFolder" forTests="false" /> - </component> -</module> \ No newline at end of file

===================================== .idea/vcs.xml deleted ===================================== @@ -1,6 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<project version="4"> - <component name="VcsDirectoryMappings"> - <mapping directory="" vcs="Git" /> - </component> -</project> \ No newline at end of file

===================================== .vscode/settings.json deleted ===================================== @@ -1,6 +0,0 @@ -{ - "ocaml.sandbox": { - "kind": "opam", - "switch": "default" - } -} \ No newline at end of file

===================================== debug_util.ml ===================================== @@ -58,8 +58,8 @@ open Builtin open Debruijn open Env

-let dloc = dummy_sinfo -let dummy_decl = Imm(String(sexp_location(dloc), "Dummy")) +let dsinfo = dummy_sinfo +let dummy_decl = Imm (String (dsinfo, "Dummy"))

let discard _v = ()

@@ -306,7 +306,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 ===================================== @@ -53,11 +53,13 @@ * * ---------------------------------------------------------------------------*)

-(* open Pexp *) (* arg_kind *) +(* open Pexp + open Sexp + *) (* arg_kind *)

module OL = Opslexp open Lexp -open Sexp +

module DB = Debruijn module E = Env @@ -98,10 +100,11 @@ let set_predef name lexp = predef_map := SMap.add name lexp (!predef_map)

(* Builtin types *) -let dloc = DB.dloc +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

@@ -110,8 +113,8 @@ let o2v_list lst = (* FIXME: We're not using predef here. This will break if we change * the definition of `List` in builtins.typer. *) List.fold_left (fun tail elem - -> E.Vcons (((sexp_location dloc), "cons"), [E.Vsexp (elem); tail])) - (E.Vcons (((sexp_location dloc), "nil"), [])) + -> E.Vcons ((dloc, "cons"), [E.Vsexp (elem); tail])) + (E.Vcons ((dloc, "nil"), [])) (List.rev lst)

@@ -141,7 +144,7 @@ let add_builtin_cst (name : string) (e : lexp) lmap := SMap.add name (e, t) map

let new_builtin_type name kind = - let t = mkBuiltin (((sexp_location dloc), name), kind) in + let t = mkBuiltin ((dloc, name), kind) in add_builtin_cst name t; t

@@ -160,7 +163,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 ===================================== @@ -83,48 +83,51 @@ let fatal ?print_action ?loc fmt = (* Type definitions * ---------------------------------- *)

-let dloc = dummy_sinfo -let type_level_sort = mkSort (dloc, StypeLevel) -let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((sexp_location dloc, "TypeLevel"), type_level_sort) +let dloc = dummy_location +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 type_int = mkBuiltin ((sexp_location dloc, "Int"), type0) -let type_integer = mkBuiltin ((sexp_location dloc, "Integer"), type0) -let type_float = mkBuiltin ((sexp_location dloc, "Float"), type0) -let type_string = mkBuiltin ((sexp_location dloc, "String"), type0) -let type_elabctx = mkBuiltin ((sexp_location dloc, "Elab_Context"), type0) +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 type_eq = mkBuiltin ((sexp_location dloc, "Eq"), type_eq_type) + 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 - mkBuiltin ((sexp_location 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, + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + let xv = (dsinfo, Some "x") in + mkBuiltin ((dloc, "Eq.refl"), + 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); @@ -197,9 +200,9 @@ let senv_lookup (name: string) (ctx: elab_context): int = else names) map [] in - if ((String.sub name 0 1) = "_" || - (String.sub name ((String.length name) - 1) 1) = "_") && - ((String.length name) > 1) then + if ((String.length name) > 1) && + ((String.sub name 0 1) = "_" || + (String.sub name ((String.length name) - 1) 1) = "_") then search r else [] in

===================================== src/elab.ml ===================================== @@ -62,8 +62,9 @@ module EL = Elexp

open Printf

-(* dummies *) -let dloc = dummy_sinfo +(* dummies +* let dsinfo = dummy_sinfo +*)

let parsing_internals = ref false let btl_folder = @@ -111,7 +112,7 @@ let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0

let add_special_form (name, func) = - BI.add_builtin_cst name (mkBuiltin (((sexp_location dloc), name) , type_special_form)); + BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form)); special_forms := SMap.add name func (!special_forms)

let get_special_form name = @@ -439,12 +440,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) - | 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) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, loop o t1, loop (1 + o) t2) + | Lambda (l, ak, v, t, e) + -> mkLambda (l, ak, v, loop o t, loop (1 + o) e) + | 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) @@ -617,12 +618,12 @@ and get_implicit_arg ctx loc oname t =

(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = - let rec instantiate t args = + let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) + | Arrow (_, ak , (_, v), t1, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args), t) + | _ -> (mkCall (dsinfo, e, List.rev args), t) in instantiate t []

and infer_type pexp ectx var = @@ -658,7 +659,7 @@ and infer_type pexp ectx var = 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 @@ -668,7 +669,7 @@ 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 @@ -706,7 +707,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; @@ -750,7 +751,7 @@ and check_case rtype (loc, target, ppatterns) ctx = -> unify_ind it it'; (cs, args) | None -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) + | Inductive (l, _, fargs, constructors) -> let (_s, targs) = List.fold_left (fun (s, targs) (ak, name, t) -> let arg = newMetavar @@ -761,12 +762,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 (l, 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'; @@ -796,7 +797,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 *) @@ -819,7 +820,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let rec inst_args ctx e = let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in match lexp_lexp' lxp with - | Lambda (Aerasable, v, t, body) + | Lambda (_, Aerasable, v, t, body) -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) v t in let nctx = ctx_extend ctx v Variable t in @@ -890,11 +891,11 @@ 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 (loc, 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 (loc, 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 @@ -943,7 +944,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = 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 @@ -952,7 +953,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 @@ -972,7 +973,7 @@ 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 (_, 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) @@ -996,16 +997,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 sarg - ltp' Anormal (dloc, None) None in + 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 = @@ -1022,11 +1023,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_sinfo, aa)) + -> mkArrow (dsinfo, ak, n, t, aa)) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> mkArrow (Aerasable, vname, t, l, e)) + -> mkArrow (l, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1034,7 +1035,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 @@ -1102,7 +1103,7 @@ 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`. *) - EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) ([], []) + EV.eval_call loc (EL.Var ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args

(* Print each generated decls *) @@ -1198,7 +1199,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = | _ -> t in let g = generalize nctx (strip_rettype t) in g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) + -> mkArrow (l, Aerasable, name, t, e)) t

and infer_and_generalize_def (ctx : elab_context) se = @@ -1206,12 +1207,12 @@ and infer_and_generalize_def (ctx : elab_context) se = let (e,t) = infer se nctx in let g = generalize nctx e in let e' = g (fun ne vname t _l e - -> mkLambda ((if ne then Aimplicit else Aerasable), + -> mkLambda (se, (if ne then Aimplicit else Aerasable), vname, t, e)) e in let t' = g (fun ne name t _l e - -> mkArrow ((if ne then Aimplicit else Aerasable), - name, t, se, e)) + -> mkArrow (se, (if ne then Aimplicit else Aerasable), + name, t, e)) t in (e', t')

@@ -1518,7 +1519,7 @@ let sform_arrow kind ctx loc sargs _ot = let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in let lt2 = infer_type st2 nctx (st2, None) in - (mkArrow (kind, v, lt1, loc, lt2), Lazy) + (mkArrow (loc, kind, v, lt1, lt2), Lazy) | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc

@@ -1638,9 +1639,9 @@ let rec sform_lambda kind ctx loc sargs ot = | Some lt2 -> Some (srename (loc, None) lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in - (mkLambda (kind, (loc, None), lt1, lbody), + (mkLambda (loc, kind, (loc, None), lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, (loc, None), lt1, loc, lt2)) + | Inferred lt2 -> Inferred (mkArrow (loc, kind, (loc, None), lt1, lt2)) | _ -> alt) in

(match ot with @@ -1653,7 +1654,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' @@ -1661,7 +1662,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. *) @@ -1672,9 +1673,9 @@ let rec sform_lambda kind ctx loc sargs ot = (* FIXME: Don't go back to sform_lambda, but use an internal * loop to avoid re-computing olt1 each time. *) let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in - (mkLambda (ak2, v, lt1, lam), + (mkLambda (loc, 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 @@ -1890,7 +1891,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 @@ -1899,7 +1900,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/eval.ml ===================================== @@ -553,7 +553,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 = @@ -624,18 +624,18 @@ 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 eval_call a b = eval_call (sexp_location loc) trace_dum depth a b 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] -> sxp, nd, sym, str, it, flt, blk - | _ -> error (sexp_location loc) "sexp_dispatch expects 7 arguments" in + | _ -> error loc "sexp_dispatch expects 7 arguments" in

let sxp = match sxp with | Vsexp(sxp) -> sxp | _ -> fatal - (sexp_location loc) + loc "sexp_dispatch expects a Sexp as 1st arg\n%s" (trace_value sxp) in

@@ -711,17 +711,17 @@ and print_eval_trace trace = let (a, _b) = !global_eval_trace in print_trace " EVAL TRACE " trace a

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

match args_val with | [Vcommand cmd; callback] -> (* bind returns another Vcommand *) Vcommand (fun () - -> match eval_call (sexp_location loc) trace_dum depth callback [cmd ()] with + -> match eval_call loc trace_dum depth callback [cmd ()] with | Vcommand cmd -> cmd () - | _ -> error (sexp_location loc) "IO.bind second arg did not return a command") - | _ -> error (sexp_location loc) "Wrong number of args or wrong first arg value in `IO.bind`" + | _ -> error loc "IO.bind second arg did not return a command") + | _ -> error loc "Wrong number of args or wrong first arg value in `IO.bind`"

let io_run loc _depth args_val = match args_val with | [Vcommand cmd; v] -> let _ = cmd () in v @@ -1030,7 +1030,7 @@ let register_builtin_functions () = ("Sexp.integer" , make_integer, 1); ("Sexp.float" , make_float, 1); ("Sexp.node" , make_node, 2); - (*("Sexp.dispatch" , sexp_dispatch, 7);*) + ("Sexp.dispatch" , sexp_dispatch, 7); ("TypeLevel.succ" , typelevel_succ, 1); ("TypeLevel.⊔" , typelevel_lub, 2); ("Reader.parse" , reader_parse,2); @@ -1042,7 +1042,7 @@ let register_builtin_functions () = ("Float->String" , float_to_string, 1); ("Int->String" , int_to_string, 1); ("Integer->String", integer_to_string, 1); - (*("IO.bind" , io_bind, 2);*) + ("IO.bind" , io_bind, 2); ("IO.return" , io_return, 1); ("IO.run" , io_run, 2); ("Sys.exit" , sys_exit, 1);

===================================== src/inverse_subst.ml ===================================== @@ -275,13 +275,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 , + | Lambda (l, ak, v, t, e) + -> mkLambda (l, ak, v, apply_inv_subst t s , apply_inv_subst e (ssink v 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 ===================================== @@ -72,9 +72,9 @@ type ltype = lexp | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of sinfo * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * sinfo * ltype - | Lambda of arg_kind * vname * ltype * lexp - | Call of lexp * (arg_kind * lexp) list (* Curried call. *) + | Arrow of sinfo * arg_kind * vname * ltype * ltype + | Lambda of sinfo * arg_kind * vname * ltype * lexp + | 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 @@ -219,12 +219,12 @@ 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)))) - | Lambda (k, v, t, e) + | Lambda (_l, k, v, t, e) -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) (U.combine_hash (lexp_hash t) (lexp_hash e))) @@ -249,7 +249,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 (_l, 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))) @@ -280,9 +280,9 @@ let hc_eq e1 e2 = (fun (_, e1, t1) (_, e2, t2) -> t1 == t2 && e1 == e2) defs1 defs2 | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) -> ak1 = ak2 && t11 == t12 && t21 == t22 - | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) + | (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)) @@ -321,17 +321,17 @@ let mkSort (l, s) = hc (Sort (l, s)) let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) 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 mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) +let mkArrow (l, k, v, t1, t2) = hc (Arrow (l, k, v, t1, t2)) +let mkLambda (l, k, v, t, e) = hc (Lambda (l, 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

@@ -519,20 +519,20 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))

let rec lexp_location e = match lexp_lexp' e with - | Sort (l,_) -> l + | Sort (si,_) -> si | SortLevel (SLsucc e) -> lexp_location e | SortLevel (SLlub (e, _)) -> lexp_location e | SortLevel SLz -> dummy_sinfo | Imm s -> s - | Var ((_l,_),_) -> dummy_sinfo - | Builtin ((_l, _), _) -> dummy_sinfo - | Let (l,_,_) -> l - | Arrow (_,_,_,l,_) -> l - | Lambda (_,(_l,_),_,_) -> dummy_sinfo - | Call (f,_) -> lexp_location f - | Inductive (l,_,_,_) -> l - | Cons (_,(_l,_)) -> dummy_sinfo - | Case (l,_,_,_,_) -> l + | Var ((_si,_),_) -> dummy_sinfo + | Builtin ((_si, _), _) -> dummy_sinfo + | Let (si,_,_) -> si + | Arrow (si,_,_,_,_) -> si + | Lambda (_,_,(_si,_),_,_) -> dummy_sinfo + | Call (_,f,_) -> lexp_location f + | Inductive (si,_,_,_) -> si + | Cons (_,(_si,_)) -> dummy_sinfo + | Case (si,_,_,_,_) -> si | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(_l,_)) -> dummy_sinfo @@ -562,10 +562,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) ) - | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s , mkSusp e (ssink v s) ) - | Call (f, args) -> mkCall (mkSusp f s , + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, mkSusp t1 s , mkSusp t2 (ssink v s) ) + | Lambda (l, ak, v, t, e) -> mkLambda (l, ak, v, mkSusp t s , mkSusp e (ssink v 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) @@ -629,10 +629,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) - | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) - | Call (f, args) -> mkCall (clean s f, + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, clean s t1, clean (ssink v s) t2) + | Lambda (l, ak, v, t, e) -> mkLambda (l, ak, v, clean s t, clean (ssink v s) e) + | 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) @@ -686,7 +686,7 @@ let rec lexp_unparse lxp = | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) - | Lambda (kind, vdef, ltp, body) + | Lambda (_loc, kind, vdef, ltp, body) -> let l = lexp_location lxp in let st = lexp_unparse ltp in Node (Symbol (sexp_location l, match kind with @@ -695,7 +695,7 @@ let rec lexp_unparse lxp = | Aerasable -> "lambda_≡>_"), [Node (Symbol (sexp_location 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 (sexp_location loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" @@ -719,7 +719,7 @@ let rec lexp_unparse lxp = [Node (Symbol (U.dummy_location, "_;_"), sdecls); lexp_unparse body ])

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

@@ -902,10 +902,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 -> @@ -1010,15 +1010,15 @@ 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 ) ^ ")"

- | Lambda(k, (_loc, name), ltype, lbody) -> + | Lambda(_loc, k, (_, name), ltype, lbody) -> let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype ) ^ ")" in

(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ @@ -1027,7 +1027,7 @@ and lexp_str ctx (exp : lexp) : string = | Cons(t, (_, ctor_name)) -> (keyword "datacons ") ^ (lexp_str' t ) ^ " " ^ ctor_name

- | Call(fname, args) -> + | Call(_loc, 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 @@ -1151,11 +1151,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)) + | (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 ===================================== @@ -127,7 +127,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 DB.dsinfo S.identity (List.rev defs) in L.scompose s2 s1

@@ -177,17 +177,17 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = * things like full normalization (e.g. lexp_conv_p). *) | Some e' -> lexp_whnf_aux e' ctx ) | Susp (e, s) -> lexp_whnf_aux (push_susp e s ) ctx - | Call (e, []) -> lexp_whnf_aux e ctx - | Call (f, (((_, arg)::args) as xs)) -> + | Call (_l, e, []) -> lexp_whnf_aux e ctx + | Call (_l, f, (((_, arg)::args) as xs)) -> (match lexp_lexp' (lexp_whnf_aux f ctx ) with - | Lambda (_, _, _, body) -> + | Lambda (l, _, _, _, 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_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx )) , + lexp_whnf_aux (mkCall (l, push_susp body (S.substitute (lexp_whnf_aux 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 +200,7 @@ let rec lexp_whnf_aux 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 @@ -235,7 +235,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] - | Call (f, aargs) -> + | Call (l, f, aargs) -> (match lexp_lexp' (lexp_whnf_aux f ctx ) with | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default) ) @@ -264,7 +264,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 (_l, refl, _) when conv_p ctx refl DB.eq_refl -> Some (lexp_whnf fx ctx) | _ -> None) | _ -> None @@ -354,17 +354,17 @@ 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') t12 (srename vd1 t22) - | (Lambda (ak1, l1, t1, e1), Lambda (ak2, _l2, t2, e2)) + | (Lambda (_, ak1, l1, t1, e1), Lambda (_, ak2, _l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) && 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) @@ -417,7 +417,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 = @@ -432,12 +432,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 (DB.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 (DB.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 @@ -468,9 +468,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, (sexp_location (DB.dloc), l1)) , + let ctor = mkSusp (mkCall (DB.dsinfo, mkCons (it, (DB.dloc, l1)) , eaargs) ) subst in - let hlxp = mkCall (ctor, args) in + let hlxp = mkCall (DB.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) @@ -481,7 +481,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 ((DB.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 @@ -663,7 +663,7 @@ 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 @@ -678,20 +678,20 @@ and check'' erased ctx e = | SortK2NotType -> log_tc_error ~loc:(sexp_location (lexp_location t2)) "Not a proper type"; mkSort (loc, StypeOmega) ) - | Lambda (ak, ((l,_) as v), t, e) + | Lambda (l, ak, ((_,_) 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 (_l, 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:(sexp_location (lexp_location arg)) "arg kind mismatch"; assert_type ctx arg at t1; @@ -741,7 +741,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 (lexp_location t, ak, v, t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) args) in @@ -751,7 +751,7 @@ and check'' erased ctx e = (* 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 @@ -779,7 +779,7 @@ and check'' erased ctx e = 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 *) @@ -800,13 +800,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:(sexp_location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (mkCons (it, ((sexp_location 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 @@ -849,16 +849,16 @@ 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 (lexp_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 @@ -937,9 +937,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)) - | Lambda (_, _, t, e) -> fv_union (fv_erase (fv t)) (fv_hoist 1 (fv e)) - | Call (f, args) + | 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) -> List.fold_left (fun fvs (ak, arg) -> let afvs = fv arg in fv_union fvs @@ -1019,7 +1019,7 @@ and get_type ctx 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 @@ -1027,11 +1027,11 @@ and get_type ctx e = match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | _ -> mkSort (l, StypeOmega) ) - | Lambda (ak, ((l,_) as v), t, e) - -> (mkArrow (ak, v, t, l, + | Lambda (l, ak, ((_,_) as v), t, e) + -> (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) @@ -1069,14 +1069,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 (lexp_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 = @@ -1087,16 +1087,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 (lexp_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 ) @@ -1148,10 +1148,10 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Var (v) -> E.Var (v) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)

- | L.Lambda (P.Aerasable, _, _, body) + | L.Lambda (_, P.Aerasable, _, _, body) -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy) )

- | L.Lambda (_, vdef, ty, body) + | L.Lambda (_, _, vdef, ty, body) -> let lctx' = DB.lctx_extend lctx vdef Variable ty in E.Lambda (vdef, erase_type lctx' body)

@@ -1159,7 +1159,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = -> let lctx', edecls = clean_decls lctx decls in E.Let (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) @@ -1268,7 +1268,7 @@ let ctx2tup ctx nctx = 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 (loc, mkCons (mkInductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname,

===================================== 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⃗) * ────────────── @@ -106,7 +106,7 @@ and positive' index lexp = && let index = index + List.length vs in Util.SMap.for_all (fun _ c -> positive_in_constructor index c) cs

- | Lexp.Lambda (_, _, _, e) -> positive index e + | Lexp.Lambda (_, _, _, _, e) -> positive index e

| Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s )

===================================== src/unification.ml ===================================== @@ -73,9 +73,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 - | Lambda (_, _, t, e) -> oi t || oi e - | Call (f, args) + | Arrow (_, _, _, t1, t2) -> oi t1 || oi t2 + | Lambda (_, _, _, t, e) -> oi t || oi e + | Call (_, f, args) -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args | Inductive (_, _, args, cases) -> SMap.fold @@ -260,8 +260,8 @@ and unify' (e1: lexp) (e2: lexp) and unify_arrow (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) @(unify' lexp1 (srename v1 lexp2) @@ -277,8 +277,8 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs *) and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' lambda, lexp_lexp' lxp) with - | (Lambda (var_kind1, v1, ltype1, lexp1), - Lambda (var_kind2, _, ltype2, lexp2)) + | (Lambda (_, var_kind1, v1, ltype1, lexp1), + Lambda (_, var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs) @(unify' lexp1 lexp2 @@ -419,7 +419,7 @@ and unify_var (var: lexp) (lxp: lexp) ctx and unify_call (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

===================================== tests/unify_test.ml ===================================== @@ -92,19 +92,19 @@ let _ = {| type Nat | Z | S (Nat); |} ectx in - let dloc = dummy_sinfo in - let nat = mkVar ((dloc, Some "Nat"), 2) in + let dsinfo = dummy_sinfo 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/62b305cd4de2a96b142d96eaa92ed2d15e...