1) hard coded linearized references removed

2) new concrete syntax for linearized references
   more compliant with URI generic syntax and ELPI

   '#' not allowed in path and name

   Decl                   cic:/path/name#dec
   Def                    cic:/path/name#def:i
   Fix of int * int       cic:/path/name#fix:i:j:h
   CoFix of int           cic:/path/name#cfx:i
   Ind of int             cic:/path/name#ind:b:i:l
   Con of int * int       cic:/path/name#con:i:j:l

   run matitaclean all after this update,
   as stored aliases depend on linearized references

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 5c0d0a7d5db30840ad39521f9f98df73a27a5d7d..59fe713e560d989766209f4d3a55b066bd92a335 100644 (file)
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -167,7 +167,8 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                    "branch pattern must be \"_\"")))
            ) branches in
          let indtype_ref =
-          NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)"
+          let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in 
+          NRef.reference_of_spec uri (NRef.Ind (true,1,1))
          in
           NCic.Match (indtype_ref, cic_outtype, cic_term,
            (List.map do_branch branches))
@@ -177,7 +178,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
           | Some (indty_ident, _) ->
              (match Disambiguate.resolve ~env ~mk_choice 
                 (DT.Id indty_ident) (`Args []) with
-              | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
+              | NCic.Const (NRef.Ref (_,NRef.Ind _) as r) -> r
               | NCic.Implicit _ ->
                  raise (Disambiguate.Try_again 
                   (lazy "The type of the term to be matched is still unknown"))
@@ -205,9 +206,9 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
 *)
               (match Disambiguate.resolve ~env ~mk_choice
                 (DT.Id (fst_constructor branches)) (`Args []) with
-              | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> 
+              | NCic.Const (NRef.Ref (_,NRef.Con _) as r) -> 
                    let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
-                   NReference.mk_indty b r
+                   NRef.mk_indty b r
               | NCic.Implicit _ ->
                  raise (Disambiguate.Try_again 
                   (lazy "The type of the term to be matched is still unknown"))
@@ -322,7 +323,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
     | NotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (NReference.reference_of_string uri)
+         NCic.Const (NRef.reference_of_string uri)
         with NRef.IllFormedReference _ ->
          NotationPt.fail loc "Ill formed reference")
     | NotationPt.NRef nref -> NCic.Const nref
@@ -466,7 +467,7 @@ let interpretate_obj status
       List.fold_left
        (fun (i,res) (name,_,_,_) ->
          let nref =
-          NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
+          NRef.reference_of_spec uri (NRef.Ind (inductive,i,leftno))
          in
           i+1,(name,nref)::res)
        (0,[]) tyl) in
@@ -521,7 +522,7 @@ let interpretate_obj status
       (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
         ~is_path:false ty) in
     let nref =
-     NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+     NRef.reference_of_spec uri (NRef.Ind (true,0,leftno)) in
     let obj_context = [name,nref] in
     let fields' =
      snd (
@@ -555,9 +556,9 @@ let interpretate_obj status
        List.fold_left
          (fun (i,acc) (_,(name,_),_,k) -> 
           (i+1, 
-            (ncic_name_of_ident name, NReference.reference_of_spec uri 
-             (if inductive then NReference.Fix (i,k,0)
-              else NReference.CoFix i)) :: acc))
+            (ncic_name_of_ident name, NRef.reference_of_spec uri 
+             (if inductive then NRef.Fix (i,k,0)
+              else NRef.CoFix i)) :: acc))
          (0,[]) defs
      in
      let inductiveFuns =

diff --git a/matita/components/ng_extraction/nCicExtraction.ml b/matita/components/ng_extraction/nCicExtraction.ml
index 4e167004d0b5e4a41d9dcf22e1792486e0b880f0..12261145e6bafdc77288daf0a4eb1ed463bd909a 100644 (file)
--- a/matita/components/ng_extraction/nCicExtraction.ml
+++ b/matita/components/ng_extraction/nCicExtraction.ml
@@ -25,11 +25,13 @@
 
 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
 
