Simon Génier pushed to branch impl-args-in-datacons at Stefan / Typer

Commits: 281c1364 by Simon Génier at 2020-10-04T12:04:28-04:00 Instantiate implicit arguments in datacons.

The datacons special form is datacons T C, where T is an (inductive) type and C is a symbol for one of its constructor. Before this commit, T has to syntactically be an inductive. This causes problems for types like Decidable, which is in fact not a Type, but a TypeLevel ≡> Type! Now, Typer tries to instanciate implicit arguments before deciding if something is a type or not. This currently only works for datacons, which is the only place I think it is a problem, but the same technique will work in other similar situations.

- - - - - 11c7f262 by Simon Génier at 2020-10-10T18:17:49-04:00 Remove arguments in typecons.

- - - - -

7 changed files:

- btl/builtins.typer - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -192,21 +192,21 @@ Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp;

%% FIXME: "List : ?" should be sufficient but triggers List : Type_ ?ℓ -> Type_ ?ℓ; -%% List a = typecons List (nil) (cons a (List a)); -%% nil = lambda a ≡> datacons (List a) nil; -%% cons = lambda a ≡> datacons (List a) cons; -List = typecons (List (ℓ ::: TypeLevel) (a : Type_ ℓ)) (nil) (cons a (List a)); -nil = datacons List nil; -cons = datacons List cons; +List = lambda a -> typecons List (nil) (cons a (List a)); +%nil = lambda (ℓ : TypeLevel) ≡> lambda (a : Type_ ℓ) ≡> datacons (List a) nil; +%cons = lambda (ℓ : TypeLevel) ≡> lambda (a : Type_ ℓ) ≡> datacons (List a) cons;

%%%% Macro-related definitions

Sexp_block = Built-in "Sexp.block" : String -> Sexp; -Sexp_symbol = Built-in "Sexp.symbol" : String -> Sexp; -Sexp_string = Built-in "Sexp.string" : String -> Sexp; +Sexp_symbol = Built-in "Sexp.symbol" : String -> Sexp; +Sexp_string = Built-in "Sexp.string" : String -> Sexp; Sexp_node = Built-in "Sexp.node" : Sexp -> List Sexp -> Sexp; -Sexp_integer = Built-in "Sexp.integer" : Integer -> Sexp; -Sexp_float = Built-in "Sexp.float" : Float -> Sexp; +Sexp_integer = Built-in "Sexp.integer" : Integer -> Sexp; +Sexp_float = Built-in "Sexp.float" : Float -> Sexp; + +A : Type; +A = 0;

Macro = typecons (Macro) (macro (List Sexp -> IO Sexp));

===================================== src/elab.ml ===================================== @@ -92,6 +92,9 @@ let lexp_fatal loc lexp = let value_fatal loc value = fatal ~loc ~print_action:(value_print_details value)

+let whnf lexp ectx = + OL.lexp_whnf lexp (ectx_to_lctx ectx) + (** Type info returned by elaboration. *) type sform_type = | Checked (* Checked that the expression has the requested type. *) @@ -121,7 +124,11 @@ let sform_default_ectx = ref empty_elab_context * to errors in the user's code). *)

let elab_check_sort (ctx : elab_context) lsort var ltp = - match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) + match (try + let () = print_endline ">>>check sort" in + let res = OL.lexp'_whnf lsort (ectx_to_lctx ctx) in + let () = print_endline "<<<check sort" in + res with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) ~loc:(lexp_location lsort) @@ -419,7 +426,7 @@ let rec meta_to_var ids (e : lexp) = | Imm _ -> e | SortLevel SLz -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1) (loop o e2)) | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e @@ -440,28 +447,21 @@ let rec meta_to_var ids (e : lexp) = -> 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) - | Inductive (l, label, args, cases) - -> let alen = List.length args in - let (_, nargs) - = List.fold_right (fun (ak, v, t) (o', args) - -> let o' = o' - 1 in - (o', (ak, v, loop (o' + o) t) - :: args)) - args (alen, []) in - let ncases - = SMap.map - (fun fields - -> let flen = List.length fields in - let (_, nfields) - = List.fold_right - (fun (ak, v, t) (o', fields) - -> let o' = o' - 1 in - (o', (ak, v, loop (o' + o) t) - :: fields)) - fields (flen + alen, []) in - nfields) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let ncases + = SMap.map + (fun fields + -> let flen = List.length fields in + let (_, nfields) + = List.fold_right + (fun (ak, v, t) (o', fields) + -> let o' = o' - 1 in + (o', (ak, v, loop (o' + o) t) + :: fields)) + fields (flen, []) in + nfields) + cases in + mkInductive (l, label, ncases) | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases @@ -577,7 +577,12 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype =

