struct
type path_string_elem =
- | Function | Constant of UriManager.uri
- | Bound of int | Variable | Proposition | Datatype ;;
+ | Constant of UriManager.uri
+ | Bound of int | Variable | Proposition | Datatype | Dead;;
type path_string = path_string_elem list;;
* "functions" *)
let ppelem = function
- | Function -> "Fun"
| Constant uri -> UriManager.name_of_uri uri
| Bound i -> string_of_int i
| Variable -> "?"
| Proposition -> "Prop"
| Datatype -> "Type"
+ | Dead -> "DEAD"
;;
let pppath l = String.concat "::" (List.map ppelem l) ;;
let elem_of_cic = function
- | Cic.Meta _ -> Variable
- | Cic.Lambda _ -> Function
+ | Cic.Meta _ | Cic.Implicit _ -> Variable
| Cic.Rel i -> Bound i
| Cic.Sort (Cic.Prop) -> Proposition
| Cic.Sort _ -> Datatype
- | term ->
- try Constant (CicUtil.uri_of_term term)
- with Invalid_argument _ -> Variable (* HACK! *)
+ | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
+ (try Constant (CicUtil.uri_of_term t)
+ with Invalid_argument _ -> assert false)
+ | Cic.Appl _ ->
+ assert false (* should not happen *)
+ | Cic.LetIn _ | Cic.Lambda _ | Cic.Prod _ | Cic.Cast _
+ | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ ->
+ prerr_endline "FIXME: the trie receives an invalid term";
+ Dead
+ (* assert false universe.ml removes these *)
;;
let path_string_of_term arities =
let set_arity arities k n =
(assert (k<>Variable || n=0);
- (k,n)::(List.remove_assoc k arities))
+ if k = Dead then arities else (k,n)::(List.remove_assoc k arities))
in
let rec aux arities = function
| Cic.Appl ((hd::tl) as l) ->