added override for \circ (notation for function composition)

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 6dbd312481a0c50e52ef7173787895a0a60bfb14..05a15691eb3d478e7e8a0e986babac1adb7640db 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -318,7 +318,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
         Cic.Meta (index, cic_subst)
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
-    | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+    | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
     | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
@@ -631,14 +631,14 @@ module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     CicNotationPt.term ->
-    (environment *                   (* new interpretation status *)
+    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.term*
      CicUniv.universe_graph) list *  (* disambiguated term *)
@@ -646,12 +646,12 @@ sig
 
   val disambiguate_obj :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
     GrafiteAst.obj ->
-    (environment *                   (* new interpretation status *)
+    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
      CicUniv.universe_graph) list *  (* disambiguated obj *)
@@ -690,8 +690,7 @@ module Make (C: Callbacks) =
            fun _ _ _ -> term))
         uris
 
-let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing"
-let disambiguate_environment_merge_profiler = CicUtil.profile "disambiguate_thing.disambiguate_environment_merge"
+let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv
       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
@@ -785,18 +784,18 @@ let disambiguate_environment_merge_profiler = CicUtil.profile "disambiguate_thin
 let foo () =
           let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
             (k , ugraph1 )
-in refine_profiler.CicUtil.profile foo ()
+in refine_profiler.HExtlib.profile foo ()
         with
         | Try_again -> Uncertain, ugraph
         | Invalid_choice -> Ko, ugraph
       in
       (* (4) build all possible interpretations *)
-      let rec aux aliases todo_dom base_univ =
+      let rec aux aliases diff todo_dom base_univ =
         match todo_dom with
         | [] ->
             (match test_env aliases [] base_univ with
             | Ok (thing, metasenv),new_univ -> 
-               [ aliases, metasenv, thing, new_univ ]
+               [ aliases, diff, metasenv, thing, new_univ ]
             | Ko,_ | Uncertain,_ -> [])
         | item :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
@@ -807,16 +806,17 @@ in refine_profiler.CicUtil.profile foo ()
               | codomain_item :: tl ->
                   debug_print (lazy (sprintf "%s CHOSEN" (fst codomain_item))) ;
                   let new_env = Environment.add item codomain_item aliases in
+                  let new_diff = (item,codomain_item)::diff in
                   (match test_env new_env remaining_dom univ with
                   | Ok (thing, metasenv),new_univ ->
                       (match remaining_dom with
-                      | [] -> [ new_env, metasenv, thing, new_univ ]
-                      | _ -> aux new_env remaining_dom new_univ )@ 
+                      | [] -> [ new_env, new_diff, metasenv, thing, new_univ ]
+                      | _ -> aux new_env new_diff remaining_dom new_univ )@ 
                         filter univ tl
                   | Uncertain,new_univ ->
                       (match remaining_dom with
                       | [] -> []
-                      | _ -> aux new_env remaining_dom new_univ )@ 
+                      | _ -> aux new_env new_diff remaining_dom new_univ )@ 
                         filter univ tl
                   | Ko,_ -> filter univ tl)
             in
@@ -825,16 +825,16 @@ in refine_profiler.CicUtil.profile foo ()
       let base_univ = initial_ugraph in
       try
         let res =
-         match aux aliases todo_dom base_univ with
+         match aux aliases [] todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
-         | [ e,me,t,u ] ->
+         | [_,diff,metasenv,t,ugraph] ->
              debug_print (lazy "SINGLE INTERPRETATION");
-             [ e,me,t,u ], false
+             [diff,metasenv,t,ugraph], false
          | l ->
              debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
              let choices =
                List.map
-                 (fun (env, _, _, _) ->
+                 (fun (env, _, _, _, _) ->
                    List.map
                      (fun domain_item ->
                        let description =
@@ -845,27 +845,10 @@ in refine_profiler.CicUtil.profile foo ()
                  l
              in
              let choosed = C.interactive_interpretation_choice choices in
-             (List.map (List.nth l) choosed), true
+             (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
+              true
         in
-(*
-        (if benchmark then
-          let res_size = List.length res in
-          debug_print (lazy (sprintf
-            ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
-            "BENCHMARK:   estimated %.2f")
-            !actual_refinements !max_refinements !domain_size res_size
-            !choices_avg
-            (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg))));
-*)
-      let choices, b = res in
-let foo () =
-      (List.map
-        (fun (env, metasenv, t, ugraph) ->
-          Environment.fold Environment.add env aliases,
-          metasenv, t, ugraph)
-        choices),
-      b
-in disambiguate_environment_merge_profiler.CicUtil.profile foo ()
+         res
      with
       CicEnvironment.CircularDependency s -> 
         failwith "Disambiguate: circular dependency"
@@ -909,7 +892,9 @@ struct
   let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
     ?(aliases = DisambiguateTypes.Environment.empty) term
   =
-    let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
+    let ast =
+      CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
+    in
     try
       fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
         ?initial_ugraph ~aliases ~universe:None)