... suite:
diff --git a/src/opslexp.ml b/src/opslexp.ml index b18a7ea..d08d170 100644 --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -190,10 +190,10 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = lexp_whnf (mkCall (l, push_susp body (S.substitute (lexp_whnf arg ctx)), args)) ctx - | Call (l, f', xs1) -> mkCall (l, f', List.append xs1 xs) + | Call (l, f', xs1) -> lexp_whnf (mkCall (l, f', List.append xs1 xs)) ctx
Yup.
| Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with - | Some f -> Option.value ~default:e (f ctx args) + | Some f -> Option.value ~default:e (f ctx xs) | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) ->
[...]
@@ -289,18 +290,29 @@ and lexp'_whnf e (ctx : DB.lexp_context) : lexp' =
and eq_cast_whnf ctx args = match args with - | [_l; _t; _x; _y; (_, p); _f; (_, fx)] + | [_l1; _l2; _t; _x; _y; (_, p); _f; (_, fx)] -> (match lexp'_whnf p ctx with - | Call (_, refl, _) when conv_p ctx refl DB.eq_refl + | Call (_, eq, _) when conv_p ctx eq DB.eq_eq -> Some (lexp_whnf fx ctx) | _ -> None) | _ -> None
Good.
@@ -203,10 +203,11 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (l, DB.eq_refl, - [Pexp.Aerasable, elevel; - Pexp.Aerasable, etype; - Pexp.Aerasable, e]) in + let constFunction = mkLambda (Pexp.Aerasable, (dsinfo, None), etype, e) in + mkCall (l, DB.eq_eq, + [Pexp.Aerasable, elevel; + Pexp.Aerasable, etype; + Pexp.Anormal, constFunction]) in let reduce it name aargs = let targs = match lexp'_whnf it ctx with | Inductive (_,_,fargs,_) -> fargs
It's probably worthwhile moving this to a separate function `mk_eq_witness` or some such.
+and eq_uneq_whnf ctx args = + match args with + | [_l; _t; (_, x); (_, y); _p; (_, i)] + -> if conv_p ctx i DB.interval_i0 + then Some (lexp_whnf x ctx) + else if conv_p ctx i DB.interval_i1 + then Some (lexp_whnf y ctx) + else None + | _ -> None
Good, compte tenu de la convention d'appel actuelle des "reducible_builtins". Mais cette convention d'appel devrait être changée: - There can also be more arguments. Same thing with `Eq.cast` and probably most other builtins for which we'll want to add rules. So I think that we should return `Some (newexp, args)` where `args` are the "leftover" args. - Also, I think it'd be better to let the caller apply `lexp_whnf` to the result, since it's probably going to be useful for all the "reducible_builtins". Voilà, Stefan