and elab_special_form ctx f args ot = let loc = lexp_location f in - match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with + match ( + let () = print_endline ">>>elab special form" in + let res = OL.lexp'_whnf f (ectx_to_lctx ctx) in + let () = print_endline "<<<elab special form" in + res + ) with | Builtin ((_, name), _, _) -> (* Special form. *) (get_special_form name) ctx loc args ot @@ -622,22 +627,56 @@ and get_implicit_arg ctx loc oname t = | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) (loc, oname) t

-(* Build the list of implicit arguments to instantiate. *) +(** Given a value [e] of type [t], wrap [e] in applications of its implicit + arguments. Returns a pair of the wrapped [e] and the [t] stripped of its + implicit arguments *) and instantiate_implicit e t ctx = let rec instantiate t args = - match OL.lexp'_whnf t (ectx_to_lctx ctx) with + match ( + let () = print_endline ">>>instanciate implicit" in + let x = OL.lexp'_whnf t (ectx_to_lctx ctx) in + let () = print_endline "<<<instanciate implicit" in + x + ) with | Arrow ((Aerasable | Aimplicit) as 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) in instantiate t []

+(** Like {!instanciate_implicit}, but works on a value directly. Wraps an + implicit (or erasable implicit) λ with an application to its instanciated + argument *) +and instantiate_implicit_of_value value ctx = + let rec instantiate e = + match ( + let () = print_endline ">>>instanciate implicit of value" in + let x = whnf e ctx in + let () = print_endline "<<<instanciate implicit of value" in + x + ) with + | Lambda ((Aerasable | Aimplicit), (_, arg_name), arg_ty, body), _ + -> let arg = get_implicit_arg ctx (lexp_location e) arg_name arg_ty in + instantiate (mkSusp body (S.substitute arg)) + | _ -> ( + let () = print_endline ">>>instanciate implicit of value (other)" in + let x = whnf e ctx in + let () = print_endline "<<<instanciate implicit of value (other)" in + x + ) + in instantiate value + and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) let t, s = infer pexp ectx in - (match OL.lexp'_whnf s (ectx_to_lctx ectx) with + (match ( + let () = print_endline ">>>infer" in + let x = OL.lexp'_whnf s (ectx_to_lctx ectx) in + let () = print_endline ">>>infer" in + x + ) with | Sort (_, _) -> () (* All clear! *) (* FIXME: We could automatically coerce Type levels to Sorts, so we * could write `(a : TypeLevel) -> a -> a` instead of @@ -716,7 +755,12 @@ and unify_or_error lctx lxp ?lxp_name expect actual = * do lots of other things. *) and check_inferred ctx e inferred_t t = let (e, inferred_t) = - match OL.lexp'_whnf t (ectx_to_lctx ctx) with + match ( + let () = print_endline ">>>check" in + let x = OL.lexp'_whnf t (ectx_to_lctx ctx) in + let () = print_endline "<<<check" in + x + ) with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in @@ -740,7 +784,12 @@ and check_case rtype (loc, target, ppatterns) ctx = (* get target and its type *) let tlxp, tltp = infer target ctx in let tknd = OL.get_type (ectx_to_lctx ctx) tltp in - let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with + let tlvl = match ( + let () = print_endline ">>>check case" in + let x = OL.lexp'_whnf tknd (ectx_to_lctx ctx) in + let () = print_endline "<<<check case" in + x + ) with | Sort (_, Stype l) -> l | _ -> fatal "Target lexp's kind is not a sort" in let it_cs_as = ref None in @@ -759,20 +808,10 @@ 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) - -> let (s, targs) = List.fold_left - (fun (s, targs) (ak, name, t) - -> let arg = newMetavar - (ectx_to_lctx ctx) - (ectx_to_scope_level ctx) - name (mkSusp t s) in - (S.cons arg s, (ak, arg) :: targs)) - (S.identity, []) - fargs in - let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); - it_cs_as := Some (it', cs, args); - (cs, args) + | Inductive (_, _, constructors) + -> (ltarget := check_inferred ctx tlxp tltp it'; + it_cs_as := Some (it', constructors, []); + (constructors, [])) | _ -> let call_split e = match OL.lexp'_whnf e (ectx_to_lctx ctx) with | Call (f, args) -> (f, args) @@ -781,9 +820,9 @@ and check_case rtype (loc, target, ppatterns) ctx = unify_ind it it'; let constructors = match OL.lexp'_whnf it (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) - -> assert (List.length fargs = List.length targs); - constructors + | Inductive (_, _, constructors) + -> assert (List.length targs == 0); + constructors | _ -> lexp_error (sexp_location target) tlxp ("Can't `case` on objects of this type: " ^ lexp_string tltp); @@ -951,7 +990,9 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = let loc = lexp_location func in

let rec handle_fun_args largs sargs pending ltp = + let () = print_endline ">>>handle fun args" in let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in + let () = print_endline "<<<handle fun args" in match sargs, lexp_lexp' ltp' with | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type) when SMap.mem aname pending @@ -1501,7 +1542,8 @@ let sform_datacons ctx loc sargs ot = match sargs with | [t; Symbol ((sloc, cname) as sym)] -> let idt, _ = infer t ctx in - (mkCons (idt, sym), Lazy) + let idt = instantiate_implicit_of_value idt ctx in + mkCons (idt, sym), Lazy

