]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_unification/cicMkImplicit.ml
eta-contraction was made on the wrong term
[helm.git] / helm / software / components / cic_unification / cicMkImplicit.ml
1 (* Copyright (C) 2004, 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$ *)
27
28 (* identity_relocation_list_for_metavariable i canonical_context         *)
29 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
30 (* where n = List.length [canonical_context]                             *)
31 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
32 let identity_relocation_list_for_metavariable ?(start = 1) canonical_context =
33   let rec aux =
34    function
35       (_,[]) -> []
36     | (n,None::tl) -> None::(aux ((n+1),tl))
37     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
38   in
39    aux (start,canonical_context)
40
41 (* Returns the first meta whose number is above the *)
42 (* number of the higher meta.                       *)
43 let new_meta metasenv subst =
44   let rec aux =
45    function
46       None, [] -> 1
47     | Some n, [] -> n
48     | None, n::tl -> aux (Some n,tl)
49     | Some m, n::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
50   in
51   let indexes = 
52     (List.map (fun (i, _, _) -> i) metasenv) @ (List.map fst subst)
53   in
54   1 + aux (None, indexes)
55
56 (* let apply_subst_context = CicMetaSubst.apply_subst_context;; *)
57 (* questa o la precedente sembrano essere equivalenti come tempi *)
58 let apply_subst_context _ context = context ;;
59
60 let mk_implicit metasenv subst context =
61   let newmeta = new_meta metasenv subst in
62   let newuniv = CicUniv.fresh () in
63   let irl = identity_relocation_list_for_metavariable context in
64     (* in the following mk_* functions we apply substitution to canonical
65     * context since we have the invariant that the metasenv has already been
66     * instantiated with subst *)
67   let context = apply_subst_context subst context in
68   ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
69     (* TASSI: ?? *)
70     newmeta + 1, context, Cic.Meta (newmeta, []);
71     newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
72    newmeta + 2)
73
74 let mk_implicit_type metasenv subst context =
75   let newmeta = new_meta metasenv subst in
76   let newuniv = CicUniv.fresh () in
77   let context = apply_subst_context subst context in
78   ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
79     (* TASSI: ?? *)
80     newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
81    newmeta + 1)
82
83 let mk_implicit_sort metasenv subst =
84   let newmeta = new_meta metasenv subst in
85   let newuniv = CicUniv.fresh () in
86   ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta)
87   (* TASSI: ?? *)
88
89 let n_fresh_metas metasenv subst context n = 
90   if n = 0 then metasenv, []
91   else 
92     let irl = identity_relocation_list_for_metavariable context in
93     let context = apply_subst_context subst context in
94     let newmeta = new_meta metasenv subst in
95     let newuniv = CicUniv.fresh () in
96     let rec aux newmeta n = 
97       if n = 0 then metasenv, [] 
98       else
99         let metasenv', l = aux (newmeta + 3) (n-1) in 
100         (* TASSI: ?? *)
101         (newmeta, context, Cic.Sort (Cic.Type newuniv))::
102         (newmeta + 1, context, Cic.Meta (newmeta, irl))::
103         (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
104         Cic.Meta(newmeta+2,irl)::l in
105     aux newmeta n
106       
107 let fresh_subst metasenv subst context uris = 
108   let irl = identity_relocation_list_for_metavariable context in
109   let context = apply_subst_context subst context in
110   let newmeta = new_meta metasenv subst in
111   let newuniv = CicUniv.fresh () in
112   let rec aux newmeta = function
113       [] -> metasenv, [] 
114     | uri::tl ->
115        let metasenv', l = aux (newmeta + 3) tl in 
116          (* TASSI: ?? *)
117          (newmeta, context, Cic.Sort (Cic.Type newuniv))::
118          (newmeta + 1, context, Cic.Meta (newmeta, irl))::
119          (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
120           (uri,Cic.Meta(newmeta+2,irl))::l in
121     aux newmeta uris
122