+nCicMetaSubst.cmo: nCicMetaSubst.cmi
+nCicMetaSubst.cmx: nCicMetaSubst.cmi
+nCicUnification.cmo: nCicUnification.cmi
+nCicUnification.cmx: nCicUnification.cmi
nCicRefiner.cmo: nCicRefiner.cmi
nCicRefiner.cmx: nCicRefiner.cmi
+nCicMetaSubst.cmo: nCicMetaSubst.cmi
+nCicMetaSubst.cmx: nCicMetaSubst.cmi
+nCicUnification.cmo: nCicUnification.cmi
+nCicUnification.cmx: nCicUnification.cmi
nCicRefiner.cmo: nCicRefiner.cmi
nCicRefiner.cmx: nCicRefiner.cmi
PREDICATES =
INTERFACE_FILES = \
- nCicRefiner.mli
+ nCicMetaSubst.mli \
+ nCicUnification.mli \
+ nCicRefiner.mli \
IMPLEMENTATION_FILES = \
$(INTERFACE_FILES:%.mli=%.ml)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+
+(*open Printf
+
+(* PROFILING *)
+(*
+let deref_counter = ref 0
+let apply_subst_context_counter = ref 0
+let apply_subst_metasenv_counter = ref 0
+let lift_counter = ref 0
+let subst_counter = ref 0
+let whd_counter = ref 0
+let are_convertible_counter = ref 0
+let metasenv_length = ref 0
+let context_length = ref 0
+let reset_counters () =
+ apply_subst_counter := 0;
+ apply_subst_context_counter := 0;
+ apply_subst_metasenv_counter := 0;
+ lift_counter := 0;
+ subst_counter := 0;
+ whd_counter := 0;
+ are_convertible_counter := 0;
+ metasenv_length := 0;
+ context_length := 0
+let print_counters () =
+ debug_print (lazy (Printf.sprintf
+"apply_subst: %d
+apply_subst_context: %d
+apply_subst_metasenv: %d
+lift: %d
+subst: %d
+whd: %d
+are_convertible: %d
+metasenv length: %d (avg = %.2f)
+context length: %d (avg = %.2f)
+"
+ !apply_subst_counter !apply_subst_context_counter
+ !apply_subst_metasenv_counter !lift_counter !subst_counter !whd_counter
+ !are_convertible_counter !metasenv_length
+ ((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
+ !context_length
+ ((float !context_length) /. (float !apply_subst_context_counter))
+ ))*)
+
+
+
+exception MetaSubstFailure of string Lazy.t
+exception Uncertain of string Lazy.t
+exception AssertFailure of string Lazy.t
+exception DeliftingARelWouldCaptureAFreeVariable;;
+
+let debug_print = fun _ -> ()
+
+type substitution = (int * (Cic.context * Cic.term)) list
+
+(*
+let rec deref subst =
+ let third _,_,a = a in
+ function
+ Cic.Meta(n,l) as t ->
+ (try
+ deref subst
+ (CicSubstitution.subst_meta
+ l (third (CicUtil.lookup_subst n subst)))
+ with
+ CicUtil.Subst_not_found _ -> t)
+ | t -> t
+;;
+*)
+
+let lookup_subst = CicUtil.lookup_subst
+;;
+
+(* clean_up_meta take a metasenv and a term and make every local context
+of each occurrence of a metavariable consistent with its canonical context,
+with respect to the hidden hipothesis *)
+
+(*
+let clean_up_meta subst metasenv t =
+ let module C = Cic in
+ let rec aux t =
+ match t with
+ C.Rel _
+ | C.Sort _ -> t
+ | C.Implicit _ -> assert false
+ | C.Meta (n,l) as t ->
+ let cc =
+ (try
+ let (cc,_) = lookup_subst n subst in cc
+ with CicUtil.Subst_not_found _ ->
+ try
+ let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc
+ with CicUtil.Meta_not_found _ -> assert false) in
+ let l' =
+ (try
+ List.map2
+ (fun t1 t2 ->
+ match t1,t2 with
+ None , _ -> None
+ | _ , t -> t) cc l
+ with
+ Invalid_argument _ -> assert false) in
+ C.Meta (n, l')
+ | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+ | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest)
+ | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest)
+ | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest)
+ | C.Appl l -> C.Appl (List.map aux l)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.Var (uri, exp_named_subst')
+ | C.Const (uri, exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.Const (uri, exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.MutInd (uri, tyno, exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.MutConstruct (uri, tyno, consno, exp_named_subst')
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ C.MutCase (uri, tyno, aux out, aux te, List.map aux pl)
+ | C.Fix (i,fl) ->
+ let fl' =
+ List.map
+ (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl
+ in
+ C.Fix (i, fl')
+ | C.CoFix (i,fl) ->
+ let fl' =
+ List.map
+ (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl
+ in
+ C.CoFix (i, fl')
+ in
+ aux t *)
+
+(*** 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 (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+ in
+ C.Var (uri, exp_named_subst')
+ | C.Meta (i, l) ->
+ (try
+ let (_, t,_) = lookup_subst i subst in
+ um_aux (S.subst_meta l t)
+ with CicUtil.Subst_not_found _ ->
+ (* unconstrained 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 _
+ | C.Implicit _ as t -> t
+ | 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,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, 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
+ let t' =
+ match um_aux he with
+ Cic.Appl l -> Cic.Appl (l@tl')
+ | he' -> Cic.Appl (he'::tl')
+ in
+ begin
+ match he with
+ Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
+ | _ -> t'
+ end
+ in
+ fun subst t ->
+(* incr apply_subst_counter; *)
+match subst with
+ [] -> t
+ | _ -> apply_subst_gen ~appl_fun subst t
+;;
+
+let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
+let apply_subst s t =
+ profiler.HExtlib.profile (apply_subst s) t
+
+
+let apply_subst_context subst context =
+ match subst with
+ [] -> context
+ | _ ->
+(*
+ incr apply_subst_context_counter;
+ context_length := !context_length + List.length 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' = 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 =
+(*
+ incr apply_subst_metasenv_counter;
+ metasenv_length := !metasenv_length + List.length metasenv;
+*)
+match subst with
+ [] -> metasenv
+ | _ ->
+ List.map
+ (fun (n, context, ty) ->
+ (n, apply_subst_context subst context, apply_subst subst ty))
+ (List.filter
+ (fun (i, _, _) -> not (List.mem_assoc i subst))
+ metasenv)
+
+(***** Pretty printing functions ******)
+
+let ppterm ~metasenv subst term =
+ CicPp.ppterm ~metasenv (apply_subst subst term)
+
+let ppterm_in_name_context ~metasenv subst term name_context =
+ CicPp.pp ~metasenv (apply_subst subst term) name_context
+
+let ppterm_in_context ~metasenv subst term context =
+ let name_context =
+ List.map (function None -> None | Some (n,_) -> Some n) context
+ in
+ ppterm_in_name_context ~metasenv subst term name_context
+
+let ppterm_in_context_ref = ref ppterm_in_context
+let set_ppterm_in_context f =
+ ppterm_in_context_ref := f
+let use_low_level_ppterm_in_context = ref false
+
+let ppterm_in_context ~metasenv subst term context =
+ if !use_low_level_ppterm_in_context then
+ ppterm_in_context ~metasenv subst term context
+ else
+ !ppterm_in_context_ref ~metasenv subst term context
+
+let ppcontext' ~metasenv ?(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_name_context ~metasenv subst t name_context),
+ (Some n)::name_context
+ | Some (n,Cic.Def (bo,ty)) ->
+ sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
+ (ppterm_in_name_context ~metasenv subst ty name_context)
+ (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
+ | None ->
+ sprintf "%s_ :? _" (separate i), None::name_context
+ ) context ("",[])
+
+let ppsubst_unfolded ~metasenv subst =
+ String.concat "\n"
+ (List.map
+ (fun (idx, (c, t,ty)) ->
+ let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
+ sprintf "%s |- ?%d : %s := %s" context idx
+(ppterm_in_name_context ~metasenv [] ty name_context)
+ (ppterm_in_name_context ~metasenv subst t name_context))
+ subst)
+(*
+ Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
+ subst) *)
+;;
+
+let ppsubst ~metasenv subst =
+ String.concat "\n"
+ (List.map
+ (fun (idx, (c, t, ty)) ->
+ let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in
+ sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context)
+ (ppterm_in_name_context ~metasenv [] t name_context))
+ subst)
+;;
+
+let ppcontext ~metasenv ?sep subst context =
+ fst (ppcontext' ~metasenv ?sep subst context)
+
+let ppmetasenv ?(sep = "\n") subst metasenv =
+ String.concat sep
+ (List.map
+ (fun (i, c, t) ->
+ let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
+ sprintf "%s |- ?%d: %s" context i
+ (ppterm_in_name_context ~metasenv subst t name_context))
+ (List.filter
+ (fun (i, _, _) -> not (List.mem_assoc i subst))
+ metasenv))
+
+let tempi_type_of_aux_subst = ref 0.0;;
+let tempi_subst = ref 0.0;;
+let tempi_type_of_aux = ref 0.0;;
+
+(**** DELIFT ****)
+(* the delift function takes in input a metavariable index, an ordered list of
+ * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
+ * (rel(nk)) with rel(k). Typically, the list of optional terms is the explicit
+ * substitution that is applied to a metavariable occurrence and the result of
+ * the delift function is a term the implicit variable can be substituted with
+ * to make the term [t] unifiable with the metavariable occurrence. In general,
+ * the problem is undecidable if we consider equivalence in place of alpha
+ * convertibility. Our implementation, though, is even weaker than alpha
+ * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
+ * (missing all the other cases). Does this matter in practice?
+ * The metavariable index is the index of the metavariable that must not occur
+ * in the term (for occur check).
+ *)
+
+exception NotInTheList;;
+
+let position n =
+ let rec aux k =
+ function
+ [] -> raise NotInTheList
+ | (Some (Cic.Rel m))::_ when m=n -> k
+ | _::tl -> aux (k+1) tl in
+ aux 1
+;;
+
+exception Occur;;
+
+let rec force_does_not_occur subst to_be_restricted t =
+ let module C = Cic in
+ let more_to_be_restricted = ref [] in
+ let rec aux k = function
+ C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
+ | C.Rel _
+ | C.Sort _ as t -> t
+ | C.Implicit _ -> assert false
+ | C.Meta (n, l) ->
+ (* we do not retrieve the term associated to ?n in subst since *)
+ (* in this way we can restrict if something goes wrong *)
+ let l' =
+ let i = ref 0 in
+ List.map
+ (function t ->
+ incr i ;
+ match t with
+ None -> None
+ | Some t ->
+ try
+ Some (aux k t)
+ with Occur ->
+ more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
+ None)
+ l
+ in
+ C.Meta (n, l')
+ | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
+ | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
+ | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
+ | C.LetIn (name,so,ty,dest) ->
+ C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
+ | C.Appl l -> C.Appl (List.map (aux k) l)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
+ in
+ C.Var (uri, exp_named_subst')
+ | C.Const (uri, exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
+ in
+ C.Const (uri, exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
+ in
+ C.MutInd (uri, tyno, exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
+ in
+ C.MutConstruct (uri, tyno, consno, exp_named_subst')
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl)
+ | C.Fix (i,fl) ->
+ let len = List.length fl in
+ let k_plus_len = k + len in
+ let fl' =
+ List.map
+ (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl
+ in
+ C.Fix (i, fl')
+ | C.CoFix (i,fl) ->
+ let len = List.length fl in
+ let k_plus_len = k + len in
+ let fl' =
+ List.map
+ (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl
+ in
+ C.CoFix (i, fl')
+ in
+ let res = aux 0 t in
+ (!more_to_be_restricted, res)
+
+let rec restrict subst to_be_restricted metasenv =
+ match to_be_restricted with
+ | [] -> metasenv, subst
+ | _ ->
+ let names_of_context_indexes context indexes =
+ String.concat ", "
+ (List.map
+ (fun i ->
+ try
+ match List.nth context (i-1) with
+ | None -> assert false
+ | Some (n, _) -> CicPp.ppname n
+ with
+ Failure _ -> assert false
+ ) indexes)
+ in
+ let force_does_not_occur_in_context to_be_restricted = function
+ | None -> [], None
+ | Some (name, Cic.Decl t) ->
+ let (more_to_be_restricted, t') =
+ force_does_not_occur subst to_be_restricted t
+ in
+ more_to_be_restricted, Some (name, Cic.Decl t')
+ | Some (name, Cic.Def (bo, ty)) ->
+ let (more_to_be_restricted, bo') =
+ force_does_not_occur subst to_be_restricted bo
+ in
+ let more_to_be_restricted, ty' =
+ let more_to_be_restricted', ty' =
+ force_does_not_occur subst to_be_restricted ty
+ in
+ more_to_be_restricted @ more_to_be_restricted',
+ ty'
+ in
+ more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
+ in
+ let rec erase i to_be_restricted n = function
+ | [] -> [], to_be_restricted, []
+ | hd::tl ->
+ let more_to_be_restricted,restricted,tl' =
+ erase (i+1) to_be_restricted n tl
+ in
+ let restrict_me = List.mem i restricted in
+ if restrict_me then
+ more_to_be_restricted, restricted, None:: tl'
+ else
+ (try
+ let more_to_be_restricted', hd' =
+ let delifted_restricted =
+ let rec aux =
+ function
+ [] -> []
+ | j::tl when j > i -> (j - i)::aux tl
+ | _::tl -> aux tl
+ in
+ aux restricted
+ in
+ force_does_not_occur_in_context delifted_restricted hd
+ in
+ more_to_be_restricted @ more_to_be_restricted',
+ restricted, hd' :: tl'
+ with Occur ->
+ more_to_be_restricted, (i :: restricted), None :: tl')
+ in
+ let (more_to_be_restricted, metasenv) = (* restrict metasenv *)
+ List.fold_right
+ (fun (n, context, t) (more, metasenv) ->
+ let to_be_restricted =
+ List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
+ in
+ let (more_to_be_restricted, restricted, context') =
+ (* just an optimization *)
+ if to_be_restricted = [] then
+ [],[],context
+ else
+ erase 1 to_be_restricted n context
+ in
+ try
+ let more_to_be_restricted', t' =
+ force_does_not_occur subst restricted t
+ in
+ let metasenv' = (n, context', t') :: metasenv in
+ (more @ more_to_be_restricted @ more_to_be_restricted',
+ metasenv')
+ with Occur ->
+ raise (MetaSubstFailure (lazy (sprintf
+ "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
+ n (names_of_context_indexes context to_be_restricted)))))
+ metasenv ([], [])
+ in
+ let (more_to_be_restricted', subst) = (* restrict subst *)
+ List.fold_right
+ (* TODO: cambiare dopo l'aggiunta del ty *)
+ (fun (n, (context, term,ty)) (more, subst') ->
+ let to_be_restricted =
+ List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
+ in
+ (try
+ let (more_to_be_restricted, restricted, context') =
+ (* just an optimization *)
+ if to_be_restricted = [] then
+ [], [], context
+ else
+ erase 1 to_be_restricted n context
+ in
+ let more_to_be_restricted', term' =
+ force_does_not_occur subst restricted term
+ in
+ let more_to_be_restricted'', ty' =
+ force_does_not_occur subst restricted ty in
+ let subst' = (n, (context', term',ty')) :: subst' in
+ let more =
+ more @ more_to_be_restricted
+ @ more_to_be_restricted'@more_to_be_restricted'' in
+ (more, subst')
+ with Occur ->
+ let error_msg = lazy (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
+ (ppterm ~metasenv subst term))
+ in
+ (* DEBUG
+ debug_print (lazy error_msg);
+ debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
+ debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
+ debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
+ raise (MetaSubstFailure error_msg)))
+ subst ([], [])
+ in
+ restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
+;;
+
+(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*)
+
+let delift n subst context metasenv l t =
+(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_),
+ otherwise the occur check does not make sense *)
+
+(*
+ debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))));
+*)
+
+ let module S = CicSubstitution in
+ let l =
+ let (_, canonical_context, _) =
+ try
+ CicUtil.lookup_meta n metasenv
+ with CicUtil.Meta_not_found _ ->
+ raise (MetaSubstFailure (lazy
+ ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^
+ "declared in the metasenv")))
+ in
+ List.map2 (fun ct lt ->
+ match (ct, lt) with
+ | None, _ -> None
+ | Some _, _ -> lt)
+ canonical_context l
+ in
+ let to_be_restricted = ref [] in
+ let rec deliftaux k =
+ let module C = Cic in
+ function
+ | C.Rel m as t->
+ if m <=k then
+ t
+ else
+ (try
+ match List.nth context (m-k-1) with
+ Some (_,C.Def (t,_)) ->
+ (try
+ C.Rel ((position (m-k) l) + k)
+ with
+ NotInTheList ->
+ (*CSC: Hmmm. This bit of reduction is not in the spirit of *)
+ (*CSC: first order unification. Does it help or does it harm? *)
+ (*CSC: ANSWER: it hurts performances since it is possible to *)
+ (*CSC: have an exponential explosion of the size of the proof.*)
+ (*CSC: However, without this bit of reduction some "apply" in *)
+ (*CSC: the library fail (e.g. nat/nth_prime.ma). *)
+ deliftaux k (S.lift m t))
+ | Some (_,C.Decl t) ->
+ C.Rel ((position (m-k) l) + k)
+ | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
+ with
+ Failure _ ->
+ raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
+ )
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
+ in
+ C.Var (uri,exp_named_subst')
+ | C.Meta (i, l1) as t ->
+ (try
+ let (_,t,_) = CicUtil.lookup_subst i subst in
+ deliftaux k (CicSubstitution.subst_meta l1 t)
+ with CicUtil.Subst_not_found _ ->
+ (* see the top level invariant *)
+ if (i = n) then
+ raise (MetaSubstFailure (lazy (sprintf
+ "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
+ i (ppterm ~metasenv subst t))))
+ else
+ begin
+ (* I do not consider the term associated to ?i in subst since *)
+ (* in this way I can restrict if something goes wrong. *)
+ let rec deliftl j =
+ function
+ [] -> []
+ | None::tl -> None::(deliftl (j+1) tl)
+ | (Some t)::tl ->
+ let l1' = (deliftl (j+1) tl) in
+ try
+ Some (deliftaux k t)::l1'
+ with
+ NotInTheList
+ | MetaSubstFailure _ ->
+ to_be_restricted :=
+ (i,j)::!to_be_restricted ; None::l1'
+ in
+ let l' = deliftl 1 l1 in
+ C.Meta(i,l')
+ end)
+ | C.Sort _ as t -> t
+ | C.Implicit _ as t -> t
+ | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
+ | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
+ | C.Appl l -> C.Appl (List.map (deliftaux k) l)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,typeno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,deliftaux k 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 (function (uri,t) -> uri,deliftaux k t) exp_named_subst
+ in
+ C.MutConstruct (uri,typeno,consno,exp_named_subst')
+ | C.MutCase (sp,i,outty,t,pl) ->
+ C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
+ List.map (deliftaux k) pl)
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, i, ty, bo) ->
+ (name, i, deliftaux k ty, deliftaux (k+len) bo))
+ fl
+ in
+ C.Fix (i, liftedfl)
+ | C.CoFix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, liftedfl)
+ in
+ let res =
+ try
+ deliftaux 0 t
+ with
+ NotInTheList ->
+ (* This is the case where we fail even first order unification. *)
+ (* The reason is that our delift function is weaker than first *)
+ (* order (in the sense of alpha-conversion). See comment above *)
+ (* related to the delift function. *)
+(* debug_print (lazy "First Order UnificationFailure during delift") ;
+debug_print(lazy (sprintf
+ "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
+ (ppterm subst t)
+ (String.concat "; "
+ (List.map
+ (function Some t -> ppterm subst t | None -> "_") l
+ )))); *)
+ let msg = (lazy (sprintf
+ "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
+ (ppterm ~metasenv subst t)
+ (String.concat "; "
+ (List.map
+ (function Some t -> ppterm ~metasenv subst t | None -> "_")
+ l))))
+ in
+ if
+ List.exists
+ (function
+ Some t -> CicUtil.is_meta_closed (apply_subst subst t)
+ | None -> true) l
+ then
+ raise (Uncertain msg)
+ else
+ raise (MetaSubstFailure msg)
+ in
+ let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
+ res, metasenv, subst
+;;
+
+(* delifts a term t of n levels strating from k, that is changes (Rel m)
+ * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
+ *)
+let delift_rels_from subst metasenv k n =
+ let rec liftaux subst metasenv k =
+ let module C = Cic in
+ function
+ C.Rel m as t ->
+ if m < k then
+ t, subst, metasenv
+ else if m < k + n then
+ raise DeliftingARelWouldCaptureAFreeVariable
+ else
+ C.Rel (m - n), subst, metasenv
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+ in
+ C.Var (uri,exp_named_subst'),subst,metasenv
+ | C.Meta (i,l) ->
+ (try
+ let (_, t,_) = lookup_subst i subst in
+ liftaux subst metasenv k (CicSubstitution.subst_meta l t)
+ with CicUtil.Subst_not_found _ ->
+ let l',to_be_restricted,subst,metasenv =
+ let rec aux con l subst metasenv =
+ match l with
+ [] -> [],[],subst,metasenv
+ | he::tl ->
+ let tl',to_be_restricted,subst,metasenv =
+ aux (con + 1) tl subst metasenv in
+ let he',more_to_be_restricted,subst,metasenv =
+ match he with
+ None -> None,[],subst,metasenv
+ | Some t ->
+ try
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ Some t',[],subst,metasenv
+ with
+ DeliftingARelWouldCaptureAFreeVariable ->
+ None,[i,con],subst,metasenv
+ in
+ he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
+ in
+ aux 1 l subst metasenv in
+ let metasenv,subst = restrict subst to_be_restricted metasenv in
+ C.Meta(i,l'),subst,metasenv)
+ | C.Sort _ as t -> t,subst,metasenv
+ | C.Implicit _ as t -> t,subst,metasenv
+ | C.Cast (te,ty) ->
+ let te',subst,metasenv = liftaux subst metasenv k te in
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ C.Cast (te',ty'),subst,metasenv
+ | C.Prod (n,s,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.Prod (n,s',t'),subst,metasenv
+ | C.Lambda (n,s,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.Lambda (n,s',t'),subst,metasenv
+ | C.LetIn (n,s,ty,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.LetIn (n,s',ty',t'),subst,metasenv
+ | C.Appl l ->
+ let l',subst,metasenv =
+ List.fold_right
+ (fun t (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ t'::l,subst,metasenv) l ([],subst,metasenv) in
+ C.Appl l',subst,metasenv
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+ in
+ C.Const (uri,exp_named_subst'),subst,metasenv
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+ in
+ C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+ in
+ C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
+ | C.MutCase (sp,i,outty,t,pl) ->
+ let outty',subst,metasenv = liftaux subst metasenv k outty in
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ let pl',subst,metasenv =
+ List.fold_right
+ (fun t (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ t'::l,subst,metasenv) pl ([],subst,metasenv)
+ in
+ C.MutCase (sp,i,outty',t',pl'),subst,metasenv
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl,subst,metasenv =
+ List.fold_right
+ (fun (name, i, ty, bo) (l,subst,metasenv) ->
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+ (name,i,ty',bo')::l,subst,metasenv
+ ) fl ([],subst,metasenv)
+ in
+ C.Fix (i, liftedfl),subst,metasenv
+ | C.CoFix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl,subst,metasenv =
+ List.fold_right
+ (fun (name, ty, bo) (l,subst,metasenv) ->
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+ (name,ty',bo')::l,subst,metasenv
+ ) fl ([],subst,metasenv)
+ in
+ C.CoFix (i, liftedfl),subst,metasenv
+ in
+ liftaux subst metasenv k
+
+let delift_rels subst metasenv n t =
+ delift_rels_from subst metasenv 1 n t
+
+
+(**** END OF DELIFT ****)
+
+
+(** {2 Format-like pretty printers} *)
+
+let fpp_gen ppf s =
+ Format.pp_print_string ppf s;
+ Format.pp_print_newline ppf ();
+ Format.pp_print_flush ppf ()
+
+let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst)
+let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
+let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)
+*)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+(*
+
+exception MetaSubstFailure of string Lazy.t
+exception Uncertain of string Lazy.t
+exception AssertFailure of string Lazy.t
+exception DeliftingARelWouldCaptureAFreeVariable;;
+
+(* The entry (i,t) in a substitution means that *)
+(* (META i) have been instantiated with t. *)
+(* type substitution = (int * (Cic.context * Cic.term)) list *)
+
+ (** @raise SubstNotFound *)
+
+(* apply_subst subst t *)
+(* applies the substitution [subst] to [t] *)
+(* [subst] must be already unwinded *)
+
+val apply_subst : Cic.substitution -> Cic.term -> Cic.term
+val apply_subst_context : Cic.substitution -> Cic.context -> Cic.context
+val apply_subst_metasenv: Cic.substitution -> Cic.metasenv -> Cic.metasenv
+
+(*** delifting ***)
+
+val delift :
+ int -> Cic.substitution -> Cic.context -> Cic.metasenv ->
+ (Cic.term option) list -> Cic.term ->
+ Cic.term * Cic.metasenv * Cic.substitution
+val restrict :
+ Cic.substitution -> (int * int) list -> Cic.metasenv ->
+ Cic.metasenv * Cic.substitution
+
+(** delifts the Rels in t of n
+ * @raise DeliftingARelWouldCaptureAFreeVariable
+ *)
+val delift_rels :
+ Cic.substitution -> Cic.metasenv -> int -> Cic.term ->
+ Cic.term * Cic.substitution * Cic.metasenv
+
+(** {2 Pretty printers} *)
+val use_low_level_ppterm_in_context : bool ref
+val set_ppterm_in_context :
+ (metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context ->
+ string) -> unit
+
+val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string
+val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string
+val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string
+val ppcontext:
+ metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context ->
+ string
+val ppterm_in_name_context:
+ metasenv:Cic.metasenv -> Cic.substitution -> Cic.term ->
+ (Cic.name option) list -> string
+val ppterm_in_context:
+ metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string
+val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> 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 -> Cic.substitution -> unit
+val fppterm: Format.formatter -> Cic.term -> unit
+val fppmetasenv: Format.formatter -> Cic.metasenv -> unit
+
+(*
+(* DEBUG *)
+val print_counters: unit -> unit
+val reset_counters: unit -> unit
+*)
+
+(* val clean_up_meta :
+ Cic.substitution -> Cic.metasenv -> Cic.term -> Cic.term
+*)
+*)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+(*
+
+open Printf
+
+exception UnificationFailure of string Lazy.t;;
+exception Uncertain of string Lazy.t;;
+exception AssertFailure of string Lazy.t;;
+
+let verbose = false;;
+let debug_print = fun _ -> ()
+
+let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
+let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
+let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
+let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
+
+let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
+
+let type_of_aux' metasenv subst context term ugraph =
+let foo () =
+ try
+ profile.HExtlib.profile
+ (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
+ with
+ CicTypeChecker.TypeCheckerFailure msg ->
+ let msg =
+ lazy
+ (sprintf
+ "Kernel Type checking error:
+%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
+ (CicMetaSubst.ppterm ~metasenv subst term)
+ (CicMetaSubst.ppterm ~metasenv [] term)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
+ (CicMetaSubst.ppmetasenv subst metasenv)
+ (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
+ raise (AssertFailure msg)
+ | CicTypeChecker.AssertFailure msg ->
+ let msg = lazy
+ (sprintf
+ "Kernel Type checking assertion failure:
+%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
+ (CicMetaSubst.ppterm ~metasenv subst term)
+ (CicMetaSubst.ppterm ~metasenv [] term)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
+ (CicMetaSubst.ppmetasenv subst metasenv)
+ (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
+ raise (AssertFailure msg)
+in profiler_toa.HExtlib.profile foo ()
+;;
+
+let exists_a_meta l =
+ List.exists
+ (function
+ | Cic.Meta _
+ | Cic.Appl (Cic.Meta _::_) -> true
+ | _ -> false) l
+
+let rec deref subst t =
+ let snd (_,a,_) = a in
+ match t with
+ Cic.Meta(n,l) ->
+ (try
+ deref subst
+ (CicSubstitution.subst_meta
+ l (snd (CicUtil.lookup_subst n subst)))
+ with
+ CicUtil.Subst_not_found _ -> t)
+ | Cic.Appl(Cic.Meta(n,l)::args) ->
+ (match deref subst (Cic.Meta(n,l)) with
+ | Cic.Lambda _ as t ->
+ deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
+ | r -> Cic.Appl(r::args))
+ | Cic.Appl(((Cic.Lambda _) as t)::args) ->
+ deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
+ | t -> t
+;;
+
+let deref subst t =
+ let foo () = deref subst t
+ in profiler_deref.HExtlib.profile foo ()
+
+exception WrongShape;;
+let eta_reduce after_beta_expansion after_beta_expansion_body
+ before_beta_expansion
+ =
+ try
+ match before_beta_expansion,after_beta_expansion_body with
+ Cic.Appl l, Cic.Appl l' ->
+ let rec all_but_last check_last =
+ function
+ [] -> assert false
+ | [Cic.Rel 1] -> []
+ | [_] -> if check_last then raise WrongShape else []
+ | he::tl -> he::(all_but_last check_last tl)
+ in
+ let all_but_last check_last l =
+ match all_but_last check_last l with
+ [] -> assert false
+ | [he] -> he
+ | l -> Cic.Appl l
+ in
+ let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
+ let all_but_last = all_but_last false l in
+ (* here we should test alpha-equivalence; however we know by
+ construction that here alpha_equivalence is equivalent to = *)
+ if t = all_but_last then
+ all_but_last
+ else
+ after_beta_expansion
+ | _,_ -> after_beta_expansion
+ with
+ WrongShape -> after_beta_expansion
+
+let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
+ let module S = CicSubstitution in
+ let module C = Cic in
+let foo () =
+ let rec aux metasenv subst n context t' ugraph =
+ try
+
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst test_equality_only subst context metasenv
+ (CicSubstitution.lift n arg) t' ugraph
+
+ in
+ subst,metasenv,C.Rel (1 + n),ugraph1
+ with
+ Uncertain _
+ | UnificationFailure _ ->
+ match t' with
+ | C.Rel m -> subst,metasenv,
+ (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
+ | C.Var (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
+ | C.Meta (i,l) ->
+ (* andrea: in general, beta_expand can create badly typed
+ terms. This happens quite seldom in practice, UNLESS we
+ iterate on the local context. For this reason, we renounce
+ to iterate and just lift *)
+ let l =
+ List.map
+ (function
+ Some t -> Some (CicSubstitution.lift 1 t)
+ | None -> None) l in
+ subst, metasenv, C.Meta (i,l), ugraph
+ | C.Sort _
+ | C.Implicit _ as t -> subst,metasenv,t,ugraph
+ | C.Cast (te,ty) ->
+ let subst,metasenv,te',ugraph1 =
+ aux metasenv subst n context te ugraph in
+ let subst,metasenv,ty',ugraph2 =
+ aux metasenv subst n context ty ugraph1 in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Cast (te', ty')),ugraph2
+ | C.Prod (nn,s,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+ ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Prod (nn, s', t')),ugraph2
+ | C.Lambda (nn,s,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
+ | C.LetIn (nn,s,ty,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,ty',ugraph1 =
+ aux metasenv subst n context ty ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
+ ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
+ | C.Appl l ->
+ let subst,metasenv,revl',ugraph1 =
+ List.fold_left
+ (fun (subst,metasenv,appl,ugraph) t ->
+ let subst,metasenv,t',ugraph1 =
+ aux metasenv subst n context t ugraph in
+ subst,metasenv,(t'::appl),ugraph1
+ ) (subst,metasenv,[],ugraph) l
+ in
+ subst,metasenv,(C.Appl (List.rev revl')),ugraph1
+ | C.Const (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
+ | C.MutCase (sp,i,outt,t,pl) ->
+ let subst,metasenv,outt',ugraph1 =
+ aux metasenv subst n context outt ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst n context t ugraph1 in
+ let subst,metasenv,revpl',ugraph3 =
+ List.fold_left
+ (fun (subst,metasenv,pl,ugraph) t ->
+ let subst,metasenv,t',ugraph1 =
+ aux metasenv subst n context t ugraph in
+ subst,metasenv,(t'::pl),ugraph1
+ ) (subst,metasenv,[],ugraph2) pl
+ in
+ subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
+ (* TASSI: not sure this is serial *)
+ | C.Fix (i,fl) ->
+(*CSC: not implemented
+ let tylen = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+*)
+ subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
+ | C.CoFix (i,fl) ->
+(*CSC: not implemented
+ let tylen = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+
+*)
+ subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
+
+ and aux_exp_named_subst metasenv subst n context ens ugraph =
+ List.fold_right
+ (fun (uri,t) (subst,metasenv,l,ugraph) ->
+ let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
+ subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
+ in
+ let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name ~subst
+ metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
+ in
+ let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
+ let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
+ subst, metasenv, t'', ugraph2
+in profiler_beta_expand.HExtlib.profile foo ()
+
+
+and beta_expand_many test_equality_only metasenv subst context t args ugraph =
+ let _,subst,metasenv,hd,ugraph =
+ List.fold_right
+ (fun arg (num,subst,metasenv,t,ugraph) ->
+ let subst,metasenv,t,ugraph1 =
+ beta_expand num test_equality_only
+ metasenv subst context t arg ugraph
+ in
+ num+1,subst,metasenv,t,ugraph1
+ ) args (1,subst,metasenv,t,ugraph)
+ in
+ subst,metasenv,hd,ugraph
+
+and warn_if_not_unique xxx to1 to2 carr car1 car2 =
+ match xxx with
+ | [] -> ()
+ | (m2,_,c2,c2')::_ ->
+ let m1,c1,c1' = carr,to1,to2 in
+ let unopt =
+ function Some (_,t) -> CicPp.ppterm t
+ | None -> "id"
+ in
+ HLog.warn
+ ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
+ CoercDb.string_of_carr car2^": " ^
+ CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
+ unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
+ unopt c2^" + "^unopt c2')
+
+(* NUOVA UNIFICAZIONE *)
+(* A substitution is a (int * Cic.term) list that associates a
+ metavariable i with its body.
+ A metaenv is a (int * Cic.term) list that associate a metavariable
+ i with is type.
+ fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
+ a new substitution which is _NOT_ unwinded. It must be unwinded before
+ applying it. *)
+
+and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module S = CicSubstitution in
+ let t1 = deref subst t1 in
+ let t2 = deref subst t2 in
+ let (&&&) a b = (a && b) || ((not a) && (not b)) in
+(* let bef = Sys.time () in *)
+ let b,ugraph =
+ if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
+ false,ugraph
+ else
+let foo () =
+ R.are_convertible ~subst ~metasenv context t1 t2 ugraph
+in profiler_are_convertible.HExtlib.profile foo ()
+ in
+(* let aft = Sys.time () in
+if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
+CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
+CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
+ if b then
+ subst, metasenv, ugraph
+ else
+ match (t1, t2) with
+ | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
+ let _,subst,metasenv,ugraph1 =
+ (try
+ List.fold_left2
+ (fun (j,subst,metasenv,ugraph) t1 t2 ->
+ match t1,t2 with
+ None,_
+ | _,None -> j+1,subst,metasenv,ugraph
+ | Some t1', Some t2' ->
+ (* First possibility: restriction *)
+ (* Second possibility: unification *)
+ (* Third possibility: convertibility *)
+ let b, ugraph1 =
+ R.are_convertible
+ ~subst ~metasenv context t1' t2' ugraph
+ in
+ if b then
+ j+1,subst,metasenv, ugraph1
+ else
+ (try
+ let subst,metasenv,ugraph2 =
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv t1' t2' ugraph
+ in
+ j+1,subst,metasenv,ugraph2
+ with
+ Uncertain _
+ | UnificationFailure _ ->
+debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
+ let metasenv, subst =
+ CicMetaSubst.restrict
+ subst [(n,j)] metasenv in
+ j+1,subst,metasenv,ugraph1)
+ ) (1,subst,metasenv,ugraph) ln lm
+ with
+ Exit ->
+ raise
+ (UnificationFailure (lazy "1"))
+ (*
+ (sprintf
+ "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))) *)
+ | Invalid_argument _ ->
+ raise
+ (UnificationFailure (lazy "2")))
+ (*
+ (sprintf
+ "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
+ in subst,metasenv,ugraph1
+ | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
+ fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
+ | (C.Meta (n,l), t)
+ | (t, C.Meta (n,l)) ->
+ let swap =
+ match t1,t2 with
+ C.Meta (n,_), C.Meta (m,_) when n < m -> false
+ | _, C.Meta _ -> false
+ | _,_ -> true
+ in
+ let lower = fun x y -> if swap then y else x in
+ let upper = fun x y -> if swap then x else y in
+ let fo_unif_subst_ordered
+ test_equality_only subst context metasenv m1 m2 ugraph =
+ fo_unif_subst test_equality_only subst context metasenv
+ (lower m1 m2) (upper m1 m2) ugraph
+ in
+ begin
+ let subst,metasenv,ugraph1 =
+ let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
+ (try
+ let tyt,ugraph1 =
+ type_of_aux' metasenv subst context t ugraph
+ in
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
+ with
+ UnificationFailure _ as e -> raise e
+ | Uncertain msg -> raise (UnificationFailure msg)
+ | AssertFailure _ ->
+ debug_print (lazy "siamo allo huge hack");
+ (* TODO huge hack!!!!
+ * we keep on unifying/refining in the hope that
+ * the problem will be eventually solved.
+ * In the meantime we're breaking a big invariant:
+ * the terms that we are unifying are no longer well
+ * typed in the current context (in the worst case
+ * we could even diverge) *)
+ (subst, metasenv,ugraph)) in
+ let t',metasenv,subst =
+ try
+ CicMetaSubst.delift n subst context metasenv l t
+ with
+ (CicMetaSubst.MetaSubstFailure msg)->
+ raise (UnificationFailure msg)
+ | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
+ in
+ let t'',ugraph2 =
+ match t' with
+ C.Sort (C.Type u) when not test_equality_only ->
+ let u' = CicUniv.fresh () in
+ let s = C.Sort (C.Type u') in
+ (try
+ let ugraph2 =
+ CicUniv.add_ge (upper u u') (lower u u') ugraph1
+ in
+ s,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg ->
+ raise (UnificationFailure msg))
+ | _ -> t',ugraph1
+ in
+ (* Unifying the types may have already instantiated n. Let's check *)
+ try
+ let (_, oldt,_) = CicUtil.lookup_subst n subst in
+ let lifted_oldt = S.subst_meta l oldt in
+ fo_unif_subst_ordered
+ test_equality_only subst context metasenv t lifted_oldt ugraph2
+ with
+ CicUtil.Subst_not_found _ ->
+ let (_, context, ty) = CicUtil.lookup_meta n metasenv in
+ let subst = (n, (context, t'',ty)) :: subst in
+ let metasenv =
+ List.filter (fun (m,_,_) -> not (n = m)) metasenv in
+ subst, metasenv, ugraph2
+ end
+ | (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
+ fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
+ exp_named_subst1 exp_named_subst2 ugraph
+ else
+ raise (UnificationFailure (lazy
+ (sprintf
+ "Can't unify %s with %s due to different constants"
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
+ | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
+ if UriManager.eq uri1 uri2 && i1 = i2 then
+ fo_unif_subst_exp_named_subst
+ test_equality_only
+ subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
+ else
+ raise (UnificationFailure
+ (lazy
+ (sprintf
+ "Can't unify %s with %s due to different inductive principles"
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
+ | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
+ C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
+ if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
+ fo_unif_subst_exp_named_subst
+ test_equality_only
+ subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
+ else
+ raise (UnificationFailure
+ (lazy
+ (sprintf
+ "Can't unify %s with %s due to different inductive constructors"
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+ | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
+ subst context metasenv te t2 ugraph
+ | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
+ subst context metasenv t1 te ugraph
+ | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
+ let subst',metasenv',ugraph1 =
+ fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
+ in
+ fo_unif_subst test_equality_only
+ subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
+ | (C.LetIn (_,s1,ty1,t1), t2)
+ | (t2, C.LetIn (_,s1,ty1,t1)) ->
+ fo_unif_subst
+ test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
+ | (C.Appl l1, C.Appl l2) ->
+ (* andrea: this case should be probably rewritten in the
+ spirit of deref *)
+ (match l1,l2 with
+ | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
+ (try
+ List.fold_left2
+ (fun (subst,metasenv,ugraph) t1 t2 ->
+ fo_unif_subst
+ test_equality_only subst context metasenv t1 t2 ugraph)
+ (subst,metasenv,ugraph) l1 l2
+ with (Invalid_argument msg) ->
+ raise (UnificationFailure (lazy msg)))
+ | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
+ (* we verify that none of the args is a Meta,
+ since beta expanding with respoect to a metavariable
+ makes no sense *)
+ (*
+ (try
+ let (_,t,_) = CicUtil.lookup_subst i subst in
+ let lifted = S.subst_meta l t in
+ let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv reduced t2 ugraph
+ with CicUtil.Subst_not_found _ -> *)
+ let subst,metasenv,beta_expanded,ugraph1 =
+ beta_expand_many
+ test_equality_only metasenv subst context t2 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ (C.Meta (i,l)) beta_expanded ugraph1
+ | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
+ (* (try
+ let (_,t,_) = CicUtil.lookup_subst i subst in
+ let lifted = S.subst_meta l t in
+ let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv t1 reduced ugraph
+ with CicUtil.Subst_not_found _ -> *)
+ let subst,metasenv,beta_expanded,ugraph1 =
+ beta_expand_many
+ test_equality_only
+ metasenv subst context t1 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ (C.Meta (i,l)) beta_expanded ugraph1
+ | _,_ ->
+ let lr1 = List.rev l1 in
+ let lr2 = List.rev l2 in
+ let rec
+ fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
+ match (l1,l2) with
+ [],_
+ | _,[] -> assert false
+ | ([h1],[h2]) ->
+ fo_unif_subst
+ test_equality_only subst context metasenv h1 h2 ugraph
+ | ([h],l)
+ | (l,[h]) ->
+ fo_unif_subst test_equality_only subst context metasenv
+ h (C.Appl (List.rev l)) ugraph
+ | ((h1::l1),(h2::l2)) ->
+ let subst', metasenv',ugraph1 =
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv h1 h2 ugraph
+ in
+ fo_unif_l
+ test_equality_only subst' metasenv' (l1,l2) ugraph1
+ in
+ (try
+ fo_unif_l
+ test_equality_only subst metasenv (lr1, lr2) ugraph
+ with
+ | UnificationFailure s
+ | Uncertain s as exn ->
+ (match l1, l2 with
+ (* {{{ pullback *)
+ | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
+ (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
+ CoercDb.is_a_coercion cc1 <> None &&
+ CoercDb.is_a_coercion cc2 <> None &&
+ not (UriManager.eq uri1 uri2) ->
+(*DEBUGGING ONLY:
+prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+*)
+ let inner_coerced t =
+ let t = CicMetaSubst.apply_subst subst t in
+ let rec aux c x t =
+ match t with
+ | Cic.Appl l ->
+ (match CoercGraph.coerced_arg l with
+ | None -> c, x
+ | Some (t,_) -> aux (List.hd l) t t)
+ | _ -> c, x
+ in
+ aux (Cic.Implicit None) (Cic.Implicit None) t
+ in
+ let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
+ let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
+ let car1, car2 =
+ match
+ CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
+ with
+ | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
+ | _ -> assert false
+ in
+ let head1_c, head2_c =
+ match
+ CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
+ with
+ | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
+ | _ -> assert false
+ in
+ let unfold uri ens args =
+ let o, _ =
+ CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
+ in
+ assert (ens = []);
+ match o with
+ | Cic.Constant (_,Some bo,_,_,_) ->
+ CicReduction.head_beta_reduce ~delta:false
+ (Cic.Appl (bo::args))
+ | _ -> assert false
+ in
+ let conclude subst metasenv ugraph last_tl1' last_tl2' =
+ let subst',metasenv,ugraph =
+(*DEBUGGING ONLY:
+prerr_endline
+ ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
+ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
+*)
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1' last_tl2' ugraph
+ in
+ if subst = subst' then raise exn
+ else
+(*DEBUGGING ONLY:
+let subst,metasenv,ugrph as res =
+*)
+ fo_unif_subst test_equality_only subst' context
+ metasenv (C.Appl l1) (C.Appl l2) ugraph
+(*DEBUGGING ONLY:
+in
+(prerr_endline
+ (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+ " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res)
+*)
+ in
+ if CoercDb.eq_carr car1 car2 then
+ match last_tl1,last_tl2 with
+ | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
+ | _, C.Meta _
+ | C.Meta _, _ ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1 last_tl2 ugraph
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
+ | _ when CoercDb.eq_carr head1_c head2_c ->
+ (* composite VS composition + metas avoiding
+ * coercions not only in coerced position *)
+ if c1 <> cc1 && c2 <> cc2 then
+ conclude subst metasenv ugraph
+ last_tl1 last_tl2
+ else
+ let l1, l2 =
+ if c1 = cc1 then
+ unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
+ else
+ Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv l1 l2 ugraph
+ | _ -> raise exn
+ else
+ let grow1 =
+ match last_tl1 with Cic.Meta _ -> true | _ -> false in
+ let grow2 =
+ match last_tl2 with Cic.Meta _ -> true | _ -> false in
+ if not (grow1 || grow2) then
+ (* no flexible terminals -> no pullback, but
+ * we still unify them, in some cases it helps *)
+ conclude subst metasenv ugraph last_tl1 last_tl2
+ else
+ let meets =
+ CoercGraph.meets
+ metasenv subst context (grow1,car1) (grow2,car2)
+ in
+ (match meets with
+ | [] -> raise exn
+ | (carr,metasenv,to1,to2)::xxx ->
+ warn_if_not_unique xxx to1 to2 carr car1 car2;
+ let last_tl1',(subst,metasenv,ugraph) =
+ match grow1,to1 with
+ | true,Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
+ metasenv coerced last_tl1 ugraph
+ | _ -> last_tl1,(subst,metasenv,ugraph)
+ in
+ let last_tl2',(subst,metasenv,ugraph) =
+ match grow2,to2 with
+ | true,Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
+ metasenv coerced last_tl2 ugraph
+ | _ -> last_tl2,(subst,metasenv,ugraph)
+ in
+ conclude subst metasenv ugraph last_tl1' last_tl2')
+ (* }}} pullback *)
+ (* {{{ CSC: This is necessary because of the "elim H" tactic
+ where the type of H is only reducible to an
+ inductive type. This could be extended from inductive
+ types to any rigid term. However, the code is
+ duplicated in two places: inside applications and
+ outside them. Probably it would be better to
+ work with lambda-bar terms instead. *)
+ | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
+ | (_, Cic.MutInd _::_) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "88")))
+ | (Cic.MutInd _::_,_) ->
+ let t2' = R.whd ~subst context t2 in
+ (match t2' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1 t2' ugraph
+ | _ -> raise
+ (UnificationFailure
+ (lazy ("not a mutind :"^
+ CicMetaSubst.ppterm ~metasenv subst t2 ))))
+ (* }}} elim H *)
+ | _ -> raise exn)))
+ | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
+ let subst', metasenv',ugraph1 =
+ fo_unif_subst test_equality_only subst context metasenv outt1 outt2
+ ugraph in
+ let subst'',metasenv'',ugraph2 =
+ fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
+ ugraph1 in
+ (try
+ List.fold_left2
+ (fun (subst,metasenv,ugraph) t1 t2 ->
+ fo_unif_subst
+ test_equality_only subst context metasenv t1 t2 ugraph
+ ) (subst'',metasenv'',ugraph2) pl1 pl2
+ with
+ Invalid_argument _ ->
+ raise (UnificationFailure (lazy "6.1")))
+ (* (sprintf
+ "Error trying to unify %s with %s: the number of branches is not the same."
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
+ | (C.Rel _, _) | (_, C.Rel _) ->
+ if t1 = t2 then
+ subst, metasenv,ugraph
+ else
+ raise (UnificationFailure (lazy
+ (sprintf
+ "Can't unify %s with %s because they are not convertible"
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
+ | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
+ let subst,metasenv,beta_expanded,ugraph1 =
+ beta_expand_many
+ test_equality_only metasenv subst context t2 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ (C.Meta (i,l)) beta_expanded ugraph1
+ | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
+ let subst,metasenv,beta_expanded,ugraph1 =
+ beta_expand_many
+ test_equality_only metasenv subst context t1 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ beta_expanded (C.Meta (i,l)) ugraph1
+(* Works iff there are no arguments applied to it; similar to the
+ case below
+ | (_, C.MutInd _) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.MutInd _ ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "8")))
+*)
+ | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
+ let subst',metasenv',ugraph1 =
+ fo_unif_subst true subst context metasenv s1 s2 ugraph
+ in
+ fo_unif_subst test_equality_only
+ subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
+ | (C.Prod _, _) ->
+ (match CicReduction.whd ~subst context t2 with
+ | C.Prod _ as t2 ->
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
+ | (_, C.Prod _) ->
+ (match CicReduction.whd ~subst context t1 with
+ | C.Prod _ as t1 ->
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
+ | (_,_) ->
+ (* delta-beta reduction should almost never be a problem for
+ unification since:
+ 1. long computations require iota reduction
+ 2. it is extremely rare that a close term t1 (that could be unified
+ to t2) beta-delta reduces to t1' while t2 does not beta-delta
+ reduces in the same way. This happens only if one meta of t2
+ occurs in head position during beta reduction. In this unluky
+ case too much reduction will be performed on t1 and unification
+ will surely fail. *)
+ let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
+ let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
+ if t1 = t1' && t2 = t2' then
+ raise (UnificationFailure
+ (lazy
+ (sprintf
+ "Can't unify %s with %s because they are not convertible"
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
+ else
+ try
+ fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
+ with
+ UnificationFailure _
+ | Uncertain _ ->
+ raise (UnificationFailure
+ (lazy
+ (sprintf
+ "Can't unify %s with %s because they are not convertible"
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
+
+and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
+ exp_named_subst1 exp_named_subst2 ugraph
+=
+ try
+ List.fold_left2
+ (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
+ assert (uri1=uri2) ;
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
+ with
+ Invalid_argument _ ->
+ let print_ens ens =
+ String.concat " ; "
+ (List.map
+ (fun (uri,t) ->
+ UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
+ ) ens)
+ in
+ raise (UnificationFailure (lazy (sprintf
+ "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))))
+
+(* A substitution is a (int * Cic.term) list that associates a *)
+(* metavariable i with its body. *)
+(* metasenv is of type Cic.metasenv *)
+(* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
+(* a new substitution which is already unwinded and ready to be applied and *)
+(* a new metasenv in which some hypothesis in the contexts of the *)
+(* metavariables may have been restricted. *)
+let fo_unif metasenv context t1 t2 ugraph =
+ fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
+
+let enrich_msg msg subst context metasenv t1 t2 ugraph =
+ lazy (
+ if verbose then
+ sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (try
+ let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+ CicPp.ppterm ty_t1
+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+ (CicMetaSubst.ppterm ~metasenv subst t2)
+ (try
+ let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+ CicPp.ppterm ty_t2
+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
+ (CicMetaSubst.ppcontext ~metasenv subst context)
+ (CicMetaSubst.ppmetasenv subst metasenv)
+ (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
+ else
+ sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
+ (try
+ let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+ CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
+ (try
+ let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+ CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
+ (CicMetaSubst.ppcontext ~metasenv subst context)
+ (CicMetaSubst.ppmetasenv subst metasenv)
+ (Lazy.force msg)
+ )
+
+let fo_unif_subst subst context metasenv t1 t2 ugraph =
+ try
+ fo_unif_subst false subst context metasenv t1 t2 ugraph
+ with
+ | AssertFailure msg ->
+ raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
+ | UnificationFailure msg ->
+ raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
+;;
+*)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+(*
+exception UnificationFailure of string Lazy.t;;
+exception Uncertain of string Lazy.t;;
+exception AssertFailure of string Lazy.t;;
+
+(* fo_unif metasenv context t1 t2 *)
+(* unifies [t1] and [t2] in a context [context]. *)
+(* Only the metavariables declared in [metasenv] *)
+(* can be used in [t1] and [t2]. *)
+(* The returned substitution can be directly *)
+(* withouth first unwinding it. *)
+val fo_unif :
+ Cic.metasenv -> Cic.context ->
+ Cic.term -> Cic.term -> CicUniv.universe_graph ->
+ Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+
+(* fo_unif_subst metasenv subst context t1 t2 *)
+(* unifies [t1] and [t2] in a context [context] *)
+(* and with [subst] as the current substitution *)
+(* (i.e. unifies ([subst] [t1]) and *)
+(* ([subst] [t2]) in a context *)
+(* ([subst] [context]) using the metasenv *)
+(* ([subst] [metasenv]) *)
+(* Only the metavariables declared in [metasenv] *)
+(* can be used in [t1] and [t2]. *)
+(* [subst] and the substitution returned are not *)
+(* unwinded. *)
+(*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la
+ cosa all'apply_subst!!!*)
+val fo_unif_subst :
+ Cic.substitution -> Cic.context -> Cic.metasenv ->
+ Cic.term -> Cic.term -> CicUniv.universe_graph ->
+ Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+
+ *)
projects / helm.git / commitdiff