From: Claudio Sacerdoti Coen Date: Fri, 26 Apr 2002 10:33:28 +0000 (+0000) Subject: First (very bugged) version of cic_unification committed. X-Git-Tag: V_0_3_0_debian_8~126 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=211f0ab4ee4c22c98147067987874b0b5a800b5b;p=helm.git First (very bugged) version of cic_unification committed. --- diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore index 2e6c28cc3..f1ca37656 100644 --- a/helm/ocaml/.cvsignore +++ b/helm/ocaml/.cvsignore @@ -8,6 +8,7 @@ META.helm-cic_cache META.helm-xml META.helm-cic_proof_checking META.helm-cic_textual_parser +META.helm-cic_unification Makefile Makefile.common configure diff --git a/helm/ocaml/META.helm-cic_unification.src b/helm/ocaml/META.helm-cic_unification.src new file mode 100644 index 000000000..6cb775dca --- /dev/null +++ b/helm/ocaml/META.helm-cic_unification.src @@ -0,0 +1,5 @@ +requires="helm-cic_proof_checking" +version="0.0.1" +archive(byte)="cic_unification.cma" +archive(native)="cic_unification.cmxa" +linkopts="" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 4cf5bb527..c9bfa3008 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,6 +1,6 @@ # Warning: the modules must be in compilation order MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ - cic_cache cic_proof_checking cic_textual_parser + cic_cache cic_proof_checking cic_textual_parser cic_unification OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/cic_unification/.cvsignore b/helm/ocaml/cic_unification/.cvsignore new file mode 100644 index 000000000..6b3eba302 --- /dev/null +++ b/helm/ocaml/cic_unification/.cvsignore @@ -0,0 +1 @@ +*.cm[iaox] *.cmxa diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend new file mode 100644 index 000000000..31eaf6dd0 --- /dev/null +++ b/helm/ocaml/cic_unification/.depend @@ -0,0 +1,2 @@ +cicUnification.cmo: cicUnification.cmi +cicUnification.cmx: cicUnification.cmi diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile new file mode 100644 index 000000000..5a88cbb4d --- /dev/null +++ b/helm/ocaml/cic_unification/Makefile @@ -0,0 +1,9 @@ +PACKAGE = cic_unification +REQUIRES = helm-cic_proof_checking +PREDICATES = + +INTERFACE_FILES = cicUnification.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = + +include ../Makefile.common diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml new file mode 100644 index 000000000..5b1d3ce1b --- /dev/null +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -0,0 +1,632 @@ +(* 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 (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 +;; diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli new file mode 100644 index 000000000..9fde49d9e --- /dev/null +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -0,0 +1,55 @@ +(* 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 +exception Free +exception OccurCheck + +(* The entry (i,t) in a substitution means that *) +(* (META i) have been instantiated with t. *) +type substitution = (int * Cic.term) list + +(* 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]. *) +val fo_unif : + (int * Cic.term) list -> Cic.context -> Cic.term -> Cic.term -> substitution + +(* apply_subst subst t *) +(* applies the substitution [sust] to [t] *) +val apply_subst : substitution -> Cic.term -> Cic.term + +(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) +(* performs as (apply_subst subst t) until it finds an application of *) +(* (META [mtr]) 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. *) +val apply_subst_reducing : + substitution -> (int * int) option -> Cic.term -> Cic.term