Huge commit with several changes:

[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 288be5fa2d5b06fc11a51d4cd682a1b33c1f068c..749f1434d2f82a34337fdd9d245d2e377672a084 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -37,15 +37,26 @@ let rec string_context_of_context =
 ;;
 
 let refine_term metasenv subst context uri ~use_coercions
- term ugraph ~localization_tbl =
+ term expty ugraph ~localization_tbl =
 (*   if benchmark then incr actual_refinements; *)
   assert (uri=None);
   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
   let saved_use_coercions = !CicRefine.insert_coercions in
   try
     CicRefine.insert_coercions := use_coercions;
+    let term = 
+      match expty with
+      | None -> term
+      | Some ty -> Cic.Cast(term,ty)
+    in
     let term', _, metasenv',ugraph1 = 
            CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl
+    in
+    let term' = 
+      match expty, term' with
+      | None,_ -> term'
+      | Some _,Cic.Cast (term',_) -> term'
+      | _ -> assert false 
     in
      CicRefine.insert_coercions := saved_use_coercions;
      (Disambiguate.Ok (term', metasenv',[],ugraph1))
@@ -66,7 +77,7 @@ let refine_term metasenv subst context uri ~use_coercions
     in
      process_exn Stdpp.dummy_loc exn
 
-let refine_obj metasenv subst context uri ~use_coercions obj ugraph
+let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph
  ~localization_tbl =
    assert (context = []);
    assert (metasenv = []);
@@ -381,8 +392,10 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
                 List.fold_right (build_term inductiveFuns) inductiveFuns
                  cic_body)
     | CicNotationPt.Ident _
-    | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
-    | CicNotationPt.Ident (name, subst)
+    | CicNotationPt.Uri _
+    | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.NRef _ -> assert false
+    | CicNotationPt.Ident (name,subst)
     | CicNotationPt.Uri (name, subst) as ast ->
         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
         (try
@@ -484,11 +497,16 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
+    | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
+    | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~mk_choice ~env
          (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
-    | _ -> assert false (* god bless Bologna *)
+    | CicNotationPt.Variable _
+    | CicNotationPt.Magic _
+    | CicNotationPt.Layout _
+    | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
   and aux_option ~localize loc context annotation = function
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
@@ -623,26 +641,12 @@ let string_context_of_context =
   List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
   (Cic.Anonymous,_) -> Some "_");;
 
-let disambiguate_term ~context ~metasenv ~subst ?goal
+let disambiguate_term ~context ~metasenv ~subst ~expty 
   ?(initial_ugraph = CicUniv.oblivion_ugraph)
   ~mk_implicit ~description_of_alias ~mk_choice
   ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
 =
-  let hint = match goal with
-    | None -> (fun _ x -> x), fun k -> k
-    | Some i ->
-        (fun metasenv t ->
-          let _,c,ty = CicUtil.lookup_meta i metasenv in
-          assert(c=context);
-          Cic.Cast(t,ty)),
-        function  
-        | Disambiguate.Ok (t,m,s,ug) ->
-            (match t with
-            | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug)
-            | _ -> assert false) 
-        | k -> k
-  in
-  let localization_tbl = Cic.CicHash.create 503 in
+  let mk_localization_tbl x = Cic.CicHash.create x in
    MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
     ~initial_ugraph ~aliases ~string_context_of_context
     ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
@@ -650,16 +654,15 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
     ~domain_of_thing:Disambiguate.domain_of_term
     ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
     ~refine_thing:refine_term (text,prefix_len,term)
-    ~localization_tbl
-    ~hint
+    ~mk_localization_tbl
+    ~expty
     ~freshen_thing:CicNotationUtil.freshen_term
     ~passes:(MultiPassDisambiguator.passes ())
 
 let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
  ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
 =
-  let hint = (fun _ x -> x), fun k -> k in
-  let localization_tbl = Cic.CicHash.create 503 in
+  let mk_localization_tbl x = Cic.CicHash.create x in
   MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] 
     ~aliases ~universe ~uri ~string_context_of_context
     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
@@ -668,8 +671,8 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
     ~initial_ugraph:CicUniv.empty_ugraph
     ~interpretate_thing:(interpretate_obj ~mk_choice)
     ~refine_thing:refine_obj
-    ~localization_tbl
-    ~hint
+    ~mk_localization_tbl
+    ~expty:None
     ~passes:(MultiPassDisambiguator.passes ())
     ~freshen_thing:CicNotationUtil.freshen_obj
     (text,prefix_len,obj)