]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_unification/cicReplace.ml
unificatiom hints with premises
[helm.git] / helm / software / components / cic_unification / cicReplace.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id: cicRefine.ml 7618 2007-09-05 10:07:39Z sacerdot $ *)
27
28 exception WhatAndWithWhatDoNotHaveTheSameLength;;
29
30 module C = Cic
31 module S = CicSubstitution
32
33 let replace_lifting ~equality ~context ~what ~with_what ~where =
34   let find_image ctx what t =
35    let rec find_image_aux =
36     function
37        [],[] -> raise Not_found
38      | what::tl1,with_what::tl2 ->
39         if equality ctx what t then with_what else find_image_aux (tl1,tl2)
40      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
41    in
42     find_image_aux (what,with_what)
43   in
44   let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
45   let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
46   let rec substaux k ctx what t =
47    try
48     S.lift (k-1) (find_image ctx what t)
49    with Not_found ->
50     match t with
51       C.Rel n as t -> t
52     | C.Var (uri,exp_named_subst) ->
53        let exp_named_subst' =
54         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
55        in
56         C.Var (uri,exp_named_subst')
57     | C.Meta (i, l) -> 
58        let l' =
59         List.map
60          (function
61              None -> None
62            | Some t -> Some (substaux k ctx what t)
63          ) l
64        in
65         C.Meta(i,l')
66     | C.Sort _ as t -> t
67     | C.Implicit _ as t -> t
68     | C.Cast (te,ty) -> C.Cast (substaux k ctx what te, substaux k ctx what ty)
69     | C.Prod (n,s,t) ->
70        C.Prod
71         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
72     | C.Lambda (n,s,t) ->
73        C.Lambda
74         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
75     | C.LetIn (n,s,ty,t) ->
76        C.LetIn
77         (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
78     | C.Appl (he::tl) ->
79        (* Invariant: no Appl applied to another Appl *)
80        let tl' = List.map (substaux k ctx what) tl in
81         begin
82          match substaux k ctx what he with
83             C.Appl l -> C.Appl (l@tl')
84           | _ as he' -> C.Appl (he'::tl')
85         end
86     | C.Appl _ -> assert false
87     | C.Const (uri,exp_named_subst) ->
88        let exp_named_subst' =
89         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
90        in
91        C.Const (uri,exp_named_subst')
92     | C.MutInd (uri,i,exp_named_subst) ->
93        let exp_named_subst' =
94         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
95        in
96         C.MutInd (uri,i,exp_named_subst')
97     | C.MutConstruct (uri,i,j,exp_named_subst) ->
98        let exp_named_subst' =
99         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
100        in
101         C.MutConstruct (uri,i,j,exp_named_subst')
102     | C.MutCase (sp,i,outt,t,pl) ->
103        C.MutCase (sp,i,substaux k ctx what outt, substaux k ctx what t,
104         List.map (substaux k ctx what) pl)
105     | C.Fix (i,fl) ->
106        let len = List.length fl in
107        let substitutedfl =
108         List.map
109          (fun (name,i,ty,bo) -> (* WRONG CTX *)
110            (name, i, substaux k ctx what ty,
111              substaux (k+len) ctx (List.map (S.lift len) what) bo)
112          ) fl
113        in
114         C.Fix (i, substitutedfl)
115     | C.CoFix (i,fl) ->
116        let len = List.length fl in
117        let substitutedfl =
118         List.map
119          (fun (name,ty,bo) -> (* WRONG CTX *)
120            (name, substaux k ctx what ty,
121              substaux (k+len) ctx (List.map (S.lift len) what) bo)
122          ) fl
123        in
124         C.CoFix (i, substitutedfl)
125  in
126   substaux 1 context what where
127 ;;
128
129