summaryrefslogtreecommitdiff
path: root/plugins/firstorder/formula.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/formula.ml')
-rw-r--r--plugins/firstorder/formula.ml270
1 files changed, 270 insertions, 0 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
new file mode 100644
index 00000000..45365cb2
--- /dev/null
+++ b/plugins/firstorder/formula.ml
@@ -0,0 +1,270 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+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 *)
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 12:17:56 +0000