Universes introduction

[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 06f18080d07466aaccba41ca71b3d83599ae4678..139a6417a3c33c6f6f4fb4328794ac4802a5195c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -57,13 +57,14 @@ let refine metasenv context term =
     | CicRefine.Uncertain _ ->
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
-    | _ ->
-        (* TODO we should catch only the RefineFailure excecption *)
+    | CicRefine.RefineFailure _ ->
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
-  snd (Environment.find item env) env num args
+  try
+    snd (Environment.find item env) env num args
+  with Not_found -> assert false
 
   (* TODO move it to Cic *)
 let find_in_environment name context =
@@ -180,10 +181,9 @@ let interpretate ~context ~env ast =
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
     | CicAst.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
+          if subst <> None then
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           Cic.Rel index
@@ -193,12 +193,16 @@ let interpretate ~context ~env ast =
             let ids_to_uris =
               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
             in
-            List.map
-              (fun (s, term) ->
-                (try
-                  List.assoc s ids_to_uris, aux loc context term
-                 with Not_found -> raise DisambiguateChoices.Invalid_choice))
-              subst
+            (match subst with
+            | Some subst ->
+                List.map
+                  (fun (s, term) ->
+                    (try
+                      List.assoc s ids_to_uris, aux loc context term
+                     with Not_found ->
+                       raise DisambiguateChoices.Invalid_choice))
+                  subst
+            | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
          in
           (match cic with
           | Cic.Const (uri, []) ->
@@ -253,7 +257,7 @@ let interpretate ~context ~env ast =
         Cic.Meta (index, cic_subst)
     | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
     | CicAst.Sort `Set -> Cic.Sort Cic.Set
-    | CicAst.Sort `Type -> Cic.Sort Cic.Type
+    | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
@@ -274,10 +278,15 @@ let domain_of_term ~context ast =
     | CicAst.AttributedTerm (_, term) -> aux loc context term
     | CicAst.Appl terms ->
         List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
-    | CicAst.Binder (_, (var, typ), body) ->
+    | CicAst.Binder (kind, (var, typ), body) ->
+        let kind_dom =
+          match kind with
+          | `Exists -> [ Symbol ("exists", 0) ]
+          | _ -> []
+        in
         let type_dom = aux_option loc context typ in
         let body_dom = aux loc (var :: context) body in
-        body_dom @ type_dom
+        body_dom @ type_dom @ kind_dom
     | CicAst.Case (term, indty_ident, outtype, branches) ->
         let term_dom = aux loc context term in
         let outtype_dom = aux_option loc context outtype in
@@ -317,19 +326,22 @@ let domain_of_term ~context ast =
         in
         where_dom @ defs_dom
     | CicAst.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
+          if subst <> None then
             CicTextualParser2.fail loc
-              "Explicit substitutions not allowed here";
-          []
+              "Explicit substitutions not allowed here"
+          else
+            []
         with Not_found ->
-          List.fold_left
-            (fun dom (_, term) ->
-              let dom' = aux loc context term in
-              dom' @ dom)
-            [ Id name ] subst)
+          (match subst with
+          | None -> [Id name]
+          | Some subst ->
+              List.fold_left
+                (fun dom (_, term) ->
+                  let dom' = aux loc context term in
+                  dom' @ dom)
+                [Id name] subst))
     | CicAst.Implicit -> []
     | CicAst.Num (num, i) -> [ Num i ]
     | CicAst.Meta (index, local_context) ->
@@ -391,13 +403,6 @@ module Make (C: Callbacks) =
        (function uri,_ ->
          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
        ) result in
-      HelmLogger.log (`Msg (`T "Locate query:"));
-      MQueryUtil.text_of_query
-       (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s)))
-       "" query; 
-      HelmLogger.log (`Msg (`T "Result:"));
-      MQueryUtil.text_of_result
-        (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
       let uris' =
        match uris with
         | [] ->
@@ -484,7 +489,7 @@ module Make (C: Callbacks) =
         match todo_dom with
         | [] ->
             (match test_env current_env [] with
-            | Ok (term, metasenv) -> [ current_env, term, metasenv ]
+            | Ok (term, metasenv) -> [ current_env, metasenv, term ]
             | Ko | Uncertain -> [])
         | item :: remaining_dom ->
             debug_print (sprintf "CHOOSED ITEM: %s"
@@ -500,7 +505,7 @@ module Make (C: Callbacks) =
                   (match test_env new_env remaining_dom with
                   | Ok (term, metasenv) ->
                       (match remaining_dom with
-                      | [] -> [ new_env, term, metasenv ]
+                      | [] -> [ new_env, metasenv, term ]
                       | _ -> aux new_env remaining_dom) @ filter tl
                   | Uncertain ->
                       (match remaining_dom with
@@ -510,30 +515,27 @@ module Make (C: Callbacks) =
             in
             filter choices
       in
-      let (choosed_env, choosed_term, choosed_metasenv) =
-        match aux current_env todo_dom with
-        | [] -> raise NoWellTypedInterpretation
-        | [ x ] ->
-            debug_print "UNA SOLA SCELTA";
-            x
-        | l ->
-            debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
-            let choices =
-              List.map
-                (fun (env, _, _) ->
-                  List.map
-                    (fun domain_item ->
-                      let description =
-                        fst (Environment.find domain_item env)
-                      in
-                      (descr_of_domain_item domain_item, description))
-                    term_dom)
-                l
-            in
-            let choosed = C.interactive_interpretation_choice choices in
-            List.nth l choosed
-      in
-      (choosed_env, choosed_metasenv, choosed_term)
+       match aux current_env todo_dom with
+       | [] -> raise NoWellTypedInterpretation
+       | [ _ ] as l ->
+           debug_print "UNA SOLA SCELTA";
+           l
+       | l ->
+           debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
+           let choices =
+             List.map
+               (fun (env, _, _) ->
+                 List.map
+                   (fun domain_item ->
+                     let description =
+                       fst (Environment.find domain_item env)
+                     in
+                     (descr_of_domain_item domain_item, description))
+                   term_dom)
+               l
+           in
+           let choosed = C.interactive_interpretation_choice choices in
+            List.map (List.nth l) choosed
 
   end