* The interface of CicTypeChecker now allows the usage of definitions in

[helm.git] / helm / gTopLevel / cic2acic.ml

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 677d633e51215050687132a951ee6f5f277b22d3..ec9dc680e376c0a3ae0ddbf888775d6ad208501b 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -110,7 +110,7 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
         | C.Prod (n,s,t) ->
             Hashtbl.add ids_to_inner_sorts fresh_id''
              (string_of_sort innertype) ;
-            C.AProd (fresh_id'', n, aux' bs s, aux' ((n,s)::bs) t)
+            C.AProd (fresh_id'', n, aux' bs s, aux' ((n, C.Decl s)::bs) t)
         | C.Lambda (n,s,t) ->
            Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
            if innersort = "Prop" then
@@ -126,12 +126,10 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
               if not father_is_lambda then
                add_inner_type fresh_id''
             end ;
-           C.ALambda (fresh_id'',n, aux' bs s, aux' ((n,s)::bs) t)
+           C.ALambda (fresh_id'',n, aux' bs s, aux' ((n, C.Decl s)::bs) t)
         | C.LetIn (n,s,t) ->
-(*CSC: Nell'environment debbo poter avere anche dichiarazioni! ;-(
           Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
-          C.ALetIn (fresh_id'', n, aux' bs s, aux' (n::bs) t)
-*) assert false
+          C.ALetIn (fresh_id'', n, aux' bs s, aux' ((n, C.Def s)::bs) t)
         | C.Appl l ->
            Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
            if innersort = "Prop" then
@@ -152,7 +150,9 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
            C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty,
             aux' bs term, List.map (aux' bs) patterns)
         | C.Fix (funno, funs) ->
-           let names = List.map (fun (name,_,ty,_) -> C.Name name,ty) funs in
+           let names =
+            List.map (fun (name,_,ty,_) -> C.Name name, C.Decl ty) funs
+           in
             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop" then
              add_inner_type fresh_id'' ;
@@ -163,7 +163,8 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
               ) funs
            )
         | C.CoFix (funno, funs) ->
-           let names = List.map (fun (name,ty,_) -> C.Name name,ty) funs in
+           let names =
+            List.map (fun (name,ty,_) -> C.Name name, C.Decl ty) funs in
             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop" then
              add_inner_type fresh_id'' ;
@@ -188,7 +189,7 @@ let acic_of_cic_env metasenv env t =
    ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
 ;;
 
-exception Found of (Cic.name * Cic.term) list;;
+exception Found of (Cic.name * Cic.context_entry) list;;
 
 (* get_context_of_meta meta term                                 *)
 (* returns the context of the occurrence of [meta] in [term].    *)
@@ -205,10 +206,9 @@ let get_context_of_meta meta term =
     | C.Sort _
     | C.Implicit -> ()
     | C.Cast (te,ty) -> aux ctx te ; aux ctx ty
-    | C.Prod (n,s,t) -> aux ctx s ; aux (((*P.Declaration,*)n,s)::ctx) t
-    | C.Lambda (n,s,t) -> aux ctx s ; aux (((*P.Declaration,*)n,s)::ctx) t
-    | C.LetIn (n,s,t) ->
-       aux ctx s ; assert false (* aux ([P.Definition,n,s]::ctx) t *)
+    | C.Prod (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
+    | C.Lambda (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
+    | C.LetIn (n,s,t) -> aux ctx s ; aux ((n, C.Def s)::ctx) t
     | C.Appl l -> List.iter (aux ctx) l
     | C.Const _ -> ()
     | C.Abst _ -> assert false
@@ -221,7 +221,7 @@ let get_context_of_meta meta term =
         let ctx' =
          List.rev_map
           (function (name,_,ty,bo) ->
-            let res = ((*P.Definition,*) C.Name name, C.Fix (!counter,ifl)) in
+            let res = (C.Name name, C.Def (C.Fix (!counter,ifl))) in
              incr counter ;
              res
           ) ifl
@@ -233,7 +233,7 @@ let get_context_of_meta meta term =
         let ctx' =
          List.rev_map
           (function (name,ty,bo) ->
-            let res = ((*P.Definition,*) C.Name name, C.CoFix (!counter,ifl)) in
+            let res = (C.Name name, C.Def (C.CoFix (!counter,ifl))) in
              incr counter ;
              res
           ) ifl