| [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc @@ -1518,46 +1560,11 @@ let elab_datacons_arg s = match s with -> (elab_colon_to_ak k, elab_p_id s, t) | _ -> (Anormal, (sexp_location s, None), s)

-let elab_typecons_arg arg : (arg_kind * vname * sexp option) = - match arg with - | 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) - | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) - (sexp_location arg) - "Unrecognized formal arg"; - (Anormal, (sexp_location 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) - | formals :: constrs - -> let (label, formals) = match formals with - | Node (label, formals) -> (label, formals) - | _ -> (formals, []) in - let label = match label with - | Symbol label -> label - | _ -> let loc = sexp_location label in - sexp_error loc "Unrecognized inductive type name"; - (loc, "<error>") in - - let rec parse_formals sformals rformals ctx = match sformals with - | [] -> (List.rev rformals, ctx) - | sformal :: sformals - -> let (kind, var, opxp) = elab_typecons_arg sformal in - let ltp = match opxp with - | Some pxp -> let (l,_) = infer pxp ctx in l - | None -> let (l,_) = var in - newMetatype (ectx_to_lctx ctx) - (ectx_to_scope_level ctx) l in - - parse_formals sformals ((kind, var, ltp) :: rformals) - (ectx_extend ctx var Variable ltp) in - - let (formals, nctx) = parse_formals formals [] ctx in - - let ctors + | (Symbol label) :: constrs + -> let ctors = List.fold_right (fun case pcases -> match case with @@ -1572,8 +1579,10 @@ let sform_typecons ctx loc sargs ot = pcases) constrs [] in

- let map_ctor = lexp_parse_inductive ctors nctx in - (mkInductive (loc, label, formals, map_ctor), Lazy) + let map_ctor = lexp_parse_inductive ctors ctx in + (mkInductive (loc, label, map_ctor), Lazy) + | _ :: _ -> sexp_error loc "##typecons: first argument must be a symbol"; + sform_dummy_ret ctx loc

let sform_hastype ctx loc sargs ot = match sargs with @@ -1708,7 +1717,9 @@ let rec sform_lambda kind ctx loc sargs ot = None (* Read var type from the provided type *) | Some t - -> let lp = OL.lexp_whnf t (ectx_to_lctx ctx) in + -> let () = print_endline ">>>sform lambda" in + let lp = OL.lexp_whnf t (ectx_to_lctx ctx) in + let () = print_endline "<<<sform lambda" in match lexp_lexp' lp with | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind -> (match olt1 with

===================================== src/inverse_subst.ml ===================================== @@ -258,7 +258,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) | SortLevel (SLlub (e1, e2)) (* FIXME: use mkSLlub? *) - -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) + -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s) (apply_inv_subst e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) | Sort (l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e @@ -281,22 +281,18 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Call (f, args) -> mkCall (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) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, apply_inv_subst t s) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let () = print_endline "subst" in let ncases = + SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, apply_inv_subst t s) + :: nargs)) + (s, []) args in + L.rev ncase) + cases in + mkInductive (l, label, ncases) | Cons (it, name) -> mkCons (apply_inv_subst it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s,

===================================== src/lexp.ml ===================================== @@ -74,8 +74,8 @@ type ltype = lexp | Arrow of arg_kind * vname * ltype * U.location * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label - * ((arg_kind * vname * ltype) list) (* formal Args *) + | Inductive of U.location + * label * ((arg_kind * vname * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) | Case of U.location * lexp @@ -220,15 +220,10 @@ let lexp'_hash (lp : lexp') = -> 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))) - | Inductive (l, n, a, cs) + | Inductive (l, n, cs) -> U.combine_hash 9 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) - (U.combine_hash (U.combine_hashes - (List.map (fun e -> let (ak, n, lt) = e in - (U.combine_hash (Hashtbl.hash ak) - (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) - a)) - (Hashtbl.hash cs))) + (Hashtbl.hash cs)) | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) -> U.combine_hash 11 (U.combine_hash @@ -277,11 +272,11 @@ let hc_eq e1 e2 = | (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)) - -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2) as1 as2 - && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2)) ctor1 ctor2 + | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2)) + -> l1 = l2 + && SMap.equal (List.for_all2 + (fun (ak1, _, e1) (ak2, _, e2) + -> ak1 = ak2 && e1 == e2)) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) -> e1 == e2 && r1 == r2 && SMap.equal @@ -305,18 +300,18 @@ let hc_table : WHC.t = WHC.create 1000 let hc (l : lexp') : lexp = WHC.merge hc_table (l, lexp'_hash l)

