arithmetics for λδ

[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 4ea6e5ac3e4dd3ee47655f62a2ac1ed05254dc8f..c9e453cf20d6c0b69fd6870b635d27eb29c93c84 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -22,6 +22,9 @@ module NRef = NReference
 let debug_print s = prerr_endline (Lazy.force s);;
 let debug_print _ = ();;
 
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
+
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
   | _ -> assert false
@@ -325,12 +328,14 @@ let interpretate_term_and_interpretate_term_option
     | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
+         NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref
+    | CicNotationPt.NCic t -> t
     | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
+    | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
@@ -411,7 +416,7 @@ let new_flavour_of_flavour = function
   | `MutualDefinition -> `Definition 
   | `Fact -> `Fact
   | `Lemma -> `Lemma
-  | `Remark -> `Corollary
+  | `Remark -> `Example
   | `Theorem -> `Theorem
   | `Variant -> `Corollary 
   | `Axiom -> `Fact
@@ -434,7 +439,7 @@ let interpretate_obj
    interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
  let uri = match uri with | None -> assert false | Some u -> u in
  match obj with
- | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) ->
      let ty' = 
        interpretate_term 
          ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty 
@@ -443,11 +448,11 @@ let interpretate_obj
      uri, height, [], [], 
      (match bo,flavour with
       | None,`Axiom -> 
-          let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+          let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
           NCic.Constant ([],name,None,ty',attrs)
       | Some _,`Axiom -> assert false
       | None,_ ->
-          let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+          let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
           NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
       | Some bo,_ ->
         (match bo with
@@ -484,14 +489,14 @@ let interpretate_obj
                    ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
                  defs
              in
-             let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+             let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
              NCic.Fixpoint (inductive,inductiveFuns,attrs)
          | bo -> 
              let bo = 
                interpretate_term 
                 ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
              in
-             let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+             let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
              NCic.Constant ([],name,Some bo,ty',attrs)))
  | CicNotationPt.Inductive (params,tyl) ->
     let context,params =
@@ -606,7 +611,7 @@ let interpretate_obj
 ;;
 
 let disambiguate_term ~context ~metasenv ~subst ~expty
-   ~mk_implicit ~description_of_alias ~mk_choice
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~rdb ~lookup_in_library 
    (text,prefix_len,term) 
  =
@@ -615,7 +620,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_term
      ~context ~metasenv ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
      ~passes:(MultiPassDisambiguator.passes ())
@@ -628,7 +633,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
 ;;
 
 let disambiguate_obj 
-   ~mk_implicit ~description_of_alias ~mk_choice
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~rdb ~lookup_in_library ~uri
    (text,prefix_len,obj) 
  =
@@ -637,7 +642,7 @@ let disambiguate_obj
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_obj
      ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe 
      ~uri:(Some uri)