summaryrefslogtreecommitdiff
path: root/plugins/firstorder/formula.ml
blob: f0043140f6ee301261160f2d4037b47b766c44f9 (plain)
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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Hipattern
open Names
open Term
open Termops
open Reductionops
open Tacmach
open Util
open Declarations
open Libnames
open Inductiveops

let qflag=ref true

let red_flags=ref Closure.betaiotazeta

let (=?) f g i1 i2 j1 j2=
  let c=f i1 i2 in
    if c=0 then g j1 j2 else c

let (==?) fg h i1 i2 j1 j2 k1 k2=
  let c=fg i1 i2 j1 j2 in
    if c=0 then h k1 k2 else c

type ('a,'b) sum = Left of 'a | Right of 'b

type counter = bool -> metavariable

exception Is_atom of constr

let meta_succ m = m+1

let rec nb_prod_after n c=
  match kind_of_term c with
    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
	1+(nb_prod_after 0 b)
    | _ -> 0

let construct_nhyps ind gls =
  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
  let hyp = nb_prod_after nparams in
    Array.map hyp constr_types

(* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
let ind_hyps nevar ind largs gls=
  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
  let lp=Array.length types in
  let myhyps i=
    let t1=Term.prod_applist types.(i) largs in
    let t2=snd (decompose_prod_n_assum nevar t1) in
      fst (decompose_prod_assum t2) in
    Array.init lp myhyps

let special_nf gl=
  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
    (fun t -> Closure.norm_val infos (Closure.inject t))

let special_whd gl=
  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
    (fun t -> Closure.whd_val infos (Closure.inject t))

type kind_of_formula=
    Arrow of constr*constr
  | False of inductive*constr list
  | And of inductive*constr list*bool
  | Or of inductive*constr list*bool
  | Exists of inductive*constr list
  | Forall of constr*constr
  | Atom of constr

let rec kind_of_formula gl term =
  let normalize=special_nf gl in
  let cciterm=special_whd gl term in
    match match_with_imp_term cciterm with
	Some (a,b)-> Arrow(a,(pop b))
      |_->
	 match match_with_forall_term cciterm with
	     Some (_,a,b)-> Forall(a,b)
	   |_->
	      match match_with_nodep_ind cciterm with
		  Some (i,l,n)->
		    let ind=destInd i in
		    let (mib,mip) = Global.lookup_inductive ind in
		    let nconstr=Array.length mip.mind_consnames in
		      if nconstr=0 then
			False(ind,l)
		      else
			let has_realargs=(n>0) in
			let is_trivial=
			  let is_constant c =
			    nb_prod c = mib.mind_nparams in
			    array_exists is_constant mip.mind_nf_lc in
			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
			    (has_realargs && not is_trivial)
			  then
			    Atom cciterm
			  else
			    if nconstr=1 then
			      And(ind,l,is_trivial)
			    else
			      Or(ind,l,is_trivial)
		| _ ->
		    match match_with_sigma_type cciterm with
			Some (i,l)-> Exists((destInd i),l)
		      |_-> Atom (normalize cciterm)

type atoms = {positive:constr list;negative:constr list}

type side = Hyp | Concl | Hint

let no_atoms = (false,{positive=[];negative=[]})

let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *)

