CicReduction.whd now requires a context.
(*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. *)
(*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
let innersort = T.type_of_aux' metasenv cicenv innertype in
let ainnertype =
if computeinnertypes then
match !ProofEngine.proof with
None -> assert false
| Some (uri,[],bo,ty) ->
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
begin
(*CSC: Wrong: [] is just plainly wrong *)
let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
exception Fail of string;;
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!) *)
(* lambda_abstract newmeta ty *)
(* returns a triple [bo],[context],[ty'] where *)
(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
match n with
C.Name _ -> n
(*CSC: generatore di nomi? Chiedere il nome? *)
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) ->
in
((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
| C.LetIn (n,s,t) ->
metano,context,ty
in
let context = cic_context_of_named_context context in
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
begin
refine_meta metano bo [] ;
goal := None
None -> assert false
| Some (metano,(context,ty)) -> metano,context,ty
in
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 *)
(* 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 *)
None -> []
| Some (_,(context,_)) -> context
in
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
;;
ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
;;
None -> assert false
| Some (metano,(context,ty)) -> metano,context,ty
in
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 *)
(* 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 *)
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) ;
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' =
begin
let ty' = ProofEngineReduction.replace goal_input input ty in
let metasenv' =
(* Takes a well-typed term and fully reduces it. *)
(*CSC: It does not perform reduction in a Case *)
(* Takes a well-typed term and fully reduces it. *)
(*CSC: It does not perform reduction in a Case *)
let rec reduceaux l =
let module C = Cic in
let module S = CicSubstitution in
let rec reduceaux l =
let module C = Cic in
let module S = CicSubstitution in
(* 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 *)
(* 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 *)
(* reduceaux is equal to the reduceaux locally defined inside *)
(*reduce, but for the const case. *)
(**** Step 1 ****)
(* reduceaux is equal to the reduceaux locally defined inside *)
(*reduce, but for the const case. *)
(**** Step 1 ****)
with
_ -> raise AlreadySimplified
in
with
_ -> raise AlreadySimplified
in
- (match CicReduction.whd recparam with
+ (match CicReduction.whd context recparam with
C.MutConstruct _
| C.Appl ((C.MutConstruct _)::_) ->
let body' =
C.MutConstruct _
| C.Appl ((C.MutConstruct _)::_) ->
let body' =
[] -> C.Const (uri,cookingsno)
| _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
in
[] -> 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
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