Re: [Typer] Implémentation du type Interval

... 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