* http://cs.unibo.it/helm/.
*)
-let expect_possible_parameters = ref false;;
-
-exception NotExpectingPossibleParameters;;
-
(* converts annotated terms into cic terms (forgetting ids and names) *)
let rec deannotate_term =
let module C = Cic in
function
- C.ARel (_,n,_) -> C.Rel n
- | C.AVar (_,uri) -> C.Var uri
+ C.ARel (_,_,n,_) -> C.Rel n
+ | C.AVar (_,uri,exp_named_subst) ->
+ let deann_exp_named_subst =
+ List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst
+ in
+ C.Var (uri, deann_exp_named_subst)
| C.AMeta (_,n, l) ->
let l' =
List.map
| C.ALetIn (_,name,so,ta) ->
C.LetIn (name, deannotate_term so, deannotate_term ta)
| C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
- | C.AConst (_,uri, cookingsno) -> C.Const (uri, cookingsno)
- | C.AMutInd (_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i)
- | C.AMutConstruct (_,uri,cookingsno,i,j) ->
- C.MutConstruct (uri,cookingsno,i,j)
- | C.AMutCase (_,uri,cookingsno,i,outtype,te,pl) ->
- C.MutCase (uri,cookingsno,i,deannotate_term outtype,
+ | C.AConst (_,uri,exp_named_subst) ->
+ let deann_exp_named_subst =
+ List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst
+ in
+ C.Const (uri, deann_exp_named_subst)
+ | C.AMutInd (_,uri,i,exp_named_subst) ->
+ let deann_exp_named_subst =
+ List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst
+ in
+ C.MutInd (uri,i,deann_exp_named_subst)
+ | C.AMutConstruct (_,uri,i,j,exp_named_subst) ->
+ let deann_exp_named_subst =
+ List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst
+ in
+ C.MutConstruct (uri,i,j,deann_exp_named_subst)
+ | C.AMutCase (_,uri,i,outtype,te,pl) ->
+ C.MutCase (uri,i,deannotate_term outtype,
deannotate_term te, List.map deannotate_term pl)
| C.AFix (_,funno,ifl) ->
C.Fix (funno, List.map deannotate_inductiveFun ifl)
| C.ACoFix (_,funno,ifl) ->
C.CoFix (funno, List.map deannotate_coinductiveFun ifl)
-and deannotate_inductiveFun (name,index,ty,bo) =
+and deannotate_inductiveFun (_,name,index,ty,bo) =
(name, index, deannotate_term ty, deannotate_term bo)
-and deannotate_coinductiveFun (name,ty,bo) =
+and deannotate_coinductiveFun (_,name,ty,bo) =
(name, deannotate_term ty, deannotate_term bo)
;;
-let deannotate_inductiveType (name, isinductive, arity, cons) =
+let deannotate_inductiveType (_, name, isinductive, arity, cons) =
(name, isinductive, deannotate_term arity,
- List.map (fun (id,ty,recs) -> (id,deannotate_term ty, recs)) cons)
+ List.map (fun (id,ty) -> (id,deannotate_term ty)) cons)
;;
let deannotate_obj =
let module C = Cic in
function
- C.ADefinition (_, id, bo, ty, params) ->
- (match params with
- C.Possible params ->
- if !expect_possible_parameters then
- C.Definition (id, deannotate_term bo, deannotate_term ty, params)
- else
- raise NotExpectingPossibleParameters
- | C.Actual params ->
- C.Definition (id, deannotate_term bo, deannotate_term ty, params)
- )
- | C.AAxiom (_, id, ty, params) ->
- C.Axiom (id, deannotate_term ty, params)
- | C.AVariable (_, name, bo, ty) ->
+ C.AConstant (_, _, id, bo, ty, params) ->
+ C.Constant (id,
+ (match bo with None -> None | Some bo -> Some (deannotate_term bo)),
+ deannotate_term ty, params)
+ | C.AVariable (_, name, bo, ty, params) ->
C.Variable (name,
(match bo with None -> None | Some bo -> Some (deannotate_term bo)),
- deannotate_term ty)
- | C.ACurrentProof (_, name, conjs, bo, ty) ->
+ deannotate_term ty, params)
+ | C.ACurrentProof (_, _, name, conjs, bo, ty, params) ->
C.CurrentProof (
name,
List.map
List.map
(function
_,Some (n,(C.ADef at)) ->
- Some (n,(C.Def (deannotate_term at)))
+ Some (n,(C.Def ((deannotate_term at),None)))
| _,Some (n,(C.ADecl at)) ->
Some (n,(C.Decl (deannotate_term at)))
| _,None -> None
in
(id,context,deannotate_term con)
) conjs,
- deannotate_term bo,deannotate_term ty
+ deannotate_term bo,deannotate_term ty,params
)
| C.AInductiveDefinition (_, tys, params, parno) ->
- C.InductiveDefinition ( List.map deannotate_inductiveType tys,
+ C.InductiveDefinition (List.map deannotate_inductiveType tys,
params, parno)
;;