From: Claudio Sacerdoti Coen 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