- mk_restricted_irl removed, the non-optimized code was the same

- delift fixed in case Meta (used to produce negative shift/irl-len)
- fix-sorts takes into account the swap parameter to implement cumulativity

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index aa49a84ee726db1edafa785df5b5cd686aa261f9..12fe977083ec04a2c9ee309c116e2cb22419929b 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -179,15 +179,6 @@ let pack_lc orig =
 ;;
 
 
-let mk_restricted_irl shift len restrictions =
-  let rec aux n =
-    if n = 0 then 0 else
-     if List.mem (n+shift) restrictions then aux (n-1)
-     else 1+aux (n-1)
-  in
-    pack_lc (shift, NCic.Irl (aux len))
-;;
-
 
 let mk_perforated_irl shift len restrictions =
   let rec aux n =
@@ -208,28 +199,22 @@ let rec force_does_not_occur metasenv subst restrictions t =
           List.length (List.filter (fun x -> x < r - k) restrictions) 
         in
         if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig
-    | NCic.Meta (n, l) as orig ->
+    | NCic.Meta (n, (shift,lc as l)) as orig ->
        (* we ignore the subst since restrict will take care of already
         * instantiated/restricted metavariabels *)
        let (metasenv,subst as ms), restrictions_for_n, l' =
-         match l with
-         | shift, NCic.Irl len -> 
-             let restrictions = 
-               List.filter 
-                (fun i -> i > shift && i <= shift + len) restrictions in
-             ms, restrictions, mk_restricted_irl shift len restrictions
-         | shift, NCic.Ctx l ->
-            let ms, _, restrictions_for_n, l =
-             List.fold_right
-               (fun t (ms, i, restrictions_for_n, l) ->
-                 try 
-                   let ms, t = aux (k-shift) ms t in
-                   ms, i-1, restrictions_for_n, t::l
-                 with Occur ->
-                   ms, i-1, i::restrictions_for_n, l)
-               l (ms, List.length l, [], [])
-            in
-             ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
+         let l = NCicUtils.expand_local_context lc in
+         let ms, _, restrictions_for_n, l =
+          List.fold_right
+            (fun t (ms, i, restrictions_for_n, l) ->
+              try 
+                let ms, t = aux (k-shift) ms t in
+                ms, i-1, restrictions_for_n, t::l
+              with Occur ->
+                ms, i-1, i::restrictions_for_n, l)
+            l (ms, List.length l, [], [])
+         in
+          ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
        in
        if restrictions_for_n = [] then
          ms, if l = l' then orig else NCic.Meta (n, l')
@@ -287,13 +272,23 @@ and restrict metasenv subst i restrictions =
         let (metasenv, subst), newbo =  
           force_does_not_occur metasenv subst restrictions bo in
         let j = newmeta () in
-        let subst_entry_j = j, (name, newctx, newty, newbo) in
+        let subst_entry_j = j, (name, newctx, newbo, newty) in
         let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in
         let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
