From 2a40efede6d4430b4ca086275bcac80905ec1a74 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 29 Apr 2002 10:22:09 +0000 Subject: [PATCH] Computed inner-types are now also put in whd normal form. This is at the same type too strong (e.g. it performs delta-reductions) and too weak (it is not full-reduction). We can consider this just a patch waiting for Coscoy's double-inference algorithm implementation. --- helm/gTopLevel/cic2acic.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index ec9dc680e..1861ce5b0 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -70,7 +70,12 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts in let ainnertype,innertype,innersort = let cicenv = List.map (function (_,ty) -> ty) bs in - let innertype = T.type_of_aux' metasenv cicenv tt in +(*CSC: Here we need the algorithm for Coscoy's double type-inference *) +(*CSC: (expected type + inferred type). Just for now we use the usual *) +(*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 innersort = T.type_of_aux' metasenv cicenv innertype in let ainnertype = if computeinnertypes then -- 2.39.2