+module Ref = NReference
+
 let fix_sorts t = t;;
 let apply_subst subst t = assert (subst=[]); t;;
 
-type typformerreference = NReference.reference
-type reference = NReference.reference
+type typformerreference = Ref.reference
+type reference = Ref.reference
 
 type kind =
   | Type
@@ -130,13 +132,13 @@ let rec size_of_term =
     | UnsafeCoerce t -> 1 + size_of_term t
 ;;
 
-module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
+module ReferenceMap = Map.Make(struct type t = Ref.reference let compare = Ref.compare end)
 
 module GlobalNames = Set.Make(String)
 
 type info_el =
  string * [`Type of typ_context * typ option | `Constructor of typ | `Function of typ ]
-type info = (NReference.reference * info_el) list
+type info = (Ref.reference * info_el) list
 type db = info_el ReferenceMap.t * GlobalNames.t
 
 let empty_info = []
@@ -146,15 +148,16 @@ type obj_kind =
  | TypeDefinition of typ_former_def
  | TermDeclaration of term_former_decl
  | TermDefinition of term_former_def
- | LetRec of (info * NReference.reference * obj_kind) list
+ | LetRec of (info * Ref.reference * obj_kind) list
    (* reference, left, right, constructors *)
- | Algebraic of (info * NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list
+ | Algebraic of (info * Ref.reference * typ_context * typ_context * (Ref.reference * typ) list) list
 
-type obj = info * NReference.reference * obj_kind
+type obj = info * Ref.reference * obj_kind
 
 (* For LetRec and Algebraic blocks *)
 let dummyref =
- NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
+ let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in
+ Ref.reference_of_spec uri (Ref.Ind (true,1,1))
 
 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
 
@@ -185,7 +188,7 @@ let rec classify_not_term status context t =
      classify_not_term status ((b,NCic.Decl s)::context) t
   | NCic.Implicit _
   | NCic.LetIn _
-  | NCic.Const (NReference.Ref (_,NReference.CoFix _))
+  | NCic.Const (Ref.Ref (_,Ref.CoFix _))
   | NCic.Appl [] ->
      assert false (* NOT POSSIBLE *)
   | NCic.Lambda (n,s,t) ->
@@ -195,10 +198,10 @@ let rec classify_not_term status context t =
   | NCic.Match (_,_,_,pl) ->
      let classified_pl = List.map (classify_not_term status context) pl in
       sup classified_pl
-  | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
+  | NCic.Const (Ref.Ref (_,Ref.Fix _)) ->
      assert false (* IMPOSSIBLE *)
   | NCic.Meta _ -> assert false (* TODO *)
-  | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix (i,_,_)) as r)::_)->
+  | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Fix (i,_,_)) as r)::_)->
      let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
      let _,_,_,_,bo = List.nth l i in
       classify_not_term status [] bo
@@ -223,7 +226,7 @@ let rec classify_not_term status context t =
       (match List.nth context (n-1) with
           _,NCic.Decl typ -> find_sort typ
         | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
-  | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
+  | NCic.Const (Ref.Ref (_,Ref.Decl) as ref) ->
      let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
       (match classify_not_term status [] ty with
         | `Proposition
@@ -231,7 +234,7 @@ let rec classify_not_term status context t =
         | `Kind
         | `KindOrType -> `Type
         | `PropKind -> `Proposition)
-  | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
+  | NCic.Const (Ref.Ref (_,Ref.Ind _) as ref) ->
      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
      let _,_,arity,_ = List.nth ityl i in
       (match classify_not_term status [] arity with
@@ -240,8 +243,8 @@ let rec classify_not_term status context t =
         | `KindOrType -> assert false (* IMPOSSIBLE *)
         | `Kind -> `Type
         | `PropKind -> `Proposition)
