with NCicLibrary.ObjectNotFound _ -> NReference.string_of_reference r
;;
-let nast_of_cic =
+let nast_of_cic ~subst =
let rec k = function
- | NCic.Rel n -> Ast.Ident (string_of_int n, None)
+ | NCic.Rel n -> Ast.Ident ("-" ^ string_of_int n, None)
| NCic.Const r -> Ast.Ident (r2s true r, None)
+ | NCic.Meta (n,lc) when List.mem_assoc n subst ->
+ let _,_,t,_ = List.assoc n subst in
+ k (*ctx*) (NCicSubstitution.subst_meta lc t)
| NCic.Meta (n,l) -> Ast.Meta (n, [](*aux_context l*))
| NCic.Sort NCic.Prop -> Ast.Sort `Prop
| NCic.Sort NCic.Type _ -> Ast.Sort `Set
Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k s)), k t)
| NCic.LetIn (n,s,ty,t) ->
Ast.LetIn ((Ast.Ident (n,None), Some (k ty)), k s, k t)
+ | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst ->
+ let _,_,t,_ = List.assoc n subst in
+ let hd = NCicSubstitution.subst_meta lc t in
+ k (*ctx*)
+ (NCicReduction.head_beta_reduce ~upto:(List.length args)
+ (match hd with
+ | NCic.Appl l -> NCic.Appl (l@args)
+ | _ -> NCic.Appl (hd :: args)))
| NCic.Appl args -> Ast.Appl (List.map k args)
(*| NCic.AConst (id,uri,substs) ->
register_uri id uri;
k
;;
-let map_sequent (i,(n,context,ty):int * NCic.conjecture) =
+let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
let module K = Content in
let context' =
List.map