Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: formula.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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 Hipattern
open Names
open Constr
open EConstr
open Vars
open Util
open Declarations
open Globnames

module RelDecl = Context.Rel.Declaration

let qflag=ref true

let red_flags=ref CClosure.betaiotazeta

let (=?) f g i1 i2 j1 j2=
  let c=f i1 i2 in
    if Int.equal 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 Int.equal 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 Constr.kind 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 env ind =
  let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in
  let constr_types = Inductiveops.arities_of_constructors env 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 env sigma nevar ind largs =
  let types= Inductiveops.arities_of_constructors env ind in
  let myhyps t =
    let t = EConstr.of_constr t in
    let nparam_decls = Context.Rel.length (fst (Global.lookup_inductive (fst ind))).mind_params_ctxt in
    let t1=Termops.prod_applist_assum sigma nparam_decls t largs in
    let t2=snd (decompose_prod_n_assum sigma nevar t1) in
      fst (decompose_prod_assum sigma t2) in
    Array.map myhyps types

let special_nf env sigma t =
  Reductionops.clos_norm_flags !red_flags env sigma t

let special_whd env sigma t =
  Reductionops.clos_whd_flags !red_flags env sigma t

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

let pop t = Vars.lift (-1) t

let kind_of_formula env sigma term =
  let normalize = special_nf env sigma in
  let cciterm = special_whd env sigma term in
    match match_with_imp_term sigma cciterm with
Some (a,b)-> Arrow (a, pop b)
      |_->
  match match_with_forall_term sigma cciterm with
      Some (_,a,b)-> Forall (a, b)
    |_->
       match match_with_nodep_ind sigma cciterm with
    Some (i,l,n)->
      let ind,u=EConstr.destInd sigma i in
      let u = EConstr.EInstance.kind sigma u in
      let (mib,mip) = Global.lookup_inductive ind in
      let nconstr=Array.length mip.mind_consnames in
        if Int.equal nconstr 0 then
   False((ind,u),l)
        else
   let has_realargs=(n>0) in
   let is_trivial=
                          let is_constant n = Int.equal n 0 in
                            Array.exists is_constant mip.mind_consnrealargs in
     if Inductiveops.mis_is_recursive (ind,mib,mip) ||
       (has_realargs && not is_trivial)
     then
       Atom cciterm
     else
       if Int.equal nconstr 1 then
         And((ind,u),l,is_trivial)
       else
         Or((ind,u),l,is_trivial)
  | _ ->
      match match_with_sigma_type sigma cciterm with
   Some (i,l)->
                          let (ind, u) = EConstr.destInd sigma i in
                          let u = EConstr.EInstance.kind sigma u in
                          Exists((ind, u), 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 env sigma metagen side cciterm =
  let trivial =ref false
  and positive=ref []
  and negative=ref [] in
  let normalize=special_nf env sigma in
  let rec build_rec subst polarity cciterm=
    match kind_of_formula env sigma cciterm with
False(_,_)->if not polarity then trivial:=true
      | Arrow (a,b)->
   build_rec subst (not polarity) a;
   build_rec subst polarity b
      | And(i,l,b) | Or(i,l,b)->
   if b then
     begin
       let unsigned=normalize (substnl subst 0 cciterm) in
  if polarity then
    positive:= unsigned :: !positive
  else
    negative:= unsigned :: !negative
     end;
   let v = ind_hyps env sigma 0 i l in
   let g i _ decl =
     build_rec subst polarity (lift i (RelDecl.get_type decl)) 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 env sigma 1 i l).(0) in
   let g i _ decl =
     build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in
     List.fold_left_i g (2-(List.length l)) () v
      | Forall(_,b)->
   let var=mkMeta (metagen true) in
     build_rec (var::subst) polarity b
      | Atom t->
   let unsigned=substnl subst 0 t in
     if not (isMeta sigma 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 sigma cciterm in
     let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in
       build_rec subst 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 pinductive*constr list
  | LLand of pinductive*constr list
  | LLor of pinductive*constr list
  | LLforall of constr
  | LLexists of pinductive*constr list
  | LLarrow of constr*constr*constr

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

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

let build_formula env sigma side nam typ metagen=
  let normalize = special_nf env sigma in
    try
      let m=meta_succ(metagen false) in
      let trivial,atoms=
if !qflag then
   build_atoms env sigma metagen side typ
else no_atoms in
      let pattern=
match side with
     Concl ->
       let pat=
  match kind_of_formula env sigma typ with
      False(_,_)        -> Rfalse
    | Atom a       -> raise (Is_atom a)
    | And(_,_,_)        -> Rand
    | Or(_,_,_)         -> Ror
    | Exists (i,l) ->
        let d = RelDecl.get_type (List.last (ind_hyps env sigma 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 env sigma 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 env sigma 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 *)

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.