-  | NCic.Const (NReference.Ref (_,NReference.Con _))
-  | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
+  | NCic.Const (Ref.Ref (_,Ref.Con _))
+  | NCic.Const (Ref.Ref (_,Ref.Def _)) ->
      assert false (* IMPOSSIBLE *)
 ;;
 
@@ -377,10 +380,10 @@ let rec split_typ_lambdas status n ~metasenv context typ =
 
 let rev_context_of_typformer status ~metasenv context =
  function
-    NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
-  | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
-  | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
-  | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
+    NCic.Const (Ref.Ref (_,Ref.Ind _) as ref)
+  | NCic.Const (Ref.Ref (_,Ref.Def _) as ref)
+  | NCic.Const (Ref.Ref (_,Ref.Decl) as ref)
+  | NCic.Const (Ref.Ref (_,Ref.Fix _) as ref) ->
      (try
        match snd (ReferenceMap.find ref (fst status#extraction_db)) with
           `Type (ctx,_) -> List.rev ctx
@@ -405,8 +408,8 @@ let rev_context_of_typformer status ~metasenv context =
      let typ = kind_of status ~metasenv typ_ctx typ in
       List.rev (fst (split_kind_prods [] typ))
   | NCic.Meta _ -> assert false (* TODO *)
-  | NCic.Const (NReference.Ref (_,NReference.Con _))
-  | NCic.Const (NReference.Ref (_,NReference.CoFix _))
+  | NCic.Const (Ref.Ref (_,Ref.Con _))
+  | NCic.Const (Ref.Ref (_,Ref.CoFix _))
   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
   | NCic.Appl _ | NCic.Prod _ ->
      assert false (* IMPOSSIBLE *)
@@ -434,7 +437,7 @@ let rec typ_of status ~metasenv context k =
   | NCic.Rel n -> Var n
   | NCic.Const ref -> TConst ref
   | NCic.Match (_,_,_,_)
-  | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix _))::_) ->
+  | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Fix _))::_) ->
      Top
   | NCic.Appl (he::args) ->
      let rev_he_context= rev_context_of_typformer status ~metasenv context he in
@@ -521,7 +524,7 @@ let fomega_lookup status ref =
    | `Function _ -> assert false
  with
   Not_found ->
-prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); None
+prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ Ref.string_of_reference ref); None
 
 let rec fomega_whd status ty =
  match ty with
@@ -548,7 +551,7 @@ let rec fomega_conv status t1 t2 =
     Var n, Var m -> n=m
   | Unit, Unit -> true
   | Top, Top -> true
-  | TConst r1, TConst r2 -> NReference.eq r1 r2
+  | TConst r1, TConst r2 -> Ref.eq r1 r2
   | Arrow (s1,t1), Arrow (s2,t2) ->
      fomega_conv status s1 s2 && fomega_conv status t1 t2
   | TSkip t1, TSkip t2 -> fomega_conv status t1 t2
@@ -574,11 +577,11 @@ let type_of_constructor status ref =
 
 let type_of_appl_he status ~metasenv context =
  function
-    NCic.Const (NReference.Ref (_,NReference.Con _) as ref)
-  | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
-  | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
-  | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref)
-  | NCic.Const (NReference.Ref (_,NReference.CoFix _) as ref) ->
+    NCic.Const (Ref.Ref (_,Ref.Con _) as ref)
+  | NCic.Const (Ref.Ref (_,Ref.Def _) as ref)
+  | NCic.Const (Ref.Ref (_,Ref.Decl) as ref)
+  | NCic.Const (Ref.Ref (_,Ref.Fix _) as ref)
+  | NCic.Const (Ref.Ref (_,Ref.CoFix _) as ref) ->
      (try
        match snd (ReferenceMap.find ref (fst status#extraction_db)) with
           `Type _ -> assert false
@@ -586,7 +589,7 @@ let type_of_appl_he status ~metasenv context =
         | `Function ty -> ty
       with
        Not_found -> assert false)
-  | NCic.Const (NReference.Ref (_,NReference.Ind _)) ->
+  | NCic.Const (Ref.Ref (_,Ref.Ind _)) ->
      assert false (* IMPOSSIBLE *)
   | NCic.Rel n ->
      (match List.nth context (n-1) with
@@ -685,7 +688,7 @@ let rec term_of status ~metasenv context =
         try
          HExtlib.list_mapi
           (fun pat i ->
-            let ref = NReference.mk_constructor (i+1) ref in
+            let ref = Ref.mk_constructor (i+1) ref in
             let ty = 
              (* BUG HERE, QUICK BUG WRONG PATCH IN PLACE *)
              try
@@ -801,7 +804,7 @@ let fresh_name_of_ref status ref =
  (*CSC: Patch while we wait for separate compilation *)
  let candidate =
   let name = NCicPp.r2s status true ref in
-  let NReference.Ref (uri,_) = ref in
+  let Ref.Ref (uri,_) = ref in
   let path = NUri.baseuri_of_uri uri in
   let path = String.sub path 5 (String.length path - 5) in
   let path = Str.global_replace (Str.regexp "/") "_" path in
@@ -879,7 +882,7 @@ let object_of_inductive status ~metasenv uri ind leftno il =
           let ctx,_ = split_kind_prods [] arity in
           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
           let ref =
-           NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
+           Ref.reference_of_spec uri (Ref.Ind (ind,i,leftno)) in
           let info = ref,`Type (ctx,None) in
           let status,info = register_name_and_info status info in
           let _,status,cl_rev,infos =
@@ -890,7 +893,7 @@ let object_of_inductive status ~metasenv uri ind leftno il =
               let ty = typ_of status ~metasenv ctx ty in
               let left = term_ctx_of_type_ctx left in
               let full_ty = glue_ctx_typ left ty in
-              let ref = NReference.mk_constructor j ref in
+              let ref = Ref.mk_constructor j ref in
               let info = ref,`Constructor full_ty in
               let status,info = register_name_and_info status info in
                j+1,status,((ref,ty)::res),info::infos
@@ -908,7 +911,7 @@ let object_of status (uri,height,metasenv,subst,obj_kind) =
   let obj_kind = apply_subst subst obj_kind in
       match obj_kind with
         | NCic.Constant (_,_,None,ty,_) ->
-          let ref = NReference.reference_of_spec uri NReference.Decl in
+          let ref = Ref.reference_of_spec uri Ref.Decl in
           (match classify status ~metasenv [] ty with
             | `Kind ->
               let ty = kind_of status ~metasenv [] ty in
@@ -927,7 +930,7 @@ let object_of status (uri,height,metasenv,subst,obj_kind) =
                 TermDeclaration (split_typ_prods [] ty))
             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
         | NCic.Constant (_,_,Some bo,ty,_) ->
-           let ref = NReference.reference_of_spec uri (NReference.Def height) in
+           let ref = Ref.reference_of_spec uri (Ref.Def height) in
             object_of_constant status ~metasenv ref bo ty
         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
           let _,status,objs =
@@ -935,10 +938,10 @@ let object_of status (uri,height,metasenv,subst,obj_kind) =
             (fun (_,_name,recno,ty,bo) (i,status,res) ->
               let ref =
                if fix_or_cofix then
-                NReference.reference_of_spec
-                 uri (NReference.Fix (i,recno,height))
+                Ref.reference_of_spec
+                 uri (Ref.Fix (i,recno,height))
                else
-                NReference.reference_of_spec uri (NReference.CoFix i)
+                Ref.reference_of_spec uri (Ref.CoFix i)
               in
               let status,obj = object_of_constant ~metasenv status ref bo ty in
                 match obj with
@@ -1041,7 +1044,7 @@ let classify_reference status ref =
    | `Function _ -> `FunctionName
  with
   Not_found ->
-prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); `FunctionName
+prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ Ref.string_of_reference ref); `FunctionName
 ;;
 
 let capitalize classification name =
@@ -1057,7 +1060,7 @@ let pp_ref status ref =
  capitalize (classify_reference status ref)
   (try fst (ReferenceMap.find ref (fst status#extraction_db))
    with Not_found ->
-prerr_endline ("BUG with coercions: " ^ NReference.string_of_reference ref);
+prerr_endline ("BUG with coercions: " ^ Ref.string_of_reference ref);
 (*assert false*)
  NCicPp.r2s status true ref (* BUG: this should never happen *)
 )
@@ -1146,7 +1149,7 @@ let rec pretty_print_term status ctxt =
          String.concat " ;\n"
            (HExtlib.list_mapi
              (fun (bound_names,rhs) i ->
-               let ref = NReference.mk_constructor (i+1) r in
+               let ref = Ref.mk_constructor (i+1) r in
                let name = pp_ref status ref in
                let ctxt,bound_names =
                 pretty_print_term_context status ctxt bound_names in

diff --git a/matita/components/ng_kernel/nReference.ml b/matita/components/ng_kernel/nReference.ml
index bb560bfd6349161810d9a0fd05a4b83e9d286f0c..102f25046f84187a495d5778deebf1f1c6148d5d 100644 (file)
--- a/matita/components/ng_kernel/nReference.ml
+++ b/matita/components/ng_kernel/nReference.ml
@@ -45,14 +45,15 @@ module MapStringsToReference = Map.Make(OrderedStrings);;
 
 let set_of_reference = ref MapStringsToReference.empty;;
 
-(* '.' not allowed in path and foo
+(* Note: valid ELPI constant
+ * '#' not allowed in path and name
  *
- * Decl                   cic:/path/foo.dec
- * Def                    cic:/path/foo.def
- * Fix of int * int       cic:/path/foo.fix(i,j)
- * CoFix of int           cic:/path/foo.cfx(i)
- * Ind of int             cic:/path/foo.ind(i)
- * Con of int * int       cic:/path/foo.con(i,j)
+ * Decl                   cic:/path/name#dec
+ * Def                    cic:/path/name#def:i
+ * Fix of int * int       cic:/path/name#fix:i:j:h
+ * CoFix of int           cic:/path/name#cfx:i
+ * Ind of int             cic:/path/name#ind:b:i:l
+ * Con of int * int       cic:/path/name#con:i:j:l
  *)
 
 let uri_suffix_of_ref_suffix = function
@@ -63,11 +64,11 @@ let uri_suffix_of_ref_suffix = function
 
 let reference_of_string =
   let get3 s dot =
-    let comma2 = String.rindex s ',' in
-    let comma = String.rindex_from s (comma2-1) ',' in
+    let comma2 = String.rindex s ':' in
+    let comma = String.rindex_from s (comma2-1) ':' in
     let s_i = String.sub s (dot+5) (comma-dot-5) in
     let s_j = String.sub s (comma+1) (comma2-comma-1) in
-    let s_h = String.sub s (comma2+1) (String.length s-comma2-2) in
+    let s_h = String.sub s (comma2+1) (String.length s-comma2-1) in
     let i = int_of_string s_i in
     let j = int_of_string s_j in
     let h = int_of_string s_h in
@@ -75,14 +76,14 @@ let reference_of_string =
   in
 (*
   let get2 s dot =
-    let comma = String.rindex s ',' in
+    let comma = String.rindex s ':' in
     let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in
-    let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in
+    let j = int_of_string (String.sub s (comma+1) (String.length s-comma-1)) in
     i,j
   in
 *)
   let get1 s dot =
-    let i = int_of_string (String.sub s (dot+5) (String.length s-1-dot-5)) in
+    let i = int_of_string (String.sub s (dot+5) (String.length s-dot-5)) in
     i
   in
 fun s ->
@@ -90,10 +91,10 @@ fun s ->
   with Not_found ->
     let new_reference =
       try
-        let dot = String.rindex s '.' in
-        let prefix = String.sub s 0 (dot+1) in
+        let dot = String.rindex s '#' in
+        let prefix = String.sub s 0 dot in
         let suffix = String.sub s (dot+1) 3 in
-        let u = NUri.uri_of_string (prefix ^ uri_suffix_of_ref_suffix suffix) in
+        let u = NUri.uri_of_string (prefix ^ "." ^ uri_suffix_of_ref_suffix suffix) in
         match suffix with
         | "dec" -> Ref (u, Decl)
         | "def" -> let i = get1 s dot in Ref (u, Def i)
@@ -113,16 +114,16 @@ let string_of_reference (Ref (u,indinfo)) =
   let dot = String.rindex s '.' in
   let s2 = String.sub s 0 dot in
   match indinfo with
-  | Decl ->  s2 ^ ".dec"
-  | Def h -> s2 ^ ".def(" ^ string_of_int h ^ ")"
+  | Decl ->  s2 ^ "#dec"
+  | Def h -> s2 ^ "#def:" ^ string_of_int h
   | Fix (i,j,h)  -> 
-      s2 ^ ".fix(" ^ string_of_int i ^ "," ^ 
-      string_of_int j ^ "," ^ string_of_int h ^ ")"
-  | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
-  | Ind (b,i,l)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^
-      "," ^ string_of_int l ^ ")"
-  | Con (i,j,l) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ 
-      "," ^ string_of_int l ^ ")"
+      s2 ^ "#fix:" ^ string_of_int i ^ ":" ^
+      string_of_int j ^ ":" ^ string_of_int h
+  | CoFix i -> s2 ^ "#cfx:" ^ string_of_int i
+  | Ind (b,i,l)->s2 ^"#ind:" ^(if b then "1" else "0")^ ":" ^ string_of_int i ^
+      ":" ^ string_of_int l
+  | Con (i,j,l) -> s2 ^ "#con:" ^ string_of_int i ^ ":" ^ string_of_int j ^
+      ":" ^ string_of_int l
 ;;
 
 let mk_constructor j = function
@@ -155,7 +156,3 @@ let mk_cofix i = function
 let reference_of_spec u spec = 
   reference_of_string (string_of_reference (Ref (u, spec)))
 ;;
-
-
-
-

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index 3aabdf1d4a2b915fa66b17901e217a75d20097ec..15fcc069aaae4e3a589dbffb2e3d9abb49d788c6 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -178,6 +178,16 @@ in
   name' ^ (if last = -1 then "" else string_of_int (last + 1))
 with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false
 
+(* let eq, eq_refl =
+    let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+    C.Const (Ref.reference_of_spec uri (Ref.Ind (true,0,2))),
+    C.Const (Ref.reference_of_spec uri Ref.Con (0,1,2))
+*)
+let eq, eq_refl = 
+ let uri = NUri.uri_of_string "cic:/matita/basics/jmeq/jmeq.ind" in
+ C.Const (Ref.reference_of_spec uri (Ref.Ind(true,0,2))),
+ C.Const (Ref.reference_of_spec uri (Ref.Con(0,1,2)))
+
 let rec typeof (status:#NCicCoercion.status)
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   metasenv subst context term expty 
@@ -603,7 +613,7 @@ and try_coercions status
         (* {{{ helper functions *)
         let get_cl_and_left_p refit outty =
           match refit with
-          | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
+          | Ref.Ref (uri, Ref.Ind (_,tyno,leftno)) ->
              let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
              let _, _, ty, cl = List.nth itl tyno in
              let constructorsno = List.length cl in
@@ -678,10 +688,6 @@ and try_coercions status
                 (List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 1 matched) (n-1))
           | _ -> assert false
         in
-        (*let eq = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
-        let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
-        let eq = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in
-        let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in
         let add_params 
           metasenv subst context cty outty mty m i 
         =
@@ -1014,8 +1020,8 @@ and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
 and guess_name status subst ctx ty = 
   let aux initial = "#" ^ String.make 1 initial in
   match ty with
-  | C.Const (NReference.Ref (u,_))
-  | C.Appl (C.Const (NReference.Ref (u,_)) :: _) ->
+  | C.Const (Ref.Ref (u,_))
+  | C.Appl (C.Const (Ref.Ref (u,_)) :: _) ->
       aux (String.sub (NUri.name_of_uri u) 0 1).[0] 
   | C.Prod _ -> aux 'f' 
   | C.Meta (n,lc) -> 
@@ -1106,7 +1112,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig
           aux metasenv subst (arg :: args_so_far) he meta tl
       | C.Match (_,_,C.Meta _,_) 
       | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
-      | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
+      | C.Appl (C.Const (Ref.Ref (_, Ref.Fix _)) :: _) ->
           raise (Uncertain (lazy (localise orig_he, Printf.sprintf
             ("The term %s is here applied to %d arguments but expects " ^^
             "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
@@ -1171,8 +1177,8 @@ let undebruijnate status inductive ref t rev_fl =
       (fun (_,_,rno,_,_,_) i -> 
          let i = len - i - 1 in
          C.Const 
-           (if inductive then NReference.mk_fix i rno ref
-            else NReference.mk_cofix i ref))
+           (if inductive then Ref.mk_fix i rno ref
+            else Ref.mk_cofix i ref))
       rev_fl)
     t
 ;; 
@@ -1224,9 +1230,9 @@ let typeof_obj
           (fun (relevance,name,k,ty,dbo) ->
             let bo = 
               undebruijnate status inductive 
-               (NReference.reference_of_spec uri 
-                 (if inductive then NReference.Fix (0,k,0) 
-                  else NReference.CoFix 0)) dbo rev_fl
+               (Ref.reference_of_spec uri 
+                 (if inductive then Ref.Fix (0,k,0) 
+                  else Ref.CoFix 0)) dbo rev_fl
             in
               relevance,name,k,ty,bo)
           fl
@@ -1365,8 +1371,8 @@ let typeof_obj
                     if i <= leftno  then
                      C.Rel i
                     else
-                     C.Const (NReference.reference_of_spec uri
-                      (NReference.Ind (ind,relsno - i,leftno))))
+                     C.Const (Ref.reference_of_spec uri
+                      (Ref.Ind (ind,relsno - i,leftno))))
                   (HExtlib.list_seq 1 (relsno+1))
                    te in
                let te =

diff --git a/matita/components/ng_refiner/nCicUnifHint.ml b/matita/components/ng_refiner/nCicUnifHint.ml
index ff8de755469b21ffb336e9f4a833e3c4016f0682..a0d767c3a6a71f4a9f5aeb7e4713f51471e3c295 100644 (file)
--- a/matita/components/ng_refiner/nCicUnifHint.ml
+++ b/matita/components/ng_refiner/nCicUnifHint.ml
@@ -11,6 +11,8 @@
 
 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
 
+module Ref = NReference
+
 let debug s = prerr_endline (Lazy.force s);;
 let debug _ = ();;
 
@@ -62,7 +64,10 @@ class virtual status =
    = fun o -> {< db = o#uhint_db >}
  end
 
-let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
+let dummy =
+ let uri = NUri.uri_of_string "cic:/matita/dummy/dec.con" in
+ NCic.Const (Ref.reference_of_spec uri Ref.Decl);;
+
 let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
 
 let index_hint status context t1 t2 precedence =
@@ -176,11 +181,11 @@ let db () =
               in 
               let n1 = 
                 NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri 
-                 u1 (NReference.Def h1)) :: mk_rels (List.length ctx))
+                 u1 (Ref.Def h1)) :: mk_rels (List.length ctx))
               in
               let n2 = 
                 NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri 
-                 u2 (NReference.Def h2)) :: mk_rels (List.length ctx))
+                 u2 (Ref.Def h2)) :: mk_rels (List.length ctx))
               in
                 [ctx,b1,b2; ctx,b1,n2; ctx,n1,b2; ctx,n1,n2]
               end else []