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 1861ce5b0222e132d53d72f08474f471f6bbbbfc..08cb06d9d93b8dcc49a827223fd1b2d7e629c01c 100644 (file)
--- 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 49510a9dde1dc7f9a2480df7d7a7afc11caf686f..47c416d8b60b9ad472098d883f4cacf2f2026345 100644 (file)
--- 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 7781be6ae11e7fc1187b0c13dcad398d13a88d3e..5457708a0a41a143d8ccd2824b931a2cdb97ed1f 100644 (file)
--- 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 58aaa04386329ef8e0de0283fa449e84bc0612d2..94e5b353de3534df42cba3016327de56abffdd6c 100644 (file)
--- 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