X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.ml;h=bc60a188d201ce11c13f6957d0e4c9ab882f9481;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=6944a4fc210dfe1a68d016dcf513e5f4d9a86d09;hpb=7ea34971b64c60e5440bf2cc42cee560f6a86abe;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 6944a4fc2..bc60a188d 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -1,227 +1,120 @@ +(* 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 canonical_context = - let canonical_context_length = List.length canonical_context in +let identity_relocation_list_for_metavariable ?(start = 1) canonical_context = let rec aux = function (_,[]) -> [] | (n,None::tl) -> None::(aux ((n+1),tl)) | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) in - aux (1,canonical_context) + aux (start,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 rec aux metasenv context = function - | (Cic.Rel _) as t -> metasenv, t - | (Cic.Sort _) as t -> metasenv, t - | Cic.Const (uri, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.Const (uri, subst') - | Cic.Var (uri, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.Var (uri, subst') - | Cic.MutInd (uri, i, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.MutInd (uri, i, subst') - | Cic.MutConstruct (uri, i, j, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.MutConstruct (uri, i, j, subst') - | 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 - let irl = identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (type_index, irl) - | Cic.Cast (te, ty) -> - let metasenv', ty' = aux metasenv context ty in - let metasenv'', te' = aux metasenv' context te in - metasenv'', Cic.Cast (te', ty') - | Cic.Prod (name, s, t) -> - let metasenv', s' = aux metasenv context s in - let metasenv'', t' = - aux metasenv' (Some (name, Cic.Decl s') :: context) t - in - metasenv'', Cic.Prod (name, s', t') - | Cic.Lambda (name, s, t) -> - let metasenv', s' = aux metasenv context s in - let metasenv'', t' = - aux metasenv' (Some (name, Cic.Decl s') :: context) t - in - metasenv'', Cic.Lambda (name, s', t') - | Cic.LetIn (name, s, t) -> - let metasenv', s' = aux metasenv context s in - let metasenv'', t' = - aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t - in - metasenv'', Cic.LetIn (name, s', t') - | Cic.Appl l when List.length l > 1 -> - let metasenv', l' = - List.fold_right - (fun term (metasenv, terms) -> - let new_metasenv, term = aux metasenv context term in - new_metasenv, term :: terms) - l (metasenv, []) - in - metasenv', Cic.Appl l' - | Cic.Appl _ -> assert false - | Cic.MutCase (uri, i, outtype, term, patterns) -> - let metasenv', l' = - List.fold_right - (fun term (metasenv, terms) -> - let new_metasenv, term = aux metasenv context term in - new_metasenv, term :: terms) - (outtype :: term :: patterns) (metasenv, []) - in - let outtype', term', patterns' = - match l' with - | outtype' :: term' :: patterns' -> outtype', term', patterns' - | _ -> assert false - in - metasenv', Cic.MutCase (uri, i, outtype', term', patterns') - | Cic.Fix (i, funs) -> - let metasenv', types = - List.fold_right - (fun (name, _, typ, _) (metasenv, types) -> - let new_metasenv, new_type = aux metasenv context typ in - (new_metasenv, (name, new_type) :: types)) - funs (metasenv, []) - in -List.iter (fun (_, t) -> assert (t <> Cic.Implicit)) types; - let context' = - (List.rev_map - (fun (name, t) -> Some (Cic.Name name, Cic.Decl t)) - types) - @ context - in - let metasenv'', bodies = - List.fold_right - (fun (_, _, _, body) (metasenv, bodies) -> - let new_metasenv, new_body = aux metasenv context' body in - (new_metasenv, new_body :: bodies)) - funs (metasenv', []) - in - let rec combine = function - | ((name, index, _, _) :: funs_tl), - ((_, typ) :: typ_tl), - (body :: body_tl) -> - (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl) - | [], [], [] -> [] - | _ -> assert false - in - let funs' = combine (funs, types, bodies) in - metasenv'', Cic.Fix (i, funs') - | Cic.CoFix (i, funs) -> - let metasenv', types = - List.fold_right - (fun (name, typ, _) (metasenv, types) -> - let new_metasenv, new_type = aux metasenv context typ in - (new_metasenv, (name, new_type) :: types)) - funs (metasenv, []) - in - let context' = - (List.rev_map - (fun (name, t) -> Some (Cic.Name name, Cic.Decl t)) - types) - @ context - in - let metasenv'', bodies = - List.fold_right - (fun (_, _, body) (metasenv, bodies) -> - let new_metasenv, new_body = aux metasenv context' body in - (new_metasenv, new_body :: bodies)) - funs (metasenv', []) - in - let rec combine = function - | ((name, _, _) :: funs_tl), - ((_, typ) :: typ_tl), - (body :: body_tl) -> - (name, typ, body) :: combine (funs_tl, typ_tl, body_tl) - | [], [], [] -> [] - | _ -> assert false - in - let funs' = combine (funs, types, bodies) in - metasenv'', Cic.CoFix (i, funs') - and do_subst metasenv context subst = - List.fold_right - (fun (uri, term) (metasenv, substs) -> - let metasenv', term' = aux metasenv context term in - (metasenv', (uri, term') :: substs)) - subst (metasenv, []) - and do_local_context metasenv context local_context = - List.fold_right - (fun term (metasenv, local_context) -> - let metasenv', term' = - match term with - | None -> metasenv, None - | Some term -> - let metasenv', term' = aux metasenv context term in - metasenv', Some term' - in - metasenv', term' :: local_context) - local_context (metasenv, []) - in - aux metasenv context term -