-let mkImm s = hc (Imm s) -let mkSortLevel l = hc (SortLevel l) -let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t, m) = hc (Builtin (v, t, m)) -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 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 mkImm s = hc (Imm s) +let mkSortLevel l = hc (SortLevel l) +let mkSort (l, s) = hc (Sort (l, s)) +let mkBuiltin (v, t, m) = hc (Builtin (v, t, m)) +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 mkInductive (l, n, cs) = hc (Inductive (l, n, 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) = match lexp_lexp' f, es with | Call (f', es'), _ -> hc (Call (f', es' @ es)) @@ -325,7 +320,7 @@ let mkCall (f, es) =

let impossible = mkImm Sexp.dummy_epsilon

-let lexp_head e = +let lexp_head (e : lexp) : string = match lexp_lexp' e with | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" @@ -343,17 +338,17 @@ let lexp_head e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel"

-let mkSLlub' (e1, e2) = - match (lexp_lexp' e1, lexp_lexp' e2) with +let mkSLlub' (e1 : lexp) (e2 : lexp) : sort_level = + match e1, e2 with (* FIXME: This first case should be handled by calling `mkSLlub` instead! *) - | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l - | (SortLevel SLz, _) | (_, SortLevel SLz) - -> Log.log_fatal ~section:"internal" "lub of SLz" - | (SortLevel (SLsucc _), SortLevel (SLsucc _)) + | (SortLevel SLz, _), (SortLevel l, _) | (SortLevel l, _), (SortLevel SLz, _) -> l + | (SortLevel (SLsucc _), _), (SortLevel (SLsucc _), _) -> Log.log_fatal ~section:"internal" "lub of two SLsucc" - | ((SortLevel _ | Var _ | Metavar _ | Susp _), - (SortLevel _ | Var _ | Metavar _ | Susp _)) + | ((SortLevel _ | Var _ | Metavar _ | Susp _), _), + ((SortLevel _ | Var _ | Metavar _ | Susp _), _) -> SLlub (e1, e2) + | (SortLevel SLz, _), other | other, (SortLevel SLz, _) + -> Log.log_fatal ~section:"internal" ("lub of SLz with " ^ lexp_head other) | _ -> Log.log_fatal ~section:"internal" ("SLlub of non-level: " ^ lexp_head e1 ^ " ∪ " ^ lexp_head e2)

@@ -392,16 +387,16 @@ let get_var_vname v =

let pred_inductive l pred = match lexp_lexp' l with - | Inductive (l, n, a, cs) -> pred (l, n, a, cs) + | Inductive (l, n, cs) -> pred (l, n, cs) | _ -> false

let get_inductive l = match lexp_lexp' l with - | Inductive (l, n, a, cs) -> (l, n, a, cs) + | Inductive (l, n, cs) -> (l, n, cs) | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive "

let get_inductive_ctor i = - let (l, n, a, cs) = i in cs + let (_, _, cs) = i in cs

let is_inductive l = pred_inductive l (fun e -> true)

@@ -515,7 +510,7 @@ let rec lexp_location e = | Arrow (_,_,_,l,_) -> l | Lambda (_,(l,_),_,_) -> l | Call (f,_) -> lexp_location f - | Inductive (l,_,_,_) -> l + | Inductive (l,_,_) -> l | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e @@ -529,13 +524,20 @@ let vdummy = (U.dummy_location, None) let maybename n = match n with None -> "<anon>" | Some v -> v let sname (l,n) = (l, maybename n)

+let level = ref 0 + let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s)) | SortLevel (SLlub (e1, e2)) - -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) + -> (print_endline (">>>[" ^ string_of_int !level ^ "]pushing susp on lub"); + level := !level + 1; + let sl = mkSortLevel (mkSLlub' (mkSusp e1 s) (mkSusp e2 s)) in + level := !level - 1; + print_endline ("<<<[" ^ string_of_int !level ^ "]pushing susp on lub"); + sl) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e @@ -552,21 +554,22 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) | Call (f, args) -> mkCall (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) - -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, mkSusp t s) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let () = print_endline ">>>push susp" in + let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, mkSusp t s) + :: nargs)) + (s, []) + args + in + L.rev ncase) + cases in + let res = mkInductive (l, label, ncases) in + let () = print_endline "<<<push susp" in + res | Cons (it, name) -> mkCons (mkSusp it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s, mkSusp ret s, @@ -603,7 +606,7 @@ let clean e = | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) | SortLevel (SLlub (e1, e2)) (* FIXME: The new SLlub could have `succ` on both sides! *) - -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) + -> (print_endline "cleaning lub"; mkSortLevel (mkSLlub' (clean s e1) (clean s e2))) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (l, _) -> e | Builtin _ -> e @@ -619,21 +622,17 @@ let clean e = | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) | Call (f, args) -> mkCall (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) - -> (ssink v s, (ak, v, clean s t) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, clean s t) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let () = print_endline "LEXP2" in let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, clean s t) + :: nargs)) + (s, []) args in + L.rev ncase) + cases in + mkInductive (l, label, ncases) | Cons (it, name) -> mkCons (clean s it, name) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, @@ -708,14 +707,11 @@ let rec lexp_unparse lxp = let sargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in Node (lexp_unparse lxp, sargs)

