path: root/contrib/first-order/formula.ml

(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \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

let qflag=ref true

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 nhyps mip = 
  let constr_types = mip.mind_nf_lc in 
  let hyp = nb_prod_after mip.mind_nparams in	
    Array.map hyp constr_types

let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind))

(* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
let ind_hyps nevar ind largs= 
  let (mib,mip) = Global.lookup_inductive ind in
  let n = mip.mind_nparams in
    (* assert (n=(List.length largs));*)
  let lp=Array.length mip.mind_consnames in
  let types= mip.mind_nf_lc in   
  let lp=Array.length types in     
  let myhyps i=
    let t1=Term.prod_applist types.(i) largs in
    let t2=snd (Sign.decompose_prod_n_assum nevar t1) in
      fst (Sign.decompose_prod_assum t2) in
    Array.init lp myhyps

let match_with_evaluable gl t=
  let env=pf_env gl in
  let hd=       
    match kind_of_term t with
	App (head,_) -> head
      | _ -> t in
    match kind_of_term hd with
	Const cst->
	  if Environ.evaluable_constant cst env 
	  then Some (EvalConstRef cst,t)
	  else None
      | _-> None

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 t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in 
  let cciterm=whd_betaiotazeta 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 has_realargs=(n>0) in
		    let (mib,mip) = Global.lookup_inductive ind in
		    let is_trivial=
		      let is_constant c =
			nb_prod c = mip.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
			(match Array.length mip.mind_consnames with
			     0->False(ind,l)
			   | 1->And(ind,l,is_trivial)
			   | _->Or(ind,l,is_trivial)) 
		| _ ->  
		    match match_with_sigma_type cciterm with
			Some (i,l)-> Exists((destInd i),l)
		      |_-> 
			 match match_with_evaluable gl cciterm with 
			     Some (ec,t)->	  
			       let nt=Tacred.unfoldn [[1],ec] 
					(pf_env gl)
					(Refiner.sig_sig gl) t in
				 kind_of_formula gl nt
			   | None ->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 "")

let build_atoms gl metagen side cciterm =
  let trivial =ref false
  and positive=ref []
  and negative=ref [] in
  let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t 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 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).(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
    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 t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t 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).(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 *)