From cf5d6fab96c47ccb7d623d72742717d9b08bae7b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 20 Jul 2004 12:50:13 +0000 Subject: [PATCH] Subst has been added to the kernel. --- helm/ocaml/cic_proof_checking/cicPp.ml | 18 + helm/ocaml/cic_proof_checking/cicPp.mli | 30 +- .../ocaml/cic_proof_checking/cicReduction.mli | 5 +- .../cic_proof_checking/cicReductionMachine.ml | 36 +- .../cic_proof_checking/cicTypeChecker.ml | 473 +++++++++--------- .../cic_proof_checking/cicTypeChecker.mli | 2 +- helm/ocaml/cic_unification/cicMetaSubst.ml | 156 +++++- helm/ocaml/cic_unification/cicMetaSubst.mli | 10 +- helm/ocaml/cic_unification/cicMkImplicit.ml | 12 +- helm/ocaml/cic_unification/cicRefine.ml | 112 +++-- helm/ocaml/cic_unification/cicUnification.ml | 413 ++++++++------- 11 files changed, 772 insertions(+), 495 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 8172b47f7..b9a5b72f4 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -193,6 +193,24 @@ let ppinductiveType (typename, inductive, arity, cons) = cons "" ;; +let ppcontext ?(sep = "\n") context = + let separate s = if s = "" then "" else s ^ sep in + fst (List.fold_right + (fun context_entry (i,name_context) -> + match context_entry with + Some (n,Cic.Decl t) -> + Printf.sprintf "%s%s : %s" (separate i) (ppname n) + (pp t name_context), (Some n)::name_context + | Some (n,Cic.Def (bo,ty)) -> + Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n) + (match ty with + None -> "_" + | Some ty -> pp ty name_context) + (pp bo name_context), (Some n)::name_context + | None -> + Printf.sprintf "%s_ :? _" (separate i), None::name_context + ) context ("",[])) + (* ppobj obj returns a string with describing the cic object obj in a syntax *) (* similar to the one used by Coq *) let ppobj obj = diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli index 371b75e29..417378d29 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.mli +++ b/helm/ocaml/cic_proof_checking/cicPp.mli @@ -23,25 +23,27 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* This module implements a very simple Coq-like pretty printer that, given *) -(* an object of cic (internal representation) returns a string describing the *) -(* object in a syntax similar to that of coq *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module implements a very simple Coq-like pretty printer that, given *) +(* an object of cic (internal representation) returns a string describing the*) +(* object in a syntax similar to that of coq *) +(* *) +(*****************************************************************************) -(* ppobj obj returns a string with describing the cic object obj in a syntax *) -(* similar to the one used by Coq *) +(* ppobj obj returns a string with describing the cic object obj in a syntax*) +(* similar to the one used by Coq *) val ppobj : Cic.obj -> string val ppterm : Cic.term -> string +val ppcontext : ?sep:string -> Cic.context -> string + (* Required only by the topLevel. It is the generalization of ppterm to *) (* work with environments. *) val pp : Cic.term -> (Cic.name option) list -> string diff --git a/helm/ocaml/cic_proof_checking/cicReduction.mli b/helm/ocaml/cic_proof_checking/cicReduction.mli index 7a6255003..eaa2265ba 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.mli +++ b/helm/ocaml/cic_proof_checking/cicReduction.mli @@ -29,5 +29,6 @@ exception ReferenceToVariable exception ReferenceToCurrentProof exception ReferenceToInductiveDefinition val fdebug : int ref -val whd : Cic.context -> Cic.term -> Cic.term -val are_convertible : Cic.context -> Cic.term -> Cic.term -> bool +val whd : ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term +val are_convertible : + ?subst:Cic.substitution -> ?metasenv:Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> bool diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index e963ddce9..4b8099fed 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -498,7 +498,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; unwind' 0 ;; - let reduce context : config -> Cic.term = + let reduce ?(subst = []) context : config -> Cic.term = let module C = Cic in let module S = CicSubstitution in let rec reduce = @@ -542,9 +542,13 @@ if List.mem uri params then prerr_endline "---- OK2" ; let ens' = push_exp_named_subst k e ens exp_named_subst in reduce (0, [], ens', body, s) ) - | (k, e, ens, (C.Meta _ as t), s) -> - let t' = unwind k e ens t in - if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) + | (k, e, ens, (C.Meta (n,l) as t), s) -> + (try + let (_, term) = CicUtil.lookup_subst n subst in + reduce (k, e, ens,CicSubstitution.lift_meta l term,s) + with CicUtil.Subst_not_found _ -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))) | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *) | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *) | (k, e, ens, (C.Cast (te,ty) as t), s) -> @@ -722,10 +726,10 @@ if List.mem uri params then prerr_endline "---- OK2" ; | (uri,t)::tl -> push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl in - reduce + reduce ;; - let rec whd context t = reduce context (0, [], [], t, []);; + let rec whd ?(subst=[]) context t = reduce ~subst context (0, [], [], t, []);; (* DEBUGGING ONLY let whd context t = @@ -769,7 +773,7 @@ module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; let whd = R.whd;; (* t1, t2 must be well-typed *) -let are_convertible = +let are_convertible ?(subst=[]) ?(metasenv=[]) = let module U = UriManager in let rec aux test_equality_only context t1 t2 = let aux2 test_equality_only t1 t2 = @@ -792,8 +796,10 @@ let are_convertible = with Invalid_argument _ -> false ) - | (C.Meta (n1,l1), C.Meta (n2,l2)) -> + | (C.Meta (n1,l1), C.Meta (n2,l2)) -> n1 = n2 && + let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in + let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in List.fold_left2 (fun b t1 t2 -> b && @@ -900,10 +906,18 @@ let are_convertible = in if aux2 test_equality_only t1 t2 then true else - begin + begin debug t1 [t2] "PREWHD"; - let t1' = whd context t1 in - let t2' = whd context t2 in + (* + (match t1 with + Cic.Meta _ -> + prerr_endline (CicPp.ppterm t1); + prerr_endline (CicPp.ppterm (whd ~subst context t1)); + prerr_endline (CicPp.ppterm t2); + prerr_endline (CicPp.ppterm (whd ~subst context t2)) + | _ -> ()); *) + let t1' = whd ~subst context t1 in + let t2' = whd ~subst context t2 in debug t1' [t2'] "POSTWHD"; aux2 test_equality_only t1' t2' end diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 1577b2f3f..5715778fb 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -592,11 +592,11 @@ and recursive_args context n nn te = | C.Fix _ | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *) -and get_new_safes context p c rl safes n nn x = +and get_new_safes ?(subst = []) context p c rl safes n nn x = let module C = Cic in let module U = UriManager in let module R = CicReduction in - match (R.whd context c, R.whd context p, rl) with + match (R.whd ~subst context c, R.whd ~subst context p, rl) with (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) -> (* we are sure that the two sources are convertible because we *) (* have just checked this. So let's go along ... *) @@ -606,7 +606,7 @@ and get_new_safes context p c rl safes n nn x = let safes'' = if b then 1::safes' else safes' in - get_new_safes ((Some (name,(C.Decl so)))::context) + get_new_safes ~subst ((Some (name,(C.Decl so)))::context) ta2 ta1 tl safes'' (n+1) (nn+1) (x+1) | (C.Prod _, (C.MutConstruct _ as e), _) | (C.Prod _, (C.Rel _ as e), _) @@ -623,30 +623,30 @@ and get_new_safes context p c rl safes n nn x = (Printf.sprintf "Get New Safes: c=%s ; p=%s" (CicPp.ppterm c) (CicPp.ppterm p))) -and split_prods context n te = +and split_prods ?(subst = []) context n te = let module C = Cic in let module R = CicReduction in match (n, R.whd context te) with (0, _) -> context,te | (n, C.Prod (name,so,ta)) when n > 0 -> - split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta + split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta | (_, _) -> raise (AssertFailure "8") -and eat_lambdas context n te = +and eat_lambdas ?(subst = []) context n te = let module C = Cic in let module R = CicReduction in - match (n, R.whd context te) with + match (n, R.whd ~subst context te) with (0, _) -> (te, 0, context) | (n, C.Lambda (name,so,ta)) when n > 0 -> let (te, k, context') = - eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta + eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta in (te, k + 1, context') | (n, te) -> raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te))) -(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) -and check_is_really_smaller_arg context n nn kl x safes te = +(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) +and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = (*CSC: forse la whd si puo' fare solo quando serve veramente. *) (*CSC: cfr guarded_by_destructors *) let module C = Cic in @@ -660,25 +660,25 @@ and check_is_really_smaller_arg context n nn kl x safes te = | C.Implicit _ | C.Cast _ (* | C.Cast (te,ty) -> - check_is_really_smaller_arg n nn kl x safes te && - check_is_really_smaller_arg n nn kl x safes ty*) + check_is_really_smaller_arg ~subst n nn kl x safes te && + check_is_really_smaller_arg ~subst n nn kl x safes ty*) (* | C.Prod (_,so,ta) -> - check_is_really_smaller_arg n nn kl x safes so && - check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) + check_is_really_smaller_arg ~subst n nn kl x safes so && + check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta*) | C.Prod _ -> raise (AssertFailure "10") | C.Lambda (name,so,ta) -> - check_is_really_smaller_arg context n nn kl x safes so && - check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context) + check_is_really_smaller_arg ~subst context n nn kl x safes so && + check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.LetIn (name,so,ta) -> - check_is_really_smaller_arg context n nn kl x safes so && - check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context) + check_is_really_smaller_arg ~subst context n nn kl x safes so && + check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl (he::_) -> (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) (*CSC: solo perche' non abbiamo trovato controesempi *) - check_is_really_smaller_arg context n nn kl x safes he + check_is_really_smaller_arg ~subst context n nn kl x safes he | C.Appl [] -> raise (AssertFailure "11") | C.Const _ | C.MutInd _ -> raise (AssertFailure "12") @@ -697,7 +697,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = let cl' = List.map (fun (id,ty) -> - (id, snd (split_prods tys paramsno ty))) cl + (id, snd (split_prods ~subst tys paramsno ty))) cl in (tys,List.length tl,isinductive,paramsno,cl') | _ -> @@ -708,7 +708,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = if not isinductive then List.fold_right (fun p i -> - i && check_is_really_smaller_arg context n nn kl x safes p) + i && check_is_really_smaller_arg ~subst context n nn kl x safes p) pl true else List.fold_right @@ -718,10 +718,10 @@ and check_is_really_smaller_arg context n nn kl x safes te = recursive_args tys 0 len debrujinedte in let (e,safes',n',nn',x',context') = - get_new_safes context p c rl' safes n nn x + get_new_safes ~subst context p c rl' safes n nn x in i && - check_is_really_smaller_arg context' n' nn' kl x' safes' e + check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e ) (List.combine pl cl) true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = @@ -735,7 +735,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = let cl' = List.map (fun (id,ty) -> - (id, snd (split_prods tys paramsno ty))) cl + (id, snd (split_prods ~subst tys paramsno ty))) cl in (tys,List.length tl,isinductive,paramsno,cl') | _ -> @@ -746,7 +746,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = if not isinductive then List.fold_right (fun p i -> - i && check_is_really_smaller_arg context n nn kl x safes p) + i && check_is_really_smaller_arg ~subst context n nn kl x safes p) pl true else (*CSC: supponiamo come prima che nessun controllo sia necessario*) @@ -761,12 +761,12 @@ and check_is_really_smaller_arg context n nn kl x safes te = get_new_safes context p c rl' safes n nn x in i && - check_is_really_smaller_arg context' n' nn' kl x' safes' e + check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e ) (List.combine pl cl) true | _ -> List.fold_right (fun p i -> - i && check_is_really_smaller_arg context n nn kl x safes p + i && check_is_really_smaller_arg ~subst context n nn kl x safes p ) pl true ) | C.Fix (_, fl) -> @@ -779,7 +779,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = List.fold_right (fun (_,_,ty,bo) i -> i && - check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl + check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo ) fl true | C.CoFix (_, fl) -> @@ -792,11 +792,11 @@ and check_is_really_smaller_arg context n nn kl x safes te = List.fold_right (fun (_,ty,bo) i -> i && - check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl + check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo ) fl true -and guarded_by_destructors context n nn kl x safes = +and guarded_by_destructors ?(subst = []) context n nn kl x safes = let module C = Cic in let module U = UriManager in function @@ -835,7 +835,7 @@ and guarded_by_destructors context n nn kl x safes = (fun param i -> i && guarded_by_destructors context n nn kl x safes param ) tl true && - check_is_really_smaller_arg context n nn kl x safes (List.nth tl k) + check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k) | C.Appl tl -> List.fold_right (fun t i -> i && guarded_by_destructors context n nn kl x safes t) @@ -863,8 +863,8 @@ and guarded_by_destructors context n nn kl x safes = List.map (fun (id,ty) -> let debrujinedty = debrujin_constructor uri len ty in - (id, snd (split_prods tys paramsno ty), - snd (split_prods tys paramsno debrujinedty) + (id, snd (split_prods ~subst tys paramsno ty), + snd (split_prods ~subst tys paramsno debrujinedty) )) cl in (tys,len,isinductive,paramsno,cl') @@ -905,7 +905,7 @@ and guarded_by_destructors context n nn kl x safes = let cl' = List.map (fun (id,ty) -> - (id, snd (split_prods tys paramsno ty))) cl + (id, snd (split_prods ~subst tys paramsno ty))) cl in (tys,List.length tl,isinductive,paramsno,cl') | _ -> @@ -1299,11 +1299,11 @@ and type_of_branch context argsno need_dummy outtype term constype = metavariable is consitent - up to relocation via the relocation list l - with the actual context *) -and check_metasenv_consistency metasenv context canonical_context l = +and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in - let lifted_canonical_context = + let lifted_canonical_context = let rec aux i = function [] -> [] @@ -1315,30 +1315,41 @@ and check_metasenv_consistency metasenv context canonical_context l = | (Some (n,C.Def (t,Some ty)))::tl -> (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl) in - aux 1 canonical_context + aux 1 canonical_context in List.iter2 (fun t ct -> match (t,ct) with | _,None -> () | Some t,Some (_,C.Def (ct,_)) -> - if not (R.are_convertible context t ct) then + if not (R.are_convertible ~subst ~metasenv context t ct) then raise (TypeCheckerFailure (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t))) | Some t,Some (_,C.Decl ct) -> - let type_t = type_of_aux' metasenv context t in - if not (R.are_convertible context type_t ct) then + let type_t = type_of_aux' ~subst metasenv context t in + if not (R.are_convertible ~subst ~metasenv context type_t ct) then + (* debug *) + ( + (* + (match type_t with + Cic.Meta (n,l) -> + try + let (cc, ecco) = CicUtil.lookup_subst n subst in + prerr_endline (CicPp.ppterm ecco) + with CicUtil.Subst_not_found _ -> + prerr_endline "Non lo trovo" + | _ -> ()); *) raise (TypeCheckerFailure (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" - (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t))) + (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))) | None, _ -> raise (TypeCheckerFailure "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated") ) l lifted_canonical_context (* type_of_aux' is just another name (with a different scope) for type_of_aux *) -and type_of_aux' metasenv context t = +and type_of_aux' ?(subst = []) metasenv context t = let rec type_of_aux context = let module C = Cic in let module R = CicReduction in @@ -1360,16 +1371,23 @@ and type_of_aux' metasenv context t = ) | C.Var (uri,exp_named_subst) -> incr fdebug ; - check_exp_named_subst context exp_named_subst ; + check_exp_named_subst ~subst context exp_named_subst ; let ty = CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) in decr fdebug ; ty | C.Meta (n,l) -> - let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in - check_metasenv_consistency metasenv context canonical_context l; - CicSubstitution.lift_meta l ty + (try + let (canonical_context, term) = CicUtil.lookup_subst n subst in + check_metasenv_consistency + ~subst metasenv context canonical_context l; + type_of_aux context (CicSubstitution.lift_meta l term) + with CicUtil.Subst_not_found _ -> + let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in + check_metasenv_consistency + ~subst metasenv context canonical_context l; + CicSubstitution.lift_meta l ty) (* TASSI: CONSTRAINTS *) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in @@ -1382,7 +1400,7 @@ and type_of_aux' metasenv context t = | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) as t -> let _ = type_of_aux context ty in - if R.are_convertible context (type_of_aux context te) ty then + if R.are_convertible ~subst ~metasenv context (type_of_aux context te) ty then ty else raise (TypeCheckerFailure @@ -1390,11 +1408,11 @@ and type_of_aux' metasenv context t = | C.Prod (name,s,t) -> let sort1 = type_of_aux context s and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in - let res = sort_of_prod context (name,s) (sort1,sort2) in + let res = sort_of_prod ~subst context (name,s) (sort1,sort2) in res | C.Lambda (n,s,t) -> let sort1 = type_of_aux context s in - (match R.whd context sort1 with + (match R.whd ~subst context sort1 with C.Meta _ | C.Sort _ -> () | _ -> @@ -1426,11 +1444,11 @@ and type_of_aux' metasenv context t = | C.Appl (he::tl) when List.length tl > 0 -> let hetype = type_of_aux context he in let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in - eat_prods context hetype tlbody_and_type + eat_prods ~subst context hetype tlbody_and_type | C.Appl _ -> raise (AssertFailure "Appl: no arguments") | C.Const (uri,exp_named_subst) -> incr fdebug ; - check_exp_named_subst context exp_named_subst ; + check_exp_named_subst ~subst context exp_named_subst ; let cty = CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) in @@ -1438,7 +1456,7 @@ and type_of_aux' metasenv context t = cty | C.MutInd (uri,i,exp_named_subst) -> incr fdebug ; - check_exp_named_subst context exp_named_subst ; + check_exp_named_subst ~subst context exp_named_subst ; let cty = CicSubstitution.subst_vars exp_named_subst (type_of_mutual_inductive_defs uri i) @@ -1446,7 +1464,7 @@ and type_of_aux' metasenv context t = decr fdebug ; cty | C.MutConstruct (uri,i,j,exp_named_subst) -> - check_exp_named_subst context exp_named_subst ; + check_exp_named_subst ~subst context exp_named_subst ; let cty = CicSubstitution.subst_vars exp_named_subst (type_of_mutual_inductive_constr uri i j) @@ -1455,219 +1473,212 @@ and type_of_aux' metasenv context t = | C.MutCase (uri,i,outtype,term,pl) -> let outsort = type_of_aux context outtype in let (need_dummy, k) = - let rec guess_args context t = - let outtype = CicReduction.whd context t in - match outtype with - C.Sort _ -> (true, 0) - | C.Prod (name, s, t) -> - let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in - if n = 0 then - (* last prod before sort *) - match CicReduction.whd context s with + let rec guess_args context t = + let outtype = CicReduction.whd ~subst context t in + match outtype with + C.Sort _ -> (true, 0) + | C.Prod (name, s, t) -> + let (b, n) = + guess_args ((Some (name,(C.Decl s)))::context) t in + if n = 0 then + (* last prod before sort *) + match CicReduction.whd ~subst context s with (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> - (false, 1) + C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> + (false, 1) (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - | C.Appl ((C.MutInd (uri',i',_)) :: _) - when U.eq uri' uri && i' = i -> (false, 1) - | _ -> (true, 1) - else - (b, n + 1) - | _ -> - raise (TypeCheckerFailure (sprintf - "Malformed case analasys' output type %s" (CicPp.ppterm outtype))) - in - (*CSC whd non serve dopo type_of_aux ? *) - let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) + | C.Appl ((C.MutInd (uri',i',_)) :: _) + when U.eq uri' uri && i' = i -> (false, 1) + | _ -> (true, 1) + else + (b, n + 1) + | _ -> + raise + (TypeCheckerFailure + (sprintf + "Malformed case analasys' output type %s" + (CicPp.ppterm outtype))) in + let (b, k) = guess_args context outsort in + if not b then (b, k - 1) else (b, k) in let (parameters, arguments, exp_named_subst) = - match R.whd context (type_of_aux context term) with - (*CSC manca il caso dei CAST *) -(*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *) -(*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *) -(*CSC: Hint: nella DTD servono per gli stylesheet. *) - C.MutInd (uri',i',exp_named_subst) as typ -> - if U.eq uri uri' && i = i' then ([],[],exp_named_subst) - else raise (TypeCheckerFailure (sprintf - "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}" - (CicPp.ppterm typ) (U.string_of_uri uri) i)) - | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> - if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in params,args,exp_named_subst - else raise (TypeCheckerFailure (sprintf - "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}" - (CicPp.ppterm typ') (U.string_of_uri uri) i)) - | _ -> - raise (TypeCheckerFailure (sprintf - "Case analysis: analysed term %s is not an inductive one" - (CicPp.ppterm term))) + match R.whd ~subst context (type_of_aux context term) with + C.MutInd (uri',i',exp_named_subst) as typ -> + if U.eq uri uri' && i = i' then ([],[],exp_named_subst) + else raise + (TypeCheckerFailure + (sprintf + "Case analysys: analysed term type is %s, + but is expected to be (an application of) %s#1/%d{_}" + (CicPp.ppterm typ) (U.string_of_uri uri) i)) + | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> + if U.eq uri uri' && i = i' then + let params,args = + split tl (List.length tl - k) + in params,args,exp_named_subst + else raise + (TypeCheckerFailure + (sprintf + "Case analysys: analysed term type is %s, + but is expected to be (an application of) %s#1/%d{_}" + (CicPp.ppterm typ') (U.string_of_uri uri) i)) + | _ -> + raise + (TypeCheckerFailure + (sprintf + "Case analysis: analysed term %s is not an inductive one" + (CicPp.ppterm term))) in - (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) - let sort_of_ind_type = + (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) + let sort_of_ind_type = if parameters = [] then - C.MutInd (uri,i,exp_named_subst) + C.MutInd (uri,i,exp_named_subst) else - C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) - in - if not (check_allowed_sort_elimination context uri i need_dummy - sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort) - then - raise + C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in + if not + (check_allowed_sort_elimination context uri i need_dummy + sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort) + then + raise (TypeCheckerFailure ("Case analasys: sort elimination not allowed")); (* let's check if the type of branches are right *) - let parsno = - match CicEnvironment.get_cooked_obj ~trust:false uri with + let parsno = + match CicEnvironment.get_cooked_obj ~trust:false uri with C.InductiveDefinition (_,_,parsno) -> parsno | _ -> raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) - in - let (_,branches_ok) = - List.fold_left - (fun (j,b) p -> + UriManager.string_of_uri uri)) + in + let (_,branches_ok) = + List.fold_left + (fun (j,b) p -> let cons = - if parameters = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) - in -(* - (j + 1, b && -*) - (j + 1, -let res = b && - R.are_convertible context (type_of_aux context p) - (type_of_branch context parsno need_dummy outtype cons - (type_of_aux context cons)) -in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res - ) - ) (1,true) pl - in - if not branches_ok then - raise - (TypeCheckerFailure "Case analysys: wrong branch type"); - if not need_dummy then - C.Appl ((outtype::arguments)@[term]) - else if arguments = [] then - outtype - else - C.Appl (outtype::arguments) + if parameters = [] then + (C.MutConstruct (uri,i,j,exp_named_subst)) + else + (C.Appl + (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in + (j + 1, + let res = + b && + R.are_convertible + ~subst ~metasenv context (type_of_aux context p) + (type_of_branch context parsno need_dummy outtype cons + (type_of_aux context cons)) in + if not res then + debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res + ) + ) (1,true) pl + in + if not branches_ok then + raise + (TypeCheckerFailure "Case analysys: wrong branch type"); + if not need_dummy then + C.Appl ((outtype::arguments)@[term]) + else if arguments = [] then + outtype + else + C.Appl (outtype::arguments) | C.Fix (i,fl) -> - let types_times_kl = + let types_times_kl = List.rev - (List.map - (fun (n,k,ty,_) -> - let _ = type_of_aux context ty in - (Some (C.Name n,(C.Decl ty)),k)) fl) - in - let (types,kl) = List.split types_times_kl in + (List.map + (fun (n,k,ty,_) -> + let _ = type_of_aux context ty in + (Some (C.Name n,(C.Decl ty)),k)) fl) + in + let (types,kl) = List.split types_times_kl in let len = List.length types in - List.iter - (fun (name,x,ty,bo) -> - if - (R.are_convertible (types@context) (type_of_aux (types@context) bo) - (CicSubstitution.lift len ty)) - then - begin - let (m, eaten, context') = - eat_lambdas (types @ context) (x + 1) bo - in - (*let's control the guarded by destructors conditions D{f,k,x,M}*) + List.iter + (fun (name,x,ty,bo) -> if - not - (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m) + (R.are_convertible + ~subst ~metasenv (types@context) (type_of_aux (types@context) bo) + (CicSubstitution.lift len ty)) then - raise - (TypeCheckerFailure ("Fix: not guarded by destructors")) - end - else - raise (TypeCheckerFailure ("Fix: ill-typed bodies")) - ) fl ; - + begin + let (m, eaten, context') = + eat_lambdas ~subst (types @ context) (x + 1) bo in + (*let's control the guarded by destructors conditions D{f,k,x,M}*) + if + not (guarded_by_destructors context' + eaten (len + eaten) kl 1 [] m) + then + raise + (TypeCheckerFailure ("Fix: not guarded by destructors")) + end + else + raise (TypeCheckerFailure ("Fix: ill-typed bodies")) + ) fl ; (*CSC: controlli mancanti solo su D{f,k,x,M} *) - let (_,_,ty,_) = List.nth fl i in - ty + let (_,_,ty,_) = List.nth fl i in + ty | C.CoFix (i,fl) -> - let types = + let types = List.rev (List.map (fun (n,ty,_) -> let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl) - in + in let len = List.length types in - List.iter + List.iter (fun (_,ty,bo) -> - if - (R.are_convertible (types @ context) - (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty)) - then - begin - (* let's control that the returned type is coinductive *) - match returns_a_coinductive context ty with - None -> - raise - (TypeCheckerFailure - ("CoFix: does not return a coinductive type")) - | Some uri -> - (*let's control the guarded by constructors conditions C{f,M}*) - if - not - (guarded_by_constructors (types @ context) 0 len false bo - [] uri) - then - raise - (TypeCheckerFailure ("CoFix: not guarded by constructors")) - end - else - raise - (TypeCheckerFailure ("CoFix: ill-typed bodies")) + if + (R.are_convertible + ~subst ~metasenv (types @ context) + (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty)) + then + begin + (* let's control that the returned type is coinductive *) + match returns_a_coinductive context ty with + None -> + raise + (TypeCheckerFailure + ("CoFix: does not return a coinductive type")) + | Some uri -> + (*let's control the guarded by constructors conditions C{f,M}*) + if + not + (guarded_by_constructors + (types @ context) 0 len false bo [] uri) + then + raise + (TypeCheckerFailure ("CoFix: not guarded by constructors")) + end + else + raise + (TypeCheckerFailure ("CoFix: ill-typed bodies")) ) fl ; - - let (_,ty,_) = List.nth fl i in + let (_,ty,_) = List.nth fl i in ty - and check_exp_named_subst context = - let rec check_exp_named_subst_aux substs = + and check_exp_named_subst ?(subst = []) context = + let rec check_exp_named_subst_aux esubsts = function [] -> () - | ((uri,t) as subst)::tl -> + | ((uri,t) as item)::tl -> let typeofvar = - CicSubstitution.subst_vars substs (type_of_variable uri) in -(* CSC: this test should not exist - (match CicEnvironment.get_cooked_obj ~trust:false uri with - Cic.Variable (_,Some bo,_,_) -> - raise - (TypeCheckerFailure - ("A variable with a body can not be explicit substituted")) - | Cic.Variable (_,None,_,_) -> () - | _ -> - raise (TypeCheckerFailure - ("Unknown variable definition:" ^ - UriManager.string_of_uri uri)) - ) ; -*) + CicSubstitution.subst_vars esubsts (type_of_variable uri) in let typeoft = type_of_aux context t in - if CicReduction.are_convertible context typeoft typeofvar then - check_exp_named_subst_aux (substs@[subst]) tl - else + if CicReduction.are_convertible + ~subst ~metasenv context typeoft typeofvar then + check_exp_named_subst_aux (esubsts@[item]) tl + else begin - CicReduction.fdebug := 0 ; - ignore (CicReduction.are_convertible context typeoft typeofvar) ; - fdebug := 0 ; - debug typeoft [typeofvar] ; - raise (TypeCheckerFailure "Wrong Explicit Named Substitution") + CicReduction.fdebug := 0 ; + ignore (CicReduction.are_convertible ~subst ~metasenv context typeoft typeofvar) ; + fdebug := 0 ; + debug typeoft [typeofvar] ; + raise (TypeCheckerFailure "Wrong Explicit Named Substitution") end in check_exp_named_subst_aux [] - and sort_of_prod context (name,s) (t1, t2) = + and sort_of_prod ?(subst = []) context (name,s) (t1, t2) = let module C = Cic in - let t1' = CicReduction.whd context t1 in - let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in + let t1' = CicReduction.whd ~subst context t1 in + let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in match (t1', t2') with (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> @@ -1690,22 +1701,22 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1') (CicPp.ppterm t2'))) - and eat_prods context hetype = + and eat_prods ?(subst = []) context hetype = (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) (*CSC: cucinati *) function [] -> hetype | (hete, hety)::tl -> - (match (CicReduction.whd context hetype) with + (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,t) -> - if CicReduction.are_convertible context hety s then + if CicReduction.are_convertible ~subst ~metasenv context hety s then (CicReduction.fdebug := -1 ; - eat_prods context (CicSubstitution.subst hete t) tl + eat_prods ~subst context (CicSubstitution.subst hete t) tl ) else begin CicReduction.fdebug := 0 ; - ignore (CicReduction.are_convertible context s hety) ; + ignore (CicReduction.are_convertible ~subst ~metasenv context s hety) ; fdebug := 0 ; debug s [hety] ; raise (TypeCheckerFailure (sprintf diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 3973c16c1..5f7e3ae97 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -33,7 +33,7 @@ val typecheck : UriManager.uri -> Cic.obj (* type_of_aux' metasenv context term *) val type_of_aux': - Cic.metasenv -> Cic.context -> Cic.term -> Cic.term + ?subst:Cic.substitution -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term (* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *) val typecheck_mutual_inductive_defs : diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 387c747f6..b594e009e 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2004, HELM Team. +(* Copyright (C) 2003, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -80,6 +80,77 @@ let lookup_subst n subst = List.assoc n subst with Not_found -> raise (SubstNotFound n) +(* 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 SubstNotFound _ -> + 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 = @@ -219,14 +290,6 @@ let apply_subst_metasenv subst metasenv = (***** Pretty printing functions ******) -let ppsubst subst = - String.concat "\n" - (List.map - (fun (idx, (_, term)) -> - Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) - subst) -;; - let ppterm subst term = CicPp.ppterm (apply_subst subst term) let ppterm_in_context subst term name_context = @@ -250,6 +313,29 @@ let ppcontext' ?(sep = "\n") subst context = sprintf "%s_ :? _" (separate i), None::name_context ) context ("",[]) +let ppsubst_unfolded subst = + String.concat "\n" + (List.map + (fun (idx, (c, t)) -> + let context,name_context = ppcontext' ~sep:"; " subst c in + sprintf "%s |- ?%d:= %s" context idx + (ppterm_in_context subst t name_context)) + subst) +(* + Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) + subst) *) +;; + +let ppsubst subst = + String.concat "\n" + (List.map + (fun (idx, (c, t)) -> + let context,name_context = ppcontext' ~sep:"; " [] c in + sprintf "%s |- ?%d:= %s" context idx + (ppterm_in_context [] t name_context)) + subst) +;; + let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context) let ppmetasenv ?(sep = "\n") metasenv subst = @@ -307,6 +393,7 @@ let tempi_type_of_aux = ref 0.0;; (* assumption: metasenv is already instantiated wrt subst *) let type_of_aux' metasenv subst context term = let time1 = Unix.gettimeofday () in +(* let term = clean_up_meta subst metasenv term in *) let term = apply_subst subst term in let context = apply_subst_context subst context in (* let metasenv = apply_subst_metasenv subst metasenv in *) @@ -431,7 +518,7 @@ let rec restrict subst to_be_restricted metasenv = (List.map (fun i -> try - match List.nth context i with + match List.nth context (i-1) with | None -> assert false | Some (n, _) -> CicPp.ppname n with @@ -512,12 +599,12 @@ let rec restrict subst to_be_restricted metasenv = with Occur -> raise (MetaSubstFailure (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)))) + n (names_of_context_indexes context to_be_restricted)))) metasenv ([], []) in let (more_to_be_restricted', subst) = (* restrict subst *) List.fold_right - (fun (n, (context, term)) (more, subst) -> + (fun (n, (context, term)) (more, subst') -> let to_be_restricted = List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) in @@ -532,14 +619,21 @@ let rec restrict subst to_be_restricted metasenv = let more_to_be_restricted', term' = force_does_not_occur subst restricted term in - let subst' = (n, (context', term')) :: subst in + let subst' = (n, (context', term')) :: subst' in let more = more @ more_to_be_restricted @ more_to_be_restricted' in (more, subst') with Occur -> - raise (MetaSubstFailure (sprintf + let error_msg = 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 subst term))))) + (ppterm subst term) + in + (* DEBUG + prerr_endline error_msg; + prerr_endline ("metasenv = \n" ^ (ppmetasenv metasenv subst)); + prerr_endline ("subst = \n" ^ (ppsubst subst)); + prerr_endline ("context = \n" ^ (ppcontext subst context)); *) + raise (MetaSubstFailure error_msg))) subst ([], []) in match more_to_be_restricted @ more_to_be_restricted' with @@ -547,8 +641,16 @@ let rec restrict subst to_be_restricted metasenv = | l -> restrict subst l metasenv ;; -(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *) +(*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 *) +(* + prerr_endline ("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, _) = CicUtil.lookup_meta n metasenv in @@ -587,11 +689,13 @@ let delift n subst context metasenv l t = in C.Var (uri,exp_named_subst') | C.Meta (i, l1) as t -> - if i = n then + (* see the top level invariant *) + if (i = n) then raise (MetaSubstFailure (sprintf "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" - i (ppterm subst t))) + i (ppterm 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 = @@ -605,10 +709,11 @@ let delift n subst context metasenv l t = with NotInTheList | MetaSubstFailure _ -> - to_be_restricted := (i,j)::!to_be_restricted ; None::l1' + to_be_restricted := (i,j)::!to_be_restricted ; None::l1' in - let l' = deliftl 1 l1 in - C.Meta(i,l') + 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) @@ -661,7 +766,14 @@ let delift n subst context metasenv l t = (* 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 "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ; +(* debug_print "First Order UnificationFailure during delift" ; +prerr_endline(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 + ))); *) raise (Uncertain (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 14d6da3f6..6ebd5a5b9 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -31,7 +31,7 @@ exception SubstNotFound of int (* The entry (i,t) in a substitution means that *) (* (META i) have been instantiated with t. *) -type substitution = (int * (Cic.context * Cic.term)) list +type substitution = (int * (Cic.context * Cic.term)) list (** @raise SubstNotFound *) val lookup_subst: int -> substitution -> Cic.context * Cic.term @@ -66,9 +66,12 @@ val delift : int -> substitution -> Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv * substitution - +val restrict : + substitution -> (int * int) list -> Cic.metasenv -> + Cic.metasenv * substitution (** {2 Pretty printers} *) +val ppsubst_unfolded: substitution -> string val ppsubst: substitution -> string val ppterm: substitution -> Cic.term -> string val ppcontext: ?sep: string -> substitution -> Cic.context -> string @@ -92,3 +95,6 @@ val print_counters: unit -> unit val reset_counters: unit -> unit *) +(* val clean_up_meta : + substitution -> Cic.metasenv -> Cic.term -> Cic.term +*) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 748307013..b6aa1df41 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -51,6 +51,10 @@ let new_meta metasenv subst = in 1 + aux (None, indexes) +(* let apply_subst_context = CicMetaSubst.apply_subst_context;; *) +(* questa o la precedente sembrano essere equivalenti come tempi *) +let apply_subst_context _ context = context ;; + let mk_implicit metasenv subst context = let newmeta = new_meta metasenv subst in let newuniv = CicUniv.fresh () in @@ -58,7 +62,7 @@ let mk_implicit metasenv subst context = (* in the following mk_* functions we apply substitution to canonical * context since we have the invariant that the metasenv has already been * instantiated with subst *) - let context = CicMetaSubst.apply_subst_context subst context in + let context = apply_subst_context subst context in ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ; (* TASSI: ?? *) newmeta + 1, context, Cic.Meta (newmeta, []); @@ -68,7 +72,7 @@ let mk_implicit metasenv subst context = let mk_implicit_type metasenv subst context = let newmeta = new_meta metasenv subst in let newuniv = CicUniv.fresh () in - let context = CicMetaSubst.apply_subst_context subst context in + let context = apply_subst_context subst context in ([ newmeta, [], Cic.Sort (Cic.Type newuniv); (* TASSI: ?? *) newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv, @@ -84,7 +88,7 @@ let n_fresh_metas metasenv subst context n = if n = 0 then metasenv, [] else let irl = identity_relocation_list_for_metavariable context in - let context = CicMetaSubst.apply_subst_context subst context in + let context = apply_subst_context subst context in let newmeta = new_meta metasenv subst in let newuniv = CicUniv.fresh () in let rec aux newmeta n = @@ -100,7 +104,7 @@ let n_fresh_metas metasenv subst context n = let fresh_subst metasenv subst context uris = let irl = identity_relocation_list_for_metavariable context in - let context = CicMetaSubst.apply_subst_context subst context in + let context = apply_subst_context subst context in let newmeta = new_meta metasenv subst in let newuniv = CicUniv.fresh () in let rec aux newmeta = function diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index c1b70df8d..7b3e4179c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -107,8 +107,9 @@ and type_of_mutual_inductive_constr uri i j = and check_branch n context metasenv subst left_args_no actualtype term expectedtype = let module C = Cic in - let module R = CicMetaSubst in - match R.whd subst context expectedtype with + (* let module R = CicMetaSubst in *) + let module R = CicReduction in + match R.whd ~subst context expectedtype with C.MutInd (_,_,_) -> (n,context,actualtype, [term]), subst, metasenv | C.Appl (C.MutInd (_,_,_)::tl) -> @@ -117,7 +118,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | C.Prod (name,so,de) -> (* we expect that the actual type of the branch has the due number of Prod *) - (match R.whd subst context actualtype with + (match R.whd ~subst context actualtype with C.Prod (name',so',de') -> let subst, metasenv = fo_unif_subst subst context metasenv so so' in @@ -158,13 +159,13 @@ and type_of_aux' metasenv context t = ty,subst',metasenv' | C.Meta (n,l) -> (try - let (canonical_context, term) = CicMetaSubst.lookup_subst n subst in + let (canonical_context, term) = CicUtil.lookup_subst n subst in let subst,metasenv = check_metasenv_consistency n subst metasenv context canonical_context l in type_of_aux subst metasenv context (CicSubstitution.lift_meta l term) - with CicMetaSubst.SubstNotFound _ -> + with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let subst,metasenv = check_metasenv_consistency n subst metasenv context @@ -202,7 +203,7 @@ and type_of_aux' metasenv context t = sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) | C.Lambda (n,s,t) -> let sort1,subst',metasenv' = type_of_aux subst metasenv context s in - (match CicMetaSubst.whd subst' context sort1 with + (match CicReduction.whd ~subst:subst' context sort1 with C.Meta _ | C.Sort _ -> () | _ -> @@ -271,7 +272,7 @@ and type_of_aux' metasenv context t = (RefineFailure ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in let rec count_prod t = - match CicMetaSubst.whd subst context t with + match CicReduction.whd ~subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in let no_args = count_prod arity in @@ -296,7 +297,7 @@ and type_of_aux' metasenv context t = let _, subst, metasenv = type_of_aux subst metasenv context expected_type in - let actual_type = CicMetaSubst.whd subst context actual_type in + let actual_type = CicReduction.whd ~subst context actual_type in let subst,metasenv = fo_unif_subst subst context metasenv expected_type actual_type in @@ -347,11 +348,21 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context appl in *) - CicMetaSubst.whd subst context appl + (* DEBUG + let prova1 = CicMetaSubst.whd subst context appl in + let prova2 = CicReduction.whd ~subst context appl in + if not (prova1 = prova2) then + begin + prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1)); + prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2)); + end; + *) + (* CicMetaSubst.whd subst context appl *) + CicReduction.whd ~subst context appl in fo_unif_subst subst context metasenv instance instance') (subst,metasenv) outtypeinstances in - CicMetaSubst.whd subst + CicReduction.whd ~subst context (C.Appl(outtype::right_args@[term])),subst,metasenv | C.Fix (i,fl) -> let subst,metasenv,types = @@ -370,7 +381,7 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context' bo in fo_unif_subst subst context' metasenv - ty_of_bo (CicMetaSubst.lift subst len ty) + ty_of_bo (CicSubstitution.lift len ty) ) (subst,metasenv) fl in let (_,_,ty,_) = List.nth fl i in ty,subst,metasenv @@ -391,7 +402,7 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context' bo in fo_unif_subst subst context' metasenv - ty_of_bo (CicMetaSubst.lift subst len ty) + ty_of_bo (CicSubstitution.lift len ty) ) (subst,metasenv) fl in let (_,ty,_) = List.nth fl i in @@ -420,7 +431,7 @@ and type_of_aux' metasenv context t = C.Def ((S.lift_meta l (S.lift i t)), Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl) in - aux 1 canonical_context + aux 1 canonical_context in try List.fold_left2 @@ -493,8 +504,8 @@ and type_of_aux' metasenv context t = and sort_of_prod subst metasenv context (name,s) (t1, t2) = let module C = Cic in let context_for_t2 = (Some (name,C.Decl s))::context in - let t1'' = CicMetaSubst.whd subst context t1 in - let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in + let t1'' = CicReduction.whd ~subst context t1 in + let t2'' = CicReduction.whd ~subst context_for_t2 t2 in match (t1'', t2'') with (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) @@ -548,21 +559,22 @@ and type_of_aux' metasenv context t = (* Thus I generate a name (name_hint) in context and *) (* then I generate a name --- using the hint name_hint *) (* --- that is fresh in (context'@context). *) - let name_hint = - FreshNamesGenerator.mk_fresh_name metasenv + let name_hint = + (* Cic.Name "pippo" *) + FreshNamesGenerator.mk_fresh_name metasenv (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) (CicMetaSubst.apply_subst_context subst context) Cic.Anonymous - (CicMetaSubst.apply_subst subst argty) + (CicMetaSubst.apply_subst subst argty) in (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) FreshNamesGenerator.mk_fresh_name [] context name_hint (Cic.Sort Cic.Prop) in let metasenv,target = - mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl + mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl in - metasenv,Cic.Prod (name,meta,target) + metasenv,Cic.Prod (name,meta,target) in let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in let (subst, metasenv) = @@ -575,10 +587,31 @@ and type_of_aux' metasenv context t = (match hetype with Cic.Prod (n,s,t) -> let subst,metasenv = - fo_unif_subst subst context metasenv hety s + fo_unif_subst subst context metasenv hety s +(* + try + fo_unif_subst subst context metasenv hety s + with _ -> + prerr_endline("senza subst fallisce"); + let hety = CicMetaSubst.apply_subst subst hety in + let s = CicMetaSubst.apply_subst subst s in + prerr_endline ("unifico = " ^(CicPp.ppterm hety)); + prerr_endline ("con = " ^(CicPp.ppterm s)); + fo_unif_subst subst context metasenv hety s *) in - eat_prods metasenv subst context - (CicMetaSubst.subst subst hete t) tl + (* DEBUG + let t1 = CicMetaSubst.subst subst hete t in + let t2 = CicSubstitution.subst hete t in + prerr_endline ("con subst = " ^(CicPp.ppterm t1)); + prerr_endline ("senza subst = " ^(CicPp.ppterm t2)); + prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^ + (CicMetaSubst.ppmetasenv metasenv subst)); + prerr_endline("++++++++++subst prima di eat_prods:\n" ^ + (CicMetaSubst.ppsubst subst)); + *) + eat_prods metasenv subst context + (* (CicMetaSubst.subst subst hete t) tl *) + (CicSubstitution.subst hete t) tl | _ -> assert false ) in @@ -634,15 +667,20 @@ and type_of_aux' metasenv context t = in aux [] [] (hetype,subst,metasenv) tlbody_and_type *) - in + in let ty,subst',metasenv' = type_of_aux [] metasenv context t in let substituted_t = CicMetaSubst.apply_subst subst' t in let substituted_ty = CicMetaSubst.apply_subst subst' ty in - let substituted_metasenv = metasenv' -(* CicMetaSubst.apply_subst_metasenv subst' metasenv' *) - in +(* Andrea: ho rimesso qui l'applicazione della subst al +metasenv dopo che ho droppato l'invariante che il metsaenv +e' sempre istanziato *) + let substituted_metasenv = + CicMetaSubst.apply_subst_metasenv subst' metasenv' in + (* metasenv' *) +(* substituted_t,substituted_ty,substituted_metasenv *) +(* ANDREA: spostare tutta questa robaccia da un altra parte *) let cleaned_t = FreshNamesGenerator.clean_dummy_dependent_types substituted_t in let cleaned_ty = @@ -672,20 +710,20 @@ and type_of_aux' metasenv context t = (n,context',ty') ) substituted_metasenv in - (cleaned_t,cleaned_ty,cleaned_metasenv) - + (cleaned_t,cleaned_ty,cleaned_metasenv) ;; -(* DEBUGGING ONLY *) + + +(* DEBUGGING ONLY let type_of_aux' metasenv context term = try - let (t,ty,m) = type_of_aux' metasenv context term in - debug_print - ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty); -(* + let (t,ty,m) = + type_of_aux' metasenv context term in + debug_print + ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty); debug_print - ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s); -*) + ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []); (t,ty,m) with | RefineFailure msg as e -> @@ -694,4 +732,4 @@ let type_of_aux' metasenv context term = | Uncertain msg as e -> debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); raise e -;; +;; *) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index e6213d6af..cebbb9e8f 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -32,6 +32,21 @@ exception AssertFailure of string;; let debug_print = prerr_endline let type_of_aux' metasenv subst context term = + try + CicTypeChecker.type_of_aux' ~subst metasenv context term + with + CicTypeChecker.TypeCheckerFailure msg -> + let msg = + (sprintf + "Kernel Type checking error: +%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." + (CicMetaSubst.ppterm subst term) + (CicMetaSubst.ppterm [] term) + (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppmetasenv metasenv subst) + (CicMetaSubst.ppsubst subst) msg) in + raise (AssertFailure msg);; +(* try CicMetaSubst.type_of_aux' metasenv subst context term with @@ -41,7 +56,19 @@ let type_of_aux' metasenv subst context term = "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms" (CicMetaSubst.ppterm subst term) (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv metasenv subst) msg))) + (CicMetaSubst.ppmetasenv metasenv subst) msg))) *) + +let rec deref subst = + function + Cic.Meta(n,l) as t -> + (try + deref subst + (CicSubstitution.lift_meta + l (snd (CicUtil.lookup_subst n subst))) + with + CicUtil.Subst_not_found _ -> t) + | t -> t +;; let rec beta_expand test_equality_only metasenv subst context t arg = let module S = CicSubstitution in @@ -49,8 +76,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg = let rec aux metasenv subst n context t' = try let subst,metasenv = - fo_unif_subst test_equality_only subst context metasenv - (CicSubstitution.lift n arg) t' + fo_unif_subst test_equality_only subst context metasenv + (CicSubstitution.lift n arg) t' in subst,metasenv,C.Rel (1 + n) with @@ -63,24 +90,32 @@ let rec beta_expand test_equality_only metasenv subst context t arg = aux_exp_named_subst metasenv subst n context exp_named_subst in subst,metasenv,C.Var (uri,exp_named_subst') - | C.Meta (i,l) as t-> - (try - let (_, t') = CicMetaSubst.lookup_subst i subst in - aux metasenv subst n context (CicSubstitution.lift_meta l t') - with CicMetaSubst.SubstNotFound _ -> - let (subst, metasenv, context, local_context) = - List.fold_left - (fun (subst, metasenv, context, local_context) t -> - match t with + | 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) + (* + let (subst, metasenv, context, local_context) = + List.fold_right + (fun t (subst, metasenv, context, local_context) -> + match t with | None -> (subst, metasenv, context, None :: local_context) | Some t -> let (subst, metasenv, t) = aux metasenv subst n context t in - (subst, metasenv, context, Some t :: local_context)) - (subst, metasenv, context, []) l - in - (subst, metasenv, C.Meta (i, local_context))) + (subst, metasenv, context, Some t :: local_context)) + l (subst, metasenv, context, []) + in + prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context)))); + (subst, metasenv, C.Meta (i, local_context)) *) | C.Sort _ | C.Implicit _ as t -> subst,metasenv,t | C.Cast (te,ty) -> @@ -149,7 +184,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg = fl in C.Fix (i, substitutedfl) -*) subst,metasenv,CicMetaSubst.lift subst 1 t' +*) (* subst,metasenv,CicMetaSubst.lift subst 1 t' *) + subst,metasenv,CicSubstitution.lift 1 t' | C.CoFix (i,fl) -> (*CSC: not implemented let tylen = List.length fl in @@ -159,7 +195,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg = fl in C.CoFix (i, substitutedfl) -*) subst,metasenv,CicMetaSubst.lift subst 1 t' +*) (* subst,metasenv,CicMetasubst.lift subst 1 t' *) + subst,metasenv,CicSubstitution.lift 1 t' and aux_exp_named_subst metasenv subst n context ens = List.fold_right @@ -173,13 +210,21 @@ let rec beta_expand test_equality_only metasenv subst context t arg = metasenv context (Cic.Name "Heta") ~typ:argty in let subst,metasenv,t' = aux metasenv subst 0 context t in + (* prova *) + (* old subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg] + *) + subst, metasenv, C.Lambda (fresh_name,argty,t') -and beta_expand_many test_equality_only metasenv subst context t = - List.fold_left - (fun (subst,metasenv,t) arg -> - beta_expand test_equality_only metasenv subst context t arg - ) (subst,metasenv,t) +and beta_expand_many test_equality_only metasenv subst context t args = + let subst,metasenv,hd = + List.fold_right + (fun arg (subst,metasenv,t) -> + let subst,metasenv,t = + beta_expand test_equality_only metasenv subst context t arg in + subst,metasenv,t + ) args (subst,metasenv,t) in + subst,metasenv,hd (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a @@ -192,45 +237,57 @@ and beta_expand_many test_equality_only metasenv subst context t = and fo_unif_subst test_equality_only subst context metasenv t1 t2 = let module C = Cic in - let module R = CicMetaSubst in + let module R = CicReduction in let module S = CicSubstitution in + let t1 = deref subst t1 in + let t2 = deref subst t2 in match (t1, t2) with (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> - let ok,subst,metasenv = - try - List.fold_left2 - (fun (b,subst,metasenv) t1 t2 -> - if b then true,subst,metasenv else - match t1,t2 with - None,_ - | _,None -> true,subst,metasenv - | Some t1', Some t2' -> - (* First possibility: restriction *) - (* Second possibility: unification *) - (* Third possibility: convertibility *) - if R.are_convertible subst context t1' t2' then - true,subst,metasenv - else - (try - let subst,metasenv = - fo_unif_subst - test_equality_only subst context metasenv t1' t2' - in - true,subst,metasenv - with - Not_found -> false,subst,metasenv) - ) (true,subst,metasenv) ln lm - with - Invalid_argument _ -> - raise (UnificationFailure (sprintf - "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) - in - if ok then - subst,metasenv - else - raise (UnificationFailure (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 subst t1) (CicMetaSubst.ppterm subst t2))) + let _,subst,metasenv = + (try + List.fold_left2 + (fun (j,subst,metasenv) t1 t2 -> + match t1,t2 with + None,_ + | _,None -> j+1,subst,metasenv + | Some t1', Some t2' -> + (* First possibility: restriction *) + (* Second possibility: unification *) + (* Third possibility: convertibility *) + if R.are_convertible ~subst ~metasenv context t1' t2' then + j+1,subst,metasenv + else + (try + let subst,metasenv = + fo_unif_subst + test_equality_only + subst context metasenv t1' t2' + in + j+1,subst,metasenv + with + Uncertain _ + | UnificationFailure _ -> +prerr_endline ("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) + ) (1,subst,metasenv) ln lm + with + Exit -> + raise + (UnificationFailure "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 subst t1) (CicMetaSubst.ppterm subst t2))) *) + | Invalid_argument _ -> + raise + (UnificationFailure "2")) +(* + (sprintf + "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))*) + in subst,metasenv | (C.Meta (n,_), C.Meta (m,_)) when n>m -> fo_unif_subst test_equality_only subst context metasenv t2 t1 | (C.Meta (n,l), t) @@ -248,101 +305,88 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = fo_unif_subst test_equality_only subst context metasenv (lower m1 m2) (upper m1 m2) in - begin - try - let (_, oldt) = CicMetaSubst.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in - let ty_lifted_oldt = - type_of_aux' metasenv subst context lifted_oldt - in - let tyt = type_of_aux' metasenv subst context t in - let (subst, metasenv) = - fo_unif_subst_ordered test_equality_only subst context metasenv - tyt ty_lifted_oldt - in - fo_unif_subst_ordered - test_equality_only subst context metasenv t lifted_oldt - with CicMetaSubst.SubstNotFound _ -> - (* First of all we unify the type of the meta with the type of the term *) + begin let subst,metasenv = - let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in - (try - let tyt = type_of_aux' metasenv subst context t in - fo_unif_subst - test_equality_only - subst context metasenv tyt (S.lift_meta l meta_type) - with AssertFailure _ -> - (* 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) - *) -(* -prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN."; -prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; -*) - (subst, metasenv)) - 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'' = - 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 - ignore (CicUniv.add_ge (upper u u') (lower u u')) ; - s - | _ -> t' - in - (* Unifying the types may have already instantiated n. Let's check *) - try - let (_, oldt) = CicMetaSubst.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in - fo_unif_subst_ordered - test_equality_only subst context metasenv t lifted_oldt - with - CicMetaSubst.SubstNotFound _ -> - let (_, context, _) = CicUtil.lookup_meta n metasenv in - let subst = (n, (context, t'')) :: subst in - let metasenv = -(* CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *) - CicMetaSubst.apply_subst_metasenv subst metasenv - in - subst, metasenv -(* (n,t'')::subst, metasenv *) - end + let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in + (try + let tyt = type_of_aux' metasenv subst context t in + fo_unif_subst + test_equality_only + subst context metasenv tyt (S.lift_meta l meta_type) + with + UnificationFailure msg + | Uncertain msg -> + prerr_endline msg;raise (UnificationFailure msg) + | AssertFailure _ -> + prerr_endline "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)) 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'' = + 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 + ignore (CicUniv.add_ge (upper u u') (lower u u')) ; + s + | _ -> t' + 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.lift_meta l oldt in + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt + with + CicUtil.Subst_not_found _ -> + let (_, context, _) = CicUtil.lookup_meta n metasenv in + let subst = (n, (context, t'')) :: subst in + let metasenv = + List.filter (fun (m,_,_) -> not (n = m)) metasenv in + subst, metasenv + 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 else - raise (UnificationFailure (sprintf + raise (UnificationFailure "3") + (* (sprintf "Can't unify %s with %s due to different constants" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm 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 else - raise (UnificationFailure (sprintf + raise (UnificationFailure "4") + (* (sprintf "Can't unify %s with %s due to different inductive principles" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm 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 else - raise (UnificationFailure (sprintf + raise (UnificationFailure "5") + (* (sprintf "Can't unify %s with %s due to different inductive constructors" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only subst context metasenv te t2 @@ -365,31 +409,55 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; fo_unif_subst test_equality_only subst context metasenv t2 (S.subst s1 t1) | (C.Appl l1, C.Appl l2) -> - let subst,metasenv,t1',t2' = - match l1,l2 with - C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j -> - subst,metasenv,t1,t2 - (* In the first two cases when we reach the next begin ... end - section useless work is done since, by construction, the list - of arguments will be equal. - *) + (* andrea: this case should be probably rewritten in the + spirit of deref *) + let rec beta_reduce = + function + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + else + beta_reduce (Cic.Appl(he''::tl')) + | t -> t in + (match l1,l2 with + C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j -> + (try + List.fold_left2 + (fun (subst,metasenv) -> + fo_unif_subst test_equality_only subst context metasenv) + (subst,metasenv) l1 l2 + with (Invalid_argument msg) -> raise (UnificationFailure msg)) | C.Meta (i,l)::args, _ -> - let subst,metasenv,t2' = - beta_expand_many test_equality_only metasenv subst context t2 args - in - subst,metasenv,t1,t2' + (try + let (_,t) = CicUtil.lookup_subst i subst in + let lifted = S.lift_meta l t in + let reduced = beta_reduce (Cic.Appl (lifted::args)) in + fo_unif_subst + test_equality_only + subst context metasenv reduced t2 + with CicUtil.Subst_not_found _ -> + let subst,metasenv,beta_expanded = + beta_expand_many + test_equality_only metasenv subst context t2 args in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded) | _, C.Meta (i,l)::args -> - let subst,metasenv,t1' = - beta_expand_many test_equality_only metasenv subst context t1 args - in - subst,metasenv,t1',t2 + (try + let (_,t) = CicUtil.lookup_subst i subst in + let lifted = S.lift_meta l t in + let reduced = beta_reduce (Cic.Appl (lifted::args)) in + fo_unif_subst + test_equality_only + subst context metasenv t1 reduced + with CicUtil.Subst_not_found _ -> + let subst,metasenv,beta_expanded = + beta_expand_many + test_equality_only metasenv subst context t1 args in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded) | _,_ -> - subst,metasenv,t1,t2 - in - begin - match t1',t2' with - C.Appl l1, C.Appl l2 -> - let lr1 = List.rev l1 in + let lr1 = List.rev l1 in let lr2 = List.rev l2 in let rec fo_unif_l test_equality_only subst metasenv = function @@ -407,9 +475,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; in fo_unif_l test_equality_only subst' metasenv' (l1,l2) in - fo_unif_l test_equality_only subst metasenv (lr1, lr2) - | _ -> assert false - end + fo_unif_l test_equality_only subst metasenv (lr1, lr2) ) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv' = fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in @@ -422,34 +488,38 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; ) (subst'',metasenv'') pl1 pl2 with Invalid_argument _ -> - raise (UnificationFailure (sprintf - "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) + raise (UnificationFailure "6")) + (* (sprintf + "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) *) | (C.Rel _, _) | (_, C.Rel _) -> if t1 = t2 then subst, metasenv else - raise (UnificationFailure (sprintf + raise (UnificationFailure "6") + (* (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) | (C.Sort _ ,_) | (_, C.Sort _) | (C.Const _, _) | (_, C.Const _) | (C.MutInd _, _) | (_, C.MutInd _) | (C.MutConstruct _, _) | (_, C.MutConstruct _) | (C.Fix _, _) | (_, C.Fix _) | (C.CoFix _, _) | (_, C.CoFix _) -> - if t1 = t2 || R.are_convertible subst context t1 t2 then + if t1 = t2 || R.are_convertible ~subst ~metasenv context t1 t2 then subst, metasenv else - raise (UnificationFailure (sprintf + raise (UnificationFailure "7") + (* (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) | (_,_) -> - if R.are_convertible subst context t1 t2 then + if R.are_convertible ~subst ~metasenv context t1 t2 then subst, metasenv else - raise (UnificationFailure (sprintf + raise (UnificationFailure "8") + (* (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 @@ -483,8 +553,8 @@ let fo_unif metasenv context t1 t2 = fo_unif_subst false [] context metasenv t1 t2 ;; let fo_unif_subst subst context metasenv t1 t2 = - let enrich_msg msg = - sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" + let enrich_msg msg = (* "bella roba" *) + sprintf "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 subst t1) (try CicPp.ppterm (type_of_aux' metasenv subst context t1) @@ -494,7 +564,8 @@ let fo_unif_subst subst context metasenv t1 t2 = CicPp.ppterm (type_of_aux' metasenv subst context t2) with _ -> "MALFORMED") (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv metasenv subst) msg + (CicMetaSubst.ppmetasenv metasenv subst) + (CicMetaSubst.ppsubst subst) msg in try fo_unif_subst false subst context metasenv t1 t2 -- 2.39.2