X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=306074ec983daf7b0adda12e594efb0bb5f7222a;hb=265cf771fbfe217b5f274b999fc3ad887683a09a;hp=f7c19073b015755c6be36edceffc8d708db4d82d;hpb=edf601b6b8eb5b28a5292d0660a3b54b5680e580;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index f7c19073b..306074ec9 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -49,14 +49,14 @@ let position n =
 let restrict to_be_restricted =
   let rec erase i n = 
     function
-	[] -> []
-      |	_::tl when List.mem (n,i) to_be_restricted ->
-	  None::(erase (i+1) n tl) 
+        [] -> []
+      |        _::tl when List.mem (n,i) to_be_restricted ->
+          None::(erase (i+1) n tl) 
       | he::tl -> he::(erase (i+1) n tl) in
   let rec aux =
     function 
-	[] -> []
-      |	(n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
+        [] -> []
+      |        (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
   aux
 ;;
 
@@ -72,13 +72,13 @@ let delift context metasenv l t =
           C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
                     (*CSC: deliftato la regola per il LetIn                 *)
          else
-	  (match List.nth context (m-k-1) with
-	    Some (_,C.Def t) -> deliftaux k (S.lift m t)
-	  | Some (_,C.Decl t) ->
+          (match List.nth context (m-k-1) with
+            Some (_,C.Def (t,_)) -> deliftaux k (S.lift m t)
+          | Some (_,C.Decl t) ->
              (* It may augment to_be_restricted *)
              ignore (deliftaux k (S.lift m t)) ;
              C.Rel ((position (m-k) l) + k)
-	  | None -> raise RelToHiddenHypothesis)
+          | None -> raise RelToHiddenHypothesis)
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
@@ -177,7 +177,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
                 (* First possibility:  restriction    *)
                 (* Second possibility: unification    *)
                 (* Third possibility:  convertibility *)
-	        R.are_convertible context t1' t2'
+                R.are_convertible context t1' t2'
          ) true ln lm
        in
         if ok then subst,metasenv else raise UnificationFailed
@@ -186,18 +186,18 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
    | (C.Meta (n,l), t)   
    | (t, C.Meta (n,l)) ->
        let subst',metasenv' =
-	try
-	 let oldt = (List.assoc n subst) in
-	 let lifted_oldt = S.lift_meta l oldt in
-	  fo_unif_subst subst context metasenv lifted_oldt t
-	with Not_found ->
-	 let t',metasenv' = delift context metasenv l t in
-	  (n, t')::subst, metasenv'
+        try
+         let oldt = (List.assoc n subst) in
+         let lifted_oldt = S.lift_meta l oldt in
+          fo_unif_subst subst context metasenv lifted_oldt t
+        with Not_found ->
+         let t',metasenv' = delift context metasenv l t in
+          (n, t')::subst, metasenv'
        in
-	let (_,_,meta_type) = 
-	 List.find (function (m,_,_) -> m=n) metasenv' in
-	let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
-	 fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+        let (_,_,meta_type) = 
+         List.find (function (m,_,_) -> m=n) metasenv' in
+        let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
+         fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
       if UriManager.eq uri1 uri2 then
@@ -259,7 +259,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
             in 
              fo_unif_l subst' metasenv' (l1,l2)
        in
-	fo_unif_l subst metasenv (lr1, lr2) 
+        fo_unif_l subst metasenv (lr1, lr2) 
    | (C.Const _, _) 
    | (_, C.Const _)
    | (C.MutInd  _, _) 
@@ -274,9 +274,9 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
        let subst', metasenv' = 
         fo_unif_subst subst context metasenv outt1 outt2 in
        let subst'',metasenv'' = 
-	fo_unif_subst subst' context metasenv' t1 t2 in
+        fo_unif_subst subst' context metasenv' t1 t2 in
        List.fold_left2 
-	(function (subst,metasenv) ->
+        (function (subst,metasenv) ->
           fo_unif_subst subst context metasenv
         ) (subst'',metasenv'') pl1 pl2 
    | (C.Fix _, _)
@@ -322,24 +322,24 @@ in canonical_context. *)
 let restrict canonical_context m k l =
   let rec erase i = 
     function
-	[] -> []
-      |	None::tl -> None::(erase (i+1) tl)
-      |	he::tl -> 
-	  let i' = (List.nth l (i-1)) in
-	  if i' <= k 
-	   then he::(erase (i+1) tl) (* local variable *) 
-	   else 
-	    let acc = 
-	      (try List.nth canonical_context (i'-k-1)
-	       with Failure _ -> None) in
-	    if acc = None 
-	     then None::(erase (i+1) tl)
-	     else he::(erase (i+1) tl) in
+        [] -> []
+      |        None::tl -> None::(erase (i+1) tl)
+      |        he::tl -> 
+          let i' = (List.nth l (i-1)) in
+          if i' <= k 
+           then he::(erase (i+1) tl) (* local variable *) 
+           else 
+            let acc = 
+              (try List.nth canonical_context (i'-k-1)
+               with Failure _ -> None) in
+            if acc = None 
+             then None::(erase (i+1) tl)
+             else he::(erase (i+1) tl) in
   let rec aux =
     function 
-	[] -> []
-      |	(n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
-      |	hd::tl -> hd::(aux tl)
+        [] -> []
+      |        (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
+      |        hd::tl -> hd::(aux tl)
   in
    aux
 ;;
@@ -378,39 +378,39 @@ CSCSCS
     | C.Sort _ -> metasenv
     | C.Implicit -> metasenv
     | C.Cast (te,ty) -> 
-	let metasenv' = aux metasenv k te in
-	aux metasenv' k ty
+        let metasenv' = aux metasenv k te in
+        aux metasenv' k ty
     | C.Prod (_,s,t) 
     | C.Lambda (_,s,t) 
     | C.LetIn (_,s,t) ->
-	let metasenv' = aux metasenv k s in
-	aux metasenv' (k+1) t
+        let metasenv' = aux metasenv k s in
+        aux metasenv' (k+1) t
     | C.Appl l ->
-	List.fold_left
-	  (function metasenv -> aux metasenv k) metasenv l
+        List.fold_left
+          (function metasenv -> aux metasenv k) metasenv l
     | C.Const _
     | C.MutInd _ 
     | C.MutConstruct _ -> metasenv
     | C.MutCase (_,_,_,outty,t,pl) ->
-	let metasenv' = aux metasenv k outty in
-	let metasenv'' = aux metasenv' k t in
-	List.fold_left
-	  (function metasenv -> aux metasenv k) metasenv'' pl
+        let metasenv' = aux metasenv k outty in
+        let metasenv'' = aux metasenv' k t in
+        List.fold_left
+          (function metasenv -> aux metasenv k) metasenv'' pl
     | C.Fix (i, fl) ->
        let len = List.length fl in
        List.fold_left
          (fun metasenv f ->
-	   let (_,_,ty,bo) = f in
-	   let metasenv' = aux metasenv k ty in
-	   aux metasenv' (k+len) bo
+           let (_,_,ty,bo) = f in
+           let metasenv' = aux metasenv k ty in
+           aux metasenv' (k+len) bo
          ) metasenv fl
     | C.CoFix (i, fl) ->
-	let len = List.length fl in
+        let len = List.length fl in
         List.fold_left
          (fun metasenv f ->
-	   let (_,ty,bo) = f in
-	   let metasenv' = aux metasenv k ty in
-	   aux metasenv' (k+len) bo
+           let (_,ty,bo) = f in
+           let metasenv' = aux metasenv k ty in
+           aux metasenv' (k+len) bo
          ) metasenv fl
   in aux metasenv 0
 ;;
@@ -427,18 +427,18 @@ let unwind metasenv subst unwinded t =
       C.Rel _ as t -> t,metasenv
     | C.Var _  as t -> t,metasenv
     | C.Meta (i,l) -> 
-	(try
+        (try
           S.lift_meta l (List.assoc i !unwinded), metasenv
          with Not_found ->
            if List.mem i !frozen then raise OccurCheck
            else
             let saved_frozen = !frozen in 
-	    frozen := i::!frozen ;
+            frozen := i::!frozen ;
             let res =
              try
-	      let t = List.assoc i subst in
+              let t = List.assoc i subst in
               let t',metasenv' = um_aux metasenv t in
-	      let _,metasenv'' =
+              let _,metasenv'' =
                let (_,canonical_context,_) = 
                 List.find (function (m,_,_) -> m=i) metasenv
                in
@@ -451,13 +451,13 @@ let unwind metasenv subst unwinded t =
                (* not constrained variable, i.e. free in subst*)
                let l',metasenv' =
                 List.fold_right
-	         (fun t (tl,metasenv) ->
+                 (fun t (tl,metasenv) ->
                    match t with
                       None -> None::tl,metasenv
                     | Some t -> 
-	               let t',metasenv' = um_aux metasenv t in
-	                (Some t')::tl, metasenv'
-	         ) l ([],metasenv)
+                       let t',metasenv' = um_aux metasenv t in
+                        (Some t')::tl, metasenv'
+                 ) l ([],metasenv)
                in
                 C.Meta (i,l'), metasenv'
             in
@@ -485,10 +485,10 @@ let unwind metasenv subst unwinded t =
     | C.Appl (he::tl) ->
        let tl',metasenv' =
         List.fold_right
-	 (fun t (tl,metasenv) ->
-	   let t',metasenv' = um_aux metasenv t in
-	    t'::tl, metasenv'
-	 ) tl ([],metasenv)
+         (fun t (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            t'::tl, metasenv'
+         ) tl ([],metasenv)
        in
         begin
          match um_aux metasenv' he with
@@ -499,28 +499,28 @@ let unwind metasenv subst unwinded t =
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst', metasenv' =
         List.fold_right
-	 (fun (uri,t) (tl,metasenv) ->
-	   let t',metasenv' = um_aux metasenv t in
-	    (uri,t')::tl, metasenv'
-	 ) exp_named_subst ([],metasenv)
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
        in
         C.Const (uri,exp_named_subst'),metasenv'
     | C.MutInd (uri,typeno,exp_named_subst) ->
        let exp_named_subst', metasenv' =
         List.fold_right
-	 (fun (uri,t) (tl,metasenv) ->
-	   let t',metasenv' = um_aux metasenv t in
-	    (uri,t')::tl, metasenv'
-	 ) exp_named_subst ([],metasenv)
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
        in
         C.MutInd (uri,typeno,exp_named_subst'),metasenv'
     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
        let exp_named_subst', metasenv' =
         List.fold_right
-	 (fun (uri,t) (tl,metasenv) ->
-	   let t',metasenv' = um_aux metasenv t in
-	    (uri,t')::tl, metasenv'
-	 ) exp_named_subst ([],metasenv)
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
        in
         C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
     | C.MutCase (sp,i,outty,t,pl) ->
@@ -528,10 +528,10 @@ let unwind metasenv subst unwinded t =
        let t',metasenv'' = um_aux metasenv' t in
        let pl',metasenv''' =
         List.fold_right
-	 (fun p (pl,metasenv) ->
-	   let p',metasenv' = um_aux metasenv p in
-	    p'::pl, metasenv'
-	 ) pl ([],metasenv'')
+         (fun p (pl,metasenv) ->
+           let p',metasenv' = um_aux metasenv p in
+            p'::pl, metasenv'
+         ) pl ([],metasenv'')
        in
         C.MutCase (sp, i, outty', t', pl'),metasenv'''
     | C.Fix (i, fl) ->
@@ -539,10 +539,10 @@ let unwind metasenv subst unwinded t =
        let liftedfl,metasenv' =
         List.fold_right
          (fun (name, i, ty, bo) (fl,metasenv) ->
-	   let ty',metasenv' = um_aux metasenv ty in
-	   let bo',metasenv'' = um_aux metasenv' bo in
-	    (name, i, ty', bo')::fl,metasenv''
-	 ) fl ([],metasenv)
+           let ty',metasenv' = um_aux metasenv ty in
+           let bo',metasenv'' = um_aux metasenv' bo in
+            (name, i, ty', bo')::fl,metasenv''
+         ) fl ([],metasenv)
        in
         C.Fix (i, liftedfl),metasenv'
     | C.CoFix (i, fl) ->
@@ -550,10 +550,10 @@ let unwind metasenv subst unwinded t =
        let liftedfl,metasenv' =
         List.fold_right
          (fun (name, ty, bo) (fl,metasenv) ->
-	   let ty',metasenv' = um_aux metasenv ty in
-	   let bo',metasenv'' = um_aux metasenv' bo in
-	    (name, ty', bo')::fl,metasenv''
-	 ) fl ([],metasenv)
+           let ty',metasenv' = um_aux metasenv ty in
+           let bo',metasenv'' = um_aux metasenv' bo in
+            (name, ty', bo')::fl,metasenv''
+         ) fl ([],metasenv)
        in
         C.CoFix (i, liftedfl),metasenv'
  in