X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;fp=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=0000000000000000000000000000000000000000;hp=e5e8469824226e37c5a2c013345f5e8d17c7d879;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
deleted file mode 100644
index e5e846982..000000000
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ /dev/null
@@ -1,365 +0,0 @@
-(* Copyright (C) 2000, 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/.
- *)
-
-exception Impossible of int;;
-exception NotRefinable of string;;
-exception Uncertain of string;;
-exception WrongUriToConstant of string;;
-exception WrongUriToVariable of string;;
-exception WrongUriToMutualInductiveDefinitions of string;;
-exception RelToHiddenHypothesis;;
-exception MetasenvInconsistency;;
-exception MutCaseFixAndCofixRefineNotImplemented;;
-exception FreeMetaFound of int;;
-
-let fdebug = ref 0;;
-let debug t context =
- let rec debug_aux t i =
-  let module C = Cic in
-  let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
- in
-  if !fdebug = 0 then
-   raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
-   (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
-;;
-
-let rec type_of_constant uri =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
-  match CicEnvironment.get_cooked_obj uri with
-     C.Constant (_,_,ty,_) -> ty
-   | C.CurrentProof (_,_,_,ty,_) -> ty
-   | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
-
-and type_of_variable uri =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
-  match CicEnvironment.get_cooked_obj uri with
-     C.Variable (_,_,ty,_) -> ty
-   |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
-
-and type_of_mutual_inductive_defs uri i =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
-  match CicEnvironment.get_cooked_obj uri with
-     C.InductiveDefinition (dl,_,_) ->
-      let (_,_,arity,_) = List.nth dl i in
-       arity
-   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
-
-and type_of_mutual_inductive_constr uri i j =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
-  match CicEnvironment.get_cooked_obj uri with
-      C.InductiveDefinition (dl,_,_) ->
-       let (_,_,_,cl) = List.nth dl i in
-        let (_,ty) = List.nth cl (j-1) in
-         ty
-   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
-
-(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-and type_of_aux' metasenv context t =
- let rec type_of_aux subst metasenv context =
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module U = UriManager in
-  let module Un = CicUnification in
-   function
-      C.Rel n ->
-       (try
-         match List.nth context (n - 1) with
-            Some (_,C.Decl t) -> S.lift n t,subst,metasenv
-          | Some (_,C.Def bo) ->
-             type_of_aux subst metasenv context (S.lift n bo)
-	  | None -> raise RelToHiddenHypothesis
-        with
-         _ -> raise (NotRefinable "Not a close term")
-       )
-    | C.Var (uri,exp_named_subst) ->
-      incr fdebug ;
-      let subst',metasenv' =
-       check_exp_named_subst subst metasenv context exp_named_subst in
-      let ty =
-       CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
-      in
-       decr fdebug ;
-       ty,subst',metasenv'
-    | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) =
-        try
-         List.find (function (m,_,_) -> n = m) metasenv
-        with
-         Not_found -> raise (FreeMetaFound n)
-       in
-        let subst',metasenv' =
-         check_metasenv_consistency subst metasenv context canonical_context l
-        in
-         CicSubstitution.lift_meta l ty, subst', metasenv'
-    | C.Sort s ->
-       C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
-        subst,metasenv
-    | C.Implicit -> raise (Impossible 21)
-    | C.Cast (te,ty) ->
-       let _,subst',metasenv' =
-        type_of_aux subst metasenv context ty in
-       let inferredty,subst'',metasenv'' =
-        type_of_aux subst' metasenv' context ty
-       in
-        (try
-          let subst''',metasenv''' =
-           Un.fo_unif_subst subst'' context metasenv'' inferredty ty
-          in
-           ty,subst''',metasenv'''
-         with
-          _ -> raise (NotRefinable "Cast"))
-    | C.Prod (name,s,t) ->
-       let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
-       let sort2,subst'',metasenv'' =
-        type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
-       in
-        sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
-   | C.Lambda (n,s,t) ->
-       let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
-       let type2,subst'',metasenv'' =
-        type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
-       in
-        let sort2,subst''',metasenv''' =
-         type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
-        in
-         (* only to check if the product is well-typed *)
-         let _,subst'''',metasenv'''' =
-          sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
-         in
-          C.Prod (n,s,type2),subst'''',metasenv''''
-   | C.LetIn (n,s,t) ->
-      (* only to check if s is well-typed *)
-      let _,subst',metasenv' = type_of_aux subst metasenv context s in
-      let inferredty,subst'',metasenv'' =
-       type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
-      in
-       (* One-step LetIn reduction. Even faster than the previous solution.
-          Moreover the inferred type is closer to the expected one. *)
-       CicSubstitution.subst s inferredty,subst',metasenv'
-   | C.Appl (he::tl) when List.length tl > 0 ->
-      let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
-      let tlbody_and_type,subst'',metasenv'' =
-       List.fold_right
-        (fun x (res,subst,metasenv) ->
-          let ty,subst',metasenv' =
-           type_of_aux subst metasenv context x
-          in
-           (x, ty)::res,subst',metasenv'
-        ) tl ([],subst',metasenv')
-      in
-       eat_prods subst'' metasenv'' context hetype tlbody_and_type
-   | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
-   | C.Const (uri,exp_named_subst) ->
-      incr fdebug ;
-      let subst',metasenv' =
-       check_exp_named_subst subst metasenv context exp_named_subst in
-      let cty =
-       CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
-      in
-       decr fdebug ;
-       cty,subst',metasenv'
-   | C.MutInd (uri,i,exp_named_subst) ->
-      incr fdebug ;
-      let subst',metasenv' =
-       check_exp_named_subst subst metasenv context exp_named_subst in
-      let cty =
-       CicSubstitution.subst_vars exp_named_subst
-        (type_of_mutual_inductive_defs uri i)
-      in
-       decr fdebug ;
-       cty,subst',metasenv'
-   | C.MutConstruct (uri,i,j,exp_named_subst) ->
-      let subst',metasenv' =
-       check_exp_named_subst subst metasenv context exp_named_subst in
-      let cty =
-       CicSubstitution.subst_vars exp_named_subst
-        (type_of_mutual_inductive_constr uri i j)
-      in
-       cty,subst',metasenv'
-   | C.MutCase _
-   | C.Fix _
-   | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
-
- (* check_metasenv_consistency checks that the "canonical" context of a
- metavariable is consitent - up to relocation via the relocation list l -
- with the actual context *)
- and check_metasenv_consistency subst metasenv context canonical_context l =
-   let module C = Cic in
-   let module R = CicReduction in
-   let module S = CicSubstitution in
-    let lifted_canonical_context = 
-     let rec aux i =
-      function
-         [] -> []
-       | (Some (n,C.Decl t))::tl ->
-          (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
-       | (Some (n,C.Def t))::tl ->
-          (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
-       | None::tl -> None::(aux (i+1) tl)
-     in
-      aux 1 canonical_context
-    in
-     List.fold_left2 
-      (fun (subst,metasenv) t ct -> 
-        match (t,ct) with
-           _,None -> subst,metasenv
-         | Some t,Some (_,C.Def ct) ->
-            (try
-              CicUnification.fo_unif_subst subst context metasenv t ct
-             with _ -> raise MetasenvInconsistency)
-         | Some t,Some (_,C.Decl ct) ->
-            let inferredty,subst',metasenv' =
-             type_of_aux subst metasenv context t
-            in
-             (try
-               CicUnification.fo_unif_subst subst context metasenv inferredty ct
-             with _ -> raise MetasenvInconsistency)
-         | _, _  -> raise MetasenvInconsistency
-      ) (subst,metasenv) l lifted_canonical_context 
-
- and check_exp_named_subst metasubst metasenv context =
-  let rec check_exp_named_subst_aux metasubst metasenv substs =
-   function
-      [] -> metasubst,metasenv
-    | ((uri,t) as subst)::tl ->
-       let typeofvar =
-        CicSubstitution.subst_vars substs (type_of_variable uri) in
-       (match CicEnvironment.get_cooked_obj ~trust:false uri with
-           Cic.Variable (_,Some bo,_,_) ->
-            raise
-             (NotRefinable
-               "A variable with a body can not be explicit substituted")
-         | Cic.Variable (_,None,_,_) -> ()
-         | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
-       ) ;
-       let typeoft,metasubst',metasenv' =
-        type_of_aux metasubst metasenv context t
-       in
-        try
-         let metasubst'',metasenv'' =
-          CicUnification.fo_unif_subst
-           metasubst' context metasenv' typeoft typeofvar
-         in
-          check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
-        with _ ->
-         raise (NotRefinable "Wrong Explicit Named Substitution")
-  in
-   check_exp_named_subst_aux metasubst metasenv []
-
- and sort_of_prod subst metasenv context (name,s) (t1, t2) =
-  let module C = Cic in
-   (* ti could be a metavariable in the domain of the substitution *)
-   let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
-   let t1' = CicUnification.apply_subst subst' t1 in
-   let t2' = CicUnification.apply_subst subst' t2 in
-    let t1'' = CicReduction.whd context t1' in
-    let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
-    match (t1'', t2'') with
-       (C.Sort s1, C.Sort s2)
-         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
-          C.Sort s2,subst',metasenv'
-     | (C.Sort s1, C.Sort s2) ->
-         (*CSC manca la gestione degli universi!!! *)
-         C.Sort C.Type,subst',metasenv'
-     | (C.Meta _,_)
-     | (_,C.Meta _) ->
-       raise
-        (Uncertain
-          ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
-           CicPp.ppterm t2''))
-     | (_,_) ->
-       raise
-        (NotRefinable
-         ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
-
- and eat_prods subst metasenv context hetype =
-  function
-     [] -> hetype,subst,metasenv
-   | (hete, hety)::tl ->
-    (match (CicReduction.whd context hetype) with
-        Cic.Prod (n,s,t) ->
-         let subst',metasenv' =
-          try
-           CicUnification.fo_unif_subst subst context metasenv s hety
-          with _ ->
-           raise (NotRefinable "Appl: wrong parameter-type")
-         in
-          CicReduction.fdebug := -1 ;
-          eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
-      | Cic.Meta _ as t ->
-         raise
-          (Uncertain
-            ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
-      | _ -> raise (NotRefinable "Appl: wrong Prod-type")
-    )
- in
-  let ty,subst',metasenv' =
-   type_of_aux [] metasenv context t
-  in
-   let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
-   (* we get rid of the metavariables that have been instantiated *)
-   let metasenv''' =
-    List.filter
-     (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
-     metasenv''
-   in
-    CicUnification.apply_subst subst'' t,
-     CicUnification.apply_subst subst'' ty,
-     subst'', metasenv'''
-;;
-
-(* DEBUGGING ONLY *)
-let type_of_aux' metasenv context term =
- try
-  let (t,ty,s,m) =
-   type_of_aux' metasenv context term
-  in
-   List.iter
-    (function (i,t) ->
-      prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
-   List.iter
-    (function (i,_,t) ->
-      prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
-   prerr_endline
-    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
-   (t,ty,s,m)
- with
-  e ->
-   List.iter
-    (function (i,_,t) ->
-      prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
-    metasenv ;
-   prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
-   raise e
-;;