- (* "envl" is a list of triples:
- * <name environment, term environment, pattern id>, where
- * name environment: (string * string) list
- * term environment: (string * Cic.annterm) list *)
-let return_closure success_k =
- (fun term_info terms envl ->
-(* prerr_endline "return_closure"; *)
- match terms with
- | [] ->
- (try
- success_k term_info (List.hd envl)
- with Failure _ -> assert false)
- | _ -> assert false)
-
-let variable_closure names k =
- (fun term_info terms envl ->
-(* prerr_endline "variable_closure"; *)
- match terms with
- | hd :: tl ->
- let envl' =
- List.map2
- (fun arg (name_env, term_env, pid) ->
- let rec aux name_env term_env pid arg term =
- match arg, term with
- Ast.IdentArg name, _ ->
- (name_env, (name, term) :: term_env, pid)
- | Ast.EtaArg (Some name, arg'),
- Cic.ALambda (id, name', ty, body) ->
- aux
- ((name, (string_of_name name', Some (ty, id))) :: name_env)
- term_env pid arg' body
- | Ast.EtaArg (Some name, arg'), _ ->
- let name' = CicNotationUtil.fresh_name () in
- aux ((name, (name', None)) :: name_env)
- term_env pid arg' term
- | Ast.EtaArg (None, arg'), Cic.ALambda (id, name, ty, body) ->
- assert false
- | Ast.EtaArg (None, arg'), _ ->
- assert false
- in
- aux name_env term_env pid arg hd)
- names envl
- in
- k term_info tl envl'
- | _ -> assert false)
-
-let appl_closure ks k =
- (fun term_info terms envl ->
-(* prerr_endline "appl_closure"; *)
- (match terms with
- | Cic.AAppl (_, args) :: tl ->
- (try
- let k' = List.assoc (List.length args) ks in
- k' term_info (args @ tl) envl
- with Not_found -> k term_info terms envl)
- | [] -> assert false
- | _ -> k term_info terms envl))
-
-let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
-
-let uri_closure ks k =
- (fun term_info terms envl ->
-(* prerr_endline "uri_closure"; *)
- (match terms with
- | [] -> assert false
- | hd :: tl ->
-(* prerr_endline (sprintf "uri_of_term = %s" (uri_of_term hd)); *)
- begin