snapshot

[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 27122ef1deaf635f594d2931d2a606046fc81069..6848338c3bf06b5c09659bacf069df8deb1385ed 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -119,7 +119,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
         resolve env (Symbol (symb, i)) ~args:cic_args ()
     | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
     | CicAst.Binder (binder_kind, (var, typ), body) ->
-        let cic_type = aux_option loc context typ in
+        let cic_type = aux_option loc context (Some `Type) typ in
         let cic_body = aux loc (var :: context) body in
         (match binder_kind with
         | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
@@ -129,7 +129,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
     | CicAst.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux loc context term in
-        let cic_outtype = aux_option loc context outtype in
+        let cic_outtype = aux_option loc context None outtype in
         let do_branch ((head, args), term) =
           let rec do_branch' context = function
             | [] -> aux loc context term
@@ -184,7 +184,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
           List.map
             (fun ((name, typ), body, decr_idx) ->
               let cic_body = aux loc context' body in
-              let cic_type = aux_option loc context typ in
+              let cic_type = aux_option loc context (Some `Type) typ in
               let name =
                 match name with
                 | Cic.Anonymous ->
@@ -230,7 +230,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
           let cic =
             if is_uri ast then  (* we have the URI, build the term out of it *)
               try
-                CicUtil.term_of_uri name
+                CicUtil.term_of_uri (UriManager.uri_of_string name)
               with UriManager.IllFormedUri _ ->
                 CicTextualParser2.fail loc "Ill formed URI"
             else
@@ -311,8 +311,8 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
-  and aux_option loc context = function
-    | None -> Cic.Implicit (Some `Type)
+  and aux_option loc context annotation = function
+    | None -> Cic.Implicit annotation
     | Some term -> aux loc context term
   in
   match ast with
@@ -412,14 +412,16 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
      let field_names = List.map fst fields in
       Cic.InductiveDefinition
        (tyl,[],List.length params,[`Class (`Record field_names)])
-  | TacticAst.Theorem (_,name,ty,bo) ->
+  | TacticAst.Theorem (flavour, name, ty, bo) ->
+     let attrs = [`Flavour flavour] in
      let ty' = interpretate_term [] env None false ty in
-     match bo with
+     (match bo with
         None ->
-         Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],[])
+         Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
       | Some bo ->
          let bo' = Some (interpretate_term [] env None false bo) in
-          Cic.Constant (name,bo',ty',[],[])
+          Cic.Constant (name,bo',ty',[],attrs))
+          
 
   (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
 let rev_uniq =
@@ -559,7 +561,12 @@ let domain_of_obj ~context ast =
            List.flatten (
             List.rev_map
              (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
-            domain_rev_of_term [] ty) tyl)
+            domain_rev_of_term [] ty) tyl) in
+      let dom = 
+       List.fold_left
+        (fun dom (_,ty) ->
+          domain_rev_of_term [] ty @ dom
+        ) dom params
       in
        List.filter
         (fun name ->
@@ -570,14 +577,17 @@ let domain_of_obj ~context ast =
       let dom =
        List.flatten
         (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
-      let dom' =
+      let dom =
        List.filter
         (fun name->
           not (  List.exists (fun (name',_) -> name = Id name') params
               || List.exists (fun (name',_) -> name = Id name') fields)
         ) dom
       in
-       dom' @ domain_rev_of_term [] ty
+       List.fold_left
+        (fun dom (_,ty) ->
+          domain_rev_of_term [] ty @ dom
+        ) (dom @ domain_rev_of_term [] ty) params
  in
   rev_uniq domain_rev
 
@@ -638,7 +648,7 @@ module Make (C: Callbacks) =
           (UriManager.string_of_uri uri,
            let term =
              try
-               CicUtil.term_of_uri (UriManager.string_of_uri uri)
+               CicUtil.term_of_uri uri
              with exn ->
                debug_print (UriManager.string_of_uri uri);
                debug_print (Printexc.to_string exn);