X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.ml;fp=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.ml;h=0000000000000000000000000000000000000000;hp=41f0589453e7521bcdd091c67e5968e28f482c76;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
deleted file mode 100644
index 41f058945..000000000
--- a/helm/ocaml/cic_unification/cicMkImplicit.ml
+++ /dev/null
@@ -1,266 +0,0 @@
-(* 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
-      (_,[]) -> []
-    | (n,None::tl) -> None::(aux ((n+1),tl))
-    | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
-  in
-   aux (start,canonical_context)
-
-(* Returns the first meta whose number is above the *)
-(* number of the higher meta.                       *)
-let new_meta metasenv =
-  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)
-  in
-   1 + aux (None,metasenv)
-
-let mk_implicit metasenv context =
-  let newmeta = new_meta metasenv in
-  let newuniv = CicUniv.fresh () in
-  let irl = identity_relocation_list_for_metavariable 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 mk_implicit_type metasenv context =
-  let newmeta = new_meta metasenv in
-  let newuniv = CicUniv.fresh () in
-  ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
-    (* TASSI: ?? *)
-    newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
-   newmeta + 1)
-
-let mk_implicit_sort metasenv =
-  let newmeta = new_meta metasenv in
-  let newuniv = CicUniv.fresh () in
-  ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta)
-  (* TASSI: ?? *)
-
-let n_fresh_metas metasenv context n = 
-  if n = 0 then metasenv, []
-  else 
-    let irl = identity_relocation_list_for_metavariable context in
-    let newmeta = new_meta metasenv 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 
-	(* 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 irl = identity_relocation_list_for_metavariable context in
-  let newmeta = new_meta metasenv in
-  let newuniv = CicUniv.fresh () in
-  let rec aux newmeta = function
-      [] -> metasenv, [] 
-    | uri::tl ->
-       let metasenv', l = aux (newmeta + 3) tl in 
-         (* 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 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 (Some `Type) ->
-        let (metasenv', idx) = mk_implicit_type metasenv 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 [] in
-        metasenv', Cic.Meta (idx, [])
-    | Cic.Implicit None ->
-        let (metasenv', idx) = mk_implicit metasenv context in
-        let irl = identity_relocation_list_for_metavariable context in
-        metasenv', Cic.Meta (idx, 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
-        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
-