-        metasenv,
-        subst_entry_j :: List.map 
-          (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst,
-        j
+        let new_subst = 
+          subst_entry_j :: List.map 
+            (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst
+        in
+(*
+    prerr_endline ("restringo nella subst: " ^string_of_int i ^ " -> " ^ 
+      string_of_int j ^ "\n" ^ 
+      NCicPp.ppsubst ~metasenv [subst_entry_j] ^ "\n\n" ^
+      NCicPp.ppsubst ~metasenv [subst_entry_i] ^ "\n" ^
+      NCicPp.ppterm ~metasenv ~subst ~context:ctx bo ^ " ---- " ^
+      NCicPp.ppterm ~metasenv ~subst ~context:newctx newbo
+            );
+*)
+        metasenv, new_subst, j
       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
             ("Cannot restrict the context of the metavariable ?%d over "^^
             "the hypotheses %s since ?%d is already instantiated "^^
@@ -362,11 +357,9 @@ let delift metasenv subst context n l t =
               let shift1,lc1 = l1 in
               let shift,lc = l in
               let shift = shift + k in
-              let _ = prerr_endline ("XXX restringo " ^ string_of_int i) in
               match lc, lc1 with
               | NCic.Irl len, NCic.Irl len1 
                 when shift1 + len1 < shift || shift1 > shift + len ->
-                        prerr_endline "WWW 1";
                   let restrictions = HExtlib.list_seq 1 (len1 + 1) in
                   let metasenv, subst, newmeta = 
                      restrict metasenv subst i restrictions 
@@ -376,7 +369,6 @@ let delift metasenv subst context n l t =
               | NCic.Irl len, NCic.Irl len1 
                 when shift1 < shift || len1 + shift1 > len + shift ->
                   (* C. Hoare. Premature optimization is the root of all evil*)
-                        prerr_endline ("WWW 2 : " ^ string_of_int i);
                   let stop = shift + len in
                   let stop1 = shift1 + len1 in
                   let low_gap = max 0 (shift - shift1) in
@@ -388,23 +380,26 @@ let delift metasenv subst context n l t =
                     let metasenv, subst, newmeta = 
                        restrict metasenv subst i restrictions 
                     in
+(*
                   prerr_endline ("RESTRICTIONS FOR: " ^ 
-                  NCicPp.ppterm ~metasenv ~subst ~context:[] 
-                    (NCic.Meta (i,l1)) ^ 
-                    " that was part of a term unified with " ^
                     NCicPp.ppterm ~metasenv ~subst ~context:[] 
-                    (NCic.Meta (n,l)) ^ " ====> " ^ 
-                    String.concat "," (List.map string_of_int restrictions)
-                    ^ "\nMENV:\n" ^ NCicPp.ppmetasenv ~subst metasenv
-                    ^ "\nSUBST:\n" ^ NCicPp.ppsubst subst ~metasenv
-                    );
-                  let newlc = 
-                    assert (if shift1 > k then shift1 + low_gap - shift = 0 else
-                    true);
-                    NCic.Irl (len1 - low_gap - high_gap + max 0 (k - shift1)) in
+                    (NCic.Meta (i,l1))^" that was part of a term unified with "
+                    ^ NCicPp.ppterm ~metasenv ~subst ~context:[] (NCic.Meta
+                    (n,l)) ^ " ====> " ^ String.concat "," (List.map
+                    string_of_int restrictions) ^ "\nMENV:\n" ^
+                    NCicPp.ppmetasenv ~subst metasenv ^ "\nSUBST:\n" ^
+                    NCicPp.ppsubst subst ~metasenv);
+*)
+                  let newlc_len = 
+                    len1 - low_gap - high_gap + max 0 (k - shift1) in
+                  assert (if shift1 > k then 
+                    shift1 + low_gap - shift = 0 else true);
                   let meta = 
-                     NCic.Meta(newmeta,(shift1 + low_gap - shift, newlc))
+                     NCic.Meta(newmeta,(shift1 + low_gap - shift, 
+                       NCic.Irl newlc_len))
                   in
+                  let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in
+                  assert (List.length cctx = newlc_len);
                     (metasenv, subst), meta
                   
               | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
@@ -412,12 +407,13 @@ let delift metasenv subst context n l t =
                    ms, NCic.Meta (i, (max 0 (shift1 - shift), lc1))
               | _ ->
                   let lc1 = NCicUtils.expand_local_context lc1 in
+                  let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in
                   let rec deliftl tbr j ms = function
                     | [] -> ms, tbr, []
                     | t::tl ->
                         let ms, tbr, tl = deliftl tbr (j+1) ms tl in
                         try 
-                          let ms, t = aux (k-shift1) ms t in 
+                          let ms, t = aux k ms t in 
                           ms, tbr, t::tl
                         with
                         | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
@@ -427,7 +423,11 @@ let delift metasenv subst context n l t =
                   prerr_endline ("TO BE RESTRICTED: " ^ 
                    (String.concat "," (List.map string_of_int to_be_r)));
 *)
-                  let l1 = pack_lc (shift, NCic.Ctx lc1') in
+                  let l1 = pack_lc (0, NCic.Ctx lc1') in
+(*
+                  prerr_endline ("newmeta:" ^ NCicPp.ppterm
+                   ~metasenv ~subst ~context (NCic.Meta (999,l1)));
+*)
                   if to_be_r = [] then
                     (metasenv, subst), 
                     (if lc1' = lc1 then orig else NCic.Meta (i,l1))
@@ -435,6 +435,7 @@ let delift metasenv subst context n l t =
                     let metasenv, subst, newmeta = 
                       restrict metasenv subst i to_be_r in
                     (metasenv, subst), NCic.Meta(newmeta,l1))
+
     | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
   in
    try aux 0 (metasenv,subst) t

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 253af6f37cdec2cefea9deed14191e7e166f2346..eb7b136c28f3ba948c9048a5f247241614181499 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -22,11 +22,13 @@ let indent = ref "";;
 let inside c = indent := !indent ^ String.make 1 c;;
 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
+(*
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
+*)
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg
@@ -292,6 +294,9 @@ let rec typeof
               let ty_branch = 
                 NCicTypeChecker.type_of_branch 
                   ~subst context leftno outtype cons ty_cons in
+              pp (lazy ("TYPEOFBRANCH: " ^
+               NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^
+               NCicPp.ppterm ~metasenv ~subst ~context ty_branch ));
               let metasenv, subst, p, _ = 
                 typeof_aux metasenv subst context (Some ty_branch) p in
               j+1, metasenv, subst, p :: branches)
@@ -327,8 +332,8 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
           in
           let flex_prod = C.Prod ("_", ty_arg, meta) in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
-            NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
-            NCicPp.ppmetasenv ~subst metasenv ^ "\nOF: " ^
+            NCicPp.ppcontext ~metasenv ~subst context
+            ^ "\nOF: " ^
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
           let metasenv, subst = 

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d3c86d2816c2c9bd050bbe1b336d033d95e4c8dd..202e68e4c86c3d056a8914451a70b6c4b25aae13 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -72,18 +72,26 @@ let indent = ref "";;
 let inside c = indent := !indent ^ String.make 1 c;;
 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
+(*
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
+*)
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
-let fix_sorts metasenv subst context meta t =
+let fix_sorts swap metasenv subst context meta t =
   let rec aux () = function
     | NCic.Sort (NCic.Type u) as orig ->
-       (match NCicEnvironment.sup u with
-       | None ->  raise (fail_exc metasenv subst context meta t)
-       | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1))
+        if swap then
+         match NCicEnvironment.sup u with
+         | None ->  raise (fail_exc metasenv subst context meta t)
+         | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
+        else
+         NCic.Sort (NCic.Type (
+           match NCicEnvironment.sup NCicEnvironment.type0 with 
+           | Some x -> x 
+           | _ -> assert false))
     | NCic.Meta _ as orig -> orig
     | t -> NCicUtils.map (fun _ _ -> ()) () aux t
   in
@@ -157,35 +165,31 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
     if swap then unify test_eq_only m s c t2 t1 
     else unify test_eq_only m s c t1 t2
   in
-  let fix_sorts t = 
-    if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t
-    else 
-      NCic.Sort (NCic.Type (
-        match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ ->
-                assert false))
-  in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
   let metasenv, subst, t = 
     match ty with 
-    | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t
+    | NCic.Implicit (`Typeof _) -> 
+       metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
     | _ ->
        pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
          with NCicTypeChecker.TypeCheckerFailure _ -> 
-           let ft = fix_sorts t in
-           if ft == t then assert false else
+           let ft = 
+            fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
+           in
+           if ft == t then assert false
+           else
             try 
               pp (lazy ("typeof: " ^ 
                 NCicPp.ppterm ~metasenv ~subst ~context ft));
               ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
-            with NCicTypeChecker.TypeCheckerFailure msg -> 
-              prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft);
-              prerr_endline (Lazy.force msg);
+            with NCicTypeChecker.TypeCheckerFailure _ -> 
               assert false
        in
        let lty = NCicSubstitution.subst_meta lc ty in
        pp (lazy("On the types: " ^
+        NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
         NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
          ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
        let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in