- | Inductive(loc, label, lfargs, ctors) -> + | Inductive(loc, label, ctors) -> (* (arg_kind * vdef * ltype) list *) (* (arg_kind * pvar * pexp option) list *) - let pfargs = List.map (fun (kind, vdef, ltp) -> - (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in - Node (stypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) + Symbol label :: List.map (fun (name, types) -> Node (Symbol (loc, name), @@ -1031,21 +1027,10 @@ and lexp_str ctx (exp : lexp) : string = | _ -> let args = List.fold_left print_arg "" args in "(" ^ (lexp_str' fname) ^ args ^ ")")

- | Inductive (_, (_, name), [], ctors) -> + | Inductive (_, (_, name), ctors) -> (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ (lexp_str_ctor ctx ctors)

- | Inductive (_, (_, name), args, ctors) - -> let args_str - = List.fold_left - (fun str (arg_kind, (_, name), ltype) - -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str' ltype) ^ ")") - "" args in - - (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ - (lexp_str_ctor ctx ctors) - | Case (_, target, _ret, map, dflt) ->( let str = (keyword "case ") ^ (lexp_str' target) in let arg_str arg @@ -1143,11 +1128,10 @@ let rec eq e1 e2 = | (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)) - -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 - && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2)) ctor1 ctor2 + | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2)) + -> let ctor_eq (ak1, _, e1) (ak2, _, e2) = + ak1 = ak2 && eq e1 e2 + in l1 = l2 && SMap.equal (List.for_all2 ctor_eq) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) -> eq e1 e2 && eq r1 r2 && SMap.equal

===================================== src/opslexp.ml ===================================== @@ -149,6 +149,8 @@ let lexp_close lctx e = * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *)