let build_atoms gl metagen side cciterm =
  let trivial =ref false
  and positive=ref []
  and negative=ref [] in
  let normalize=special_nf gl in
  let rec build_rec env polarity cciterm=
    match kind_of_formula gl cciterm with
	False(_,_)->if not polarity then trivial:=true
      | Arrow (a,b)->
	  build_rec env (not polarity) a;
	  build_rec env polarity b
      | And(i,l,b) | Or(i,l,b)->
	  if b then
	    begin
	      let unsigned=normalize (substnl env 0 cciterm) in
		if polarity then
		  positive:= unsigned :: !positive
		else
		  negative:= unsigned :: !negative
	    end;
	  let v = ind_hyps 0 i l gl in
	  let g i _ (_,_,t) =
	    build_rec env polarity (lift i t) in
	  let f l =
	    list_fold_left_i g (1-(List.length l)) () l in
	    if polarity && (* we have a constant constructor *)
	      array_exists (function []->true|_->false) v
	    then trivial:=true;
	    Array.iter f v
      | Exists(i,l)->
	  let var=mkMeta (metagen true) in
	  let v =(ind_hyps 1 i l gl).(0) in
	  let g i _ (_,_,t) =
	    build_rec (var::env) polarity (lift i t) in
	    list_fold_left_i g (2-(List.length l)) () v
      | Forall(_,b)->
	  let var=mkMeta (metagen true) in
	    build_rec (var::env) polarity b
      | Atom t->
	  let unsigned=substnl env 0 t in
	    if not (isMeta unsigned) then (* discarding wildcard atoms *)
	      if polarity then
		positive:= unsigned :: !positive
	      else
		negative:= unsigned :: !negative in
    begin
      match side with
	  Concl    -> build_rec [] true cciterm
	| Hyp      -> build_rec [] false cciterm
	| Hint     ->
	    let rels,head=decompose_prod cciterm in
	    let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in
	      build_rec env false head;trivial:=false (* special for hints *)
    end;
    (!trivial,
     {positive= !positive;
      negative= !negative})

type right_pattern =
    Rarrow
  | Rand
  | Ror
  | Rfalse
  | Rforall
  | Rexists of metavariable*constr*bool

type left_arrow_pattern=
    LLatom
  | LLfalse of inductive*constr list
  | LLand of inductive*constr list
  | LLor of inductive*constr list
  | LLforall of constr
  | LLexists of inductive*constr list
  | LLarrow of constr*constr*constr

type left_pattern=
    Lfalse
  | Land of inductive
  | Lor of inductive
  | Lforall of metavariable*constr*bool
  | Lexists of inductive
  | LA of constr*left_arrow_pattern

type t={id:global_reference;
	constr:constr;
	pat:(left_pattern,right_pattern) sum;
	atoms:atoms}

let build_formula side nam typ gl metagen=
  let normalize = special_nf gl in
    try
      let m=meta_succ(metagen false) in
      let trivial,atoms=
	if !qflag then
	  build_atoms gl metagen side typ
	else no_atoms in
      let pattern=
	match side with
	    Concl ->
	      let pat=
		match kind_of_formula gl typ with
		    False(_,_)        -> Rfalse
		  | Atom a       -> raise (Is_atom a)
		  | And(_,_,_)        -> Rand
		  | Or(_,_,_)         -> Ror
		  | Exists (i,l) ->
		      let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in
			Rexists(m,d,trivial)
		  | Forall (_,a) -> Rforall
		  | Arrow (a,b) -> Rarrow in
		Right pat
	  | _ ->
	      let pat=
		match kind_of_formula gl typ with
		    False(i,_)        ->  Lfalse
		  | Atom a       ->  raise (Is_atom a)
		  | And(i,_,b)         ->
		      if b then
			let nftyp=normalize typ in raise (Is_atom nftyp)
		      else Land i
		  | Or(i,_,b)          ->
		      if b then
			let nftyp=normalize typ in raise (Is_atom nftyp)
		      else Lor i
		  | Exists (ind,_) ->  Lexists ind
		  | Forall (d,_) ->
		      Lforall(m,d,trivial)
		  | Arrow (a,b) ->
		      let nfa=normalize a in
			LA (nfa,
			    match kind_of_formula gl a with
				False(i,l)-> LLfalse(i,l)
			      | Atom t->     LLatom
			      | And(i,l,_)-> LLand(i,l)
			      | Or(i,l,_)->  LLor(i,l)
			      | Arrow(a,c)-> LLarrow(a,c,b)
			      | Exists(i,l)->LLexists(i,l)
			      | Forall(_,_)->LLforall a) in
		Left pat
      in
	Left {id=nam;
	      constr=normalize typ;
	      pat=pattern;
	      atoms=atoms}
    with Is_atom a-> Right a (* already in nf *)