Source file `heads.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Util
open Names
open EConstr
open Vars
open Context.Named.Declaration

(** Characterization of the head of a term *)

(* We only compute an approximation to ensure the computation is not
   arbitrary long (e.g. the head constant of [h] defined to be
   [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch
   the evaluation of [phi(0)] and the head of [h] is declared unknown). *)

type rigid_head_kind =
| RigidParameter of Constant.t (* a Const without body. Module substitution may instantiate it with something else. *)
| RigidOther (* a Var without body, inductive, product, sort, projection *)

type head_approximation =
| RigidHead of rigid_head_kind
| ConstructorHead
| FlexibleHead of int * int * int * bool (* [true] if a surrounding case *)
| NotImmediatelyComputableHead

let rec compute_head_const env sigma cst =
  let body = Environ.constant_opt_value_in env (cst,UVars.Instance.empty) in
  match body with
  | None -> RigidHead (RigidParameter cst)
  | Some c -> kind_of_head env sigma (EConstr.of_constr c)

and compute_head_var env sigma id = match lookup_named id env with
| LocalDef (_,c,_) -> kind_of_head env sigma c
| _ -> RigidHead RigidOther

and kind_of_head env sigma t =
  let rec aux k l t b = match EConstr.kind sigma (Reductionops.clos_whd_flags RedFlags.betaiotazeta env sigma t) with
  | Rel n when n > k -> NotImmediatelyComputableHead
  | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
  | Var id ->
      (try on_subterm k l b (compute_head_var env sigma id)
       with Not_found ->
        (* a goal variable *)
        match lookup_named id env with
        | LocalDef (_,c,_) -> aux k l c b
        | LocalAssum _ -> NotImmediatelyComputableHead)
  | Const (cst,_) ->
      (try on_subterm k l b (compute_head_const env sigma cst)
       with Not_found ->
         CErrors.anomaly
           Pp.(str "constant not found in kind_of_head: " ++
               Names.Constant.print cst ++
               str "."))
  | Construct _ | CoFix _ ->
      if b then NotImmediatelyComputableHead else ConstructorHead
  | Sort _ | Ind _ | Prod _ -> RigidHead RigidOther
  | Cast (c,_,_) -> aux k l c b
  | Lambda (_,_,c) ->
    begin match l with
    | [] ->
      let () = assert (not b) in
      aux (k + 1) [] c b
    | h :: l -> aux k l (subst1 h c) b
    end
  | LetIn _ -> assert false
  | Meta _ | Evar _ -> NotImmediatelyComputableHead
  | App (c,al) -> aux k (Array.to_list al @ l) c b
  | Proj (p,_,c) -> RigidHead RigidOther

  | Case (_,_,_,_,_,c,_) -> aux k [] c true
  | Int _ | Float _ | String _ | Array _ -> ConstructorHead
  | Fix ((i,j),_) ->
      let n = i.(j) in
      try aux k [] (List.nth l n) true
      with Failure _ -> FlexibleHead (k + n + 1, k + n + 1, 0, true)
  and on_subterm k l with_case = function
  | FlexibleHead (n,i,q,with_subcase) ->
      let m = List.length l in
      let k',rest,a =
        if n > m then
          (* eta-expansion *)
          let a =
            if i <= m then
              (* we pick the head in the existing arguments *)
              lift (n-m) (List.nth l (i-1))
            else
              (* we pick the head in the added arguments *)
              mkRel (n-i+1) in
          k+n-m,[],a
        else
          (* enough arguments to [cst] *)
          k,List.skipn n l,List.nth l (i-1) in
      let l' = List.make q (mkMeta 0) @ rest in
      aux k' l' a (with_subcase || with_case)
  | ConstructorHead when with_case -> NotImmediatelyComputableHead
  | x -> x
  in aux 0 [] t false

let is_rigid env sigma t =
  match kind_of_head env sigma t with
  | RigidHead _ | ConstructorHead -> true
  | _ -> false