+let whnf_level = ref 0 + (* FIXME This large letrec closes the loop between lexp_whnf_aux and get_type so that we can use get_type in the WHNF of a case to get the inductive type of the target (and it's typelevel). A better @@ -185,33 +187,28 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | _ -> Log.internal_error "" in mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in let reduce it name aargs = - let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with - | Inductive (_,_,fargs,_) -> fargs - | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in + let () = match lexp_lexp' (lexp_whnf_aux it ctx) with + | Inductive _ -> () + | _ -> Log.log_error "Case on a non-inductive type in whnf!" in try let (_, _, branch) = SMap.find name branches in - let (subst, _) + let subst = List.fold_left - (fun (s, targs) (_, arg) -> - match targs with - | [] -> (S.cons (lexp_whnf_aux arg ctx) s, []) - | _targ::targs -> - (* Ignore the type arguments *) - (s, targs)) - (S.identity, targs) + (fun s (_, arg) -> S.cons (lexp_whnf_aux arg ctx) s) + S.identity aargs in (* Substitute case Eq variable by the proof (Eq.refl l t e') *) let subst = S.cons (get_refl e') subst in lexp_whnf_aux (push_susp branch subst) ctx with Not_found - -> match default - with | Some (v,default) - -> let subst = S.cons (get_refl e') (S.substitute e') in - lexp_whnf_aux (push_susp default subst) ctx - | _ -> Log.log_error ~section:"WHNF" ~loc:l - ("Unhandled constructor " ^ - name ^ "in case expression"); - mkCase (l, e, rt, branches, default) in + -> match default with + | Some (v,default) + -> let subst = S.cons (get_refl e') (S.substitute e') in + lexp_whnf_aux (push_susp default subst) ctx + | _ -> Log.log_error ~section:"WHNF" ~loc:l + ("Unhandled constructor " ^ + name ^ "in case expression"); + mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> @@ -231,7 +228,13 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =

| elem -> e

- in lexp_whnf_aux e ctx + in (print_endline (">>>lexp_whnf_aux[" ^ string_of_int !whnf_level ^ "]: " ^ Lexp.lexp_string e); + whnf_level := !whnf_level + 1; + let r = lexp_whnf_aux e ctx in + whnf_level := !whnf_level - 1; + print_endline ("<<<lexp_whnf_aux[" ^ string_of_int !whnf_level ^ "]: " ^ Lexp.lexp_string e); + r) +

and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = lexp_lexp' (lexp_whnf_aux e ctx) @@ -292,8 +295,10 @@ and level_leq (c1, m1) (c2, m2) =

(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = + let () = print_endline ">>>conv_p'" in let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in + let () = print_endline "<<<conv_p'" in e1' == e2' || let changed = not (e1 == e1' && e2 == e2') in if changed && set_member_p vs e1' e2' then true else @@ -335,29 +340,17 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = && (conv_erase && ak1 = P.Aerasable || conv_p t1 t2)) true args1 args2 in conv_p f1 f2 && conv_arglist_p args1 args2 - | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) + | (Inductive (_, l1, cases1), Inductive (_, l2, cases2)) -> let rec conv_fields ctx vs fields1 fields2 = - match fields1, fields2 with - | ([], []) -> true - | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) - (set_shift vs) - fields1 fields2 - | _,_ -> false in - let rec conv_args ctx vs args1 args2 = - match args1, args2 with - | ([], []) -> - (* Args checked alright, now go on with the fields, - * using the new context. *) - SMap.equal (conv_fields ctx vs) cases1 cases2 - | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) - (set_shift vs) - args1 args2 - | _,_ -> false in - l1 == l2 && conv_args ctx vs' args1 args2 + match fields1, fields2 with + | ([], []) -> true + | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) + -> ak1 == ak2 && conv_p' ctx vs t1 t2 + && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) + (set_shift vs) + fields1 fields2 + | _,_ -> false in + l1 == l2 && SMap.equal (conv_fields ctx vs) cases1 cases2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 | (Case (_, target1, r1, cases1, def1), Case (_, target2, r2, cases2, def2)) -> (* FIXME The termination of this case conversion is very @@ -382,15 +375,11 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let it, aargs = match lexp_lexp' etype with | Call (f, args) -> (f, args) | _ -> (etype, []) in - (* 2. Build the substitution for the inductive arguments *) - let fargs, ctors = + (* 2. Compare the branches *) + let ctors = (match lexp'_whnf it ctx with - | Inductive (_, _, fargs, constructors) - -> fargs, constructors + | Inductive (_, _, constructors) -> constructors | _ -> Log.log_fatal ("Case of non-inductive in conv_p")) in - let fargs_subst = List.fold_left2 (fun s _farg (_, aarg) -> S.cons aarg s) - S.identity fargs aargs in - (* 3. Compare the branches *) let ctx_extend_with_eq ctx subst hlxp = let tlxp = mkSusp target subst in let tltp = mkSusp etype subst in @@ -423,7 +412,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = vdefs1 vdefs2 fieldtypes else None | _,_,_ -> None in - match mkctx ctx [] fargs_subst (List.length fields1) + match mkctx ctx [] S.identity (List.length fields1) fields1 fields2 fieldtypes with | None -> false | Some (nctx, args, _subst) -> @@ -474,7 +463,7 @@ and mkSLlub ctx e1 e2 = let ce2 = level_canon lwhnf2 in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 - else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) + else mkSortLevel (mkSLlub' e1 e2) (* FIXME: Could be more canonical *)

and sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen @@ -668,53 +657,42 @@ and check'' erased ctx e = ^ lexp_string ft ^ ")!"); ft)) ft args - | Inductive (l, label, args, cases) - -> let rec arg_loop ctx erased args = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _, _) = - List.fold_left - (fun (level, ictx, erased, n) (ak, v, t) -> - ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in - match lexp_lexp' lwhnf with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (* FIXME: If it does refer, - * we get an ugly error! *) - (mkSusp level' (L.sunshift n)) - | tt -> error_tc ~loc:(lexp_location t) - ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline () - ) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string lwhnf ^")"); - level), - DB.lctx_extend ictx v Variable t, - DB.set_sink 1 erased, - n + 1)) - (level, ctx, erased, 0) - case in - level) - cases (mkSortLevel SLz) in - 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, - arg_loop (DB.lctx_extend ctx v Variable t) - (dbset_push ak erased) - args) in - let tct = arg_loop ctx erased args in - tct + | Inductive (l, label, cases) + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _, _) = + List.fold_left + (fun (level, ictx, erased, n) (ak, v, t) -> + ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in + match lexp_lexp' lwhnf with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (* FIXME: If it does refer, + * we get an ugly error! *) + (mkSusp level' (L.sunshift n)) + | tt -> error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string lwhnf ^")"); + level), + DB.lctx_extend ictx v Variable t, + DB.set_sink 1 erased, + n + 1)) + (level, ctx, erased, 0) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -731,7 +709,7 @@ and check'' erased ctx e = "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with - | Inductive (_, _, fargs, constructors), aargs -> + | Inductive (_, _, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with | [], [] -> s @@ -741,7 +719,7 @@ and check'' erased ctx e = -> mksubst (S.cons aarg s) fargs aargs | _,_ -> (error_tc ~loc:l "Wrong arg number to inductive type!"; s) in - let s = mksubst S.identity fargs aargs in + let s = mksubst S.identity [] aargs in let ctx_extend_with_eq ctx subst hlxp nerased = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in @@ -804,37 +782,26 @@ and check'' erased ctx e = ret | Cons (t, (l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) - -> (try - let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in - let rec fieldargs ftypes = - match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) - | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location 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, - buildtype fargs) in - buildtype fargs - with Not_found - -> (error_tc ~loc:l + | Inductive (l, _, constructors) + -> (try + let fieldtypes = SMap.find name constructors in + let rec fieldargs ftypes = + match ftypes with + | [] + -> let nargs = List.length fieldtypes in + mkSusp t (S.shift nargs) + | (ak, vd, ftype) :: ftypes + -> mkArrow (ak, vd, ftype, lexp_location ftype, + fieldargs ftypes) in + fieldargs fieldtypes + with Not_found + -> (error_tc ~loc:l ("Constructor "" ^ name ^ "" does not exist"); - DB.type_int)) - | _ -> (error_tc ~loc:(lexp_location e) - ("Cons of a non-inductive type: " - ^ lexp_string t); - DB.type_int)) + DB.type_int)) + | _ -> (error_tc ~loc:(lexp_location e) + ("Cons of a non-inductive type: " + ^ lexp_string t); + DB.type_int)) | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> let e = push_susp e s in @@ -913,23 +880,17 @@ and fv (e : lexp) : (DB.set * mv_set) = then fv_erase afvs else afvs)) (fv f) args - | Inductive (_, _, args, cases) - -> let alen = List.length args in - let s - = List.fold_left (fun s (_, _, t) - -> fv_sink 1 (fv_union s (fv t))) - fv_empty args in - let s - = SMap.fold - (fun _ fields s - -> fv_union - s - (fv_hoist (List.length fields) - (List.fold_left (fun s (_, _, t) - -> fv_sink 1 (fv_union s (fv t))) - fv_empty fields))) - cases s in - fv_hoist alen s + | Inductive (_, _, cases) + -> SMap.fold + (fun _ fields s + -> fv_union + s + (fv_hoist (List.length fields) + (List.fold_left (fun s (_, _, t) + -> fv_sink 1 (fv_union s (fv t))) + fv_empty fields))) + cases + fv_empty | Cons (t, _) -> fv_erase (fv t) | Case (_, e, t, cases, def) -> let s = fv_union (fv e) (fv_erase (fv t)) in @@ -994,65 +955,45 @@ and get_type ctx e = -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args - | Inductive (l, label, args, cases) + | Inductive (l, label, cases) (* FIXME: Use `check` here but silencing errors? *) - -> let rec arg_loop args ctx = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _) = - List.fold_left - (fun (level, ictx, n) (ak, v, t) -> - ((match lexp'_whnf (get_type ictx t) ictx with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (mkSusp level' (L.sunshift n)) - | tt -> level), - DB.lctx_extend ictx v Variable t, - n + 1)) - (level, ctx, 0) - case in - level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) - | (ak, v, t)::args - -> mkArrow (ak, v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in - let tct = arg_loop args ctx in - tct + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _) = + List.fold_left + (fun (level, ictx, n) (ak, v, t) -> + ((match lexp'_whnf (get_type ictx t) ictx with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) + | tt -> level), + DB.lctx_extend ictx v Variable t, + n + 1)) + (level, ctx, 0) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) + | Inductive (l, _, constructors) -> (try let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) + | [] -> let nargs = List.length fieldtypes in + mkSusp t (S.shift nargs) | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location 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, - buildtype fargs) in - buildtype fargs + fieldargs fieldtypes with Not_found -> DB.type_int) | _ -> DB.type_int) | Metavar (idx, s, _) @@ -1092,7 +1033,7 @@ let rec erase_type (lxp: lexp): E.elexp = | L.SortLevel _ -> E.Type lxp | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Type lxp + | L.Inductive(l, label, _) -> E.Type lxp | L.Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s) @@ -1158,7 +1099,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 (mkCons (mkInductive (loc, type_label, SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname,

