From: Claudio Sacerdoti Coen Date: Wed, 8 May 2002 09:17:24 +0000 (+0000) Subject: Experimental commit: definitions are now allowed in contexts. As a consequence, X-Git-Tag: V_0_3_0_debian_8~108 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=200d1d63cd5fc282df768f97d33214c1572c89da Experimental commit: definitions are now allowed in contexts. As a consequence, CicReduction.whd now requires a context. --- diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index 1861ce5b0..08cb06d9d 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -75,7 +75,9 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts (*CSC: type-inference, but the result is very poort. As a very weak *) (*CSC: patch, I apply whd to the computed type. Full beta *) (*CSC: reduction would be a much better option. *) - let innertype = CicReduction.whd (T.type_of_aux' metasenv cicenv tt) in + let innertype = + CicReduction.whd cicenv (T.type_of_aux' metasenv cicenv tt) + in let innersort = T.type_of_aux' metasenv cicenv innertype in let ainnertype = if computeinnertypes then diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 49510a9dd..47c416d8b 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -582,7 +582,10 @@ let save rendering_window () = match !ProofEngine.proof with None -> assert false | Some (uri,[],bo,ty) -> - if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then + if + CicReduction.are_convertible [] + (CicTypeChecker.type_of_aux' [] [] bo) ty + then begin (*CSC: Wrong: [] is just plainly wrong *) let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 7781be6ae..5457708a0 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -162,6 +162,15 @@ let perforate context term ty = exception Fail of string;; +(*CSC: generatore di nomi? Chiedere il nome? *) +let fresh_name = + let next_fresh_index = ref 0 +in + function () -> + incr next_fresh_index ; + "fresh_name" ^ string_of_int !next_fresh_index +;; + (* lambda_abstract newmeta ty *) (* returns a triple [bo],[context],[ty'] where *) (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *) @@ -179,7 +188,7 @@ let lambda_abstract newmeta ty = match n with C.Name _ -> n (*CSC: generatore di nomi? Chiedere il nome? *) - | C.Anonimous -> C.Name "fresh_name" + | C.Anonimous -> C.Name (fresh_name ()) in ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo)) | C.LetIn (n,s,t) -> @@ -229,7 +238,7 @@ let exact bo = metano,context,ty in let context = cic_context_of_named_context context in - if R.are_convertible (T.type_of_aux' metasenv context bo) ty then + if R.are_convertible context (T.type_of_aux' metasenv context bo) ty then begin refine_meta metano bo [] ; goal := None @@ -577,7 +586,8 @@ let reduction_tactic reduction_function term = None -> assert false | Some (metano,(context,ty)) -> metano,context,ty in - let term' = reduction_function term in + let ciccontext = cic_context_of_named_context context in + let term' = reduction_function ciccontext term in (* We don't know if [term] is a subterm of [ty] or a subterm of *) (* the type of one metavariable. So we replace it everywhere. *) (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) @@ -613,7 +623,8 @@ let reduction_tactic_in_scratch reduction_function ty term = None -> [] | Some (_,(context,_)) -> context in - let term' = reduction_function term in + let ciccontext = cic_context_of_named_context context in + let term' = reduction_function ciccontext term in ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty ;; @@ -639,7 +650,8 @@ let fold term = None -> assert false | Some (metano,(context,ty)) -> metano,context,ty in - let term' = CicReduction.whd term in + let ciccontext = cic_context_of_named_context context in + let term' = CicReduction.whd ciccontext term in (* We don't know if [term] is a subterm of [ty] or a subterm of *) (* the type of one metavariable. So we replace it everywhere. *) (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) @@ -736,7 +748,7 @@ let change ~goal_input ~input = let ciccontext = cic_context_of_named_context context in (* are_convertible works only on well-typed terms *) ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ; - if CicReduction.are_convertible goal_input input then + if CicReduction.are_convertible ciccontext goal_input input then begin let ty' = ProofEngineReduction.replace goal_input input ty in let metasenv' = diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 58aaa0438..94e5b353d 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -91,7 +91,7 @@ let replace ~what ~with_what ~where = (* Takes a well-typed term and fully reduces it. *) (*CSC: It does not perform reduction in a Case *) -let reduce = +let reduce context = let rec reduceaux l = let module C = Cic in let module S = CicSubstitution in @@ -274,7 +274,7 @@ exception WhatShouldIDo;; (* change in every iteration, i.e. to the actual arguments for the *) (* lambda-abstractions that precede the Fix. *) (*CSC: It does not perform simplification in a Case *) -let simpl = +let simpl context = (* reduceaux is equal to the reduceaux locally defined inside *) (*reduce, but for the const case. *) (**** Step 1 ****) @@ -337,7 +337,7 @@ let simpl = with _ -> raise AlreadySimplified in - (match CicReduction.whd recparam with + (match CicReduction.whd context recparam with C.MutConstruct _ | C.Appl ((C.MutConstruct _)::_) -> let body' = @@ -362,7 +362,7 @@ let simpl = [] -> C.Const (uri,cookingsno) | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args) in - let reduced_term_to_fold = reduce term_to_fold in + let reduced_term_to_fold = reduce context term_to_fold in prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ; prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ; replace reduced_term_to_fold term_to_fold res