arithmetics for λδ

[helm.git] / helm / software / components / grafite_engine / nCicCoercDeclaration.ml

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
index 550cb93c4a10394ffcdd7ecc74146d416de77cfb..7fcd6a473f4595f70047f2bda5fce0b6867b68bf 100644 (file)
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-let debug s = prerr_endline (Lazy.force s) ;;
+(* let debug s = prerr_endline (Lazy.force s) ;;*)
 let debug _ = ();;
 
 let skel_dummy = NCic.Implicit `Type;;
@@ -32,12 +32,6 @@ let pos_in_list x l =
       | None -> assert false
 ;;
 
-let pos_of x t = 
-  match t with
-  | NCic.Appl l -> pos_in_list x l
-  | _ -> assert false
-;;
-
 let rec count_prod = function
   | NCic.Prod (_,_,x) -> 1 + count_prod x
   | _ -> 0
@@ -133,7 +127,7 @@ let only_head = function
 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
   let status, src, cpos = 
     let rec aux cpos ctx = function
-      | NCic.Prod (name,ty,bo) ->
+      | NCic.Prod (name,ty,bo) -> 
          if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
          else
            (try 
@@ -183,6 +177,7 @@ let fresh_uri status prefix suffix =
    diverge (mk "") 0
 ;;
 
+exception Stop;;
 
 let close_graph name t s d to_s from_d p a status =
   let c =
@@ -201,13 +196,13 @@ let close_graph name t s d to_s from_d p a status =
     let c_o_from_d = 
       product 
         (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) -> 
-          compose_names n1 n,m1@mc,t1,[i,c],j,count_prod ty) 
+          compose_names n n1,m1@mc,t1,[i,c],j,count_prod ty) 
         [c] from_d
     in
     let to_s_o_c_o_from_d =
       product 
         (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)-> 
-          compose_names n n1,m@m1,t,(i,t1)::upl,j,a)
+          compose_names n1 n,m@m1,t,(i,t1)::upl,j,a)
         to_s c_o_from_d
     in
     to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
@@ -223,19 +218,21 @@ let close_graph name t s d to_s from_d p a status =
             (metasenv,[]) upl
          in
          let bo = NCicUntrusted.apply_subst subst [] bo in
+         let p = NCicUntrusted.apply_subst subst [] p in
+         let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
          let metasenv = toposort metasenv in
          let bo = close_in_context bo metasenv in
          let pos = 
            match p with 
            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
-           | _ -> assert false
+           | t -> raise Stop
          in
          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
          let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
          let src = only_head src in
          let tgt = only_head tgt in
          debug (lazy(
-           "composite: "^
+           "composite " ^ name ^ ": "^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
@@ -255,7 +252,7 @@ let close_graph name t s d to_s from_d p a status =
        with 
        | NCicTypeChecker.TypeCheckerFailure _
        | NCicUnification.UnificationFailure _ 
-       | NCicUnification.Uncertain _ -> None
+       | NCicUnification.Uncertain _ | Stop -> None
      ) composites
   in
     composites
@@ -294,7 +291,10 @@ let record_ncoercion =
  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
    List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
  in
-  NRstatus.Serializer.register "ncoercion" aux_l
+  NCicLibrary.Serializer.register#run "ncoercion"
+   object(self : 'a NCicLibrary.register_type)
+    method run = aux_l 
+   end
 ;;
 
 let basic_eval_and_record_ncoercion infos status =