===================================== src/unification.ml ===================================== @@ -79,13 +79,13 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | 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) + | Inductive (_, _, cases) -> SMap.fold - (fun _ fields o - -> List.fold_left (fun o (_, _, t) -> o || oi t) - o fields) - cases - (List.fold_left (fun o (_, _, t) -> o || oi t) false args) + (fun _ fields o + -> List.fold_left (fun o (_, _, t) -> o || oi t) + o fields) + cases + false | Cons (t, _) -> oi t | Case (_, e, t, cases, def) -> let o = oi e || oi t in @@ -201,8 +201,11 @@ and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = if e1 == e2 then [] else + let () = print_endline "unify 1" in let e1' = OL.lexp_whnf e1 ctx in + let () = print_endline "unify 2" in let e2' = OL.lexp_whnf e2 ctx in + let () = print_endline "unify 3" in if e1' == e2' then [] else let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then [] else @@ -565,24 +568,24 @@ and is_same arglist arglist2 =

and unify_inductive lxp1 lxp2 ctx vs = match lexp_lexp' lxp1, lexp_lexp' lxp2 with - | (Inductive (_loc1, label1, args1, consts1), - Inductive (_loc2, label2, args2, consts2)) - -> unify_inductive' ctx vs args1 args2 consts1 consts2 lxp1 lxp2 + | (Inductive (_loc1, label1, consts1), + Inductive (_loc2, label2, consts2)) + -> unify_inductive' ctx vs consts1 consts2 lxp1 lxp2 | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]

