matitaB/components/ng_paramodulation/nCicBlob.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
  13
  14 let default_eqP =
  15   let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
  16   let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
  17     NCic.Const ref
  18 ;;
  19
  20 let eqPref = ref default_eqP;;
  21 let set_eqP t = eqPref := t;;
  22
  23 let equivalence_relation =
  24   let uri = NUri.uri_of_string "cic:/matita/ng/properties/relations/eq_rel.con"
  25   in
  26   let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,2))
  27   in NCic.Const ref
  28
  29 let setoid_eq =
  30   let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
  31   let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2))
  32   in NCic.Const ref
  33
  34 let set_default_eqP() = eqPref := default_eqP
  35
  36 let saturate status metasenv subst context t ty =
  37   let sty, _, args =
  38     (* CSC: NCicPp.status is the best I can put here *)
  39     NCicMetaSubst.saturate status ~delta:0 metasenv subst context ty 0
  40   in
  41   let proof =
  42     if args = [] then t
  43     else NCic.Appl (t :: args)
  44   in
  45   proof, sty
  46 ;;
  47
  48
  49 module NCicBlob: Terms.Blob
  50 with type t = NCic.term and type input = NCic.term = struct
  51
  52   type t = NCic.term
  53
  54   let eq x y = x = y;;
  55     (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *)
  56
  57   let height_of_ref = function
  58     | NReference.Def h -> h
  59     | NReference.Fix(_,_,h) -> h
  60     | _ -> 0
  61
  62   let compare_refs (NReference.Ref (u1,r1)) (NReference.Ref (u2,r2)) =
  63     let x = height_of_ref r2 - height_of_ref r1 in
  64       if x = 0 then
  65         Hashtbl.hash (NUri.string_of_uri u1,r1) -
  66           Hashtbl.hash (NUri.string_of_uri u2,r2)
  67       else x
  68
  69   let rec compare x y =
  70     match x,y with
  71     | NCic.Rel i, NCic.Rel j -> j-i
  72     | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
  73     | NCic.Const r1, NCic.Const r2 -> compare_refs r1 r2
  74     (*NReference.compare r1 r2*)
  75     | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
  76     | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
  77     | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
  78     | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
  79     | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
  80     | NCic.Appl _, NCic.Meta _ -> ~-1
  81     | NCic.Meta _, NCic.Appl _ -> 1
  82     | _ -> Pervasives.compare x y
  83         (* was assert false, but why? *)
  84
  85   ;;
  86
  87   let rec alpha_norm k = function
  88     | NCic.Lambda (_,ty,t) ->
  89         NCic.Lambda("_",alpha_norm k ty,alpha_norm k t)
  90     | NCic.Prod (_,ty,t) ->
  91         NCic.Prod("_",alpha_norm k ty,alpha_norm k t)
  92     | NCic.LetIn (_,ty,t,b) ->
  93         NCic.LetIn("_",alpha_norm k ty,alpha_norm k t,alpha_norm k b)
  94     | NCic.Meta (_,(_,NCic.Irl _)) as t -> t
  95     | NCic.Meta (n,(s,NCic.Ctx tl)) as t ->
  96         let tl' = HExtlib.sharing_map (alpha_norm k) tl in
  97         if tl == tl' then t else NCic.Meta (n,(s,NCic.Ctx tl'))
  98     | t -> NCicUtils.map ~hbr:false (new NCicPp.status None)
  99         (fun _ _ -> ()) () alpha_norm t
 100
 101   (* let compare x y =
 102     (* CSC: NCicPp.status is the best I can put here *)
 103     (* WR: and I can't guess a user id, so I must put None *)
 104     if NCicReduction.alpha_eq (new NCicPp.status None) [] [] [] x y  then 0
 105     (* if x = y  then 0 *)
 106     else compare x y
 107   ;; *)
 108
 109   let eqP = fun () -> !eqPref
 110   ;;
 111
 112   let is_eq = function
 113     | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq (eqP()) eqt ->
 114         Some (ty,l,r)
 115     | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] ->
 116         None
 117 (*
 118     | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r]
 119         when eq equivalence_relation eqt && eq setoid_eq eqt2 ->
 120         Some (ty,l,r) *)
 121     | _ -> None
 122
 123   let pp t =
 124     (* CSC: NCicPp.status is the best I can put here *)
 125     (new NCicPp.status None)#ppterm ~context:[] ~metasenv:[] ~subst:[] t
 126
 127   type input = NCic.term
 128
 129   let rec embed = function
 130     | NCic.Meta (i,_) -> Terms.Var i, [i]
 131     | NCic.Appl l ->
 132         let rec aux acc l = function
 133           |[] -> acc@l
 134           |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
 135         in
 136         let res,vars = List.fold_left
 137           (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
 138         in (Terms.Node (List.rev res)), vars
 139     | t -> Terms.Leaf (alpha_norm () t), []
 140   ;;
 141
 142   let embed t = fst (embed t) ;;
 143
 144  end