--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+exception UnificationFailed;;
+(*CSC: Vecchia unificazione: exception Impossible;;*)
+exception Free;;
+exception OccurCheck;;
+
+type substitution = (int * Cic.term) list
+
+(*CSC: Hhhmmm. Forse dovremmo spostarla in CicSubstitution dove si trova la *)
+(*CSC: lift? O creare una proofEngineSubstitution? *)
+(* the function delift n m un-lifts a lambda term m of n level of abstractions.
+ It returns an exception Free if M contains a free variable in the range 1--n *)
+let delift n =
+ let rec deliftaux k =
+ let module C = Cic in
+ function
+ C.Rel m ->
+ if m < k then C.Rel m else
+ if m < k+n then raise Free
+ else C.Rel (m - n)
+ | C.Var _ as t -> t
+ | C.Meta _ as t -> t
+ | 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,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
+ | C.Appl l -> C.Appl (List.map (deliftaux k) l)
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
+ C.MutCase (sp, cookingsno, 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
+ if n = 0 then
+ (function t -> t)
+ else
+ deliftaux 1
+;;
+
+(* Questa funzione non serve piu'... per il momento la lascio *)
+(*
+let closed_up_to_n n m =
+ let rec closed_aux k =
+ let module C = Cic in
+ function
+ C.Rel m -> if m > k then () else raise Free
+ | C.Var _
+ | C.Meta _ (* we assume Meta are closed up to k; note that during
+ meta-unfolding we shall need to properly lift the
+ "body" of Metavariables *)
+ | C.Sort _
+ | C.Implicit -> ()
+ | C.Cast (te,ty) -> closed_aux k te; closed_aux k ty
+ | C.Prod (n,s,t) -> closed_aux k s; closed_aux (k+1) t
+ | C.Lambda (n,s,t) -> closed_aux k s; closed_aux (k+1) t
+ | C.LetIn (n,s,t) -> closed_aux k s; closed_aux (k+1) t
+ | C.Appl l -> List.iter (closed_aux k) l
+ | C.Const _
+ | C.Abst _
+ | C.MutInd _
+ | C.MutConstruct _ -> ()
+ | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
+ closed_aux k outty; closed_aux k t;
+ List.iter (closed_aux k) pl
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ List.iter
+ (fun (name, i, ty, bo) -> closed_aux k ty; closed_aux (k+len) bo)
+ fl
+ | C.CoFix (i, fl) ->
+ let len = List.length fl in
+ List.iter
+ (fun (name, ty, bo) -> closed_aux k ty; closed_aux (k+len) bo)
+ fl
+ in
+ if n = 0 then true
+ else
+ try closed_aux n m; true
+ with Free -> false
+;; *)
+
+(* 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. *)
+
+let fo_unif_new metasenv context t1 t2 =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module S = CicSubstitution in
+ let rec fo_unif_aux subst k t1 t2 =
+ match (t1, t2) with
+ (C.Meta n, C.Meta m) -> if n == m then subst
+ else let subst'=
+ let tn = try List.assoc n subst
+ with Not_found -> C.Meta n in
+ let tm = try List.assoc m subst
+ with Not_found -> C.Meta m in
+ (match (tn, tm) with
+ (C.Meta n, C.Meta m) -> if n==m then subst
+ else if n<m
+ then (m, C.Meta n)::subst
+ else (n, C.Meta m)::subst
+ | (C.Meta n, tm) -> (n, tm)::subst
+ | (tn, C.Meta m) -> (m, tn)::subst
+ | (tn,tm) -> fo_unif_aux subst 0 tn tm) in
+ (* unify types first *)
+ let tyn = List.assoc n metasenv in
+ let tym = List.assoc m metasenv in
+ fo_unif_aux subst' 0 tyn tym
+ | (C.Meta n, t)
+ | (t, C.Meta n) -> (* unify types first *)
+ let t' = delift k t in
+ let subst' =
+ (try fo_unif_aux subst 0 (List.assoc n subst) t'
+ with Not_found -> (n, t')::subst) in
+ let tyn = List.assoc n metasenv in
+ let tyt = CicTypeChecker.type_of_aux' metasenv context t' in
+ fo_unif_aux subst' 0 tyn tyt
+ | (C.Rel _, _)
+ | (_, C.Rel _)
+ | (C.Var _, _)
+ | (_, C.Var _)
+ | (C.Sort _ ,_)
+ | (_, C.Sort _)
+ | (C.Implicit, _)
+ | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
+ else raise UnificationFailed
+ | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
+ | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
+ | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) ->
+ let subst' = fo_unif_aux subst k s1 s2 in
+ fo_unif_aux subst' (k+1) t1 t2
+ | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) ->
+ let subst' = fo_unif_aux subst k s1 s2 in
+ fo_unif_aux subst' (k+1) t1 t2
+ | (C.LetIn (_,s1,t1), t2) -> fo_unif_aux subst k (S.subst s1 t1) t2
+ | (t1, C.LetIn (_,s2,t2)) -> fo_unif_aux subst k t1 (S.subst s2 t2)
+ | (C.Appl l1, C.Appl l2) ->
+ let lr1 = List.rev l1 in
+ let lr2 = List.rev l2 in
+ let rec fo_unif_l subst = function
+ [],_
+ | _,[] -> assert false
+ | ([h1],[h2]) -> fo_unif_aux subst k h1 h2
+ | ([h],l)
+ | (l,[h]) -> fo_unif_aux subst k h (C.Appl l)
+ | ((h1::l1),(h2::l2)) ->
+ let subst' = fo_unif_aux subst k h1 h2 in
+ fo_unif_l subst' (l1,l2)
+ in
+ fo_unif_l subst (lr1, lr2)
+ | (C.Const _, _)
+ | (_, C.Const _)
+ | (C.Abst _, _)
+ | (_, C.Abst _)
+ | (C.MutInd _, _)
+ | (_, C.MutInd _)
+ | (C.MutConstruct _, _)
+ | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
+ else raise UnificationFailed
+ | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
+ let subst' = fo_unif_aux subst k outt1 outt2 in
+ let subst'' = fo_unif_aux subst' k t1 t2 in
+ List.fold_left2 (function subst -> fo_unif_aux subst k) subst'' pl1 pl2
+ | (C.Fix _, _)
+ | (_, C.Fix _)
+ | (C.CoFix _, _)
+ | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
+ else raise UnificationFailed
+ | (_,_) -> raise UnificationFailed
+ in fo_unif_aux [] 0 t1 t2;;
+
+(* VECCHIA UNIFICAZIONE -- molto piu' bella, alas *)
+(*
+let fo_unif_mgu k t1 t2 mgu =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module S = CicSubstitution in
+ let rec deref n = match mgu.(n) with
+ C.Meta m as t -> if n = m then t else (deref m)
+ | t -> t
+ in
+ let rec fo_unif k t1 t2 = match (t1, t2) with
+ (* aggiungere l'unificazione sui tipi in caso di istanziazione *)
+ (C.Meta n, C.Meta m) -> if n == m then () else
+ let t1' = deref n in
+ let t2' = deref m in
+ (* deref of metavariables ARE already delifted *)
+ (match (t1',t2') with
+ (C.Meta n, C.Meta m) -> if n = m then () else
+ if n < m then mgu.(m) <- t1' else
+ if n > m then mgu.(n) <- t2'
+ | (C.Meta n, _) -> mgu.(n) <- t2'
+ | (_, C.Meta m) -> mgu.(m) <- t1'
+ | (_,_) -> fo_unif k t1' t2')
+ | (C.Meta n, _) -> let t1' = deref n in
+ let t2' = try delift k t2
+ with Free -> raise UnificationFailed in
+ (match t1' with
+ C.Meta n -> mgu.(n) <- t2'
+ | _ -> fo_unif k t1' t2')
+ | (_, C.Meta m) -> let t2' = deref m in
+ let t1' = try delift k t1
+ with Free -> raise UnificationFailed in
+ (match t2' with
+ C.Meta m -> mgu.(m) <- t1'
+ | _ -> fo_unif k t1' t2')
+ | (C.Rel _, _)
+ | (_, C.Rel _)
+ | (C.Var _, _)
+ | (_, C.Var _)
+ | (C.Sort _ ,_)
+ | (_, C.Sort _)
+ | (C.Implicit, _)
+ | (_, C.Implicit) -> if R.are_convertible t1 t2 then ()
+ else raise UnificationFailed
+ | (C.Cast (te,ty), _) -> fo_unif k te t2
+ | (_, C.Cast (te,ty)) -> fo_unif k t1 te
+ | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) -> fo_unif k s1 s2;
+ fo_unif (k+1) t1 t2
+ | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) -> fo_unif k s1 s2;
+ fo_unif (k+1) t1 t2
+ | (C.LetIn (_,s1,t1), _) -> fo_unif k (S.subst s1 t1) t2
+ | (_, C.LetIn (_,s2,t2)) -> fo_unif k t1 (S.subst s2 t2)
+ | (C.Appl (h1::l1), C.Appl (h2::l2)) ->
+ let lr1 = List.rev l1 in
+ let lr2 = List.rev l2 in
+ let rec fo_unif_aux = function
+ ([],l2) -> ([],l2)
+ | (l1,[]) -> (l1,[])
+ | ((h1::l1),(h2::l2)) -> fo_unif k h1 h2;
+ fo_unif_aux (l1,l2)
+ in
+ (match fo_unif_aux (lr1, lr2) with
+ ([],[]) -> fo_unif k h1 h2
+ | ([],l2) -> fo_unif k h1 (C.Appl (h2::List.rev l2))
+ | (l1,[]) -> fo_unif k (C.Appl (h1::List.rev l1)) h2
+ | (_,_) -> raise Impossible)
+ | (C.Const _, _)
+ | (_, C.Const _)
+ | (C.Abst _, _)
+ | (_, C.Abst _)
+ | (C.MutInd _, _)
+ | (_, C.MutInd _)
+ | (C.MutConstruct _, _)
+ | (_, C.MutConstruct _) -> print_endline "siamo qui"; flush stdout;
+ if R.are_convertible t1 t2 then ()
+ else raise UnificationFailed
+ | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
+ fo_unif k outt1 outt2;
+ fo_unif k t1 t2;
+ List.iter2 (fo_unif k) pl1 pl2
+ | (C.Fix _, _)
+ | (_, C.Fix _)
+ | (C.CoFix _, _)
+ | (_, C.CoFix _) -> if R.are_convertible t1 t2 then ()
+ else raise UnificationFailed
+ | (_,_) -> raise UnificationFailed
+ in fo_unif k t1 t2;mgu ;;
+*)
+
+(* unwind mgu mark m applies mgu to the term m; mark is an array of integers
+mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding,
+and is 1 if it has been succesfully unwinded. Meeting the value 2 during
+the computation is an error: occur-check *)
+
+let unwind subst unwinded t =
+ let unwinded = ref unwinded in
+ let frozen = ref [] in
+ let rec um_aux k =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded)
+ with Not_found ->
+ if List.mem i !frozen then
+ raise OccurCheck
+ else
+ let saved_frozen = !frozen in
+ frozen := i::!frozen ;
+ let res =
+ try
+ let t = List.assoc i subst in
+ let t' = um_aux 0 t in
+ unwinded := (i,t)::!unwinded ;
+ S.lift k t'
+ with
+ Not_found ->
+ (* not constrained variable, i.e. free in subst *)
+ C.Meta i
+ in
+ frozen := saved_frozen ;
+ res
+ )
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
+ | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
+ | C.Appl (he::tl) ->
+ let tl' = List.map (um_aux k) tl in
+ begin
+ match um_aux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ end
+ | C.Appl _ -> assert false
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
+ C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
+ List.map (um_aux k) pl)
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (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, um_aux k ty, um_aux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, liftedfl)
+ in
+ um_aux 0 t,!unwinded
+;;
+
+(*
+let unwind_meta mgu mark =
+ let rec um_aux k =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta i as t -> if mark.(i)=2 then raise OccurCheck else
+ if mark.(i)=1 then S.lift k mgu.(i)
+ else (match mgu.(i) with
+ C.Meta k as t1 -> if k = i then t
+ else (mark.(i) <- 2;
+ mgu.(i) <- (um_aux 0 t1);
+ mark.(i) <- 1;
+ S.lift k mgu.(i))
+ | _ -> (mark.(i) <- 2;
+ mgu.(i) <- (um_aux 0 mgu.(i));
+ mark.(i) <- 1;
+ S.lift k mgu.(i)))
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
+ | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
+ | C.Appl (he::tl) ->
+ let tl' = List.map (um_aux k) tl in
+ begin
+ match um_aux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ end
+ | C.Appl _ -> assert false
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
+ C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
+ List.map (um_aux k) pl)
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (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, um_aux k ty, um_aux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, liftedfl)
+ in
+ um_aux 0
+;;
+*)
+
+(* 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 subst meta_to_reduce t =
+ let unwinded = ref subst in
+ let rec um_aux k =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta i as t ->
+ (try
+ S.lift k (List.assoc i !unwinded)
+ with Not_found ->
+ C.Meta i)
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
+ | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
+ | C.Appl (he::tl) ->
+ let tl' = List.map (um_aux k) tl in
+ let t' =
+ match um_aux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ in
+ begin
+ match meta_to_reduce with
+ Some (mtr,reductions_no) when he = C.Meta mtr ->
+ let rec beta_reduce =
+ function
+ (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
+ let he'' = CicSubstitution.subst he' t in
+ if tl' = [] then
+ he''
+ else
+ beta_reduce (n-1,C.Appl(he''::tl'))
+ | (_,t) -> t
+ in
+ beta_reduce (reductions_no,t')
+ | _ -> t'
+ end
+ | C.Appl _ -> assert false
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
+ C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
+ List.map (um_aux k) pl)
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (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, um_aux k ty, um_aux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, liftedfl)
+ in
+ um_aux 0 t
+;;
+
+(* unwind mgu mark mm m applies mgu to the term m; mark is an array of integers
+mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding,
+and is 1 if it has been succesfully unwinded. Meeting the value 2 during
+the computation is an error: occur-check. When the META mm is to be unfolded
+and it is applied to something, one-step beta reduction is performed just
+after the unfolding. *)
+
+(*
+let unwind_meta_reducing mgu mark meta_to_reduce =
+ let rec um_aux k =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta i as t -> if mark.(i)=2 then raise OccurCheck else
+ if mark.(i)=1 then S.lift k mgu.(i)
+ else (match mgu.(i) with
+ C.Meta k as t1 -> if k = i then t
+ else (mark.(i) <- 2;
+ mgu.(i) <- (um_aux 0 t1);
+ mark.(i) <- 1;
+ S.lift k mgu.(i))
+ | _ -> (mark.(i) <- 2;
+ mgu.(i) <- (um_aux 0 mgu.(i));
+ mark.(i) <- 1;
+ S.lift k mgu.(i)))
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
+ | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
+ | C.Appl (he::tl) ->
+ let tl' = List.map (um_aux k) tl in
+ let t' =
+ match um_aux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ in
+ begin
+ match t', meta_to_reduce with
+ (C.Appl (C.Lambda (n,s,t)::he'::tl')),Some mtr
+ when he = C.Meta mtr ->
+(*CSC: Sbagliato!!! Effettua beta riduzione solo del primo argomento
+ *CSC: mentre dovrebbe farla dei primi n, dove n sono quelli eta-astratti
+*)
+ C.Appl((CicSubstitution.subst he' t)::tl')
+ | _ -> t'
+ end
+ | C.Appl _ -> assert false
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
+ C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
+ List.map (um_aux k) pl)
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (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, um_aux k ty, um_aux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, liftedfl)
+ in
+ um_aux 0
+;; *)
+
+(* UNWIND THE MGU INSIDE THE MGU *)
+(* let unwind mgu =
+ let mark = Array.make (Array.length mgu) 0 in
+ Array.iter (fun x -> let foo = unwind_meta mgu mark x in ()) mgu; mgu;; *)
+
+let unwind_subst subst =
+ List.fold_left
+ (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst
+;;
+
+let apply_subst subst t =
+ fst (unwind [] subst t)
+;;
+
+(* 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 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. *)
+let fo_unif metasenv context t1 t2 =
+ let subst_to_unwind = fo_unif_new metasenv context t1 t2 in
+ unwind_subst subst_to_unwind
+;;
projects / helm.git / commitdiff