-and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive' ctx vs consts1 consts2 e1 e2 = + let () = print_endline "unify_inductive'" in let unif_formals ctx vs args1 args2 = if not (List.length args1 == List.length args2) then (ctx, vs, [(CKimpossible, ctx, e1, e2)]) else List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, v2, t2)) -> (DB.lexp_ctx_cons ctx v1 Variable t1, - OL.set_shift vs, - if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] - else (unify' t1 t2 ctx vs) @ residue)) + OL.set_shift vs, + if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] + else (unify' t1 t2 ctx vs) @ residue)) (ctx, vs, []) (List.combine args1 args2) in - let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in if not (SMap.cardinal consts1 == SMap.cardinal consts2) then [(CKimpossible, ctx, e1, e2)] else @@ -592,7 +595,8 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = = unif_formals ctx vs args1 args2 in residue' @ residue | exception Not_found -> [(CKimpossible, ctx, e1, e2)]) - consts1 residue + consts1 + []

(** unify the SMap of list in Inductive *) (* and unify_induct_sub_list l1 l2 subst =

===================================== tests/elab_test.ml ===================================== @@ -49,13 +49,12 @@ let add_elab_test_decl = add_elab_test Elab.lexp_decl_str expect_equal_decls

let _ = add_elab_test_expr - "Instanciate implicit arguments" + "Instanciate implicit arguments in datacons" ~setup:{| -f : (i : Int) -> Eq i i -> Int; -f = lambda i -> lambda eq -> i; +A = typecons (A (prop : Type_ ?ℓ)) (c (p ::: prop)); |} - ~expected:"f 4 (Eq_refl (x := 4));" - "f 4 Eq_refl;" + ~expected:"datacons (A (ℓ := ?ℓ)) c;" + "datacons A c;"

let _ = add_elab_test_decl "Whnf of case"

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6666e7a2ad1db0457f837fe1a9ffe48e8...