From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Feb 2004 14:27:47 +0000 (+0000)
Subject: Code riorganization.
X-Git-Tag: V_0_2_3~16
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=34dfcf625e3ee6fac4ad4f7199055dee4edc5abb;p=helm.git

Code riorganization.
---

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 41802530b..bd6eca4a5 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -8,11 +8,242 @@ let debug_print = prerr_endline
 
 type substitution = (int * Cic.term) list
 
+(*** Functions to apply a substitution ***)
+
+let apply_subst_gen ~appl_fun subst term =
+ let rec um_aux =
+  let module C = Cic in
+  let module S = CicSubstitution in 
+   function
+      C.Rel _ as t -> t
+    | C.Var _  as t -> t
+    | C.Meta (i, l) -> 
+        (try
+          let t = List.assoc i subst in
+          um_aux (S.lift_meta l t)
+        with Not_found -> (* not constrained variable, i.e. free in subst*)
+          let l' =
+            List.map (function None -> None | Some t -> Some (um_aux t)) l
+          in
+           C.Meta (i,l'))
+    | C.Sort _ as t -> t
+    | C.Implicit -> assert false
+    | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
+    | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
+    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
+    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+    | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
+    | C.Appl _ -> assert false
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+       in
+       C.Const (uri, exp_named_subst')
+    | C.MutInd (uri,typeno,exp_named_subst) ->
+       let exp_named_subst' =
+         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+       in
+       C.MutInd (uri,typeno,exp_named_subst')
+    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+       let exp_named_subst' =
+         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+       in
+       C.MutConstruct (uri,typeno,consno,exp_named_subst')
+    | C.MutCase (sp,i,outty,t,pl) ->
+       let pl' = List.map um_aux pl in
+       C.MutCase (sp, i, um_aux outty, um_aux t, pl')
+    | C.Fix (i, fl) ->
+       let fl' =
+         List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
+       in
+       C.Fix (i, fl')
+    | C.CoFix (i, fl) ->
+       let fl' =
+         List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
+       in
+       C.CoFix (i, fl')
+ in
+ um_aux term
+;;
+
+let apply_subst =
+  let appl_fun um_aux he tl =
+    let tl' = List.map um_aux tl in
+      begin
+       match um_aux he with
+          Cic.Appl l -> Cic.Appl (l@tl')
+        | he' -> Cic.Appl (he'::tl')
+      end
+  in
+  apply_subst_gen ~appl_fun
+;;
+
+(* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
+(* performs as (apply_subst subst t) until it finds an application of   *)
+(* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
+(* a new beta-redex; in this case up to [reductions_no] consecutive     *)
+(* beta-reductions are performed.                                       *)
+(* Hint: this function is usually called when [reductions_no]           *)
+(*  eta-expansions have been performed and the head of the new          *)
+(*  application has been unified with (META [meta_to_reduce]):          *)
+(*  during the unwinding the eta-expansions are undone.                 *)
+
+let apply_subst_reducing meta_to_reduce =
+  let appl_fun um_aux he tl =
+    let tl' = List.map um_aux tl in
+    let t' =
+     match um_aux he with
+        Cic.Appl l -> Cic.Appl (l@tl')
+      | he' -> Cic.Appl (he'::tl')
+    in
+     begin
+      match meta_to_reduce, he with
+         Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr ->
+          let rec beta_reduce =
+           function
+              (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
+                let he'' = CicSubstitution.subst he' t in
+                 if tl' = [] then
+                  he''
+                 else
+                  beta_reduce (n-1,Cic.Appl(he''::tl'))
+            | (_,t) -> t
+          in
+           beta_reduce (reductions_no,t')
+       | _,_ -> t'
+     end
+  in
+  apply_subst_gen ~appl_fun
+
+let rec apply_subst_context subst context =
+  List.fold_right
+    (fun item context ->
+      match item with
+      | Some (n, Cic.Decl t) ->
+          let t' = apply_subst subst t in
+          Some (n, Cic.Decl t') :: context
+      | Some (n, Cic.Def (t, ty)) ->
+          let ty' =
+            match ty with
+            | None -> None
+            | Some ty -> Some (apply_subst subst ty)
+          in
+          let t' = apply_subst subst t in
+          Some (n, Cic.Def (t', ty')) :: context
+      | None -> None :: context)
+    context []
+
+let apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, apply_subst_context subst context, apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+      metasenv)
+
+(***** Pretty printing functions ******)
+
 let ppsubst subst =
   String.concat "\n"
     (List.map
       (fun (idx, term) -> Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
       subst)
+;;
+
+let ppterm subst term = CicPp.ppterm (apply_subst subst term)
+
+let ppterm_in_context subst term name_context =
+ CicPp.pp (apply_subst subst term) name_context
+
+let ppcontext' ?(sep = "\n") subst context =
+ let separate s = if s = "" then "" else s ^ sep in
+  List.fold_right 
+   (fun context_entry (i,name_context) ->
+     match context_entry with
+        Some (n,Cic.Decl t) ->
+         sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
+          (ppterm_in_context subst t name_context), (Some n)::name_context
+      | Some (n,Cic.Def (bo,ty)) ->
+         sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
+          (match ty with
+              None -> "_"
+            | Some ty -> ppterm_in_context subst ty name_context)
+          (ppterm_in_context subst bo name_context), (Some n)::name_context
+       | None ->
+          sprintf "%s_ :? _" (separate i), None::name_context
+    ) context ("",[])
+
+let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
+
+let ppmetasenv ?(sep = "\n") metasenv subst =
+  String.concat sep
+    (List.map
+      (fun (i, c, t) ->
+        let context,name_context = ppcontext' ~sep:"; " subst c in
+         sprintf "%s |- ?%d: %s" context i
+          (ppterm_in_context subst t name_context))
+      (List.filter
+        (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+        metasenv))
+
+(* From now on we recreate a kernel abstraction where substitutions are part of
+ * the calculus *)
+
+let lift subst n term =
+  let term = apply_subst subst term in
+  try
+    CicSubstitution.lift n term
+  with e ->
+    raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
+
+let subst subst t1 t2 =
+  let t1 = apply_subst subst t1 in
+  let t2 = apply_subst subst t2 in
+  try
+    CicSubstitution.subst t1 t2
+  with e ->
+    raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
+
+let whd subst context term =
+  let term = apply_subst subst term in
+  let context = apply_subst_context subst context in
+  try
+    CicReduction.whd context term
+  with e ->
+    raise (MetaSubstFailure ("Weak head reduction failure: " ^
+      Printexc.to_string e))
+
+let are_convertible subst context t1 t2 =
+  let context = apply_subst_context subst context in
+  let t1 = apply_subst subst t1 in
+  let t2 = apply_subst subst t2 in
+  CicReduction.are_convertible context t1 t2
+
+let tempi_type_of_aux_subst = ref 0.0;;
+let tempi_type_of_aux = ref 0.0;;
+
+let type_of_aux' metasenv subst context term =
+let time1 = Unix.gettimeofday () in
+  let term = apply_subst subst term in
+  let context = apply_subst_context subst context in
+  let metasenv =
+    List.map
+      (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
+      (List.filter
+        (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+        metasenv)
+  in
+let time2 = Unix.gettimeofday () in
+let res =
+  try
+    CicTypeChecker.type_of_aux' metasenv context term
+  with CicTypeChecker.TypeCheckerFailure msg ->
+    raise (MetaSubstFailure ("Type checker failure: " ^ msg))
+in
+let time3 = Unix.gettimeofday () in
+ tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; 
+ tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; 
+ res
 
 (**** DELIFT ****)
 (* the delift function takes in input a metavariable index, an ordered list of
@@ -214,7 +445,7 @@ let rec restrict subst to_be_restricted metasenv =
               raise (MetaSubstFailure (sprintf
                 "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
                 n (names_of_context_indexes context to_be_restricted) n
-                (CicPp.ppterm s)))
+                (ppterm subst s)))
            with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
         with Occur ->
           raise (MetaSubstFailure (sprintf
@@ -275,7 +506,7 @@ let delift n subst context metasenv l t =
         if i = n then
           raise (MetaSubstFailure (sprintf
             "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
-            i (CicPp.ppterm t)))
+            i (ppterm subst t)))
         else
          (* I do not consider the term associated to ?i in subst since *)
          (* in this way I can restrict if something goes wrong.        *)
@@ -349,10 +580,10 @@ let delift n subst context metasenv l t =
 debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
       raise (MetaSubstFailure (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
-        (CicPp.ppterm t)
+        (ppterm subst t)
         (String.concat "; "
           (List.map
-            (function Some t -> CicPp.ppterm t | None -> "_")
+            (function Some t -> ppterm subst t | None -> "_")
             l))))
    in
    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
@@ -361,247 +592,6 @@ debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have
 
 (**** END OF DELIFT ****)
 
-let apply_subst_gen ~appl_fun subst term =
- let rec um_aux =
-  let module C = Cic in
-  let module S = CicSubstitution in 
-   function
-      C.Rel _ as t -> t
-    | C.Var _  as t -> t
-    | C.Meta (i, l) -> 
-        (try
-          let t = List.assoc i subst in
-          um_aux (S.lift_meta l t)
-        with Not_found -> (* not constrained variable, i.e. free in subst*)
-          let l' =
-            List.map (function None -> None | Some t -> Some (um_aux t)) l
-          in
-           C.Meta (i,l'))
-    | C.Sort _ as t -> t
-    | C.Implicit -> assert false
-    | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
-    | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
-    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
-    | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
-    | C.Appl _ -> assert false
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
-       in
-       C.Const (uri, exp_named_subst')
-    | C.MutInd (uri,typeno,exp_named_subst) ->
-       let exp_named_subst' =
-         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
-       in
-       C.MutInd (uri,typeno,exp_named_subst')
-    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-       let exp_named_subst' =
-         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
-       in
-       C.MutConstruct (uri,typeno,consno,exp_named_subst')
-    | C.MutCase (sp,i,outty,t,pl) ->
-       let pl' = List.map um_aux pl in
-       C.MutCase (sp, i, um_aux outty, um_aux t, pl')
-    | C.Fix (i, fl) ->
-       let fl' =
-         List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
-       in
-       C.Fix (i, fl')
-    | C.CoFix (i, fl) ->
-       let fl' =
-         List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
-       in
-       C.CoFix (i, fl')
- in
- um_aux term
-
-let apply_subst =
-  let appl_fun um_aux he tl =
-    let tl' = List.map um_aux tl in
-      begin
-       match um_aux he with
-          Cic.Appl l -> Cic.Appl (l@tl')
-        | he' -> Cic.Appl (he'::tl')
-      end
-  in
-  apply_subst_gen ~appl_fun
-
-let ppterm subst term = CicPp.ppterm (apply_subst subst term)
-
-(* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
-(* performs as (apply_subst subst t) until it finds an application of   *)
-(* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
-(* a new beta-redex; in this case up to [reductions_no] consecutive     *)
-(* beta-reductions are performed.                                       *)
-(* Hint: this function is usually called when [reductions_no]           *)
-(*  eta-expansions have been performed and the head of the new          *)
-(*  application has been unified with (META [meta_to_reduce]):          *)
-(*  during the unwinding the eta-expansions are undone.                 *)
-
-let apply_subst_reducing meta_to_reduce =
-  let appl_fun um_aux he tl =
-    let tl' = List.map um_aux tl in
-    let t' =
-     match um_aux he with
-        Cic.Appl l -> Cic.Appl (l@tl')
-      | he' -> Cic.Appl (he'::tl')
-    in
-     begin
-      match meta_to_reduce, he with
-         Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr ->
-          let rec beta_reduce =
-           function
-              (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
-                let he'' = CicSubstitution.subst he' t in
-                 if tl' = [] then
-                  he''
-                 else
-                  beta_reduce (n-1,Cic.Appl(he''::tl'))
-            | (_,t) -> t
-          in
-           beta_reduce (reductions_no,t')
-       | _,_ -> t'
-     end
-  in
-  apply_subst_gen ~appl_fun
-
-let rec apply_subst_context subst context =
-  List.fold_right
-    (fun item context ->
-      match item with
-      | Some (n, Cic.Decl t) ->
-          let t' = apply_subst subst t in
-          Some (n, Cic.Decl t') :: context
-      | Some (n, Cic.Def (t, ty)) ->
-          let ty' =
-            match ty with
-            | None -> None
-            | Some ty -> Some (apply_subst subst ty)
-          in
-          let t' = apply_subst subst t in
-          Some (n, Cic.Def (t', ty')) :: context
-      | None -> None :: context)
-    context []
-
-let apply_subst_metasenv subst metasenv =
-  List.map
-    (fun (n, context, ty) ->
-      (n, apply_subst_context subst context, apply_subst subst ty))
-    (List.filter
-      (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
-      metasenv)
-
-let ppterm subst term = CicPp.ppterm (apply_subst subst term)
-
-let ppterm_in_context subst term name_context =
- CicPp.pp (apply_subst subst term) name_context
-
-let ppcontext' ?(sep = "\n") subst context =
- let separate s = if s = "" then "" else s ^ sep in
-  List.fold_right 
-   (fun context_entry (i,name_context) ->
-     match context_entry with
-        Some (n,Cic.Decl t) ->
-         sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_context subst t name_context), (Some n)::name_context
-      | Some (n,Cic.Def (bo,ty)) ->
-         sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
-          (match ty with
-              None -> "_"
-            | Some ty -> ppterm_in_context subst ty name_context)
-          (ppterm_in_context subst bo name_context), (Some n)::name_context
-       | None ->
-          sprintf "%s_ :? _" (separate i), None::name_context
-    ) context ("",[])
-
-let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
-
-let ppmetasenv ?(sep = "\n") metasenv subst =
-  String.concat sep
-    (List.map
-      (fun (i, c, t) ->
-        let context,name_context = ppcontext' ~sep:"; " subst c in
-         sprintf "%s |- ?%d: %s" context i
-          (ppterm_in_context subst t name_context))
-      (List.filter
-        (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
-        metasenv))
-
-(* UNWIND THE MGU INSIDE THE MGU *)
-(*
-let unwind_subst metasenv subst =
-  List.fold_left
-   (fun (unwinded,metasenv) (i,_) ->
-     let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
-     let identity_relocation_list =
-      CicMkImplicit.identity_relocation_list_for_metavariable canonical_context
-     in
-      let (_,metasenv',subst') =
-       unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
-      in
-       subst',metasenv'
-   ) ([],metasenv) subst
-*)
-
-(* From now on we recreate a kernel abstraction where substitutions are part of
- * the calculus *)
-
-let lift subst n term =
-  let term = apply_subst subst term in
-  try
-    CicSubstitution.lift n term
-  with e ->
-    raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
-
-let subst subst t1 t2 =
-  let t1 = apply_subst subst t1 in
-  let t2 = apply_subst subst t2 in
-  try
-    CicSubstitution.subst t1 t2
-  with e ->
-    raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
-
-let whd subst context term =
-  let term = apply_subst subst term in
-  let context = apply_subst_context subst context in
-  try
-    CicReduction.whd context term
-  with e ->
-    raise (MetaSubstFailure ("Weak head reduction failure: " ^
-      Printexc.to_string e))
-
-let are_convertible subst context t1 t2 =
-  let context = apply_subst_context subst context in
-  let t1 = apply_subst subst t1 in
-  let t2 = apply_subst subst t2 in
-  CicReduction.are_convertible context t1 t2
-
-let tempi_type_of_aux_subst = ref 0.0;;
-let tempi_type_of_aux = ref 0.0;;
-
-let type_of_aux' metasenv subst context term =
-let time1 = Unix.gettimeofday () in
-  let term = apply_subst subst term in
-  let context = apply_subst_context subst context in
-  let metasenv =
-    List.map
-      (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
-      (List.filter
-        (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
-        metasenv)
-  in
-let time2 = Unix.gettimeofday () in
-let res =
-  try
-    CicTypeChecker.type_of_aux' metasenv context term
-  with CicTypeChecker.TypeCheckerFailure msg ->
-    raise (MetaSubstFailure ("Type checker failure: " ^ msg))
-in
-let time3 = Unix.gettimeofday () in
- tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; 
- tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; 
- res
 
 (** {2 Format-like pretty printers} *)
 
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index 60228fe08..6034853da 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -30,11 +30,6 @@ exception MetaSubstFailure of string
 (* (META i) have been instantiated with t.      *)
 type substitution = (int * Cic.term) list
 
-val delift : 
-  int -> substitution -> Cic.context -> Cic.metasenv ->
-  (Cic.term option) list -> Cic.term ->
-    Cic.term * Cic.metasenv * substitution
-
 (* apply_subst subst t                     *)
 (* applies the substitution [subst] to [t] *)
 (* [subst] must be already unwinded        *)
@@ -65,16 +60,6 @@ val ppterm_in_context:
  substitution -> Cic.term -> (Cic.name option) list -> string
 val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string
 
-(** {2 Format-like pretty printers}
- * As above with prototypes suitable for toplevel/ocamldebug printers. No
- * subsitutions are applied here since such printers are required to be invoked
- * with only one argument.
- *)
-
-val fppsubst: Format.formatter -> substitution -> unit
-val fppterm: Format.formatter -> Cic.term -> unit
-val fppmetasenv: Format.formatter -> Cic.metasenv -> unit
-
 (* {2 Kernel wrappers}
  * From now on we recreate a kernel abstraction where substitutions are part of
  * the calculus *)
@@ -87,3 +72,22 @@ val are_convertible: substitution -> Cic.context -> Cic.term -> Cic.term -> bool
 val type_of_aux':
   Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
 
+val tempi_type_of_aux : float ref
+val tempi_type_of_aux_subst : float ref
+
+(*** delifting ***)
+
+val delift : 
+  int -> substitution -> Cic.context -> Cic.metasenv ->
+  (Cic.term option) list -> Cic.term ->
+    Cic.term * Cic.metasenv * substitution
+
+(** {2 Format-like pretty printers}
+ * As above with prototypes suitable for toplevel/ocamldebug printers. No
+ * subsitutions are applied here since such printers are required to be invoked
+ * with only one argument.
+ *)
+
+val fppsubst: Format.formatter -> substitution -> unit
+val fppterm: Format.formatter -> Cic.term -> unit
+val fppmetasenv: Format.formatter -> Cic.metasenv -> unit