X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.ml;h=851355e95eaf76e60f1e5609a6bd9730b23eca42;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=9db79254651bbdda49ecc464ad94332a14166100;hpb=3a996119583c255a34fa2f5274939f78f0d940bc;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 9db792546..851355e95 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -1,10 +1,33 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) (* identity_relocation_list_for_metavariable i canonical_context *) (* returns the identity relocation list, which is the list [1 ; ... ; n] *) (* where n = List.length [canonical_context] *) (*CSC: ma mi basta la lunghezza del contesto canonico!!!*) let identity_relocation_list_for_metavariable ?(start = 1) canonical_context = - let canonical_context_length = List.length canonical_context in let rec aux = function (_,[]) -> [] @@ -15,64 +38,87 @@ let identity_relocation_list_for_metavariable ?(start = 1) canonical_context = (* Returns the first meta whose number is above the *) (* number of the higher meta. *) -let new_meta metasenv = +let new_meta metasenv subst = let rec aux = function - None,[] -> 1 - | Some n,[] -> n - | None,(n,_,_)::tl -> aux (Some n,tl) - | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) + None, [] -> 1 + | Some n, [] -> n + | None, n::tl -> aux (Some n,tl) + | Some m, n::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) in - 1 + aux (None,metasenv) + let indexes = + (List.map (fun (i, _, _) -> i) metasenv) @ (List.map fst subst) + in + 1 + aux (None, indexes) + +(* let apply_subst_context = CicMetaSubst.apply_subst_context;; *) +(* questa o la precedente sembrano essere equivalenti come tempi *) +let apply_subst_context _ context = context ;; -let mk_implicit metasenv context = - let newmeta = new_meta metasenv in +let mk_implicit metasenv subst context = + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in let irl = identity_relocation_list_for_metavariable context in - ([ newmeta, context, Cic.Sort Cic.Type ; - newmeta + 1, context, Cic.Meta (newmeta, irl); + (* in the following mk_* functions we apply substitution to canonical + * context since we have the invariant that the metasenv has already been + * instantiated with subst *) + let context = apply_subst_context subst context in + ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ; + (* TASSI: ?? *) + newmeta + 1, context, Cic.Meta (newmeta, []); newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv, newmeta + 2) -let n_fresh_metas metasenv context n = +let mk_implicit_type metasenv subst context = + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in + let context = apply_subst_context subst context in + ([ newmeta, [], Cic.Sort (Cic.Type newuniv); + (* TASSI: ?? *) + newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv, + newmeta + 1) + +let mk_implicit_sort metasenv subst = + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in + ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta) + (* TASSI: ?? *) + +let n_fresh_metas metasenv subst context n = if n = 0 then metasenv, [] else let irl = identity_relocation_list_for_metavariable context in - let newmeta = new_meta metasenv in + let context = apply_subst_context subst context in + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in let rec aux newmeta n = if n = 0 then metasenv, [] else let metasenv', l = aux (newmeta + 3) (n-1) in - (newmeta, context, Cic.Sort Cic.Type):: + (* TASSI: ?? *) + (newmeta, context, Cic.Sort (Cic.Type newuniv)):: (newmeta + 1, context, Cic.Meta (newmeta, irl)):: (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', Cic.Meta(newmeta+2,irl)::l in aux newmeta n -let fresh_subst metasenv context uris = +let fresh_subst metasenv subst context uris = let irl = identity_relocation_list_for_metavariable context in - let newmeta = new_meta metasenv in + let context = apply_subst_context subst context in + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in let rec aux newmeta = function [] -> metasenv, [] | uri::tl -> let metasenv', l = aux (newmeta + 3) tl in - (newmeta, context, Cic.Sort Cic.Type):: + (* TASSI: ?? *) + (newmeta, context, Cic.Sort (Cic.Type newuniv)):: (newmeta + 1, context, Cic.Meta (newmeta, irl)):: (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', (uri,Cic.Meta(newmeta+2,irl))::l in aux newmeta uris -let mk_implicit' metasenv context = - let (metasenv, index) = mk_implicit metasenv context in - (metasenv, index - 1, index) - -let mk_implicit_type metasenv context = - let newmeta = new_meta metasenv in - let irl = identity_relocation_list_for_metavariable context in - ([ newmeta, context, Cic.Sort Cic.Type ; - newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv, - newmeta + 1) - -let expand_implicits metasenv context term = +let expand_implicits metasenv subst context term = let rec aux metasenv context = function | (Cic.Rel _) as t -> metasenv, t | (Cic.Sort _) as t -> metasenv, t @@ -91,10 +137,18 @@ let expand_implicits metasenv context term = | Cic.Meta (n,l) -> let metasenv', l' = do_local_context metasenv context l in metasenv', Cic.Meta (n, l') - | Cic.Implicit -> - let (metasenv', type_index, _) = mk_implicit' metasenv context in + | Cic.Implicit (Some `Type) -> + let (metasenv', idx) = mk_implicit_type metasenv subst context in + let irl = identity_relocation_list_for_metavariable context in + metasenv', Cic.Meta (idx, irl) + | Cic.Implicit (Some `Closed) -> + let (metasenv', idx) = mk_implicit metasenv subst [] in + metasenv', Cic.Meta (idx, []) + | Cic.Implicit None -> + let (metasenv', idx) = mk_implicit metasenv subst context in let irl = identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (type_index, irl) + metasenv', Cic.Meta (idx, irl) + | Cic.Implicit _ -> assert false | Cic.Cast (te, ty) -> let metasenv', ty' = aux metasenv context ty in let metasenv'', te' = aux metasenv' context te in