diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-16 13:24:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-23 18:15:24 +0100 |
| commit | 39cbf75c554cd7e5228bd6cd962766e865c3f26b (patch) | |
| tree | c434651d7d17b9e268b053a40b676009189aca5b /kernel/cClosure.ml | |
| parent | 22ae762fa8940028f6a3d8a5fd4147d5ca3b53b9 (diff) | |
Make some functions on terms more robust w.r.t new term constructs.
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index e1b086b75..fa12e5406 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -480,7 +480,8 @@ let rec lft_fconstr n ft = | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false - | _ -> {norm=ft.norm; term=FLIFT(n,ft)} + | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _ + | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = @@ -958,7 +959,10 @@ let rec knr info m stk = (match evar_value info.i_cache ev with Some c -> knit info env c stk | None -> (m,stk)) - | _ -> (m,stk) + | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _ + | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ + | FCLOS _ -> (m, stk) + (* Computes the weak head normal form of a term *) and kni info m stk = @@ -1034,7 +1038,8 @@ and norm_head info m = mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args) | FProj (p,c) -> mkProj (p, kl info c) - | t -> term_of_fconstr m + | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _ + | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m (* Initialization and then normalization *) |